* http://helm.cs.unibo.it/
*)
-let debug_print = prerr_endline
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
open Printf
(string * Cic.annterm) list (* id, name, inductive, arity, constructors *)
| Meta_subst of Cic.annterm option
| Obj_class of Cic.object_class
+ | Obj_flavour of Cic.object_flavour
| Obj_field of string (* field name *)
| Obj_generated
| Tag of string * (string * string) list (* tag name, attributes *)
sprintf "Inductive_type %s (id=%s)" name id
| Meta_subst _ -> "Meta_subst"
| Obj_class _ -> "Obj_class"
+ | Obj_flavour _ -> "Obj_flavour"
| Obj_field name -> "Obj_field " ^ name
| Obj_generated -> "Obj_generated"
| Tag (tag, _) -> "Tag " ^ tag)
(** {2 Parsing context management} *)
let pop ctxt =
-(* debug_print "pop";*)
+(* debug_print (lazy "pop");*)
match ctxt.stack with
| hd :: tl -> (ctxt.stack <- tl)
| _ -> assert false
let push ctxt v =
-(* debug_print "push";*)
+(* debug_print (lazy "push");*)
ctxt.stack <- v :: ctxt.stack
let set_top ctxt v =
-(* debug_print "set_top";*)
+(* debug_print (lazy "set_top");*)
match ctxt.stack with
| _ :: tl -> (ctxt.stack <- v :: tl)
| _ -> assert false
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)
* each callback needs to be instantiated to a parsing context *)
let start_element ctxt tag attrs =
-(* debug_print (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs)));*)
+(* debug_print (lazy (sprintf "<%s%s>" tag (match attrs with | [] -> "" | _ -> " " ^ String.concat " " (List.map (fun (a,v) -> sprintf "%s=\"%s\"" a v) attrs))));*)
push ctxt (Tag (tag, attrs))
let end_element ctxt tag =
-(* debug_print (sprintf "</%s>" tag);*)
-(* debug_print (string_of_stack ctxt);*)
+(* debug_print (lazy (sprintf "</%s>" tag));*)
+(* debug_print (lazy (string_of_stack ctxt));*)
let attribute_error () = attribute_error ctxt tag in
let parse_error = parse_error ctxt in
let sort_of_string = sort_of_string ctxt in
| "REL" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["binder", binder; "id", id; "idref", idref; "value", value]
| ["binder", binder; "id", id; "idref", idref; "sort", _;
"value", value] ->
Cic.ARel (id, idref, int_of_string value, binder)
| "VAR" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "uri", uri]
| ["id", id; "sort", _; "uri", uri] ->
Cic.AVar (id, uri_of_string uri, [])
| _ -> attribute_error ()))
| "CONST" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "uri", uri]
| ["id", id; "sort", _; "uri", uri] ->
Cic.AConst (id, uri_of_string uri, [])
| _ -> attribute_error ()))
let args = pop_cics ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id ]
| ["id", id; "sort", _] -> Cic.AAppl (id, args)
| _ -> attribute_error ()))
| "decl" ->
let source = pop_cic ctxt in
push ctxt
(match pop_tag_attrs ctxt with
+ | ["binder", binder; "id", id ]
| ["binder", binder; "id", id; "type", _] ->
Decl (id, Cic.Name binder, source)
+ | ["id", id]
| ["id", id; "type", _] -> Decl (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "def" -> (* same as "decl" above *)
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)
+ | ["id", id]
| ["id", id; "sort", _] -> Def (id, Cic.Anonymous, source)
| _ -> attribute_error ())
| "arity" (* transparent elements (i.e. which contain a CIC) *)
in
let term = add_decl target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["type", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
in
let term = add_decl target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["sort", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
in
let term = add_def target ctxt.stack in
(match pop_tag_attrs ctxt with
+ []
| ["sort", _] -> ()
| _ -> attribute_error ());
push ctxt (Cic_term term)
let term = pop_cic ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ ["id", id]
| ["id", id; "sort", _] -> Cic.ACast (id, term, typ)
| _ -> attribute_error ()));
| "IMPLICIT" ->
let meta_substs = pop_meta_substs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "no", no]
| ["id", id; "no", no; "sort", _] ->
Cic.AMeta (id, int_of_string no, meta_substs)
| _ -> attribute_error ()));
| "MUTCONSTRUCT" ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noConstr", noConstr; "noType", noType; "uri", uri]
| ["id", id; "noConstr", noConstr; "noType", noType; "sort", _;
"uri", uri] ->
Cic.AMutConstruct (id, uri_of_string uri, int_of_string noType,
let fix_funs = pop_fix_funs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noFun", noFun]
| ["id", id; "noFun", noFun; "sort", _] ->
Cic.AFix (id, int_of_string noFun, fix_funs)
| _ -> attribute_error ()))
let cofix_funs = pop_cofix_funs ctxt in
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noFun", noFun]
| ["id", id; "noFun", noFun; "sort", _] ->
Cic.ACoFix (id, int_of_string noFun, cofix_funs)
| _ -> attribute_error ()))
| patternsType :: inductiveTerm :: patterns ->
push ctxt (Cic_term
(match pop_tag_attrs ctxt with
+ | ["id", id; "noType", noType; "uriType", uriType]
| ["id", id; "noType", noType; "sort", _; "uriType", uriType] ->
Cic.AMutCase (id, uri_of_string uriType, int_of_string noType,
patternsType, inductiveTerm, patterns)
| "attributes" ->
let rec aux acc = function (* retrieve object attributes *)
| Obj_class c :: tl -> aux (`Class c :: acc) tl
+ | Obj_flavour f :: tl -> aux (`Flavour f :: acc) tl
| Obj_generated :: tl -> aux (`Generated :: acc) tl
| tl -> acc, tl
in
(match pop_tag_attrs ctxt with
| ["name", name] -> Obj_field name
| _ -> attribute_error ())
+ | "flavour" ->
+ push ctxt
+ (match pop_tag_attrs ctxt with
+ | [ "value", "definition"] -> Obj_flavour `Definition
+ | [ "value", "fact"] -> Obj_flavour `Fact
+ | [ "value", "lemma"] -> Obj_flavour `Lemma
+ | [ "value", "remark"] -> Obj_flavour `Remark
+ | [ "value", "theorem"] -> Obj_flavour `Theorem
+ | [ "value", "variant"] -> Obj_flavour `Variant
+ | _ -> attribute_error ())
| "class" ->
let class_modifiers = pop_class_modifiers ctxt in
push ctxt
* leak when used in conjunction with such structures *)
raise exn);
ctxt.xml_parser <- None; (* ZACK: same comment as above *)
-(* debug_print (string_of_stack stack);*)
+(* debug_print (lazy (string_of_stack stack));*)
(* assert (List.length ctxt.stack = 1) *)
List.hd ctxt.stack
with
projects / helm.git / blobdiff