(* id, name, type, body *)
| Constructor of string * Cic.annterm (* name, type *)
| Decl of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
- | Def of Cic.id * Cic.name * Cic.annterm (* id, binder, source *)
+ | Def of Cic.id * Cic.name * Cic.annterm * Cic.annterm (* id, binder, source, type *)
| Fix_fun of Cic.id * string * int * Cic.annterm * Cic.annterm
(* id, name, ind. index, type, body *)
| Inductive_type of string * string * bool * Cic.annterm *
| Constructor (name, _) -> "Constructor " ^ name
| Cofix_fun (id, _, _, _) -> sprintf "Cofix_fun (id=%s)" id
| Decl (id, _, _) -> sprintf "Decl (id=%s)" id
- | Def (id, _, _) -> sprintf "Def (id=%s)" id
+ | Def (id, _, _, _) -> sprintf "Def (id=%s)" id
| Fix_fun (id, _, _, _, _) -> sprintf "Fix_fun (id=%s)" id
| Inductive_type (id, name, _, _, _) ->
sprintf "Inductive_type %s (id=%s)" name id
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
+ let ty = pop_cic ctxt in
let source = pop_cic ctxt in
push ctxt
(match pop_tag_attrs ctxt with
| ["binder", binder; "id", id]
| ["binder", binder; "id", id; "sort", _] ->
- Def (id, Cic.Name binder, source)
+ Def (id, Cic.Name binder, source, ty)
| ["id", id]
- | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
+ | ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source, ty)
| _ -> attribute_error ())
| "arity" (* transparent elements (i.e. which contain a CIC) *)
| "body"
| "LETIN" ->
let target = pop_cic ctxt in
let rec add_def target = function
- | Def (id, binder, source) :: tl ->
- add_def (Cic.ALetIn (id, binder, source, target)) tl
+ | Def (id, binder, source, ty) :: tl ->
+ add_def (Cic.ALetIn (id, binder, source, ty, target)) tl
| tl ->
ctxt.stack <- tl;
target