summaryrefslogtreecommitdiff
path: root/parsing/g_xml.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_xml.ml4')
-rw-r--r--parsing/g_xml.ml4247
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)))