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.ml468
1 files changed, 33 insertions, 35 deletions
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index b8fee3ff..c9e135ed 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -1,27 +1,24 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4use: "pa_extend.cmo" i*)
-
-(* $Id: g_xml.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
open Term
open Pcoq
-open Rawterm
+open Glob_term
open Genarg
open Tacexpr
open Libnames
open Nametab
open Detyping
+open Tok
(* Generic xml parser without raw data *)
@@ -33,7 +30,7 @@ let check_tags loc otag ctag =
user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++
str "does not match open xml tag " ++ str otag ++ str ".")
-let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e)
+let xml_eoi = (Gram.entry_create "xml_eoi" : xml Gram.entry)
GEXTEND Gram
GLOBAL: xml_eoi;
@@ -98,9 +95,9 @@ let inductive_of_cdata a = match global_of_cdata a with
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
+ | "Prop" -> GProp Null
+ | "Set" -> GProp Pos
+ | "Type" -> GType None
| _ -> user_err_loc (loc,"",str "sort expected.")
let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
@@ -138,63 +135,64 @@ let compute_branches_lengths ind =
let compute_inductive_nargs ind =
Inductiveops.inductive_nargs (Global.env()) ind
-(* Interpreting constr as a rawconstr *)
+(* Interpreting constr as a glob_constr *)
let rec interp_xml_constr = function
| XmlTag (loc,"REL",al,[]) ->
- RVar (loc, get_xml_ident al)
+ GVar (loc, get_xml_ident al)
| 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 ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> RLambda (loc, na, Explicit, t, b))
+ 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 ctx = List.map interp_xml_decl decls in
- List.fold_right (fun (na,t) b -> RProd (loc, na, Explicit, t, b))
+ 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 ctx = List.map interp_xml_def defs in
- List.fold_right (fun (na,t) b -> RLetIn (loc, na, t, b))
+ List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
ctx (interp_xml_target body)
| XmlTag (loc,"APPLY",_,x::xl) ->
- RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
+ GApp (loc, interp_xml_constr x, List.map interp_xml_constr xl)
| XmlTag (loc,"instantiate",_,
(XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) ->
- RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
+ GApp (loc, interp_xml_constr x, List.map interp_xml_arg xl)
| XmlTag (loc,"META",al,xl) ->
- REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
+ GEvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl))
| XmlTag (loc,"CONST",al,[]) ->
- RRef (loc, ConstRef (get_xml_constant al))
+ GRef (loc, ConstRef (get_xml_constant al))
| 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 brs = List.map interp_xml_pattern yl in
- let brns = Array.to_list (compute_branches_lengths ind) in
- let mat = simple_cases_matrix_of_branches ind brns brs 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
+ 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
- RCases (loc,RegularStyle,rtn,[tm,nal],mat)
+ GCases (loc,RegularStyle,rtn,[tm,nal],mat)
| XmlTag (loc,"MUTIND",al,[]) ->
- RRef (loc, IndRef (get_xml_inductive al))
+ GRef (loc, IndRef (get_xml_inductive al))
| XmlTag (loc,"MUTCONSTRUCT",al,[]) ->
- RRef (loc, ConstructRef (get_xml_constructor al))
+ GRef (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
let lctx = List.map (fun _ -> []) ln in
- RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
+ 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
- RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
+ 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]) ->
- RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
+ GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
| XmlTag (loc,"SORT",al,[]) ->
- RSort (loc, get_xml_sort al)
+ GSort (loc, get_xml_sort al)
| XmlTag (loc,s,_,_) ->
user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
@@ -232,15 +230,15 @@ and interp_xml_recursionOrder x =
let (locs, s) = get_xml_attr "type" al in
match s with
"Structural" ->
- (match l with [] -> RStructRec
+ (match l with [] -> GStructRec
| _ -> error_expect_no_argument loc)
| "WellFounded" ->
(match l with
- [c] -> RWfRec (interp_xml_type c)
+ [c] -> GWfRec (interp_xml_type c)
| _ -> error_expect_one_argument loc)
| "Measure" ->
(match l with
- [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+ [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.")
@@ -252,7 +250,7 @@ and interp_xml_FixFunction x =
interp_xml_recursionOrder x1),
(get_xml_name al, interp_xml_type x2, interp_xml_body x3))
| (loc,al,[x1;x2]) ->
- ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
+ ((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
@@ -277,5 +275,5 @@ let rec interp_xml_tactic_arg = function
let parse_tactic_arg ch =
interp_xml_tactic_arg
- (Pcoq.Gram.Entry.parse xml_eoi
- (Pcoq.Gram.parsable (Stream.of_channel ch)))
+ (Pcoq.Gram.entry_parse xml_eoi
+ (Pcoq.Gram.parsable (Stream.of_channel ch)))
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-14 06:30:43 +0000