X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=357f9e53977aa10be34f8df4b805304d5cd92041;hb=0369aa83a42ed4730ed1946b02365760817f6ea2;hp=e3384407cc06a0d1612f6baac12f59223952b69b;hpb=6b3242efcd29ea188ef09b445985abb06c5fad3a;p=helm.git diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index e3384407c..357f9e539 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,8 +27,14 @@ let cic_name_of_name = function | _ -> assert false ;; +let rec mk_rels howmany from = + match howmany with + | 0 -> [] + | _ -> (NCic.Rel (howmany + from)) :: (mk_rels (howmany-1) 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))); @@ -40,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, ()) @@ -61,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=[]); @@ -75,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, [], [], ()) @@ -306,22 +307,25 @@ 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.Implicit -> NCic.Implicit `Term + | CicNotationPt.NRef nref -> NCic.Const nref + | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector + | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term | CicNotationPt.UserInput -> NCic.Implicit `Hole | CicNotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) @@ -336,11 +340,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 []) @@ -357,7 +363,8 @@ let interpretate_term_and_interpretate_term_option res | Some (CicNotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) - | Some CicNotationPt.Implicit -> NCic.Implicit annotation + | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation + | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector | Some term -> aux ~localize loc context term in (fun ~context -> aux ~localize:true HExtlib.dummy_floc context), @@ -488,7 +495,7 @@ let interpretate_obj (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit + None -> CicNotationPt.Implicit `JustOne | Some t -> t in let name = cic_name_of_name name in let t = @@ -539,56 +546,65 @@ let interpretate_obj let attrs = `Provided, `Regular in uri, height, [], [], NCic.Inductive (true,leftno,tyl,attrs) - | _ -> assert false -(* - | CicNotationPt.Record (params,name,ty,fields) -> - let uri = match uri with Some uri -> uri | None -> assert false in - let context,params = - let context,res = - List.fold_left - (fun (context,res) (name,t) -> - let t = - match t with - None -> CicNotationPt.Implicit - | Some t -> t in - let name = cic_name_of_name name in - name::context,(name, interpretate_term context env None false t)::res - ) ([],[]) params - in - context,List.rev res in - let add_params = - List.fold_right - (fun (name,ty) t -> Cic.Prod (name,ty,t)) params in - let ty' = add_params (interpretate_term context env None false ty) in - let fields' = - snd ( - List.fold_left - (fun (context,res) (name,ty,_coercion,arity) -> - let context' = Cic.Name name :: context in - context',(name,interpretate_term context env None false ty)::res - ) (context,[]) fields) in - let concl = - (*here the explicit_named_substituion is assumed to be of length 0 *) - let mutind = Cic.MutInd (uri,0,[]) in - if params = [] then mutind - else - Cic.Appl - (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in - let con = + | CicNotationPt.Record (params,name,ty,fields) -> + let context,params = + let context,res = List.fold_left - (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) - concl fields' in - let con' = add_params con in - let tyl = [name,true,ty',["mk_" ^ name,con']] in - let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in - Cic.InductiveDefinition - (tyl,[],List.length params,[`Class (`Record field_names)]) -*) + (fun (context,res) (name,t) -> + let t = + match t with + None -> CicNotationPt.Implicit `JustOne + | Some t -> t in + let name = cic_name_of_name name in + let t = + interpretate_term ~obj_context:[] ~context ~env ~uri:None + ~is_path:false t + in + (name,NCic.Decl t)::context,(name,t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right (fun (name,ty) t -> NCic.Prod (name,ty,t)) params in + let leftno = List.length params in + let ty' = + 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 + ~is_path:false ty in + let context' = (name,NCic.Decl ty)::context in + context',(name,ty)::res + ) (context,[]) fields) in + let concl = + let mutind = NCic.Const nref in + if params = [] then mutind + else + NCic.Appl + (mutind::mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left (fun t (name,ty) -> NCic.Prod (name,ty,t)) concl fields' in + let con' = add_params con in + let relevance = [] in + let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in + let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in + let height = (* XXX calculate *) 0 in + let attrs = `Provided, `Record field_names in + uri, height, [], [], + NCic.Inductive (true,leftno,tyl,attrs) ;; 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 @@ -602,7 +618,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 @@ -610,7 +626,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 @@ -626,12 +642,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 @@ -670,4 +687,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*)