+let nmap_obj status (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 status ~idref ~output_type:`Term ~metasenv ~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 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.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,
+ `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))
+ in
+ res,ids_to_refs
+;;