summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_cases.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_cases.ml')
-rw-r--r--plugins/subtac/subtac_cases.ml2027
1 files changed, 2027 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
new file mode 100644
index 00000000..e8f4f05f
--- /dev/null
+++ b/plugins/subtac/subtac_cases.ml
@@ -0,0 +1,2027 @@
+(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+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 Rawterm
+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 : rawconstr;
+ }
+
+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 rawpattern_of_partial_history args2 = function
+ | Continuation (n, args1, h) ->
+ let args3 = make_anonymous_patvars (n - (List.length args2)) in
+ build_rawpattern (List.rev_append args1 (args2@args3)) h
+ | Result pl -> pl
+
+and build_rawpattern args = function
+ | Top -> args
+ | MakeAlias (AliasLeaf, rh) ->
+ assert (args = []);
+ rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
+ | MakeAlias (AliasConstructor pci, rh) ->
+ rawpattern_of_partial_history
+ [PatCstr (dummy_loc, pci, args, Anonymous)] rh
+
+let complete_history = rawpattern_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 -> rawconstr -> 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 _ -> 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_rawconstr 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_rawconstr 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 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_rawconstr 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 t = mkRel (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 _ -> 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 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 (Lazy.force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y =
+ mkApp (Lazy.force Subtac_utils.jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (Lazy.force Subtac_utils.jmeq_refl, [| typ; x |])
+
+let hole = RHole (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 (lift (n - m) 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,
+ (RApp (dummy_loc,
+ (RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
+ | _ ->
+ match na with
+ Anonymous -> raise (Invalid_argument "vars_of_ctx")
+ | Name n -> n, RVar (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 (Lazy.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 ("branch_" ^ (string_of_int !i)) in
+ let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
+ let branch =
+ let bref = RVar (dummy_loc, branch_name) in
+ match vars_of_ctx rhs_rels with
+ [] -> bref
+ | l -> RApp (dummy_loc, bref, l)
+ in
+ let branch = match ineqs with
+ Some _ -> RApp (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_occ all_occurrences (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, 0, [], [], 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
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 10:12:35 +0000