diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 854 |
1 files changed, 467 insertions, 387 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6e4d7270..fe0f20f8 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,23 +1,28 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) +module CVars = Vars + open Pp open CErrors open Util open Names open Nameops -open Term -open Vars +open Constr open Termops +open Environ +open EConstr +open Vars open Namegen open Declarations open Inductiveops -open Environ open Reductionops open Type_errors open Glob_term @@ -29,8 +34,11 @@ open Evardefine open Evarsolve open Evarconv open Evd -open Sigma.Notations open Context.Rel.Declaration +open Ltac_pretype + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (* Pattern-matching errors *) @@ -45,26 +53,26 @@ type pattern_matching_error = exception PatternMatchingError of env * evar_map * pattern_matching_error -let raise_pattern_matching_error (loc,env,sigma,te) = - Loc.raise loc (PatternMatchingError(env,sigma,te)) +let raise_pattern_matching_error ?loc (env,sigma,te) = + Loc.raise ?loc (PatternMatchingError(env,sigma,te)) -let error_bad_pattern_loc loc env sigma cstr ind = - raise_pattern_matching_error - (loc, env, sigma, BadPattern (cstr,ind)) +let error_bad_pattern ?loc env sigma cstr ind = + raise_pattern_matching_error ?loc + (env, sigma, BadPattern (cstr,ind)) -let error_bad_constructor_loc loc env cstr ind = - raise_pattern_matching_error - (loc, env, Evd.empty, BadConstructor (cstr,ind)) +let error_bad_constructor ?loc env cstr ind = + raise_pattern_matching_error ?loc + (env, Evd.empty, BadConstructor (cstr,ind)) -let error_wrong_numarg_constructor_loc loc env c n = - raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n)) +let error_wrong_numarg_constructor ?loc env c n = + raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n)) -let error_wrong_numarg_inductive_loc loc env c n = - raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) +let error_wrong_numarg_inductive ?loc env c n = + raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n)) let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> @@ -89,33 +97,34 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (PatVar (Loc.ghost,Anonymous)) + List.make n (DAst.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'] *) let relocate_rel n1 n2 k j = if Int.equal j (n1 + k) then n2+k else j -let rec relocate_index n1 n2 k t = match kind_of_term t with +let rec relocate_index sigma n1 n2 k t = + match EConstr.kind sigma t with | Rel j when Int.equal j (n1 + k) -> mkRel (n2+k) | Rel j when j < n1+k -> t | Rel j when j > n1+k -> t - | _ -> map_constr_with_binders succ (relocate_index n1 n2) k t + | _ -> EConstr.map_with_binders sigma succ (relocate_index sigma n1 n2) k t (**********************************************************************) (* Structures used in compiling pattern-matching *) type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -135,7 +144,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool*(Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * Context.Rel.Declaration.t + | Abstract of int * rel_declaration type tomatch_stack = tomatch_status list @@ -155,9 +164,9 @@ let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) | Continuation (n, _, _) -> - anomaly (str "Bad number of expected remaining patterns: " ++ int n) + anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".") | Result _ -> - anomaly (Pp.str "Exhausted pattern history") + anomaly (Pp.str "Exhausted pattern history.") (* This is for non exhaustive error message *) @@ -171,7 +180,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [PatCstr (Loc.ghost, pci, args, Anonymous)] rh + [DAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -181,12 +190,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 (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> - anomaly (Pp.str "Constructor not yet filled with its arguments") + anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = - feed_history (PatVar (Loc.ghost, Anonymous)) h + feed_history (DAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -239,12 +248,13 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } @@ -266,24 +276,29 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | PatVar _ :: l -> find_row_ind l - | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) + | p :: l -> + match DAst.get p with + | PatVar _ -> find_row_ind l + | PatCstr(c,_,_) -> Some (p.CAst.loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in let arsign = inductive_alldecls_env env indu in - let hole_source = match tmloc with - | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) - | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in + let indu = on_snd EInstance.make indu in + let hole_source i = match tmloc with + | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i) + | None -> Loc.tag @@ Evar_kinds.TomatchTypeParameter (ind,i) in let (_,evarl,_) = List.fold_right (fun decl (subst,evarl,n) -> match decl with | LocalAssum (na,ty) -> + let ty = EConstr.of_constr ty in let ty' = substl subst ty in let e = e_new_evar env evdref ~src:(hole_source n) ty' in (e::subst,e::evarl,n+1) | LocalDef (na,b,ty) -> + let b = EConstr.of_constr b in (substl subst b::subst,evarl,n+1)) arsign ([],[],1) in applist (mkIndU indu,List.rev evarl) @@ -307,9 +322,9 @@ let inh_coerce_to_ind evdref env loc ty tyi = un inductif cela doit être égal *) if not (e_cumul env evdref expected_typ ty) then evdref := sigma -let binding_vars_of_inductive = function +let binding_vars_of_inductive sigma = function | NotInd _ -> [] - | IsInd (_,IndType(_,realargs),_) -> List.filter isRel realargs + | IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs let extract_inductive_data env sigma decl = match decl with @@ -317,7 +332,7 @@ let extract_inductive_data env sigma decl = let tmtyp = try try_find_ind env sigma t None with Not_found -> NotInd (None,t) in - let tmtypvars = binding_vars_of_inductive tmtyp in + let tmtypvars = binding_vars_of_inductive sigma tmtyp in (tmtyp,tmtypvars) | LocalDef (_,_,t) -> (NotInd (None, t), []) @@ -332,35 +347,55 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames = let find_tomatch_tycon evdref env loc = function (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,realnal) -> + | Some {CAst.v=(ind,realnal)} -> mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal) | None -> empty_tycon,None -let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_glob_constr tomatch) in +let make_return_predicate_ltac_lvar sigma na tm c lvar = + match na, DAst.get tm with + | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> + if Id.Map.mem id lvar.ltac_genargs then + let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in + let ltac_idents = match kind sigma c with + | Var id' -> Id.Map.add id id' lvar.ltac_idents + | _ -> lvar.ltac_idents in + { lvar with ltac_genargs; ltac_idents } + else lvar + | _ -> lvar + +let ltac_interp_realnames lvar = function + | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal) + | _ as x -> x + +let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) = + let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in - let j = typing_fun tycon env evdref tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + let j = typing_fun tycon env evdref !lvar tomatch in + let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in evdref := evd; let typ = nf_evar !evdref j.uj_type in + lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar; let t = try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in (j.uj_val,t) -let coerce_to_indtype typing_fun evdref env matx tomatchl = +let coerce_to_indtype typing_fun evdref env lvar matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) | m -> m in - List.map2 (coerce_row typing_fun evdref env) matx' tomatchl + let lvar = ref lvar in + let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in + let tms = List.map (ltac_interp_realnames !lvar) tms in + !lvar,tms (************************************************************************) (* Utils *) -let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref = +let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e let evd_comb2 f evdref x y = @@ -387,12 +422,12 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = | Some (_,(ind,_)) -> let indt = inductive_template pb.evdref pb.env None ind in let current = - if List.is_empty deps && isEvar typ then + if List.is_empty deps && isEvar !(pb.evdref) typ then (* Don't insert coercions if dependent; only solve evars *) let _ = e_cumul pb.env pb.evdref indt typ in current else - (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in (current,try_find_ind pb.env sigma indt names)) @@ -406,7 +441,7 @@ let map_tomatch_type f = function | IsInd (t,ind,names) -> IsInd (f t,map_inductive_type f ind,names) | NotInd (c,t) -> NotInd (Option.map f c, f t) -let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) +let liftn_tomatch_type n depth = map_tomatch_type (Vars.liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 (**********************************************************************) @@ -415,11 +450,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1 let current_pattern eqn = match eqn.patterns with | pat::_ -> pat - | [] -> anomaly (Pp.str "Empty list of patterns") - -let alias_of_pat = function - | PatVar (_,name) -> name - | PatCstr(_,_,_,name) -> name + | [] -> anomaly (Pp.str "Empty list of patterns.") let remove_current_pattern eqn = match eqn.patterns with @@ -427,7 +458,7 @@ let remove_current_pattern eqn = { eqn with patterns = pats; alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let push_current_pattern (cur,ty) eqn = match eqn.patterns with @@ -436,7 +467,7 @@ let push_current_pattern (cur,ty) eqn = { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") (* spiwack: like [push_current_pattern] but does not introduce an alias in rhs_env. Aliasing binders are only useful for variables at @@ -446,7 +477,7 @@ let push_noalias_current_pattern eqn = match eqn.patterns with | _::pats -> { eqn with patterns = pats } - | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns") + | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.") @@ -458,17 +489,18 @@ let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } exception NotAdjustable -let rec adjust_local_defs loc = function +let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> - pat :: adjust_local_defs loc (pats,decls) + pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls) + (DAst.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 - | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> +let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with + | PatVar _ -> pat + | PatCstr (((_,i) as cstr),args,alias) -> + let loc = pat.CAst.loc in (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -478,35 +510,37 @@ let check_and_adjust_constructor env ind cstrs = function if Int.equal (List.length args) nb_args_constr then pat else try - let args' = adjust_local_defs loc (args, List.rev ci.cs_args) - in PatCstr (loc, cstr, args', alias) + let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) + in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> - error_wrong_numarg_constructor_loc loc env cstr nb_args_constr + error_wrong_numarg_constructor ?loc env cstr nb_args_constr else (* Try to insert a coercion *) try - Coercion.inh_pattern_coerce_to loc env pat ind' ind + Coercion.inh_pattern_coerce_to ?loc env pat ind' ind with Not_found -> - error_bad_constructor_loc loc env cstr ind + error_bad_constructor ?loc env cstr ind let check_all_variables env sigma typ mat = List.iter - (fun eqn -> match current_pattern eqn with - | PatVar (_,id) -> () - | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern_loc loc env sigma cstr_sp typ) + (fun eqn -> + let pat = current_pattern eqn in + match DAst.get pat with + | PatVar id -> () + | PatCstr (cstr_sp,_,_) -> + let loc = pat.CAst.loc in + error_bad_pattern ?loc env sigma cstr_sp typ) mat let check_unused_pattern env eqn = if not !(eqn.used) then - raise_pattern_matching_error - (eqn.eqn_loc, env, Evd.empty, UnusedClause eqn.patterns) + raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) let set_used_pattern eqn = eqn.used := true let extract_rhs pb = match pb.mat with - | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion()) + | [] -> user_err ~hdr:"build_leaf" (msg_may_need_inversion()) | eqn::_ -> set_used_pattern eqn; eqn.rhs @@ -517,10 +551,10 @@ let extract_rhs pb = let occur_in_rhs na rhs = match na with | Anonymous -> false - | Name id -> Id.List.mem id rhs.rhs_vars + | Name id -> Id.Set.mem id rhs.rhs_vars -let is_dep_patt_in eqn = function - | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs +let is_dep_patt_in eqn pat = match DAst.get pat with + | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs | PatCstr _ -> true let mk_dep_patt_row (pats,_,eqn) = @@ -533,19 +567,19 @@ let dependencies_in_pure_rhs nargs eqns = let deps_columns = matrix_transpose deps_rows in List.map (List.exists (fun x -> x)) deps_columns -let dependent_decl a = +let dependent_decl sigma a = function - | LocalAssum (na,t) -> dependent a t - | LocalDef (na,c,t) -> dependent a t || dependent a c + | LocalAssum (na,t) -> dependent sigma a t + | LocalDef (na,c,t) -> dependent sigma a t || dependent sigma a c -let rec dep_in_tomatch n = function - | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch n l - | Abstract (_,d) :: l -> dependent_decl (mkRel n) d || dep_in_tomatch (n+1) l +let rec dep_in_tomatch sigma n = function + | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l + | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l | [] -> false -let dependencies_in_rhs nargs current tms eqns = - match kind_of_term current with - | Rel n when dep_in_tomatch n tms -> List.make nargs true +let dependencies_in_rhs sigma nargs current tms eqns = + match EConstr.kind sigma current with + | Rel n when dep_in_tomatch sigma n tms -> List.make nargs true | _ -> dependencies_in_pure_rhs nargs eqns (* Computing the matrix of dependencies *) @@ -554,31 +588,30 @@ let dependencies_in_rhs nargs current tms eqns = declarations [d(i+1);...;dn] the term [tmi] is dependent in. [find_dependencies_signature (used1,...,usedn) ((tm1,d1),...,(tmn,dn))] - returns [(deps1,...,depsn)] where [depsi] is a subset of n,..,i+1 + returns [(deps1,...,depsn)] where [depsi] is a subset of tm(i+1),..,tmn denoting in which of the d(i+1)...dn, the term tmi is dependent. - Dependencies are expressed by index, e.g. in dependency list - [n-2;1], [1] points to [dn] and [n-2] to [d3] *) -let rec find_dependency_list tmblock = function +let rec find_dependency_list sigma tmblock = function | [] -> [] - | (used,tdeps,d)::rest -> - let deps = find_dependency_list tmblock rest in - if used && List.exists (fun x -> dependent_decl x d) tmblock + | (used,tdeps,tm,d)::rest -> + let deps = find_dependency_list sigma tmblock rest in + if used && List.exists (fun x -> dependent_decl sigma x d) tmblock then - List.add_set Int.equal - (List.length rest + 1) (List.union Int.equal deps tdeps) + match EConstr.kind sigma tm with + | Rel n -> List.add_set Int.equal n (List.union Int.equal deps tdeps) + | _ -> List.union Int.equal deps tdeps else deps -let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = - let deps = find_dependency_list (tm::tmtypleaves) nextlist in +let find_dependencies sigma is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = + let deps = find_dependency_list sigma (tm::tmtypleaves) nextlist in if is_dep_or_cstr_in_rhs || not (List.is_empty deps) - then ((true ,deps,d)::nextlist) - else ((false,[] ,d)::nextlist) + then ((true ,deps,tm,d)::nextlist) + else ((false,[] ,tm,d)::nextlist) -let find_dependencies_signature deps_in_rhs typs = - let l = List.fold_right2 find_dependencies deps_in_rhs typs [] in - List.map (fun (_,deps,_) -> deps) l +let find_dependencies_signature sigma deps_in_rhs typs = + let l = List.fold_right2 (find_dependencies sigma) deps_in_rhs typs [] in + List.map (fun (_,deps,_,_) -> deps) l (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |- and xn:Tn has just been regeneralized into x:Tn so that the terms @@ -591,31 +624,31 @@ let find_dependencies_signature deps_in_rhs typs = [relocate_index_tomatch 1 n tomatch] will go the way back. *) -let relocate_index_tomatch n1 n2 = +let relocate_index_tomatch sigma n1 n2 = let rec genrec depth = function | [] -> [] | Pushed (b,((c,tm),l,na)) :: rest -> - let c = relocate_index n1 n2 depth c in - let tm = map_tomatch_type (relocate_index n1 n2 depth) tm in + let c = relocate_index sigma n1 n2 depth c in + let tm = map_tomatch_type (relocate_index sigma n1 n2 depth) tm in let l = List.map (relocate_rel n1 n2 depth) l in Pushed (b,((c,tm),l,na)) :: genrec depth rest | Alias (initial,(na,c,d)) :: rest -> (* [c] is out of relocation scope *) - Alias (initial,(na,c,map_pair (relocate_index n1 n2 depth) d)) :: genrec depth rest + Alias (initial,(na,c,map_pair (relocate_index sigma n1 n2 depth) d)) :: genrec depth rest | NonDepAlias :: rest -> NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i, map_constr (relocate_index n1 n2 depth) d) + Abstract (i, RelDecl.map_constr (fun c -> relocate_index sigma n1 n2 depth c) d) :: genrec (depth+1) rest in genrec 0 (* [replace_tomatch n c tomatch] replaces [Rel n] by [c] in [tomatch] *) -let rec replace_term n c k t = - if isRel t && Int.equal (destRel t) (n + k) then lift k c - else map_constr_with_binders succ (replace_term n c) k t +let rec replace_term sigma n c k t = + if isRel sigma t && Int.equal (destRel sigma t) (n + k) then Vars.lift k c + else EConstr.map_with_binders sigma succ (replace_term sigma n c) k t let length_of_tomatch_type_sign na t = let l = match na with @@ -626,21 +659,21 @@ let length_of_tomatch_type_sign na t = | NotInd _ -> l | IsInd (_, _, names) -> List.length names + l -let replace_tomatch n c = +let replace_tomatch sigma n c = let rec replrec depth = function | [] -> [] | Pushed (initial,((b,tm),l,na)) :: rest -> - let b = replace_term n c depth b in - let tm = map_tomatch_type (replace_term n c depth) tm in - List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l; + let b = replace_term sigma n c depth b in + let tm = map_tomatch_type (replace_term sigma n c depth) tm in + List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l; Pushed (initial,((b,tm),l,na)) :: replrec depth rest | Alias (initial,(na,b,d)) :: rest -> (* [b] is out of replacement scope *) - Alias (initial,(na,b,map_pair (replace_term n c depth) d)) :: replrec depth rest + Alias (initial,(na,b,map_pair (replace_term sigma n c depth) d)) :: replrec depth rest | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i, map_constr (replace_term n c depth) d) + Abstract (i, RelDecl.map_constr (fun t -> replace_term sigma n c depth t) d) :: replrec (depth+1) rest in replrec 0 @@ -665,7 +698,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i, map_constr (liftn n depth) d) + Abstract (i, RelDecl.map_constr (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -700,7 +733,7 @@ let merge_name get_name obj = function let merge_names get_name = List.map2 (merge_name get_name) -let get_names env sign eqns = +let get_names env sigma sign eqns = let names1 = List.make (Context.Rel.length sign) Anonymous in (* If any, we prefer names used in pats, from top to bottom *) let names2,aliasname = @@ -712,17 +745,17 @@ let get_names env sign eqns = (* Otherwise, we take names from the parameters of the constructor but avoiding conflicts with user ids *) let allvars = - List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids) - [] eqns in + List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids) + Id.Set.empty eqns in let names3,_ = List.fold_left2 (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env t na) avoid)) + (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(out_name na)::avoid)) + (na::l,Id.Set.add (Name.get_id na) avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -733,7 +766,7 @@ let get_names env sign eqns = (* We now replace the names y1 .. yn y by the actual names *) (* xi1 .. xin xi to be found in the i-th clause of the matrix *) -let recover_initial_subpattern_names = List.map2 set_name +let recover_initial_subpattern_names = List.map2 RelDecl.set_name let recover_and_adjust_alias_names names sign = let rec aux = function @@ -742,7 +775,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) + (DAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -758,11 +791,11 @@ let push_rels_eqn_with_names sign eqn = push_rels_eqn sign eqn let push_generalized_decl_eqn env n decl eqn = - match get_name decl with + match RelDecl.get_name decl with | Anonymous -> push_rels_eqn [decl] eqn | Name _ -> - push_rels_eqn [set_name (get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn + push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn let drop_alias_eqn eqn = { eqn with alias_stack = List.tl eqn.alias_stack } @@ -770,7 +803,7 @@ let drop_alias_eqn eqn = let push_alias_eqn alias eqn = let aliasname = List.hd eqn.alias_stack in let eqn = drop_alias_eqn eqn in - let alias = set_name aliasname alias in + let alias = RelDecl.set_name aliasname alias in push_rels_eqn [alias] eqn (**********************************************************************) @@ -830,13 +863,13 @@ let rec map_predicate f k ccl = function | Abstract _ :: rest -> map_predicate f (k+1) ccl rest -let noccur_predicate_between n = map_predicate (noccur_between n) +let noccur_predicate_between sigma n = map_predicate (noccur_between sigma n) let liftn_predicate n = map_predicate (liftn n) let lift_predicate n = liftn_predicate n 1 -let regeneralize_index_predicate n = map_predicate (relocate_index n 1) 0 +let regeneralize_index_predicate sigma n = map_predicate (relocate_index sigma n 1) 0 let substnl_predicate sigma = map_predicate (substnl sigma) @@ -847,7 +880,7 @@ let subst_predicate (subst,copt) ccl tms = | Some c -> c::subst in substnl_predicate sigma 0 ccl tms -let specialize_predicate_var (cur,typ,dep) tms ccl = +let specialize_predicate_var (cur,typ,dep) env tms ccl = let c = match dep with | Anonymous -> None | Name _ -> Some cur @@ -855,7 +888,10 @@ let specialize_predicate_var (cur,typ,dep) tms ccl = let l = match typ with | IsInd (_, IndType (_, _), []) -> [] - | IsInd (_, IndType (_, realargs), names) -> realargs + | IsInd (_, IndType (indf, realargs), names) -> + let arsign,_ = get_arity env indf in + let arsign = List.map EConstr.of_rel_decl arsign in + subst_of_rel_context_instance arsign realargs | NotInd _ -> [] in subst_predicate (l,c) ccl tms @@ -868,13 +904,13 @@ let specialize_predicate_var (cur,typ,dep) tms ccl = (* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x' *) (* then we have to replace x by x' in t(x) and y by y' in P *) (*****************************************************************************) -let generalize_predicate (names,na) ny d tms ccl = +let generalize_predicate sigma (names,na) ny d tms ccl = let () = match na with - | Anonymous -> anomaly (Pp.str "Undetected dependency") + | Anonymous -> anomaly (Pp.str "Undetected dependency.") | _ -> () in let p = List.length names + 1 in let ccl = lift_predicate 1 ccl tms in - regeneralize_index_predicate (ny+p+1) ccl tms + regeneralize_index_predicate sigma (ny+p+1) ccl tms (*****************************************************************************) (* We just matched over cur:ind(realargs) in the following matching problem *) @@ -916,16 +952,16 @@ let rec extract_predicate ccl = function ccl let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = - let sign = make_arity_signature env true indf in + let sign = make_arity_signature env sigma true indf in (* n is the number of real args + 1 (+ possible let-ins in sign) *) let n = List.length sign in (* Before abstracting we generalize over cur and on those realargs *) (* that are rels, consistently with the specialization made in *) (* build_branch *) let tms = List.fold_right2 (fun par arg tomatch -> - match kind_of_term par with - | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch - | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list 0 sign) + match EConstr.kind sigma par with + | Rel i -> relocate_index_tomatch sigma (i+n) (destRel sigma arg) tomatch + | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list EConstr.mkRel 0 sign) (lift_tomatch_stack n tms) in (* Pred is already dependent in the current term to match (if *) (* (na<>Anonymous) and its realargs; we just need to adjust it to *) @@ -937,7 +973,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let pred = extract_predicate ccl tms in (* Build the predicate properly speaking *) let sign = List.map2 set_name (na::names) sign in - it_mkLambda_or_LetIn_name env pred sign + it_mkLambda_or_LetIn_name env sigma pred sign (* [expand_arg] is used by [specialize_predicate] if Yk denotes [Xk;xk] or [Xk], @@ -949,34 +985,37 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in (p+k,liftn_predicate (k-1) (p+1) ccl tms) - let use_unit_judge evd = let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in 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 _ -> DAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in [ { patterns = pats; rhs = { rhs_env = pb.env; - rhs_vars = []; - avoid_ids = []; + rhs_vars = Id.Set.empty; + avoid_ids = Id.Set.empty; it = None }; alias_stack = Anonymous::aliasnames; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false } ] let adjust_impossible_cases pb pred tomatch submat = match submat with | [] -> - begin match kind_of_term pred with + (** FIXME: This breaks if using evar-insensitive primitives. In particular, + this means that the Evd.define below may redefine an already defined + evar. See e.g. first definition of test for bug #3388. *) + let pred = EConstr.Unsafe.to_constr pred in + begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd end; add_assert_false_case pb tomatch | _ -> @@ -1022,12 +1061,13 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = (* We prepare the substitution of X and x:I(X) *) let realargsi = if not (Int.equal nrealargs 0) then - subst_of_rel_context_instance arsign (Array.to_list cs.cs_concl_realargs) + CVars.subst_of_rel_context_instance arsign (Array.to_list cs.cs_concl_realargs) else [] in + let realargsi = List.map EConstr.of_constr realargsi in let copti = match depna with | Anonymous -> None - | Name _ -> Some (build_dependent_constructor cs) + | Name _ -> Some (EConstr.of_constr (build_dependent_constructor cs)) in (* The substituends realargsi, copti are all defined in gamma, x1...xn *) (* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *) @@ -1063,69 +1103,69 @@ let adjust_predicate_from_tomatch tomatch (current,typ as ct) pb = (* Remove commutative cuts that turn out to be non-dependent after some evars have been instantiated *) -let rec ungeneralize n ng body = - match kind_of_term body with +let rec ungeneralize sigma n ng body = + match EConstr.kind sigma body with | Lambda (_,_,c) when Int.equal ng 0 -> subst1 (mkRel n) c | Lambda (na,t,c) -> (* We traverse an inner generalization *) - mkLambda (na,t,ungeneralize (n+1) (ng-1) c) + mkLambda (na,t,ungeneralize sigma (n+1) (ng-1) c) | LetIn (na,b,t,c) -> (* We traverse an alias *) - mkLetIn (na,b,t,ungeneralize (n+1) ng c) + mkLetIn (na,b,t,ungeneralize sigma (n+1) ng c) | Case (ci,p,c,brs) -> (* We traverse a split *) let p = - let sign,p = decompose_lam_assum p in - let sign2,p = decompose_prod_n_assum ng p in - let p = prod_applist p [mkRel (n+List.length sign+ng)] in + let sign,p = decompose_lam_assum sigma p in + let sign2,p = decompose_prod_n_assum sigma ng p in + let p = prod_applist sigma p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in mkCase (ci,p,c,Array.map2 (fun q c -> - let sign,b = decompose_lam_n_decls q c in - it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) + let sign,b = decompose_lam_n_decls sigma q c in + it_mkLambda_or_LetIn (ungeneralize sigma (n+q) ng b) sign) ci.ci_cstr_ndecls brs) | App (f,args) -> (* We traverse an inner generalization *) - assert (isCase f); - mkApp (ungeneralize n (ng+Array.length args) f,args) + assert (isCase sigma f); + mkApp (ungeneralize sigma n (ng+Array.length args) f,args) | _ -> assert false -let ungeneralize_branch n k (sign,body) cs = - (sign,ungeneralize (n+cs.cs_nargs) k body) +let ungeneralize_branch sigma n k (sign,body) cs = + (sign,ungeneralize sigma (n+cs.cs_nargs) k body) -let rec is_dependent_generalization ng body = - match kind_of_term body with +let rec is_dependent_generalization sigma ng body = + match EConstr.kind sigma body with | Lambda (_,_,c) when Int.equal ng 0 -> - dependent (mkRel 1) c + not (noccurn sigma 1 c) | Lambda (na,t,c) -> (* We traverse an inner generalization *) - is_dependent_generalization (ng-1) c + is_dependent_generalization sigma (ng-1) c | LetIn (na,b,t,c) -> (* We traverse an alias *) - is_dependent_generalization ng c + is_dependent_generalization sigma ng c | Case (ci,p,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> - let _,b = decompose_lam_n_decls q c in - is_dependent_generalization ng b) + let _,b = decompose_lam_n_decls sigma q c in + is_dependent_generalization sigma ng b) ci.ci_cstr_ndecls brs | App (g,args) -> (* We traverse an inner generalization *) - assert (isCase g); - is_dependent_generalization (ng+Array.length args) g + assert (isCase sigma g); + is_dependent_generalization sigma (ng+Array.length args) g | _ -> assert false -let is_dependent_branch k (_,br) = - is_dependent_generalization k br +let is_dependent_branch sigma k (_,br) = + is_dependent_generalization sigma k br let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> - let d = map_constr (nf_evar evd) d in + let d = map_constr (fun c -> nf_evar evd c) d in let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in - if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck - && Array.exists (is_dependent_branch k) brs then + if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck + && Array.exists (is_dependent_branch evd k) brs then (* Dependency in the current term to match and its dependencies is real *) let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in let inst = match d with @@ -1138,9 +1178,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (* terms by its actual value in both the remaining terms to match and *) (* the bodies of the Case *) let pred = lift_predicate (-1) pred tomatch in - let tomatch = relocate_index_tomatch 1 (n+1) tomatch in + let tomatch = relocate_index_tomatch evd 1 (n+1) tomatch in let tomatch = lift_tomatch_stack (-1) tomatch in - let brs = Array.map2 (ungeneralize_branch n k) brs cs in + let brs = Array.map2 (ungeneralize_branch evd n k) brs cs in aux k brs tomatch pred tocheck deps | _ -> assert false in aux 0 brs tomatch pred tocheck deps @@ -1148,9 +1188,9 @@ 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,_) -> +let rec irrefutable env pat = match DAst.get pat with + | 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 @@ -1170,15 +1210,15 @@ let group_equations pb ind current cstrs mat = (fun eqn () -> 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) -> + match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with + | 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) -> + | PatCstr (((_,i)),args,name) -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1192,17 +1232,17 @@ let rec generalize_problem names pb = function | [] -> pb, [] | i::l -> let pb',deps = generalize_problem names pb l in - let d = map_constr (lift i) (Environ.lookup_rel i pb.env) in + let d = map_constr (lift i) (lookup_rel i pb.env) in begin match d with | LocalDef (Anonymous,_,_) -> pb', deps | _ -> (* for better rendering *) - let d = map_type (whd_betaiota !(pb.evdref)) d in + let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) c) d in let tomatch = lift_tomatch_stack 1 pb'.tomatch in - let tomatch = relocate_index_tomatch (i+1) 1 tomatch in + let tomatch = relocate_index_tomatch !(pb.evdref) (i+1) 1 tomatch in { pb' with tomatch = Abstract (i,d) :: tomatch; - pred = generalize_predicate names i d pb'.tomatch pb'.pred }, + pred = generalize_predicate !(pb'.evdref) names i d pb'.tomatch pb'.pred }, i::deps end @@ -1224,10 +1264,17 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* build the name x1..xn from the names present in the equations *) (* that had matched constructor C *) let cs_args = const_info.cs_args in - let names,aliasname = get_names pb.env cs_args eqns in - let typs = List.map2 set_name names cs_args + let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in + let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in + let typs = List.map2 RelDecl.set_name names cs_args in + (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *) + (* This is a bit too strong I think, in the sense that what we would *) + (* really like is to have beta-iota reduction only at the positions where *) + (* parameters are substituted *) + let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in + (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) (* a matching on "x1 .. xn eqn" *) @@ -1247,35 +1294,35 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* We compute over which of x(i+1)..xn and x matching on xi will need a *) (* generalization *) let dep_sign = - find_dependencies_signature - (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns) + find_dependencies_signature !(pb.evdref) + (dependencies_in_rhs !(pb.evdref) const_info.cs_nargs current pb.tomatch eqns) (List.rev typs') in (* The dependent term to subst in the types of the remaining UnPushed terms is relative to the current context enriched by topushs *) - let ci = build_dependent_constructor const_info in + let ci = EConstr.of_constr (build_dependent_constructor const_info) in (* Current context Gamma has the form Gamma1;cur:I(realargs);Gamma2 *) (* We go from Gamma |- PI tms. pred to *) (* Gamma;x1..xn;curalias:I(x1..xn) |- PI tms'. pred' *) (* where, in tms and pred, those realargs that are vars are *) (* replaced by the corresponding xi and cur replaced by curalias *) - let cirealargs = Array.to_list const_info.cs_concl_realargs in + let cirealargs = Array.map_to_list EConstr.of_constr const_info.cs_concl_realargs in (* Do the specialization for terms to match *) let tomatch = List.fold_right2 (fun par arg tomatch -> - match kind_of_term par with - | Rel i -> replace_tomatch (i+const_info.cs_nargs) arg tomatch + match EConstr.kind !(pb.evdref) par with + | Rel i -> replace_tomatch !(pb.evdref) (i+const_info.cs_nargs) arg tomatch | _ -> tomatch) (current::realargs) (ci::cirealargs) (lift_tomatch_stack const_info.cs_nargs pb.tomatch) in let pred_is_not_dep = - noccur_predicate_between 1 (List.length realnames + 1) pb.pred tomatch in + noccur_predicate_between !(pb.evdref) 1 (List.length realnames + 1) pb.pred tomatch in let typs' = List.map2 (fun (tm, (tmtyp,_), decl) deps -> - let na = get_name decl in + let na = RelDecl.get_name decl in let na = match curname, na with | Name _, Anonymous -> curname | Name _, Name _ -> na @@ -1296,10 +1343,10 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn | Name _ -> let cur_alias = lift const_info.cs_nargs current in let ind = - appvect ( - applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), snd const_info.cs_cstr), - List.map (lift const_info.cs_nargs) const_info.cs_params), - const_info.cs_concl_realargs) in + mkApp ( + applist (mkIndU (inductive_of_constructor (fst const_info.cs_cstr), EInstance.make (snd const_info.cs_cstr)), + List.map (EConstr.of_constr %> lift const_info.cs_nargs) const_info.cs_params), + Array.map EConstr.of_constr const_info.cs_concl_realargs) in Alias (initial,(aliasname,cur_alias,(ci,ind))) in let tomatch = List.rev_append (alias :: currents) tomatch in @@ -1307,8 +1354,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let submat = adjust_impossible_cases pb pred tomatch submat in let () = match submat with | [] -> - raise_pattern_matching_error - (Loc.ghost, pb.env, Evd.empty, NonExhaustive (complete_history history)) + raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history)) | _ -> () in @@ -1366,23 +1412,24 @@ and match_current pb (initial,tomatch) = (* We compile branches *) let brvals = Array.map2 (compile_branch initial current realargs (names,dep) deps pb arsign) eqns cstrs in (* We build the (elementary) case analysis *) - let depstocheck = current::binding_vars_of_inductive typ in + let depstocheck = current::binding_vars_of_inductive !(pb.evdref) typ in let brvals,tomatch,pred,inst = postprocess_dependencies !(pb.evdref) depstocheck brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> + let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in it_mkLambda_or_LetIn body sign) brvals in let (pred,typ) = find_predicate pb.caseloc pb.env pb.evdref pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in - let pred = nf_betaiota !(pb.evdref) pred in + let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); - uj_type = prod_applist typ inst } + uj_type = prod_applist !(pb.evdref) typ inst } (* Building the sub-problem when all patterns are variables. Case @@ -1390,7 +1437,7 @@ and match_current pb (initial,tomatch) = and shift_problem ((current,t),_,na) pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in - let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in let pb = { pb with env = push_rel (LocalDef (na,current,ty)) pb.env; @@ -1407,7 +1454,7 @@ and shift_problem ((current,t),_,na) pb = are already introduced in the context, we avoid creating aliases to themselves by treating this case specially. *) and pop_problem ((current,t),_,na) pb = - let pred = specialize_predicate_var (current,t,na) pb.tomatch pb.pred in + let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in let pb = { pb with pred = pred; @@ -1450,8 +1497,9 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = history = pop_history_pattern pb.history; mat = List.map (push_alias_eqn alias) pb.mat } in let j = compile pb in + let sigma = !(pb.evdref) in { uj_val = - if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then + if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then subst1 c j.uj_val else mkLetIn (na,c,t,j.uj_val); @@ -1476,10 +1524,10 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = evaluation; the drawback is that it might duplicate the instances of the term to match when the corresponding variable is substituted by a non-evaluated expression *) - if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then + if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then (* Try to compile first using non expanded alias *) try - if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) + if initial then f orig (Retyping.get_type_of pb.env sigma orig) else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) @@ -1515,15 +1563,15 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,ids,lpat,rhs) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} = + let avoid = ids_of_named_context_val (named_context_val env) in + let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = { rhs_env = env; rhs_vars = free_glob_vars initial_rhs; - avoid_ids = ids@(ids_of_named_context (named_context env)); + avoid_ids = avoid; it = Some initial_rhs } in { patterns = initial_lpat; alias_stack = []; @@ -1560,7 +1608,7 @@ let matx_of_eqns env eqns = returning True never happens and any inhabited type can be put instead). *) -let adjust_to_extended_env_and_remove_deps env extenv subst t = +let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context extenv) in (* We first remove the bindings that are dependently typed (they are @@ -1578,11 +1626,11 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = let (p, _, _) = lookup_rel_id x (rel_context extenv) in let rec traverse_local_defs p = match lookup_rel p extenv with - | LocalDef (_,c,_) -> assert (isRel c); traverse_local_defs (p + destRel c) + | LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c) | LocalAssum _ -> p in let p = traverse_local_defs p in let u = lift (n' - n) u in - try Some (p, u, expand_vars_in_term extenv u) + try Some (p, u, expand_vars_in_term extenv sigma u) (* pedrot: does this really happen to raise [Failure _]? *) with Failure _ -> None in let subst0 = List.map_filter map subst in @@ -1611,19 +1659,19 @@ let rec list_assoc_in_triple x = function * similarly for each ti. *) -let abstract_tycon loc env evdref subst tycon extenv t = - let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*) - let src = match kind_of_term t with - | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk) - | _ -> (loc,Evar_kinds.CasesType true) in - let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in +let abstract_tycon ?loc env evdref subst tycon extenv t = + let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) + let src = match EConstr.kind !evdref t with + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in + let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part is in subst); these subterms are the "good" subterms and we replace them by an evar that may depend (and only depend) on the corresponding convertible subterms of the substitution *) let rec aux (k,env,subst as x) t = - let t = whd_evar !evdref t in match kind_of_term t with + match EConstr.kind !evdref t with | Rel n when is_local_def (lookup_rel n env) -> t | Evar ev -> let ty = get_type_of env !evdref t in @@ -1643,7 +1691,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in match good with | [] -> - map_constr_with_full_binders push_binder aux x t + map_constr_with_full_binders !evdref push_binder aux x t | (_, _, u) :: _ -> (* u is in extenv *) let vl = List.map pi1 good in let ty = @@ -1651,17 +1699,16 @@ let abstract_tycon loc env evdref subst tycon extenv t = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in - let depvl = free_rels ty in + let depvl = free_rels !evdref ty in let inst = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in let rel_filter = - List.map (fun a -> not (isRel a) || dependent a u - || Int.Set.mem (destRel a) depvl) inst in + List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u + || Int.Set.mem (destRel !evdref a) depvl) inst in let named_filter = - let open Context.Named.Declaration in - List.map (fun d -> dependent (mkVar (get_id d)) u) + List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u) (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in @@ -1670,7 +1717,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = in aux (0,extenv,subst0) t0 -let build_tycon loc env tycon_env s subst tycon extenv evdref t = +let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let t,tt = match t with | None -> (* This is the situation we are building a return predicate and @@ -1678,15 +1725,15 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in + e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in (lift (n'-n) impossible_case_type, mkSort u) | Some t -> - let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in + let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type"); + if not b then anomaly (Pp.str "Build_tycon: should be a type."); { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1701,26 +1748,26 @@ 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 t Anonymous) avoid in - PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in + let id = next_name_away (named_hd env sigma t Anonymous) avoid in + DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in let rec reveal_pattern t (subst,avoid as acc) = - match kind_of_term (whd_all env sigma t) with - | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc - | App (f,v) when isConstruct f -> - let cstr,u = destConstruct f in + match EConstr.kind sigma (whd_all env sigma t) with + | Construct (cstr,u) -> DAst.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 - PatCstr (Loc.ghost,cstr,l,Anonymous), acc + let l,acc = List.fold_right_map reveal_pattern l acc in + DAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with | [] -> [], acc_sign, acc | (t, IsInd (_,IndType(indf,realargs),_)) :: tms -> - let patl,acc = List.fold_map' reveal_pattern realargs acc in + let patl,acc = List.fold_right_map reveal_pattern realargs acc in let pat,acc = make_patvar t acc in let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env true indf' in + let sign = make_arity_signature env sigma true indf' in let patl = pat :: List.rev patl in let patl,sign = recover_and_adjust_alias_names patl sign in let p = List.length patl in @@ -1732,7 +1779,7 @@ let build_inversion_problem loc env sigma tms t = let d = LocalAssum (alias_of_pat pat,typ) in let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in - let avoid0 = ids_of_context env in + let avoid0 = vars_of_env env in (* [patl] is a list of patterns revealing the substructure of constructors present in the constraints on the type of the multiple terms t1..tn that are matched in the original problem; @@ -1753,11 +1800,11 @@ let build_inversion_problem loc env sigma tms t = List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in let decls = List.rev decls in - let dep_sign = find_dependencies_signature (List.make n true) decls in + let dep_sign = find_dependencies_signature sigma (List.make n true) decls in let sub_tms = List.map2 (fun deps (tm, (tmtyp,_), decl) -> - let na = if List.is_empty deps then Anonymous else force_name (get_name decl) in + let na = if List.is_empty deps then Anonymous else force_name (RelDecl.get_name decl) in Pushed (true,((tm,tmtyp),deps,na))) dep_sign decls in let subst = List.map (fun (na,t) -> (na,lift n t)) subst in @@ -1769,12 +1816,12 @@ let build_inversion_problem loc env sigma tms t = let main_eqn = { patterns = patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent vars so that the field rhs_vars is normally not used *) - rhs_vars = List.map fst subst; + rhs_vars = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty subst; avoid_ids = avoid; it = Some (lift n t) } } in (* [catch_all] is a catch-all default clause of the auxiliary @@ -1787,22 +1834,23 @@ 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 _ -> DAst.make @@ PatVar Anonymous) patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; - rhs_vars = []; + rhs_vars = Id.Set.empty; avoid_ids = avoid0; it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) let s' = Retyping.get_sort_of env sigma t in - let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in + let sigma, s = Evd.new_sort_variable univ_flexible sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in let pb = { env = pb_env; + lvar = empty_lvar; evdref = evdref; pred = (*ty *) mkSort s; tomatch = sub_tms; @@ -1810,7 +1858,7 @@ let build_inversion_problem loc env sigma tms t = mat = main_eqn :: catch_all_eqn; caseloc = loc; casestyle = RegularStyle; - typing_function = build_tycon loc env pb_env s subst} in + typing_function = build_tycon ?loc env pb_env s subst} in let pred = (compile pb).uj_val in (!evdref,pred) @@ -1820,52 +1868,62 @@ let build_initial_predicate arsign pred = let rec buildrec n pred tmnames = function | [] -> List.rev tmnames,pred | (decl::realdecls)::lnames -> - let na = get_name decl in + let na = RelDecl.get_name decl in let n' = n + List.length realdecls in buildrec (n'+1) pred (force_name na::tmnames) lnames | _ -> assert false in buildrec 0 pred [] (List.rev arsign) -let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = +let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign = let lift = if dolift then lift else fun n t -> t in let get_one_sign n tm (na,t) = match tm with | NotInd (bo,typ) -> (match t with - | None -> (match bo with + | None -> let sign = match bo with | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)]) - | Some (loc,_,_) -> - user_err_loc (loc,"", - str"Unexpected type annotation for a term of non inductive type.")) + | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign + | Some {CAst.loc} -> + user_err ?loc + (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in let arsign = fst (get_arity env0 indf') in - let realnal = + let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in + let realnal, realnal' = match t with - | Some (loc,ind',realnal) -> + | Some {CAst.loc;v=(ind',realnal)} -> if not (eq_ind ind ind') then - user_err_loc (loc,"",str "Wrong inductive type."); + user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then - anomaly (Pp.str "Ill-formed 'in' clause in cases"); - List.rev realnal - | None -> List.make nrealargs_ctxt Anonymous in - LocalAssum (na, build_dependent_inductive env0 indf') - ::(List.map2 set_name realnal arsign) in + anomaly (Pp.str "Ill-formed 'in' clause in cases."); + let realnal = List.rev realnal in + let realnal' = List.map (ltac_interp_name lvar) realnal in + realnal,realnal' + | None -> + let realnal = List.make nrealargs_ctxt Anonymous in + realnal, realnal in + let na' = ltac_interp_name lvar na in + let t = EConstr.of_constr (build_dependent_inductive env0 indf') in + (* Context with names for typing *) + let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in + (* Context with names for building the term *) + let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in + arsign1,arsign2 in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> let l = get_one_sign n tm x in - l :: buildrec (n + List.length l) (ltm,tmsign) + l :: buildrec (n + List.length (fst l)) (ltm,tmsign) | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) -let inh_conv_coerce_to_tycon loc env evdref j tycon = +let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in evdref := evd'; j | None -> j @@ -1877,8 +1935,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in - match kind_of_term tm with - | Rel n when dependent tm c + match EConstr.kind sigma tm with + | Rel n when dependent sigma tm c && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, @@ -1889,21 +1947,21 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = let subst, len = List.fold_left (fun (subst, len) arg -> - match kind_of_term arg with - | Rel n when dependent arg c -> + match EConstr.kind sigma arg with + | Rel n when dependent sigma arg c -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent tm c && List.for_all isRel realargs + if dependent sigma tm c && List.for_all (isRel sigma) realargs then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) (List.rev tomatchs) arsign ([], nar) in let rec predicate lift c = - match kind_of_term c with + match EConstr.kind sigma c with | Rel n when n > lift -> (try (* Make the predicate dependent on the matched variable *) @@ -1913,7 +1971,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = (* A variable that is not matched, lift over the arsign. *) mkRel (n + nar)) | _ -> - map_constr_with_binders succ predicate lift c + EConstr.map_with_binders sigma succ predicate lift c in assert (len == 0); let p = predicate 0 c in @@ -1933,7 +1991,22 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = * tycon to make the predicate if it is not closed. *) -let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = +exception LocalOccur + +let noccur_with_meta sigma n m term = + let rec occur_rec n c = match EConstr.kind sigma c with + | Rel p -> if n<=p && p<n+m then raise LocalOccur + | App(f,cl) -> + (match EConstr.kind sigma f with + | Cast (c,_,_) when isMeta sigma c -> () + | Meta _ -> () + | _ -> EConstr.iter_with_binders sigma succ occur_rec n c) + | Evar (_, _) -> () + | _ -> EConstr.iter_with_binders sigma succ occur_rec n c + in + try (occur_rec n term; true) with LocalOccur -> false + +let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred = let refresh_tycon sigma t = (** If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe @@ -1941,16 +2014,17 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) env sigma t in + let typing_arsign,building_arsign = List.split arsign in let preds = match pred, tycon with (* No return clause *) - | None, Some t when not (noccur_with_meta 0 max_int t) -> + | None, Some t when not (noccur_with_meta sigma 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) (* First strategy: we abstract the tycon wrt to the dependencies *) let sigma, t = refresh_tycon sigma t in let p1 = - prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in + prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in (match p1 with @@ -1962,31 +2036,29 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let sigma,t = match tycon with | Some t -> refresh_tycon sigma t | None -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((t, _), sigma, _) = - new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in - let sigma = Sigma.to_evar_map sigma in + let (sigma, (t, _)) = + new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in sigma, t in (* First strategy: we build an "inversion" predicate *) let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in (* Second strategy: we directly use the evar as a non dependent pred *) - let pred2 = lift (List.length (List.flatten arsign)) t in + let pred2 = lift (List.length (List.flatten typing_arsign)) t in [sigma1, pred1; sigma, pred2] (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let envar = List.fold_right push_rel_context arsign env in + let envar = List.fold_right push_rel_context typing_arsign env in let sigma, newt = new_sort_variable univ_flexible_alg sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in let sigma = !evdref in - let predccl = (j_nf_evar sigma predcclj).uj_val in + let predccl = nf_evar sigma predcclj.uj_val in [sigma, predccl] in List.map (fun (sigma,pred) -> - let (nal,pred) = build_initial_predicate arsign pred in + let (nal,pred) = build_initial_predicate building_arsign pred in sigma,nal,pred) preds @@ -2011,7 +2083,7 @@ let prime avoid name = let make_prime avoid prevname = let previd, id = prime !avoid prevname in - avoid := id :: !avoid; + avoid := Id.Set.add id !avoid; previd, id let eq_id avoid id = @@ -2026,31 +2098,33 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = - GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false), +let hole na = DAst.make @@ + GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = - match pat with - | PatVar (l,name) -> + let loc = pat.CAst.loc in + match DAst.get pat with + | 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 + Name id, Id.Set.add id avoid in - (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((DAst.make ?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) - with Not_found -> error_case_not_inductive env + with Not_found -> error_case_not_inductive env !evdref {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in - if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; + let params = List.map EConstr.of_constr params in + 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 @@ -2058,7 +2132,7 @@ let constr_of_pat env evdref arsign pat avoid = let patargs, args, sign, env, n, m, avoid = List.fold_right2 (fun decl ua (patargs, args, sign, env, n, m, avoid) -> - let t = get_type decl in + let t = EConstr.of_constr (RelDecl.get_type decl) in let pat', sign', arg', typ', argtypargs, n', avoid = let liftt = liftn (List.length sign) (succ (List.length args)) t in typ env (substl args liftt, []) ua avoid @@ -2070,18 +2144,18 @@ 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 cstr = mkConstructU ci.cs_cstr in - let app = applistc cstr (List.map (lift (List.length sign)) params) in - let app = applistc app args in + let pat' = DAst.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 let apptype = Retyping.get_type_of env ( !evdref) app in - let IndType (indf, realargs) = find_rectype env ( !evdref) apptype in + let IndType (indf, realargs) = find_rectype env (!evdref) apptype in match alias with Anonymous -> pat', sign, app, apptype, realargs, n, avoid | Name id -> let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = id :: avoid in + let avoid = Id.Set.add id avoid in let sign, i, avoid = try let env = push_rel_context sign env in @@ -2092,58 +2166,61 @@ let constr_of_pat env evdref arsign pat avoid = (lift 1 app) (* aliased term *) in let neq = eq_id avoid id in - LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid + LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in - let pat', sign, patc, patty, args, z, avoid = typ env (get_type (List.hd arsign), List.tl arsign) pat avoid in - pat', (sign, patc, (get_type (List.hd arsign), args), pat'), avoid + let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in + pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid (* shadows functional version *) let eq_id avoid id = let hid = Id.of_string ("Heq_" ^ Id.to_string id) in let hid' = next_ident_away hid !avoid in - avoid := hid' :: !avoid; + avoid := Id.Set.add hid' !avoid; hid' -let is_topvar t = -match kind_of_term t with +let is_topvar sigma t = +match EConstr.kind sigma t with | Rel 0 -> true | _ -> false -let rels_of_patsign = +let rels_of_patsign sigma = List.map (fun decl -> match decl with - | LocalDef (na,t',t) when is_topvar t' -> LocalAssum (na,t) + | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) | _ -> decl) -let vars_of_ctx ctx = +let vars_of_ctx sigma ctx = let _, y = List.fold_right (fun decl (prev, vars) -> match decl with - | LocalDef (na,t',t) when is_topvar t' -> + | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (GApp (Loc.ghost, - (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), - [hole; GVar (Loc.ghost, prev)])) :: vars + (DAst.make @@ GApp ( + (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole na; DAst.make @@ GVar prev])) :: vars | _ -> - match get_name decl with + match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, GVar (Loc.ghost, n) :: vars) + | Name n -> n, (DAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = - match x, y with + match DAst.get x, DAst.get 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 +let lift_rel_context n l = + map_rel_context_with_binders (liftn n) l + (* liftsign is the current pattern's complete signature length. Hence pats is already typed in its full signature. However prevpatterns are in the original one signature per pattern form. @@ -2180,14 +2257,14 @@ let build_ineqs evdref prevpatterns pats liftsign = (Some ([], 0, 0, [])) eqnpats pats in match acc with None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c')) - (lift_rel_context liftsign sign) - in - conj :: c) + | Some (sign, len, _, c') -> + let sigma, conj = mk_coq_and !evdref c' in + let sigma, neg = mk_coq_not sigma conj in + let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in + evdref := sigma; conj :: c) [] prevpatterns in match diffs with [] -> None - | _ -> Some (mk_coq_and diffs) + | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj) let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let i = ref 0 in @@ -2199,7 +2276,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = (fun (idents, newpatterns, pats) pat arsign -> let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in (idents, pat' :: newpatterns, cpat :: pats)) - ([], [], []) eqn.patterns sign + (Id.Set.empty, [], []) eqn.patterns sign in let newpatterns = List.rev newpatterns and opats = List.rev pats in let rhs_rels, pats, signlen = @@ -2218,12 +2295,12 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = (* lift to get outside of past patterns to get terms in the combined environment. *) (fun (pats, n) (sign, c, (s, args), p) -> let len = List.length sign in - ((rels_of_patsign sign, lift n c, + ((rels_of_patsign !evdref sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n)) ([], 0) pats in let ineqs = build_ineqs evdref prevpatterns pats signlen in - let rhs_rels' = rels_of_patsign rhs_rels in + let rhs_rels' = rels_of_patsign !evdref rhs_rels in let _signenv = push_rel_context rhs_rels' env in let arity = let args, nargs = @@ -2241,7 +2318,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = | Some ineqs -> [LocalAssum (Anonymous, ineqs)], lift 1 arity in - let eqs_rels, arity = decompose_prod_n_assum neqs arity in + let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity in let rhs_env = push_rel_context rhs_rels' env in @@ -2252,13 +2329,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 = GVar (Loc.ghost, branch_name) in - match vars_of_ctx rhs_rels with + let bref = DAst.make @@ GVar branch_name in + match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> GApp (Loc.ghost, bref, l) + | l -> DAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> GApp (Loc.ghost, branch, [ hole ]) + Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; @@ -2287,27 +2364,27 @@ let lift_ctx n ctx = in ctx' (* Turn matched terms into variables. *) -let abstract_tomatch env tomatchs tycon = +let abstract_tomatch env sigma tomatchs tycon = let prev, ctx, names, tycon = List.fold_left (fun (prev, ctx, names, tycon) (c, t) -> let lenctx = List.length ctx in - match kind_of_term c with + match EConstr.kind sigma c with Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon | _ -> let tycon = Option.map - (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in + (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in let name = next_ident_away (Id.of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, - name :: names, tycon) - ([], [], [], tycon) tomatchs + Id.Set.add name names, tycon) + ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon let build_dependent_signature env evdref avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in - let allnames = List.rev_map (List.map get_name) arsign in + let allnames = List.rev_map (List.map RelDecl.get_name) arsign in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let eqs, neqs, refls, slift, arsign' = List.fold_left2 @@ -2324,14 +2401,14 @@ let build_dependent_signature env evdref avoid tomatchs arsign = as much as possible *) let argsign = List.tl arsign in (* arguments in inverse application order *) let app_decl = List.hd arsign in (* The matched argument *) - let appn = get_name app_decl in - let appt = get_type app_decl in + let appn = RelDecl.get_name app_decl in + let appt = RelDecl.get_type app_decl in let argsign = List.rev argsign in (* arguments in application order *) let env', nargeqs, argeqs, refl_args, slift, argsign' = List.fold_left2 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl -> - let name = get_name decl in - let t = get_type decl in + let name = RelDecl.get_name decl in + let t = RelDecl.get_type decl in let argt = Retyping.get_type_of env !evdref arg in let eq, refl_arg = if Reductionops.is_conv env !evdref argt t then @@ -2348,8 +2425,8 @@ let build_dependent_signature env evdref avoid tomatchs arsign = in let previd, id = let name = - match kind_of_term arg with - Rel n -> get_name (lookup_rel n env) + match EConstr.kind !evdref arg with + Rel n -> RelDecl.get_name (lookup_rel n env) | _ -> name in make_prime avoid name @@ -2358,7 +2435,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, refl_arg :: refl_args, pred slift, - set_name (Name id) decl :: argsign')) + RelDecl.set_name (Name id) decl :: argsign')) (env, neqs, [], [], slift, []) args argsign in let eq = mk_JMeq evdref @@ -2373,13 +2450,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign = succ nargeqs, refl_eq :: refl_args, pred slift, - ((set_name (Name id) app_decl :: argsign') :: arsigns)) + ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) | _ -> (* Non dependent inductive or not inductive, just use a regular equality *) let decl = match arsign with [x] -> x | _ -> assert(false) in - let name = get_name decl in + let name = RelDecl.get_name decl in let previd, id = make_prime avoid name in - let arsign' = set_name (Name id) decl in + let arsign' = RelDecl.set_name (Name id) decl in let tomatch_ty = type_of_tomatch ty in let eq = mk_eq evdref (lift nar tomatch_ty) @@ -2401,10 +2478,10 @@ let context_of_arsign l = l ([], 0) in x -let compile_program_cases loc style (typing_function, evdref) tycon env +let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar (predopt, tomatchl, eqns) = let typing_fun tycon env = function - | Some t -> typing_function tycon env evdref t + | Some t -> typing_function tycon env evdref lvar t | None -> Evarutil.evd_comb0 use_unit_judge evdref in (* We build the matrix of patterns and right-hand side *) @@ -2412,29 +2489,30 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in + let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in let tycon = valcon_of_tycon tycon in - let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in + let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in let env = push_rel_context tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = (* The arity signature *) - let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in + let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in + let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *) (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) - let avoid = [] in + let avoid = Id.Set.empty in build_dependent_signature env evdref avoid tomatchs arsign in let tycon, arity = + let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in match tycon' with - | None -> let ev = mkExistential env evdref in ev, ev + | None -> let ev = mkExistential env evdref in ev, lift nar ev | Some t -> let pred = match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with | Some (evd, pred) -> evdref := evd; pred | None -> - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t in Option.get tycon, pred in @@ -2468,25 +2546,26 @@ let compile_program_cases loc style (typing_function, evdref) tycon env List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in let dep_sign = - find_dependencies_signature + find_dependencies_signature !evdref (List.make (List.length typs) true) typs in let typs' = List.map3 (fun (tm,tmt) deps na -> - let deps = if not (isRel tm) then [] else deps in + let deps = if not (isRel !evdref tm) then [] else deps in ((tm,tmt),deps,na)) tomatchs dep_sign nal in let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in let typing_function tycon env evdref = function - | Some t -> typing_function tycon env evdref t + | Some t -> typing_function tycon env evdref lvar t | None -> evd_comb0 use_unit_judge evdref in let pb = { env = env; + lvar = lvar; evdref = evdref; pred = pred; tomatch = initial_pushed; @@ -2499,19 +2578,19 @@ let compile_program_cases loc style (typing_function, evdref) tycon env let j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in + let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = nf_evar !evdref tycon; } + uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); } in j (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = +let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) = if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then - compile_program_cases loc style (typing_fun, evdref) - tycon env (predopt, tomatchl, eqns) + compile_program_cases ?loc style (typing_fun, evdref) + tycon env lvar (predopt, tomatchl, eqns) else (* We build the matrix of patterns and right-hand side *) @@ -2519,15 +2598,15 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* We build the vector of terms to match consistently with the *) (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in + let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in (* If an elimination predicate is provided, we check it is compatible with the type of arguments to match; if none is provided, we build alternative possible predicates *) - let arsign = extract_arity_signature env tomatchs tomatchl in - let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in + let arsign = extract_arity_signature env predlvar tomatchs tomatchl in + let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) @@ -2543,14 +2622,14 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in let dep_sign = - find_dependencies_signature + find_dependencies_signature !evdref (List.make (List.length typs) true) typs in let typs' = List.map3 (fun (tm,tmt) deps na -> - let deps = if not (isRel tm) then [] else deps in + let deps = if not (isRel !evdref tm) then [] else deps in ((tm,tmt),deps,na)) tomatchs dep_sign nal in @@ -2558,13 +2637,14 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e (* A typing function that provides with a canonical term for absurd cases*) let typing_fun tycon env evdref = function - | Some t -> typing_fun tycon env evdref t + | Some t -> typing_fun tycon env evdref lvar t | None -> evd_comb0 use_unit_judge evdref in let myevdref = ref sigma in let pb = { env = env; + lvar = lvar; evdref = myevdref; pred = pred; tomatch = initial_pushed; @@ -2577,7 +2657,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e let j = compile pb in (* We coerce to the tycon (if an elim predicate was provided) *) - let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in + let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in evdref := !myevdref; j in |