Lines Matching defs:e1
146 val sf = ``sf_ls f e1 e2``
179 val sf = ``sf_tree (f1::f2::l) e1 e2``
180 val sf = ``sf_ls f e1 e2``
219 val sf = ``sf_points_to e ((f1, e1)::(f2,e2)::l)``
272 fun is_uneq_2 e1 e2 pf =
274 val (e1', e2') = dest_pf_unequal pf;
276 ((e1 = e1') andalso (e2 = e2')) orelse
277 ((e2 = e1') andalso (e1 = e2'))
280 fun is_eq_2 e1 e2 pf =
282 val (e1', e2') = dest_pf_equal pf;
284 ((e1 = e1') andalso (e2 = e2')) orelse
285 ((e2 = e1') andalso (e1 = e2'))
290 val (e1, e2) = dest_pf_unequal pf;
292 ((e1 = ex) andalso (is_dse_nil e2)) orelse
293 ((e2 = ex) andalso (is_dse_nil e1))
299 val (e1, e2) = dest_pf_equal pf;
301 e1 = e2
307 val (e1, e2) = dest_pf_unequal pf;
309 e1 = e2
315 val (f, e1, e2) = dest_sf_ls sf;
317 e1 = e2
323 val (f, e1, e2) = dest_sf_ls sf
325 (e1 = e2)
339 val (_, e1, e2) = dest_sf_tree sf
341 (e1 = e2)
370 val (e1, e2) = dest_pf_equal pf1;
371 val (e1', e2') = dest_pf_equal pf2;
373 ((e1 = e2') andalso (e2 = e1'), true) (*e1 = e1' ... => pf1 = pf2*)
378 val (e1, e2) = dest_pf_unequal pf1;
379 val (e1', e2') = dest_pf_unequal pf2;
381 ((e1 = e2') andalso (e2 = e1'), true) (*e1 = e1' ... => pf1 = pf2*)
390 val (_, e1, _) = dest_sf_ls t;
392 is_dse_nil e1
484 val t = ``LIST_DS_ENTAILS ([e3;e4], [(e5,e6);(e8,e8)]) ((pf_equal e1 e2::pf_unequal dse_nil e2::pf_equal e1 e2::l),[]) ((pf_equal e1 e2::pf_unequal e1 e2::pf_equal e1 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))``
576 val (e1, e2) = pairLib.dest_pair t;
578 (e1 = e2)
636 val t = ``LIST_DS_ENTAILS (e1::c1,c2) ([pf1;pf_unequal e3 e;pf2],[sf_points_to e1 []; sf_points_to dse_nil []]) ([],[])``
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]) ([],[])``
809 val (e1, e2) = dest_pf_equal pf;
811 (not (e1 = e2)) andalso ((is_dse_var e1) orelse (is_dse_var e2))
821 val (e1, e2) = dest_pf_equal uneq;
822 val (inf, e1, e2) = if (is_dse_var e1) then (INFERENCE_SUBSTITUTION___EVAL1, e1, e2) else
823 (INFERENCE_SUBSTITUTION___EVAL2, e2, e1);
825 val thm = ISPECL [numLib.term_of_int n, e2, dest_dse_var e1, c1, c2, pf, sf, pf', sf'] inf;
838 val t = ``LIST_DS_ENTAILS ([e7;e5;e4;e6], []) ([pf_unequal e1 e2;pf1;pf_unequal dse_nil e5;pf2;pf_unequal e1 e2],sfL) ([pf5;pf_unequal e6 e7;pf4;pf1;pf_equal e2 e1;pf_unequal dse_nil e4;pf_unequal e2 e1],pfL')``
877 val (e1, e2) = dest_pf_unequal h;
878 val (e1, turn) = if is_dse_nil e2 then (e1, true) else
879 if is_dse_nil e1 then (e2, false) else
882 val cOpt = find_entry 0 e1 cL;
891 val (e1, e2) = dest_pf_unequal h;
892 val _ = if (e1 = e2) then SMALLFOOT_ERR "preserve for inconsistence" else ();
894 val n1 = valOf (find_entry 0 e1 cL);
970 val t = ``LIST_DS_ENTAILS ([], []) (pfL,[sf1;sf2;sf_points_to e1 [("f", b);("g", c)];sf_points_to e2 [("f", b)];sf_bin_tree ("f", "g") e3; sf_bin_tree ("g", "f") e4;sf_points_to e3 [("f", b);("g", c)];sf5;sf_ls "f" e1 e3]++sfL) (pfL',[sf5;sf_points_to e1 [("g", c);("f", b)];sf_points_to e1 [("f", b);("h", c)];sf_points_to e2 [("f", b)];sf_ls "f" e1 e3;sf_points_to e3 [("f", b);("g", c)];sf4;sf_bin_tree ("f", "g") e3; sf_bin_tree ("f", "g") e4;sf1]++sfL)``
979 | find_pairs_helper P n1 n2 l (e1::l1) (e2::l2) r =
980 if ((P e1 e2) handle _ => false) then
981 find_pairs_helper P n1 (n2+1) l (e1::l1) l2 ((n1, e1, n2, e2)::r)
983 find_pairs_helper P n1 (n2+1) l (e1::l1) l2 r
992 adapt_pair_list_to_deletes___map n1 n2 ((n1', e1, n2', e2)::l) =
997 (if n1' > n1 then (n1'-1) else n1', e1,
1002 adapt_pair_list_to_deletes___helper l1 ((n1, e1, n2, e2)::l) =
1003 adapt_pair_list_to_deletes___helper ((n1, e1, n2, e2)::l1) (adapt_pair_list_to_deletes___map n1 n2 l);
1013 val (e1, _, a1, aL1) = dest_sf_points_to sf1;
1016 (e1 = e2) andalso (aL1 = aL2) andalso
1031 val (e1, a1, _, _) = dest_sf_points_to sf1;
1035 val thm = ISPECL [e1, numLib.term_of_int n1, a1, numLib.term_of_int n2, a2, c1, c2, pf, sf, pf', sf']
1065 val (f, e1, e2) = dest_sf_ls sf1;
1068 val thm = ISPECL [f, e1, e2, numLib.term_of_int n1, numLib.term_of_int n2, c1, c2, pf, sf, pf', sf']
1095 val (f11, f12, e1, _) = dest_sf_bin_tree sf1;
1098 (e1 = e2) andalso
1107 val (f11, f12, e1, _) = dest_sf_bin_tree sf1;
1111 val thm = ISPECL [e1, f11, f12, f21, f22, numLib.term_of_int n1, numLib.term_of_int n2, c1, c2, pf, sf, pf', sf']
1215 val t = ``LIST_DS_ENTAILS ([e6], []) ([pf_unequal e1 dse_nil; pf_unequal dse_nil e3;pf_unequal e3 e2],[sf_points_to e1 [("g", e5)];sf_points_to e3 [];sf_ls f e1 e2;sf_ls f e2 e3;sf_points_to e4 []]) ([],[])``
1242 val (e1, _, _, _) = dest_sf_points_to sf;
1244 e1
1247 val (_, _, _, e1) = dest_sf_tree_ext sf;
1249 e1
1306 val t = ``LIST_DS_ENTAILS ([e2;e1;e4;e6;e5], []) ([pf_unequal e3 e2],[sf_points_to e1 x;sf_points_to e2 x;sf_points_to e3 x;sf_points_to e4 x;sf_ls f e3 e2]) ([],[])``
1339 fun check_unequal_is_necessary cL pfL (e1, e2) =
1340 not (isSome (find_in_list (is_uneq_2 e1 e2) pfL)) andalso
1341 ((e1 = e2) orelse
1342 not (isSome (find_entry 0 e1 cL)) orelse
1348 get_uneq_filter overeager cL pfL r l' ((e1,e2)::l) =
1352 (not (mem (e1,e2) l')) andalso
1353 (not (mem (e2,e1) l')) andalso
1354 check_unequal_is_necessary cL pfL (e1,e2));
1356 (get_uneq_filter overeager cL pfL (necessary::r) (if necessary then (e1,e2)::l' else l') l)
1399 val t = ``LIST_DS_ENTAILS ([e1;e2],[(e2,e3);(e3,e4);(e4,e2);(e9,e10);(e4,e2);(e9,e10)]) ([pf_unequal e3 e4;pf1;pf_unequal e2 e4; pf3],[sf1;sf_ls "f" e1 e2;sf2]) ([],[])``
1403 | find_strengthen_uneq_pairs___helper accu n1 n2 pfLorg ((e1,e2)::cL) [] =
1405 | find_strengthen_uneq_pairs___helper accu n1 n2 pfLorg ((e1,e2)::cL) (pf::pfL) =
1407 val (e1', e2') = dest_pf_unequal pf;
1409 if ((e1 = e1') andalso (e2 = e2')) then (n1,n2,false,e1,e2)::accu else
1410 if ((e2 = e1') andalso (e1 = e2')) then (n1,n2,true,e1,e2)::accu else
1413 find_strengthen_uneq_pairs___helper accu' n1 (n2+1) pfLorg ((e1,e2)::cL) pfL
1423 fun ds_inference_PRECONDITION_STRENGTHEN___SINGLE_CONV (n1,n2,turn,e1,e2) t =
1430 val thm = ISPECL [numLib.term_of_int n2, numLib.term_of_int n1, e1, e2, c1, c2, pf, sf, pf', sf'] inf;
1456 | find_strengthen_eq_pair___helper n1 n2 pfL ((e1,e2)::cL) [] =
1458 | find_strengthen_eq_pair___helper n1 n2 pfL ((e1,e2)::cL) ((e1',e2')::cL') =
1460 val cond = (e1 = e1') andalso (e2 = e2') andalso
1461 not (isSome (find_in_list (is_eq_2 e1 e2) pfL)) handle _ => false;
1463 if cond then SOME (n1, n2, e1, e2) else
1464 find_strengthen_eq_pair___helper n1 (n2+1) pfL ((e1,e2)::cL) cL'
1478 val (n1,n2,e1,e2) = find_strengthen_eq_pair cL pfL handle _ =>
1481 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, c1, c2, pf, sf, pf', sf']
1491 | find_strengthen_eq_precondition___helper n cL1 ((e1,e2)::cL2) =
1493 val n1 = valOf (find_entry 0 e1 cL1);
1495 SOME (n1, n, e1, e2)
1511 val (n1,n2,e1,e2) = find_strengthen_eq_precondition cL1 cL2 handle _ =>
1515 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, c1, c2, pf, sf, pf', sf']
1531 val t = ``LIST_DS_ENTAILS ([e1],[(e2,e3);(e3,e4);(e4,e2);(e9,e10);(e4,e2);(e9,e10)]) ([pf_unequal e3 e4;pf1;pf_unequal e2 e4; pf3],[sf_ls "g" e5 e7; sf_ls "f" dse_nil e3;sf1;sf_ls "f" e1 e2;sf2]) ([],[])``
1553 val (f, e1, e2) = dest_sf_ls lsf;
1570 val (f, e1, e2) = dest_sf_ls h;
1571 val cOpt = find_entry 0 e1 cL;
1573 if (isSome cOpt) then SOME (n, valOf cOpt, f, e1, e2) else
1587 val (n, m, f, e1, e2) = valOf sfOpt;
1589 val thm = ISPECL [numLib.term_of_int m, numLib.term_of_int n, f, e1, e2, c1, c2, pf, sf, pf', sf']
1599 val t = ``LIST_DS_ENTAILS ([e1],[(e2,e3)]) ([pf_unequal e1 e3;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]) ([],[sf432;sf_ls "f" e1 e3;sf4])``
1601 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_ls "f" e1 e3])``
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])``
1605 val t = ``LIST_DS_ENTAILS ([e1],[(e2,e3)]) ([pf_unequal e3 e1;pf1;pf_unequal e2 e4; pf3],[sf_ls "g" e5 e7;sf_points_to e1 [("g", x); ("f", y)]; sf1;sf2]) ([],[sf_bin_tree ("g","fa") e1])``
1613 val (f, e1, e3) = dest_sf_ls h;
1614 val (n3, pointer) = valOf (find_in_list (is_sf_points_to_ex e1) sfL);
1617 val (n2, uneq) = valOf (find_in_list (is_uneq_2 e1 e3) pfL);
1618 val (e1',e2') = dest_pf_unequal uneq;
1619 val turn = (e1 = e2');
1621 SOME (n, n2, n3, turn, e1, e2,e3, f, a)
1630 val e1 = snd (first (fn (x,y) => x = f1) pointer_list);
1633 SOME (n, n2, ex, e1, e2, f1, f2, a)
1647 val (n1, n2, n3, turn, e1, e2,e3, f, a) = valOf searchOpt;
1650 if turn then F else T, e1, e2, e3, f, a, c1, c2, pf, sf, pf', sf']
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']
1692 val t = ``LIST_DS_ENTAILS (c1,c2) ([pf_unequal e1 e2],[sf1;sf3;sf_ls "f" e1 e2;sf2]) ([],[])``
1693 val t = ``LIST_DS_ENTAILS (c1,c2) ([pf2;pf_unequal e2 e1],[sf1;sf3;sf_ls "f" e1 e2;sf2]) ([],[])``
1715 val (f, e1, e2) = dest_sf_ls h;
1716 val (n2, uneq) = valOf (find_in_list (is_uneq_2 e1 e2) pfL);
1717 val (e1',e2') = dest_pf_unequal uneq;
1718 val turn = (e1 = e2');
1720 SOME (n, n2, turn, e1, e2, f)
1733 val (n, n2, turn, e1, e2, f) = valOf searchOpt;
1736 if turn then T else F, e1, e2, f, c1, c2, pf, sf, pf', sf']
1759 val (f, e1, e2) = dest_sf_ls list_term;
1762 e1, e2, f, c1, c2, pf, sf, pf', sf']
1781 val (f1,f2, e1, _) = dest_sf_bin_tree tree_term;
1784 e1, f1, f2, c1, c2, pf, sf, pf', sf']
1797 val t = ``LIST_DS_ENTAILS (c1,c2) ([pf_equal e2 e1],[sf1;sf3;sf2]) ([],[sf_ls f e1 e2;sf_tree fL es e])``
1801 val (_, e2, e1) = dest_sf_tree t;
1803 not (isSome (find_in_list (is_uneq_2 e1 e2) pfL)) andalso
1804 not (isSome (find_in_list (is_eq_2 e1 e2) pfL))
1818 val (_, e1, e2) = dest_sf_tree tree_term;
1820 val thm = ISPECL [e1, e2, c1, c2, pf, sf, pf', sf']
1837 val t = ``LIST_DS_ENTAILS ([],[]) ([pf1;pf2],[sf4;sf_ls f e1 e2; sf5;sf6]) ([],[sf2;sf_ls f e1 dse_nil;sf1])``
1839 val t = ``LIST_DS_ENTAILS ([e3],[]) ([pf1;pf2;pf_unequal e3 e1],[sf4;sf_ls f e1 e2; sf5;sf6]) ([],[sf2;sf_ls f e1 e3;sf1])``
1842 val t = ``LIST_DS_ENTAILS ([],[]) ([pf1;pf2;pf_unequal e3 e1],[sf_points_to e3 [(f,e2)];sf4;sf_ls f e1 e2; sf5;sf6]) ([],[sf2;sf_ls f e1 e3;sf1])``
1845 val t = ``LIST_DS_ENTAILS ([],[]) ([pf1;pf_unequal e2 e3;pf2;pf_unequal e3 e1],[sf_points_to e3 [(f,e2)];sf4;sf_ls f e1 e2; sf5;sf_ls g e3 e2;sf6]) ([],[sf2;sf_ls f e1 e3;sf1])``
1851 fun get_uneq_index_turn pfL e1 e3 = let
1852 val (n, pf) = valOf (find_in_list (is_uneq_2 e1 e3) pfL);
1853 val (e1', e3') = dest_pf_unequal pf;
1854 val turn = not (e1' = e1);
1859 fun find_list_append_instance_nil n1 n2 e1 e2 e3 f =
1862 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f] INFERENCE_APPEND_LIST___nil___EVAL
1867 fun find_list_append_instance_precond n1 n2 e1 e2 e3 f n3 b1 c1L =
1870 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f, e3, numLib.term_of_int n4, numLib.term_of_int n3, if b1 then T else F] INFERENCE_APPEND_LIST___precond___EVAL
1876 fun find_list_append_instance_points_to n1 n2 e1 e2 e3 f n3 b1 sfL =
1881 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2, f, e3, numLib.term_of_int n4, a, numLib.term_of_int n3, if b1 then T else F] INFERENCE_APPEND_LIST___points_to___EVAL
1891 fun find_list_append_instance_tree n1 n2 e1 e2 e3 f n3 b1 pfL sfL =
1905 val thm = ISPECL [numLib.term_of_int n1, numLib.term_of_int n2, e1, e2,
1917 val (f, e1, e3) = dest_sf_ls sf';
1918 val (n1, sf) = valOf (find_in_list (fn sf => (let val (f', e1', e2') = dest_sf_ls sf in (f = f') andalso (e1' = e1) end)) sfL);
1920 val thm = find_list_append_instance_nil n1 n2 e1 e2 e3 f handle _ =>
1922 val (n3,b1) = get_uneq_index_turn pfL e1 e3;
1924 find_list_append_instance_precond n1 n2 e1 e2 e3 f n3 b1 c1L handle _ =>
1925 find_list_append_instance_points_to n1 n2 e1 e2 e3 f n3 b1 sfL handle _ =>
1926 find_list_append_instance_tree n1 n2 e1 e2 e3 f n3 b1 pfL sfL