Bug fixed: the debrujinate function (hence the one to compute objects height)

[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 5f64b1b0a91384c9fb77b7e34f1db2ccf30357c5..eb994854f49c6d0e648aa7c4fa916aad18a38b63 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -475,7 +475,10 @@ let basic_eval_unification_hint (t,n) status =
 ;;
 
 let inject_unification_hint =
- let basic_eval_unification_hint (t,n) ~refresh_uri_in_term =
+ let basic_eval_unification_hint (t,n) 
+   ~refresh_uri_in_universe 
+   ~refresh_uri_in_term
+ =
   let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n)
  in
   NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint
@@ -488,6 +491,29 @@ let eval_unification_hint status t n =
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = basic_eval_unification_hint (t,n) status in
  let dump = inject_unification_hint (t,n)::status#dump in
+ let status = status#set_dump dump in
+  status,`New []
+;;
+
+let basic_eval_add_constraint (s,u1,u2) status =
+ NCicLibrary.add_constraint status s u1 u2
+;;
+
+let inject_constraint =
+ let basic_eval_add_constraint (s,u1,u2) 
+       ~refresh_uri_in_universe 
+       ~refresh_uri_in_term
+ =
+  let u1 = refresh_uri_in_universe u1 in 
+  let u2 = refresh_uri_in_universe u2 in 
+  basic_eval_add_constraint (s,u1,u2)
+ in
+  NRstatus.Serializer.register "constraints" basic_eval_add_constraint
+;;
+
+let eval_add_constraint status s u1 u2 = 
+ let status = basic_eval_add_constraint (s,u1,u2) status in
+ let dump = inject_constraint (s,u1,u2)::status#dump in
  let status = status#set_dump dump in
   status,`Old []
 ;;
@@ -679,7 +705,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj_kind =
          NCicUntrusted.map_obj_kind 
           (NCicUntrusted.apply_subst subst []) obj_kind in
-        let height = NCicTypeChecker.height_of_obj_kind uri 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 -> 
@@ -699,14 +725,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           | _ -> obj_kind
         in
         let obj = uri,height,[],[],obj_kind in
-         NCicTypeChecker.typecheck_obj obj;
-         let status = NCicLibrary.add_obj status uri obj in
+         let status = NCicLibrary.add_obj status obj in
          let objs = NCicElim.mk_elims obj in
          let timestamp,uris_rev =
            List.fold_left
             (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
-              NCicTypeChecker.typecheck_obj obj;
-              let status = NCicLibrary.add_obj status uri obj in
+              let status = NCicLibrary.add_obj status obj in
                status,uri::uris_rev
             ) (status,[]) objs in
          let uris = uri::List.rev uris_rev in
@@ -729,8 +753,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
   | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) ->
-      NCicEnvironment.add_constraint strict [false,u1] [false,u2];
-      status, `New [u1;u2]
+      eval_add_constraint status strict [false,u1] [false,u2]
 ;;
 
 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
@@ -797,24 +820,32 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      LibraryObjects.set_default what uris;
      GrafiteTypes.add_moo_content [cmd] status,`Old []
   | GrafiteAst.Drop loc -> raise Drop
-  | GrafiteAst.Include (loc, _, baseuri) ->
-     let moopath_rw, moopath_r = 
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:true,
-       LibraryMisc.obj_file_of_baseuri 
-         ~must_exist:false ~baseuri ~writable:false
-     in
-     let moopath = 
-       if Sys.file_exists moopath_r then moopath_r else
-         if Sys.file_exists moopath_rw then moopath_rw else
-           raise (IncludedFileNotCompiled (moopath_rw,baseuri))
-     in
-     let status = eval_from_moo.efm_go status moopath in
+  | GrafiteAst.Include (loc, mode, new_or_old, baseuri) ->
+     (* Old Include command is not recursive; new one is *)
      let status =
-       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
-        status
+      if new_or_old = `OldAndNew then
+       let moopath_rw, moopath_r = 
+        LibraryMisc.obj_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:true,
+        LibraryMisc.obj_file_of_baseuri 
+          ~must_exist:false ~baseuri ~writable:false in
+       let moopath = 
+        if Sys.file_exists moopath_r then moopath_r else
+          if Sys.file_exists moopath_rw then moopath_rw else
+            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
+       in
+        eval_from_moo.efm_go status moopath
+      else
+       status
      in
-      status,`Old []
+      let status =
+       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+        status in
+      let status =
+       GrafiteTypes.add_moo_content
+        [GrafiteAst.Include (loc,mode,`New,baseuri)] status
+      in
+       status,`Old []
   | GrafiteAst.Print (_,"proofterm") ->
       let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
       prerr_endline (Auto.pp_proofterm (Lazy.force p));