From: Claudio Sacerdoti Coen Date: Wed, 29 Jun 2005 16:24:08 +0000 (+0000) Subject: 1. new syntax for patterns: X-Git-Tag: PRE_GETTER_STORAGE~110 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddf4e9d7ed1cde82e64e95054cf9b0fa49cdf226;p=helm.git 1. new syntax for patterns: [t] [in p] where t is the term to be matched and p is the pattern on the hypotheses and on the conclusion (whose syntax is not changed). All the tactics now use the new syntax. 2. several tactics have been changed to use the new kind of patterns (that also have the optional term in them) 3. the signature of the select function has changed to require the context (and return a context and not a "context patch"); moreover it performs now both the search for roots and the search for subterms of the roots that are alpha-convertible with the optional given term (if any) WARNING!!! The following tactics have been commented out for a while: replace rewrite change fold --- diff --git a/helm/matita/.depend b/helm/matita/.depend index afd46f500..74f662413 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -27,9 +27,11 @@ matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaLog.cmx \ matitaLog.cmo: matitaLog.cmi matitaLog.cmx: matitaLog.cmi matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ - matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo matitaMathView.cmi + matitaGui.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \ + matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx matitaMathView.cmi + matitaGui.cmx matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ + matitaMathView.cmi matitaMisc.cmo: matitaTypes.cmo buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ @@ -44,10 +46,10 @@ matitaTypes.cmo: matitaLog.cmi matitaTypes.cmx: matitaLog.cmx matitac.cmo: matitacLib.cmi matitac.cmx: matitacLib.cmx -matitacLib.cmo: matitaTypes.cmo matitaLog.cmi matitaEngine.cmi matitaDb.cmi \ - buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitaTypes.cmx matitaLog.cmx matitaEngine.cmx matitaDb.cmx \ - buildTimeConf.cmx matitacLib.cmi +matitacLib.cmo: matitaTypes.cmo matitaLog.cmi matitaExcPp.cmi \ + matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ + matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi matitaDisambiguator.cmi: matitaTypes.cmo matitaEngine.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 222ca491b..a28cdedf8 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -27,8 +27,8 @@ let tactic_of_ast = function | TacticAst.Assumption _ -> Tactics.assumption | TacticAst.Auto (_,depth,width) -> AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) () - | TacticAst.Change (_, what, with_what, pattern) -> - Tactics.change ~what ~with_what ~pattern + | TacticAst.Change (_, pattern, with_what) -> + Tactics.change ~pattern with_what | TacticAst.Clear (_,id) -> Tactics.clear id | TacticAst.ClearBody (_,id) -> Tactics.clearbody id | TacticAst.Contradiction _ -> Tactics.contradiction @@ -46,7 +46,7 @@ let tactic_of_ast = function | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Exists _ -> Tactics.exists | TacticAst.Fail _ -> Tactics.fail - | TacticAst.Fold (_, reduction_kind ,term, pattern) -> + | TacticAst.Fold (_, reduction_kind, pattern) -> let reduction = match reduction_kind with | `Normalize -> CicReduction.normalize ~delta:false ~subst:[] @@ -54,13 +54,13 @@ let tactic_of_ast = function | `Simpl -> ProofEngineReduction.simpl | `Whd -> CicReduction.whd ~delta:false ~subst:[] in - Tactics.fold ~reduction ~pattern ~term + Tactics.fold ~reduction ~pattern | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.FwdSimpl (_, term) -> Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) - | TacticAst.Generalize (_,term,ident,pat) -> + | TacticAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in - Tactics.generalize ~term ~mk_fresh_name_callback:(namer_of names) pat + Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern | TacticAst.Goal (_, n) -> Tactics.set_goal n | TacticAst.IdTac _ -> Tactics.id | TacticAst.Injection (_,term) -> Tactics.injection term @@ -376,14 +376,18 @@ let disambiguate_obj status obj = in status, cic -let disambiguate_pattern aliases (hyp_paths ,goal_path) = - let interp path = Disambiguate.interpretate_path [] aliases path in - let goal_path = - match goal_path with - | None -> None - | Some path -> Some (interp path) in +let disambiguate_pattern status (wanted, hyp_paths, goal_path) = + let interp path = Disambiguate.interpretate_path [] status.aliases path in + let goal_path = interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in - (hyp_paths ,goal_path) + let status,wanted = + match wanted with + None -> status,None + | Some wanted -> + let status,wanted = disambiguate_term status wanted in + status, Some wanted + in + status, (wanted, hyp_paths ,goal_path) let disambiguate_tactic status = function | TacticAst.Apply (loc, term) -> @@ -394,11 +398,10 @@ let disambiguate_tactic status = function status, TacticAst.Absurd (loc, cic) | TacticAst.Assumption loc -> status, TacticAst.Assumption loc | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width) - | TacticAst.Change (loc, what, with_what, pattern) -> - let status, cic1 = disambiguate_term status what in - let status, cic2 = disambiguate_term status with_what in - let pattern = disambiguate_pattern status.aliases pattern in - status, TacticAst.Change (loc, cic1, cic2, pattern) + | TacticAst.Change (loc, pattern, with_what) -> + let status, with_what = disambiguate_term status with_what in + let status, pattern = disambiguate_pattern status pattern in + status, TacticAst.Change (loc, pattern, with_what) | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id) | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id) | TacticAst.Compare (loc,term) -> @@ -434,18 +437,16 @@ let disambiguate_tactic status = function status, TacticAst.ElimType (loc, cic) | TacticAst.Exists loc -> status, TacticAst.Exists loc | TacticAst.Fail loc -> status,TacticAst.Fail loc - | TacticAst.Fold (loc,reduction_kind, term, pattern) -> - let status, term = disambiguate_term status term in - let pattern = disambiguate_pattern status.aliases pattern in - status, TacticAst.Fold (loc,reduction_kind, term, pattern) + | TacticAst.Fold (loc,reduction_kind, pattern) -> + let status, pattern = disambiguate_pattern status pattern in + status, TacticAst.Fold (loc,reduction_kind, pattern) | TacticAst.FwdSimpl (loc, term) -> let status, term = disambiguate_term status term in status, TacticAst.FwdSimpl (loc, term) | TacticAst.Fourier loc -> status, TacticAst.Fourier loc - | TacticAst.Generalize (loc,term,ident,pattern) -> - let status,term = disambiguate_term status term in - let pattern = disambiguate_pattern status.aliases pattern in - status, TacticAst.Generalize(loc,term,ident,pattern) + | TacticAst.Generalize (loc,pattern,ident) -> + let status, pattern = disambiguate_pattern status pattern in + status, TacticAst.Generalize(loc,pattern,ident) | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) | TacticAst.IdTac loc -> status,TacticAst.IdTac loc | TacticAst.Injection (loc,term) -> @@ -468,16 +469,16 @@ let disambiguate_tactic status = function let status, term = disambiguate_term status term in status, TacticAst.LetIn (loc,term,name) | TacticAst.Reduce (loc, reduction_kind, pattern) -> - let pattern = disambiguate_pattern status.aliases pattern in + let status, pattern = disambiguate_pattern status pattern in status, TacticAst.Reduce(loc, reduction_kind, pattern) | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc | TacticAst.Replace (loc, pattern, with_what) -> - let pattern = disambiguate_pattern status.aliases pattern in + let status, pattern = disambiguate_pattern status pattern in let status, with_what = disambiguate_term status with_what in status, TacticAst.Replace (loc, pattern, with_what) | TacticAst.Rewrite (loc, dir, t, pattern) -> let status, term = disambiguate_term status t in - let pattern = disambiguate_pattern status.aliases pattern in + let status, pattern = disambiguate_pattern status pattern in status, TacticAst.Rewrite (loc, dir, term, pattern) | TacticAst.Right loc -> status, TacticAst.Right loc | TacticAst.Ring loc -> status, TacticAst.Ring loc