separationLogic/src/vars_as_resourceFunctor.sml

330    val (xenv,penv,prog,abst) = dest_ASL_PROGRAM_IS_ABSTRACTION tt
333    val thm0 = ISPECL [xenv,penv,qP,prog,qQ] ASL_PROGRAM_IS_ABSTRACTION___var_res_quant_best_local_action
584 fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t)
586 val t = ``ASL_PROGRAM_IS_ABSTRACTION xenv penv (var_res_prog_local_var (\v. body v 2))``;
587 val xenv = el 1 (snd (strip_comb t));
592 fun ASL_PROGRAM_ABSTRACTION___local_var pf abstL sys xenv penv p =
597       val body_thm_opt = sys xenv penv body;
601       val thm0 = ISPECL [xenv, penv] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_local_var___CONG
609 fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t)
611 val t = ``ASL_PROGRAM_IS_ABSTRACTION xenv penv (var_res_prog_call_by_value_arg (\v. body v 2) c)``;
612 val xenv = el 1 (snd (strip_comb t));
617 fun ASL_PROGRAM_ABSTRACTION___call_by_value_arg pf abstL sys xenv penv p =
622       val body_thm_opt = sys xenv penv body;
626       val thm0 = ISPECL [xenv,penv,c] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_call_by_value_arg___CONG
636 fun sys xenv penv t = SOME (prove_ASL_PROGRAM_ABSTRACTION_REFL xenv penv t)
642 val xenv = el 1 (snd (strip_comb t));
647 fun ASL_PROGRAM_ABSTRACTION___eval_expressions pf abstL sys xenv penv p =
653       val body_thm_opt = sys xenv penv body;
657       val thm0 = ISPECL [xenv,penv,expL] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_eval_expressions;
671 val xenv = el 1 (snd (strip_comb t));
678 val (abstL, sys, xenv,penv,p) = el 3 (!t_opt)
681 fun ASL_PROGRAM_ABSTRACTION___var_res_prog_procedure_call pf abstL sys xenv penv p =
684       val thm0 = ISPECL [xenv,penv,name,args] ASL_PROGRAM_IS_ABSTRACTION___var_res_prog_procedure_call
712 val xenv = el 1 (snd (strip_comb t));
719 val SOME (abstL, xenv,penv,p) = !t_opt
727 fun ASL_PROGRAM_ABSTRACTION___var_res_prog_parallel_procedure_call pf abstL sys xenv penv p =
731       val thm0 = ISPECL [xenv,penv,args1,args2,name1,name2]
774 val xenv = el 1 (snd (strip_comb t));
782 val _ = t_opt := SOME (abstL, sys, xenv,penv,p);
783 val SOME (abstL, sys, xenv,penv,p) = !t_opt
794 fun ASL_PROGRAM_ABSTRACTION___var_res_cond_critical_section pf abstL sys xenv penv p =
798       (*destruct the xenv*)
799       val (_, lock_env) = pairLib.dest_pair xenv;
867      val sys_thm_opt =  sys xenv penv p2;
872              val xthm1 = ISPECL [xenv, penv, p1, p2, p3] ASL_PROGRAM_IS_ABSTRACTION___TRANSITIVE;
1086     val (xenv, penv) = let (* a crude, but robust and simple way *)
1090          val xenv = rand (rator t0)
1092          (xenv, penv)
1095           ASL_PROGRAM_ABSTRACTION___block_flatten___no_rec xenv penv prog1
3339 fun profile_program_abst s a abstL sys xenv penv =
3340    Profile.profile s (fn p => (a abstL sys xenv penv p)