From: Claudio Sacerdoti Coen Date: Wed, 29 Apr 2009 00:04:12 +0000 (+0000) Subject: Records are now interpreted in the NG (but I am sure there is some bug X-Git-Tag: make_still_working~4037 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ce251730873891f2975bc8c46b122e842d203db;p=helm.git Records are now interpreted in the NG (but I am sure there is some bug somewhere). --- diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 216b88b05..5a22a4b62 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -794,8 +794,10 @@ EXTEND indty = tactic_term; paramspec = inverter_param_list -> G.Inverter (loc, name, indty, paramspec) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> + | IDENT "record" ; (params,name,ty,fields) = record_spec -> G.Obj (loc, N.Record (params,name,ty,fields)) + | IDENT "nrecord" ; (params,name,ty,fields) = record_spec -> + G.NObj (loc, N.Record (params,name,ty,fields)) | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in G.Default (loc,what,uris) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index e3384407c..520db6aca 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); @@ -539,51 +545,59 @@ 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 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 nref = + NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in + 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 diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma index 86226fb02..75d3eda6a 100644 --- a/helm/software/matita/tests/ng_commands.ma +++ b/helm/software/matita/tests/ng_commands.ma @@ -42,4 +42,11 @@ nqed. (* ninductive nnat: Type ≝ nO: nnat - | nS: nnat → nnat. *) \ No newline at end of file + | nS: nnat → nnat. +*) + +(* testare anche i record e le ricorsioni/coricorsioni/(co)induttivi MUTUI *) + +(* +nrecord pair: Type ≝ { l: pair; r: pair }. +*) \ No newline at end of file