[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
matitaLog.cmo: matitaLog.cmi
matitaLog.cmx: matitaLog.cmi
matitaMathView.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \
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 \
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 \
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 \
matitaTypes.cmx: matitaLog.cmx
matitac.cmo: matitacLib.cmi
matitac.cmx: matitacLib.cmx
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
matitaDisambiguator.cmi: matitaTypes.cmo
matitaEngine.cmi: matitaTypes.cmo
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
| TacticAst.Assumption _ -> Tactics.assumption
| TacticAst.Auto (_,depth,width) ->
AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
| 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
| TacticAst.Clear (_,id) -> Tactics.clear id
| TacticAst.ClearBody (_,id) -> Tactics.clearbody id
| TacticAst.Contradiction _ -> Tactics.contradiction
| TacticAst.Exact (_, term) -> Tactics.exact term
| TacticAst.Exists _ -> Tactics.exists
| TacticAst.Fail _ -> Tactics.fail
| 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:[]
let reduction =
match reduction_kind with
| `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
| `Simpl -> ProofEngineReduction.simpl
| `Whd -> CicReduction.whd ~delta:false ~subst:[]
in
| `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.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
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
| TacticAst.Goal (_, n) -> Tactics.set_goal n
| TacticAst.IdTac _ -> Tactics.id
| TacticAst.Injection (_,term) -> Tactics.injection term
-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
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+ 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) ->
let disambiguate_tactic status = function
| TacticAst.Apply (loc, term) ->
status, TacticAst.Absurd (loc, cic)
| TacticAst.Assumption loc -> status, TacticAst.Assumption loc
| TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
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) ->
| TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
| TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
| TacticAst.Compare (loc,term) ->
status, TacticAst.ElimType (loc, cic)
| TacticAst.Exists loc -> status, TacticAst.Exists loc
| TacticAst.Fail loc -> status,TacticAst.Fail loc
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.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) ->
| TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
| TacticAst.IdTac loc -> status,TacticAst.IdTac loc
| TacticAst.Injection (loc,term) ->
let status, term = disambiguate_term status term in
status, TacticAst.LetIn (loc,term,name)
| TacticAst.Reduce (loc, reduction_kind, pattern) ->
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) ->
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 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
status, TacticAst.Rewrite (loc, dir, term, pattern)
| TacticAst.Right loc -> status, TacticAst.Right loc
| TacticAst.Ring loc -> status, TacticAst.Ring loc