From 9547c888a55a5372ff2f6a2d2a9eab7d5d7c01fb Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Mon, 26 Sep 2005 14:59:01 +0000 Subject: [PATCH] new signature of auto_tac, with a new optional argument "full", to invoke the new paramodulation --- helm/ocaml/cic_notation/grafiteAst.ml | 4 +- helm/ocaml/cic_notation/grafiteParser.ml | 5 ++- helm/ocaml/tactics/.depend | 6 ++- helm/ocaml/tactics/autoTactic.ml | 11 +++-- helm/ocaml/tactics/autoTactic.mli | 5 ++- helm/ocaml/tactics/metadataQuery.ml | 52 +++++++++++++++++------- helm/ocaml/tactics/tactics.mli | 3 +- 7 files changed, 58 insertions(+), 28 deletions(-) diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index da5c85411..53cbc353f 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -47,8 +47,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term | Assumption of loc - | Auto of loc * int option * int option * string option - (* depth, width, paramodulation *) + | Auto of loc * int option * int option * string option * string option + (* depth, width, paramodulation, full *) (* ALB *) | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident | ClearBody of loc * 'ident diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml index 5caba868b..c3a4b7f01 100644 --- a/helm/ocaml/cic_notation/grafiteParser.ml +++ b/helm/ocaml/cic_notation/grafiteParser.ml @@ -112,8 +112,9 @@ EXTEND | IDENT "auto"; depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; - paramodulation = OPT [ IDENT "paramodulation" ] -> (* ALB *) - GrafiteAst.Auto (loc,depth,width,paramodulation) + paramodulation = OPT [ IDENT "paramodulation" ]; + full = OPT [ IDENT "full" ] -> (* ALB *) + GrafiteAst.Auto (loc,depth,width,paramodulation,full) | IDENT "clear"; id = IDENT -> GrafiteAst.Clear (loc,id) | IDENT "clearbody"; id = IDENT -> diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index d28ff337d..1ef89807d 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -18,10 +18,12 @@ statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi -proofEngineReduction.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi -proofEngineReduction.cmx: proofEngineHelpers.cmx proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi +proofEngineReduction.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi +proofEngineReduction.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmi tacticals.cmo: proofEngineTypes.cmi tacticals.cmi tacticals.cmx: proofEngineTypes.cmx tacticals.cmi reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \ diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index a0835a9b8..9b716637a 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -305,13 +305,15 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) *) let paramodulation_tactic = ref - (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));; + (fun dbd ?full ?depth ?width status -> + raise (ProofEngineTypes.Fail "Not Ready yet..."));; 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 ~(dbd:HMysql.dbd) () = +let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation + ?full ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof, goal) = let normal_auto () = let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in @@ -333,18 +335,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd (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 - !term_is_equality meta_goal + full || (!term_is_equality meta_goal) in if paramodulation_ok then ( debug_print (lazy "USO PARAMODULATION..."); (* try *) - !paramodulation_tactic dbd (proof, goal) + !paramodulation_tactic dbd ~depth ~width ~full (proof, goal) (* with ProofEngineTypes.Fail _ -> *) (* normal_auto () *) ) else diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index e2f20f787..696c97007 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -25,12 +25,13 @@ *) val auto_tac: - ?depth:int -> ?width:int -> ?paramodulation:string -> + ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val paramodulation_tactic: - (HMysql.dbd -> ProofEngineTypes.status -> + (HMysql.dbd -> ?full:bool -> ?depth:int -> ?width:int -> + ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list) ref val term_is_equality: diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index c266502cb..6f6b2e00a 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -255,24 +255,46 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) = uris let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) = + let to_string set = + "{ " ^ + (String.concat ", " + (Constr.UriManagerSet.fold + (fun u l -> (UriManager.string_of_uri u)::l) set [])) + ^ " }" + in let (_, metasenv, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = Constr.signature_of ty in - match main with - None -> raise Goal_is_not_an_equation - | Some (m,l) -> - if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then - let set = signature_of_hypothesis context in - let set = Constr.UriManagerSet.union set sig_constants in - let set = close_with_types set metasenv context in - let set = close_with_constructors set metasenv context in - let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in - let uris = - sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in - let uris = List.filter nonvar (List.map snd uris) in - let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in - uris - else raise Goal_is_not_an_equation +(* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *) +(* match main with *) +(* None -> raise Goal_is_not_an_equation *) +(* | Some (m,l) -> *) + let m, l = + let eq_URI = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI in + match main with + | None -> eq_URI, [] + | Some (m, l) when UriManager.eq m eq_URI -> m, l + | Some (m, l) -> eq_URI, [] + in + Printf.printf "\nSome (m, l): %s, [%s]\n\n" + (UriManager.string_of_uri m) + (String.concat "; " (List.map UriManager.string_of_uri l)); + (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *) + let set = signature_of_hypothesis context in + (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *) + let set = Constr.UriManagerSet.union set sig_constants in + let set = close_with_types set metasenv context in + (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *) + let set = close_with_constructors set metasenv context in + (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *) + let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in + let uris = + sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in + let uris = List.filter nonvar (List.map snd uris) in + let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in + uris + (* ) *) + (* else raise Goal_is_not_an_equation *) let experimental_hint ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 8ea9f641c..6d5240935 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -5,7 +5,8 @@ val assumption : ProofEngineTypes.tactic val auto : ?depth:int -> ?width:int -> - ?paramodulation:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic + ?paramodulation:string -> + ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic val change : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic -- 2.39.2