(* 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
fun s ->
List.map uri_of_string (Str.split space_RE s)
+let impredicative_set = ref true;;
+
let sort_of_string ctxt = function
| "Prop" -> Cic.Prop
- | "Set" -> Cic.Set
- | "CProp" -> Cic.CProp
(* THIS CASE IS HERE ONLY TO ALLOW THE PARSING OF COQ LIBRARY
* THIS SHOULD BE REMOVED AS SOON AS univ_maker OR COQ'S EXPORTATION
* IS FIXED *)
+ | "CProp" -> Cic.CProp (CicUniv.fresh ~uri:ctxt.uri ())
| "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
+ | "Set" when !impredicative_set -> Cic.Set
+ | "Set" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
| s ->
let len = String.length s in
- if not(len > 5) then parse_error ctxt "sort expected";
- if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
- try
- Cic.Type
- (CicUniv.fresh
- ~uri:ctxt.uri
- ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+ let sort_len, mk_sort =
+ if len > 5 && String.sub s 0 5 = "Type:" then 5,fun x -> Cic.Type x
+ else if len > 6 && String.sub s 0 6 = "CProp:" then 6,fun x->Cic.CProp x
+ else parse_error ctxt "sort expected"
+ in
+ let s = String.sub s sort_len (len - sort_len) in
+ let i = String.index s ':' in
+ let id = int_of_string (String.sub s 0 i) in
+ let suri = String.sub s (i+1) (len - sort_len - i - 1) in
+ let uri = UriManager.uri_of_string suri in
+ try mk_sort (CicUniv.fresh ~uri ~id ())
with
| Failure "int_of_string"
| Invalid_argument _ -> parse_error ctxt "sort expected"
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
- let source = pop_cic ctxt in
+ let ty,source =
+ (*CSC: hack to parse Coq files where the LetIn is not typed *)
+ let ty = pop_cic ctxt in
+ try
+ let source = pop_cic ctxt in
+ ty,source
+ with
+ Parser_failure _ -> Cic.AImplicit ("MISSING_def_TYPE",None),ty
+ 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
let class_modifiers = pop_class_modifiers ctxt in
push ctxt
(match pop_tag_attrs ctxt with
- | ["value", "coercion"] -> Obj_class (`Coercion 0)
- | ("value", "coercion")::["arity",n]
- | ("arity",n)::["value", "coercion"] ->
- let arity = try int_of_string n with Failure _ ->
- parse_error "\"arity\" must be an integer"
- in
- Obj_class (`Coercion arity)
| ["value", "elim"] ->
(match class_modifiers with
| [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
| Getter_failure _ as exn ->
raise exn
| exn ->
- raise (Parser_failure ("uncaught exception: " ^ Printexc.to_string exn))
+ raise (Parser_failure ("CicParser: uncaught exception: " ^ Printexc.to_string exn))
(** {2 API implementation} *)