- C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
- assert false (* TO DO *)
- | C.AConstant (id,idbody,n,bo,ty,params) ->
- (match idbody with
- Some idb ->
- let sort =
- (try Hashtbl.find ids_to_inner_sorts idb
- with notfound -> "Type") in
- if sort = "Prop" then
- let proof =
- (match bo with
- Some body ->
- acic2content seed ~name:None ~ids_to_inner_sorts
- ~ids_to_inner_types body
- | None -> assert false) in
- Theorem(id,idbody,n,Some proof,ty,params)
- else
- Def(id,idbody,n,bo,ty,params)
- | None -> Def(id,idbody,n,bo,ty,params))
- | C.AVariable (id,n,bo,ty,params) ->
- Variable(id,n,bo,ty,params)
- | C.AInductiveDefinition (id,tys,params,nparams) ->
- InductiveDefinition(id,tys,params,nparams)
+ C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
+ (gen_id seed, params,
+ Some
+ (List.map
+ (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
+ conjectures),
+ `Def (Const,ty,
+ build_def_item seed (get_id bo) (C.Name n) bo
+ ~ids_to_inner_sorts ~ids_to_inner_types))
+ | C.AConstant (_,_,n,Some bo,ty,params) ->
+ (gen_id seed, params, None,
+ `Def (Const,ty,
+ build_def_item seed (get_id bo) (C.Name n) bo
+ ~ids_to_inner_sorts ~ids_to_inner_types))
+ | C.AConstant (id,_,n,None,ty,params) ->
+ (gen_id seed, params, None,
+ `Decl (Const,
+ build_decl_item seed id (C.Name n) ty
+ ~ids_to_inner_sorts))
+ | C.AVariable (_,n,Some bo,ty,params) ->
+ (gen_id seed, params, None,
+ `Def (Var,ty,
+ build_def_item seed (get_id bo) (C.Name n) bo
+ ~ids_to_inner_sorts ~ids_to_inner_types))
+ | C.AVariable (id,n,None,ty,params) ->
+ (gen_id seed, params, None,
+ `Decl (Var,
+ build_decl_item seed id (C.Name n) ty
+ ~ids_to_inner_sorts))
+ | C.AInductiveDefinition (id,l,params,nparams) ->
+ (gen_id seed, params, None,
+ `Joint
+ { joint_id = gen_id seed;
+ joint_kind = `Inductive nparams;
+ joint_defs = List.map (build_inductive seed) l
+ })
+
+and
+ build_inductive seed =
+ fun (_,n,b,ty,l) ->
+ `Inductive
+ { inductive_id = gen_id seed;
+ inductive_kind = b;
+ inductive_type = ty;
+ inductive_constructors = build_constructors seed l
+ }