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.ml4160
1 files changed, 85 insertions, 75 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 6f5e378a..84e4a573 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -1,32 +1,34 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Compat
open Pp
+open Errors
open Util
open Names
-open Term
open Pcoq
open Glob_term
-open Genarg
open Tacexpr
open Libnames
-
-open Nametab
+open Globnames
open Detyping
-open Tok
+open Misctypes
+open Decl_kinds
+open Genredexpr
+open Tok (* necessary for camlp4 *)
(* Generic xml parser without raw data *)
-type attribute = string * (loc * string)
-type xml = XmlTag of loc * string * attribute list * xml list
+type attribute = string * (Loc.t * string)
+type xml = XmlTag of Loc.t * string * attribute list * xml list
let check_tags loc otag ctag =
- if otag <> ctag then
+ if not (String.equal otag ctag) then
user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
str "does not match open xml tag " ++ str otag ++ str ".")
@@ -41,27 +43,22 @@ GEXTEND Gram
xml:
[ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
"<"; "/"; ctag = IDENT; ">" ->
- check_tags loc otag ctag;
- XmlTag (loc,ctag,attrs,l)
+ check_tags (!@loc) otag ctag;
+ XmlTag (!@loc,ctag,attrs,l)
| "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
- XmlTag (loc,tag,attrs,[])
+ XmlTag (!@loc,tag,attrs,[])
] ]
;
attr:
- [ [ name = IDENT; "="; data = STRING -> (name, (loc, data)) ] ]
+ [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
;
END
(* Errors *)
-let error_expect_two_arguments loc =
- user_err_loc (loc,"",str "wrong number of arguments (expect two).")
-
-let error_expect_one_argument loc =
- user_err_loc (loc,"",str "wrong number of arguments (expect one).")
-
-let error_expect_no_argument loc =
- user_err_loc (loc,"",str "wrong number of arguments (expect none).")
+let error_bad_arity loc n =
+ let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in
+ user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^")."))
(* Interpreting attributes *)
@@ -70,33 +67,49 @@ let nmtoken (loc,a) =
with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
let get_xml_attr s al =
- try List.assoc s al
+ try String.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 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)
+ try
+ 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
+ match s.[i] with
+ | '/' -> s.[i] <- '.'
+ | _ -> ()
+ done;
+ qualid_of_string s
+ with Not_found | Invalid_argument _ ->
+ error ("Malformed URI \""^s^"\"")
+
+let constant_of_cdata (loc,a) =
+ let q = uri_of_data a in
+ try Nametab.locate_constant q
+ with Not_found -> error ("No such constant "^string_of_qualid q)
+
+let global_of_cdata (loc,a) =
+ let q = uri_of_data a in
+ try Nametab.locate q
+ with Not_found -> error ("No such global "^string_of_qualid q)
let inductive_of_cdata a = match global_of_cdata a with
- | IndRef (kn,_) -> kn
- | _ -> anomaly "XML parser: not an inductive"
+ | IndRef (kn,_) -> kn
+ | _ -> error (string_of_qualid (uri_of_data (snd a)) ^" is not an inductive")
-let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
+let ltacref_of_cdata (loc,a) =
+ let q = uri_of_data a in
+ try (loc,Nametab.locate_tactic q)
+ with Not_found -> error ("No such ltac "^string_of_qualid q)
let sort_of_cdata (loc,a) = match a with
- | "Prop" -> GProp Null
- | "Set" -> GProp Pos
+ | "Prop" -> GProp
+ | "Set" -> GSet
| "Type" -> GType None
| _ -> user_err_loc (loc,"",str "sort expected.")
@@ -105,7 +118,7 @@ let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
let get_xml_inductive_kn al =
inductive_of_cdata (* uriType apparent synonym of uri *)
(try get_xml_attr "uri" al
- with e when Errors.noncritical e -> get_xml_attr "uriType" al)
+ with UserError _ -> get_xml_attr "uriType" al)
let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
@@ -116,7 +129,7 @@ let get_xml_constructor al =
(get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al))
let get_xml_binder al =
- try Name (ident_of_cdata (List.assoc "binder" al))
+ try Name (ident_of_cdata (String.List.assoc "binder" al))
with Not_found -> Anonymous
let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al)
@@ -125,7 +138,7 @@ let get_xml_name al = ident_of_cdata (get_xml_attr "name" al)
let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al)
-let get_xml_no al = nmtoken (get_xml_attr "no" al)
+let get_xml_no al = Evar.unsafe_of_int (nmtoken (get_xml_attr "no" al))
(* A leak in the xml dtd: arities of constructor need to know global env *)
@@ -133,8 +146,8 @@ let compute_branches_lengths ind =
let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
mip.Declarations.mind_consnrealdecls
-let compute_inductive_nargs ind =
- Inductiveops.inductive_nargs (Global.env()) ind
+let compute_inductive_ndecls ind =
+ Inductiveops.inductive_nrealdecls ind
(* Interpreting constr as a glob_constr *)
@@ -144,17 +157,17 @@ let rec interp_xml_constr = function
| XmlTag (loc,"VAR",al,[]) ->
error "XML parser: unable to interp free variables"
| XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
- let body,decls = list_sep_last xl in
+ let body,decls = List.sep_last xl in
let ctx = List.map interp_xml_decl decls in
List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
ctx (interp_xml_target body)
| XmlTag (loc,"PROD",al,(_::_ as xl)) ->
- let body,decls = list_sep_last xl in
+ let body,decls = List.sep_last xl in
let ctx = List.map interp_xml_decl decls in
List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
ctx (interp_xml_target body)
| XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
- let body,defs = list_sep_last xl in
+ let body,defs = List.sep_last xl in
let ctx = List.map interp_xml_def defs in
List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
ctx (interp_xml_target body)
@@ -164,48 +177,48 @@ let rec interp_xml_constr = function
(XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
| XmlTag (loc,"META",al,xl) ->
- GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
+ GEvar (loc, get_xml_name al, Some (List.map interp_xml_substitution xl))
| XmlTag (loc,"CONST",al,[]) ->
- GRef (loc, ConstRef (get_xml_constant al))
+ GRef (loc, ConstRef (get_xml_constant al), None)
| XmlTag (loc,"MUTCASE",al,x::y::yl) ->
let ind = get_xml_inductive al in
let p = interp_xml_patternsType x in
let tm = interp_xml_inductiveTerm y in
let vars = compute_branches_lengths ind in
- let brs = list_map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
+ let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
in
let mat = simple_cases_matrix_of_branches ind brs in
- let nparams,n = compute_inductive_nargs ind in
- let nal,rtn = return_type_of_predicate ind nparams n p in
+ let n = compute_inductive_ndecls ind in
+ let nal,rtn = return_type_of_predicate ind n p in
GCases (loc,RegularStyle,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
- GRef (loc, IndRef (get_xml_inductive al))
+ GRef (loc, IndRef (get_xml_inductive al), None)
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- GRef (loc, ConstructRef (get_xml_constructor al))
+ GRef (loc, ConstructRef (get_xml_constructor al), None)
| 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
+ let ln,lc,lt = List.split3 lnct in
let lctx = List.map (fun _ -> []) ln in
GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, 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
+ let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
| XmlTag (loc,"CAST",al,[x1;x2]) ->
- GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
+ GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
| XmlTag (loc,"SORT",al,[]) ->
GSort (loc, get_xml_sort al)
| XmlTag (loc,s,_,_) ->
user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
and interp_xml_tag s = function
- | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl)
+ | XmlTag (loc,tag,al,xl) when String.equal tag s -> (loc,al,xl)
| XmlTag (loc,tag,_,_) -> user_err_loc (loc, "",
str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
and interp_xml_constr_alias s x =
match interp_xml_tag s x with
| (_,_,[x]) -> interp_xml_constr x
- | (loc,_,_) -> error_expect_one_argument loc
+ | (loc,_,_) -> error_bad_arity loc 1
and interp_xml_term x = interp_xml_constr_alias "term" x
and interp_xml_type x = interp_xml_constr_alias "type" x
@@ -215,13 +228,16 @@ 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_arg x = interp_xml_constr_alias "arg" x
-and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
+and interp_xml_substitution x =
+ match interp_xml_tag "substitution" x with
+ _, al, [x] -> get_xml_name al, interp_xml_constr x
+ | loc, _, _ -> error_bad_arity loc 1
(* no support for empty substitution from official dtd *)
and interp_xml_decl_alias s x =
match interp_xml_tag s x with
| (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
- | (loc,_,_) -> error_expect_one_argument loc
+ | (loc,_,_) -> error_bad_arity loc 1
and interp_xml_def x = interp_xml_decl_alias "def" x
and interp_xml_decl x = interp_xml_decl_alias "decl" x
@@ -229,20 +245,14 @@ 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 [] -> GStructRec
- | _ -> error_expect_no_argument loc)
- | "WellFounded" ->
- (match l with
- [c] -> GWfRec (interp_xml_type c)
- | _ -> error_expect_one_argument loc)
- | "Measure" ->
- (match l with
- [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
- | _ -> error_expect_two_arguments loc)
- | _ ->
- user_err_loc (locs,"",str "Invalid recursion order.")
+ match s, l with
+ | "Structural", [] -> GStructRec
+ | "Structural", _ -> error_bad_arity loc 0
+ | "WellFounded", [c] -> GWfRec (interp_xml_type c)
+ | "WellFounded", _ -> error_bad_arity loc 1
+ | "Measure", [m;r] -> GMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+ | "Measure", _ -> error_bad_arity loc 2
+ | _ -> user_err_loc (locs,"",str "Invalid recursion order.")
and interp_xml_FixFunction x =
match interp_xml_tag "FixFunction" x with
@@ -254,14 +264,14 @@ and interp_xml_FixFunction x =
((Some (nmtoken (get_xml_attr "recIndex" al)), GStructRec),
(get_xml_name al, interp_xml_type x1, interp_xml_body x2))
| (loc,_,_) ->
- error_expect_one_argument loc
+ error_bad_arity loc 1
and interp_xml_CoFixFunction x =
match interp_xml_tag "CoFixFunction" x with
| (loc,al,[x1;x2]) ->
(get_xml_name al, interp_xml_type x1, interp_xml_body x2)
| (loc,_,_) ->
- error_expect_one_argument loc
+ error_bad_arity loc 1
(* Interpreting tactic argument *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 01:59:15 +0000