first snapshot of separate compilation

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a28cdedf85ac214b3d56b854bb82ce454be9b19b..852608d5147d5a5cea305e2c7defdd9c42b86758 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -46,7 +46,7 @@ let tactic_of_ast = function
   | TacticAst.Exact (_, term) -> Tactics.exact term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fail _ -> Tactics.fail
-  | TacticAst.Fold (_, reduction_kind, pattern) ->
+  | TacticAst.Fold (_, reduction_kind, term, pattern) ->
      let reduction =
       match reduction_kind with
        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
@@ -54,10 +54,10 @@ let tactic_of_ast = function
        | `Simpl -> ProofEngineReduction.simpl
        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
      in
-      Tactics.fold ~reduction ~pattern
+      Tactics.fold ~reduction ~term ~pattern
   | TacticAst.Fourier _ -> Tactics.fourier
-  | TacticAst.FwdSimpl (_, term) -> 
-     Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+  | TacticAst.FwdSimpl (_, hyp, names) -> 
+     Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
   | TacticAst.Generalize (_,pattern,ident) ->
      let names = match ident with None -> [] | Some id -> [id] in
      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
@@ -69,9 +69,9 @@ let tactic_of_ast = function
   | TacticAst.Intros (_, Some num, names) ->
       PrimitiveTactics.intros_tac ~howmany:num
         ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.LApply (_, to_what, what, ident) ->
+  | TacticAst.LApply (_, 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) ?to_what what
+     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -84,11 +84,8 @@ let tactic_of_ast = function
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Replace (_, pattern, with_what) ->
      Tactics.replace ~pattern ~with_what
-  | TacticAst.Rewrite (_, dir, t, pattern) ->
-      if dir = `Left then
-        EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
-      else
-        EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
+  | TacticAst.Rewrite (_, direction, t, pattern) ->
+     EqualityTactics.rewrite_tac ~direction ~pattern t
   | TacticAst.Right _ -> Tactics.right
   | TacticAst.Ring _ -> Tactics.ring
   | TacticAst.Split _ -> Tactics.split
@@ -224,7 +221,14 @@ let generate_projections uri fields status =
  
 let eval_command status cmd =
   match cmd with
-  | TacticAst.Set (loc, name, value) -> set_option status name value
+  | TacticAst.Set (loc, name, value) -> 
+      let value = 
+        if name = "baseuri" then
+          MatitaMisc.strip_trailing_slash value
+        else
+          value
+      in
+      set_option status name value
   | TacticAst.Drop loc -> raise Drop
   | TacticAst.Qed loc ->
       let uri, metasenv, bo, ty = 
@@ -437,12 +441,12 @@ let disambiguate_tactic status = function
       status, TacticAst.ElimType (loc, cic)
   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
   | TacticAst.Fail loc -> status,TacticAst.Fail loc
-  | TacticAst.Fold (loc,reduction_kind, pattern) ->
+  | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
      let status, pattern = disambiguate_pattern status pattern in
-     status, TacticAst.Fold (loc,reduction_kind, pattern)
-  | TacticAst.FwdSimpl (loc, term) ->
      let status, term = disambiguate_term status term in
-     status, TacticAst.FwdSimpl (loc, term)  
+     status, TacticAst.Fold (loc,reduction_kind, term, pattern)
+  | TacticAst.FwdSimpl (loc, hyp, names) ->
+     status, TacticAst.FwdSimpl (loc, hyp, names)  
   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
   | TacticAst.Generalize (loc,pattern,ident) ->
       let status, pattern = disambiguate_pattern status pattern in
@@ -454,16 +458,14 @@ let disambiguate_tactic status = function
       status, TacticAst.Injection (loc,term)
   | TacticAst.Intros (loc, num, names) ->
       status, TacticAst.Intros (loc, num, names)
-  | TacticAst.LApply (loc, to_what, what, ident) ->
-     let status, to_what =
-      match to_what with
-         None -> status,None
-       | Some to_what -> 
-           let status, to_what = disambiguate_term status to_what in
-           status, Some to_what
+  | TacticAst.LApply (loc, depth, to_what, what, ident) ->
+     let f term (status, to_what) =
+        let status, term = disambiguate_term status term in
+        status, term :: to_what
      in
+     let status, to_what = List.fold_right f to_what (status, []) in 
      let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, to_what, what, ident)
+     status, TacticAst.LApply (loc, depth, to_what, what, ident)
   | TacticAst.Left loc -> status, TacticAst.Left loc
   | TacticAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in