avoid fixing non-recursive terms

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

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9b454f29429647d6a4bb6202ae6e4a6b7357d382..98bfef9d6f5c60a6b445e2c2feb400032e1955f6 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -470,16 +470,22 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
   GrafiteAst.Coercion
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
+let basic_eval_unification_hint (t,n) status =
+ let hstatus =
+  NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
+ in
+  { status with NRstatus.uhint_db = hstatus }
+;;
+
+let inject_unification_hint =
+ NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
+;;
+
 let eval_unification_hint status t n = 
- let aux status =
-  let hstatus =
-   NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
-  in
-   { status with NRstatus.uhint_db = hstatus } in
- let rstatus = aux (GrafiteTypes.get_rstatus status) in
+ let rstatus =
+  basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in
  let status = GrafiteTypes.set_rstatus rstatus status in
- let dump = GrafiteTypes.get_dump status in
- let dump = fun status -> aux (dump status) in
+ let dump = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in
  let status = GrafiteTypes.set_dump dump status in
   status,`Old []
 ;;
@@ -736,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      let status = eval_from_moo.efm_go status moopath in
      let rstatus = GrafiteTypes.get_rstatus status in
      let rstatus =
-      NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in
+      NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus
+     in
      let status = GrafiteTypes.set_rstatus rstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
@@ -795,6 +802,24 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
                NCicUntrusted.map_obj_kind 
                 (NCicUntrusted.apply_subst subst []) obj_kind in
               let height = NCicTypeChecker.height_of_obj_kind uri obj_kind in
+              (* fix the height inside the object *)
+              let rec fix () = function 
+                | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
+                   NCic.Const (NReference.reference_of_spec u
+                    (match spec with
+                    | NReference.Def _ -> NReference.Def height
+                    | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
+                    | NReference.CoFix _ -> NReference.CoFix height
+                    | NReference.Ind _ | NReference.Con _
+                    | NReference.Decl as s -> s))
+                | t -> NCicUtils.map (fun _ () -> ()) () fix t
+              in
+              let obj_kind = 
+                match obj_kind with
+                | NCic.Fixpoint _ -> 
+                    NCicUntrusted.map_obj_kind (fix ()) obj_kind 
+                | _ -> obj_kind
+              in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
                let timestamp = NCicLibrary.add_obj uri obj in