diff options
Diffstat (limited to 'parsing/g_xml.ml4')
| -rw-r--r-- | parsing/g_xml.ml4 | 68 |
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))) |