X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=5fa3b81887b9b7f17ff4fe52a23fb4ee6fb1b6da;hb=bbb2b03fee9f7c7595870d997118d51c1ce469f2;hp=520db6aca994a6710ba955362387803e8564d7a7;hpb=7ce251730873891f2975bc8c46b122e842d203db;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 520db6aca..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 []) @@ -570,19 +569,20 @@ let interpretate_obj add_params (interpretate_term ~obj_context:[] ~context ~env ~uri:None ~is_path:false ty) in + let nref = + NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in + let obj_context = [name,nref] in let fields' = snd ( List.fold_left (fun (context,res) (name,ty,_coercion,_arity) -> let ty = - interpretate_term ~obj_context:[] ~context ~env ~uri:None + interpretate_term ~obj_context ~context ~env ~uri:None ~is_path:false ty in let context' = (name,NCic.Decl ty)::context in context',(name,ty)::res ) (context,[]) fields) in let concl = - let nref = - NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in let mutind = NCic.Const nref in if params = [] then mutind else @@ -602,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 @@ -616,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 @@ -624,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 @@ -640,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 @@ -684,4 +685,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*)