X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=2bf3600f289d4de84e76daa71a2f3197bd78c1bb;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=6c0b24327d6fca5dcedc1a0417d8f6caa8999056;hpb=2b4dcaef8f1bef33eeb27e760a1fe518a58edc8a;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 6c0b24327..2bf3600f2 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -1,4 +1,4 @@ -(* cOpyright (C) 2005, HELM Team. +(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,198 +23,13 @@ * http://cs.unibo.it/helm/. *) -(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *) - - -(******* CIC substitution ***************************************************) - -type cic_substitution = Cic.substitution -let cic_apply_subst = CicMetaSubst.apply_subst -let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv -let cic_ppsubst = CicMetaSubst.ppsubst -let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail -let cic_flatten_subst subst = - List.map - (fun (i, (context, term, ty)) -> - let context = (* cic_apply_subst_context subst*) context in - let term = cic_apply_subst subst term in - let ty = cic_apply_subst subst ty in - (i, (context, term, ty))) subst -let rec cic_lookup_subst meta subst = - match meta with - | Cic.Meta (i, _) -> ( - try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst - in cic_lookup_subst t subst - with Not_found -> meta - ) - | _ -> meta -;; - -let cic_merge_subst_if_possible s1 s2 = - let already_in = Hashtbl.create 13 in - let rec aux acc = function - | ((i,_,x) as s)::tl -> - (try - let x' = Hashtbl.find already_in i in - if x = x' then aux acc tl else None - with - | Not_found -> - Hashtbl.add already_in i x; - aux (s::acc) tl) - | [] -> Some acc - in - aux [] (s1@s2) -;; - -(******** NAIF substitution **************************************************) -(* - * naif version of apply subst; the local context of metas is ignored; - * we assume the substituted term must be lifted according to the nesting - * depth of the meta. - * Alternatively, we could used implicit instead of metas - *) - -type naif_substitution = (int * Cic.term) list - -let naif_apply_subst subst term = - let rec aux k t = - match t with - Cic.Rel _ -> t - | Cic.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.Var (uri, exp_named_subst') - | Cic.Meta (i, l) -> - (try - aux k (CicSubstitution.lift k (List.assoc i subst)) - with Not_found -> t) - | Cic.Sort _ - | Cic.Implicit _ -> t - | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty) - | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t) - | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t) - | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t) - | Cic.Appl [] -> assert false - | Cic.Appl l -> Cic.Appl (List.map (aux k) l) - | Cic.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - if exp_named_subst' != exp_named_subst then - Cic.Const (uri, exp_named_subst') - else - t (* TODO: provare a mantenere il piu' possibile sharing *) - | Cic.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.MutInd (uri,typeno,exp_named_subst') - | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.MutConstruct (uri,typeno,consno,exp_named_subst') - | Cic.MutCase (sp,i,outty,t,pl) -> - let pl' = List.map (aux k) pl in - Cic.MutCase (sp, i, aux k outty, aux k t, pl') - | Cic.Fix (i, fl) -> - let len = List.length fl in - let fl' = - List.map - (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl - in - Cic.Fix (i, fl') - | Cic.CoFix (i, fl) -> - let len = List.length fl in - let fl' = - List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl - in - Cic.CoFix (i, fl') -in - aux 0 term -;; - -(* naif version of apply_subst_metasenv: we do not apply the -substitution to the context *) - -let naif_apply_subst_metasenv subst metasenv = - List.map - (fun (n, context, ty) -> - (n, context, naif_apply_subst subst ty)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv) - -let naif_ppsubst names subst = - "{" ^ String.concat "; " - (List.map - (fun (idx, t) -> - Printf.sprintf "%d:= %s" idx (CicPp.pp t names)) - subst) ^ "}" -;; - -let naif_buildsubst n context t ty tail = (n,t) :: tail ;; - -let naif_flatten_subst subst = - List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst -;; - -let rec naif_lookup_subst meta subst = - match meta with - | Cic.Meta (i, _) -> - (try - naif_lookup_subst (List.assoc i subst) subst - with - Not_found -> meta) - | _ -> meta -;; - -let naif_merge_subst_if_possible s1 s2 = - let already_in = Hashtbl.create 13 in - let rec aux acc = function - | ((i,x) as s)::tl -> - (try - let x' = Hashtbl.find already_in i in - if x = x' then aux acc tl else None - with - | Not_found -> - Hashtbl.add already_in i x; - aux (s::acc) tl) - | [] -> Some acc - in - aux [] (s1@s2) -;; - -(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************) - -type substitution = naif_substitution -let apply_subst = naif_apply_subst -let apply_subst_metasenv = naif_apply_subst_metasenv -let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l -let buildsubst = naif_buildsubst -let flatten_subst = naif_flatten_subst -let lookup_subst = naif_lookup_subst - -(* 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 -;; - -let is_in_subst i subst = List.mem_assoc i subst;; - -let merge_subst_if_possible = naif_merge_subst_if_possible;; - -let empty_subst = [];; +(* let _profiler = <:profiler<_profiler>>;; *) -(********* EQUALITY **********************************************************) +(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *) type rule = SuperpositionRight | SuperpositionLeft | Demodulation type uncomparable = int -> int + type equality = uncomparable * (* trick to break structural equality *) int * (* weight *) @@ -225,102 +40,121 @@ type equality = Utils.comparison) * (* ordering *) Cic.metasenv * (* environment for metas *) int (* id *) -and proof = new_proof * old_proof - -and new_proof = +and proof = | Exact of Cic.term - | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *) -and old_proof = - | NoProof (* term is the goal missing a proof *) - | BasicProof of substitution * Cic.term - | ProofBlock of - substitution * UriManager.uri * - (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof - | ProofGoalBlock of old_proof * old_proof - | ProofSymBlock of Cic.term list * old_proof - | SubProof of Cic.term * int * old_proof -and goal_proof = (Utils.pos * int * substitution * Cic.term) list + | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) + (* subst, (rule,eq1, eq2,predicate) *) +and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; +(* the hashtbl eq_id -> proof, max_eq_id *) +module IntOt = struct type t = int let compare = Pervasives.compare end +module M = Map.Make(IntOt) +type equality_bag = equality M.t * int + +type goal = goal_proof * Cic.metasenv * Cic.term (* globals *) -let maxid = ref 0;; -let id_to_eq = Hashtbl.create 1024;; +let mk_equality_bag () = M.empty, 10000 ;; -let freshid () = - incr maxid; !maxid -;; +let freshid (m,i) = (m,i+1), i+1 ;; -let reset () = - maxid := 0; - Hashtbl.clear id_to_eq -;; +let add_to_bag (id_to_eq,i) id eq = M.add id eq id_to_eq,i ;; let uncomparable = fun _ -> 0 -let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = - let id = freshid () in - let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in - Hashtbl.add id_to_eq id eq; - eq +let mk_equality bag (weight,p,(ty,l,r,o),m) = + let bag, id = freshid bag in + let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in + let bag = add_to_bag bag id eq in + bag, eq ;; +let mk_tmp_equality (weight,(ty,l,r,o),m) = + let id = -1 in + uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id +;; + + let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) +let id_of e = + let _,_,_,_,id = open_equality e in id +;; + + +let string_of_rule = function + | SuperpositionRight -> "SupR" + | SuperpositionLeft -> "SupL" + | Demodulation -> "Demod" +;; + let string_of_equality ?env eq = match env with | None -> - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* "..." *) | Some (_, context, _) -> let names = Utils.names_of_context context in - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.pp ty names) (CicPp.pp left names) (Utils.string_of_comparison o) (CicPp.pp right names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* "..." *) ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = Pervasives.compare s1 s2 ;; -let rec string_of_proof_old ?(names=[]) = function - | NoProof -> "NoProof " - | BasicProof (s, t) -> "BasicProof(" ^ - ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")" - | SubProof (t, i, p) -> - Printf.sprintf "SubProof(%s, %s, %s)" - (CicPp.pp t names) (string_of_int i) (string_of_proof_old p) - | ProofSymBlock (_,p) -> - Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p) - | ProofBlock (subst, _, _, _ ,(_,eq),old) -> - let _,(_,p),_,_,_ = open_equality eq in - "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^ - string_of_proof_old p ^ ")" - | ProofGoalBlock (p1, p2) -> - Printf.sprintf "ProofGoalBlock(%s, %s)" - (string_of_proof_old p1) (string_of_proof_old p2) -;; - - -let proof_of_id id = +let rec max_weight_in_proof ((id_to_eq,_) as bag) current = + function + | Exact _ -> current + | Step (_, (_,id1,(_,id2),_)) -> + let eq1 = M.find id1 id_to_eq in + let eq2 = M.find id2 id_to_eq in + let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in + let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in + let current = max current w1 in + let current = max_weight_in_proof bag current p1 in + let current = max current w2 in + max_weight_in_proof bag current p2 + +let max_weight_in_goal_proof ((id_to_eq,_) as bag) = + List.fold_left + (fun current (_,_,id,_,_) -> + let eq = M.find id id_to_eq in + let (w,p,(_,_,_,_),_,_) = open_equality eq in + let current = max current w in + max_weight_in_proof bag current p) + +let max_weight bag goal_proof proof = + let current = max_weight_in_proof bag 0 proof in + max_weight_in_goal_proof bag current goal_proof + +let proof_of_id (id_to_eq,_) id = try - let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in p,l,r with - Not_found -> assert false + Not_found -> + prerr_endline ("Unable to find the proof of " ^ string_of_int id); + assert false +;; +let is_in (id_to_eq,_) id = + M.mem id id_to_eq +;; -let string_of_proof_new ?(names=[]) p gp = - let str_of_rule = function - | SuperpositionRight -> "SupR" - | SuperpositionLeft -> "SupL" - | Demodulation -> "Demod" - in + +let string_of_proof ?(names=[]) bag p gp = let str_of_pos = function | Utils.Left -> "left" | Utils.Right -> "right" @@ -333,30 +167,50 @@ let string_of_proof_new ?(names=[]) p gp = prefix (CicPp.pp t names) | Step (subst,(rule,eq1,(pos,eq2),pred)) -> Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n" - prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) + prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ - aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ - aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) + aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id bag eq1)) ^ + aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id bag eq2)) in aux 0 "" p ^ String.concat "\n" (List.map - (fun (pos,i,s,t) -> + (fun (r,pos,i,s,t) -> (Printf.sprintf - "GOAL: %s %d %s %s\n" - (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ - aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) + "GOAL: %s %s %d %s %s\n" (string_of_rule r) + (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ + aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id bag i))) gp) ;; -let ppsubst = ppsubst ~names:[] +let rec depend ((id_to_eq,_) as bag) eq id seen = + let (_,p,(_,_,_,_),_,ideq) = open_equality eq in + if List.mem ideq seen then + false,seen + else + if id = ideq then + true,seen + else + match p with + | Exact _ -> false,seen + | Step (_,(_,id1,(_,id2),_)) -> + let seen = ideq::seen in + let eq1 = M.find id1 id_to_eq in + let eq2 = M.find id2 id_to_eq in + let b1,seen = depend bag eq1 id seen in + if b1 then b1,seen else depend bag eq2 id seen +;; + +let depend bag eq id = fst (depend bag eq id []);; + +let ppsubst = Subst.ppsubst ~names:[];; (* returns an explicit named subst and a list of arguments for sym_eq_URI *) let build_ens uri termlist = let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match obj with | Cic.Constant (_, _, _, uris, _) -> - assert (List.length uris <= List.length termlist); + (* assert (List.length uris <= List.length termlist); *) let rec aux = function | [], tl -> [], tl | (uri::uris), (term::tl) -> @@ -368,61 +222,6 @@ let build_ens uri termlist = | _ -> assert false ;; -let build_proof_term_old ?(noproof=Cic.Implicit None) proof = - let rec do_build_proof proof = - match proof with - | NoProof -> - Printf.fprintf stderr "WARNING: no proof!\n"; - noproof - | BasicProof (s,term) -> apply_subst s 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 (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), (ty, what, other, _), menv',_ = open_equality eq in - let proof' = do_build_proof proof in - let eqproof = do_build_proof eqproof in - let what, other = - if pos = Utils.Left then what, other else other, what - in - 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 mk_sym uri ty t1 t2 p = let ens, args = build_ens uri [ty;t1;t2;p] in Cic.Appl (Cic.Const(uri, ens) :: args) @@ -434,7 +233,8 @@ let mk_trans uri ty t1 t2 t3 p12 p23 = ;; let mk_eq_ind uri ty what pred p1 other p2 = - Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2] + let ens, args = build_ens uri [ty; what; pred; p1; other; p2] in + Cic.Appl (Cic.Const (uri, ens) :: args) ;; let p_of_sym ens tl = @@ -451,7 +251,74 @@ let open_trans ens tl = | _ -> assert false ;; -let canonical t = +let open_sym ens tl = + let args = List.map snd ens @ tl in + match args with + | [ty;l;r;p] -> ty,l,r,p + | _ -> assert false +;; + +let open_eq_ind args = + match args with + | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr + | _ -> assert false +;; + +let open_pred pred = + match pred with + | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) + when LibraryObjects.is_eq_URI uri -> ty,uri,l,r + | _ -> Utils.debug_print (lazy (CicPp.ppterm pred)); assert false +;; + +let is_not_fixed t = + CicSubstitution.subst (Cic.Implicit None) t <> + CicSubstitution.subst (Cic.Rel 1) t +;; + +let canonical t context menv = + let remove_cycles t = + let is_transitive = + function + Cic.Appl (Cic.Const (uri_trans,_)::_) + when LibraryObjects.is_trans_eq_URI uri_trans -> + true + | _ -> false in + let rec collect = + function + Cic.Appl (Cic.Const (uri_trans,ens)::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,p1,p2 = open_trans ens tl in + (if is_transitive p1 then fst (collect p1) else [l,p1]) @ + (if is_transitive p2 then fst (collect p2) else [m,p2]), + (r, uri_trans, ty) + | t -> assert false in + let rec cut_to_last_duplicate l acc = + function + [] -> List.rev acc + | (l',p)::tl when l=l' -> +if acc <> [] then +Utils.debug_print (lazy ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI")); + cut_to_last_duplicate l [l',p] tl + | (l',p)::tl -> + cut_to_last_duplicate l ((l',p)::acc) tl + in + let rec rebuild = + function + (l,_)::_::_ as steps, ((r,uri_trans,ty) as last) -> + (match cut_to_last_duplicate l [] steps with + (l,p1)::((m,_)::_::_ as tl) -> + mk_trans uri_trans ty l m r p1 (rebuild (tl,last)) + | [l,p1 ; m,p2] -> mk_trans uri_trans ty l m r p1 p2 + | [l,p1] -> p1 + | [] -> assert false) + | _ -> assert false + in + if is_transitive t then + rebuild (collect t) + else + t + in let rec remove_refl t = match t with | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args) @@ -464,355 +331,609 @@ let canonical t = remove_refl p1 | _ -> Cic.Appl (List.map remove_refl args)) | Cic.Appl l -> Cic.Appl (List.map remove_refl l) + | Cic.LetIn (name,bo,ty,rest) -> + Cic.LetIn (name,remove_refl bo,remove_refl ty,remove_refl rest) | _ -> t in - let rec canonical t = + let rec canonical_trough_lambda context = function + | Cic.Lambda(name,ty,bo) -> + let context' = (Some (name,Cic.Decl ty))::context in + Cic.Lambda(name,ty,canonical_trough_lambda context' bo) + | t -> canonical context t + + and canonical context t = match t with + | Cic.LetIn(name,bo,ty,rest) -> + let bo = canonical_trough_lambda context bo in + let ty = canonical_trough_lambda context ty in + let context' = (Some (name,Cic.Def (bo,ty)))::context in + Cic.LetIn(name,bo,ty,canonical context' rest) | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args) when LibraryObjects.is_sym_eq_URI uri_sym -> (match p_of_sym ens tl with | Cic.Appl ((Cic.Const(uri,ens))::tl) when LibraryObjects.is_sym_eq_URI uri -> - canonical (p_of_sym ens tl) + canonical context (p_of_sym ens tl) | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) when LibraryObjects.is_trans_eq_URI uri_trans -> let ty,l,m,r,p1,p2 = open_trans ens tl in mk_trans uri_trans ty r m l - (canonical (mk_sym uri_sym ty m r p2)) - (canonical (mk_sym uri_sym ty l m p1)) - | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) - when LibraryObjects.is_eq_ind_URI uri_ind || - LibraryObjects.is_eq_ind_r_URI uri_ind -> - let ty, what, pred, p1, other, p2 = - match tl with - | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2 - | _ -> assert false - in - let pred,l,r = - match pred with - | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r]) - when LibraryObjects.is_eq_URI uri -> - Cic.Lambda - (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r - | _ -> - prerr_endline (CicPp.ppterm pred); - assert false + (canonical context (mk_sym uri_sym ty m r p2)) + (canonical context (mk_sym uri_sym ty l m p1)) + | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) + when LibraryObjects.is_eq_f_URI uri_feq -> + let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in + let eq_f_sym = + Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, []) in - let l = CicSubstitution.subst what l in - let r = CicSubstitution.subst what r in - Cic.Appl - [he;ty;what;pred; - canonical (mk_sym uri_sym ty l r p1);other;canonical p2] + let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in + Utils.debug_print (lazy ("CANONICAL " ^ CicPp.ppterm rc)); + rc | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t when LibraryObjects.is_eq_URI uri -> t - | _ -> Cic.Appl (List.map canonical args)) - | Cic.Appl l -> Cic.Appl (List.map canonical l) + | _ -> Cic.Appl (List.map (canonical context) args)) + | Cic.Appl l -> Cic.Appl (List.map (canonical context) l) | _ -> t in - remove_refl (canonical t) + remove_cycles (remove_refl (canonical context t)) +;; + +let compose_contexts ctx1 ctx2 = + ProofEngineReduction.replace_lifting + ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1 +;; + +let put_in_ctx ctx t = + ProofEngineReduction.replace_lifting + ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx +;; + +let mk_eq uri ty l r = + let ens, args = build_ens uri [ty; l; r] in + Cic.Appl (Cic.MutInd(uri,0,ens) :: args) +;; + +let mk_refl uri ty t = + let ens, args = build_ens uri [ty; t] in + Cic.Appl (Cic.MutConstruct(uri,0,1,ens) :: args) ;; -let build_proof_step subst p1 p2 pos l r pred = - let p1 = apply_subst subst p1 in - let p2 = apply_subst subst p2 in - let l = apply_subst subst l in - let r = apply_subst subst r in - let pred = apply_subst subst pred in - let ty,body = (* Cic.Implicit None *) +let open_eq = function + | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri -> + uri, ty, l ,r + | _ -> assert false +;; + +let mk_feq uri_feq ty ty1 left pred right t = + let ens, args = build_ens uri_feq [ty;ty1;pred;left;right;t] in + Cic.Appl (Cic.Const(uri_feq,ens) :: args) +;; + +let rec look_ahead aux = function + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty1,what,pred,p1,other,p2 = open_eq_ind tl in + let ty2,eq,lp,rp = open_pred pred in + let hole = Cic.Implicit (Some `Hole) in + let ty2 = CicSubstitution.subst hole ty2 in + aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t + | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t) + | t -> t +;; + +let contextualize uri ty left right t = + let hole = Cic.Implicit (Some `Hole) in + (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [t] + * + * the parameters validate this invariant + * t: eq(uri) ty left right + * that is used only by the base case + * + * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context + * ctx_ty is the type of ctx + *) + let rec aux uri ty left right ctx_d ctx_ty t = + match t with + | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) + when LibraryObjects.is_sym_eq_URI uri_sym -> + let ty,l,r,p = open_sym ens tl in + mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p) + | Cic.LetIn (name,body,bodyty,rest) -> + Cic.LetIn + (name,look_ahead (aux uri) body, bodyty, + aux uri ty left right ctx_d ctx_ty rest) + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty1,what,pred,p1,other,p2 = open_eq_ind tl in + let ty2,eq,lp,rp = open_pred pred in + let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in + let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in + let is_not_fixed_lp = is_not_fixed lp in + let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in + (* extract the context and the fixed term from the predicate *) + let m, ctx_c, ty2 = + let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in + (* they were under a lambda *) + let m = CicSubstitution.subst hole m in + let ctx_c = CicSubstitution.subst hole ctx_c in + let ty2 = CicSubstitution.subst hole ty2 in + m, ctx_c, ty2 + in + (* create the compound context and put the terms under it *) + let ctx_dc = compose_contexts ctx_d ctx_c in + let dc_what = put_in_ctx ctx_dc what in + let dc_other = put_in_ctx ctx_dc other in + (* m is already in ctx_c so it is put in ctx_d only *) + let d_m = put_in_ctx ctx_d m in + (* we also need what in ctx_c *) + let c_what = put_in_ctx ctx_c what in + (* now put the proofs in the compound context *) + let p1 = (* p1: dc_what = d_m *) + if is_not_fixed_lp then + aux uri ty2 c_what m ctx_d ctx_ty p1 + else + mk_sym uri_sym ctx_ty d_m dc_what + (aux uri ty2 m c_what ctx_d ctx_ty p1) + in + let p2 = (* p2: dc_other = dc_what *) + if avoid_eq_ind then + mk_sym uri_sym ctx_ty dc_what dc_other + (aux uri ty1 what other ctx_dc ctx_ty p2) + else + aux uri ty1 other what ctx_dc ctx_ty p2 + in + (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m + if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *) + let a,b,c,paeqb,pbeqc = + if is_not_fixed_lp then + dc_other,dc_what,d_m,p2,p1 + else + d_m,dc_what,dc_other, + (mk_sym uri_sym ctx_ty dc_what d_m p1), + (mk_sym uri_sym ctx_ty dc_other dc_what p2) + in + mk_trans uri_trans ctx_ty a b c paeqb pbeqc + | t when ctx_d = hole -> t + | t -> +(* let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *) +(* let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *) + + let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in + let pred = +(* let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *) + let l = + let ctx_d = CicSubstitution.lift 1 ctx_d in + put_in_ctx ctx_d (Cic.Rel 1) + in +(* let lty = CicSubstitution.lift 1 ctx_ty in *) +(* Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) *) + Cic.Lambda (Cic.Name "foo",ty,l) + in +(* let d_left = put_in_ctx ctx_d left in *) +(* let d_right = put_in_ctx ctx_d right in *) +(* let refl_eq = mk_refl uri ctx_ty d_left in *) +(* mk_sym uri_sym ctx_ty d_right d_left *) +(* (mk_eq_ind uri_ind ty left pred refl_eq right t) *) + (mk_feq uri_feq ty ctx_ty left pred right t) + in + aux uri ty left right hole ty t +;; + +let contextualize_rewrites t ty = + let eq,ty,l,r = open_eq ty in + contextualize eq ty l r t +;; + +let add_subst subst = + function + | Exact t -> Exact (Subst.apply_subst subst t) + | Step (s,(rule, id1, (pos,id2), pred)) -> + Step (Subst.concat subst s,(rule, id1, (pos,id2), pred)) +;; + +let build_proof_step eq lift subst p1 p2 pos l r pred = + let p1 = Subst.apply_subst_lift lift subst p1 in + let p2 = Subst.apply_subst_lift lift subst p2 in + let l = CicSubstitution.lift lift l in + let l = Subst.apply_subst_lift lift subst l in + let r = CicSubstitution.lift lift r in + let r = Subst.apply_subst_lift lift subst r in + let pred = CicSubstitution.lift lift pred in + let pred = Subst.apply_subst_lift lift subst pred in + let ty,body = match pred with | Cic.Lambda (_,ty,body) -> ty,body | _ -> assert false in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) + let what, other = if pos = Utils.Left then l,r else r,l in - let is_not_fixed t = - CicSubstitution.subst (Cic.Implicit None) t <> - CicSubstitution.subst (Cic.Rel 1) t + let p = + match pos with + | Utils.Left -> + mk_eq_ind (LibraryObjects.eq_ind_URI ~eq) ty what pred p1 other p2 + | Utils.Right -> + mk_eq_ind (LibraryObjects.eq_ind_r_URI ~eq) ty what pred p1 other p2 in - match body,pos with - |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in - mk_trans uri_trans ty other what third - (mk_sym uri_sym ty what other p2) p1 - |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - mk_trans uri_trans ty other what third p2 p1 - |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - mk_trans uri_trans ty third what other p1 p2 - |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in - mk_trans uri_trans ty third what other p1 - (mk_sym uri_sym ty other what p2) - | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs - -> - let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t lhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) - (inject ty lhs m r pmr) (inject ty lhs l m plm) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2) - in - mk_trans uri_trans ty pred_of_other pred_of_what rhs - (inject ty lhs what other p2) p1 - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs - -> - let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t lhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) - (inject ty lhs m l plm) - (inject ty lhs r m pmr) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = - CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - mk_eq_ind (Utils.eq_ind_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2 - in - mk_trans uri_trans ty pred_of_other pred_of_what rhs - (inject ty lhs what other p2) p1 - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs - -> - let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t rhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) - (inject ty lhs m r pmr) - (inject ty lhs l m plm) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2) - in - mk_trans uri_trans ty lhs pred_of_what pred_of_other - p1 (inject ty rhs other what p2) - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs - -> - let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t rhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) - (inject ty lhs m l plm) - (inject ty lhs r m pmr)) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - mk_eq_ind (Utils.eq_ind_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2 - in - mk_trans uri_trans ty lhs pred_of_what pred_of_other - p1 (inject ty rhs other what p2) - | _, Utils.Left -> - mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2 - | _, Utils.Right -> - mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2 + p ;; -let build_proof_term_new proof = - let rec aux = function - | Exact term -> term - | Step (subst,(_, id1, (pos,id2), pred)) -> - let p,_,_ = proof_of_id id1 in - let p1 = aux p in - let p,l,r = proof_of_id id2 in - let p2 = aux p in - build_proof_step subst p1 p2 pos l r pred +let parametrize_proof p l r = + let uniq l = HExtlib.list_uniq (List.sort (fun (i,_) (j,_) -> Pervasives.compare i j) l) in + let mot = CicUtil.metas_of_term_set in + let parameters = uniq (mot p @ mot l @ mot r) in + (* ?if they are under a lambda? *) +(* + let parameters = + HExtlib.list_uniq (List.sort Pervasives.compare parameters) in - aux proof +*) + (* resorts l such that *hopefully* dependencies can be inferred *) + let guess_dependency p l = + match p with + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty,_,_,_,_,_ = open_eq_ind tl in + let metas = CicUtil.metas_of_term ty in + let nondep, dep = + List.partition (fun (i,_) -> List.exists (fun (j,_) -> j=i) metas) l + in + nondep@dep + | _ -> l + in + let parameters = guess_dependency p parameters in + let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in + let with_what, lift_no = + List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) + in + let p = CicSubstitution.lift (lift_no-1) p in + let p = + ProofEngineReduction.replace_lifting + ~equality:(fun _ t1 t2 -> + match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) + ~context:[] + ~what ~with_what ~where:p + in + let ty_of_m _ = Cic.Implicit (Some `Type) in + let args, proof,_ = + List.fold_left + (fun (instance,p,n) m -> + (instance@[m], + Cic.Lambda + (Cic.Name ("X"^string_of_int n), + CicSubstitution.lift (lift_no - n - 1) (ty_of_m m), + p), + n+1)) + ([Cic.Rel 1],p,1) + what + in + let instance = match args with | [x] -> x | _ -> Cic.Appl args in + proof, instance ;; -let wfo goalproof = +let wfo bag goalproof proof id = let rec aux acc id = - let p,_,_ = proof_of_id id in + let p,_,_ = proof_of_id bag id in match p with - | Exact _ -> id :: acc + | Exact _ -> if (List.mem id acc) then acc else id :: acc | Step (_,(_,id1, (_,id2), _)) -> let acc = if not (List.mem id1 acc) then aux acc id1 else acc in let acc = if not (List.mem id2 acc) then aux acc id2 else acc in id :: acc in - List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof + let acc = + match proof with + | Exact _ -> [id] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2 + in + List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof ;; -let string_of_id names id = +let string_of_id (id_to_eq,_) names id = + if id = 0 then "" else try - let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(t,l,r,_),m,_) = open_equality (M.find id id_to_eq) in match p with | Exact t -> - Printf.sprintf "%d = %s: %s = %s" id + Printf.sprintf "%d = %s: %s = %s [%s]" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) - | Step (_,(step,id1, (_,id2), _) ) -> - Printf.sprintf "%5d: %s %4d %4d %s = %s" id - (if step = SuperpositionRight then "SupR" else "Demo") - id1 id2 (CicPp.pp l names) (CicPp.pp r names) +(* "..." *) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + | Step (_,(step,id1, (dir,id2), p) ) -> + Printf.sprintf "%6d: %s %6d %6d %s =(%s) %s [%s]" id + (string_of_rule step) + id1 id2 (CicPp.pp l names) (CicPp.pp t names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + (*"..."*) with Not_found -> assert false -let pp_proof names goalproof = - String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) +let pp_proof bag names goalproof proof subst id initial_goal = + String.concat "\n" (List.map (string_of_id bag names) (wfo bag goalproof proof id)) ^ + "\ngoal:\n " ^ + (String.concat "\n " + (fst (List.fold_right + (fun (r,pos,i,s,pred) (acc,g) -> + let _,_,left,right = open_eq g in + let ty = + match pos with + | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right]) + | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left]) + in + let ty = Subst.apply_subst s ty in + ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> " + ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^ + "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst +;; + +let rec find_deps bag m i = + if M.mem i m then m + else + let p,_,_ = proof_of_id bag i in + match p with + | Exact _ -> M.add i [] m + | Step (_,(_,id1,(_,id2),_)) -> + let m = find_deps bag m id1 in + let m = find_deps bag m id2 in + (* without the uniq there is a stack overflow doing concatenation *) + let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in + let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in + M.add i xxx m +;; -let build_goal_proof l initial = - let proof = - List.fold_left - (fun current_proof (pos,id,subst,pred) -> - let p,l,r = proof_of_id id in - let p = build_proof_term_new p in - let pos = if pos = Utils.Left then Utils.Right else Utils.Left in - build_proof_step subst current_proof p pos l r pred) - initial l +let topological_sort bag l = + (* build the partial order relation *) + let m = List.fold_left (fun m i -> find_deps bag m i) M.empty l in + let m = (* keep only deps inside l *) + List.fold_left + (fun m' i -> + M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') + M.empty l in - canonical proof + let m = M.map (fun x -> Some x) m in + (* utils *) + let keys m = M.fold (fun i _ acc -> i::acc) m [] in + let split l m = List.filter (fun i -> M.find i m = Some []) l in + let purge l m = + M.mapi + (fun k v -> if List.mem k l then None else + match v with + | None -> None + | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) + m + in + let rec aux m res = + let keys = keys m in + let ok = split keys m in + let m = purge ok m in + let res = ok @ res in + if ok = [] then res else aux m res + in + let rc = List.rev (aux m []) in + rc +;; + +(* returns the list of ids that should be factorized *) +let get_duplicate_step_in_wfo bag l p = + let ol = List.rev l in + let h = Hashtbl.create 13 in + (* NOTE: here the n parameter is an approximation of the dependency + between equations. To do things seriously we should maintain a + dependency graph. This approximation is not perfect. *) + let add i = + let p,_,_ = proof_of_id bag i in + match p with + | Exact _ -> true + | _ -> + try + let no = Hashtbl.find h i in + Hashtbl.replace h i (no+1); + false + with Not_found -> Hashtbl.add h i 1;true + in + let rec aux = function + | Exact _ -> () + | Step (_,(_,i1,(_,i2),_)) -> + let go_on_1 = add i1 in + let go_on_2 = add i2 in + if go_on_1 then aux (let p,_,_ = proof_of_id bag i1 in p); + if go_on_2 then aux (let p,_,_ = proof_of_id bag i2 in p) + in + aux p; + List.iter + (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id bag id in p)) + ol; + (* now h is complete *) + let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in + let proofs = List.filter (fun (_,c) -> c > 1) proofs in + let res = topological_sort bag (List.map (fun (i,_) -> i) proofs) in + res ;; -let refl_proof ty term = - Cic.Appl - [Cic.MutConstruct - (LibraryObjects.eq_URI (), 0, 1, []); - ty; term] +let build_proof_term bag eq h lift proof = + let proof_of_id aux id = + let p,l,r = proof_of_id bag id in + try List.assoc id h,l,r with Not_found -> aux p, l, r + in + let rec aux = function + | Exact term -> + CicSubstitution.lift lift term + | Step (subst,(rule, id1, (pos,id2), pred)) -> + let p1,_,_ = proof_of_id aux id1 in + let p2,l,r = proof_of_id aux id2 in + let varname = + match rule with + | SuperpositionRight -> Cic.Name ("SupR" ^ Utils.string_of_pos pos) + | Demodulation -> Cic.Name ("DemEq"^ Utils.string_of_pos pos) + | _ -> assert false + in + let pred = + match pred with + | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b) + | _ -> assert false + in + let p = build_proof_step eq lift subst p1 p2 pos l r pred in +(* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in + if not cond then + prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2); + assert cond;*) + p + in + aux proof ;; -let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;; +let build_goal_proof ?(contextualize=true) ?(forward=false) bag eq l initial ty se context menv = + let se = List.map (fun i -> Cic.Meta (i,[])) se in + let lets = get_duplicate_step_in_wfo bag l initial in + let letsno = List.length lets in + let l = if forward then List.rev l else l in + let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in + let lets,_,h = + List.fold_left + (fun (acc,n,h) id -> + let p,l,r = proof_of_id bag id in + let cic = build_proof_term bag eq h n p in + let real_cic,instance = + parametrize_proof cic l r + in + let h = (id, instance)::lift_list h in + acc@[id,real_cic],n+1,h) + ([],0,[]) lets + in + let lets = + List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets + in + let proof,se = + let rec aux se current_proof = function + | [] -> current_proof,se + | (rule,pos,id,subst,pred)::tl -> + let p,l,r = proof_of_id bag id in + let p = build_proof_term bag eq h letsno p in + let pos = if forward then pos else + if pos = Utils.Left then Utils.Right else Utils.Left in + let varname = + match rule with + | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) + | Demodulation -> Cic.Name ("DemG"^ Utils.string_of_pos pos) + | _ -> assert false + in + let pred = + match pred with + | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b) + | _ -> assert false + in + let proof = + build_proof_step eq letsno subst current_proof p pos l r pred + in + let proof,se = aux se proof tl in + Subst.apply_subst_lift letsno subst proof, + List.map (fun x -> Subst.apply_subst(*_lift letsno*) subst x) se + in + aux se (build_proof_term bag eq h letsno initial) l + in + let n,proof = + let initial = proof in + List.fold_right + (fun (id,cic,ty) (n,p) -> + n-1, + Cic.LetIn ( + Cic.Name ("H"^string_of_int id), + cic, + ty, + p)) + lets (letsno-1,initial) + in + let proof = + if contextualize + then contextualize_rewrites proof (CicSubstitution.lift letsno ty) + else proof in + canonical proof context menv, se +;; + +let refl_proof eq_uri ty term = + Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term] +;; + +let metas_of_proof bag p = + let eq = + match LibraryObjects.eq_URI () with + | Some u -> u + | None -> + raise + (ProofEngineTypes.Fail + (lazy "No default equality defined when calling metas_of_proof")) + in + let p = build_proof_term bag eq [] 0 p in + Utils.metas_of_term p +;; + +let remove_local_context eq = + let w, p, (ty, left, right, o), menv,id = open_equality eq in + let p = Utils.remove_local_context p in + let ty = Utils.remove_local_context ty in + let left = Utils.remove_local_context left in + let right = Utils.remove_local_context right in + w, p, (ty, left, right, o), menv, id +;; -let relocate newmeta menv = - let subst, metasenv, newmeta = +let relocate newmeta menv to_be_relocated = + let subst, newmetasenv, newmeta = List.fold_right - (fun (i, context, ty) (subst, menv, maxmeta) -> - let irl = [] (* - CicMkImplicit.identity_relocation_list_for_metavariable context *) - in - let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in - let newmeta = maxmeta, context, ty in - newsubst, newmeta::menv, maxmeta+1) - menv ([], [], newmeta+1) - in - let metasenv = apply_subst_metasenv subst metasenv in - let subst = flatten_subst subst in - subst, metasenv, newmeta - - -let fix_metas newmeta eq = - let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq 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 = apply_subst subst ty in - let left = apply_subst subst left in - let right = apply_subst subst right in + (fun i (subst, metasenv, maxmeta) -> + let _,context,ty = CicUtil.lookup_meta i menv in + let irl = [] in + let newmeta = Cic.Meta(maxmeta,irl) in + let newsubst = Subst.buildsubst i context newmeta ty subst in + (* newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) *) + newsubst, (maxmeta,[],ty)::metasenv, maxmeta+1) + to_be_relocated (Subst.empty_subst, [], newmeta+1) + in + (* let subst = Subst.flatten_subst subst in *) + let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in + subst, menv, newmeta + +let fix_metas_goal (id_to_eq,newmeta) goal = + let (proof, menv, ty) = goal in + let to_be_relocated = List.map (fun i ,_,_ -> i) menv in + let subst, menv, newmeta = relocate newmeta menv to_be_relocated in + let ty = Subst.apply_subst subst ty in + let proof = + match proof with + | [] -> assert false (* is a nonsense to relocate the initial goal *) + | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl + in + (id_to_eq,newmeta+1),(proof, menv, ty) +;; + +let fix_metas (id_to_eq, newmeta) eq = + let w, p, (ty, left, right, o), menv,_ = open_equality eq in + let to_be_relocated = List.map (fun i ,_,_ -> i) menv in + let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in + let ty = Subst.apply_subst subst ty in + let left = Subst.apply_subst subst left in + let right = Subst.apply_subst subst right in let fix_proof = function - | NoProof -> NoProof - | BasicProof (subst',term) -> BasicProof (subst@subst',term) - | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) -> - (* - let newsubst = - List.map - (fun (i, (context, term, ty)) -> - 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 *) - ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p) - | p -> assert false - in - let fix_new_proof = function - | Exact p -> Exact (apply_subst subst p) + | Exact p -> Exact (Subst.apply_subst subst p) | Step (s,(r,id1,(pos,id2),pred)) -> - Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred)) + Step (Subst.concat s subst,(r,id1,(pos,id2), pred)) in - let new_p = fix_new_proof p1 in - let old_p = fix_proof p2 in - let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in - (* debug prerr_endline (string_of_equality eq); *) - newmeta+1, eq + let p = fix_proof p in + let bag = id_to_eq, newmeta in + let bag, e = mk_equality bag (w, p, (ty, left, right, o), metasenv) in + bag, e +;; 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 = + let rec aux ((table_l,table_r) as table) t1 t2 = match t1, t2 with + | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 = m2 -> table + | C.Meta (m1, tl1), C.Meta (m2, tl2) when m1 < m2 -> aux table t2 t1 | C.Meta (m1, tl1), C.Meta (m2, tl2) -> let m1_binding, table_l = try List.assoc m1 table_l, table_l @@ -823,26 +944,18 @@ let meta_convertibility_aux table t1 t2 = 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 - ) + else table_l,table_r | 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) -> + | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) -> + let table = aux table s1 s2 in + aux table t1 t2 + | C.LetIn (_, s1, ty1, t1), C.LetIn (_, s2, ty2, t2) -> let table = aux table s1 s2 in + let table = aux table ty1 ty2 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 @@ -910,73 +1023,99 @@ let meta_convertibility_eq eq1 eq2 = true else try - let table = meta_convertibility_aux ([], []) left left' in + 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 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); + ignore(meta_convertibility_aux ([],[]) t1 t2); true with NotMetaConvertible -> false ;; +let meta_convertibility_subst t1 t2 menv = + if t1 = t2 then + Some([]) + else + try + let (l,_) = meta_convertibility_aux ([],[]) t1 t2 in + let subst = + List.map + (fun (x,y) -> + try + let (_,c,t) = CicUtil.lookup_meta x menv in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable c in + (y,(c,Cic.Meta(x,irl),t)) + with CicUtil.Meta_not_found _ -> + try + let (_,c,t) = CicUtil.lookup_meta y menv in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable c in + (x,(c,Cic.Meta(y,irl),t)) + with CicUtil.Meta_not_found _ -> assert false) l in + Some subst + with NotMetaConvertible -> + None +;; + exception TermIsNotAnEquality;; 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 + | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] + when LibraryObjects.is_eq_URI uri -> true | _ -> false ;; -let equality_of_term proof term = - let eq_uri = LibraryObjects.eq_URI () in - let iseq uri = UriManager.eq uri eq_uri in +let equality_of_term bag proof term newmetas = match term with - | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = Utils.compute_equality_weight stat in - let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in - e + let bag, e = mk_equality bag (w, Exact proof, stat,newmetas) in + bag, e | _ -> raise TermIsNotAnEquality ;; let is_weak_identity eq = let _,_,(_,left, right,_),_,_ = open_equality eq in - left = right || meta_convertibility left right + left = right + (* doing metaconv here is meaningless *) ;; let is_identity (_, context, ugraph) eq = let _,_,(ty,left,right,_),menv,_ = open_equality eq in - left = right || - (* (meta_convertibility left right)) *) - fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + (* doing metaconv here is meaningless *) + left = right +(* fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + * *) ;; -let term_of_equality equality = +let term_of_equality eq_uri equality = let _, _, (ty, left, right, _), menv, _= open_equality 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]) + (Cic.Appl [Cic.MutInd (eq_uri, 0, []); ty; left; right]) in snd ( List.fold_right @@ -992,3 +1131,249 @@ let term_of_equality equality = menv (argsno, t)) ;; +let symmetric bag eq_ty l id uri m = + let eq = Cic.MutInd(uri,0,[]) in + let pred = + Cic.Lambda (Cic.Name "Sym",eq_ty, + Cic.Appl [CicSubstitution.lift 1 eq ; + CicSubstitution.lift 1 eq_ty; + Cic.Rel 1;CicSubstitution.lift 1 l]) + in + let prefl = + Exact (Cic.Appl + [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) + in + let bag, id1 = + let bag, eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in + let (_,_,_,_,id) = open_equality eq in + bag, id + in + bag, Step(Subst.empty_subst, + (Demodulation,id1,(Utils.Left,id),pred)) +;; + +module IntOT = struct + type t = int + let compare = Pervasives.compare +end + +module IntSet = Set.Make(IntOT);; + +let n_purged = ref 0;; + +let collect ((id_to_eq,maxmeta) as bag) alive1 alive2 alive3 = + let deps_of id = + let p,_,_ = proof_of_id bag id in + match p with + | Exact _ -> IntSet.empty + | Step (_,(_,id1,(_,id2),_)) -> + IntSet.add id1 (IntSet.add id2 IntSet.empty) + in + let rec close s = + let news = IntSet.fold (fun id s -> IntSet.union (deps_of id) s) s s in + if IntSet.equal news s then s else close news + in + let l_to_s s l = List.fold_left (fun s x -> IntSet.add x s) s l in + let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in + let closed_alive_set = close alive_set in + let to_purge = + M.fold + (fun k _ s -> + if not (IntSet.mem k closed_alive_set) then + k::s else s) id_to_eq [] + in + n_purged := !n_purged + List.length to_purge; + List.fold_right M.remove to_purge id_to_eq, maxmeta +;; + +let get_stats () = "" +(* + <:show> ^ + "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n" +*) +;; + +let rec pp_proofterm name t context = + let rec skip_lambda tys ctx = function + | Cic.Lambda (n,s,t) -> skip_lambda (s::tys) ((Some n)::ctx) t + | t -> ctx,tys,t + in + let rename s name = + match name with + | Cic.Name s1 -> Cic.Name (s ^ s1) + | _ -> assert false + in + let rec skip_letin ctx = function + | Cic.LetIn (n,b,_,t) -> + pp_proofterm (Some (rename "Lemma " n)) b ctx:: + skip_letin ((Some n)::ctx) t + | t -> + let ppterm t = CicPp.pp t ctx in + let rec pp inner = function + | Cic.Appl [Cic.Const (uri,[]);_;l;m;r;p1;p2] + when Pcre.pmatch ~pat:"trans_eq" (UriManager.string_of_uri uri)-> + if not inner then + (" " ^ ppterm l) :: pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 @ + [ " = " ^ ppterm r ] + else + pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 + | Cic.Appl [Cic.Const (uri,[]);_;l;m;p] + when Pcre.pmatch ~pat:"sym_eq" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_OF_eq" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] + when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)-> + [ "witness " ^ ppterm t ] @ pp true p + | Cic.Appl (t::_) ->[ " [by " ^ ppterm t ^ "]"] + | t ->[ " [by " ^ ppterm t ^ "]"] + in + let rec compat = function + | a::b::tl -> (b ^ a) :: compat tl + | h::[] -> [h] + | [] -> [] + in + let compat l = List.hd l :: compat (List.tl l) in + compat (pp false t) @ ["";""] + in + let names, tys, body = skip_lambda [] context t in + let ppname name = (match name with Some (Cic.Name s) -> s | _ -> "") in + ppname name ^ ":\n" ^ + (if context = [] then + let rec pp_l ctx = function + | (t,name)::tl -> + " " ^ ppname name ^ ": " ^ CicPp.pp t ctx ^ "\n" ^ + pp_l (name::ctx) tl + | [] -> "\n\n" + in + pp_l [] (List.rev (List.combine tys names)) + else "") + ^ + String.concat "\n" (skip_letin names body) +;; + +let pp_proofterm t = + "\n\n" ^ + pp_proofterm (Some (Cic.Name "Hypothesis")) t [] +;; + +let initial_nameset_list = [ + "x"; "y"; "z"; "t"; "u"; "v"; "a"; "b"; "c"; "d"; + "e"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; +] + +module S = Set.Make(String) + +let initial_nameset = List.fold_right S.add initial_nameset_list S.empty, [];; + +let freshname (nameset, subst) term = + let m = CicUtil.metas_of_term term in + let nameset, subst = + List.fold_left + (fun (set,rc) (m,_) -> + if List.mem_assoc m rc then set,rc else + let name = S.choose set in + let set = S.remove name set in + set, + (m,Cic.Const(UriManager.uri_of_string + ("cic:/"^name^".con"),[]))::rc) + (nameset,subst) m + in + let term = + ProofEngineReduction.replace + ~equality:(fun i t -> match t with Cic.Meta (j,_) -> i=j| _ -> false) + ~what:(List.map fst subst) + ~with_what:(List.map snd subst) ~where:term + in + (nameset, subst), term +;; + +let remove_names_in_context (set,subst) names = + List.fold_left + (fun s n -> + match n with Some (Cic.Name n) -> S.remove n s | _ -> s) + set names, subst +;; + +let string_of_id2 (id_to_eq,_) names nameset id = + if id = 0 then "" else + try + let (_,_,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in + let nameset, l = freshname nameset l in + let nameset, r = freshname nameset r in + Printf.sprintf "%s = %s" (CicPp.pp l names) (CicPp.pp r names) + with + Not_found -> assert false +;; + +let draw_proof bag names goal_proof proof id = + let b = Buffer.create 100 in + let fmt = Format.formatter_of_buffer b in + let sint = string_of_int in + let fst3 (x,_,_) = x in + let visited = ref [] in + let nameset = remove_names_in_context initial_nameset names in + let rec fact id = function + | Exact t -> + if not (List.mem id !visited) then + begin + visited := id :: !visited; + let nameset, t = freshname nameset t in + let t = CicPp.pp t names in + GraphvizPp.Dot.node (sint id) + ~attrs:["label",t^":"^string_of_id2 bag names nameset id; + "shape","rectangle"] fmt; + end + | Step (_,(_,id1,(_,id2),_)) -> + GraphvizPp.Dot.edge (sint id) (sint id1) fmt; + GraphvizPp.Dot.edge (sint id) (sint id2) fmt; + let p1,_,_ = proof_of_id bag id1 in + let p2,_,_ = proof_of_id bag id2 in + fact id1 p1; + fact id2 p2; + if not (List.mem id !visited); then + begin + visited := id :: !visited; + GraphvizPp.Dot.node (sint id) + ~attrs:["label",sint id^":"^string_of_id2 bag names nameset id; + "shape","ellipse"] fmt + end + in + let sleft acc (_,_,id,_,_) = + if acc != 0 then GraphvizPp.Dot.edge (sint acc) (sint id) fmt; + fact id (fst3 (proof_of_id bag id)); + id + in + GraphvizPp.Dot.header ~node_attrs:["fontsize","10"; ] fmt; + ignore(List.fold_left sleft id goal_proof); + GraphvizPp.Dot.trailer fmt; + let oc = open_out "/tmp/matita_paramod.dot" in + Buffer.output_buffer oc b; + close_out oc; + Utils.debug_print (lazy "dot!"); + ignore(Unix.system + "dot -Tps -o /tmp/matita_paramod.eps /tmp/matita_paramod.dot" +(* "cat /tmp/matita_paramod.dot| tred | dot -Tps -o /tmp/matita_paramod.eps" *) + ); + ignore(Unix.system "gv /tmp/matita_paramod.eps"); +;; + +let saturate_term (id_to_eq, maxmeta) metasenv subst context term = + let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in + let head, metasenv, args, newmeta = + TermUtil.saturate_term maxmeta metasenv context term 0 + in + (id_to_eq, newmeta), head, metasenv, args +;; + +let push_maxmeta (id_to_eq, maxmeta) m = id_to_eq, max maxmeta m ;; +let filter_metasenv_gt_maxmeta (_,maxmeta) = + List.filter (fun (j,_,_) -> j >= maxmeta) +;; +let maxmeta = snd;;