X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=b6c3dc66a6625ec2e2ba92043e5108d6375f501d;hb=be69d5604639ffb64ca56fcbf0a9d4afa97c6c41;hp=953635dbd8e65df346c11dbc45c0f683f4c3d42f;hpb=d5950e1810f3a6d89328f18c2c5796e54a907473;p=helm.git diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 953635dbd..b6c3dc66a 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -25,194 +25,6 @@ (* $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 = [];; - -(********* EQUALITY **********************************************************) - type rule = SuperpositionRight | SuperpositionLeft | Demodulation type uncomparable = int -> int type equality = @@ -225,21 +37,11 @@ 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 = (Utils.pos * int * Subst.substitution * Cic.term) list ;; (* globals *) @@ -257,13 +59,19 @@ let reset () = let uncomparable = fun _ -> 0 -let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = +let mk_equality (weight,p,(ty,l,r,o),m) = let id = freshid () in - let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in + let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in Hashtbl.add id_to_eq id eq; 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) @@ -288,34 +96,15 @@ 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 = try - let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in - p,m,l,r + let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + p,l,r with Not_found -> assert false -let string_of_proof_new ?(names=[]) p gp = +let string_of_proof ?(names=[]) p gp = let str_of_rule = function | SuperpositionRight -> "SupR" | SuperpositionLeft -> "SupL" @@ -325,7 +114,7 @@ let string_of_proof_new ?(names=[]) p gp = | Utils.Left -> "left" | Utils.Right -> "right" in - let fst4 (x,_,_,_) = x in + let fst3 (x,_,_) = x in let rec aux margin name = let prefix = String.make margin ' ' ^ name ^ ": " in function | Exact t -> @@ -333,10 +122,10 @@ 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 (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ - aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^ - aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2)) + aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ + aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) in aux 0 "" p ^ String.concat "\n" @@ -344,16 +133,27 @@ let string_of_proof_new ?(names=[]) p gp = (fun (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) (fst4 (proof_of_id i))) + (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ + aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) gp) ;; -let ppsubst = ppsubst ~names:[] +let rec depend eq id = + let (_,p,(_,_,_,_),_,ideq) = open_equality eq in + if id = ideq then true else + match p with + Exact _ -> false + | Step (_,(_,id1,(_,id2),_)) -> + let eq1 = Hashtbl.find id_to_eq id1 in + let eq2 = Hashtbl.find id_to_eq id2 in + depend eq1 id || depend eq2 id +;; + +let ppsubst = Subst.ppsubst ~names:[];; (* 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 +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); @@ -368,121 +168,315 @@ let build_ens_for_sym_eq sym_eq_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_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), (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 +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) +;; + +let mk_trans uri ty t1 t2 t3 p12 p23 = + let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in + Cic.Appl (Cic.Const (uri, ens) :: args) +;; + +let mk_eq_ind uri ty what pred p1 other p2 = + Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2] +;; + +let p_of_sym ens tl = + let args = List.map snd ens @ tl in + match args with + | [_;_;_;p] -> p + | _ -> assert false +;; + +let open_trans ens tl = + let args = List.map snd ens @ tl in + match args with + | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2 + | _ -> 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 (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) + when LibraryObjects.is_eq_URI uri -> ty,uri,l,r + | _ -> prerr_endline (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 = + let rec remove_refl t = + match t with + | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,p1,p2 = open_trans ens tl in + (match p1,p2 with + | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 -> + remove_refl p2 + | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] -> + remove_refl p1 + | _ -> Cic.Appl (List.map remove_refl args)) + | Cic.Appl l -> Cic.Appl (List.map remove_refl l) + | _ -> t + in + let rec canonical t = + match t with + | 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) + | 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 + 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] + | 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) + | _ -> t + in + remove_refl (canonical t) +;; + +let ty_of_lambda = function + | Cic.Lambda (_,ty,_) -> ty + | _ -> assert false +;; + +let compose_contexts ctx1 ctx2 = + ProofEngineReduction.replace_lifting + ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1 +;; + +let put_in_ctx ctx t = + ProofEngineReduction.replace_lifting + ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx +;; + +let mk_eq uri ty l r = + Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] +;; + +let mk_refl uri ty t = + Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t] +;; + +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 contextualize uri ty left right t = + (* aux [uri] [ty] [left] [right] [ctx] [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 open (Rel 1). (Rel 1) is the empty context + *) + let rec aux uri ty left right ctx_d = function + | 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 = + 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 (Cic.Implicit None) m in + let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in + m, ctx_c + 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 ty1 c_what m ctx_d p1 + else + mk_sym uri_sym ty d_m dc_what + (aux uri ty1 m c_what ctx_d p1) + in + let p2 = (* p2: dc_other = dc_what *) + if avoid_eq_ind then + mk_sym uri_sym ty dc_what dc_other + (aux uri ty1 what other ctx_dc p2) + else + aux uri ty1 other what ctx_dc 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 ty dc_what d_m p1), + (mk_sym uri_sym ty dc_other dc_what p2) + in + mk_trans uri_trans ty a b c paeqb pbeqc + | t -> + let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in + let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in + let pred = + (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *) + let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *) + let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in + let l = ctx_d in + let lty = CicSubstitution.lift 1 ty in + Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) in - ProofEngineReduction.replace - ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term + 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 ty d_left in + mk_sym uri_sym ty d_right d_left + (mk_eq_ind uri_ind ty left pred refl_eq right t) + in + let empty_context = Cic.Rel 1 in + aux uri ty left right empty_context t +;; - 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 +let contextualize_rewrites t ty = + let eq,ty,l,r = open_eq ty in + contextualize eq ty l r t +;; + +let build_proof_step subst p1 p2 pos l r pred = + let p1 = Subst.apply_subst subst p1 in + let p2 = Subst.apply_subst subst p2 in + let l = Subst.apply_subst subst l in + let r = Subst.apply_subst subst r in + let pred = Subst.apply_subst subst pred in + let ty,body = + match pred with + | Cic.Lambda (_,ty,body) -> ty,body + | _ -> assert false + in + let what, other = + if pos = Utils.Left then l,r else r,l in - do_build_proof proof + match pos with + | 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 ;; -let build_proof_term_new proof = - let rec aux extra = function +let build_proof_term proof = + let rec aux = function | Exact term -> term | Step (subst,(_, id1, (pos,id2), pred)) -> - let p,m1,_,_ = proof_of_id id1 in - let p1 = aux [] p in - let p,m3,l,r = proof_of_id id2 in - let p2 = aux [] p in - 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 = (* Cic.Implicit None *) - match pred with - | Cic.Lambda (_,ty,_) -> ty - | _ -> assert false - in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) - if pos = Utils.Left then l,r else r,l - in - let eq_URI = - match pos with - | Utils.Left -> Utils.eq_ind_URI () - | Utils.Right -> Utils.eq_ind_r_URI () - in - (Cic.Appl [ - Cic.Const (eq_URI, []); - ty; what; pred; p1; other; p2]) + 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 in - aux [] proof + aux proof +;; -let build_goal_proof l refl= - let proof, subst = +let wfo goalproof proof = + let rec aux acc id = + let p,_,_ = proof_of_id id in + match p with + | 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 + let acc = + match proof with + | Exact _ -> [] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2 + in + List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof +;; + +let string_of_id names id = + try + let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + match p with + | Exact t -> + Printf.sprintf "%d = %s: %s = %s" id + (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) + | Step (_,(step,id1, (_,id2), _) ) -> + Printf.sprintf "%6d: %s %6d %6d %s = %s" id + (if step = SuperpositionRight then "SupR" else "Demo") + id1 id2 (CicPp.pp l names) (CicPp.pp r names) + with + Not_found -> assert false + +let pp_proof names goalproof proof = + String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ + "\ngoal is demodulated with " ^ + (String.concat " " + ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) +;; + +let build_goal_proof l initial ty = + let proof = List.fold_left - (fun (current_proof,current_subst) (pos,id,subst,pred) -> - let p,m,l,r = proof_of_id id in - let p = build_proof_term_new p in - let p = apply_subst subst p in - let l = apply_subst subst l in - let r = apply_subst subst r in - let pred = apply_subst subst pred in - let ty = (* Cic.Implicit None *) - match pred with - | Cic.Lambda (_,ty,_) -> ty - | _ -> assert false - in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) - if pos = Utils.Right then l,r else r,l - in - let eq_URI = - match pos with - | Utils.Left -> Utils.eq_ind_r_URI () - | Utils.Right -> Utils.eq_ind_URI () - in - ((Cic.Appl [Cic.Const (eq_URI, []); - ty; what; pred; current_proof; other; p]), subst @ current_subst)) - (refl,[]) l + (fun current_proof (pos,id,subst,pred) -> + let p,l,r = proof_of_id id in + let p = build_proof_term 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 in - proof + proof + (*canonical (contextualize_rewrites proof ty)*) ;; let refl_proof ty term = @@ -492,7 +486,9 @@ let refl_proof ty term = ty; term] ;; -let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;; +let metas_of_proof p = + Utils.metas_of_term (build_proof_term p) +;; let relocate newmeta menv = let subst, metasenv, newmeta = @@ -501,49 +497,33 @@ let relocate newmeta menv = let irl = [] (* CicMkImplicit.identity_relocation_list_for_metavariable context *) in - let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in + let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in let newmeta = maxmeta, context, ty in newsubst, newmeta::menv, maxmeta+1) - menv ([], [], newmeta+1) + menv (Subst.empty_subst, [], newmeta+1) in - let metasenv = apply_subst_metasenv subst metasenv in - let subst = flatten_subst subst in + let metasenv = Subst.apply_subst_metasenv subst metasenv in + let subst = 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 + let w, p, (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 + 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_substs 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 + let p = fix_proof p in + let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in (* debug prerr_endline (string_of_equality eq); *) newmeta+1, eq @@ -691,7 +671,7 @@ let equality_of_term proof term = 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 + let e = mk_equality (w, Exact proof, stat,[]) in e | _ -> raise TermIsNotAnEquality