X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=91fcee8a22833b645784a6e62ef03996e41d8f56;hb=ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef;hp=e2f21b25cfe823d004c5579238d5f3562586f3dd;hpb=801f0eb3eabe1cbcd66d6a3f52c24eb8f1189611;p=helm.git diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index e2f21b25c..91fcee8a2 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -23,70 +23,16 @@ * http://cs.unibo.it/helm/. *) +let _profiler = <:profiler<_profiler>>;; + (* $Id$ *) open Utils;; - -let metas_of_proof_time = ref 0.;; -let metas_of_term_time = ref 0.;; - -type equality = - int * (* weight *) - proof * - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term * (* right side *) - Utils.comparison) * (* ordering *) - Cic.metasenv (* environment for metas *) - -and proof = - | NoProof (* term is the goal missing a proof *) - | BasicProof of Cic.term - | ProofBlock of - Cic.substitution * UriManager.uri * - (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof - | ProofGoalBlock of proof * proof - | ProofSymBlock of Cic.term list * proof - | SubProof of Cic.term * int * proof -;; - -let string_of_equality ?env = - match env with - | None -> ( - function - | w, _, (ty, left, right, o), _ -> - Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty) - (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) - ) - | Some (_, context, _) -> ( - let names = names_of_context context in - function - | w, _, (ty, left, right, o), _ -> - Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names) - (CicPp.pp left names) (string_of_comparison o) - (CicPp.pp right names) - ) -;; - - -let rec string_of_proof = function - | NoProof -> "NoProof " - | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t) - | SubProof (t, i, p) -> - Printf.sprintf "SubProof(%s, %s, %s)" - (CicPp.ppterm t) (string_of_int i) (string_of_proof p) - | ProofSymBlock _ -> "ProofSymBlock" - | ProofBlock (subst, _, _, _ ,_,_) -> - "ProofBlock" ^ (CicMetaSubst.ppsubst subst) - | ProofGoalBlock (p1, p2) -> - Printf.sprintf "ProofGoalBlock(%s, %s)" - (string_of_proof p1) (string_of_proof p2) -;; - +open Printf;; let check_disjoint_invariant subst metasenv msg = if (List.exists - (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv) + (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -94,257 +40,6 @@ let check_disjoint_invariant subst metasenv msg = end ;; -(* filter out from metasenv the variables in substs *) -let filter subst metasenv = - List.filter - (fun (m, _, _) -> - try let _ = List.find (fun (i, _) -> m = i) subst in false - with Not_found -> true) - metasenv -;; - -(* returns an explicit named subst and a list of arguments for sym_eq_URI *) -let build_ens_for_sym_eq sym_eq_URI termlist = - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in - match obj with - | Cic.Constant (_, _, _, uris, _) -> - assert (List.length uris <= List.length termlist); - let rec aux = function - | [], tl -> [], tl - | (uri::uris), (term::tl) -> - let ens, args = aux (uris, tl) in - (uri, term)::ens, args - | _, _ -> assert false - in - aux (uris, termlist) - | _ -> assert false -;; - - -let build_proof_term ?(noproof=Cic.Implicit None) proof = - let rec do_build_proof proof = - match proof with - | NoProof -> - Printf.fprintf stderr "WARNING: no proof!\n"; - noproof - | BasicProof term -> term - | ProofGoalBlock (proofbit, proof) -> - print_endline "found ProofGoalBlock, going up..."; - do_build_goal_proof proofbit proof - | ProofSymBlock (termlist, proof) -> - let proof = do_build_proof proof in - let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in - Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof]) - | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) -> - let t' = Cic.Lambda (name, ty, bo) in - let proof' = - let _, proof', _, _ = eq in - do_build_proof proof' - in - let eqproof = do_build_proof eqproof in - let _, _, (ty, what, other, _), menv' = eq in - let what, other = - if pos = Utils.Left then what, other else other, what - in - CicMetaSubst.apply_subst subst - (Cic.Appl [Cic.Const (eq_URI, []); ty; - what; t'; eqproof; other; proof']) - | SubProof (term, meta_index, proof) -> - let proof = do_build_proof proof in - let eq i = function - | Cic.Meta (j, _) -> i = j - | _ -> false - in - ProofEngineReduction.replace - ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term - - and do_build_goal_proof proofbit proof = - match proof with - | ProofGoalBlock (pb, p) -> - do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p)) - | _ -> do_build_proof (replace_proof proofbit proof) - - and replace_proof newproof = function - | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) -> - let eqproof' = replace_proof newproof eqproof in - ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof') - | ProofGoalBlock (pb, p) -> - let pb' = replace_proof newproof pb in - ProofGoalBlock (pb', p) - | BasicProof _ -> newproof - | SubProof (term, meta_index, p) -> - SubProof (term, meta_index, replace_proof newproof p) - | p -> p - in - do_build_proof proof -;; - - -let rec metas_of_term = function - | Cic.Meta (i, c) -> [i] - | Cic.Var (_, ens) - | Cic.Const (_, ens) - | Cic.MutInd (_, _, ens) - | Cic.MutConstruct (_, _, _, ens) -> - List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) - | Cic.Cast (s, t) - | Cic.Prod (_, s, t) - | Cic.Lambda (_, s, t) - | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) - | Cic.Appl l -> List.flatten (List.map metas_of_term l) - | Cic.MutCase (uri, i, s, t, l) -> - (metas_of_term s) @ (metas_of_term t) @ - (List.flatten (List.map metas_of_term l)) - | Cic.Fix (i, il) -> - List.flatten - (List.map (fun (s, i, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | Cic.CoFix (i, il) -> - List.flatten - (List.map (fun (s, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | _ -> [] -;; - -let rec metas_of_proof p = - if Utils.debug then - let t1 = Unix.gettimeofday () in - let res = metas_of_term (build_proof_term p) in - let t2 = Unix.gettimeofday () in - metas_of_proof_time := !metas_of_proof_time +. (t2 -. t1); - res - else - metas_of_term (build_proof_term p) -;; - -exception NotMetaConvertible;; - -let meta_convertibility_aux table t1 t2 = - let module C = Cic in - let rec aux ((table_l, table_r) as table) t1 t2 = - match t1, t2 with - | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - let m1_binding, table_l = - try List.assoc m1 table_l, table_l - with Not_found -> m2, (m1, m2)::table_l - and m2_binding, table_r = - try List.assoc m2 table_r, table_r - with Not_found -> m1, (m2, m1)::table_r - in - if (m1_binding <> m2) || (m2_binding <> m1) then - raise NotMetaConvertible - else ( - try - List.fold_left2 - (fun res t1 t2 -> - match t1, t2 with - | None, Some _ | Some _, None -> raise NotMetaConvertible - | None, None -> res - | Some t1, Some t2 -> (aux res t1 t2)) - (table_l, table_r) tl1 tl2 - with Invalid_argument _ -> - raise NotMetaConvertible - ) - | C.Var (u1, ens1), C.Var (u2, ens2) - | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) -> - aux_ens table ens1 ens2 - | C.Cast (s1, t1), C.Cast (s2, t2) - | C.Prod (_, s1, t1), C.Prod (_, s2, t2) - | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) - | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> - let table = aux table s1 s2 in - aux table t1 t2 - | C.Appl l1, C.Appl l2 -> ( - try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2) - when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2 - | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2) - when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 -> - aux_ens table ens1 ens2 - | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2) - when (UriManager.eq u1 u2) && i1 = i2 -> - let table = aux table s1 s2 in - let table = aux table t1 t2 in ( - try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> ( - try - List.fold_left2 - (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) -> - if i1 <> i2 then raise NotMetaConvertible - else - let res = (aux res s1 s2) in aux res t1 t2) - table il1 il2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> ( - try - List.fold_left2 - (fun res (n1, s1, t1) (n2, s2, t2) -> - let res = aux res s1 s2 in aux res t1 t2) - table il1 il2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | t1, t2 when t1 = t2 -> table - | _, _ -> raise NotMetaConvertible - - and aux_ens table ens1 ens2 = - let cmp (u1, t1) (u2, t2) = - compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) - in - let ens1 = List.sort cmp ens1 - and ens2 = List.sort cmp ens2 in - try - List.fold_left2 - (fun res (u1, t1) (u2, t2) -> - if not (UriManager.eq u1 u2) then raise NotMetaConvertible - else aux res t1 t2) - table ens1 ens2 - with Invalid_argument _ -> raise NotMetaConvertible - in - aux table t1 t2 -;; - - -let meta_convertibility_eq eq1 eq2 = - let _, _, (ty, left, right, _), _ = eq1 - and _, _, (ty', left', right', _), _ = eq2 in - if ty <> ty' then - false - else if (left = left') && (right = right') then - true - else if (left = right') && (right = left') then - true - else - try - let table = meta_convertibility_aux ([], []) left left' in - let _ = meta_convertibility_aux table right right' in - true - with NotMetaConvertible -> - try - let table = meta_convertibility_aux ([], []) left right' in - let _ = meta_convertibility_aux table right left' in - true - with NotMetaConvertible -> - false -;; - - -let meta_convertibility t1 t2 = - if t1 = t2 then - true - else - try - ignore(meta_convertibility_aux ([], []) t1 t2); - true - with NotMetaConvertible -> - false -;; - - let rec check_irl start = function | [] -> true | None::tl -> check_irl (start+1) tl @@ -353,7 +48,6 @@ let rec check_irl start = function | _ -> false ;; - let rec is_simple_term = function | Cic.Appl ((Cic.Meta _)::_) -> false | Cic.Appl l -> List.for_all is_simple_term l @@ -365,17 +59,6 @@ let rec is_simple_term = function | _ -> false ;; - -let rec lookup_subst meta subst = - match meta with - | Cic.Meta (i, _) -> ( - try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst - in lookup_subst t subst - with Not_found -> meta - ) - | _ -> meta -;; - let locked menv i = List.exists (fun (j,_,_) -> i = j) menv ;; @@ -384,7 +67,7 @@ let unification_simple locked_menv 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 lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with | t when what = t -> true @@ -402,33 +85,33 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = match s, t with | s, t when s = t -> subst, menv | C.Meta (i, _), C.Meta (j, _) - when (locked locked_menv i) &&(locked locked_menv j) -> - raise + when (locked locked_menv i) &&(locked locked_menv j) -> + raise (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> - unif subst menv t s + | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> + unif subst menv t s | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t when (locked locked_menv i) -> - raise + raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in - assert (not (List.mem_assoc i subst)); - let subst = (i, (context, t, ty))::subst in + assert (not (Subst.is_in_subst i subst)); + let subst = Subst.buildsubst i context t ty subst in let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) subst, menv with CicUtil.Meta_not_found m -> let names = names_of_context context in - debug_print - (lazy + (*debug_print + (lazy*) prerr_endline (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m (CicPp.pp t1 names) (CicPp.pp t2 names) - (print_metasenv menv) (print_metasenv metasenv))); + (print_metasenv menv) (print_metasenv metasenv)); assert false ) | _, C.Meta _ -> unif subst menv t s @@ -445,9 +128,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = | _, _ -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) in - let subst, menv = unif [] metasenv t1 t2 in - let menv = filter subst menv in - List.rev subst, menv, ugraph + let subst, menv = unif Subst.empty_subst metasenv t1 t2 in + let menv = Subst.filter subst menv in + subst, menv, ugraph ;; let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]" @@ -456,293 +139,60 @@ let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]" let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = - let metasenv = metasenv1 @ metasenv2 in + let metasenv = + HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) + (* metasenv1 @ metasenv2 *) + in let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( debug_print (lazy (Printf.sprintf "NOT SIMPLE TERMS: %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); - raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif")) + raise (CicUnification.UnificationFailure (lazy "Inference.unification.unif")) ) else if b then - (* full unification *) - unification_simple [] metasenv context t1 t2 ugraph + (* full unification *) + unification_simple [] metasenv context t1 t2 ugraph else - (* matching: metasenv1 is locked *) - unification_simple metasenv1 metasenv context t1 t2 ugraph + (* matching: metasenv1 is locked *) + unification_simple metasenv1 metasenv context t1 t2 ugraph in if Utils.debug_res then - ignore(check_disjoint_invariant subst menv "unif"); - let flatten subst = + ignore(check_disjoint_invariant subst menv "unif"); + (* let flatten subst = List.map (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst + let context = apply_subst_context subst context in + let term = apply_subst subst term in + let ty = apply_subst subst ty in + (i, (context, term, ty))) subst in - let flatten_fast subst = - let resolve_meta (i, (context, term, ty)) subst = - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty)) - in - let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in - let filter j (i,_) = i <> j in - let filter a b = profiler4.HExtlib.profile (filter a) b in - List.fold_left - (fun subst (j,(c,t,ty)) as s -> - let s = resolve_meta s subst in - s::(List.filter (filter j) subst)) - subst subst - in - (*let flatten subst = profiler.HExtlib.profile flatten subst in*) - let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in - (*let subst = flatten subst in*) -(* let subst = flatten_fast subst in*) + let flatten subst = profiler.HExtlib.profile flatten subst in + let subst = flatten subst in *) subst, menv, ug ;; exception MatchingFailure;; -let matching1 metasenv1 metasenv2 context t1 t2 ugraph = +(** matching takes in input the _disjoint_ metasenv of t1 and t2; +it perform unification in the union metasenv, then check that +the first metasenv has not changed *) +let matching metasenv1 metasenv2 context t1 t2 ugraph = try unification_aux false metasenv1 metasenv2 context t1 t2 ugraph with - CicUnification .UnificationFailure _ -> - raise MatchingFailure -;; - -let unification = unification_aux true -;; - - - -(* -let unification metasenv1 metasenv2 context t1 t2 ugraph = - let (subst, metasenv, ugraph) = - CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "fo_unif"); - (subst, metasenv, ugraph) - -;; -*) - - -(* -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 = - match s, t with - | s, t when s = t -> subst, menv - | 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 - | 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 - | 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 Invalid_argument _ -> - raise MatchingFailure - ) - | _, _ -> - raise MatchingFailure - in - let subst, menv = do_match [] metasenv t1 t2 in - subst, menv, ugraph -;; -*) - -(* -let matching metasenv context t1 t2 ugraph = - try - let subst, metasenv, ugraph = - try - unification metasenv context t1 t2 ugraph - with CicUtil.Meta_not_found _ as exn -> - Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!" - (CicPp.ppterm t1) (CicPp.ppterm t2) - (CicMetaSubst.ppmetasenv [] metasenv); - raise exn - in - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "qua-2"); - let t' = CicMetaSubst.apply_subst subst t1 in - if not (meta_convertibility t1 t') then - raise MatchingFailure - else - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "qua-1"); - let metas = metas_of_term t1 in - let subst = - List.map - (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst in - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "qua0"); - - let subst, metasenv = - List.fold_left - (fun - (subst,metasenv) s -> - match s with - | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas -> - let metasenv' = - List.filter (fun (x, _, _) -> x<>j) metasenv - in - ((j, (c, Cic.Meta (i, lc), ty))::subst, - (i,c,ty)::metasenv') - |_ -> s::subst,metasenv) ([],metasenv) subst - in - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "qua1"); -(* - 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 *) - if CicMetaSubst.apply_subst subst t1 = t1 then - subst, metasenv, ugraph - else - (prerr_endline "mah"; raise MatchingFailure) - with - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> + CicUnification.UnificationFailure _ -> raise MatchingFailure ;; -*) -(** matching takes in input the _disjoint_ metasenv of t1 and t2; -it perform unification in the union metasenv, then check that -the first metasenv has not changed *) - - -let matching2 metasenv1 metasenv2 context t1 t2 ugraph = - let subst, metasenv, ugraph = - try - unification metasenv1 metasenv2 context t1 t2 ugraph - with - CicUtil.Meta_not_found _ as exn -> - Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!" - (CicPp.ppterm t1) (CicPp.ppterm t2) - (CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2)); - raise exn - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> - raise MatchingFailure - in - if Utils.debug_res then - ignore(check_disjoint_invariant subst metasenv "qua-2"); - (* let us unfold subst *) - if metasenv = metasenv1 then - let subst = - List.map - (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst in - subst, metasenv, ugraph (* everything is fine *) - else - (* let us unfold subst *) - (* - let subst = - List.map - (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst in - *) - (* let us revert Meta-Meta in subst privileging metasenv1 *) - let subst, metasenv = - List.fold_left - (fun - (subst,metasenv) s -> - match s with - | (i, (c, Cic.Meta (j, lc), ty)) - when (List.exists (fun (x, _, _) -> x=i) metasenv1) && - not (List.exists (fun (x, _) -> x=j) subst) -> - let metasenv' = - List.filter (fun (x, _, _) -> x<>j) metasenv - in - ((j, (c, Cic.Meta (i, lc), ty))::subst, - (i,c,ty)::metasenv') - |_ -> s::subst,metasenv) ([],metasenv) subst - in - (* finally, let us chek again that metasenv = metasenv1 *) - if metasenv = metasenv1 then - subst, metasenv, ugraph - else raise MatchingFailure +let unification m1 m2 c t1 t2 ug = + try + unification_aux true m1 m2 c t1 t2 ug + with exn -> + raise exn ;; -(* debug -let matching metasenv1 metasenv2 context t1 t2 ugraph = - let rc1 = - try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph) - with MatchingFailure -> None - in - let rc2 = - try - Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph) - with MatchingFailure -> None - in - match rc1,rc2 with - | Some (s,m,g) , None -> - prerr_endline (CicPp.ppterm t1); - prerr_endline (CicPp.ppterm t2); - prerr_endline "SOLO NOI"; - prerr_endline (CicMetaSubst.ppsubst s); - s,m,g - | None , Some _ -> - prerr_endline (CicPp.ppterm t1); - prerr_endline (CicPp.ppterm t2); - prerr_endline "SOLO LUI"; - assert false - | None, None -> raise MatchingFailure - | Some (s,m,g), Some (s',m',g') -> - let s = List.sort (fun (i,_) (j,_) -> i - j) s in - let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in - if s <> s' then - begin - prerr_endline (CicMetaSubst.ppsubst s); - prerr_endline (CicMetaSubst.ppsubst s'); - prerr_endline (CicPp.ppterm t1); - prerr_endline (CicPp.ppterm t2); - end; - s,m,g -*) -let matching = matching1;; let check_eq context msg eq = let w, proof, (eq_ty, left, right, order), metas = eq in @@ -761,7 +211,7 @@ let find_equalities context proof = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let eq_uri = LibraryObjects.eq_URI () in + let eq_uri = Utils.eq_URI () in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv @@ -791,8 +241,8 @@ let find_equalities context proof = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let proof = BasicProof p in - let e = (w, proof, stat, newmetas) in + let proof = Equality.Exact p in + let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -804,15 +254,17 @@ let find_equalities context proof = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof (C.Rel index), stat, []) in + let p = C.Rel index in + let proof = Equality.Exact p in + let e = Equality.mk_equality (w, proof,stat,[]) in Some e, (newmeta+1) | _ -> None, newmeta in ( match do_find context term with | Some p, newmeta -> let tl, newmeta' = (aux (index+1) newmeta tl) in - if newmeta' < newmeta then - prerr_endline "big trouble"; + if newmeta' < newmeta then + prerr_endline "big trouble"; (index, p)::tl, newmeta' (* max???? *) | None, _ -> aux (index+1) newmeta tl @@ -822,7 +274,7 @@ let find_equalities context proof = in let il, maxm = aux 1 newmeta context in let indexes, equalities = List.split il in - ignore (List.iter (check_eq context "find") equalities); + (* ignore (List.iter (check_eq context "find") equalities); *) indexes, equalities, maxm ;; @@ -897,7 +349,7 @@ let find_library_equalities dbd context status maxmeta = eqs) in let eq_uri1 = eq_XURI () - and eq_uri2 = LibraryObjects.eq_URI () in + and eq_uri2 = Utils.eq_URI () in let iseq uri = (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) in @@ -912,7 +364,7 @@ let find_library_equalities dbd context status maxmeta = | C.LetIn (_, s, t) | C.Cast (s, t) -> (has_vars s) || (has_vars t) | _ -> false - in + in let rec aux newmeta = function | [] -> [], newmeta | (uri, term, termty)::tl -> @@ -932,17 +384,17 @@ let find_library_equalities dbd context status maxmeta = else C.Appl (term::args) in ( - match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (iseq uri) && (ok_types ty newmetas) -> + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when (iseq uri) && (ok_types ty newmetas) -> debug_print (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let proof = BasicProof p in - let e = (w, proof, stat, newmetas) in + let proof = Equality.Exact p in + let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -951,28 +403,30 @@ let find_library_equalities dbd context status maxmeta = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof term, stat, []) in + let proof = Equality.Exact term in + let e = Equality.mk_equality (w, proof, stat, []) in Some e, (newmeta+1) | _ -> None, newmeta in match res with | Some e -> let tl, newmeta' = aux newmeta tl in - if newmeta' < newmeta then - prerr_endline "big trouble"; + if newmeta' < newmeta then + prerr_endline "big trouble"; (uri, e)::tl, newmeta' (* max???? *) | None -> aux newmeta tl in let found, maxm = aux maxmeta candidates in let uriset, eqlist = + let mceq = Equality.meta_convertibility_eq in (List.fold_left (fun (s, l) (u, e) -> - if List.exists (meta_convertibility_eq e) (List.map snd l) then ( + if List.exists (mceq e) (List.map snd l) then ( debug_print (lazy (Printf.sprintf "NO!! %s already there!" - (string_of_equality e))); + (Equality.string_of_equality e))); (UriManager.UriSet.add u s, l) ) else (UriManager.UriSet.add u s, (u, e)::l)) (UriManager.UriSet.empty, []) found) @@ -1038,225 +492,4 @@ let find_context_hypotheses env equalities_indexes = res ;; - -let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) = - let table = Hashtbl.create (List.length args) in - - let newargs, newmeta = - List.fold_right - (fun t (newargs, index) -> - match t with - | Cic.Meta (i, l) -> - if Hashtbl.mem table i then - let idx = Hashtbl.find table i in - ((Cic.Meta (idx, l))::newargs, index+1) - else - let _ = Hashtbl.add table i index in - ((Cic.Meta (index, l))::newargs, index+1) - | _ -> assert false) - args ([], newmeta+1) - in - - let repl where = - ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs - ~where - in - let menv' = - List.fold_right - (fun (i, context, term) menv -> - try - let index = Hashtbl.find table i in - (index, context, term)::menv - with Not_found -> - (i, context, term)::menv) - menv [] - in - let ty = repl ty - and left = repl left - and right = repl right in - let metas = - (metas_of_term left) @ - (metas_of_term right) @ - (metas_of_term ty) @ (metas_of_proof p) in - let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in - let newargs = - List.filter - (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs - in - let _ = - if List.length metas > 0 then - let first = List.hd metas in - (* this new equality might have less variables than its parents: here - we fill the gap with a dummy arg. Example: - with (f X Y) = X we can simplify - (g X) = (f X Y) in - (g X) = X. - So the new equation has only one variable, but it still has type like - \lambda X,Y:..., so we need to pass a dummy arg for Y - (I hope this makes some sense...) - *) - Hashtbl.iter - (fun k v -> - if not (List.exists - (function Cic.Meta (i, _) -> i = v | _ -> assert false) - newargs) then - Hashtbl.replace table k first) - (Hashtbl.copy table) - in - let rec fix_proof = function - | NoProof -> NoProof - | BasicProof term -> BasicProof (repl term) - | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) -> - let subst' = - List.fold_left - (fun s arg -> - match arg with - | Cic.Meta (i, l) -> ( - try - let j = Hashtbl.find table i in - if List.mem_assoc i subst then - s - else - let _, context, ty = CicUtil.lookup_meta i menv in - (i, (context, Cic.Meta (j, l), ty))::s - with Not_found | CicUtil.Meta_not_found _ -> - s - ) - | _ -> assert false) - [] args - in - ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p) - | p -> assert false - in - let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in - (newmeta +1, neweq) -;; - - -let relocate newmeta menv = - let subst, metasenv, newmeta = - List.fold_right - (fun (i, context, ty) (subst, menv, maxmeta) -> - let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in - let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in - let newmeta = maxmeta, context, ty in - newsubst::subst, newmeta::menv, maxmeta+1) - menv ([], [], newmeta+1) - in - let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in - let subst = - List.map - (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst in - subst, metasenv, newmeta - - -let fix_metas newmeta (w, p, (ty, left, right, o), menv) = - (* - let metas = (metas_of_term left)@(metas_of_term right) - @(metas_of_term ty)@(metas_of_proof p) in - let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in - *) - (* debug - let _ , eq = - fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in - prerr_endline (string_of_equality eq); *) - let subst, metasenv, newmeta = relocate newmeta menv in - let ty = CicMetaSubst.apply_subst subst ty in - let left = CicMetaSubst.apply_subst subst left in - let right = CicMetaSubst.apply_subst subst right in - let rec fix_proof = function - | NoProof -> NoProof - | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term) - | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) -> - (* - let newsubst = - List.map - (fun (i, (context, term, ty)) -> - let context = CicMetaSubst.apply_subst_context subst context in - let term = CicMetaSubst.apply_subst subst term in - let ty = CicMetaSubst.apply_subst subst ty in - (i, (context, term, ty))) subst' in *) - ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p) - | p -> assert false - in - let p = fix_proof p in - (* - let metas = (metas_of_term left)@(metas_of_term right) - @(metas_of_term ty)@(metas_of_proof p) in - let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in - *) - let eq = (w, p, (ty, left, right, o), metasenv) in - (* debug prerr_endline (string_of_equality eq); *) - newmeta+1, eq - -let term_is_equality term = - let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in - match term with - | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true - | _ -> false -;; - - -exception TermIsNotAnEquality;; - -let equality_of_term proof term = - let eq_uri = LibraryObjects.eq_URI () in - let iseq uri = UriManager.eq uri eq_uri in - match term with - | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let e = (w, BasicProof proof, stat, []) in - e - | _ -> - raise TermIsNotAnEquality -;; - - -type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; - -let is_weak_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv) -> - (left = right || - (meta_convertibility left right)) - (* the test below is not a good idea since it stops - demodulation too early *) - (* (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph)))*) -;; - -let is_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv) -> - (left = right || - (* (meta_convertibility left right)) *) - (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph))) -;; - - -let term_of_equality equality = - let _, _, (ty, left, right, _), menv = equality in - let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in - let argsno = List.length menv in - let t = - CicSubstitution.lift argsno - (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right]) - in - snd ( - List.fold_right - (fun (i,_,ty) (n, t) -> - let name = Cic.Name ("X" ^ (string_of_int n)) in - let ty = CicSubstitution.lift (n-1) ty in - let t = - ProofEngineReduction.replace - ~equality:eq ~what:[i] - ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t - in - (n-1, Cic.Prod (name, ty, t))) - menv (argsno, t)) -;; +let get_stats () = <:show> ;;