DEPOBJS = \
$(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
- trie.ml \
path_indexing.ml \
discrimination_tree.ml \
test_indexing.ml \
let indexing_retrieval_time = ref 0.;;
+(* let my_apply_subst subst term = *)
+(* let module C = Cic in *)
+(* let lookup lift_amount meta = *)
+(* match meta with *)
+(* | C.Meta (i, _) -> ( *)
+(* try *)
+(* let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
+(* (\* CicSubstitution.lift lift_amount *\)t *)
+(* with Not_found -> meta *)
+(* ) *)
+(* | _ -> assert false *)
+(* in *)
+(* let rec apply_aux lift_amount = function *)
+(* | C.Meta (i, l) as t -> lookup lift_amount t *)
+(* | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
+(* | C.Prod (nn, s, t) -> *)
+(* C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
+(* | C.Lambda (nn, s, t) -> *)
+(* C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
+(* | t -> t *)
+(* in *)
+(* apply_aux 0 term *)
+(* ;; *)
+
+
+(* let apply_subst subst term = *)
+(* Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
+(* (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
+(* let res = my_apply_subst subst term in *)
+(* (\* let res = CicMetaSubst.apply_subst subst term in *\) *)
+(* Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
+(* print_endline "|"; *)
+(* res *)
+(* ;; *)
+
+(* let apply_subst = my_apply_subst *)
+let apply_subst = CicMetaSubst.apply_subst
+
+
+let apply_subst =
+ let profile = CicUtil.profile "apply_subst" in
+ (fun s a -> profile (apply_subst s) a)
+;;
+
+
+(*
let empty_table () =
Path_indexing.PSTrie.empty
;;
indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
res
;;
+*)
-(*
let empty_table () =
Discrimination_tree.DiscriminationTree.empty
;;
and in_index = Discrimination_tree.in_index;;
let get_candidates mode tree term =
+ let t1 = Unix.gettimeofday () in
let res =
let s =
match mode with
Discrimination_tree.PosEqSet.elements s
in
(* print_candidates mode term res; *)
+ let t2 = Unix.gettimeofday () in
+ indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
res
;;
-*)
+
+
+(* let get_candidates = *)
+(* let profile = CicUtil.profile "Indexing.get_candidates" in *)
+(* (fun mode tree term -> profile (get_candidates mode tree) term) *)
+(* ;; *)
+
let match_unif_time_ok = ref 0.;;
let match_unif_time_no = ref 0.;;
let res = try do_match c other eq_URI with e -> None in
match res with
| Some (_, s, _, _, _) ->
- let c' = M.apply_subst s c
- and other' = M.apply_subst s other in
+ let c' = (* M. *)apply_subst s c
+ and other' = (* M. *)apply_subst s other in
let order = cmp c' other' in
let names = U.names_of_context context in
if order = U.Gt then
;;
-let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
+let rec find_all_matches ?(unif_fun=Inference.unification)
metasenv context ugraph lift_amount term =
let module C = Cic in
let module U = Utils in
let res = do_match c other eq_URI in
match res with
| _, s, _, _, _ ->
- let c' = M.apply_subst s c
- and other' = M.apply_subst s other in
+ let c' = (* M. *)apply_subst s c
+ and other' = (* M. *)apply_subst s other in
let order = cmp c' other' in
let names = U.names_of_context context in
if order <> U.Lt && order <> U.Le then
let subsumption env table target =
- let _, (ty, tl, tr, _), tmetas, _ = target in
+ let _, (ty, left, right, _), tmetas, _ = target in
let metasenv, context, ugraph = env in
let metasenv = metasenv @ tmetas in
let samesubst subst subst' =
true)
subst'
in
- let subsaux left right =
- let leftc = get_candidates Matching table left in
- let leftr =
- find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 left leftc
- in
- let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
- try
- let other = if pos = Utils.Left then r else l in
- let subst', menv', ug' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- Inference.matching metasenv context what other ugraph in
- let t2 = Unix.gettimeofday () in
- match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
- r
- with e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
- in
- samesubst subst subst'
- with e ->
- false
- in
- let r = List.exists (ok right) leftr in
- if r then
- true
- else
- let rightc = get_candidates Matching table right in
- let rightr =
+ let leftr =
+ match left with
+ | Cic.Meta _ -> []
+ | _ ->
+ let leftc = get_candidates Matching table left in
find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 right rightc
+ metasenv context ugraph 0 left leftc
+ in
+ let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
+ try
+ let other = if pos = Utils.Left then r else l in
+ let subst', menv', ug' =
+ let t1 = Unix.gettimeofday () in
+ try
+ let r =
+ Inference.matching metasenv context what other ugraph in
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+ r
+ with e ->
+ let t2 = Unix.gettimeofday () in
+ match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+ raise e
in
- List.exists (ok left) rightr
+ samesubst subst subst'
+ with e ->
+ false
in
- let res = subsaux tl tr in
- if res then (
- Printf.printf "subsumption!:\ntarget: %s\n"
- (Inference.string_of_equality ~env target);
- print_newline ();
- );
- res
+ let r = List.exists (ok right) leftr in
+ if r then
+ true
+ else
+ let rightr =
+ match right with
+ | Cic.Meta _ -> []
+ | _ ->
+ let rightc = get_candidates Matching table right in
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 right rightc
+ in
+ List.exists (ok left) rightr
;;
;;
+let build_newtarget_time = ref 0.;;
+
let rec demodulation newmeta env table target =
let module C = Cic in
let module S = CicSubstitution in
let proof, (eq_ty, left, right, order), metas, args = target in
let metasenv' = metasenv @ metas in
let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let time1 = Unix.gettimeofday () in
+
let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = M.apply_subst subst (S.subst other t) in
+ let bo = (* M. *)apply_subst subst (S.subst other t) in
let bo'' =
C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
S.lift 1 eq_ty] @
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo,
- M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; proof'])
+ C.Implicit None
+(* (\* M. *\)apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(* proof; other; proof']) *)
in
let left, right = if is_left then newterm, right else left, newterm in
let m =
args
in
let ordering = !Utils.compare_terms left right in
+
+ let time2 = Unix.gettimeofday () in
+ build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+
newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
in
+(* let build_newtarget = *)
+(* let profile = CicUtil.profile "Indexing.demodulation.build_newtarget" in *)
+(* (fun a b -> profile (build_newtarget a) b) *)
+(* in *)
let res = demodulate_term metasenv' context ugraph table 0 left in
let build_identity (p, (t, l, r, o), m, a) =
match o with
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- if subsumption env table newtarget then
- newmeta, build_identity newtarget
- else
+(* if subsumption env table newtarget then *)
+(* newmeta, build_identity newtarget *)
+(* else *)
demodulation newmeta env table newtarget
| None ->
let res = demodulate_term metasenv' context ugraph table 0 right in
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- if subsumption env table newtarget then
- newmeta, build_identity newtarget
- else
+(* if subsumption env table newtarget then *)
+(* newmeta, build_identity newtarget *)
+(* else *)
demodulation newmeta env table newtarget
| None ->
newmeta, target
betaexpand_term metasenv context ugraph table 0 term
in
let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
+ let time1 = Unix.gettimeofday () in
+
let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = M.apply_subst s (S.subst other bo) in
+ let bo' = (* M. *)apply_subst s (S.subst other bo) in
let bo'' =
C.Appl (
[C.MutInd (HL.Logic.eq_URI, 0, []);
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; proof'])
+ C.Implicit None
+(* (\* M. *\)apply_subst s *)
+(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(* proof; other; proof']) *)
in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
let neworder = !Utils.compare_terms left right in
+
+ let time2 = Unix.gettimeofday () in
+ build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+
(newproof, (eq_ty, left, right, neworder), [], [])
in
+(* let build_new = *)
+(* let profile = CicUtil.profile "Inference.superposition_left.build_new" in *)
+(* (fun e -> profile build_new e) *)
+(* in *)
List.map build_new expansions
;;
let res l r =
List.filter
(fun (_, subst, _, _, _) ->
- let subst = M.apply_subst subst in
+ let subst = (* M. *)apply_subst subst in
let o = !Utils.compare_terms (subst l) (subst r) in
o <> U.Lt && o <> U.Le)
(fst (betaexpand_term metasenv' context ugraph table 0 l))
(res left right), (res right left)
in
let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
+
+ let time1 = Unix.gettimeofday () in
+
let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = M.apply_subst s (S.subst other bo) in
+ let bo' = (* M. *)apply_subst s (S.subst other bo) in
let bo'' =
C.Appl (
[C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
in
let t' = C.Lambda (C.Anonymous, ty, bo'') in
bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- eqproof; other; proof'])
+ C.Implicit None
+(* (\* M. *\)apply_subst s *)
+(* (C.Appl [C.Const (eq_URI, []); ty; what; t'; *)
+(* eqproof; other; proof']) *)
in
let newmeta, newequality =
let left, right =
- if ordering = U.Gt then newgoal, M.apply_subst s right
- else M.apply_subst s left, newgoal in
+ if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
+ else (* M. *)apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right
and newmenv = newmetas @ menv'
and newargs = args @ args' in
newm, eq'
in
maxmeta := newmeta;
+
+ let time2 = Unix.gettimeofday () in
+ build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
+
newequality
in
+
+(* let build_new = *)
+(* let profile = CicUtil.profile "Indexing.superposition_right.build_new" in *)
+(* (fun o e -> profile (build_new o) e) *)
+(* in *)
+
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
let ok = function
;;
-exception MatchingFailure;;
+let rec check_irl start = function
+ | [] -> true
+ | None::tl -> check_irl (start+1) tl
+ | (Some (Cic.Rel x))::tl ->
+ if x = start then check_irl (start+1) tl else false
+ | _ -> false
+;;
-let matching metasenv context t1 t2 ugraph =
- try
- let subst, metasenv, ugraph =
- CicUnification.fo_unif metasenv context t1 t2 ugraph
+let rec is_simple_term = function
+ | Cic.Appl ((Cic.Meta _)::_) -> false
+ | Cic.Appl l -> List.for_all is_simple_term l
+ | Cic.Meta (i, l) -> check_irl 1 l
+ | Cic.Rel _ -> true
+ | _ -> false
+;;
+
+
+let lookup_subst meta subst =
+ match meta with
+ | Cic.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+;;
+
+
+let unification_simple metasenv context t1 t2 ugraph =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup = lookup_subst in
+ let rec occurs_check subst what where =
+ (* Printf.printf "occurs_check %s %s" *)
+ (* (CicPp.ppterm what) (CicPp.ppterm where); *)
+ (* print_newline (); *)
+ match where with
+ | t when what = t -> true
+ | C.Appl l -> List.exists (occurs_check subst what) l
+ | C.Meta _ ->
+ let t = lookup where subst in
+ if t <> where then occurs_check subst what t else false
+ | _ -> false
+ in
+ let rec unif subst menv s t =
+(* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
+(* (print_subst subst); *)
+(* print_newline (); *)
+ let s = match s with C.Meta _ -> lookup s subst | _ -> s
+ and t = match t with C.Meta _ -> lookup t subst | _ -> t
in
- let t' = CicMetaSubst.apply_subst subst t1 in
- if not (meta_convertibility t1 t') then
- raise MatchingFailure
+ (* Printf.printf "after apply_subst: %s %s\n%s" *)
+ (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
+ (* print_newline (); *)
+ match s, t with
+ | s, t when s = t -> subst, menv
+ | C.Meta (i, _), C.Meta (j, _) when i > j ->
+ unif subst menv t s
+ | C.Meta _, t when occurs_check subst s t ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+(* | C.Meta (i, l), C.Meta (j, l') -> *)
+(* let _, _, ty = CicUtil.lookup_meta i menv in *)
+(* let _, _, ty' = CicUtil.lookup_meta j menv in *)
+(* let binding1 = lookup s subst in *)
+(* let binding2 = lookup t subst in *)
+(* let subst, menv = *)
+(* if binding1 != s then *)
+(* if binding2 != t then *)
+(* unif subst menv binding1 binding2 *)
+(* else *)
+(* if binding1 = t then *)
+(* subst, menv *)
+(* else *)
+(* ((j, (context, binding1, ty'))::subst, *)
+(* List.filter (fun (m, _, _) -> j <> m) menv) *)
+(* else *)
+(* if binding2 != t then *)
+(* if s = binding2 then *)
+(* subst, menv *)
+(* else *)
+(* ((i, (context, binding2, ty))::subst, *)
+(* List.filter (fun (m, _, _) -> i <> m) menv) *)
+(* else *)
+(* ((i, (context, t, ty))::subst, *)
+(* List.filter (fun (m, _, _) -> i <> m) menv) *)
+(* in *)
+(* subst, menv *)
+
+ | C.Meta (i, l), t ->
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ let subst =
+ if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+ else subst
+ in
+ let menv = List.filter (fun (m, _, _) -> i <> m) menv in
+ subst, menv
+ | _, C.Meta _ -> unif subst menv t s
+ | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+ | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
+ try
+ List.fold_left2
+ (fun (subst', menv) s t -> unif subst' menv s t)
+ (subst, menv) tls tlt
+ with e ->
+ raise (U.UnificationFailure "Inference.unification.unif")
+ )
+ | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+ in
+ let subst, menv = unif [] metasenv t1 t2 in
+ (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+ (* print_newline (); *)
+(* let rec fix_term = function *)
+(* | (C.Meta (i, l) as t) -> *)
+(* lookup t subst *)
+(* | C.Appl l -> C.Appl (List.map fix_term l) *)
+(* | t -> t *)
+(* in *)
+(* let rec fix_subst = function *)
+(* | [] -> [] *)
+(* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
+(* in *)
+(* List.rev (fix_subst subst), menv, ugraph *)
+ List.rev subst, menv, ugraph
+;;
+
+
+let unification metasenv context t1 t2 ugraph =
+(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+ let subst, menv, ug =
+ if not (is_simple_term t1) || not (is_simple_term t2) then
+ CicUnification.fo_unif metasenv context t1 t2 ugraph
else
- let metas = metas_of_term t1 in
- let fix_subst = function
- | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
- (j, (c, Cic.Meta (i, lc), ty))
- | s -> s
+ unification_simple metasenv context t1 t2 ugraph
+ in
+ let rec fix_term = function
+ | (Cic.Meta (i, l) as t) ->
+ let t' = lookup_subst t subst in
+ if t <> t' then fix_term t' else t
+ | Cic.Appl l -> Cic.Appl (List.map fix_term l)
+ | t -> t
+ in
+ let rec fix_subst = function
+ | [] -> []
+ | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
+ in
+(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
+(* print_endline "|"; *)
+ (* fix_subst *) subst, menv, ug
+;;
+
+(* let unification = CicUnification.fo_unif;; *)
+
+exception MatchingFailure;;
+
+
+let matching_simple metasenv context t1 t2 ugraph =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let module U = CicUnification in
+ let lookup meta subst =
+ match meta with
+ | C.Meta (i, _) -> (
+ try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+ with Not_found -> meta
+ )
+ | _ -> assert false
+ in
+ let rec do_match subst menv s t =
+(* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
+(* (print_subst subst); *)
+(* print_newline (); *)
+(* let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
+(* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *)
+ (* Printf.printf "after apply_subst: %s %s\n%s" *)
+ (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
+ (* print_newline (); *)
+ match s, t with
+ | s, t when s = t -> subst, menv
+(* | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
+(* do_match subst menv t s *)
+(* | C.Meta _, t when occurs_check subst s t -> *)
+(* raise MatchingFailure *)
+(* | s, C.Meta _ when occurs_check subst t s -> *)
+(* raise MatchingFailure *)
+ | s, C.Meta (i, l) ->
+ let filter_menv i menv =
+ List.filter (fun (m, _, _) -> i <> m) menv
+ in
+ let subst, menv =
+ let value = lookup t subst in
+ match value with
+(* | C.Meta (i', l') when Hashtbl.mem table i' -> *)
+(* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
+ | value when value = t ->
+ let _, _, ty = CicUtil.lookup_meta i menv in
+ (i, (context, s, ty))::subst, filter_menv i menv
+ | value when value <> s ->
+ raise MatchingFailure
+ | value -> do_match subst menv s value
+ in
+ subst, menv
+(* else if value <> s then *)
+(* raise MatchingFailure *)
+(* else subst *)
+(* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
+(* else subst *)
+(* in *)
+(* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
+(* subst, menv *)
+(* | _, C.Meta _ -> do_match subst menv t s *)
+(* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
+(* raise MatchingFailure *)
+ | C.Appl ls, C.Appl lt -> (
+ try
+ List.fold_left2
+ (fun (subst, menv) s t -> do_match subst menv s t)
+ (subst, menv) ls lt
+ with e ->
+(* print_endline (Printexc.to_string e); *)
+(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(* print_newline (); *)
+ raise MatchingFailure
+ )
+ | _, _ ->
+(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
+(* print_newline (); *)
+ raise MatchingFailure
+ in
+ let subst, menv = do_match [] metasenv t1 t2 in
+ (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
+ (* print_newline (); *)
+ subst, menv, ugraph
+;;
+
+
+let matching metasenv context t1 t2 ugraph =
+(* if (is_simple_term t1) && (is_simple_term t2) then *)
+(* let subst, menv, ug = *)
+(* matching_simple metasenv context t1 t2 ugraph in *)
+(* (\* Printf.printf "matching %s %s:\n%s\n" *\) *)
+(* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
+(* (\* print_newline (); *\) *)
+(* subst, menv, ug *)
+(* else *)
+ try
+ let subst, metasenv, ugraph =
+ (* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
+ unification metasenv context t1 t2 ugraph
in
- let subst = List.map fix_subst subst in
- subst, metasenv, ugraph
- with e ->
- raise MatchingFailure
+ let t' = CicMetaSubst.apply_subst subst t1 in
+ if not (meta_convertibility t1 t') then
+ raise MatchingFailure
+ else
+ let metas = metas_of_term t1 in
+ let fix_subst = function
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ (j, (c, Cic.Meta (i, lc), ty))
+ | s -> s
+ in
+ let subst = List.map fix_subst subst in
+
+(* Printf.printf "matching %s %s:\n%s\n" *)
+(* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
+(* print_newline (); *)
+
+ subst, metasenv, ugraph
+ with e ->
+(* Printf.printf "failed to match %s %s\n" *)
+(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+ raise MatchingFailure
;;
+(* let matching = *)
+(* let profile = CicUtil.profile "Inference.matching" in *)
+(* (fun metasenv context t1 t2 ugraph -> *)
+(* profile (matching metasenv context t1 t2) ugraph) *)
+(* ;; *)
+
let beta_expand ?(metas_ok=true) ?(match_only=false)
what type_of_what where context metasenv ugraph =
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+val unification:
+ Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ CicUniv.universe_graph ->
+ Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+
(**
Performs the beta expansion of the term "where" w.r.t. "what",
i.e. returns the list of all the terms t s.t. "(t what) = where".
(* profiling statistics... *)
let infer_time = ref 0.;;
let forward_simpl_time = ref 0.;;
+let forward_simpl_new_time = ref 0.;;
let backward_simpl_time = ref 0.;;
+let passive_maintainance_time = ref 0.;;
(* limited-resource-strategy related globals *)
let processed_clauses = ref 0;; (* number of equalities selected so far... *)
let time_limit = ref 0.;; (* in seconds, settable by the user... *)
let start_time = ref 0.;; (* time at which the execution started *)
let elapsed_time = ref 0.;;
-let maximal_weight = ref None;;
-(* let maximal_retained_equality = ref None;; *)
+(* let maximal_weight = ref None;; *)
+let maximal_retained_equality = ref None;;
(* equality-selection related globals *)
let use_fullred = ref false;;
let weight_of_equality (_, (ty, left, right, _), _, _) =
- let weight_of t = fst (weight_of_term ~consider_metas:false t) in
- (weight_of ty) + (weight_of left) + (weight_of right)
+ let meta_number = ref 0 in
+ let weight_of t =
+ let weight, ml = weight_of_term t in
+ meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml);
+ weight
+ in
+ (weight_of ty) + (weight_of left) + (weight_of right), meta_number
;;
| false ->
let _, (ty, left, right, _), _, _ = eq1
and _, (ty', left', right', _), _, _ = eq2 in
+(* let w1, m1 = weight_of_equality eq1 *)
+(* and w2, m2 = weight_of_equality eq2 in *)
let weight_of t = fst (weight_of_term ~consider_metas:false t) in
let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
-(* let w1 = weight_of_equality eq1 *)
-(* and w2 = weight_of_equality eq2 in *)
match Pervasives.compare w1 w2 with
| 0 -> Pervasives.compare eq1 eq2
+(* let res = Pervasives.compare m1 m2 in *)
+(* if res = 0 then Pervasives.compare eq1 eq2 else res *)
| res -> res
end
in
let c = others + (abs (common - card)) in
if c < i then (c, equality)
+(* else if c = i then *)
+(* match OrderedEquality.compare equality e with *)
+(* | -1 -> (c, equality) *)
+(* | res -> (i, e) *)
else (i, e)
in
let e1 = EqualitySet.min_elt pos_set in
let in_age, ns, nl = picka in_age ns nl in
let _, ps, pl = picka in_age ps pl in
if not (EqualitySet.is_empty ps) then
- maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps));
-(* maximal_retained_equality := Some (EqualitySet.max_elt ps); *)
+(* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
+ maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
(fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
in
derived_clauses := !derived_clauses + (List.length new_neg) +
(List.length new_pos);
- match !maximal_weight(* !maximal_retained_equality *) with
+ match (* !maximal_weight *)!maximal_retained_equality with
| None -> new_neg, new_pos
- | Some w (* eq *) ->
+ | Some (* w *) eq ->
let new_pos =
- List.filter (fun e -> (weight_of_equality e) <= w (* OrderedEquality.compare e eq <= 0 *)) new_pos in
+ List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
new_neg, new_pos
;;
(* else find_duplicate sign current tl *)
(* | _::tl -> find_duplicate sign current tl *)
(* in *)
+
+(* let res = *)
+(* if sign = Positive then *)
+(* Indexing.subsumption env active_table current *)
+(* else *)
+(* false *)
+(* in *)
+(* if res then *)
+(* None *)
+(* else *)
+
let demodulate table current =
let newmeta, newcurrent =
Indexing.demodulation !maxmeta env table current in
in
let new_pos = EqualitySet.elements new_pos_set in
-(* let subs = *)
-(* match passive_table with *)
-(* | None -> *)
-(* (fun e -> not (Indexing.subsumption env active_table e)) *)
-(* | Some passive_table -> *)
-(* (fun e -> not ((Indexing.subsumption env active_table e) || *)
-(* (Indexing.subsumption env passive_table e))) *)
-(* in *)
+ let subs =
+ match passive_table with
+ | None ->
+ (fun e -> not (Indexing.subsumption env active_table e))
+ | Some passive_table ->
+ (fun e -> not ((Indexing.subsumption env active_table e) ||
+ (Indexing.subsumption env passive_table e)))
+ in
let t1 = Unix.gettimeofday () in
;;
-let backward_simplify_active env (new_neg, new_pos) active =
+let backward_simplify_active env new_pos new_table active =
let active_list, active_table = active in
- let new_pos, new_table =
- List.fold_left
- (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
- ([], Indexing.empty_table ()) new_pos
- in
let active_list, newa =
List.fold_right
(fun (s, equality) (res, newn) ->
;;
-let backward_simplify_passive env (new_neg, new_pos) passive =
- let new_pos, new_table =
- List.fold_left
- (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
- ([], Indexing.empty_table ()) new_pos
- in
+let backward_simplify_passive env new_pos new_table passive =
let (nl, ns), (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
match forward_simplify env (sign, equality) (new_pos, new_table) with
let backward_simplify env new' ?passive active =
- let active, newa = backward_simplify_active env new' active in
+ let new_pos, new_table =
+ List.fold_left
+ (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
+ ([], Indexing.empty_table ()) (snd new')
+ in
+ let active, newa = backward_simplify_active env new_pos new_table active in
match passive with
| None ->
active, (make_passive [] []), newa, None
| Some passive ->
let passive, newp =
- backward_simplify_passive env new' passive in
+ backward_simplify_passive env new_pos new_table passive in
active, passive, newa, newp
;;
(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
int_of_float (
ceil ((float_of_int !processed_clauses) *.
- ((!time_limit *. 2.) /. !elapsed_time -. 1.)))
+ ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
;;
let rec given_clause env passive active =
+ let time1 = Unix.gettimeofday () in
+
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
passive
in
+ let time2 = Unix.gettimeofday () in
+ passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+
kept_clauses := (size_of_passive passive) + (size_of_active active);
match passive_is_empty passive with
| true -> Failure
| false ->
let (sign, current), passive = select env passive active in
- match forward_simplify env (sign, current) ~passive active with
+ let time1 = Unix.gettimeofday () in
+ let res = forward_simplify env (sign, current) ~passive active in
+ let time2 = Unix.gettimeofday () in
+ forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+ match res with
| None ->
given_clause env passive active
| Some (sign, current) ->
let new' = forward_simplify_new env new' (* ~passive *) active in
let t2 = Unix.gettimeofday () in
let _ =
- forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
+ forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
in
let active =
match sign with
let rec given_clause_fullred env passive active =
+ let time1 = Unix.gettimeofday () in
+
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
) else
passive
in
+
+ let time2 = Unix.gettimeofday () in
+ passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
+ kept_clauses := (size_of_passive passive) + (size_of_active active);
+
match passive_is_empty passive with
| true -> Failure
| false ->
let (sign, current), passive = select env passive active in
- match forward_simplify env (sign, current) ~passive active with
+ let time1 = Unix.gettimeofday () in
+ let res = forward_simplify env (sign, current) ~passive active in
+ let time2 = Unix.gettimeofday () in
+ forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
+ match res with
| None ->
given_clause_fullred env passive active
| Some (sign, current) ->
let t1 = Unix.gettimeofday () in
let new' = forward_simplify_new env new' ~passive active in
let t2 = Unix.gettimeofday () in
- forward_simpl_time := !forward_simpl_time +. (t2 -. t1);
+ forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
let t1 = Unix.gettimeofday () in
let active, passive, newa, retained =
backward_simplify env new' ~passive active in
if k < (kept - 1) then
processed_clauses := !processed_clauses + (kept - 1 - k);
- let _ =
- Printf.printf "active:\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
- (string_of_equality ~env e)) (fst active))));
- print_newline ();
- in
- let _ =
- match new' with
- | neg, pos ->
- Printf.printf "new':\n%s\n"
- (String.concat "\n"
- ((List.map
- (fun e -> "Negative " ^
- (string_of_equality ~env e)) neg) @
- (List.map
- (fun e -> "Positive " ^
- (string_of_equality ~env e)) pos)));
- print_newline ();
- in
+(* let _ = *)
+(* Printf.printf "active:\n%s\n" *)
+(* (String.concat "\n" *)
+(* ((List.map *)
+(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
+(* (string_of_equality ~env e)) (fst active)))); *)
+(* print_newline (); *)
+(* in *)
+(* let _ = *)
+(* match new' with *)
+(* | neg, pos -> *)
+(* Printf.printf "new':\n%s\n" *)
+(* (String.concat "\n" *)
+(* ((List.map *)
+(* (fun e -> "Negative " ^ *)
+(* (string_of_equality ~env e)) neg) @ *)
+(* (List.map *)
+(* (fun e -> "Positive " ^ *)
+(* (string_of_equality ~env e)) pos))); *)
+(* print_newline (); *)
+(* in *)
match contains_empty env new' with
| false, _ ->
let passive = add_to_passive passive new' in
Printf.printf "Success, but no proof?!?\n\n"
in
Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ "forward_simpl_new_time: %.9f\n" ^^
"backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !backward_simpl_time;
- Printf.printf "successful unification/matching time: %.9f\n"
+ !infer_time !forward_simpl_time !forward_simpl_new_time
+ !backward_simpl_time;
+ Printf.printf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time;
+ Printf.printf " successful unification/matching time: %.9f\n"
!Indexing.match_unif_time_ok;
- Printf.printf "failed unification/matching time: %.9f\n"
+ Printf.printf " failed unification/matching time: %.9f\n"
!Indexing.match_unif_time_no;
- Printf.printf "indexing retrieval time: %.9f\n"
+ Printf.printf " indexing retrieval time: %.9f\n"
!Indexing.indexing_retrieval_time;
+ Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time;
Printf.printf "derived %d clauses, kept %d clauses.\n"
!derived_clauses !kept_clauses;
with exc ->
;;
+let test_subst () =
+ let module C = Cic in
+ let module M = CicMetaSubst in
+ let term = C.Appl [
+ C.Rel 1;
+ C.Appl [C.Rel 11;
+ C.Meta (43, []);
+ C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
+ C.Appl [C.Rel 11;
+ C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
+ C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
+ ] in
+ let subst1 = [
+ (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
+ (10, ([], C.Rel 12, C.Rel 16));
+ (12, ([], C.Meta (41, []), C.Rel 16))
+ ]
+ and subst2 = [
+ (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
+ (10, ([], C.Rel 12, C.Rel 16));
+ (12, ([], C.Meta (41, []), C.Rel 16))
+ ] in
+ let t1 = M.apply_subst subst1 term
+ and t2 = M.apply_subst subst2 term in
+ Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
+;;
+
+
(* differing ();; *)
(* next_after ();; *)
-discrimination_tree_test ();;
+(* discrimination_tree_test ();; *)
(* path_indexing_test ();; *)
+test_subst ();;
;;
-let print_subst subst =
- String.concat "\n"
+let print_subst ?(prefix="\n") subst =
+ String.concat prefix
(List.map
(fun (i, (c, t, ty)) ->
Printf.sprintf "?%d -> %s : %s" i
val print_metasenv: Cic.metasenv -> string
-val print_subst: Cic.substitution -> string
+val print_subst: ?prefix:string -> Cic.substitution -> string
val string_of_weight: weight -> string
projects / helm.git / commitdiff