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 d28300802e3ee280b242a8d5ae091ba76bd30ba9..12dc298e78260861fbc93a9c82d1777a444cce69 100644 (file)
--- 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 4a6a21d9da0a92a648927404e58f4cb4572457ac..79014def5ef29866317569197dba712875688276 100644 (file)
--- 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 53e6a6ffe5ecf54d72b62adfea1c2a97b409da9c..0984ea23f94e3a606121ced1ec669e2118517384 100644 (file)
--- 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 ->