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 afd46f5004c5e191411e89e48c7ae458dc9690a1..74f6624138cbbc0e90db193f03712c0aad110001 100644 (file)
--- 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 222ca491b9745b80eed476b5274b62f3941d2e08..a28cdedf85ac214b3d56b854bb82ce454be9b19b 100644 (file)
--- 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