From d33ced344ba377f0a4003102d77f880fda108fd7 Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 24 Dec 2010 23:49:21 +0000 Subject: More {raw => glob} changes for consistency perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 12 ++++++------ pretyping/detyping.ml | 8 ++++---- pretyping/detyping.mli | 2 +- pretyping/glob_term.ml | 16 ++++++++-------- pretyping/glob_term.mli | 18 +++++++++--------- pretyping/matching.ml | 4 ++-- pretyping/pattern.ml | 10 +++++----- pretyping/pattern.mli | 2 +- pretyping/pretype_errors.ml | 2 +- pretyping/pretype_errors.mli | 2 +- pretyping/pretyping.ml | 20 ++++++++++---------- pretyping/pretyping.mli | 6 +++--- 12 files changed, 51 insertions(+), 51 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6abcd0314f..8e0d28fbfb 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -196,22 +196,22 @@ let feed_history arg = function (* This is for non exhaustive error message *) -let rec rawpattern_of_partial_history args2 = function +let rec glob_pattern_of_partial_history args2 = function | Continuation (n, args1, h) -> let args3 = make_anonymous_patvars (n - (List.length args2)) in - build_rawpattern (List.rev_append args1 (args2@args3)) h + build_glob_pattern (List.rev_append args1 (args2@args3)) h | Result pl -> pl -and build_rawpattern args = function +and build_glob_pattern args = function | Top -> args | MakeAlias (AliasLeaf, rh) -> assert (args = []); - rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh + glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh | MakeAlias (AliasConstructor pci, rh) -> - rawpattern_of_partial_history + glob_pattern_of_partial_history [PatCstr (dummy_loc, pci, args, Anonymous)] rh -let complete_history = rawpattern_of_partial_history [] +let complete_history = glob_pattern_of_partial_history [] (* This is to build glued pattern-matching history and alias bodies *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 4ff4cd3334..106629d2b0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -357,8 +357,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort = function - | Prop c -> RProp c - | Type u -> RType (Some u) + | Prop c -> GProp c + | Type u -> GType (Some u) type binder_kind = BProd | BLambda | BLetIn @@ -424,7 +424,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let v = array_map3 (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in - GRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -440,7 +440,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) = let v = array_map2 (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) bodies tys in - GRec(dl,RCoFix n,Array.of_list (List.rev lfi), + GRec(dl,GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index fd16c0013b..ff98f747e4 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -34,7 +34,7 @@ val detype_case : identifier list -> inductive * case_style * int * int array * int -> 'a option -> 'a -> 'a array -> glob_constr -val detype_sort : sorts -> rawsort +val detype_sort : sorts -> glob_sort val detype_rel_context : constr option -> identifier list -> names_context -> rel_context -> glob_decl list diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index deba9a257a..b973a24f74 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -30,7 +30,7 @@ let cases_pattern_loc = function type patvar = identifier -type rawsort = RProp of Term.contents | RType of Univ.universe option +type glob_sort = GProp of Term.contents | GType of Univ.universe option type binding_kind = Lib.binding_kind = Explicit | Implicit @@ -64,18 +64,18 @@ type glob_constr = | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array - | GSort of loc * rawsort + | GSort of loc * glob_sort | GHole of (loc * hole_kind) | GCast of loc * glob_constr * glob_constr cast_type | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr -and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option +and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option and fix_kind = - | RFix of ((int option * fix_recursion_order) array * int) - | RCoFix of int + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int and predicate_pattern = name * (loc * inductive * int * name list) option @@ -366,7 +366,7 @@ let glob_constr_of_closed_cases_pattern = function (**********************************************************************) (* Reduction expressions *) -type 'a raw_red_flag = { +type 'a glob_red_flag = { rBeta : bool; rIota : bool; rZeta : bool; @@ -392,8 +392,8 @@ type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf | Simpl of 'c with_occurrences option - | Cbv of 'b raw_red_flag - | Lazy of 'b raw_red_flag + | Cbv of 'b glob_red_flag + | Lazy of 'b glob_red_flag | Unfold of 'b with_occurrences list | Fold of 'a list | Pattern of 'a with_occurrences list diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 95305d58c2..4e11221d8b 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -31,7 +31,7 @@ val cases_pattern_loc : cases_pattern -> loc type patvar = identifier -type rawsort = RProp of Term.contents | RType of Univ.universe option +type glob_sort = GProp of Term.contents | GType of Univ.universe option type binding_kind = Lib.binding_kind = Explicit | Implicit @@ -65,18 +65,18 @@ type glob_constr = | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr | GRec of loc * fix_kind * identifier array * glob_decl list array * glob_constr array * glob_constr array - | GSort of loc * rawsort + | GSort of loc * glob_sort | GHole of (loc * Evd.hole_kind) | GCast of loc * glob_constr * glob_constr cast_type | GDynamic of loc * Dyn.t and glob_decl = name * binding_kind * glob_constr option * glob_constr -and fix_recursion_order = RStructRec | RWfRec of glob_constr | RMeasureRec of glob_constr * glob_constr option +and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option and fix_kind = - | RFix of ((int option * fix_recursion_order) array * int) - | RCoFix of int + | GFix of ((int option * fix_recursion_order) array * int) + | GCoFix of int and predicate_pattern = name * (loc * inductive * int * name list) option @@ -120,7 +120,7 @@ val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr (** {6 Reduction expressions} *) -type 'a raw_red_flag = { +type 'a glob_red_flag = { rBeta : bool; rIota : bool; rZeta : bool; @@ -128,7 +128,7 @@ type 'a raw_red_flag = { rConst : 'a list } -val all_flags : 'a raw_red_flag +val all_flags : 'a glob_red_flag type 'a or_var = ArgArg of 'a | ArgVar of identifier located @@ -145,8 +145,8 @@ type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf | Simpl of 'c with_occurrences option - | Cbv of 'b raw_red_flag - | Lazy of 'b raw_red_flag + | Cbv of 'b glob_red_flag + | Lazy of 'b glob_red_flag | Unfold of 'b with_occurrences list | Fold of 'a list | Pattern of 'a with_occurrences list diff --git a/pretyping/matching.ml b/pretyping/matching.ml index fc56f31d3f..1facb7c7ab 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -173,9 +173,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PRel n1, Rel n2 when n1 = n2 -> subst - | PSort (RProp c1), Sort (Prop c2) when c1 = c2 -> subst + | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst - | PSort (RType _), Sort (Type _) -> subst + | PSort (GType _), Sort (Type _) -> subst | PApp (p, [||]), _ -> sorec stk subst p t diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 19c5d156a1..50dd413c68 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -36,7 +36,7 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of (case_style * int array * inductive option * (int * int) option) @@ -92,8 +92,8 @@ let pattern_of_constr sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) | Var id -> PVar id - | Sort (Prop c) -> PSort (RProp c) - | Sort (Type _) -> PSort (RType None) + | Sort (Prop c) -> PSort (GProp c) + | Sort (Type _) -> PSort (GType None) | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) @@ -300,7 +300,7 @@ let rec pat_of_raw metas vars = function | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind | _ -> None in let cbrs = - Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs) + Array.init (List.length brs) (pat_of_glob_branch loc metas vars ind brs) in let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in PCase ((sty,cstr_nargs,ind,ind_nargs), pred, @@ -310,7 +310,7 @@ let rec pat_of_raw metas vars = function let loc = loc_of_glob_constr r in user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.") -and pat_of_raw_branch loc metas vars ind brs i = +and pat_of_glob_branch loc metas vars ind brs i = let bri = List.filter (function (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1 diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index b25637de9e..23de675989 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -70,7 +70,7 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of (case_style * int array * inductive option * (int * int) option) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b331574140..c0fa620485 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -183,7 +183,7 @@ let error_unexpected_type_loc loc env sigma actty expty = let error_not_product_loc loc env sigma c = raise_pretype_error (loc, env, sigma, NotProduct c) -(*s Error in conversion from AST to rawterms *) +(*s Error in conversion from AST to glob_constr *) let error_var_not_found_loc loc s = raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 11722bee2d..b558020440 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -123,6 +123,6 @@ val error_unexpected_type_loc : val error_not_product_loc : loc -> env -> Evd.evar_map -> constr -> 'b -(** {6 Error in conversion from AST to rawterms } *) +(** {6 Error in conversion from AST to glob_constr } *) val error_var_not_found_loc : loc -> identifier -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index baa783d0c6..a2fb8ea12d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -93,13 +93,13 @@ let ((constr_in : constr -> Dyn.t), (** Miscellaneous interpretation functions *) let interp_sort = function - | RProp c -> Prop c - | RType _ -> new_Type_sort () + | GProp c -> Prop c + | GType _ -> new_Type_sort () let interp_elimination_sort = function - | RProp Null -> InProp - | RProp Pos -> InSet - | RType _ -> InType + | GProp Null -> InProp + | GProp Pos -> InSet + | GType _ -> InType module type S = sig @@ -122,7 +122,7 @@ sig (* More general entry point with evars from ltac *) (* Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the rawterm cannot be instantiated. + unresolved holes in the glob_constr cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -293,8 +293,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct make_judge c (Retyping.get_type_of env Evd.empty c) let pretype_sort = function - | RProp c -> judge_of_prop_contents c - | RType _ -> judge_of_new_Type () + | GProp c -> judge_of_prop_contents c + | GType _ -> judge_of_new_Type () exception Found of fixpoint @@ -381,7 +381,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with - | RFix (vn,i) -> + | GFix (vn,i) -> (* First, let's find the guard indexes. *) (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, @@ -397,7 +397,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | RCoFix i -> + | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Loc.raise loc e); make_judge (mkCoFix cofix) ftys.(i) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 70e1a22fb6..e1f79f36c5 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -53,7 +53,7 @@ sig (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr, failing - unresolved holes in the rawterm cannot be instantiated. + unresolved holes in the glob_constr cannot be instantiated. In [understand_ltac expand_evars sigma env ltac_env constraint c], @@ -114,6 +114,6 @@ module Default : S val constr_in : constr -> Dyn.t val constr_out : Dyn.t -> constr -val interp_sort : rawsort -> sorts -val interp_elimination_sort : rawsort -> sorts_family +val interp_sort : glob_sort -> sorts +val interp_elimination_sort : glob_sort -> sorts_family -- cgit v1.2.3