X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=f0a3fa0eb7386ba9747243c4050d718ed2ffeea7;hpb=f3a40daf813df6d33289d4df64da6c16ea9d3ca4;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index f0a3fa0eb..5fa3b8188 100644 --- 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); ;; +*)