From d924c0133e2ecd9b68f23eb00cb4230320f155df Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Feb 2007 14:48:05 +0000 Subject: [PATCH] reverted a commented substitution in build_newgoal, added an euristic to order the lambdas of a proof abstracted in a letin such that dependency betwwen the types of the lambdas is inferrable by the refiner --- .../tactics/paramodulation/equality.ml | 84 +++++++++++-------- .../tactics/paramodulation/indexing.ml | 8 +- .../tactics/paramodulation/saturation.ml | 38 ++++++--- 3 files changed, 76 insertions(+), 54 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 7f093e3f8..1bc87f8c5 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -96,8 +96,8 @@ let string_of_equality ?env eq = 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)) *) - "..." + (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), m , id = open_equality eq in @@ -105,8 +105,8 @@ let string_of_equality ?env eq = 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)) *) - "..." + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* "..." *) ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = @@ -327,11 +327,18 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); Cic.LetIn (name,remove_refl bo,remove_refl rest) | _ -> t in - let rec canonical context 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,rest) -> + let bo = canonical_trough_lambda context bo in let context' = (Some (name,Cic.Def (bo,None)))::context in - Cic.LetIn(name,canonical context bo,canonical context' rest) + Cic.LetIn(name,bo,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 @@ -344,12 +351,15 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); mk_trans uri_trans ty r m l (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])) -> + | 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 - Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p])) + let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in + prerr_endline ("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 context) args)) @@ -539,8 +549,8 @@ let build_proof_step eq lift subst p1 p2 pos l r pred = p ;; -let parametrize_proof menv p l r ty = - let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in +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? *) @@ -549,6 +559,21 @@ let parametrize_proof menv p l r ty = HExtlib.list_uniq (List.sort Pervasives.compare parameters) in *) + (* 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) @@ -560,22 +585,7 @@ let parametrize_proof menv p l r ty = match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p in - let ty_of_m _ = Cic.Implicit (Some `Type) -(* - let ty_of_m = function - | Cic.Meta (i,_) -> - (try - let _,_,ty = CicUtil.lookup_meta i menv in ty - with CicUtil.Meta_not_found _ -> - prerr_endline "eccoci";assert false) - | _ -> assert false -*) - (* - let ty_of_m _ = ty (*function - | Cic.Meta (i,_) -> List.assoc i menv - | _ -> assert false *) - *) - in + let ty_of_m _ = Cic.Implicit (Some `Type) in let args, proof,_ = List.fold_left (fun (instance,p,n) m -> @@ -613,19 +623,19 @@ let wfo bag goalproof proof id = let string_of_id (id_to_eq,_) names id = if id = 0 then "" else try - let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in match p with | Exact t -> Printf.sprintf "%d = %s: %s = %s [%s]" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) - "..." -(* (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 +(* "..." *) + (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 r names) -(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) - "..." + 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 @@ -776,7 +786,6 @@ let build_goal_proof 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 _,mty,_,_ = open_eq ty in let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in let lets,_,h = List.fold_left @@ -784,7 +793,7 @@ let build_goal_proof bag eq l initial ty se context menv = 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 menv cic l r (CicSubstitution.lift n mty) + parametrize_proof cic l r in let h = (id, instance)::lift_list h in acc@[id,real_cic],n+1,h) @@ -894,7 +903,8 @@ let fix_metas bag newmeta eq = (* List.map (fun i ,_,_ -> i) menv *) HExtlib.list_uniq (List.sort Pervasives.compare - (Utils.metas_of_term left @ Utils.metas_of_term right)) + (Utils.metas_of_term left @ Utils.metas_of_term right @ + Utils.metas_of_term ty)) in let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index b535119ed..e453d95c1 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -621,6 +621,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) with CicUtil.Meta_not_found _ -> ty in + let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = let bo = @@ -858,6 +859,7 @@ let superposition_right bag Equality.open_equality equality in let what, other = if pos = Utils.Left then what, other else other, what in + let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in let newgoal, newproof = (* qua *) let bo' = @@ -1003,10 +1005,8 @@ let build_newgoal bag context goal posu rule expansion = Utils.guarded_simpl context (apply_subst subst (CicSubstitution.subst other t)) in - let bo' = (*apply_subst subst*) t in - (* patch?? - let bo' = t in - let ty = apply_subst subst ty in *) + let bo' = apply_subst subst t in + let ty = apply_subst subst ty in let name = Cic.Name "x" in let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 514cd049e..30561bf07 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1351,20 +1351,28 @@ let build_proof let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) *) + let pp_error goal_proof names error exn = + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + prerr_endline (CicPp.pp goal_proof names); + prerr_endline "THE PROOF DOES NOT TYPECHECK!"; + prerr_endline error; + prerr_endline "THE PROOF DOES NOT TYPECHECK! "; + raise exn + in let goal_proof,goal_ty,real_menv,_ = (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *) try + prerr_endline (CicPp.ppterm goal_proof); CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph with - | CicUtil.Meta_not_found _ - | CicRefine.RefineFailure _ - | CicRefine.Uncertain _ - | CicRefine.AssertFailure _ + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s as exn -> + pp_error goal_proof names (Lazy.force s) exn + | CicUtil.Meta_not_found i as exn -> + pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn | Invalid_argument "list_fold_left2" as exn -> - prerr_endline "THE PROOF DOES NOT TYPECHECK!"; - prerr_endline (CicPp.pp goal_proof names); - prerr_endline "THE PROOF DOES NOT TYPECHECK!"; - raise exn + pp_error goal_proof names "Invalid_argument: list_fold_left2" exn in let subst_side_effects,real_menv,_ = try @@ -1531,15 +1539,17 @@ let build_proof let pump_actives context bag maxm active passive saturation_steps max_time = reset_refs(); maxmeta := maxm; +(* let max_l l = List.fold_left (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) 0 l in - let active_l = fst active in - let passive_l = fst passive in - let ma = max_l active_l in - let mp = max_l passive_l in +*) +(* let active_l = fst active in *) +(* let passive_l = fst passive in *) +(* let ma = max_l active_l in *) +(* let mp = max_l passive_l in *) match LibraryObjects.eq_URI () with | None -> active, passive, !maxmeta | Some eq_uri -> @@ -1591,16 +1601,18 @@ let given_clause = reset_refs(); maxmeta := maxm; + let active_l = fst active in +(* let max_l l = List.fold_left (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in List.fold_left (fun acc (i,_,_) -> max i acc) acc menv) 0 l in - let active_l = fst active in let passive_l = fst passive in let ma = max_l active_l in let mp = max_l passive_l in +*) let proof, goalno = status in let uri, metasenv, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in -- 2.39.2