diff options
Diffstat (limited to 'plugins/subtac/subtac_cases.ml')
-rw-r--r-- | plugins/subtac/subtac_cases.ml | 2023 |
1 files changed, 0 insertions, 2023 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml deleted file mode 100644 index 9ff8ba50..00000000 --- a/plugins/subtac/subtac_cases.ml +++ /dev/null @@ -1,2023 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Cases -open Util -open Names -open Nameops -open Term -open Termops -open Namegen -open Declarations -open Inductiveops -open Environ -open Sign -open Reductionops -open Typeops -open Type_errors -open Glob_term -open Retyping -open Pretype_errors -open Evarutil -open Evarconv -open Subtac_utils - -(************************************************************************) -(* Pattern-matching compilation (Cases) *) -(************************************************************************) - -(************************************************************************) -(* Configuration, errors and warnings *) - -open Pp - -let mssg_may_need_inversion () = - str "Found a matching with no clauses on a term unknown to have an empty inductive type" - -(* Utils *) -let make_anonymous_patvars = - list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous)) - -(* Environment management *) -let push_rels vars env = List.fold_right push_rel vars env - -(* 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 regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j - -let rec regeneralize_index i k t = match kind_of_term t with - | Rel j when j = i+k -> mkRel (k+1) - | Rel j when j < i+k -> t - | Rel j when j > i+k -> t - | _ -> map_constr_with_binders succ (regeneralize_index i) k t - -type alias_constr = - | DepAlias - | NonDepAlias - -let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) = - { uj_val = - (match d with - | DepAlias -> mkLetIn (na,deppat,t,j.uj_val) - | NonDepAlias -> - if (not (dependent (mkRel 1) j.uj_type)) - or (* A leaf: *) isRel deppat - then - (* The body of pat is not needed to type j - see *) - (* insert_aliases - and both deppat and nondeppat have the *) - (* same type, then one can freely substitute one by the other *) - subst1 nondeppat j.uj_val - else - (* The body of pat is not needed to type j but its value *) - (* is dependent in the type of j; our choice is to *) - (* enforce this dependency *) - mkLetIn (na,deppat,t,j.uj_val)); - uj_type = subst1 deppat j.uj_type } - -(**********************************************************************) -(* Structures used in compiling pattern-matching *) - -type rhs = - { rhs_env : env; - avoid_ids : identifier list; - it : glob_constr; - } - -type equation = - { patterns : cases_pattern list; - rhs : rhs; - alias_stack : name list; - eqn_loc : loc; - used : bool ref } - -type matrix = equation list - -(* 1st argument of IsInd is the original ind before extracting the summary *) -type tomatch_type = - | IsInd of types * inductive_type - | NotInd of constr option * types - -type tomatch_status = - | Pushed of ((constr * tomatch_type) * int list) - | Alias of (constr * constr * alias_constr * constr) - | Abstract of rel_declaration - -type tomatch_stack = tomatch_status list - -(* The type [predicate_signature] types the terms to match and the rhs: - - - [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]), - if dep<>Anonymous, the term is dependent, let n=|names|, if - n<>0 then the type of the pushed term is necessarily an - inductive with n real arguments. Otherwise, it may be - non inductive, or inductive without real arguments, or inductive - originating from a subterm in which case real args are not dependent; - it accounts for n+1 binders if dep or n binders if not dep - - [PrProd] types abstracted term ([Abstract]); it accounts for one binder - - [PrCcl] types the right-hand side - - Aliases [Alias] have no trace in [predicate_signature] -*) - -type predicate_signature = - | PrLetIn of (name list * name) * predicate_signature - | PrProd of predicate_signature - | PrCcl of constr - -(* We keep a constr for aliases and a cases_pattern for error message *) - -type alias_builder = - | AliasLeaf - | AliasConstructor of constructor - -type pattern_history = - | Top - | MakeAlias of alias_builder * pattern_continuation - -and pattern_continuation = - | Continuation of int * cases_pattern list * pattern_history - | Result of cases_pattern list - -let start_history n = Continuation (n, [], Top) - -let feed_history arg = function - | Continuation (n, l, h) when n>=1 -> - Continuation (n-1, arg :: l, h) - | Continuation (n, _, _) -> - anomaly ("Bad number of expected remaining patterns: "^(string_of_int n)) - | Result _ -> - anomaly "Exhausted pattern history" - -(* This is for non exhaustive error message *) - -let rec glob_pattern_of_partial_history args2 = function - | Continuation (n, args1, h) -> - let args3 = make_anonymous_patvars (n - (List.length args2)) in - build_glob_pattern (List.rev_append args1 (args2@args3)) h - | Result pl -> pl - -and build_glob_pattern args = function - | Top -> args - | MakeAlias (AliasLeaf, rh) -> - assert (args = []); - glob_pattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh - | MakeAlias (AliasConstructor pci, rh) -> - glob_pattern_of_partial_history - [PatCstr (dummy_loc, pci, args, Anonymous)] rh - -let complete_history = glob_pattern_of_partial_history [] - -(* This is to build glued pattern-matching history and alias bodies *) - -let rec simplify_history = function - | Continuation (0, l, Top) -> Result (List.rev l) - | Continuation (0, l, MakeAlias (f, rh)) -> - let pargs = List.rev l in - let pat = match f with - | AliasConstructor pci -> - PatCstr (dummy_loc,pci,pargs,Anonymous) - | AliasLeaf -> - assert (l = []); - PatVar (dummy_loc, Anonymous) in - feed_history pat rh - | h -> h - -(* Builds a continuation expecting [n] arguments and building [ci] applied - to this [n] arguments *) - -let push_history_pattern n current cont = - Continuation (n, [], MakeAlias (current, cont)) - -(* A pattern-matching problem has the following form: - - env, isevars |- <pred> Cases tomatch of mat end - - where tomatch is some sequence of "instructions" (t1 ... tn) - - and mat is some matrix - (p11 ... p1n -> rhs1) - ( ... ) - (pm1 ... pmn -> rhsm) - - Terms to match: there are 3 kinds of instructions - - - "Pushed" terms to match are typed in [env]; these are usually just - Rel(n) except for the initial terms given by user and typed in [env] - - "Abstract" instructions means an abstraction has to be inserted in the - current branch to build (this means a pattern has been detected dependent - in another one and generalisation is necessary to ensure well-typing) - - "Alias" instructions means an alias has to be inserted (this alias - is usually removed at the end, except when its type is not the - same as the type of the matched term from which it comes - - typically because the inductive types are "real" parameters) - - Right-hand-sides: - - They consist of a raw term to type in an environment specific to the - clause they belong to: the names of declarations are those of the - variables present in the patterns. Therefore, they come with their - own [rhs_env] (actually it is the same as [env] except for the names - of variables). - -*) -type pattern_matching_problem = - { env : env; - isevars : Evd.evar_map ref; - pred : predicate_signature option; - tomatch : tomatch_stack; - history : pattern_continuation; - mat : matrix; - caseloc : loc; - casestyle: case_style; - typing_function: type_constraint -> env -> glob_constr -> unsafe_judgment } - -(*--------------------------------------------------------------------------* - * A few functions to infer the inductive type from the patterns instead of * - * checking that the patterns correspond to the ind. type of the * - * destructurated object. Allows type inference of examples like * - * match n with O => true | _ => false end * - * match x in I with C => true | _ => false end * - *--------------------------------------------------------------------------*) - -(* Computing the inductive type from the matrix of patterns *) - -(* We use the "in I" clause to coerce the terms to match and otherwise - use the constructor to know in which type is the matching problem - - Note that insertion of coercions inside nested patterns is done - each time the matrix is expanded *) - -let rec find_row_ind = function - [] -> None - | PatVar _ :: l -> find_row_ind l - | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) - -let inductive_template isevars env tmloc ind = - let arsign = get_full_arity_sign env ind in - let hole_source = match tmloc with - | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i)) - | None -> fun _ -> (dummy_loc, Evd.InternalHole) in - let (_,evarl,_) = - List.fold_right - (fun (na,b,ty) (subst,evarl,n) -> - match b with - | None -> - let ty' = substl subst ty in - let e = e_new_evar isevars env ~src:(hole_source n) ty' in - (e::subst,e::evarl,n+1) - | Some b -> - (b::subst,evarl,n+1)) - arsign ([],[],1) in - applist (mkInd ind,List.rev evarl) - - -(************************************************************************) -(* Utils *) - -let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars = - e_new_evar isevars env ~src:src (new_Type ()) - -let evd_comb2 f isevars x y = - let (evd',y) = f !isevars x y in - isevars := evd'; - y - -let context_of_arsign l = - let (x, _) = List.fold_right - (fun c (x, n) -> - (lift_rel_context n c @ x, List.length c + n)) - l ([], 0) - in x - -(* We put the tycon inside the arity signature, possibly discovering dependencies. *) - -let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in - let subst, len = - List.fold_left2 (fun (subst, len) (tm, tmtype) sign -> - let signlen = List.length sign in - match kind_of_term tm with - | Rel n when dependent tm c - && 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, - maybe some variable in its type appears in the tycon. *) -> - (match tmtype with - | NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *) - | IsInd (_, IndType(indf,realargs)) -> - let subst = - if dependent tm c && List.for_all isRel realargs - then (n, 1) :: subst else subst - in - List.fold_left - (fun (subst, len) arg -> - match kind_of_term arg with - | Rel n when dependent arg c -> - ((n, len) :: subst, pred len) - | _ -> (subst, pred len)) - (subst, len) realargs) - | _ -> (subst, len - signlen)) - ([], nar) tomatchs arsign - in - let rec predicate lift c = - match kind_of_term c with - | Rel n when n > lift -> - (try - (* Make the predicate dependent on the matched variable *) - let idx = List.assoc (n - lift) subst in - mkRel (idx + lift) - with Not_found -> - (* A variable that is not matched, lift over the arsign. *) - mkRel (n + nar)) - | _ -> - map_constr_with_binders succ predicate lift c - in - try - (* The tycon may be ill-typed after abstraction. *) - let pred = predicate 0 c in - let env' = push_rel_context (context_of_arsign arsign) env in - ignore(Typing.sort_of env' evm pred); pred - with e when Errors.noncritical e -> lift nar c - -module Cases_F(Coercion : Coercion.S) : S = struct - -let inh_coerce_to_ind isevars env ty tyi = - let expected_typ = inductive_template isevars env None tyi in - (* devrait être indifférent d'exiger leq ou pas puisque pour - un inductif cela doit être égal *) - let _ = e_cumul env isevars expected_typ ty in () - -let unify_tomatch_with_patterns isevars env loc typ pats = - match find_row_ind pats with - | None -> NotInd (None,typ) - | Some (_,(ind,_)) -> - inh_coerce_to_ind isevars env typ ind; - try IsInd (typ,find_rectype env ( !isevars) typ) - with Not_found -> NotInd (None,typ) - -let find_tomatch_tycon isevars env loc = function - (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind) - | None -> empty_tycon - -let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_glob_constr tomatch) in - let tycon = find_tomatch_tycon isevars env loc indopt in - let j = typing_fun tycon env tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !isevars j in - isevars := evd; - let typ = nf_evar ( !isevars) j.uj_type in - let t = - try IsInd (typ,find_rectype env ( !isevars) typ) - with Not_found -> - unify_tomatch_with_patterns isevars env loc typ pats in - (j.uj_val,t) - -let coerce_to_indtype typing_fun isevars env 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 isevars env) matx' tomatchl - - - -let adjust_tomatch_to_pattern pb ((current,typ),deps) = - (* Ideally, we could find a common inductive type to which both the - term to match and the patterns coerce *) - (* In practice, we coerce the term to match if it is not already an - inductive type and it is not dependent; moreover, we use only - the first pattern type and forget about the others *) - let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in - let typ = - try IsInd (typ,find_rectype pb.env ( !(pb.isevars)) typ) - with Not_found -> NotInd (None,typ) in - let tomatch = ((current,typ),deps) in - match typ with - | NotInd (None,typ) -> - let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in - (match find_row_ind tm1 with - | None -> tomatch - | Some (_,(ind,_)) -> - let indt = inductive_template pb.isevars pb.env None ind in - let current = - if deps = [] & isEvar typ then - (* Don't insert coercions if dependent; only solve evars *) - let _ = e_cumul pb.env pb.isevars indt typ in - current - else - (evd_comb2 (Coercion.inh_conv_coerce_to true dummy_loc pb.env) - pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in - let sigma = !(pb.isevars) in - let typ = IsInd (indt,find_rectype pb.env sigma indt) in - ((current,typ),deps)) - | _ -> tomatch - - (* extract some ind from [t], possibly coercing from constructors in [tm] *) -let to_mutind env isevars tm c t = -(* match c with - | Some body -> *) NotInd (c,t) -(* | None -> unify_tomatch_with_patterns isevars env t tm*) - -let type_of_tomatch = function - | IsInd (t,_) -> t - | NotInd (_,t) -> t - -let mkDeclTomatch na = function - | IsInd (t,_) -> (na,None,t) - | NotInd (c,t) -> (na,c,t) - -let map_tomatch_type f = function - | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (Option.map f c, f t) - -let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) -let lift_tomatch_type n = liftn_tomatch_type n 1 - -(**********************************************************************) -(* Utilities on patterns *) - -let current_pattern eqn = - match eqn.patterns with - | pat::_ -> pat - | [] -> anomaly "Empty list of patterns" - -let alias_of_pat = function - | PatVar (_,name) -> name - | PatCstr(_,_,_,name) -> name - -let remove_current_pattern eqn = - match eqn.patterns with - | pat::pats -> - { eqn with - patterns = pats; - alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly "Empty list of patterns" - -let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } - -(**********************************************************************) -(* Well-formedness tests *) -(* Partial check on patterns *) - -exception NotAdjustable - -let rec adjust_local_defs loc = function - | (pat :: pats, (_,None,_) :: decls) -> - pat :: adjust_local_defs loc (pats,decls) - | (pats, (_,Some _,_) :: decls) -> - PatVar (loc, 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 -> - (* Check it is constructor of the right type *) - let ind' = inductive_of_constructor cstr in - if Names.eq_ind ind' ind then - (* Check the constructor has the right number of args *) - let ci = cstrs.(i-1) in - let nb_args_constr = ci.cs_nargs in - if 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) - with NotAdjustable -> - error_wrong_numarg_constructor_loc loc (Global.env()) - cstr nb_args_constr - else - (* Try to insert a coercion *) - try - Coercion.inh_pattern_coerce_to loc pat ind' ind - with Not_found -> - error_bad_constructor_loc loc cstr ind - -let check_all_variables typ mat = - List.iter - (fun eqn -> match current_pattern eqn with - | PatVar (_,id) -> () - | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern_loc loc cstr_sp typ) - mat - -let check_unused_pattern env eqn = - if not !(eqn.used) then - raise_pattern_matching_error - (eqn.eqn_loc, env, UnusedClause eqn.patterns) - -let set_used_pattern eqn = eqn.used := true - -let extract_rhs pb = - match pb.mat with - | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion()) - | eqn::_ -> - set_used_pattern eqn; - eqn.rhs - -(**********************************************************************) -(* Functions to deal with matrix factorization *) - -let occur_in_rhs na rhs = - match na with - | Anonymous -> false - | Name id -> occur_glob_constr id rhs.it - -let is_dep_patt eqn = function - | PatVar (_,name) -> occur_in_rhs name eqn.rhs - | PatCstr _ -> true - -let dependencies_in_rhs nargs eqns = - if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *) - else - let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in - let columns = matrix_transpose deps in - List.map (List.exists ((=) true)) columns - -let dependent_decl a = function - | (na,None,t) -> dependent a t - | (na,Some c,t) -> dependent a t || dependent a c - -(* Computing the matrix of dependencies *) - -(* We are in context d1...dn |- and [find_dependencies k 1 nextlist] - computes for declaration [k+1] in which of declarations in - [nextlist] (which corresponds to d(k+2)...dn) it depends; - declarations 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 k n = function - | [] -> [] - | (used,tdeps,d)::rest -> - let deps = find_dependency_list k (n+1) rest in - if used && dependent_decl (mkRel n) d - then list_add_set (List.length rest + 1) (list_union deps tdeps) - else deps - -let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) = - let deps = find_dependency_list k 1 nextlist in - if is_dep_or_cstr_in_rhs || deps <> [] - then (k-1,(true ,deps,d)::nextlist) - else (k-1,(false,[] ,d)::nextlist) - -let find_dependencies_signature deps_in_rhs typs = - let k = List.length deps_in_rhs in - let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in - List.map (fun (_,deps,_) -> deps) l - -(******) - -(* A Pushed term to match has just been substituted by some - constructor t = (ci x1...xn) and the terms x1 ... xn have been added to - match - - - all terms to match and to push (dependent on t by definition) - must have (Rel depth) substituted by t and Rel's>depth lifted by n - - all pushed terms to match (non dependent on t by definition) must - be lifted by n - - We start with depth=1 -*) - -let regeneralize_index_tomatch n = - let rec genrec depth = function - | [] -> [] - | Pushed ((c,tm),l)::rest -> - let c = regeneralize_index n depth c in - let tm = map_tomatch_type (regeneralize_index n depth) tm in - let l = List.map (regeneralize_rel n depth) l in - Pushed ((c,tm),l)::(genrec depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (regeneralize_index n depth c1,c2,d,t)::(genrec depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (regeneralize_index n depth) d) - ::(genrec (depth+1) rest) in - genrec 0 - -let rec replace_term n c k t = - if isRel t && destRel t = n+k then lift k c - else map_constr_with_binders succ (replace_term n c) k t - -let replace_tomatch n c = - let rec replrec depth = function - | [] -> [] - | Pushed ((b,tm),l)::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 i=n+depth then anomaly "replace_tomatch") l; - Pushed ((b,tm),l)::(replrec depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (replace_term n c depth c1,c2,d,t)::(replrec depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (replace_term n c depth) d) - ::(replrec (depth+1) rest) in - replrec 0 - -let rec liftn_tomatch_stack n depth = function - | [] -> [] - | Pushed ((c,tm),l)::rest -> - let c = liftn n depth c in - let tm = liftn_tomatch_type n depth tm in - let l = List.map (fun i -> if i<depth then i else i+n) l in - Pushed ((c,tm),l)::(liftn_tomatch_stack n depth rest) - | Alias (c1,c2,d,t)::rest -> - Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t) - ::(liftn_tomatch_stack n depth rest) - | Abstract d::rest -> - Abstract (map_rel_declaration (liftn n depth) d) - ::(liftn_tomatch_stack n (depth+1) rest) - - -let lift_tomatch_stack n = liftn_tomatch_stack n 1 - -(* if [current] has type [I(p1...pn u1...um)] and we consider the case - of constructor [ci] of type [I(p1...pn u'1...u'm)], then the - default variable [name] is expected to have which type? - Rem: [current] is [(Rel i)] except perhaps for initial terms to match *) - -(************************************************************************) -(* Some heuristics to get names for variables pushed in pb environment *) -(* Typical requirement: - - [match y with (S (S x)) => x | x => x end] should be compiled into - [match y with O => y | (S n) => match n with O => y | (S x) => x end end] - - and [match y with (S (S n)) => n | n => n end] into - [match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end] - - i.e. user names should be preserved and created names should not - interfere with user names *) - -let merge_name get_name obj = function - | Anonymous -> get_name obj - | na -> na - -let merge_names get_name = List.map2 (merge_name get_name) - -let get_names env sign eqns = - let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in - (* If any, we prefer names used in pats, from top to bottom *) - let names2 = - List.fold_right - (fun (pats,eqn) names -> merge_names alias_of_pat pats names) - eqns names1 in - (* 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 l eqn.rhs.avoid_ids) [] eqns in - let names4,_ = - List.fold_left2 - (fun (l,avoid) d na -> - let na = - merge_name - (fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid)) - d na - in - (na::l,(out_name na)::avoid)) - ([],allvars) (List.rev sign) names2 in - names4 - -(************************************************************************) -(* Recovering names for variables pushed to the rhs' environment *) - -let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t)) - -let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in - (n, b, t)) sign - -let push_rels_eqn sign eqn = - let sign = all_name sign in - {eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } } - -let push_rels_eqn_with_names sign eqn = - let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in - let sign = recover_alias_names alias_of_pat pats sign in - push_rels_eqn sign eqn - -let build_aliases_context env sigma names allpats pats = - (* pats is the list of bodies to push as an alias *) - (* They all are defined in env and we turn them into a sign *) - (* cuts in sign need to be done in allpats *) - let rec insert env sign1 sign2 n newallpats oldallpats = function - | (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) -> - (* Anonymous leaves must be considered named and treated in the *) - (* next clause because they may occur in implicit arguments *) - insert env sign1 sign2 - n newallpats (List.map List.tl oldallpats) (pats,names) - | (deppat,nondeppat,d,t)::pats, na::names -> - let nondeppat = lift n nondeppat in - let deppat = lift n deppat in - let newallpats = - List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in - let oldallpats = List.map List.tl oldallpats in - let decl = (na,Some deppat,t) in - let a = (deppat,nondeppat,d,t) in - insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1) - newallpats oldallpats (pats,names) - | [], [] -> newallpats, sign1, sign2, env - | _ -> anomaly "Inconsistent alias and name lists" in - let allpats = List.map (fun x -> [x]) allpats - in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names) - -let insert_aliases_eqn sign eqnnames alias_rest eqn = - let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in - push_rels_eqn thissign { eqn with alias_stack = alias_rest; } - - -let insert_aliases env sigma alias eqns = - (* Là, y a une faiblesse, si un alias est utilisé dans un cas par *) - (* défaut présent mais inutile, ce qui est le cas général, l'alias *) - (* est introduit même s'il n'est pas utilisé dans les cas réguliers *) - let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in - let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in - (* names2 takes the meet of all needed aliases *) - let names2 = - List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in - (* Only needed aliases are kept by build_aliases_context *) - let eqnsnames, sign1, sign2, env = - build_aliases_context env sigma [names2] eqnsnames [alias] in - let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in - sign2, env, eqns - -(**********************************************************************) -(* Functions to deal with elimination predicate *) - -exception Occur -let noccur_between_without_evar n m term = - let rec occur_rec n c = match kind_of_term c with - | Rel p -> if n<=p && p<n+m then raise Occur - | Evar (_,cl) -> () - | _ -> iter_constr_with_binders succ occur_rec n c - in - try occur_rec n term; true with Occur -> false - -(* Inferring the predicate *) -let prepare_unif_pb typ cs = - let n = List.length (assums_of_rel_context cs.cs_args) in - - (* We may need to invert ci if its parameters occur in typ *) - let typ' = - if noccur_between_without_evar 1 n typ then lift (-n) typ - else (* TODO4-1 *) - error "Unable to infer return clause of this pattern-matching problem" in - let args = extended_rel_list (-n) cs.cs_args in - let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in - - (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = typ' *) - (Array.map (lift (-n)) cs.cs_concl_realargs, ci, typ') - - -(* Infering the predicate *) -(* -The problem to solve is the following: - -We match Gamma |- t : I(u01..u0q) against the following constructors: - - Gamma, x11...x1p1 |- C1(x11..x1p1) : I(u11..u1q) - ... - Gamma, xn1...xnpn |- Cn(xn1..xnp1) : I(un1..unq) - -Assume the types in the branches are the following - - Gamma, x11...x1p1 |- branch1 : T1 - ... - Gamma, xn1...xnpn |- branchn : Tn - -Assume the type of the global case expression is Gamma |- T - -The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy -the following n+1 equations: - - Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1)) = T1 - ... - Gamma, xn1...xnpn |- (phi un1..unq (Cn xn1..xnpn)) = Tn - Gamma |- (phi u01..u0q t) = T - -Some hints: - -- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..." - should be inserted somewhere in Ti. - -- If T is undefined, an easy solution is to insert a "match z with (Ci - xi1..xipi) => ..." in front of each Ti - -- Otherwise, T1..Tn and T must be step by step unified, if some of them - diverge, then try to replace the diverging subterm by one of y1..yq or z. - -- The main problem is what to do when an existential variables is encountered - -let prepare_unif_pb typ cs = - let n = cs.cs_nargs in - let _,p = decompose_prod_n n typ in - let ci = build_dependent_constructor cs in - (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *) - (n, cs.cs_concl_realargs, ci, p) - -let eq_operator_lift k (n,n') = function - | OpRel p, OpRel p' when p > k & p' > k -> - if p < k+n or p' < k+n' then false else p - n = p' - n' - | op, op' -> op = op' - -let rec transpose_args n = - if n=0 then [] - else - (Array.map (fun l -> List.hd l) lv):: - (transpose_args (m-1) (Array.init (fun l -> List.tl l))) - -let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k - -let reloc_operator (k,n) = function OpRel p when p > k -> -let rec unify_clauses k pv = - let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) ( isevars)) p) pv in - let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in - if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv' - then - let argvl = transpose_args (List.length args1) pv' in - let k' = shift_operator k op1 in - let argl = List.map (unify_clauses k') argvl in - gather_constr (reloc_operator (k,n1) op1) argl -*) - -let abstract_conclusion typ cs = - let n = List.length (assums_of_rel_context cs.cs_args) in - let (sign,p) = decompose_prod_n n typ in - it_mkLambda p sign - -let infer_predicate loc env isevars typs cstrs indf = - (* Il faudra substituer les isevars a un certain moment *) - if Array.length cstrs = 0 then (* "TODO4-3" *) - error "Inference of annotation for empty inductive types not implemented" - else - (* Empiric normalization: p may depend in a irrelevant way on args of the*) - (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *) - let typs = - Array.map (local_strong whd_beta ( !isevars)) typs - in - let eqns = array_map2 prepare_unif_pb typs cstrs in - (* First strategy: no dependencies at all *) -(* - let (mis,_) = dest_ind_family indf in - let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in -*) - let (sign,_) = get_arity env indf in - let mtyp = - if array_exists is_Type typs then - (* Heuristic to avoid comparison between non-variables algebric univs*) - new_Type () - else - mkExistential env ~src:(loc, Evd.CasesType) isevars - in - if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns - then - (* Non dependent case -> turn it into a (dummy) dependent one *) - let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in - let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in - (true,pred) (* true = dependent -- par défaut *) - else -(* - let s = get_sort_of env ( isevars) typs.(0) in - let predpred = it_mkLambda_or_LetIn (mkSort s) sign in - let caseinfo = make_default_case_info mis in - let brs = array_map2 abstract_conclusion typs cstrs in - let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in - let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in -*) - (* "TODO4-2" *) - (* We skip parameters *) - let cis = - Array.map - (fun cs -> - applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args)) - cstrs in - let ct = array_map2 (fun ci (_,_,t) -> (ci,t)) cis eqns in - raise_pattern_matching_error (loc,env, CannotInferPredicate ct) -(* - (true,pred) -*) - -(* Propagation of user-provided predicate through compilation steps *) - -let rec map_predicate f k = function - | PrCcl ccl -> PrCcl (f k ccl) - | PrProd pred -> - PrProd (map_predicate f (k+1) pred) - | PrLetIn ((names,dep as tm),pred) -> - let k' = List.length names + (if dep<>Anonymous then 1 else 0) in - PrLetIn (tm, map_predicate f (k+k') pred) - -let rec noccurn_predicate k = function - | PrCcl ccl -> noccurn k ccl - | PrProd pred -> noccurn_predicate (k+1) pred - | PrLetIn ((names,dep),pred) -> - let k' = List.length names + (if dep<>Anonymous then 1 else 0) in - noccurn_predicate (k+k') pred - -let liftn_predicate n = map_predicate (liftn n) - -let lift_predicate n = liftn_predicate n 1 - -let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0 - -let substnl_predicate sigma = map_predicate (substnl sigma) - -(* This is parallel bindings *) -let subst_predicate (args,copt) pred = - let sigma = match copt with - | None -> List.rev args - | Some c -> c::(List.rev args) in - substnl_predicate sigma 0 pred - -let specialize_predicate_var (cur,typ) = function - | PrProd _ | PrCcl _ -> - anomaly "specialize_predicate_var: a pattern-variable must be pushed" - | PrLetIn (([],dep),pred) -> - subst_predicate ([],if dep<>Anonymous then Some cur else None) pred - | PrLetIn ((_,dep),pred) -> - (match typ with - | IsInd (_,IndType (_,realargs)) -> - subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred - | _ -> anomaly "specialize_predicate_var") - -let ungeneralize_predicate = function - | PrLetIn _ | PrCcl _ -> anomaly "ungeneralize_predicate: expects a product" - | PrProd pred -> pred - -(*****************************************************************************) -(* We have pred = [X:=realargs;x:=c]P typed in Gamma1, x:I(realargs), Gamma2 *) -(* and we want to abstract P over y:t(x) typed in the same context to get *) -(* *) -(* pred' = [X:=realargs;x':=c](y':t(x'))P[y:=y'] *) -(* *) -(* 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 ny d = function - | PrLetIn ((names,dep as tm),pred) -> - if dep=Anonymous then anomaly "Undetected dependency"; - let p = List.length names + 1 in - let pred = lift_predicate 1 pred in - let pred = regeneralize_index_predicate (ny+p+1) pred in - PrLetIn (tm, PrProd pred) - | PrProd _ | PrCcl _ -> - anomaly "generalize_predicate: expects a non trivial pattern" - -let rec extract_predicate l = function - | pred, Alias (deppat,nondeppat,_,_)::tms -> - let tms' = match kind_of_term nondeppat with - | Rel i -> replace_tomatch i deppat tms - | _ -> (* initial terms are not dependent *) tms in - extract_predicate l (pred,tms') - | PrProd pred, Abstract d'::tms -> - let d' = map_rel_declaration (lift (List.length l)) d' in - substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms))) - | PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms -> - extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) - | PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms -> - let l = List.rev realargs@l in - extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms) - | PrCcl ccl, [] -> - substl l ccl - | _ -> anomaly"extract_predicate: predicate inconsistent with terms to match" - -let abstract_predicate env sigma indf cur tms = function - | (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn" - | PrLetIn ((names,dep),pred) -> - let sign = make_arity_signature env true indf in - (* n is the number of real args + 1 *) - let n = List.length sign in - let tms = lift_tomatch_stack n tms in - let tms = - match kind_of_term cur with - | Rel i -> regeneralize_index_tomatch (i+n) tms - | _ -> (* Initial case *) tms in - (* Depending on whether the predicate is dependent or not, and has real - args or not, we lift it to make room for [sign] *) - (* Even if not intrinsically dep, we move the predicate into a dep one *) - let sign,k = - if names = [] & n <> 1 then - (* Real args were not considered *) - (if dep<>Anonymous then - ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) - else - (sign,n)) - else - (* Real args are OK *) - (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, - if dep<>Anonymous then 0 else 1) in - let pred = lift_predicate k pred in - let pred = extract_predicate [] (pred,tms) in - (true, it_mkLambda_or_LetIn_name env pred sign) - -let rec known_dependent = function - | None -> false - | Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous - | Some (PrCcl _) -> false - | Some (PrProd _) -> - anomaly "known_dependent: can only be used when patterns remain" - -(* [expand_arg] is used by [specialize_predicate] - it replaces gamma, x1...xn, x1...xk |- pred - by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or - by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *) - -let expand_arg n alreadydep (na,t) deps (k,pred) = - (* current can occur in pred even if the original problem is not dependent *) - let dep = - if alreadydep<>Anonymous then alreadydep - else if deps = [] && noccurn_predicate 1 pred then Anonymous - else Name (id_of_string "x") in - let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in - (* There is no dependency in realargs for subpattern *) - (k-1, PrLetIn (([],dep), pred)) - - -(*****************************************************************************) -(* pred = [X:=realargs;x:=c]P types the following problem: *) -(* *) -(* Gamma |- match Pushed(c:I(realargs)) rest with...end: pred *) -(* *) -(* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi) *) -(* is considered. Assume each Ti is some Ii(argsi). *) -(* We let e=Ci(x1,...,xn) and replace pred by *) -(* *) -(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *) -(* *) -(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*) -(* *) -(*****************************************************************************) -let specialize_predicate tomatchs deps cs = function - | (PrProd _ | PrCcl _) -> - anomaly "specialize_predicate: a matched pattern must be pushed" - | PrLetIn ((names,isdep),pred) -> - (* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *) - let nrealargs = List.length names in - let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in - (* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *) - let n = cs.cs_nargs in - let pred' = liftn_predicate n (k+1) pred in - let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in - let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in - (* The substituends argsi, copti are all defined in gamma, x1...xn *) - (* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *) - let pred'' = subst_predicate (argsi, copti) pred' in - (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *) - let pred''' = liftn_predicate n (n+1) pred'' in - (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*) - snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred''')) - -let find_predicate loc env isevars p typs cstrs current - (IndType (indf,realargs)) tms = - let (dep,pred) = - match p with - | Some p -> abstract_predicate env ( !isevars) indf current tms p - | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta ( !isevars) (applist (pred, realargs)) in - if dep then - (pred, whd_beta ( !isevars) (applist (typ, [current])), - new_Type ()) - else - (pred, typ, new_Type ()) - -(************************************************************************) -(* Sorting equations by constructor *) - -type inversion_problem = - (* the discriminating arg in some Ind and its order in Ind *) - | Incompatible of int * (int * int) - | Constraints of (int * constr) list - -let solve_constraints constr_info indt = - (* TODO *) - Constraints [] - -let rec irrefutable env = function - | 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 = Array.length mip.mind_user_lc = 1 in - one_constr & List.for_all (irrefutable env) args - -let first_clause_irrefutable env = function - | eqn::mat -> List.for_all (irrefutable env) eqn.patterns - | _ -> false - -let group_equations pb ind current cstrs mat = - let mat = - if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in - let brs = Array.create (Array.length cstrs) [] in - let only_default = ref true in - let _ = - List.fold_right (* To be sure it's from bottom to top *) - (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) -> - (* This is a default clause that we expand *) - for i=1 to Array.length cstrs do - let n = cstrs.(i-1).cs_nargs in - let args = make_anonymous_patvars n in - brs.(i-1) <- (args, rest) :: brs.(i-1) - done - | PatCstr (loc,((_,i)),args,_) -> - (* This is a regular clause *) - only_default := false; - brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in - (brs,!only_default) - -(************************************************************************) -(* Here starts the pattern-matching compilation algorithm *) - -(* Abstracting over dependent subterms to match *) -let rec generalize_problem pb = function - | [] -> pb - | i::l -> - let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in - let pb' = generalize_problem pb l in - let tomatch = lift_tomatch_stack 1 pb'.tomatch in - let tomatch = regeneralize_index_tomatch (i+1) tomatch in - { pb with - tomatch = Abstract d :: tomatch; - pred = Option.map (generalize_predicate i d) pb'.pred } - -(* No more patterns: typing the right-hand side of equations *) -let build_leaf pb = - let rhs = extract_rhs pb in - let tycon = match pb.pred with - | None -> anomaly "Predicate not found" - | Some (PrCcl typ) -> mk_tycon typ - | Some _ -> anomaly "not all parameters of pred have been consumed" in - pb.typing_function tycon rhs.rhs_env rhs.it - -(* Building the sub-problem when all patterns are variables *) -let shift_problem (current,t) pb = - {pb with - tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = Option.map (specialize_predicate_var (current,t)) pb.pred; - history = push_history_pattern 0 AliasLeaf pb.history; - mat = List.map remove_current_pattern pb.mat } - -(* Building the sub-pattern-matching problem for a given branch *) -let build_branch current deps pb eqns const_info = - (* We remember that we descend through a constructor *) - let alias_type = - if Array.length const_info.cs_concl_realargs = 0 - & not (known_dependent pb.pred) & deps = [] - then - NonDepAlias - else - DepAlias - in - let history = - push_history_pattern const_info.cs_nargs - (AliasConstructor const_info.cs_cstr) - pb.history in - - (* We find matching clauses *) - let cs_args = (*assums_of_rel_context*) const_info.cs_args in - let names = get_names pb.env cs_args eqns in - let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in - if submat = [] then - raise_pattern_matching_error - (dummy_loc, pb.env, NonExhaustive (complete_history history)); - let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in - let _,typs',_ = - List.fold_right - (fun (na,c,t as d) (env,typs,tms) -> - let tm1 = List.map List.hd tms in - let tms = List.map List.tl tms in - (push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms)) - typs (pb.env,[],List.map fst eqns) in - - let dep_sign = - find_dependencies_signature - (dependencies_in_rhs const_info.cs_nargs 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 - - (* We replace [(mkRel 1)] by its expansion [ci] *) - (* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *) - (* This is done in two steps : first from "Gamma |- tms" *) - (* into "Gamma; typs; curalias |- tms" *) - let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in - - let currents = - list_map2_i - (fun i (na,t) deps -> Pushed ((mkRel i, lift_tomatch_type i t), deps)) - 1 typs' (List.rev dep_sign) in - - let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in - let ind = - appvect ( - applist (mkInd (inductive_of_constructor const_info.cs_cstr), - List.map (lift const_info.cs_nargs) const_info.cs_params), - const_info.cs_concl_realargs) in - - let cur_alias = lift (List.length sign) current in - let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in - let env' = push_rels sign pb.env in - let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in - sign, - { pb with - env = env'; - tomatch = List.rev_append currents tomatch; - pred = pred'; - history = history; - mat = List.map (push_rels_eqn_with_names sign) submat } - -(********************************************************************** - INVARIANT: - - pb = { env, subst, tomatch, mat, ...} - tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T) - - "Pushed" terms and types are relative to env - "Abstract" types are relative to env enriched by the previous terms to match - -*) - -(**********************************************************************) -(* Main compiling descent *) -let rec compile pb = - match pb.tomatch with - | (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur - | (Alias x)::rest -> compile_alias pb x rest - | (Abstract d)::rest -> compile_generalization pb d rest - | [] -> build_leaf pb - -and match_current pb tomatch = - let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in - match typ with - | NotInd (_,typ) -> - check_all_variables typ pb.mat; - compile (shift_problem ct pb) - | IsInd (_,(IndType(indf,realargs) as indt)) -> - let mind,_ = dest_ind_family indf in - let cstrs = get_constructors pb.env indf in - let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in - if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then - compile (shift_problem ct pb) - else - let _constraints = Array.map (solve_constraints indt) cstrs in - - (* We generalize over terms depending on current term to match *) - let pb = generalize_problem pb deps in - - (* We compile branches *) - let brs = array_map2 (compile_branch current deps pb) eqns cstrs in - - (* We build the (elementary) case analysis *) - let brvals = Array.map (fun (v,_) -> v) brs in - let brtyps = Array.map (fun (_,t) -> t) brs in - let (pred,typ,s) = - find_predicate pb.caseloc pb.env pb.isevars - pb.pred brtyps cstrs current indt pb.tomatch in - let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in - let inst = List.map mkRel deps in - { uj_val = applist (case, inst); - uj_type = substl inst typ } - -and compile_branch current deps pb eqn cstr = - let sign, pb = build_branch current deps pb eqn cstr in - let j = compile pb in - (it_mkLambda_or_LetIn j.uj_val sign, j.uj_type) - -and compile_generalization pb d rest = - let pb = - { pb with - env = push_rel d pb.env; - tomatch = rest; - pred = Option.map ungeneralize_predicate pb.pred; - mat = List.map (push_rels_eqn [d]) pb.mat } in - let j = compile pb in - { uj_val = mkLambda_or_LetIn d j.uj_val; - uj_type = mkProd_or_LetIn d j.uj_type } - -and compile_alias pb (deppat,nondeppat,d,t) rest = - let history = simplify_history pb.history in - let sign, newenv, mat = - insert_aliases pb.env ( !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in - let n = List.length sign in - - (* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *) - (* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *) - let tomatch = lift_tomatch_stack n rest in - let tomatch = match kind_of_term nondeppat with - | Rel i -> - if n = 1 then regeneralize_index_tomatch (i+n) tomatch - else replace_tomatch i deppat tomatch - | _ -> (* initial terms are not dependent *) tomatch in - - let pb = - {pb with - env = newenv; - tomatch = tomatch; - pred = Option.map (lift_predicate n) pb.pred; - history = history; - mat = mat } in - let j = compile pb in - List.fold_left mkSpecialLetInJudge j sign - -(* pour les alias des initiaux, enrichir les env de ce qu'il faut et -substituer après par les initiaux *) - -(**************************************************************************) -(* Preparation of the pattern-matching problem *) - -(* builds the matrix of equations testing that each eqn has n patterns - * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) -let matx_of_eqns env eqns = - let build_eqn (loc,ids,lpat,rhs) = - let rhs = - { rhs_env = env; - avoid_ids = ids@(ids_of_named_context (named_context env)); - it = rhs; - } in - { patterns = lpat; - alias_stack = []; - eqn_loc = loc; - used = ref false; - rhs = rhs } - in List.map build_eqn eqns - -(************************************************************************) -(* preparing the elimination predicate if any *) - -let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c = - let cook (n, l, env, signs) = function - | c,IsInd (_,IndType(indf,realargs)) -> - let indf' = lift_inductive_family n indf in - let sign = make_arity_signature env dep indf' in - let p = List.length realargs in - if dep then - (n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs) - else - (n + p, (List.rev realargs)@l, push_rels sign env,sign::signs) - | c,NotInd _ -> - (n, l, env, []::signs) in - let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in - let names = List.rev (List.map (List.map pi1) signs) in - let allargs = - List.map (fun c -> lift n (nf_betadeltaiota env ( !isevars) c)) allargs in - let rec build_skeleton env c = - (* Don't put into normal form, it has effects on the synthesis of evars *) - (* let c = whd_betadeltaiota env ( isevars) c in *) - (* We turn all subterms possibly dependent into an evar with maximum ctxt*) - if isEvar c or List.exists (eq_constr c) allargs then - e_new_evar isevars env ~src:(loc, Evd.CasesType) - (Retyping.get_type_of env ( !isevars) c) - else - map_constr_with_full_binders push_rel build_skeleton env c - in - names, build_skeleton env (lift n c) - -(* Here, [pred] is assumed to be in the context built from all *) -(* realargs and terms to match *) -let build_initial_predicate isdep allnames pred = - let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in - let rec buildrec n pred = function - | [] -> PrCcl pred - | names::lnames -> - let names' = if isdep then List.tl names else names in - let n' = n + List.length names' in - let pred, p, user_p = - if isdep then - if dependent (mkRel (nar-n')) pred then pred, 1, 1 - else liftn (-1) (nar-n') pred, 0, 1 - else pred, 0, 0 in - let na = - if p=1 then - let na = List.hd names in - if na = Anonymous then - (* peut arriver en raison des evars *) - Name (id_of_string "x") (*Hum*) - else na - else Anonymous in - PrLetIn ((names',na), buildrec (n'+user_p) pred lnames) - in buildrec 0 pred allnames - -let extract_arity_signature env0 tomatchl tmsign = - let get_one_sign n tm (na,t) = - match tm with - | NotInd (bo,typ) -> - (match t with - | None -> [na,Option.map (lift n) bo,lift n typ] - | Some (loc,_,_,_) -> - user_err_loc (loc,"", - str "Unexpected type annotation for a term of non inductive type")) - | IsInd (_,IndType(indf,realargs)) -> - let indf' = lift_inductive_family n indf in - let (ind,params) = dest_ind_family indf' in - let nrealargs = List.length realargs in - let realnal = - match t with - | Some (loc,ind',nparams,realnal) -> - if ind <> ind' then - user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then - anomaly "Ill-formed 'in' clause in cases"; - List.rev realnal - | None -> list_tabulate (fun _ -> Anonymous) nrealargs in - let arsign = fst (get_arity env0 indf') in - (na,None,build_dependent_inductive env0 indf') - ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) 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) - | _ -> assert false - in List.rev (buildrec 0 (tomatchl,tmsign)) - -let extract_arity_signatures env0 tomatchl tmsign = - let get_one_sign tm (na,t) = - match tm with - | NotInd (bo,typ) -> - (match t with - | None -> [na,bo,typ] - | Some (loc,_,_,_) -> - user_err_loc (loc,"", - str "Unexpected type annotation for a term of non inductive type")) - | IsInd (_,IndType(indf,realargs)) -> - let (ind,params) = dest_ind_family indf in - let nrealargs = List.length realargs in - let realnal = - match t with - | Some (loc,ind',nparams,realnal) -> - if ind <> ind' then - user_err_loc (loc,"",str "Wrong inductive type"); - if List.length params <> nparams - or nrealargs <> List.length realnal then - anomaly "Ill-formed 'in' clause in cases"; - List.rev realnal - | None -> list_tabulate (fun _ -> Anonymous) nrealargs in - let arsign = fst (get_arity env0 indf) in - (na,None,build_dependent_inductive env0 indf) - ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign - with e when Errors.noncritical e -> assert false) in - let rec buildrec = function - | [],[] -> [] - | (_,tm)::ltm, x::tmsign -> - let l = get_one_sign tm x in - l :: buildrec (ltm,tmsign) - | _ -> assert false - in List.rev (buildrec (tomatchl,tmsign)) - -let inh_conv_coerce_to_tycon loc env isevars j tycon = - match tycon with - | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in - isevars := evd'; - j - | None -> j - -let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false) - -let string_of_name name = - match name with - | Anonymous -> "anonymous" - | Name n -> string_of_id n - -let id_of_name n = id_of_string (string_of_name n) - -let make_prime_id name = - let str = string_of_name name in - id_of_string str, id_of_string (str ^ "'") - -let prime avoid name = - let previd, id = make_prime_id name in - previd, next_ident_away id avoid - -let make_prime avoid prevname = - let previd, id = prime !avoid prevname in - avoid := id :: !avoid; - previd, id - -let eq_id avoid id = - let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away hid avoid in - hid' - -let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |]) -let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |]) -let mk_JMeq typ x typ' y = - mkApp (delayed_force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |]) -let mk_JMeq_refl typ x = mkApp (delayed_force Subtac_utils.jmeq_refl, [| typ; x |]) - -let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true)) - -let constr_of_pat env isevars arsign pat avoid = - let rec typ env (ty, realargs) pat avoid = - match pat with - | PatVar (l,name) -> - let name, avoid = match name with - Name n -> name, avoid - | Anonymous -> - let previd, id = prime avoid (Name (id_of_string "wildcard")) in - Name id, id :: avoid - in - PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid - | PatCstr (l,((_, i) as cstr),args,alias) -> - let cind = inductive_of_constructor cstr in - let IndType (indf, _) = - try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) - with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !isevars ty} - in - let ind, params = dest_ind_family indf in - if ind <> cind then error_bad_constructor_loc l cstr ind; - let cstrs = get_constructors env indf in - let ci = cstrs.(i-1) in - let nb_args_constr = ci.cs_nargs in - assert(nb_args_constr = List.length args); - let patargs, args, sign, env, n, m, avoid = - List.fold_right2 - (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) -> - let pat', sign', arg', typ', argtypargs, n', avoid = - typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid - in - let args' = arg' :: List.map (lift n') args in - let env' = push_rels sign' env in - (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid)) - ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid) - in - let args = List.rev args in - let patargs = List.rev patargs in - let pat' = PatCstr (l, cstr, patargs, alias) in - let cstr = mkConstruct ci.cs_cstr in - let app = applistc cstr (List.map (lift (List.length sign)) params) in - let app = applistc app args in - let apptype = Retyping.get_type_of env ( !isevars) app in - let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in - match alias with - Anonymous -> - pat', sign, app, apptype, realargs, n, avoid - | Name id -> - let sign = (alias, None, lift m ty) :: sign in - let avoid = id :: avoid in - let sign, i, avoid = - try - let env = push_rels sign env in - isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars; - let eq_t = mk_eq (lift (succ m) ty) - (mkRel 1) (* alias *) - (lift 1 app) (* aliased term *) - in - let neq = eq_id avoid id in - (Name neq, Some (mkRel 0), eq_t) :: sign, 2, 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 (pi3 (List.hd arsign), List.tl arsign) pat avoid in - pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid - - -(* shadows functional version *) -let eq_id avoid id = - let hid = id_of_string ("Heq_" ^ string_of_id id) in - let hid' = next_ident_away hid !avoid in - avoid := hid' :: !avoid; - hid' - -let rels_of_patsign = - List.map (fun ((na, b, t) as x) -> - match b with - | Some t' when kind_of_term t' = Rel 0 -> (na, None, t) - | _ -> x) - -let vars_of_ctx ctx = - let _, y = - List.fold_right (fun (na, b, t) (prev, vars) -> - match b with - | Some t' when kind_of_term t' = Rel 0 -> - prev, - (GApp (dummy_loc, - (GRef (dummy_loc, delayed_force refl_ref)), [hole; GVar (dummy_loc, prev)])) :: vars - | _ -> - match na with - Anonymous -> raise (Invalid_argument "vars_of_ctx") - | Name n -> n, GVar (dummy_loc, n) :: vars) - ctx (id_of_string "vars_of_ctx_error", []) - in List.rev y - -let rec is_included x y = - match x, y with - | PatVar _, _ -> true - | _, PatVar _ -> true - | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> - if i = i' then List.for_all2 is_included args args' - else false - -(* 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. - *) -let build_ineqs prevpatterns pats liftsign = - let _tomatchs = List.length pats in - let diffs = - List.fold_left - (fun c eqnpats -> - let acc = List.fold_left2 - (* ppat is the pattern we are discriminating against, curpat is the current one. *) - (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat) - (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) -> - match acc with - None -> None - | Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *) - if is_included curpat ppat then - (* Length of previous pattern's signature *) - let lens = List.length ppat_sign in - (* Accumulated length of previous pattern's signatures *) - let len' = lens + len in - let acc = - ((* Jump over previous prevpat signs *) - lift_rel_context len ppat_sign @ sign, - len', - succ n, (* nth pattern *) - mkApp (delayed_force eq_ind, - [| lift (len' + liftsign) curpat_ty; - liftn (len + liftsign) (succ lens) ppat_c ; - lift len' curpat_c |]) :: - List.map (lift lens (* Jump over this prevpat signature *)) c) - in Some acc - else None) - (Some ([], 0, 0, [])) eqnpats pats - in match acc with - None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_not (mk_conj c')) - (lift_rel_context liftsign sign) - in - conj :: c) - [] prevpatterns - in match diffs with [] -> None - | _ -> Some (mk_conj diffs) - -let subst_rel_context k ctx subst = - let (_, ctx') = - List.fold_right - (fun (n, b, t) (k, acc) -> - (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) - ctx (k, []) - in ctx' - -let lift_rel_contextn n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) - | [] -> [] - in - liftrec (rel_context_length sign + k) sign - -let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity = - let i = ref 0 in - let (x, y, z) = - List.fold_left - (fun (branches, eqns, prevpatterns) eqn -> - let _, newpatterns, pats = - List.fold_left2 - (fun (idents, newpatterns, pats) pat arsign -> - let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in - (idents, pat' :: newpatterns, cpat :: pats)) - ([], [], []) eqn.patterns sign - in - let newpatterns = List.rev newpatterns and opats = List.rev pats in - let rhs_rels, pats, signlen = - List.fold_left - (fun (renv, pats, n) (sign,c, (s, args), p) -> - (* Recombine signatures and terms of all of the row's patterns *) - let sign' = lift_rel_context n sign in - let len = List.length sign' in - (sign' @ renv, - (* lift to get outside of previous pattern's signatures. *) - (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats, - len + n)) - ([], [], 0) opats in - let pats, _ = List.fold_left - (* 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, (s, List.map (lift n) args), p) :: pats, len + n)) - ([], 0) pats - in - let ineqs = build_ineqs prevpatterns pats signlen in - let rhs_rels' = rels_of_patsign rhs_rels in - let _signenv = push_rel_context rhs_rels' env in - let arity = - let args, nargs = - List.fold_right (fun (sign, c, (_, args), _) (allargs,n) -> - (args @ c :: allargs, List.length args + succ n)) - pats ([], 0) - in - let args = List.rev args in - substl args (liftn signlen (succ nargs) arity) - in - let rhs_rels', tycon = - let neqs_rels, arity = - match ineqs with - | None -> [], arity - | Some ineqs -> - [Anonymous, None, ineqs], lift 1 arity - in - let eqs_rels, arity = decompose_prod_n_assum neqs arity in - eqs_rels @ neqs_rels @ rhs_rels', arity - in - let rhs_env = push_rels rhs_rels' env in - let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in - let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' - and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in - let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in - let branch = - let bref = GVar (dummy_loc, branch_name) in - match vars_of_ctx rhs_rels with - [] -> bref - | l -> GApp (dummy_loc, bref, l) - in - let branch = match ineqs with - Some _ -> GApp (dummy_loc, branch, [ hole ]) - | None -> branch - in - incr i; - let rhs = { eqn.rhs with it = branch } in - (branch_decl :: branches, - { eqn with patterns = newpatterns; rhs = rhs } :: eqns, - opats :: prevpatterns)) - ([], [], []) eqns - in x, y - -(* Builds the predicate. If the predicate is dependent, its context is - * made of 1+nrealargs assumptions for each matched term in an inductive - * type and 1 assumption for each term not _syntactically_ in an - * inductive type. - - * Each matched terms are independently considered dependent or not. - - * A type constraint but no annotation case: it is assumed non dependent. - *) - -let lift_ctx n ctx = - let ctx', _ = - List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0) - in ctx' - -(* Turn matched terms into variables. *) -let abstract_tomatch env 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 - 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 - let name = next_ident_away (id_of_string "filtered_var") names in - (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, - (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, - name :: names, tycon) - ([], [], [], tycon) tomatchs - in List.rev prev, ctx, tycon - -let is_dependent_ind = function - IsInd (_, IndType (indf, args)) when List.length args > 0 -> true - | _ -> false - -let build_dependent_signature env evars avoid tomatchs arsign = - let avoid = ref avoid in - let arsign = List.rev arsign in - let allnames = List.rev (List.map (List.map pi1) 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 - (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign -> - (* The accumulator: - previous eqs, - number of previous eqs, - lift to get outside eqs and in the introduced variables ('as' and 'in'), - new arity signatures - *) - match ty with - IsInd (ty, IndType (indf, args)) when List.length args > 0 -> - (* Build the arity signature following the names in matched terms as much as possible *) - let argsign = List.tl arsign in (* arguments in inverse application order *) - let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *) - 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 (name, b, t) -> - let argt = Retyping.get_type_of env evars arg in - let eq, refl_arg = - if Reductionops.is_conv env evars argt t then - (mk_eq (lift (nargeqs + slift) argt) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) arg), - mk_eq_refl argt arg) - else - (mk_JMeq (lift (nargeqs + slift) t) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) argt) - (lift (nargeqs + nar) arg), - mk_JMeq_refl argt arg) - in - let previd, id = - let name = - match kind_of_term arg with - Rel n -> pi1 (lookup_rel n env) - | _ -> name - in - make_prime avoid name - in - (env, succ nargeqs, - (Name (eq_id avoid previd), None, eq) :: argeqs, - refl_arg :: refl_args, - pred slift, - (Name id, b, t) :: argsign')) - (env, neqs, [], [], slift, []) args argsign - in - let eq = mk_JMeq - (lift (nargeqs + slift) appt) - (mkRel (nargeqs + slift)) - (lift (nargeqs + nar) ty) - (lift (nargeqs + nar) tm) - in - let refl_eq = mk_JMeq_refl ty tm in - let previd, id = make_prime avoid appn in - (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs, - succ nargeqs, - refl_eq :: refl_args, - pred slift, - (((Name id, appb, appt) :: argsign') :: arsigns)) - - | _ -> - (* Non dependent inductive or not inductive, just use a regular equality *) - let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in - let previd, id = make_prime avoid name in - let arsign' = (Name id, b, typ) in - let tomatch_ty = type_of_tomatch ty in - let eq = - mk_eq (lift nar tomatch_ty) - (mkRel slift) (lift nar tm) - in - ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs, - (mk_eq_refl tomatch_ty tm) :: refl_args, - pred slift, (arsign' :: []) :: arsigns)) - ([], 0, [], nar, []) tomatchs arsign - in - let arsign'' = List.rev arsign' in - assert(slift = 0); (* we must have folded over all elements of the arity signature *) - arsign'', allnames, nar, eqs, neqs, refls - -(**************************************************************************) -(* Main entry of the matching compilation *) - -let liftn_rel_context n k sign = - let rec liftrec k = function - | (na,c,t)::sign -> - (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) - | [] -> [] - in - liftrec (k + rel_context_length sign) sign - -let nf_evars_env sigma (env : env) : env = - let nf t = nf_evar sigma t in - let env0 : env = reset_context env in - let f e (na, b, t) e' : env = - Environ.push_named (na, Option.map nf b, nf t) e' - in - let env' = Environ.fold_named_context f ~init:env0 env in - Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e') - ~init:env' env - - -let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp = - (* We extract the signature of the arity *) - let arsign = extract_arity_signature env tomatchs sign in - let newenv = List.fold_right push_rels arsign env in - let allnames = List.rev (List.map (List.map pi1) arsign) in - match rtntyp with - | Some rtntyp -> - let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in - let predccl = (j_nf_evar !isevars predcclj).uj_val in - Some (build_initial_predicate true allnames predccl) - | None -> - match valcon_of_tycon tycon with - | Some ty -> - let pred = - prepare_predicate_from_arsign_tycon loc env !isevars tomatchs arsign ty - in Some (build_initial_predicate true allnames pred) - | None -> None - -let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = - - let typing_fun tycon env = typing_fun tycon env isevars in - - (* We build the matrix of patterns and right-hand side *) - let matx = matx_of_eqns env eqns in - - (* We build the vector of terms to match consistently with the *) - (* constructors found in patterns *) - let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in - let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in - if predopt = None then - let tycon = valcon_of_tycon tycon in - let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env 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_signatures env tomatchs (List.map snd tomatchl) in - (* Build the dependent arity signature, the equalities which makes - the first part of the predicate and their instantiations. *) - let avoid = [] in - build_dependent_signature env ( !isevars) avoid tomatchs arsign - - in - let tycon, arity = - match tycon' with - | None -> let ev = mkExistential env isevars in ev, ev - | Some t -> - Option.get tycon, prepare_predicate_from_arsign_tycon loc env ( !isevars) - tomatchs sign t - in - let neqs, arity = - let ctx = context_of_arsign eqs in - let neqs = List.length ctx in - neqs, it_mkProd_or_LetIn (lift neqs arity) ctx - in - let lets, matx = - (* Type the rhs under the assumption of equations *) - constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity - in - let matx = List.rev matx in - let _ = assert(len = List.length lets) in - let env = push_rels lets env in - let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in - let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in - let args = List.rev_map (lift len) args in - let pred = liftn len (succ signlen) arity in - let pred = build_initial_predicate true allnames pred in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - - let pb = - { env = env; - isevars = isevars; - pred = Some pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - casestyle= style; - typing_function = typing_fun } in - - 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 j = - { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = nf_evar !isevars tycon; } - in j - else - (* We build the elimination predicate if any and check its consistency *) - (* with the type of arguments to match *) - let tmsign = List.map snd tomatchl in - let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in - - (* We push the initial terms to match and push their alias to rhs' envs *) - (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in - let pb = - { env = env; - isevars = isevars; - pred = pred; - tomatch = initial_pushed; - history = start_history (List.length initial_pushed); - mat = matx; - caseloc = loc; - casestyle= style; - typing_function = typing_fun } in - - let j = compile pb in - (* We check for unused patterns *) - List.iter (check_unused_pattern env) matx; - inh_conv_coerce_to_tycon loc env isevars j tycon - -end - |