From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- parsing/g_xml.ml4 | 68 +++++++++++++++++++++++++++---------------------------- 1 file changed, 33 insertions(+), 35 deletions(-) (limited to 'parsing/g_xml.ml4') 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 *) -(* 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))) -- cgit v1.2.3