bugfix to developments:

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index ff173bc37aa1d717ed3b7e32f69d26043b5a9b42..ad5423b3e77097bbf9f603d2bcf05bcad15b94af 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -28,7 +28,8 @@
 open Printf
 
 exception Drop
-exception IncludedFileNotCompiled of string (* file name *)
+(* mo file name, ma file name *)
+exception IncludedFileNotCompiled of string * string 
 exception Macro of
  GrafiteAst.loc *
   (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
@@ -60,10 +61,11 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyS (_, term) ->
+     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
-      AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
-        ~dbd:(LibraryDb.instance ()) ()
+  | GrafiteAst.Auto (_,params) ->
+      AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -81,7 +83,8 @@ let tactic_of_ast ast =
       let user_types = List.rev_map to_type types in
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+  | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -95,8 +98,6 @@ let tactic_of_ast ast =
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
       let reduction =
         match reduction_kind with
-        | `Demodulate -> 
-            GrafiteTypes.command_error "demodulation can't be folded"
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
@@ -129,16 +130,15 @@ let tactic_of_ast ast =
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
-  | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+  | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
-        ~to_what what
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+        ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
-        | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
         | `Normalize -> Tactics.normalize ~pattern
         | `Reduce -> Tactics.reduce ~pattern  
         | `Simpl -> Tactics.simpl ~pattern 
@@ -582,7 +582,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      let moopath = 
        if Sys.file_exists moopath_r then moopath_r else
          if Sys.file_exists moopath_rw then moopath_rw else
-           raise (IncludedFileNotCompiled moopath_rw)
+           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      let status = eval_from_moo.efm_go status moopath in
      status,[]