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 *)
| "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 s = String.sub s 5 (len - 5) 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 - 5 - i - 1) in
+ let uri = UriManager.uri_of_string suri in
+ try Cic.Type (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 ty = pop_cic ctxt in
- 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]