From d1126c6b78a3333bbf415daf027004496b77c2f4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 8 Sep 2005 10:42:03 +0000 Subject: [PATCH] implemented lazy disambiguation of tactics arguments, when those arguments have to be parsed in contexts extracted by a pattern --- helm/matita/matitaEngine.ml | 362 ++++++++++-------- helm/matita/matitaEngine.mli | 4 +- helm/matita/matitaMisc.mli | 3 +- .../cic_disambiguation/disambiguateTypes.ml | 4 +- .../cic_disambiguation/disambiguateTypes.mli | 4 +- helm/ocaml/cic_notation/grafiteAst.ml | 65 ++-- helm/ocaml/cic_notation/grafiteAstPp.mli | 35 +- helm/ocaml/cic_notation/grafiteParser.mli | 6 +- helm/ocaml/tactics/discriminationTactics.ml | 26 +- helm/ocaml/tactics/equalityTactics.ml | 5 +- helm/ocaml/tactics/equalityTactics.mli | 2 +- helm/ocaml/tactics/fourierR.ml | 14 +- helm/ocaml/tactics/proofEngineHelpers.ml | 48 +-- helm/ocaml/tactics/proofEngineTypes.ml | 28 +- helm/ocaml/tactics/proofEngineTypes.mli | 16 +- helm/ocaml/tactics/reductionTactics.ml | 188 +++++---- helm/ocaml/tactics/reductionTactics.mli | 18 +- helm/ocaml/tactics/tactics.mli | 11 +- helm/ocaml/tactics/variousTactics.ml | 18 +- helm/ocaml/tactics/variousTactics.mli | 2 +- 20 files changed, 488 insertions(+), 371 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 46c83de3f..a9b46267f 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -40,7 +40,9 @@ type options = { } type statement = - (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, + string) + GrafiteAst.statement (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation @@ -56,11 +58,13 @@ let namer_of names = end else FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ -let tactic_of_ast = function +let tactic_of_ast ast = + let module PET = ProofEngineTypes in + match ast with | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *) + | GrafiteAst.Auto (_,depth,width,paramodulation) -> AutoTactic.auto_tac ?depth ?width ?paramodulation ~dbd:(MatitaDb.instance ()) () | GrafiteAst.Change (_, pattern, with_what) -> @@ -85,25 +89,36 @@ let tactic_of_ast = function Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term | GrafiteAst.Elim (_, what, using, depth, names) -> - Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what + Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) + what | GrafiteAst.ElimType (_, what, using, depth, names) -> - Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what + Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) + what | GrafiteAst.Exact (_, term) -> Tactics.exact term | GrafiteAst.Exists _ -> Tactics.exists | GrafiteAst.Fail _ -> Tactics.fail | GrafiteAst.Fold (_, reduction_kind, term, pattern) -> - let reduction = - match reduction_kind with - | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] - | `Reduce -> ProofEngineReduction.reduce - | `Simpl -> ProofEngineReduction.simpl - | `Unfold what -> ProofEngineReduction.unfold ?what - | `Whd -> CicReduction.whd ~delta:false ~subst:[] - in + let reduction = + match reduction_kind with + | `Normalize -> + PET.const_lazy_reduction + (CicReduction.normalize ~delta:false ~subst:[]) + | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce + | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl + | `Unfold None -> + PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) + | `Unfold (Some lazy_term) -> + (fun context metasenv ugraph -> + let what, metasenv, ugraph = lazy_term context metasenv ugraph in + ProofEngineReduction.unfold ~what, metasenv, ugraph) + | `Whd -> + PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[]) + in Tactics.fold ~reduction ~term ~pattern | GrafiteAst.Fourier _ -> Tactics.fourier | GrafiteAst.FwdSimpl (_, hyp, names) -> - Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) + ~dbd:(MatitaDb.instance ()) hyp | GrafiteAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern @@ -116,8 +131,9 @@ let tactic_of_ast = function PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () | GrafiteAst.LApply (_, how_many, to_what, what, ident) -> - let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what + let names = match ident with None -> [] | Some id -> [id] in + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many + ~to_what what | GrafiteAst.Left _ -> Tactics.left | GrafiteAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) @@ -139,171 +155,190 @@ let tactic_of_ast = function | GrafiteAst.Symmetry _ -> Tactics.symmetry | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term -let disambiguate_term status term = +let singleton = function + | [x] -> x + | _ -> assert false + +let disambiguate_term status_ref term = + let status = !status_ref in let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) + singleton + (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) - ~metasenv:(MatitaMisc.get_proof_metasenv status) term - with - | [x] -> x - | _ -> assert false - in - let proof_status = - match status.proof_status with - | No_proof -> Intermediate metasenv - | Incomplete_proof ((uri, _, proof, ty), goal) -> - Incomplete_proof ((uri, metasenv, proof, ty), goal) - | Intermediate _ -> Intermediate metasenv - | Proof _ -> assert false + ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in - let status = { status with proof_status = proof_status } in + let status = MatitaTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status aliases in - status, cic + status_ref := status; + cic -let disambiguate_pattern status (wanted, hyp_paths, goal_path) = - let interp path = Disambiguate.interpretate_path [] status.aliases path in + (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term + * rationale: lazy_term will be invoked in different context to obtain a term, + * each invocation will disambiguate the term and can add aliases. Once all + * disambiguations have been performed, the first returned function can be + * used to obtain the resulting aliases *) +let disambiguate_lazy_term status_ref term = + (fun context metasenv ugraph -> + let status = !status_ref in + let (aliases, metasenv, cic, ugraph) = + singleton + (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) + ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv + term) + in + let status = MatitaTypes.set_metasenv metasenv status in + let status = MatitaSync.set_proof_aliases status aliases in + status_ref := status; + cic, metasenv, ugraph) + +let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = + let interp path = + Disambiguate.interpretate_path [] !status_ref.aliases path + in let goal_path = interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - let status,wanted = + let wanted = match wanted with - None -> status,None + None -> None | Some wanted -> - let status,wanted = disambiguate_term status wanted in - status, Some wanted + let wanted = disambiguate_lazy_term status_ref wanted in + Some wanted in - status, (wanted, hyp_paths ,goal_path) + (wanted, hyp_paths ,goal_path) -let disambiguate_reduction_kind status = function +let disambiguate_reduction_kind aliases_ref = function | `Unfold (Some t) -> - let status, t = disambiguate_term status t in - status, `Unfold (Some t) + let t = disambiguate_lazy_term aliases_ref t in + `Unfold (Some t) | `Normalize | `Reduce | `Simpl | `Unfold None - | `Whd as kind -> status, kind + | `Whd as kind -> kind -let disambiguate_tactic status = function - | GrafiteAst.Apply (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Apply (loc, cic) - | GrafiteAst.Absurd (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Absurd (loc, cic) - | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *) - | GrafiteAst.Change (loc, pattern, with_what) -> - let status, with_what = disambiguate_term status with_what in - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Change (loc, pattern, with_what) - | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id) - | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compare (loc,term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Compare (loc,term) - | GrafiteAst.Constructor (loc,n) -> - status, GrafiteAst.Constructor (loc,n) - | GrafiteAst.Contradiction loc -> - status, GrafiteAst.Contradiction loc - | GrafiteAst.Cut (loc, ident, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.DecideEquality loc -> - status, GrafiteAst.DecideEquality loc - | GrafiteAst.Decompose (loc, types, what, names) -> - let disambiguate (status, types) = function - | GrafiteAst.Type _ -> assert false - | GrafiteAst.Ident id -> - match disambiguate_term status (CicNotationPt.Ident (id, None)) with - | status, Cic.MutInd (uri, tyno, _) -> - status, (GrafiteAst.Type (uri, tyno) :: types) - | _ -> - raise Disambiguate.NoWellTypedInterpretation - in - let status, types = List.fold_left disambiguate (status, []) types in - status, GrafiteAst.Decompose(loc, types, what, names) - | GrafiteAst.Discriminate (loc,term) -> - let status,term = disambiguate_term status term in - status, GrafiteAst.Discriminate(loc,term) - | GrafiteAst.Exact (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Exact (loc, cic) - | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> - let status, what = disambiguate_term status what in - let status, using = disambiguate_term status using in - status, GrafiteAst.Elim (loc, what, Some using, depth, idents) - | GrafiteAst.Elim (loc, what, None, depth, idents) -> - let status, what = disambiguate_term status what in - status, GrafiteAst.Elim (loc, what, None, depth, idents) - | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> - let status, what = disambiguate_term status what in - let status, using = disambiguate_term status using in - status, GrafiteAst.ElimType (loc, what, Some using, depth, idents) - | GrafiteAst.ElimType (loc, what, None, depth, idents) -> - let status, what = disambiguate_term status what in - status, GrafiteAst.ElimType (loc, what, None, depth, idents) - | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc - | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc - | GrafiteAst.Fold (loc,red_kind, term, pattern) -> - let status, pattern = disambiguate_pattern status pattern in - let status, term = disambiguate_term status term in - let status, red_kind = disambiguate_reduction_kind status red_kind in - status, GrafiteAst.Fold (loc,red_kind, term, pattern) - | GrafiteAst.FwdSimpl (loc, hyp, names) -> - status, GrafiteAst.FwdSimpl (loc, hyp, names) - | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc - | GrafiteAst.Generalize (loc,pattern,ident) -> - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Generalize(loc,pattern,ident) - | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g) - | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc - | GrafiteAst.Injection (loc,term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Injection (loc,term) - | GrafiteAst.Intros (loc, num, names) -> - status, GrafiteAst.Intros (loc, num, names) - | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> - let f term (status, to_what) = - let status, term = disambiguate_term status term in - status, term :: to_what - in - let status, to_what = List.fold_right f to_what (status, []) in - let status, what = disambiguate_term status what in - status, GrafiteAst.LApply (loc, depth, to_what, what, ident) - | GrafiteAst.Left loc -> status, GrafiteAst.Left loc - | GrafiteAst.LetIn (loc, term, name) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.LetIn (loc,term,name) - | GrafiteAst.Reduce (loc, red_kind, pattern) -> - let status, pattern = disambiguate_pattern status pattern in - let status, red_kind = disambiguate_reduction_kind status red_kind in - status, GrafiteAst.Reduce(loc, red_kind, pattern) - | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc - | GrafiteAst.Replace (loc, pattern, with_what) -> - let status, pattern = disambiguate_pattern status pattern in - let status, with_what = disambiguate_term status with_what in - status, GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern) -> - let status, term = disambiguate_term status t in - let status, pattern = disambiguate_pattern status pattern in - status, GrafiteAst.Rewrite (loc, dir, term, pattern) - | GrafiteAst.Right loc -> status, GrafiteAst.Right loc - | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc - | GrafiteAst.Split loc -> status, GrafiteAst.Split loc - | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc - | GrafiteAst.Transitivity (loc, term) -> - let status, cic = disambiguate_term status term in - status, GrafiteAst.Transitivity (loc, cic) +let disambiguate_tactic status tactic = + let status_ref = ref status in + let tactic = + match tactic with + | GrafiteAst.Absurd (loc, term) -> + let cic = disambiguate_term status_ref term in + GrafiteAst.Absurd (loc, cic) + | GrafiteAst.Apply (loc, term) -> + let cic = disambiguate_term status_ref term in + GrafiteAst.Apply (loc, cic) + | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc + | GrafiteAst.Auto (loc,depth,width,paramodulation) -> + GrafiteAst.Auto (loc,depth,width,paramodulation) + | GrafiteAst.Change (loc, pattern, with_what) -> + let with_what = disambiguate_lazy_term status_ref with_what in + let pattern = disambiguate_pattern status_ref pattern in + GrafiteAst.Change (loc, pattern, with_what) + | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id) + | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id) + | GrafiteAst.Compare (loc,term) -> + let term = disambiguate_term status_ref term in + GrafiteAst.Compare (loc,term) + | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n) + | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc + | GrafiteAst.Cut (loc, ident, term) -> + let cic = disambiguate_term status_ref term in + GrafiteAst.Cut (loc, ident, cic) + | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc + | GrafiteAst.Decompose (loc, types, what, names) -> + let disambiguate types = function + | GrafiteAst.Type _ -> assert false + | GrafiteAst.Ident id -> + (match disambiguate_term status_ref (CicNotationPt.Ident (id, None)) with + | Cic.MutInd (uri, tyno, _) -> + (GrafiteAst.Type (uri, tyno) :: types) + | _ -> raise Disambiguate.NoWellTypedInterpretation) + in + let types = List.fold_left disambiguate [] types in + GrafiteAst.Decompose (loc, types, what, names) + | GrafiteAst.Discriminate (loc,term) -> + let term = disambiguate_term status_ref term in + GrafiteAst.Discriminate(loc,term) + | GrafiteAst.Exact (loc, term) -> + let cic = disambiguate_term status_ref term in + GrafiteAst.Exact (loc, cic) + | GrafiteAst.Elim (loc, what, Some using, depth, idents) -> + let what = disambiguate_term status_ref what in + let using = disambiguate_term status_ref using in + GrafiteAst.Elim (loc, what, Some using, depth, idents) + | GrafiteAst.Elim (loc, what, None, depth, idents) -> + let what = disambiguate_term status_ref what in + GrafiteAst.Elim (loc, what, None, depth, idents) + | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> + let what = disambiguate_term status_ref what in + let using = disambiguate_term status_ref using in + GrafiteAst.ElimType (loc, what, Some using, depth, idents) + | GrafiteAst.ElimType (loc, what, None, depth, idents) -> + let what = disambiguate_term status_ref what in + GrafiteAst.ElimType (loc, what, None, depth, idents) + | GrafiteAst.Exists loc -> GrafiteAst.Exists loc + | GrafiteAst.Fail loc -> GrafiteAst.Fail loc + | GrafiteAst.Fold (loc,red_kind, term, pattern) -> + let pattern = disambiguate_pattern status_ref pattern in + let term = disambiguate_lazy_term status_ref term in + let red_kind = disambiguate_reduction_kind status_ref red_kind in + GrafiteAst.Fold (loc, red_kind, term, pattern) + | GrafiteAst.FwdSimpl (loc, hyp, names) -> + GrafiteAst.FwdSimpl (loc, hyp, names) + | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc + | GrafiteAst.Generalize (loc,pattern,ident) -> + let pattern = disambiguate_pattern status_ref pattern in + GrafiteAst.Generalize (loc,pattern,ident) + | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g) + | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc + | GrafiteAst.Injection (loc, term) -> + let term = disambiguate_term status_ref term in + GrafiteAst.Injection (loc,term) + | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names) + | GrafiteAst.LApply (loc, depth, to_what, what, ident) -> + let f term to_what = + let term = disambiguate_term status_ref term in + term :: to_what + in + let to_what = List.fold_right f to_what [] in + let what = disambiguate_term status_ref what in + GrafiteAst.LApply (loc, depth, to_what, what, ident) + | GrafiteAst.Left loc -> GrafiteAst.Left loc + | GrafiteAst.LetIn (loc, term, name) -> + let term = disambiguate_term status_ref term in + GrafiteAst.LetIn (loc,term,name) + | GrafiteAst.Reduce (loc, red_kind, pattern) -> + let pattern = disambiguate_pattern status_ref pattern in + let red_kind = disambiguate_reduction_kind status_ref red_kind in + GrafiteAst.Reduce(loc, red_kind, pattern) + | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc + | GrafiteAst.Replace (loc, pattern, with_what) -> + let pattern = disambiguate_pattern status_ref pattern in + let with_what = disambiguate_lazy_term status_ref with_what in + GrafiteAst.Replace (loc, pattern, with_what) + | GrafiteAst.Rewrite (loc, dir, t, pattern) -> + let term = disambiguate_term status_ref t in + let pattern = disambiguate_pattern status_ref pattern in + GrafiteAst.Rewrite (loc, dir, term, pattern) + | GrafiteAst.Right loc -> GrafiteAst.Right loc + | GrafiteAst.Ring loc -> GrafiteAst.Ring loc + | GrafiteAst.Split loc -> GrafiteAst.Split loc + | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc + | GrafiteAst.Transitivity (loc, term) -> + let cic = disambiguate_term status_ref term in + GrafiteAst.Transitivity (loc, cic) + in + status_ref, tactic let apply_tactic tactic status = - let status,tactic = disambiguate_tactic status tactic in + let status_ref, tactic = disambiguate_tactic status tactic in + let proof_status = MatitaMisc.get_proof_status !status_ref in let tactic = tactic_of_ast tactic in - let (proof, goals) = - ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in + (* apply tactic will change the status pointed by status_ref ... *) + let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in let dummy = -1 in - { status with - proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals + { !status_ref with + proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, + goals module MatitaStatus = struct @@ -509,11 +544,12 @@ let disambiguate_command status = function | GrafiteAst.Set _ as cmd -> status,cmd | GrafiteAst.Coercion (loc, term) -> - let status, term = disambiguate_term status term in - status, GrafiteAst.Coercion (loc,term) + let status_ref = ref status in + let term = disambiguate_term status_ref term in + !status_ref, GrafiteAst.Coercion (loc,term) | GrafiteAst.Obj (loc,obj) -> let status,obj = disambiguate_obj status obj in - status, GrafiteAst.Obj (loc,obj) + status, GrafiteAst.Obj (loc,obj) let make_absolute paths path = if path = "coq.ma" then path diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 6c8b86605..280b6c8f4 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -28,7 +28,9 @@ exception UnableToInclude of string exception IncludedFileNotCompiled of string type statement = - (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, + string) + GrafiteAst.statement (* heavy checks slow down the compilation process but give you some interesting * infos like if the theorem is a duplicate *) diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 9cbada588..568bcc5ed 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -25,7 +25,8 @@ val baseuri_of_file : string -> string -val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option +val baseuri_of_baseuri_decl: + ('a, 'b, 'c, 'd, 'e) GrafiteAst.statement -> string option (** check whether no objects are defined below a given baseuri *) val is_empty: string -> bool diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index c30316769..6c530c2bf 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -24,8 +24,8 @@ *) type term = CicNotationPt.term -type tactic = (term, string) GrafiteAst.tactic -type tactical = (term, string) GrafiteAst.tactical +type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic +type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical type script_entry = | Command of tactical | Comment of CicNotationPt.location * string diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 084ce0122..b6d74a7fd 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -70,8 +70,8 @@ val string_of_domain: domain_item list -> string (** {3 type shortands} *) type term = CicNotationPt.term -type tactic = (term, string) GrafiteAst.tactic -type tactical = (term, string) GrafiteAst.tactical +type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic +type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical type script_entry = | Command of tactical diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml index 82d904989..f7e953b8c 100644 --- a/helm/ocaml/cic_notation/grafiteAst.ml +++ b/helm/ocaml/cic_notation/grafiteAst.ml @@ -26,23 +26,30 @@ module Ast = CicNotationPt type direction = [ `LeftToRight | `RightToLeft ] -type 'term reduction_kind = - [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ] type loc = Ast.location -type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term +type ('term, 'lazy_term, 'ident) pattern = + 'lazy_term option * ('ident * 'term) list * 'term type ('term, 'ident) type_spec = | Ident of 'ident | Type of UriManager.uri * int -type ('term, 'ident) tactic = +type reduction = + [ `Normalize + | `Reduce + | `Simpl + | `Unfold of CicNotationPt.term option + | `Whd ] + +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 ALB *) - | Change of loc * ('term,'ident) pattern * 'term + | Auto of loc * int option * int option * string option + (* depth, width, paramodulation *) + | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident | ClearBody of loc * 'ident | Compare of loc * 'term @@ -57,10 +64,10 @@ type ('term, 'ident) tactic = | Exact of loc * 'term | Exists of loc | Fail of loc - | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern + | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern | Fourier of loc | FwdSimpl of loc * string * 'ident list - | Generalize of loc * ('term, 'ident) pattern * 'ident option + | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option | Goal of loc * int (* change current goal, argument is goal number 1-based *) | IdTac of loc | Injection of loc * 'term @@ -68,10 +75,11 @@ type ('term, 'ident) tactic = | LApply of loc * int option * 'term list * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident - | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern + | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern | Reflexivity of loc - | Replace of loc * ('term, 'ident) pattern * 'term - | Rewrite of loc * direction * 'term * ('term, 'ident) pattern + | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term + | Rewrite of loc * direction * 'term * + ('term, 'lazy_term, 'ident) pattern | Right of loc | Ring of loc | Split of loc @@ -153,28 +161,31 @@ type ('term,'obj) command = (* DEBUGGING *) | Render of loc * UriManager.uri (* render library object *) -type ('term, 'ident) tactical = - | Tactic of loc * ('term, 'ident) tactic - | Do of loc * int * ('term, 'ident) tactical - | Repeat of loc * ('term, 'ident) tactical - | Seq of loc * ('term, 'ident) tactical list (* sequential composition *) - | Then of loc * ('term, 'ident) tactical * ('term, 'ident) tactical list - | First of loc * ('term, 'ident) tactical list +type ('term, 'lazy_term, 'reduction, 'ident) tactical = + | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic + | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical + | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical + | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list + (* sequential composition *) + | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical * + ('term, 'lazy_term, 'reduction, 'ident) tactical list + | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) - | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) - | Solve of loc * ('term, 'ident) tactical list + | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical + (* try a tactical and mask failures *) + | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list -type ('term, 'obj, 'ident) code = +type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term,'obj) command | Macro of loc * 'term macro - | Tactical of loc * ('term, 'ident) tactical + | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical -type ('term, 'obj, 'ident) comment = +type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = | Note of loc * string - | Code of loc * ('term, 'obj, 'ident) code + | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code -type ('term, 'obj, 'ident) statement = - | Executable of loc * ('term, 'obj, 'ident) code - | Comment of loc * ('term, 'obj, 'ident) comment +type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement = + | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code + | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment diff --git a/helm/ocaml/cic_notation/grafiteAstPp.mli b/helm/ocaml/cic_notation/grafiteAstPp.mli index 9268ea25b..ad6c26db1 100644 --- a/helm/ocaml/cic_notation/grafiteAstPp.mli +++ b/helm/ocaml/cic_notation/grafiteAstPp.mli @@ -23,16 +23,41 @@ * http://helm.cs.unibo.it/ *) -val pp_tactic: (CicNotationPt.term, string) GrafiteAst.tactic -> string +val pp_tactic: + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string) + GrafiteAst.tactic -> + string + val pp_obj: GrafiteAst.obj -> string val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string -val pp_comment: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.comment -> string -val pp_executable: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.code -> string -val pp_statement: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.statement -> string + +val pp_comment: + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, + string) + GrafiteAst.comment -> + string + +val pp_executable: + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, + string) + GrafiteAst.code -> + string + +val pp_statement: + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj, + string) + GrafiteAst.statement -> + string + val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string val pp_macro_cic: Cic.term GrafiteAst.macro -> string -val pp_tactical: (CicNotationPt.term, string) GrafiteAst.tactical -> string + +val pp_tactical: + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string) + GrafiteAst.tactical -> + string + val pp_alias: GrafiteAst.alias_spec -> string val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string diff --git a/helm/ocaml/cic_notation/grafiteParser.mli b/helm/ocaml/cic_notation/grafiteParser.mli index ccea04836..3d4112016 100644 --- a/helm/ocaml/cic_notation/grafiteParser.mli +++ b/helm/ocaml/cic_notation/grafiteParser.mli @@ -25,6 +25,8 @@ (** @raise End_of_file *) val parse_statement: - char Stream.t -> - (CicNotationPt.term, GrafiteAst.obj, string) GrafiteAst.statement + char Stream.t -> + (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, + GrafiteAst.obj, string) + GrafiteAst.statement diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 590b482c7..a26895e62 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -162,21 +162,18 @@ and injection1_tac ~term ~i = in ProofEngineTypes.apply_tactic (ReductionTactics.change_tac - ~pattern:(ProofEngineTypes.conclusion_pattern (Some new_t1')) - (C.Appl [ - C.Lambda ( - C.Name "x", tty, - C.MutCase ( - turi, typeno, - (C.Lambda ( - (C.Name "x"), + ~pattern:(ProofEngineTypes.conclusion_pattern + (Some new_t1')) + (fun _ m u -> + C.Appl [ C.Lambda (C.Name "x", tty, + C.MutCase (turi, typeno, + (C.Lambda ((C.Name "x"), (S.lift 1 tty), (S.lift 2 tty'))), (C.Rel 1), pattern ) ); - t1] - )) + t1], m, u)) status )) ~continuation: @@ -300,8 +297,9 @@ let discriminate'_tac ~term = (T.then_ ~start: (ReductionTactics.change_tac - ~pattern:(ProofEngineTypes.conclusion_pattern (Some gty')) - (C.Appl [ + ~pattern:(ProofEngineTypes.conclusion_pattern + (Some gty')) + (fun _ m u -> C.Appl [ C.Lambda ( C.Name "x", tty, C.MutCase ( @@ -310,9 +308,7 @@ let discriminate'_tac ~term = (C.Rel 1), pattern ) ); - t2] - ) - ) + t2], m, u)) ~continuation: ( T.then_ diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index a14a418bf..94cb0624b 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -71,7 +71,9 @@ let rewrite_tac ~direction ~pattern equality = let lifted_gty = CicSubstitution.lift 1 gty in let lifted_conjecture = metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in - let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in + let lifted_pattern = + Some (fun _ m u -> lifted_t1, m, u),[],CicSubstitution.lift 1 concl_pat + in let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select ~metasenv:metasenv' ~ugraph ~conjecture:lifted_conjecture @@ -140,6 +142,7 @@ let replace_tac ~pattern ~with_what = ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture ~pattern in let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let with_what, metasenv, u = with_what context metasenv u in let with_what = CicMetaSubst.apply_subst subst with_what in let pbo = CicMetaSubst.apply_subst subst pbo in let pty = CicMetaSubst.apply_subst subst pty in diff --git a/helm/ocaml/tactics/equalityTactics.mli b/helm/ocaml/tactics/equalityTactics.mli index a9b4d1d0b..b9112deed 100644 --- a/helm/ocaml/tactics/equalityTactics.mli +++ b/helm/ocaml/tactics/equalityTactics.mli @@ -32,7 +32,7 @@ val rewrite_simpl_tac: val replace_tac: pattern:ProofEngineTypes.pattern -> - with_what:Cic.term -> ProofEngineTypes.tactic + with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index a424987a2..f586455a2 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -692,17 +692,19 @@ let tac_zero_infeq_false gl (n,d) = apply_tactic (Tacticals.then_ ~start: - (ReductionTactics.fold_tac ~reduction:CicReduction.whd + (ReductionTactics.fold_tac + ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern:(ProofEngineTypes.conclusion_pattern None) ~term: - (Cic.Appl + (const_lazy_term + (Cic.Appl [_Rle ; _R0 ; Cic.Appl - [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])) + [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]]))) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) - ~continuation:(tac_zero_inf_pos (-n,d)))) + ~continuation:(tac_zero_inf_pos (-n,d)))) status in mk_tactic (tac_zero_infeq_false gl (n,d)) @@ -1135,7 +1137,7 @@ let rec fourier (s_proof,s_goal)= apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) - (Cic.Appl [ _not; ineq])) + (const_lazy_term (Cic.Appl [ _not; ineq]))) status)) ~continuation:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term: @@ -1181,7 +1183,7 @@ let rec fourier (s_proof,s_goal)= let r = apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) - w1) status + (const_lazy_term w1)) status in debug("fine MY_CHNGE\n"); r)) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 5c9b1f7a0..a7c1d39bd 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -309,12 +309,10 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = [] -> [],metasenv,ugraph,[] | (context',where)::tl -> let subst,metasenv,ugraph,tl' = find_in_roots tl in - let context'_len = List.length context' in let subst,metasenv,ugraph,found = - let wanted = - CicSubstitution.lift (context'_len - context_len) wanted - in - find_subterms ~subst ~metasenv ~ugraph ~wanted ~context where + let wanted, metasenv, ugraph = wanted context' metasenv ugraph in + find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context' + where in subst,metasenv,ugraph,found @ tl' in @@ -494,30 +492,12 @@ exception Fail of string | None -> subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context) | Some pat -> - try - let what = - match what with - None -> None - | Some what -> - let what,subst',metasenv' = - CicMetaSubst.delift_rels [] metasenv - (context_len - List.length context) what - in - assert (subst' = []); - assert (metasenv' = metasenv); - Some what in let subst,metasenv,ugraph,terms = select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(what,pat) in subst,metasenv,ugraph,((Some (`Decl terms))::res), - (entry::context) - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) + (entry::context)) | Some (name,Cic.Def (bo, ty)) -> (match find_pattern_for name with | None -> @@ -525,18 +505,6 @@ exception Fail of string subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res), (entry::context) | Some pat -> - try - let what = - match what with - None -> None - | Some what -> - let what,subst',metasenv' = - CicMetaSubst.delift_rels [] metasenv - (context_len - List.length context) what - in - assert (subst' = []); - assert (metasenv' = metasenv); - Some what in let subst,metasenv,ugraph,terms_bo = select_in_term ~metasenv ~context ~ugraph ~term:bo ~pattern:(what,pat) in @@ -551,13 +519,7 @@ exception Fail of string subst,metasenv,ugraph,Some res in subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res), - (entry::context) - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise - (Fail - ("The term the user wants to convert is not closed " ^ - "in the context of the position of the substitution."))) + (entry::context)) ) context (subst,metasenv,ugraph,[],[])) in subst,metasenv,ugraph,res diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 9e92a076c..2e25e4a05 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -56,9 +56,31 @@ type tactic = status -> proof * goal list (** creates an opaque tactic from a status->proof*goal list function *) let mk_tactic t = t - (** what, hypothesis patterns, conclusion pattern *) -type pattern = Cic.term option * (string * Cic.term) list * Cic.term -let conclusion_pattern t = t,[],Cic.Implicit (Some `Hole) +type reduction = Cic.context -> Cic.term -> Cic.term + +type lazy_term = + Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> + Cic.term * Cic.metasenv * CicUniv.universe_graph + +let const_lazy_term t = + (fun _ metasenv ugraph -> t, metasenv, ugraph) + +type lazy_reduction = + Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> + reduction * Cic.metasenv * CicUniv.universe_graph + +let const_lazy_reduction red = + (fun _ metasenv ugraph -> red, metasenv, ugraph) + +type pattern = lazy_term option * (string * Cic.term) list * Cic.term + +let conclusion_pattern t = + let t' = + match t with + | None -> None + | Some t -> Some (fun _ m u -> t, m, u) + in + t',[],Cic.Implicit (Some `Hole) (** tactic failure *) exception Fail of string diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index 4d418b5bc..63be26bb7 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -44,8 +44,22 @@ val initial_status: Cic.term -> Cic.metasenv -> status type tactic val mk_tactic: (status -> proof * goal list) -> tactic +type reduction = Cic.context -> Cic.term -> Cic.term + +type lazy_term = + Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> + Cic.term * Cic.metasenv * CicUniv.universe_graph + +val const_lazy_term: Cic.term -> lazy_term + +type lazy_reduction = + Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> + reduction * Cic.metasenv * CicUniv.universe_graph + +val const_lazy_reduction: reduction -> lazy_reduction + (** what, hypothesis patterns, conclusion pattern *) -type pattern = Cic.term option * (string * Cic.term) list * Cic.term +type pattern = lazy_term option * (string * Cic.term) list * Cic.term (** conclusion_pattern [t] returns the pattern (t,[],%) *) val conclusion_pattern : Cic.term option -> pattern diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index f5c82a9fe..8f806883e 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -30,40 +30,56 @@ open ProofEngineTypes let reduction_tac ~reduction ~pattern (proof,goal) = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let change subst where terms = - if terms = [] then where + let change subst where terms metasenv ugraph = + if terms = [] then where, metasenv, ugraph else - let terms, terms' = - List.split (List.map (fun (context, t) -> t, reduction context t) terms) - in - let where' = - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where - in - CicMetaSubst.apply_subst subst where' in + let pairs, metasenv, ugraph = + List.fold_left + (fun (pairs, metasenv, ugraph) (context, t) -> + let reduction, metasenv, ugraph = reduction context metasenv ugraph in + ((t, reduction context t) :: pairs), metasenv, ugraph) + ([], metasenv, ugraph) + terms + in + let terms, terms' = List.split pairs in + let where' = + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where + in + CicMetaSubst.apply_subst subst where', metasenv, ugraph + in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph - ~conjecture ~pattern in - let ty' = change subst ty selected_ty in - let context' = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ~conjecture ~pattern + in + let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in + let context', metasenv, ugraph = List.fold_right2 - (fun entry selected_entry context' -> + (fun entry selected_entry (context', metasenv, ugraph) -> match entry,selected_entry with - None,None -> None::context' + None,None -> None::context', metasenv, ugraph | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> - let ty' = change subst ty selected_ty in - Some (name,Cic.Decl ty')::context' + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + Some (name,Cic.Decl ty')::context', metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> - let bo' = change subst bo selected_bo in - let ty' = + let bo', metasenv, ugraph = + change subst bo selected_bo metasenv ugraph + in + let ty', metasenv, ugraph = match ty,selected_ty with - None,None -> None - | Some ty,Some selected_ty -> Some (change subst ty selected_ty) + None,None -> None, metasenv, ugraph + | Some ty,Some selected_ty -> + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + Some ty', metasenv, ugraph | _,_ -> assert false in - Some (name,Cic.Def (bo',ty'))::context' + (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false - ) context selected_context [] in + ) context selected_context ([], metasenv, ugraph) in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') @@ -74,20 +90,31 @@ let reduction_tac ~reduction ~pattern (proof,goal) = ;; let simpl_tac ~pattern = - mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern) let reduce_tac ~pattern = - mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern) let unfold_tac what ~pattern = - mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what) - ~pattern);; + let reduction = + match what with + | None -> const_lazy_reduction (ProofEngineReduction.unfold ?what:None) + | Some lazy_term -> + (fun context metasenv ugraph -> + let what, metasenv, ugraph = lazy_term context metasenv ugraph in + ProofEngineReduction.unfold ~what, metasenv, ugraph) + in + mk_tactic (reduction_tac ~reduction ~pattern) let whd_tac ~pattern = - mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern) let normalize_tac ~pattern = - mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);; + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern) exception NotConvertible @@ -104,74 +131,71 @@ let change_tac ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = let curi,metasenv,pbo,pty = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let context_len = List.length context in - let change subst context'_len where terms = - if terms = [] then where + let change subst where terms metasenv ugraph = + if terms = [] then where, metasenv, ugraph else - let terms, terms' = - List.split - (List.map - (fun (context_of_t, t) -> - let context_of_t_len = List.length context_of_t in - let with_what_in_context' = - if context_len > context'_len then - begin - let with_what,subst,metasenv' = - CicMetaSubst.delift_rels [] metasenv - (context_len - context'_len) with_what - in - assert (subst = []); - assert (metasenv = metasenv'); - with_what - end - else - with_what in - let with_what_in_context_of_t = - if context_of_t_len > context'_len then - CicSubstitution.lift (context_of_t_len - context'_len) - with_what_in_context' - else - with_what in + let pairs, metasenv, ugraph = + List.fold_left + (fun (pairs, metasenv, ugraph) (context_of_t, t) -> +prerr_endline "++++++++++++++++++++++++++"; +prerr_endline "context_of_t"; +prerr_endline (CicMetaSubst.ppcontext [] context_of_t); +prerr_endline "t"; +prerr_endline (CicMetaSubst.ppterm [] t); + let with_what, metasenv, ugraph = + with_what context_of_t metasenv ugraph + in let _,u = - CicTypeChecker.type_of_aux' metasenv context_of_t with_what - CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph + in let b,_ = - CicReduction.are_convertible ~metasenv context_of_t t with_what u in + CicReduction.are_convertible ~metasenv context_of_t t with_what u + in if b then - t, with_what_in_context_of_t + ((t, with_what) :: pairs), metasenv, ugraph else - raise NotConvertible) terms) + raise NotConvertible) + ([], metasenv, ugraph) + terms in + let terms, terms' = List.split pairs in let where' = ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' ~where:where in - CicMetaSubst.apply_subst subst where' in + CicMetaSubst.apply_subst subst where', metasenv, ugraph + in let (subst,metasenv,ugraph,selected_context,selected_ty) = ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture ~pattern in - let ty' = change subst context_len ty selected_ty in - let context' = + let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in + let context', metasenv, ugraph = List.fold_right2 - (fun entry selected_entry context' -> - let context'_len = List.length context' in + (fun entry selected_entry (context', metasenv, ugraph) -> match entry,selected_entry with - None,None -> None::context' + None,None -> (None::context'), metasenv, ugraph | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> - let ty' = change subst context'_len ty selected_ty in - Some (name,Cic.Decl ty')::context' + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + (Some (name,Cic.Decl ty')::context'), metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> - let bo' = change subst context'_len bo selected_bo in - let ty' = + let bo', metasenv, ugraph = + change subst bo selected_bo metasenv ugraph + in + let ty', metasenv, ugraph = match ty,selected_ty with - None,None -> None + None,None -> None, metasenv, ugraph | Some ty,Some selected_ty -> - Some (change subst context'_len ty selected_ty) + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + Some ty', metasenv, ugraph | _,_ -> assert false in - Some (name,Cic.Def (bo',ty'))::context' + (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false - ) context selected_context [] in + ) context selected_context ([], metasenv, ugraph) in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') @@ -185,12 +209,14 @@ let change_tac ~pattern with_what = let fold_tac ~reduction ~term ~pattern = let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status = assert (wanted = None); (* this should be checked syntactically *) - let proof,goal = status in - let _,metasenv,_,_ = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in - let reduced_term = reduction context term in + let reduced_term = + (fun context metasenv ugraph -> + let term, metasenv, ugraph = term context metasenv ugraph in + let reduction, metasenv, ugraph = reduction context metasenv ugraph in + reduction context term, metasenv, ugraph) + in apply_tactic (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status in mk_tactic (fold_tac ~reduction ~term ~pattern) -;; + diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 56b80c06a..dbec3fb72 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -23,17 +23,25 @@ * http://cs.unibo.it/helm/. *) -(* The default of term is the thesis of the goal to be prooved *) val simpl_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reduce_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + +(* The default of term is the thesis of the goal to be prooved *) val unfold_tac: - Cic.term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + ProofEngineTypes.lazy_term option -> + pattern:ProofEngineTypes.pattern -> + ProofEngineTypes.tactic val change_tac: - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> + ProofEngineTypes.lazy_term -> + ProofEngineTypes.tactic val fold_tac: - reduction:(Cic.context -> Cic.term -> Cic.term) -> term:Cic.term -> - pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic + reduction:ProofEngineTypes.lazy_reduction -> + term:ProofEngineTypes.lazy_term -> + pattern:ProofEngineTypes.pattern -> + ProofEngineTypes.tactic + diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 77e3f8ac5..5ac63b07e 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -7,7 +7,8 @@ val auto : ?width:int -> ?paramodulation:string -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic val change : - pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.pattern -> + ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val clear : hyp:string -> ProofEngineTypes.tactic val clearbody : hyp:string -> ProofEngineTypes.tactic val compare : term:Cic.term -> ProofEngineTypes.tactic @@ -35,8 +36,8 @@ val exact : term:Cic.term -> ProofEngineTypes.tactic val exists : ProofEngineTypes.tactic val fail : ProofEngineTypes.tactic val fold : - reduction:(Cic.context -> Cic.term -> Cic.term) -> - term:Cic.term -> + reduction:ProofEngineTypes.lazy_reduction -> + term:ProofEngineTypes.lazy_term -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic val fwd_simpl : @@ -64,7 +65,7 @@ val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : pattern:ProofEngineTypes.pattern -> - with_what:Cic.term -> ProofEngineTypes.tactic + with_what:ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic val rewrite : direction:[ `LeftToRight | `RightToLeft ] -> pattern:ProofEngineTypes.pattern -> Cic.term -> ProofEngineTypes.tactic @@ -79,6 +80,6 @@ val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val unfold : - Cic.term option -> + ProofEngineTypes.lazy_term option -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index bc6d522b9..51f28b3c9 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -94,15 +94,21 @@ let generalize_tac let term = match term with None -> None - | Some term -> Some (CicMetaSubst.apply_subst subst term) in - let u,typ,term = - let context_of_t,t = + | Some term -> + Some (fun context metasenv ugraph -> + let term, metasenv, ugraph = term context metasenv ugraph in + CicMetaSubst.apply_subst subst term, metasenv, ugraph) + in + let u,typ,term, metasenv = + let context_of_t, (t, metasenv, u) = match terms_with_context, term with [], None -> raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly - | _, Some t -> context,t - | (context_of_t,t)::_, None -> context_of_t,t + | [], Some t -> context, t context metasenv u + | (context_of_t, _)::_, Some t -> + context_of_t, t context_of_t metasenv u + | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u) in let t,subst,metasenv' = try @@ -116,7 +122,7 @@ let generalize_tac assert (subst = []); assert (metasenv' = metasenv); let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in - u,typ,t + u,typ,t,metasenv in (* We need to check: 1. whether they live in the context of the goal; diff --git a/helm/ocaml/tactics/variousTactics.mli b/helm/ocaml/tactics/variousTactics.mli index a71332879..f792666c2 100644 --- a/helm/ocaml/tactics/variousTactics.mli +++ b/helm/ocaml/tactics/variousTactics.mli @@ -31,4 +31,4 @@ val assumption_tac: ProofEngineTypes.tactic val generalize_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ProofEngineTypes.pattern -> - ProofEngineTypes.tactic + ProofEngineTypes.tactic -- 2.39.2