+let nmap_obj (uri,_,metasenv,subst,kind) =
+ let module K = Content in
+ let ids_to_refs = Hashtbl.create 211 in
+ let register_ref = Hashtbl.add ids_to_refs in
+ let idref = idref register_ref in
+ let nast_of_cic =
+ nast_of_cic1 ~idref ~output_type:`Term ~subst in
+ let seed = ref 0 in
+ let conjectures =
+ match metasenv with
+ [] -> None
+ | _ -> (*Some (List.map (map_conjectures seed) metasenv)*)
+ (*CSC: used to be the previous line, that uses seed *)
+ Some (List.map (nmap_sequent0 ~idref ~subst) metasenv)
+ in
+ let res =
+ match kind with
+ 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,
+ `Def (K.Const,ty,
+ build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
+ | NCic.Constant (_,_,None,ty,_) ->
+ let ty = nast_of_cic ~context:[] ty in
+ (gen_id object_prefix seed, [], conjectures,
+ `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
+;;