* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
exception Drop
exception IncludedFileNotCompiled of string (* file name *)
+exception Macro of
+ GrafiteAst.loc *
+ (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
type options = {
do_heavy_checks: bool ;
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
?do_heavy_checks:bool ->
?clean_baseuri:bool ->
GrafiteTypes.status ->
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
options ->
GrafiteTypes.status ->
('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code ->
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
| _ -> status,uris
-} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status ex ->
match ex with
| GrafiteAst.Tactical (_, tac, None) ->
eval_tactical ~disambiguate_tactic status tac,[]
eval_tactical ~disambiguate_tactic status punct,[]
| GrafiteAst.Command (_, cmd) ->
eval_command.ec_go ~disambiguate_command opts status cmd
- | GrafiteAst.Macro (_, mac) ->
-(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
- raise (Command_error
- (Printf.sprintf "The macro %s can't be in a script"
- (GrafiteAstPp.pp_macro_ast mac)))
-*) assert false
+ | GrafiteAst.Macro (loc, macro) ->
+ raise (Macro (loc,disambiguate_macro status macro))
} and eval_from_moo = {efm_go = fun status fname ->
let ast_of_cmd cmd =
eval_ast.ea_go
~disambiguate_tactic:(fun status _ tactic -> status,tactic)
~disambiguate_command:(fun status cmd -> status,cmd)
+ ~disambiguate_macro:(fun _ _ -> assert false)
status ast
in
assert (lemmas=[]);
status)
status moo
-} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
- st
+} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status st
->
let opts = {
do_heavy_checks = do_heavy_checks ;
in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~disambiguate_tactic
- ~disambiguate_command opts status ex
+ eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
+ ~disambiguate_macro opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c,[]
}