1. Macros are now handled using an execption that is caught by matitacLib

[helm.git] / helm / ocaml / grafite_engine / grafiteEngine.ml

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml
index c820986b39f47e2a6fce588ada47db8d35d2bd02..a035a68e1214983caa90b34e9dabb7f58f9bb44f 100644 (file)
--- a/helm/ocaml/grafite_engine/grafiteEngine.ml
+++ b/helm/ocaml/grafite_engine/grafiteEngine.ml
@@ -25,6 +25,9 @@
 
 exception Drop
 exception IncludedFileNotCompiled of string (* file name *)
+(* the integer is expected to be the goal the user is currently seeing *)
+exception Macro of
+ GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
 
 type options = { 
   do_heavy_checks: bool ; 
@@ -330,6 +333,11 @@ type eval_ast =
     'obj GrafiteAst.command ->
     GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
+  disambiguate_macro:
+   (GrafiteTypes.status ->
+    'term GrafiteAst.macro ->
+    int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
   ?do_heavy_checks:bool ->
   ?clean_baseuri:bool ->
   GrafiteTypes.status ->
@@ -361,6 +369,11 @@ type 'a eval_executable =
     'obj GrafiteAst.command ->
     GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
 
+  disambiguate_macro:
+   (GrafiteTypes.status ->
+    'term GrafiteAst.macro ->
+    int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
   options ->
   GrafiteTypes.status ->
   ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code ->
@@ -648,7 +661,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
       {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,[]
@@ -657,12 +670,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
       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 =
@@ -678,13 +687,13 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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 ; 
@@ -692,8 +701,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
   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,[]
 }