X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=24872ffd0c408ceffdb163eb58499baa125946c8;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=767182bc196e60bfd635ba8f64a56e86d86f2db2;hpb=29657d5f10bd3796ba8f2cc1add48de8a02c1466;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 767182bc1..24872ffd0 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -27,7 +27,8 @@ open Printf
 open MatitaTypes
 
 exception Drop;;
-exception UnableToInclude of string;;
+exception UnableToInclude of string
+exception IncludedFileNotCompiled of string
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -59,8 +60,9 @@ let tactic_of_ast = function
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width) -> 
-      AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
+  | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *)
+      AutoTactic.auto_tac ?depth ?width ?paramodulation
+        ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -95,6 +97,7 @@ let tactic_of_ast = function
        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
        | `Reduce -> ProofEngineReduction.reduce
        | `Simpl -> ProofEngineReduction.simpl
+       | `Unfold what -> ProofEngineReduction.unfold ?what
        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
      in
       Tactics.fold ~reduction ~term ~pattern
@@ -123,6 +126,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
+      | `Unfold what -> Tactics.unfold ~pattern what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->
@@ -169,6 +173,16 @@ let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
         status, Some wanted
   in
    status, (wanted, hyp_paths ,goal_path)
+
+let disambiguate_reduction_kind status = function
+  | `Unfold (Some t) ->
+      let status, t = disambiguate_term status t in
+      status, `Unfold (Some t)
+  | `Normalize
+  | `Reduce
+  | `Simpl
+  | `Unfold None
+  | `Whd as kind -> status, kind
   
 let disambiguate_tactic status = function
   | GrafiteAst.Apply (loc, term) ->
@@ -178,7 +192,7 @@ let disambiguate_tactic status = function
       let status, cic = disambiguate_term status term in
       status, GrafiteAst.Absurd (loc, cic)
   | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
-  | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width)
+  | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
   | GrafiteAst.Change (loc, pattern, with_what) -> 
       let status, with_what = disambiguate_term status with_what in
       let status, pattern = disambiguate_pattern status pattern in
@@ -231,10 +245,11 @@ let disambiguate_tactic status = function
       status, GrafiteAst.ElimType (loc, what, None, depth, idents)
   | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc 
   | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
-  | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
+  | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
      let status, pattern = disambiguate_pattern status pattern in
      let status, term = disambiguate_term status term in
-     status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
+     let status, red_kind = disambiguate_reduction_kind status red_kind in
+     status, GrafiteAst.Fold (loc,red_kind, term, pattern)
   | GrafiteAst.FwdSimpl (loc, hyp, names) ->
      status, GrafiteAst.FwdSimpl (loc, hyp, names)  
   | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
@@ -260,9 +275,10 @@ let disambiguate_tactic status = function
   | GrafiteAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in
       status, GrafiteAst.LetIn (loc,term,name)
-  | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
+  | GrafiteAst.Reduce (loc, red_kind, pattern) ->
       let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
+      let status, red_kind = disambiguate_reduction_kind status red_kind in
+      status, GrafiteAst.Reduce(loc, red_kind, pattern)
   | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
   | GrafiteAst.Replace (loc, pattern, with_what) -> 
       let status, pattern = disambiguate_pattern status pattern in
@@ -502,18 +518,19 @@ let disambiguate_command status = function
        status, GrafiteAst.Obj (loc,obj)
 
 let make_absolute paths path =
-  let rec aux = function
-  | [] -> ignore (Unix.stat path); path
-  | p :: tl ->
-     let path = p ^ "/" ^ path in
-      try
-        ignore (Unix.stat path); path
-      with Unix.Unix_error _ -> aux tl
-  in
-  try
-    aux paths
-  with Unix.Unix_error _ as exc ->
-    command_error ("File " ^ path ^ " not found")
+  if path = "coq.ma" then path
+  else
+   let rec aux = function
+   | [] -> ignore (Unix.stat path); path
+   | p :: tl ->
+      let path = p ^ "/" ^ path in
+       try
+         ignore (Unix.stat path); path
+       with Unix.Unix_error _ -> aux tl
+   in
+   try
+     aux paths
+   with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =
@@ -531,7 +548,8 @@ let eval_command opts status cmd =
      let absolute_path = make_absolute opts.include_paths path in
      let moopath = MatitaMisc.obj_file_of_script absolute_path in
      let ic =
-      try open_in moopath with Sys_error _ -> raise (UnableToInclude moopath) in
+      try open_in moopath with Sys_error _ -> 
+        raise (IncludedFileNotCompiled moopath) in
      let stream = Stream.of_channel ic in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());