diff options
author | 2017-01-16 13:02:55 +0100 | |
---|---|---|
committer | 2017-04-24 23:58:22 +0200 | |
commit | ad3aab9415b98a247a6cbce05752632c3c42391c (patch) | |
tree | 1fba7e25aa16dbb7e42db283f8210b31a0b8931d /pretyping | |
parent | 6d9e008ffd81bbe927e3442fb0c37269ed25b21f (diff) |
[location] Move Glob_term.cases_pattern to located.
We continue the uniformization pass. No big news here, trying to be
minimally invasive.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 71 | ||||
-rw-r--r-- | pretyping/coercion.ml | 5 | ||||
-rw-r--r-- | pretyping/detyping.ml | 22 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 40 | ||||
-rw-r--r-- | pretyping/patternops.ml | 10 |
5 files changed, 75 insertions, 73 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6bc2a4f94..ce4610e3b 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -95,7 +95,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (PatVar (Loc.ghost,Anonymous)) + List.make n (Loc.tag @@ PatVar Anonymous) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -178,7 +178,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [PatCstr (Loc.ghost, pci, args, Anonymous)] rh + [Loc.tag @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -188,12 +188,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh + feed_history (Loc.tag @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments") let pop_history h = - feed_history (PatVar (Loc.ghost, Anonymous)) h + feed_history (Loc.tag @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -273,8 +273,8 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | PatVar _ :: l -> find_row_ind l - | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) + | (_, PatVar _) :: l -> find_row_ind l + | (loc, PatCstr(c,_,_)) :: _ -> Some (loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -427,9 +427,10 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns") -let alias_of_pat = function - | PatVar (_,name) -> name - | PatCstr(_,_,_,name) -> name +let alias_of_pat = Loc.with_loc (fun ~loc -> function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) let remove_current_pattern eqn = match eqn.patterns with @@ -472,13 +473,13 @@ let rec adjust_local_defs loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs loc (pats,decls) | (pats, LocalDef _ :: decls) -> - PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls) + (Loc.tag ~loc @@ PatVar Anonymous) :: adjust_local_defs loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable let check_and_adjust_constructor env ind cstrs = function - | PatVar _ as pat -> pat - | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> + | _, PatVar _ as pat -> pat + | loc, PatCstr (((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -489,7 +490,7 @@ let check_and_adjust_constructor env ind cstrs = function else try let args' = adjust_local_defs loc (args, List.rev ci.cs_args) - in PatCstr (loc, cstr, args', alias) + in Loc.tag ~loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ~loc env cstr nb_args_constr else @@ -502,8 +503,8 @@ let check_and_adjust_constructor env ind cstrs = function let check_all_variables env sigma typ mat = List.iter (fun eqn -> match current_pattern eqn with - | PatVar (_,id) -> () - | PatCstr (loc,cstr_sp,_,_) -> + | _, PatVar id -> () + | loc, PatCstr (cstr_sp,_,_) -> error_bad_pattern ~loc env sigma cstr_sp typ) mat @@ -529,8 +530,8 @@ let occur_in_rhs na rhs = | Name id -> Id.List.mem id rhs.rhs_vars let is_dep_patt_in eqn = function - | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | PatCstr _ -> true + | _, PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | _, PatCstr _ -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -750,7 +751,7 @@ let recover_and_adjust_alias_names names sign = | x::names, LocalAssum (_,t)::sign -> (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (PatVar (Loc.ghost,na), decl) :: aux (names,sign) + (Loc.tag @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -967,7 +968,7 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in + let pats = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -1165,8 +1166,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (* Sorting equations by constructor *) let rec irrefutable env = function - | PatVar (_,name) -> true - | PatCstr (_,cstr,args,_) -> + | _, PatVar name -> true + | _, PatCstr (cstr,args,_) -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in @@ -1187,14 +1188,14 @@ let group_equations pb ind current cstrs mat = let rest = remove_current_pattern eqn in let pat = current_pattern eqn in match check_and_adjust_constructor pb.env ind cstrs pat with - | PatVar (_,name) -> + | _, PatVar name -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in brs.(i-1) <- (args, name, rest) :: brs.(i-1) done; if !only_default == None then only_default := Some true - | PatCstr (loc,((_,i)),args,name) -> + | loc, PatCstr (((_,i)),args,name) -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1718,16 +1719,16 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in + Loc.tag @@ PatVar (Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with - | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc + | Construct (cstr,u) -> Loc.tag (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_map' reveal_pattern l acc in - PatCstr (Loc.ghost,cstr,l,Anonymous), acc + Loc.tag (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1803,7 +1804,7 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl; + [ { patterns = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = Loc.ghost; used = ref false; @@ -2063,18 +2064,18 @@ let hole = Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = - let rec typ env (ty, realargs) pat avoid = + let rec typ env (ty, realargs) (loc, pat) avoid = match pat with - | PatVar (l,name) -> + | PatVar name -> let name, avoid = match name with Name n -> name, avoid | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((Loc.tag ~loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) - | PatCstr (l,((_, i) as cstr),args,alias) -> + | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) @@ -2083,7 +2084,7 @@ let constr_of_pat env evdref arsign pat avoid = in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in - if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind; + if not (eq_ind ind cind) then error_bad_constructor ~loc env cstr ind; let cstrs = get_constructors env indf in let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -2103,7 +2104,7 @@ let constr_of_pat env evdref arsign pat avoid = in let args = List.rev args in let patargs = List.rev patargs in - let pat' = PatCstr (l, cstr, patargs, alias) in + let pat' = Loc.tag ~loc @@ PatCstr (cstr, patargs, alias) in let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in @@ -2169,11 +2170,11 @@ let vars_of_ctx sigma ctx = ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y -let rec is_included x y = +let rec is_included (loc_x, x) (loc_y, y) = match x, y with | PatVar _, _ -> true | _, PatVar _ -> true - | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> + | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> if Int.equal i i' then List.for_all2 is_included args args' else false diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 542db7fdf..b2c1d0116 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -78,8 +78,9 @@ let apply_coercion_args env evd check isproj argl funj = let apply_pattern_coercion loc pat p = List.fold_left (fun pat (co,n) -> - let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in - Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous)) + let f i = + if i<n then (Loc.tag ~loc @@ Glob_term.PatVar Anonymous) else pat in + Loc.tag ~loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8ba408679..eef6d34ac 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -285,7 +285,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = Loc.tag @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten @@ -308,7 +308,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> - let pat = PatVar(dl,update_name sigma na rhs) in + let pat = Loc.tag @@ PatVar(update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -644,17 +644,17 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = if force_wildcard () && noccurn sigma 1 b then - PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids + Loc.tag @@ PatVar (Anonymous),avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in let na,avoid' = compute_displayed_name_in sigma flag avoid x b in - PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na + Loc.tag @@ PatVar na,avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with | _, [] -> (dl, Id.Set.elements ids, - [PatCstr(dl, constr, List.rev patlist,Anonymous)], + [Loc.tag ~loc:dl @@ PatCstr(constr, List.rev patlist,Anonymous)], detype flags avoid env sigma b) | Lambda (x,t,b), false::l -> let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in @@ -668,7 +668,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran buildrec ids patlist avoid env l c | _, true::l -> - let pat = PatVar (dl,Anonymous) in + let pat = Loc.tag ~loc:dl @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -793,14 +793,14 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst pat = +let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@ match pat with | PatVar _ -> pat - | PatCstr (loc,((kn,i),j),cpl,n) -> + | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else - PatCstr (loc,((kn',i),j),cpl',n) + PatCstr (((kn',i),j),cpl',n) let (f_subst_genarg, subst_genarg_hook) = Hook.make () @@ -910,8 +910,8 @@ let rec subst_glob_constr subst raw = let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = PatVar (Loc.ghost,na) in - let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = Loc.tag @@ PatVar na in + let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let map name = try Some (Nameops.out_name name) with Failure _ -> None in let ids = List.map_filter map nal in (Loc.ghost,ids,[p],c)) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ebbfa195f..27ceabf4e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -15,9 +15,7 @@ open Glob_term (* Untyped intermediate terms, after ASTs and before constr. *) -let cases_pattern_loc = function - PatVar(loc,_) -> loc - | PatCstr(loc,_,_,_) -> loc +let cases_pattern_loc (loc, _) = loc let cases_predicate_names tml = List.flatten (List.map (function @@ -47,9 +45,9 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | _ -> false -let rec cases_pattern_eq p1 p2 = match p1, p2 with -| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2 -| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) -> +let rec cases_pattern_eq (_loc1, p1) (_loc2, p2) = match p1, p2 with +| PatVar na1, PatVar na2 -> Name.equal na1 na2 +| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && Name.equal na1 na2 | _ -> false @@ -423,18 +421,19 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = function - | PatVar (loc,na) as x -> +let rec map_case_pattern_binders f = Loc.map (function + | PatVar na as x -> let r = f na in if r == na then x - else PatVar (loc,r) - | PatCstr (loc,c,ps,na) as x -> + else PatVar r + | PatCstr (c,ps,na) as x -> let rna = f na in let rps = CList.smartmap (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x - else PatCstr(loc,c,rps,rna) + else PatCstr(c,rps,rna) + ) let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause = (* spiwack: not sure if I must do something with the list of idents. @@ -558,26 +557,27 @@ let rec cases_pattern_of_glob_constr na = function | Name _ -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found - | Anonymous -> PatVar (loc,Name id) + | Anonymous -> Loc.tag ~loc @@ PatVar (Name id) end - | GHole (loc,_,_,_) -> PatVar (loc,na) + | GHole (loc,_,_,_) -> Loc.tag ~loc @@ PatVar na | GRef (loc,ConstructRef cstr,_) -> - PatCstr (loc,cstr,[],na) + Loc.tag ~loc @@ PatCstr (cstr,[],na) | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + Loc.tag ~loc @@ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux = function - | PatCstr (loc,cstr,[],Anonymous) -> +let rec glob_constr_of_closed_cases_pattern_aux x = Loc.with_loc (fun ~loc -> function + | PatCstr (cstr,[],Anonymous) -> GRef (loc,ConstructRef cstr,None) - | PatCstr (loc,cstr,l,Anonymous) -> + | PatCstr (cstr,l,Anonymous) -> let ref = GRef (loc,ConstructRef cstr,None) in GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found + ) x let glob_constr_of_closed_cases_pattern = function - | PatCstr (loc,cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) + | loc, PatCstr (cstr,l,na) -> + na,glob_constr_of_closed_cases_pattern_aux (loc, PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b16d04495..8c570dffe 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = function [0,tags,pat_of_raw metas vars c]) | GCases (loc,sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind + | (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -408,15 +408,15 @@ let rec pat_of_raw metas vars = function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | PatVar(_,na) -> + | _, PatVar na -> name_iter (fun n -> metas := n::!metas) na; na - | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") + | loc, PatCstr(_,_,_) -> err ~loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) - | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs -> + | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) + | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> |