diff options
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 247 |
1 files changed, 247 insertions, 0 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 new file mode 100644 index 00000000..b4580750 --- /dev/null +++ b/parsing/g_xml.ml4 @@ -0,0 +1,247 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_xml.ml4 8624 2006-03-13 17:38:17Z msozeau $ *) + +open Pp +open Util +open Names +open Term +open Pcoq +open Rawterm +open Genarg +open Tacexpr +open Libnames + +open Nametab + +(* Generic xml parser without raw data *) + +type attribute = string * (loc * string) +type xml = XmlTag of loc * string * attribute list * xml list + +let check_tags loc otag ctag = + if otag <> ctag then + user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ + str "does not match open xml tag " ++ str otag) + +let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) + +GEXTEND Gram + GLOBAL: xml_eoi; + + xml_eoi: + [ [ x = xml; EOI -> x ] ] + ; + xml: + [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml; + "<"; "/"; ctag = IDENT; ">" -> + check_tags loc otag ctag; + XmlTag (loc,ctag,attrs,l) + | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" -> + XmlTag (loc,tag,attrs,[]) + ] ] + ; + attr: + [ [ name = IDENT; "="; data = STRING -> (name, (loc, data)) ] ] + ; +END + +(* Interpreting attributes *) + +let nmtoken (loc,a) = + try int_of_string a + with Failure _ -> user_err_loc (loc,"",str "nmtoken expected") + +let interp_xml_attr_qualid = function + | "uri", s -> qualid_of_string s + | _ -> error "Ill-formed xml attribute" + +let get_xml_attr s al = + try List.assoc s al + with Not_found -> error ("No attribute "^s) + +(* Interpreting specific attributes *) + +let ident_of_cdata (loc,a) = id_of_string a + +let uri_of_data s = + let n = String.index s ':' in + let p = String.index s '.' in + let s = String.sub s (n+2) (p-n-2) in + for i=0 to String.length s - 1 do if s.[i]='/' then s.[i]<-'.' done; + qualid_of_string s + +let constant_of_cdata (loc,a) = Nametab.locate_constant (uri_of_data a) + +let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a) + +let inductive_of_cdata a = match global_of_cdata a with + | IndRef (kn,_) -> kn + | _ -> failwith "kn" + +let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) + +let sort_of_cdata (loc,a) = match a with + | "Prop" -> RProp Null + | "Set" -> RProp Pos + | "Type" -> RType None + | _ -> user_err_loc (loc,"",str "sort expected") + +let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) + +let get_xml_inductive_kn al = inductive_of_cdata (get_xml_attr "uri" al) + +let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) + +let get_xml_inductive al = + (get_xml_inductive_kn al, nmtoken (get_xml_attr "noType" al)) + +let get_xml_constructor al = + (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) + +let get_xml_name al = + try Name (ident_of_cdata (List.assoc "binder" al)) + with Not_found -> Anonymous + +let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) + +let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al) + +(* Interpreting constr as a rawconstr *) + +let rec interp_xml_constr = function + | XmlTag (loc,"REL",al,[]) -> + RVar (loc, get_xml_ident al) + | XmlTag (loc,"VAR",al,[]) -> failwith "" + | XmlTag (loc,"LAMBDA",al,[x1;x2]) -> + let na,t = interp_xml_decl x1 in + RLambda (loc, na, t, interp_xml_target x2) + | XmlTag (loc,"PROD",al,[x1;x2]) -> + let na,t = interp_xml_decl x1 in + RProd (loc, na, t, interp_xml_target x2) + | XmlTag (loc,"LETIN",al,[x1;x2]) -> + let na,t = interp_xml_def x1 in + RLetIn (loc, na, t, interp_xml_target x2) + | XmlTag (loc,"APPLY",_,x::xl) -> + RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) + | XmlTag (loc,"META",al,xl) -> + failwith "META: TODO" + | XmlTag (loc,"CONST",al,[]) -> + RRef (loc, ConstRef (get_xml_constant al)) + | XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *) + failwith "XML MUTCASE TO DO"; +(* + ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x), + interp_xml_inductiveTerm y, + Array.of_list (List.map interp_xml_pattern yl), + ref None) +*) + | XmlTag (loc,"MUTIND",al,[]) -> + RRef (loc, IndRef (get_xml_inductive al)) + | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> + RRef (loc, ConstructRef (get_xml_constructor al)) + | XmlTag (loc,"FIX",al,xl) -> + let li,lnct = List.split (List.map interp_xml_FixFunction xl) in + let ln,lc,lt = list_split3 lnct in + RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + | XmlTag (loc,"COFIX",al,xl) -> + let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in + RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + | XmlTag (loc,"CAST",al,[x1;x2]) -> + RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2) + | XmlTag (loc,"SORT",al,[]) -> + RSort (loc, get_xml_sort al) + | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + +and interp_xml_tag s = function + | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl) + | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", + str "Expect tag " ++ str s ++ str " but find " ++ str s) + +and interp_xml_constr_alias s x = + match interp_xml_tag s x with + | (_,_,[x]) -> interp_xml_constr x + | (loc,_,_) -> + user_err_loc (loc,"",str "wrong number of arguments (expect one)") + +and interp_xml_term x = interp_xml_constr_alias "term" x +and interp_xml_type x = interp_xml_constr_alias "type" x +and interp_xml_target x = interp_xml_constr_alias "target" x +and interp_xml_body x = interp_xml_constr_alias "body" x +and interp_xml_pattern x = interp_xml_constr_alias "pattern" x +and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x +and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x + +and interp_xml_decl_alias s x = + match interp_xml_tag s x with + | (_,al,[x]) -> (get_xml_name al, interp_xml_constr x) + | (loc,_,_) -> + user_err_loc (loc,"",str "wrong number of arguments (expect one)") + +and interp_xml_def x = interp_xml_decl_alias "def" x +and interp_xml_decl x = interp_xml_decl_alias "decl" x + +and interp_xml_recursionOrder x = + let (loc, al, l) = interp_xml_tag "RecursionOrder" x in + let (locs, s) = get_xml_attr "type" al in + match s with + "Structural" -> + (match l with [] -> RStructRec + | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)")) + | "WellFounded" -> + (match l with + [c] -> RWfRec (interp_xml_type c) + | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> + user_err_loc (locs,"",str "invalid recursion order") + + +and interp_xml_FixFunction x = + match interp_xml_tag "FixFunction" x with + | (loc,al,[x1;x2;x3]) -> + ((nmtoken (get_xml_attr "recIndex" al), + interp_xml_recursionOrder x1), + (get_xml_ident al, interp_xml_type x2, interp_xml_body x3)) + | (loc,al,[x1;x2]) -> (* For backwards compatibility *) + ((nmtoken (get_xml_attr "recIndex" al), RStructRec), + (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)) + | (loc,_,_) -> + user_err_loc (loc,"",str "wrong number of arguments (expect one)") + +and interp_xml_CoFixFunction x = + match interp_xml_tag "CoFixFunction" x with + | (loc,al,[x1;x2]) -> + (get_xml_ident al, interp_xml_type x1, interp_xml_body x2) + | (loc,_,_) -> + user_err_loc (loc,"",str "wrong number of arguments (expect one)") + +(* Interpreting tactic argument *) + +let rec (interp_xml_tactic_expr : xml -> glob_tactic_expr) = function + | XmlTag (loc,"TACARG",[],[x]) -> + TacArg (interp_xml_tactic_arg x) + | _ -> error "Ill-formed xml tree" + +and interp_xml_tactic_arg = function + | XmlTag (loc,"TERM",[],[x]) -> + ConstrMayEval (ConstrTerm (interp_xml_constr x,None)) + | XmlTag (loc,"CALL",al,xl) -> + let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in + TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) +(* + | XmlTag (loc,"TACTIC",[],[x]) -> + Tacexp (interp_xml_tactic_expr x) + | _ -> error "Ill-formed xml tree" +*) + | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + +let parse_tactic_arg ch = + interp_xml_tactic_arg + (Pcoq.Gram.Entry.parse xml_eoi + (Pcoq.Gram.parsable (Stream.of_channel ch))) |