X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=24872ffd0c408ceffdb163eb58499baa125946c8;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=3d738e1b9b74e62f2c7f21155dc56a19a96263cc;hpb=3e86f296f53e98401b281ce96fc7ba545dbd05b4;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3d738e1b9..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
@@ -501,21 +517,20 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, GrafiteAst.Obj (loc,obj)
 
-let try_open_in paths path =
-  let rec aux = function
-  | [] -> open_in path
-  | p :: tl ->
-      try
-        open_in (p ^ "/" ^ path)
-      with Sys_error _ -> aux tl
-  in
-  try
-    aux paths
-  with Sys_error _ as exc ->
-    MatitaLog.error ("Unable to read " ^ path);
-    MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
-    MatitaLog.error ("current working directory is " ^ Unix.getcwd ());
-    raise exc
+let make_absolute paths path =
+  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 =
@@ -530,14 +545,15 @@ let eval_command opts status cmd =
      {status with moo_content_rev =
         (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | GrafiteAst.Include (loc, path) ->
-     let path = MatitaMisc.obj_file_of_script path in
-     let stream = 
-       try
-         Stream.of_channel (try_open_in opts.include_paths path) 
-       with Sys_error _ -> raise (UnableToInclude path)
-     in
+     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 (IncludedFileNotCompiled moopath) in
+     let stream = Stream.of_channel ic in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());
+      close_in ic;
       !status
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
@@ -550,7 +566,7 @@ let eval_command opts status cmd =
         else
           value
       in
-      if not (MatitacleanLib.is_empty value) then
+      if not (MatitaMisc.is_empty value) then
         begin
           MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
           if opts.clean_baseuri then
@@ -627,6 +643,12 @@ let eval_command opts status cmd =
            begin
              let dbd = MatitaDb.instance () in
              let similar = MetadataQuery.match_term ~dbd ty in
+             let similar_len = List.length similar in
+             if similar_len> 30 then
+               (MatitaLog.message
+                 ("Duplicate check will compare your theorem with " ^ 
+                   string_of_int similar_len ^ 
+                   " theorems, this may take a while."));
              let convertible =
                List.filter (
                  fun u ->