decidable_separationLogic/src/decidable_separationLogicLib.sml

161    val sf = ``sf_bin_tree (f1,f2) e``
171       val (f1,f2) = pairLib.dest_pair (el 1 args)
172       val _ = if f1 = f2 then (SMALLFOOT_ERR "NO SF_BIN_TREE!") else ();
174       (f1,f2, el 2 args, el 1 args)
179    val sf = ``sf_tree (f1::f2::l) e1 e2``
181    val sf = ``sf_bin_tree (f1,f2) e``
205       val (f1, f2, e, _) = dest_sf_bin_tree sf;
209       (sf, ([f1,f2], mk_list ([], type_of f1)), es, e)
219    val sf = ``sf_points_to e ((f1, e1)::(f2,e2)::l)``
541 val t = ``LIST_DS_ENTAILS ([], [(e1,e2);(e9,e9)]) ((pf1::pf_equal e e::pf_true::pf2::pf_equal e' e'::pf3::l),(sf1::sf2::(sf_ls f e e) ::sf3::(sf_points_to e [(f, e)])::(sf_bin_tree (f1, f2) dse_nil)::(sf_tree fL e2 e2)::(sf_ls f e1 e2)::l2)) ((pf1::pfx::pf_equal e e::pf2::pf_equal e' e'::pf3::l),(sf1::sf2::(sf_ls f e2 e2) ::sf3::sf_emp::(sf_points_to e [(f, e)])::(sf_bin_tree (f1, f2) e)::(sf_tree fL e1 e2)::(sf_ls f e e)::l3))``
618       val (f2, p2) = get_pf_trival_filter pf;
625       val thm = ISPECL [f1, f2,f3,f4, f5, c1, c2, pf, sf, pf', sf'] INFERENCE_TRIVIAL_FILTER;
637 val t = ``LIST_DS_ENTAILS (e1::e45::e6::e45::dse_nil::c1,c2) ([pf1;pf_unequal e e;pf2],[sf_points_to e3 []; sf_points_to dse_nil [];sf_bin_tree (f1, f2) e1]) ([],[])``
951       val (f2, p2) = get_hypothesis_filter cL pfL pfL';
955       val thm = ISPECL [f1, f2, c1, c2, pf, sf, pf', sf']
1311                  (LIST_PRODUCT (SF_POINTS_TO_LIST_COND_FILTER pfL f2 sfL)
1314                     (SF_POINTS_TO_LIST_COND_FILTER pfL f2 (sfL:('c, 'b, 'a) ds_spatial_formula list))``;
1324 fun EVAL___DISJOINT_LIST_PRODUCT c1 pf sf f2 =
1332              mk_var("f2",type_of f2) |-> f2,
1369       val f2 = mk_list (f2L, Type `:pointsto_cases`);
1372       val SF_POINTS_TO_LIST___THM = EVAL___DISJOINT_LIST_PRODUCT c1 pf sf f2;
1380       val thm = ISPECL [f, f2, c1, c2, pf, sf, pf', sf'] INFERENCE_PARTIAL___EVAL
1603 val t = ``LIST_DS_ENTAILS ([e1],[(e2,e3)]) ([pf_unequal e3 e1;pf1;pf_unequal e2 e4; pf3],[sf_ls "g" e5 e7; sf_ls "f" dse_nil e3;sf_points_to e1 [("g", x); ("f", y)]; sf1;sf2]) ([],[sf_bin_tree ("f1","f2") e1])``
1627          val (f1,f2, ex, _) = dest_sf_bin_tree h;
1631          val e2 = snd (first (fn (x,y) => x = f2) pointer_list);
1633          SOME (n, n2, ex, e1, e2, f1, f2, a)
1669       val (n, n2, ex, e1, e2, f1, f2, a) = valOf searchOpt;
1671             ex, e1, e2, f1, f2, a, c1, c2, pf, sf, pf', sf']
1691 val t = ``LIST_DS_ENTAILS (c1,c2) ([],[sf1;sf3;sf_bin_tree ("f1","f2") e;sf2]) ([],[])``
1781       val (f1,f2, e1, _) = dest_sf_bin_tree tree_term;
1784             e1, f1, f2, c1, c2, pf, sf, pf', sf']