* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s)
let sort_of_string ctxt = function
| "Prop" -> Cic.Prop
| "Set" -> Cic.Set
- | "Type" -> Cic.Type (CicUniv.fresh ~uri:ctxt.uri ())
-(* | "Type" -> CicUniv.restart_numbering (); |+ useful only to test parser +| *)
| "CProp" -> Cic.CProp
- | _ -> parse_error ctxt "sort expected"
+ (* 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 ())
+ | 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))) ())
+ with
+ | Failure "int_of_string"
+ | Invalid_argument _ -> parse_error ctxt "sort expected"
let patch_subst ctxt subst = function
| Cic.AConst (id, uri, _) -> Cic.AConst (id, uri, subst)
let fields =
List.map
(function
- | Obj_field name -> name
+ | Obj_field name ->
+ (match Str.split (Str.regexp " ") name with
+ | [name] -> name, false
+ | [name;"coercion"] -> name,true
+ | _ ->
+ parse_error
+ "wrong \"field\"'s name attribute")
| _ ->
parse_error
"unexpected extra content for \"record\" object class")
(match parse uri filename, parse uri filenamebody with
| Cic_constant_type (type_id, name, params, typ, obj_attributes),
Cic_constant_body (body_id, _, _, body, _) ->
- Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,[])
+ Cic.AConstant (type_id, Some body_id, name, Some body, typ, params,obj_attributes)
| _ ->
raise (Parser_failure (sprintf "no constant found in %s, %s"
filename filenamebody)))