X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=c2db06efaeee6b5a708caecd5735a9eace2a94d9;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=1d23ac063709e3fe57265c86f57a95ae56bcb1e4;hpb=2d03016df7f68c81dd0f25bf18a792a80b412702;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 1d23ac063..c2db06efa 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -97,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
@@ -125,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) ->
@@ -171,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) ->
@@ -233,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
@@ -262,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
@@ -504,17 +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 -> raise (UnableToInclude 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 =
@@ -582,6 +598,8 @@ let eval_command opts status cmd =
       eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let aliases =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in DisambiguatePp *)
       match spec with
       | GrafiteAst.Ident_alias (id,uri) -> 
          DisambiguateTypes.Environment.add