From: Enrico Tassi Date: Sun, 28 May 2006 16:09:00 +0000 (+0000) Subject: added the rule field to goal_proof. X-Git-Tag: make_still_working~7314 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9809bb28066665067dc4669a631fdd4fe18b6a22;p=helm.git added the rule field to goal_proof. fixed the SupL proof generation (but I think the fix should not be here) --- diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index ec311615e..b10dc818e 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -41,7 +41,7 @@ and proof = | Exact of Cic.term | 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 +and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; (* globals *) @@ -75,6 +75,12 @@ let mk_tmp_equality (weight,(ty,l,r,o),m) = let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) +let string_of_rule = function + | SuperpositionRight -> "SupR" + | SuperpositionLeft -> "SupL" + | Demodulation -> "Demod" +;; + let string_of_equality ?env eq = match env with | None -> @@ -107,11 +113,6 @@ let proof_of_id id = let string_of_proof ?(names=[]) p gp = - let str_of_rule = function - | SuperpositionRight -> "SupR" - | SuperpositionLeft -> "SupL" - | Demodulation -> "Demod" - in let str_of_pos = function | Utils.Left -> "left" | Utils.Right -> "right" @@ -124,7 +125,7 @@ let string_of_proof ?(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) (Subst.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)) @@ -132,9 +133,9 @@ let string_of_proof ?(names=[]) p gp = 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" + "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 i))) gp) @@ -400,7 +401,7 @@ let contextualize_rewrites t ty = contextualize eq ty l r t ;; -let build_proof_step lift subst p1 p2 pos l r pred = +let build_proof_step ?(sym=false) 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 @@ -417,11 +418,23 @@ let build_proof_step lift subst p1 p2 pos l r pred = let what, other = if pos = Utils.Left then l,r else r,l in + let p = 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 + in + if sym then + let uri,pl,pr = + let eq,_,pl,pr = open_eq body in + LibraryObjects.sym_eq_URI ~eq, pl, pr + in + let l = CicSubstitution.subst other pl in + let r = CicSubstitution.subst other pr in + mk_sym uri ty l r p + else + p ;; let parametrize_proof p l r ty = @@ -439,7 +452,9 @@ in (* ?if they are under a lambda? *) 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) ~what ~with_what ~where:p + ~equality:(fun t1 t2 -> + match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) + ~what ~with_what ~where:p in let ty_of_m _ = ty (*function | Cic.Meta (i,_) -> List.assoc i menv @@ -461,7 +476,7 @@ in (* ?if they are under a lambda? *) proof, instance ;; -let wfo goalproof proof = +let wfo goalproof proof id = let rec aux acc id = let p,_,_ = proof_of_id id in match p with @@ -473,13 +488,14 @@ let wfo goalproof proof = in let acc = match proof with - | Exact _ -> [] - | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2 + | Exact _ -> [id] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2 in - List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof + List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof ;; let string_of_id names id = + if id = 0 then "" else try let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in match p with @@ -489,17 +505,31 @@ let string_of_id names id = (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) | Step (_,(step,id1, (_,id2), _) ) -> Printf.sprintf "%6d: %s %6d %6d %s = %s [%s]" id - (if step = SuperpositionRight then "SupR" else "Demo") + (string_of_rule step) id1 id2 (CicPp.pp l 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 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 pp_proof names goalproof proof subst id initial_goal = + prerr_endline ("AAAAA" ^ string_of_int id); + prerr_endline (String.concat "+" (List.map string_of_int (wfo goalproof proof + id))); + String.concat "\n" (List.map (string_of_id names) (wfo 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 ;; (* returns the list of ids that should be factorized *) @@ -529,7 +559,7 @@ let get_duplicate_step_in_wfo l p = let i = aux 0 p in let _ = List.fold_left - (fun acc (_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p)) + (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p)) i ol in (* now h is complete *) @@ -549,9 +579,6 @@ let build_proof_term h lift proof = let rec aux = function | Exact term -> CicSubstitution.lift lift term | Step (subst,(_, id1, (pos,id2), pred)) -> - if Subst.is_in_subst 302 subst then - prerr_endline ("TROVATA in " ^ string_of_int id1 ^ " " ^ string_of_int id2); - let p1,_,_ = proof_of_id aux id1 in let p2,l,r = proof_of_id aux id2 in let p = build_proof_step lift subst p1 p2 pos l r pred in @@ -586,15 +613,24 @@ let build_goal_proof l initial ty se = let proof,se = let rec aux se current_proof = function | [] -> current_proof,se - | (pos,id,subst,pred)::tl -> - if Subst.is_in_subst 302 subst then - prerr_endline ("TROVATA in " ^ string_of_int id ); - + | (rule,pos,id,subst,pred)::tl -> let p,l,r = proof_of_id id in let p = build_proof_term h letsno p in let pos = if pos = Utils.Left then Utils.Right else Utils.Left in + let sym,pred = + match rule with + | SuperpositionLeft when pos = Utils.Left -> + let pred = + match pred with + | Cic.Lambda (name,ty,Cic.Appl[eq;ty1;l;r]) -> + Cic.Lambda (name,ty,Cic.Appl[eq;ty1;r;l]) + | _ -> assert false + in + true, pred + | _ -> false,pred + in let proof = - build_proof_step letsno subst current_proof p pos l r pred + build_proof_step ~sym 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, diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 6b5e34af9..ee90d7b6e 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -31,9 +31,11 @@ and proof = Exact of Cic.term | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term) -and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list +and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list -val pp_proof: (Cic.name option) list -> goal_proof -> proof -> string +val pp_proof: + (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int -> + Cic.term -> string val reset : unit -> unit