| TacticAst.LetIn of 'term * 'ident
| TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
| TacticAst.Replace_pattern of 'term pattern * 'term
- | TacticAst.Rewrite of direction * 'term * 'ident option
*)
+ | TacticAst.Rewrite (_,dir,t,ident) ->
+ if dir = `Left then
+ EqualityTactics.rewrite_tac ~term:t
+ else
+ EqualityTactics.rewrite_back_tac ~term:t
| _ -> assert false
let eval_tactical status tac =
(DisambiguateTypes.Num instance)
(DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
-let eval status st =
- match st with
+let eval_executable status ex =
+ match ex with
| TacticAst.Tactical (_, tac) -> eval_tactical status tac
| TacticAst.Command (_, cmd) -> eval_command status cmd
| TacticAst.Macro (_, mac) ->
command_error (sprintf "The macro %s can't be in a script"
(TacticAstPp.pp_macro_cic mac))
+let eval_comment status c = status
+
+let eval status st =
+ match st with
+ | TacticAst.Executable (_,ex) -> eval_executable status ex
+ | TacticAst.Comment (_,c) -> eval_comment status c
+
let disambiguate_term status term =
let (aliases, metasenv, cic, _) =
match
| TacticAst.LetIn of 'term * 'ident
| TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
| TacticAst.Replace_pattern of 'term pattern * 'term
- | TacticAst.Rewrite of direction * 'term * 'ident option
*)
+ | TacticAst.Rewrite (loc,dir,t,ident) ->
+ let status, term = disambiguate_term status t in
+ status, TacticAst.Rewrite (loc,dir,term,ident)
| TacticAst.Intros (loc, num, names) ->
status, TacticAst.Intros (loc, num, names)
| TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
status, cmd
| TacticAst.Alias _ as x -> status, x
-let disambiguate_statement status statement =
- match statement with
+let disambiguate_executable status ex =
+ match ex with
| TacticAst.Tactical (loc, tac) ->
let status, tac = disambiguate_tactical status tac in
status, (TacticAst.Tactical (loc, tac))
command_error
(sprintf ("The engine is not allowed to disambiguate any macro, "^^
"in particular %s") (TacticAstPp.pp_macro_ast mac))
+
+let disambiguate_comment status c =
+ match c with
+ | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
+ | TacticAst.Code (loc,ex) ->
+ let status, ex = disambiguate_executable status ex in
+ status, TacticAst.Code (loc,ex)
+
+let disambiguate_statement status statement =
+ match statement with
+ | TacticAst.Comment (loc,c) ->
+ let status, c = disambiguate_comment status c in
+ status, TacticAst.Comment (loc,c)
+ | TacticAst.Executable (loc,ex) ->
+ let status, ex = disambiguate_executable status ex in
+ status, TacticAst.Executable (loc,ex)
let eval_ast status ast =
let status,st = disambiguate_statement status ast in