| TacticAst.Reflexivity _ -> Tactics.reflexivity
| TacticAst.Assumption _ -> Tactics.assumption
| TacticAst.Contradiction _ -> Tactics.contradiction
+ | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
| TacticAst.Exists _ -> Tactics.exists
| TacticAst.Fourier _ -> Tactics.fourier
+ | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
| TacticAst.Goal (_, n) -> Tactics.set_goal n
| TacticAst.Left _ -> Tactics.left
| TacticAst.Right _ -> Tactics.right
| TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
| TacticAst.Change of 'term * 'term * 'ident option
| TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
| TacticAst.Fold of reduction_kind * 'term
| TacticAst.Injection of 'ident
| TacticAst.Replace_pattern of 'term pattern * 'term
*)
| TacticAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
- ProofEngineTypes.mk_tactic
- (fun (((_,metasenv,_,_),goal) as status) ->
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let where, also_in_hypotheses =
- if ident = "goal" then
- ty, false
- else
- let hyp =
- try
- List.find (function
- | Some (Cic.Name name,entry) when name = ident -> true
- | _ -> false)
- context
- with
- Not_found ->
- raise (ProofEngineTypes.Fail
- (ident ^ " is not an hypothesis"))
- in
- (match hyp with
- | Some (_, Cic.Decl term) -> term
- | Some (_, Cic.Def (term,ty)) -> term
- | None -> assert false),true
- in
- let pointers = CicUtil.select ~term:where ~context:path in
- (match reduction_kind with
- | `Normalize ->
- ProofEngineTypes.apply_tactic
- (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Reduce ->
- ProofEngineTypes.apply_tactic
- (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Simpl ->
- ProofEngineTypes.apply_tactic
- (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Whd ->
- ProofEngineTypes.apply_tactic
- (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
- status))
- | TacticAst.Reduce (_,reduction_kind,opts) ->
- let terms, also_in_hypotheses =
- match opts with
- | Some (l,`Goal) -> Some l, false
- | Some (l,`Everywhere) -> Some l, true
- | None -> None, false
- in
+ | TacticAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
- | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
- | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
- | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
- | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
- | TacticAst.Rewrite (_,dir,t,ident) ->
+ | `Normalize -> Tactics.normalize ~pattern
+ | `Reduce -> Tactics.reduce ~pattern
+ | `Simpl -> Tactics.simpl ~pattern
+ | `Whd -> Tactics.whd ~pattern)
+ | TacticAst.Rewrite (_, dir, t, pattern) ->
if dir = `Left then
- EqualityTactics.rewrite_tac ~term:t
+ EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
else
- EqualityTactics.rewrite_back_tac ~term:t
- | TacticAst.FwdSimpl (_, name) ->
- Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ())
- | TacticAst.LApply (_, term, substs) ->
- let f (name, term) = Cic.Name name, term in
- Tactics.lapply ~substs:(List.map f substs) term
- | _ -> assert false
+ EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
+ | TacticAst.FwdSimpl (_, term) ->
+ Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+ | TacticAst.LApply (_, to_what, what) ->
+ Tactics.lapply ?to_what what
let eval_tactical status tac =
let apply_tactic tactic =
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 hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
+ (hyp_paths ,goal_path)
+
let disambiguate_tactic status = function
| TacticAst.Transitivity (loc, term) ->
let status, cic = disambiguate_term status term in
let status, cic1 = disambiguate_term status what in
let status, cic2 = disambiguate_term status with_what in
status, TacticAst.Replace (loc, cic1, cic2)
- | TacticAst.Change (loc, what, with_what, ident) ->
+ | TacticAst.Change (loc, what, with_what, pattern) ->
let status, cic1 = disambiguate_term status what in
let status, cic2 = disambiguate_term status with_what in
- status, TacticAst.Change (loc, cic1, cic2, ident)
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Change (loc, cic1, cic2, pattern)
+ | TacticAst.Generalize (loc,term,pattern) ->
+ let status,term = disambiguate_term status term in
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Generalize(loc,term,pattern)
+ | TacticAst.Discriminate (loc,term) ->
+ let status,term = disambiguate_term status term in
+ status, TacticAst.Discriminate(loc,term)
(*
(* TODO Zack a lot more of tactics to be implemented here ... *)
| TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
| TacticAst.Change of 'term * 'term * 'ident option
| TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
| TacticAst.Fold of reduction_kind * 'term
| TacticAst.Injection of 'ident
| TacticAst.Replace_pattern of 'term pattern * 'term
*)
- | TacticAst.LetIn (loc,term,name) ->
+ | TacticAst.LetIn (loc, term, name) ->
let status, term = disambiguate_term status term in
status, TacticAst.LetIn (loc,term,name)
- | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
- let path = Disambiguate.interpretate_path [] status.aliases path in
- status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
- | TacticAst.Reduce (loc, reduction_kind, opts) ->
- let status, opts =
- match opts with
- | None -> status, None
- | Some (l,pat) ->
- let status, l =
- List.fold_right (fun t (status,acc) ->
- let status',t' = disambiguate_term status t in
- status', t'::acc)
- l (status,[])
- in
- status, Some (l, pat)
- in
- status, TacticAst.Reduce (loc, reduction_kind, opts)
- | TacticAst.Rewrite (loc,dir,t,ident) ->
+ | TacticAst.Reduce (loc, reduction_kind, pattern) ->
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Reduce(loc, reduction_kind, pattern)
+ | TacticAst.Rewrite (loc, dir, t, pattern) ->
let status, term = disambiguate_term status t in
- status, TacticAst.Rewrite (loc,dir,term,ident)
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Rewrite (loc, dir, term, pattern)
| TacticAst.Intros (loc, num, names) ->
status, TacticAst.Intros (loc, num, names)
| TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
| TacticAst.Split loc -> status, TacticAst.Split loc
| TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
| TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
- | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name)
- | TacticAst.LApply (loc, term, substs) ->
- let f (status, substs) (name, term) =
- let status, term = disambiguate_term status term in
- status, (name, term) :: substs
- in
+ | TacticAst.FwdSimpl (loc, term) ->
let status, term = disambiguate_term status term in
- let status, substs = List.fold_left f (status, []) substs in
- status, TacticAst.LApply (loc, term, substs)
-
- | x ->
- print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
- assert false
+ status, TacticAst.FwdSimpl (loc, term)
+ | TacticAst.LApply (loc, Some to_what, what) ->
+ let status, to_what = disambiguate_term status to_what in
+ let status, what = disambiguate_term status what in
+ status, TacticAst.LApply (loc, Some to_what, what)
+ | TacticAst.LApply (loc, None, what) ->
+ let status, what = disambiguate_term status what in
+ status, TacticAst.LApply (loc, None, what)
let rec disambiguate_tactical status = function
| TacticAst.Tactic (loc, tactic) ->
projects / helm.git / blobdiff