X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=d81521f99e335e18b77ca2d20092298e3b646ae0;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=a289683772312aa3114040a53261b48fe186ce7d;hpb=18b2b2742fe8ebb3d11b32b9bb727f510df6927a;p=helm.git diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index a28968377..d81521f99 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -23,7 +23,8 @@ * 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 @@ -134,17 +135,17 @@ let attribute_error ctxt 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 @@ -296,10 +297,23 @@ let uri_list_of_string = 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) @@ -335,12 +349,12 @@ let find_helm_exception ctxt = * 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 "" tag);*) -(* debug_print (string_of_stack ctxt);*) +(* debug_print (lazy (sprintf "" 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 @@ -348,6 +362,7 @@ let end_element ctxt tag = | "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) @@ -355,12 +370,14 @@ let end_element ctxt tag = | "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 ())) @@ -373,22 +390,27 @@ let end_element ctxt tag = 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) *) @@ -421,6 +443,7 @@ let end_element ctxt tag = in let term = add_decl target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["type", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -435,6 +458,7 @@ let end_element ctxt tag = in let term = add_decl target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["sort", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -449,6 +473,7 @@ let end_element ctxt tag = in let term = add_def target ctxt.stack in (match pop_tag_attrs ctxt with + [] | ["sort", _] -> () | _ -> attribute_error ()); push ctxt (Cic_term term) @@ -457,6 +482,7 @@ let end_element ctxt tag = 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" -> @@ -477,6 +503,7 @@ let end_element ctxt tag = 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 ())); @@ -489,6 +516,7 @@ let end_element ctxt tag = | "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, @@ -514,6 +542,7 @@ let end_element ctxt tag = 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 ())) @@ -521,6 +550,7 @@ let end_element ctxt tag = 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 ())) @@ -529,6 +559,7 @@ let end_element ctxt tag = | 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) @@ -705,7 +736,7 @@ let parse uri filename = * 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