diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 79 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 110 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 8 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 52 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 20 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
7 files changed, 135 insertions, 145 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index eb0d01718..3beef7773 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 (Loc.tag @@ PatVar Anonymous) + List.make n (CAst.make @@ 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 - [Loc.tag @@ PatCstr (pci, args, Anonymous)] rh + [CAst.make @@ 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 (Loc.tag @@ PatCstr (pci,List.rev l,Anonymous)) rh + feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments") let pop_history h = - feed_history (Loc.tag @@ PatVar Anonymous) h + feed_history (CAst.make @@ 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 - | (loc, PatCstr(c,_,_)) :: _ -> Some (loc,c) + | { CAst.v = PatVar _ } :: l -> find_row_ind l + | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -427,7 +427,7 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns") -let alias_of_pat = Loc.with_loc (fun ?loc -> function +let alias_of_pat = CAst.with_val (function | PatVar name -> name | PatCstr(_,_,name) -> name ) @@ -473,13 +473,13 @@ let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (Loc.tag ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) + (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable let check_and_adjust_constructor env ind cstrs = function - | _, PatVar _ as pat -> pat - | loc, PatCstr (((_,i) as cstr),args,alias) as pat -> + | { CAst.v = PatVar _ } as pat -> pat + | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -490,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 Loc.tag ?loc @@ PatCstr (cstr, args', alias) + in CAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ?loc env cstr nb_args_constr else @@ -503,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 -> () - | loc, PatCstr (cstr_sp,_,_) -> + | { CAst.v = PatVar id } -> () + | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> error_bad_pattern ?loc env sigma cstr_sp typ) mat @@ -530,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 + | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | { CAst.v = PatCstr _ } -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -751,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 -> - (Loc.tag @@ PatVar na, decl) :: aux (names,sign) + (CAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -968,7 +968,7 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) tomatch in + let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -1166,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,_) -> + | { CAst.v = PatVar name } -> true + | { CAst.v = 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 @@ -1188,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 -> + | { CAst.v = 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 - | loc, PatCstr (((_,i)),args,name) -> + | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1719,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 - Loc.tag @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + CAst.make @@ 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) -> Loc.tag (PatCstr (cstr,[],Anonymous)), acc + | Construct (cstr,u) -> CAst.make (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 - Loc.tag (PatCstr (cstr,l,Anonymous)), acc + CAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1804,7 +1804,7 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) patl; + [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = None; used = ref false; @@ -2059,13 +2059,14 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = Loc.tag @@ +let hole = CAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = - let rec typ env (ty, realargs) (loc, pat) avoid = - match pat with + let rec typ env (ty, realargs) pat avoid = + let loc = pat.CAst.loc in + match pat.CAst.v with | PatVar name -> let name, avoid = match name with Name n -> name, avoid @@ -2073,7 +2074,7 @@ let constr_of_pat env evdref arsign pat avoid = let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - ((Loc.tag ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2104,7 +2105,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' = Loc.tag ?loc @@ PatCstr (cstr, patargs, alias) in + let pat' = CAst.make ?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 @@ -2160,18 +2161,18 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (Loc.tag @@ GApp ( - (Loc.tag @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole; Loc.tag @@ GVar prev])) :: vars + (CAst.make @@ GApp ( + (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole; CAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, (Loc.tag @@ GVar n) :: vars) + | Name n -> n, (CAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y -let rec is_included (loc_x, x) (loc_y, y) = - match x, y with +let rec is_included x y = + match CAst.(x.v, y.v) with | PatVar _, _ -> true | _, PatVar _ -> true | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> @@ -2289,13 +2290,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = - let bref = Loc.tag @@ GVar branch_name in + let bref = CAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> Loc.tag @@ GApp (bref, l) + | l -> CAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> Loc.tag @@ GApp (branch, [ hole ]) + Some _ -> CAst.make @@ GApp (branch, [ hole ]) | None -> branch in incr i; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index acccfc125..a93653f32 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -79,8 +79,8 @@ let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> 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)) + if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + CAst.make ?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 721d1d749..2bfd67f6f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -283,7 +283,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 = Loc.tag @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = CAst.make @@ 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 @@ -306,7 +306,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 = Loc.tag @@ PatVar(update_name sigma na rhs) in + let pat = CAst.make @@ 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 @@ -329,7 +329,7 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match snd r,l with + match r.CAst.v, l with | r', [] -> r | GLambda (_,_,_,t), false::l -> strip l t | GLetIn (_,_,_,t), true::l -> strip l t @@ -339,7 +339,7 @@ let extract_nondep_branches test c b l = let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match snd c, l with + match c.CAst.v, l with | _, [] -> (List.rev nal,c) | GLambda (na,_,_,c), false::l -> aux l (na::nal) c | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c @@ -353,11 +353,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = Loc.tag @@ GVar x in + let a = CAst.make @@ GVar x in aux l (Name x :: nal) (match c with - | loc, GApp (p,l) -> (loc, GApp (p,l@[a])) - | _ -> Loc.tag @@ GApp (c,[a])) + | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) + | _ -> CAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -373,7 +373,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match snd typ with + let n,typ = match typ.CAst.v with | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = @@ -395,7 +395,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = else st with Not_found -> st - in Loc.tag @@ + in match tag, aliastyp with | LetStyle, None -> let bl' = Array.map detype bl in @@ -440,12 +440,12 @@ let detype_instance sigma l = if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) -let rec detype flags avoid env sigma t = Loc.tag @@ +let rec detype flags avoid env sigma t = CAst.make @@ match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar id - | Anonymous -> snd @@ !detype_anonymous n + | Anonymous -> (!detype_anonymous n).CAst.v with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) in GVar (Id.of_string s)) @@ -458,7 +458,7 @@ let rec detype flags avoid env sigma t = Loc.tag @@ with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - snd (detype flags avoid env sigma c1) + (detype flags avoid env sigma c1).CAst.v | Cast (c1,k,c2) -> let d1 = detype flags avoid env sigma c1 in let d2 = detype flags avoid env sigma c2 in @@ -468,12 +468,12 @@ let rec detype flags avoid env sigma t = Loc.tag @@ | _ -> CastConv d2 in GCast(d1,cast) - | Prod (na,ty,c) -> snd @@ detype_binder flags BProd avoid env sigma na None ty c - | Lambda (na,ty,c) -> snd @@ detype_binder flags BLambda avoid env sigma na None ty c - | LetIn (na,b,ty,c) -> snd @@ detype_binder flags BLetIn avoid env sigma na (Some b) ty c + | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c + | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c + | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match snd f' with + match f'.CAst.v with | GApp (f',args'') -> GApp (f',args''@args') | _ -> GApp (f',args') @@ -485,16 +485,16 @@ let rec detype flags avoid env sigma t = Loc.tag @@ let noparams () = let pb = Environ.lookup_projection p (snd env) in let pars = pb.Declarations.proj_npars in - let hole = Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in + let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in let args = List.make pars hole in - GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), (args @ [detype flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then @@ -512,12 +512,12 @@ let rec detype flags avoid env sigma t = Loc.tag @@ substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") - in snd @@ detype flags avoid env sigma c' + in (detype flags avoid env sigma c').CAst.v else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - snd @@ detype flags avoid env sigma c + (detype flags avoid env sigma c).CAst.v with Retyping.RetypeError _ -> noparams () else noparams () @@ -552,7 +552,6 @@ let rec detype flags avoid env sigma t = Loc.tag @@ GRef (ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in - snd @@ detype_case comp (detype flags avoid env sigma) (detype_eqns flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid @@ -643,17 +642,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 - Loc.tag @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + CAst.make @@ 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 - Loc.tag @@ PatVar na,avoid',(add_name na body ty env),add_vname ids na + CAst.make (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 | _, [] -> Loc.tag @@ (Id.Set.elements ids, - [Loc.tag @@ PatCstr(constr, List.rev patlist,Anonymous)], + [CAst.make @@ 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 @@ -667,7 +666,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 = Loc.tag @@ PatVar Anonymous in + let pat = CAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -682,7 +681,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = Loc.tag @@ +and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c @@ -740,7 +739,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | Name id -> Name (convert_id cl id) | Anonymous -> Anonymous in - let rec detype_closed_glob cl cg = Loc.map (function + let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function | GVar id -> (* if [id] is bound to a name. *) begin try @@ -754,11 +753,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = [Printer.pr_constr_under_binders_env] does. *) let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in let env = push_rel_context assums env in - snd @@ detype ?lax isgoal avoid env sigma c + (detype ?lax isgoal avoid env sigma c).CAst.v (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try let {closure;term} = Id.Map.find id cl.untyped in - snd @@ detype_closed_glob closure term + (detype_closed_glob closure term).CAst.v (* Otherwise [id] stands for itself *) with Not_found -> GVar id @@ -785,7 +784,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = in GCases(sty,po,tml,eqns) | c -> - snd @@ Glob_ops.map_glob_constr (detype_closed_glob cl) cg + (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v ) cg in detype_closed_glob t.closure t.term @@ -793,52 +792,52 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst (loc, pat) = Loc.tag ?loc @@ - match pat with - | PatVar _ -> pat - | PatCstr (((kn,i),j),cpl,n) -> +let rec subst_cases_pattern subst = CAst.map (function + | PatVar _ as pat -> pat + | PatCstr (((kn,i),j),cpl,n) as pat -> 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 (((kn',i),j),cpl',n) + ) let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ - match raw with - | GRef (ref,u) -> +let rec subst_glob_constr subst = CAst.map (function + | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - snd @@ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t) + (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v - | GVar _ -> raw - | GEvar _ -> raw - | GPatVar _ -> raw + | GSort _ + | GVar _ + | GEvar _ + | GPatVar _ as raw -> raw - | GApp (r,rl) -> + | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r and rl' = List.smartmap (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') - | GLambda (n,bk,r1,r2) -> + | GLambda (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else GLambda (n,bk,r1',r2') - | GProd (n,bk,r1,r2) -> + | GProd (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else GProd (n,bk,r1',r2') - | GLetIn (n,r1,t,r2) -> + | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in let t' = Option.smartmap (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') - | GCases (sty,rtno,rl,branches) -> + | GCases (sty,rtno,rl,branches) as raw -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno and rl' = List.smartmap (fun (a,x as y) -> let a' = subst_glob_constr subst a in @@ -860,14 +859,14 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if rtno' == rtno && rl' == rl && branches' == branches then raw else GCases (sty,rtno',rl',branches') - | GLetTuple (nal,(na,po),b,c) -> + | GLetTuple (nal,(na,po),b,c) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') - | GIf (c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 @@ -875,7 +874,7 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else GIf (c',(na,po'),b1',b2') - | GRec (fix,ida,bl,ra1,ra2) -> + | GRec (fix,ida,bl,ra1,ra2) as raw -> let ra1' = Array.smartmap (subst_glob_constr subst) ra1 and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in let bl' = Array.smartmap @@ -887,9 +886,7 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else GRec (fix,ida,bl',ra1',ra2') - | GSort _ -> raw - - | GHole (knd, naming, solve) -> + | GHole (knd, naming, solve) as raw -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -900,18 +897,19 @@ let rec subst_glob_constr subst (loc, raw) = Loc.tag ?loc @@ if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) - | GCast (r1,k) -> + | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + ) (* Utilities to transform kernel cases to simple pattern-matching problem *) 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 = Loc.tag @@ PatVar na in - let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = CAst.make @@ PatVar na in + let p = CAst.make @@ 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.tag @@ (ids,[p],c)) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 84da3652f..da287ae9f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -35,14 +35,6 @@ val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> cons val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr -val detype_case : - bool -> (constr -> glob_constr) -> - (constructor array -> bool list array -> constr array -> - (Id.t list * cases_pattern list * glob_constr) Loc.located list) -> - (constr -> bool list -> bool) -> - Id.t list -> inductive * case_style * bool list array * bool list -> - constr option -> constr -> constr array -> glob_constr - val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7e6b063d0..94bc24e3c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -15,15 +15,15 @@ open Glob_term (* Untyped intermediate terms, after ASTs and before constr. *) -let cases_pattern_loc (loc, _) = loc +let cases_pattern_loc c = c.CAst.loc let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp ?loc p t = Loc.tag ?loc @@ - match snd p with +let mkGApp ?loc p t = CAst.make ?loc @@ + match p.CAst.v with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) @@ -45,7 +45,7 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | _ -> false -let rec cases_pattern_eq (_loc1, p1) (_loc2, p2) = match p1, p2 with +let rec cases_pattern_eq { CAst.v = p1} { CAst.v = 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 && @@ -59,7 +59,7 @@ let cast_type_eq eq t1 t2 = match t1, t2 with | CastNative t1, CastNative t2 -> eq t1 t2 | _ -> false -let rec glob_constr_eq (_loc1, c1) (_loc2, c2) = match c1, c2 with +let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> @@ -137,7 +137,7 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with and instance_eq (x1,c1) (x2,c2) = Id.equal x1 x2 && glob_constr_eq c1 c2 -let map_glob_constr_left_to_right f = Loc.map (function +let map_glob_constr_left_to_right f = CAst.map (function | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in @@ -186,7 +186,7 @@ let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = Loc.with_unloc (function +let fold_glob_constr f acc = CAst.with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,b,c) | GProd (_,_,b,c) -> @@ -221,7 +221,7 @@ let same_id na id = match na with | Name id' -> Id.equal id id' let occur_glob_constr id = - let rec occur gt = Loc.with_unloc (function + let rec occur gt = CAst.with_val (function | GVar (id') -> Id.equal id id' | GApp (f,args) -> (occur f) || (List.exists occur args) | GLambda (na,bk,ty,c) -> @@ -270,7 +270,7 @@ let add_name_to_ids set na = | Name id -> Id.Set.add id set let free_glob_vars = - let rec vars bounded vs = Loc.with_unloc @@ (function + let rec vars bounded vs = CAst.with_val @@ (function | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args) | GLambda (na,_,ty,c) | GProd (na,_,ty,c) -> @@ -335,7 +335,7 @@ let free_glob_vars = let glob_visible_short_qualid c = let rec aux acc = function - | _, GRef (c,_) -> + | { CAst.v = GRef (c,_) } -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then id :: acc else acc @@ -354,10 +354,10 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = Loc.with_loc (fun ?loc -> function - | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c -> + let rec vars bound c = match c.CAst.v with + | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) -> let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound (loc, c) + fold_glob_constr vars bound c | GCases (sty,rtntypopt,tml,pl) -> let bound = vars_option bound rtntypopt in let bound = @@ -391,8 +391,7 @@ let bound_glob_vars = in Array.fold_left_i vars_fix bound idl | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound (loc, c) - ) + | GApp _ | GCast _ -> fold_glob_constr vars bound c and vars_pattern bound (loc,(idl,p,c)) = let bound = List.fold_right add_and_check_ident idl bound in @@ -425,7 +424,7 @@ 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 = Loc.map (function +let rec map_case_pattern_binders f = CAst.map (function | PatVar na as x -> let r = f na in if r == na then x @@ -463,7 +462,7 @@ let map_pattern f tomatch branches = List.map (fun tm -> map_tomatch f tm) tomatch, List.map (fun br -> map_cases_branch f br) branches -let loc_of_glob_constr (loc, _) = loc +let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) @@ -495,7 +494,7 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function +let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -535,14 +534,13 @@ let rec rename_glob_vars l = Loc.map_with_loc (fun ?loc -> function test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - (* XXX: This located use case should be improved. *) - | r -> snd @@ map_glob_constr (rename_glob_vars l) (loc, r) - ) + | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = Loc.map (function +let rec cases_pattern_of_glob_constr na = CAst.map (function | GVar id -> begin match na with | Name _ -> @@ -552,22 +550,22 @@ let rec cases_pattern_of_glob_constr na = Loc.map (function end | GHole (_,_,_) -> PatVar na | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) - | GApp ((_loc, GRef (ConstructRef cstr,_)),l) -> + | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> 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 x = Loc.map_with_loc (fun ?loc -> function +let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> - let ref = Loc.tag ?loc @@ GRef (ConstructRef cstr,None) in + let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x let glob_constr_of_closed_cases_pattern = function - | loc, PatCstr (cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (loc, PatCstr (cstr,l,Anonymous)) + | { CAst.loc ; v = PatCstr (cstr,l,na) } -> + na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 84d846afd..1884b6927 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -324,7 +324,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function +let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -333,7 +333,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ((_, GPatVar (true,n)), cl) -> + | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, @@ -362,8 +362,8 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = Loc.tag ?loc @@ - GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda c na = CAst.make ?loc @@ + GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; @@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind + | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (_, GHole _)), _ -> PMeta None + | (None | Some { CAst.v = GHole _}), _ -> PMeta None | Some p, None -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in @@ -409,15 +409,15 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | _, PatVar na -> + | { CAst.v = PatVar na } -> name_iter (fun n -> metas := n::!metas) na; na - | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.") + | { CAst.v = PatCstr(_,_,_) ; loc } -> 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 -> + | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) + | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a256eaa5d..76df89a26 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -567,12 +567,13 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) (loc, t) = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in - match t with + let loc = t.CAst.loc in + match t.CAst.v with | GRef (ref,u) -> inh_conv_coerce_to_tycon ?loc env evdref (pretype_ref ?loc evdref env ref u) @@ -1097,7 +1098,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | loc, GHole (knd, naming, None) -> + | { loc; CAst.v = GHole (knd, naming, None) } -> let rec is_Type c = match EConstr.kind !evdref c with | Sort s -> begin match ESorts.kind !evdref s with |