X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=e36a1290c949ed8bdc5549546228fb82efff9ea3;hb=fb2fabf6c94d6a2f930b7a84673c90af32c48803;hp=68733a8ef36a24328f80e98111da58ae297eadcc;hpb=bc7d32fd5c34cc2ac0edff13292662585e6ffa51;p=helm.git diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 68733a8ef..e36a1290c 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -58,6 +58,12 @@ let idref register_ref = Ast.AttributedTerm (`IdRef id, t) ;; +let level_of_uri u = + let name = NUri.name_of_uri u in + assert(String.length name > String.length "Type"); + String.sub name 4 (String.length name - 4) +;; + (* CODICE c&p da NCicPp *) let nast_of_cic0 status ~(idref: @@ -81,19 +87,16 @@ let nast_of_cic0 status idref (Ast.Meta (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l)) | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop) - | NCic.Sort NCic.Type _ -> idref (Ast.Sort `Set) - (* CSC: | C.Sort (C.Type []) -> F.fprintf f "Type0" - | C.Sort (C.Type [false, u]) -> F.fprintf f "%s" (NUri.name_of_uri u) - | C.Sort (C.Type [true, u]) -> F.fprintf f "S(%s)" (NUri.name_of_uri u) - | C.Sort (C.Type l) -> - F.fprintf f "Max("; - aux ctx (C.Sort (C.Type [List.hd l])); - List.iter (fun x -> F.fprintf f ",";aux ctx (C.Sort (C.Type [x]))) - (List.tl l); - F.fprintf f ")"*) - (* CSC: qua siamo grezzi *) + | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set) + | NCic.Sort NCic.Type ((`Type,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u))) + | NCic.Sort NCic.Type ((`CProp,u)::_) -> + idref(Ast.Sort (`NCProp (level_of_uri u))) + | NCic.Sort NCic.Type ((`Succ,u)::_) -> + idref(Ast.Sort (`NType (level_of_uri u ^ "+1"))) | NCic.Implicit `Hole -> idref (Ast.UserInput) - | NCic.Implicit _ -> idref (Ast.Implicit) + | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector) + | NCic.Implicit _ -> idref (Ast.Implicit `JustOne) | NCic.Prod (n,s,t) -> let n = if n.[0] = '_' then "_" else n in let binder_kind = `Forall in @@ -102,9 +105,11 @@ let nast_of_cic0 status | NCic.Lambda (n,s,t) -> idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)), k ~context:((n,NCic.Decl s)::context) t)) + | NCic.LetIn (n,s,ty,NCic.Rel 1) -> + idref (Ast.Cast (k ~context ty, k ~context s)) | NCic.LetIn (n,s,ty,t) -> - idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context ty)), k ~context s, - k ~context:((n,NCic.Decl s)::context) t)) + idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context + ty, k ~context:((n,NCic.Decl s)::context) t)) | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst -> let _,_,t,_ = List.assoc n subst in let hd = NCicSubstitution.subst_meta lc t in @@ -453,6 +458,8 @@ let nmap_sequent status ~metasenv ~subst conjecture = let object_prefix = "obj:";; let declaration_prefix = "decl:";; let definition_prefix = "def:";; +let inductive_prefix = "ind:";; +let joint_prefix = "joint:";; let get_id = function @@ -533,9 +540,61 @@ let nmap_obj status (uri,_,metasenv,subst,kind) = (*CSC: used to be the previous line, that uses seed *) Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv) in +let build_constructors seed l = + List.map + (fun (_,n,ty) -> + let ty = nast_of_cic ~context:[] ty in + { K.dec_name = Some n; + K.dec_id = gen_id declaration_prefix seed; + K.dec_inductive = false; + K.dec_aref = ""; + K.dec_type = ty + }) l +in +let build_inductive b seed = + fun (_,n,ty,cl) -> + let ty = nast_of_cic ~context:[] ty in + `Inductive + { K.inductive_id = gen_id inductive_prefix seed; + K.inductive_name = n; + K.inductive_kind = b; + K.inductive_type = ty; + K.inductive_constructors = build_constructors seed cl + } +in +let build_fixpoint b seed = + fun (_,n,_,ty,t) -> + let t = nast_of_cic ~context:[] t in + let ty = nast_of_cic ~context:[] ty in + `Definition + { K.def_id = gen_id inductive_prefix seed; + K.def_name = Some n; + K.def_aref = ""; + K.def_type = ty; + K.def_term = t; + } +in let res = match kind with - NCic.Constant (_,_,Some bo,ty,_) -> + | NCic.Fixpoint (is_rec, ifl, _) -> + (gen_id object_prefix seed, [], conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_rec then + `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl) + else `CoRecursive; + K.joint_defs = List.map (build_fixpoint is_rec seed) ifl + }) + | NCic.Inductive (is_ind, lno, itl, _) -> + (gen_id object_prefix seed, [], conjectures, + `Joint + { K.joint_id = gen_id joint_prefix seed; + K.joint_kind = + if is_ind then `Inductive lno else `CoInductive lno; + K.joint_defs = List.map (build_inductive is_ind seed) itl + }) + | NCic.Constant (_,_,Some bo,ty,_) -> let ty = nast_of_cic ~context:[] ty in let bo = nast_of_cic ~context:[] bo in (gen_id object_prefix seed, [], conjectures, @@ -547,39 +606,6 @@ let nmap_obj status (uri,_,metasenv,subst,kind) = `Decl (K.Const, (*CSC: ??? get_id ty here used to be the id of the axiom! *) build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty)) -(* - | C.AInductiveDefinition (id,l,params,nparams,_) -> - (gen_id object_prefix seed, params, conjectures, - `Joint - { K.joint_id = gen_id joint_prefix seed; - K.joint_kind = `Inductive nparams; - K.joint_defs = List.map (build_inductive seed) l - }) - -and - build_inductive seed = - let module K = Content in - fun (_,n,b,ty,l) -> - `Inductive - { K.inductive_id = gen_id inductive_prefix seed; - K.inductive_name = n; - K.inductive_kind = b; - K.inductive_type = ty; - K.inductive_constructors = build_constructors seed l - } - -and - build_constructors seed l = - let module K = Content in - List.map - (fun (n,t) -> - { K.dec_name = Some n; - K.dec_id = gen_id declaration_prefix seed; - K.dec_inductive = false; - K.dec_aref = ""; - K.dec_type = t - }) l -*) in res,ids_to_refs ;;