From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 10:12:25 +0000 (+0000)
Subject: added get_obj in nCicEnvironment that returns an object and a boolean stating
X-Git-Tag: make_still_working~5456
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76ab642ba92a6775d6421698f3caaf2e40cebcd3;p=helm.git

added get_obj in nCicEnvironment that returns an object and a boolean stating
if the object is checked or not (to be used by the typechecker, function
type_of_constant
---

diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index d28300802..12dc298e7 100644
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -21,10 +21,12 @@ nCicEnvironment.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCic.cmo \
     nCicEnvironment.cmi 
 nCicEnvironment.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCic.cmx \
     nCicEnvironment.cmi 
-nCicTypeChecker.cmo: nCicUtils.cmi nCicSubstitution.cmi nCicReduction.cmi \
-    nCicPp.cmi nCic.cmo nCicTypeChecker.cmi 
-nCicTypeChecker.cmx: nCicUtils.cmx nCicSubstitution.cmx nCicReduction.cmx \
-    nCicPp.cmx nCic.cmx nCicTypeChecker.cmi 
+nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \
+    nCicSubstitution.cmi nCicReduction.cmi nCicPp.cmi nCicEnvironment.cmi \
+    nCic.cmo nCicTypeChecker.cmi 
+nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \
+    nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \
+    nCic.cmx nCicTypeChecker.cmi 
 oCicTypeChecker.cmo: oCic2NCic.cmi nCicTypeChecker.cmi oCicTypeChecker.cmi 
 oCicTypeChecker.cmx: oCic2NCic.cmx nCicTypeChecker.cmx oCicTypeChecker.cmi 
 nCicUtils.cmo: nCic.cmo nCicUtils.cmi 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 4a6a21d9d..79014def5 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -5,14 +5,25 @@ let get_checked_obj u =
   with Not_found ->
     let ouri = NUri.ouri_of_nuri u in
     let o,_ = 
-      CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph 
-        ouri in
+      CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri 
+    in
     (* FIX: add all objects to the environment and give back the last one *)
     let no = HExtlib.list_last (OCic2NCic.convert_obj ouri o) in
     NUri.UriHash.add cache u no;
     no
 ;;
 
+let get_obj u =
+  try true, NUri.UriHash.find cache u
+  with Not_found ->
+    (* in th final implementation should get it from disk *)
+    let ouri = NUri.ouri_of_nuri u in
+    let o,_ = 
+      CicEnvironment.get_cooked_obj ~trust:false CicUniv.oblivion_ugraph ouri 
+    in
+    false, HExtlib.list_last (OCic2NCic.convert_obj ouri o)
+;;
+
 let get_checked_def = function
   | NReference.Ref (_, uri, NReference.Def) ->
       (match get_checked_obj uri with
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 53e6a6ffe..0984ea23f 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -27,6 +27,7 @@
  * functions strictly necessary to the typechecking algorithm *)
 
 val get_checked_obj: NUri.uri -> NCic.obj
+val get_obj: NUri.uri -> bool * NCic.obj
 
 val get_checked_def:
   NReference.reference ->