From 679f6296c9a979213425104fa606809d9f1e3bad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 21 Jun 2006 15:33:02 +0000 Subject: [PATCH] added the geniric auto params syntax and the auto superposition tactic --- components/grafite/grafiteAst.ml | 3 +- components/grafite/grafiteAstPp.ml | 5 +- components/grafite_engine/grafiteEngine.ml | 5 +- .../grafite_parser/grafiteDisambiguate.ml | 4 +- components/grafite_parser/grafiteParser.ml | 10 +- components/tactics/autoTactic.ml | 309 ++++++++++-------- components/tactics/autoTactic.mli | 4 +- .../tactics/paramodulation/saturation.ml | 77 ++++- .../tactics/paramodulation/saturation.mli | 9 +- components/tactics/tactics.mli | 7 +- matita/matita.ml | 11 + matita/matitaGui.ml | 2 +- 12 files changed, 278 insertions(+), 168 deletions(-) diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index ffd35c703..a9ac1c6eb 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -49,8 +49,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Apply of loc * 'term | ApplyS of loc * 'term | Assumption of loc - | Auto of loc * int option * int option * string option * string option - (* depth, width, paramodulation, full *) (* ALB *) + | Auto of loc * (string * string) list | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident | ClearBody of loc * 'ident diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 20d57ef9e..24d37c4f3 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -73,8 +73,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term | ApplyS (_, term) -> "applyS " ^ term_pp term - | Auto (_,_,_,Some kind,_) -> "auto " ^ kind - | Auto _ -> "auto" + | Auto (_,params) -> "auto " ^ + String.concat " " + (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | Assumption _ -> "assumption" | Change (_, where, with_what) -> sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index e4f70117a..ae497fc12 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -63,9 +63,8 @@ let tactic_of_ast ast = | GrafiteAst.ApplyS (_, term) -> Tactics.applyS ~term ~dbd:(LibraryDb.instance ()) | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> - AutoTactic.auto_tac ?depth ?width ?paramodulation ?full - ~dbd:(LibraryDb.instance ()) () + | GrafiteAst.Auto (_,params) -> + AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what | GrafiteAst.Clear (_,id) -> Tactics.clear id diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 0e96aaf2d..16421efaf 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -129,8 +129,8 @@ let disambiguate_tactic metasenv,GrafiteAst.ApplyS (loc, cic) | GrafiteAst.Assumption loc -> metasenv,GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation,full) -> - metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full) + | GrafiteAst.Auto (loc,params) -> + metasenv,GrafiteAst.Auto (loc,params) | GrafiteAst.Change (loc, pattern, with_what) -> let with_what = disambiguate_lazy_term with_what in let pattern = disambiguate_pattern pattern in diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index ad081d664..c0ce1c27d 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -132,12 +132,10 @@ EXTEND GrafiteAst.ApplyS (loc, t) | IDENT "assumption" -> GrafiteAst.Assumption loc - | IDENT "auto"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; - paramodulation = OPT [ IDENT "paramodulation" ]; - full = OPT [ IDENT "full" ] -> (* ALB *) - GrafiteAst.Auto (loc,depth,width,paramodulation,full) + | IDENT "auto"; params = + LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + string_of_int v | v = IDENT -> v ] -> i,v ] -> + GrafiteAst.Auto (loc,params) | IDENT "clear"; id = IDENT -> GrafiteAst.Clear (loc,id) | IDENT "clearbody"; id = IDENT -> diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 9f54c6cec..1ba1dd912 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -46,7 +46,7 @@ type exitus = No of int | Yes of Cic.term * int | NotYetInspected - + let inspected_goals = Hashtbl.create 503;; let search_theorems_in_context status = @@ -93,17 +93,17 @@ let compare_goals proof goal1 goal2 = let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 - CicUniv.empty_ugraph in + CicUniv.empty_ugraph in let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2 - CicUniv.empty_ugraph in + CicUniv.empty_ugraph in let prop1 = let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 - CicUniv.empty_ugraph in + CicUniv.empty_ugraph in if b then 0 else 1 in let prop2 = let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 - CicUniv.empty_ugraph in + CicUniv.empty_ugraph in if b then 0 else 1 in prop1 - prop2 @@ -139,90 +139,90 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals let is_meta_closed = CicUtil.is_meta_closed ty in begin match exitus with - Yes (bo,_) -> + Yes (bo,_) -> (* debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); - debug_print (lazy (CicPp.ppterm ty)); + debug_print (lazy (CicPp.ppterm ty)); *) let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) - CicMetaSubst.apply_subst - [(goal,(ey, bo, Cic.Implicit None))] in - let (proof,_) = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst_in metasenv in - [(subst_in,(proof,[],sign))] + CicMetaSubst.apply_subst + [(goal,(ey, bo, Cic.Implicit None))] in + let (proof,_) = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal subst_in metasenv in + [(subst_in,(proof,[],sign))] | No d when (d >= depth) -> - (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) - [] (* the empty list means no choices, i.e. failure *) - | No _ - | NotYetInspected -> - debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); - debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); - debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); - let sign, new_sign = - if is_meta_closed then - None, Some (MetadataConstraints.signature_of ty) - else sign,sign in (* maybe the union ? *) - let local_choices = - new_search_theorems - search_theorems_in_context dbd - proof goal (depth-1) new_sign in - let global_choices = - new_search_theorems - (fun status -> - List.map snd - (new_experimental_hint - ~dbd ~facts:facts ?signature:sign ~universe status)) - dbd proof goal (depth-1) new_sign in - let all_choices = - local_choices@global_choices in - let sorted_choices = - List.stable_sort - (fun (_, (_, goals1, _)) (_, (_, goals2, _)) -> - Pervasives.compare - (List.length goals1) (List.length goals2)) - all_choices in - (match (auto_new dbd width already_seen_goals universe sorted_choices) - with - [] -> - (* no proof has been found; we update the - hastable *) - (* if is_meta_closed then *) - Hashtbl.add inspected_goals ty (No depth); - [] - | (subst,(proof,[],sign))::tl1 -> - (* a proof for goal has been found: - in order to get the proof we apply subst to - Meta[goal] *) - if is_meta_closed then - begin - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable ey in - let meta_proof = - subst (Cic.Meta(goal,irl)) in - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); + (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) + [] (* the empty list means no choices, i.e. failure *) + | No _ + | NotYetInspected -> + debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty)); + debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p)); + debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey)); + let sign, new_sign = + if is_meta_closed then + None, Some (MetadataConstraints.signature_of ty) + else sign,sign in (* maybe the union ? *) + let local_choices = + new_search_theorems + search_theorems_in_context dbd + proof goal (depth-1) new_sign in + let global_choices = + new_search_theorems + (fun status -> + List.map snd + (new_experimental_hint + ~dbd ~facts:facts ?signature:sign ~universe status)) + dbd proof goal (depth-1) new_sign in + let all_choices = + local_choices@global_choices in + let sorted_choices = + List.stable_sort + (fun (_, (_, goals1, _)) (_, (_, goals2, _)) -> + Pervasives.compare + (List.length goals1) (List.length goals2)) + all_choices in + (match (auto_new dbd width already_seen_goals universe sorted_choices) + with + [] -> + (* no proof has been found; we update the + hastable *) + (* if is_meta_closed then *) + Hashtbl.add inspected_goals ty (No depth); + [] + | (subst,(proof,[],sign))::tl1 -> + (* a proof for goal has been found: + in order to get the proof we apply subst to + Meta[goal] *) + if is_meta_closed then + begin + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable ey in + let meta_proof = + subst (Cic.Meta(goal,irl)) in + Hashtbl.add inspected_goals + ty (Yes (meta_proof,depth)); (* - begin - let cty,_ = - CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph - in - if not (cty = ty) then - begin - debug_print (lazy ("ty = "^CicPp.ppterm ty)); - debug_print (lazy ("cty = "^CicPp.ppterm cty)); - assert false - end - Hashtbl.add inspected_goals - ty (Yes (meta_proof,depth)); - end; + begin + let cty,_ = + CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph + in + if not (cty = ty) then + begin + debug_print (lazy ("ty = "^CicPp.ppterm ty)); + debug_print (lazy ("cty = "^CicPp.ppterm cty)); + assert false + end + Hashtbl.add inspected_goals + ty (Yes (meta_proof,depth)); + end; *) - end; - (subst,(proof,[],sign))::tl1 - | _ -> assert false) + end; + (subst,(proof,[],sign))::tl1 + | _ -> assert false) end and auto_new dbd width already_seen_goals universe = function @@ -232,7 +232,7 @@ and auto_new dbd width already_seen_goals universe = function let goals'= List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals in - auto_new_aux dbd + auto_new_aux dbd width already_seen_goals universe ((subst,(proof, goals', sign))::tl) and auto_new_aux dbd width already_seen_goals universe = function @@ -247,23 +247,23 @@ and auto_new_aux dbd width already_seen_goals universe = function let _,metasenv,p,_ = proof in let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in match (auto_single dbd proof goal ey ty depth - (width - (List.length gtl)) sign already_seen_goals) universe + (width - (List.length gtl)) sign already_seen_goals) universe with - [] -> auto_new dbd width already_seen_goals universe tl - | (local_subst,(proof,[],sign))::tl1 -> - let new_subst f t = f (subst t) in - let is_meta_closed = CicUtil.is_meta_closed ty in - let all_choices = - if is_meta_closed then - (new_subst local_subst,(proof,gtl,sign))::tl - else - let tl2 = - (List.map - (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1) - in - (new_subst local_subst,(proof,gtl,sign))::tl2@tl in - auto_new dbd width already_seen_goals universe all_choices - | _ -> assert false + [] -> auto_new dbd width already_seen_goals universe tl + | (local_subst,(proof,[],sign))::tl1 -> + let new_subst f t = f (subst t) in + let is_meta_closed = CicUtil.is_meta_closed ty in + let all_choices = + if is_meta_closed then + (new_subst local_subst,(proof,gtl,sign))::tl + else + let tl2 = + (List.map + (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1) + in + (new_subst local_subst,(proof,gtl,sign))::tl2@tl in + auto_new dbd width already_seen_goals universe all_choices + | _ -> assert false ;; let default_depth = 5 @@ -281,14 +281,14 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with [] -> debug_print (lazy "Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") + raise (ProofEngineTypes.Fail "No Applicable theorem") | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in - debug_print (lazy (CicPp.ppterm p)); + debug_print (lazy "AUTO_TAC HA FINITO"); + let _,_,p,_ = proof in + debug_print (lazy (CicPp.ppterm p)); Printf.printf "tempo: %.9f\n" (t2 -. t1); - (proof,[]) + (proof,[]) | _ -> assert false in ProofEngineTypes.mk_tactic (auto_tac dbd) @@ -304,8 +304,35 @@ let term_is_equality = ref (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; *) -let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation - ?full ~(dbd:HMysql.dbd) () = +let bool name params = + try let _ = List.assoc name params in true with + | Not_found -> false +;; + +let string name params = + try List.assoc name params with + | Not_found -> "" +;; + +let int name params = + try int_of_string (List.assoc name params) with + | Not_found -> default_depth + | Failure _ -> + raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) +;; + +let auto_tac ~params ~(dbd:HMysql.dbd) = + (* argument parsing *) + let depth = int "depth" params in + let width = int "width" params in + let paramodulation = bool "paramodulation" params in + let full = bool "full" params in + let superposition = bool "superposition" params in + let what = string "what" params in + let other = string "other" params in + let subterms_only = bool "subterms_only" params in + let demodulate = bool "demodulate" params in + (* the real tactic *) let auto_tac dbd (proof, goal) = let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in @@ -317,24 +344,20 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] with [] -> debug_print(lazy "Auto failed"); - raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) + raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in - debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in - debug_print (lazy (CicPp.ppterm p)); + debug_print (lazy "AUTO_TAC HA FINITO"); + let _,_,p,_ = proof in + debug_print (lazy (CicPp.ppterm p)); debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); - (proof,[]) + (proof,[]) | _ -> assert false in - let full = match full with None -> false | Some _ -> true in let paramodulation_ok = - match paramodulation with - | None -> false - | Some _ -> - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - full || (Equality.term_is_equality meta_goal) + let _, metasenv, _, _ = proof in + let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in + paramodulation && (full || (Equality.term_is_equality meta_goal)) in if paramodulation_ok then ( debug_print (lazy "USO PARAMODULATION..."); @@ -352,7 +375,11 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ) else normal_auto () in - ProofEngineTypes.mk_tactic (auto_tac dbd) + match superposition with + | true -> + ProofEngineTypes.mk_tactic + (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate) + | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) ;; (********************** applyS *******************) @@ -368,37 +395,37 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' let proof'',goals = match LibraryObjects.eq_URI () with | Some uri -> - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) - ~continuation: - (PrimitiveTactics.cut_tac - (CicSubstitution.lift 1 - (Cic.Appl - [Cic.MutInd (uri,0,[]); - Cic.Sort Cic.Prop; - consthead; - ty])))) (proof',goal) + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) + ~continuation: + (PrimitiveTactics.cut_tac + (CicSubstitution.lift 1 + (Cic.Appl + [Cic.MutInd (uri,0,[]); + Cic.Sort Cic.Prop; + consthead; + ty])))) (proof',goal) | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) in match goals with [g1;g2] -> - let proof'',goals = - ProofEngineTypes.apply_tactic - (auto_tac ~paramodulation:"qualsiasi" ~dbd ()) (proof'',g2) - in - let proof'',goals = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) + let proof'',goals = + ProofEngineTypes.apply_tactic + (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2) + in + let proof'',goals = + ProofEngineTypes.apply_tactic + (Tacticals.then_ + ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft + ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - ) (proof'',g1) - in + ) (proof'',g1) + in proof'', - (*CSC: Brrrr.... *) - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:(let _,m,_,_ = proof'' in m) + (*CSC: Brrrr.... *) + ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv + ~newmetasenv:(let _,m,_,_ = proof'' in m) | _ -> assert false let rec count_prods context ty = diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli index 207011648..1dfe0e2a9 100644 --- a/components/tactics/autoTactic.mli +++ b/components/tactics/autoTactic.mli @@ -25,8 +25,8 @@ *) val auto_tac: - ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string -> - dbd:HMysql.dbd -> unit -> + params:(string * string) list -> + dbd:HMysql.dbd -> ProofEngineTypes.tactic val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index ca9dc194b..f81556c8f 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1454,6 +1454,12 @@ let eq_of_goal = function | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) ;; +let eq_and_ty_of_goal = function + | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> + uri,t + | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) +;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1819,7 +1825,6 @@ let main_demod_equalities dbd term metasenv ugraph = ;; let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = - let module I = Inference in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_uri = eq_of_goal ty in @@ -1827,7 +1832,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = Inference.find_equalities context proof in let lib_eq_uris, library_equalities, maxm = - I.find_library_equalities dbd context (proof, goal) (maxm+2) in + Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in if library_equalities = [] then prerr_endline "VUOTA!!!"; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in @@ -1871,6 +1876,74 @@ let demodulate_tac ~dbd ~pattern = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern) ;; +let rec find_in_ctx i name = function + | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) + | Some (Cic.Name name', _)::tl when name = name' -> i + | _::tl -> find_in_ctx (i+1) name tl +;; + +let rec position_of i x = function + | [] -> assert false + | j::tl when j <> x -> position_of (i+1) x tl + | _ -> i +;; + +let superposition_tac ~what ~other ~subterms_only ~demodulate status = + reset_refs(); + let proof,goalno = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + let eq_uri,tty = eq_and_ty_of_goal ty in + let env = (metasenv, context, CicUniv.empty_ugraph) in + let names = names_of_context context in + let eq_index, equalities, maxm = find_equalities context proof in + let what = find_in_ctx 1 what context in + let other = find_in_ctx 1 other context in + let eq_what = List.nth equalities (position_of 0 what eq_index) in + let eq_other = List.nth equalities (position_of 0 other eq_index) in + let index = Indexing.index Indexing.empty eq_other in + let maxm, eql = + Indexing.superposition_right + ~subterms_only eq_uri maxm env index eq_what + in + prerr_endline ("Superposition right:"); + prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env); + prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env); + prerr_endline ("\n result: "); + List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + if demodulate then + begin + let table = List.fold_left Indexing.index Indexing.empty equalities in + let maxm,eql = + List.fold_left + (fun (maxm,acc) e -> + let maxm,eq = + Indexing.demodulation_equality + eq_uri maxm env table Utils.Positive e + in + maxm,eq::acc) + (maxm,[]) eql + in + let eql = List.rev eql in + prerr_endline ("\n result [demod]: "); + List.iter + (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql; + prerr_endline ("\n result [demod] (cut&paste): "); + List.iter + (fun e -> + let t = Equality.term_of_equality eq_uri e in + prerr_endline (CicPp.pp t names)) + eql; + end; + proof,[goalno] +;; + let get_stats () = <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ Equality.get_stats ();; diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 7a16895a7..6a4688711 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -32,8 +32,7 @@ val saturate : ?depth:int -> ?width:int -> ProofEngineTypes.proof * ProofEngineTypes.goal -> - (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) * - ProofEngineTypes.goal list + ProofEngineTypes.proof * ProofEngineTypes.goal list val weight_age_ratio : int ref val weight_age_counter: int ref @@ -52,4 +51,10 @@ val demodulate_tac: dbd:HMysql.dbd -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val superposition_tac: + what:string -> other:string -> subterms_only:bool -> + demodulate:bool -> + ProofEngineTypes.proof * ProofEngineTypes.goal -> + ProofEngineTypes.proof * ProofEngineTypes.goal list + val get_stats: unit -> string diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 06b62911c..2ff482ff1 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -3,11 +3,8 @@ val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic -val auto : - ?depth:int -> - ?width:int -> - ?paramodulation:string -> - ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic +val auto : + params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.lazy_pattern -> Cic.lazy_term -> ProofEngineTypes.tactic diff --git a/matita/matita.ml b/matita/matita.ml index 58b7de9f3..3c5bf8441 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -149,6 +149,17 @@ let _ = (MatitaScript.current ())#proofMetasenv)); prerr_endline ("stack: " ^ Continuationals.Stack.pp (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_status))); + addDebugItem "Print current proof term" + (fun _ -> + HLog.debug + (CicPp.ppterm + (match + (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status + with + | GrafiteTypes.No_proof -> (Cic.Implicit None) + | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p + | Proof p -> let _,_,p,_ = p in p + | Intermediate _ -> assert false))); (* addDebugItem "ask record choice" (fun _ -> HLog.debug (string_of_int diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index b1b2a6ad3..b230adecc 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -612,7 +612,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,[]))); MatitaGtkMisc.toggle_widget_visibility ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) ~check:main#tacticsBarMenuItem; -- 2.39.2