X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=6e72042e83c6a34901de94fe5607e6f41ecc9088;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;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..6e72042e8 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -27,6 +27,12 @@ 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= assert (uri=None); @@ -306,21 +312,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) -> @@ -336,11 +344,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 []) @@ -539,51 +549,60 @@ 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 + | 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 @@ -632,6 +651,7 @@ let disambiguate_obj 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 +690,5 @@ in NCicEnvironment.add_constraint false (mk_type 3) (mk_cprop 3); ;; +*)