Initial implementation of statuses using objects in place of nested records.

[helm.git] / helm / software / components / ng_disambiguation / nCicDisambiguate.ml

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index f0a3fa0eb7386ba9747243c4050d718ed2ffeea7..5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da 100644 (file)
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -34,7 +34,7 @@ let rec mk_rels howmany from =
 ;;
 
 let refine_term 
- metasenv subst context uri ~coercion_db ~use_coercions term expty _ ~localization_tbl=
+ metasenv subst context uri ~rdb ~use_coercions term expty _ ~localization_tbl=
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
     (NCicPp.ppterm ~metasenv ~subst ~context term)));
@@ -46,12 +46,9 @@ let refine_term
         (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
-      NCicRefiner.typeof
-        (NCicUnifHint.db ())
-        ~look_for_coercion:(
-          if use_coercions then 
-           NCicCoercion.look_for_coercion coercion_db
-          else (fun _ _ _ _ _ -> []))
+      NCicRefiner.typeof 
+        (rdb#set_coerc_db 
+          (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
         metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
@@ -67,7 +64,7 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~coercion_db metasenv subst context _uri 
+  ~rdb metasenv subst context _uri 
   ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
@@ -81,11 +78,9 @@ let refine_obj
   try
     let obj =
       NCicRefiner.typeof_obj
-        (NCicUnifHint.db ())
-        ~look_for_coercion:(
-          if use_coercions then 
-           NCicCoercion.look_for_coercion coercion_db
-          else (fun _ _ _ _ _ -> []))
+        (rdb#set_coerc_db
+           (if use_coercions then rdb#coerc_db 
+            else NCicCoercion.empty_db))
         obj ~localise 
     in
       Disambiguate.Ok (obj, [], [], ())
@@ -312,21 +307,23 @@ let interpretate_term_and_interpretate_term_option
         NCic.LetIn (cic_name, cic_typ, cic_def, cic_body)
     | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
     | CicNotationPt.Ident (name, subst) ->
        assert (subst = None);
        (try
-         NCic.Rel (find_in_context name context)
+             NCic.Rel (find_in_context name context)
        with Not_found -> 
          try NCic.Const (List.assoc name obj_context)
          with Not_found ->
            Disambiguate.resolve ~env ~mk_choice (Id name) (`Args []))
-    | CicNotationPt.Uri (name, subst) ->
+    | CicNotationPt.Uri (uri, subst) ->
        assert (subst = None);
        (try
-         NCic.Const (NRef.reference_of_string name)
+         NCic.Const (OCic2NCic.reference_of_oxuri(UriManager.uri_of_string uri))
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
+    | CicNotationPt.NRef nref -> NCic.Const nref
     | CicNotationPt.Implicit -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
@@ -342,11 +339,13 @@ let interpretate_term_and_interpretate_term_option
     | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
     | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/Type.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/Type0.univ"])
     | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type
        [false,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
+    | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
+       [false,NUri.uri_of_string ("cic:/matita/pts/CProp" ^ s ^ ".univ")])
     | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type
-       [false,NUri.uri_of_string "cic:/matita/pts/CProp.univ"])
+       [false,NUri.uri_of_string "cic:/matita/pts/CProp0.univ"])
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~env ~mk_choice 
          (Symbol (symbol, instance)) (`Args [])
@@ -603,7 +602,7 @@ let interpretate_obj
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
    ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library 
+   ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -617,7 +616,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
-     ~refine_thing:(refine_term ~coercion_db) (text,prefix_len,term)
+     ~refine_thing:(refine_term ~rdb) (text,prefix_len,term)
      ~mk_localization_tbl ~expty ~subst
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
@@ -625,7 +624,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 
 let disambiguate_obj 
    ~mk_implicit ~description_of_alias ~mk_choice
-   ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+   ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
@@ -641,12 +640,13 @@ let disambiguate_obj
      ~passes:(MultiPassDisambiguator.passes ())
      ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
      ~interpretate_thing:(interpretate_obj ~mk_choice)
-     ~refine_thing:(refine_obj ~coercion_db) 
+     ~refine_thing:(refine_obj ~rdb) 
      (text,prefix_len,obj)
      ~mk_localization_tbl ~expty:None
    in
     List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
 ;;
+(*
 let _ = 
 let mk_type n = 
   if n = 0 then
@@ -685,4 +685,5 @@ in
          NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3);
 
 ;;
+*)