diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 94 | ||||
| -rw-r--r-- | engine/eConstr.mli | 32 | ||||
| -rw-r--r-- | engine/evarutil.ml | 2 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/termops.ml | 60 | ||||
| -rw-r--r-- | engine/termops.mli | 10 | ||||
| -rw-r--r-- | engine/univSubst.ml | 20 |
7 files changed, 137 insertions, 85 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index c29de27efb..ec255aad03 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -35,6 +35,10 @@ include (Evd.MiniEConstr : module type of Evd.MiniEConstr type types = t type constr = t type existential = t pexistential +type case_return = t pcase_return +type case_branch = t pcase_branch +type case_invert = (t, EInstance.t) pcase_invert +type case = (t, t, EInstance.t) pcase type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment @@ -69,7 +73,7 @@ let mkInd i = of_kind (Ind (in_punivs i)) let mkConstructU pc = of_kind (Construct pc) let mkConstruct c = of_kind (Construct (in_punivs c)) let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u)) -let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p)) +let mkCase (ci, u, pms, c, iv, r, p) = of_kind (Case (ci, u, pms, c, iv, r, p)) let mkFix f = of_kind (Fix f) let mkCoFix f = of_kind (CoFix f) let mkProj (p, c) = of_kind (Proj (p, c)) @@ -195,7 +199,7 @@ let destCoFix sigma c = match kind sigma c with | _ -> raise DestKO let destCase sigma c = match kind sigma c with -| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p) +| Case (ci, u, pms, t, iv, c, p) -> (ci, u, pms, t, iv, c, p) | _ -> raise DestKO let destProj sigma c = match kind sigma c with @@ -320,19 +324,28 @@ let existential_type = Evd.existential_type let lift n c = of_constr (Vars.lift n (unsafe_to_constr c)) -let map_under_context f n c = - let f c = unsafe_to_constr (f (of_constr c)) in - of_constr (Constr.map_under_context f n (unsafe_to_constr c)) -let map_branches f ci br = - let f c = unsafe_to_constr (f (of_constr c)) in - of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br)) -let map_return_predicate f ci p = - let f c = unsafe_to_constr (f (of_constr c)) in - of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p)) +let of_branches : Constr.case_branch array -> case_branch array = + match Evd.MiniEConstr.unsafe_eq with + | Refl -> fun x -> x + +let unsafe_to_branches : case_branch array -> Constr.case_branch array = + match Evd.MiniEConstr.unsafe_eq with + | Refl -> fun x -> x + +let of_return : Constr.case_return -> case_return = + match Evd.MiniEConstr.unsafe_eq with + | Refl -> fun x -> x -let map_user_view sigma f c = +let unsafe_to_return : case_return -> Constr.case_return = + match Evd.MiniEConstr.unsafe_eq with + | Refl -> fun x -> x + +let map_branches f br = + let f c = unsafe_to_constr (f (of_constr c)) in + of_branches (Constr.map_branches f (unsafe_to_branches br)) +let map_return_predicate f p = let f c = unsafe_to_constr (f (of_constr c)) in - of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c))) + of_return (Constr.map_return_predicate f (unsafe_to_return p)) let map sigma f c = let f c = unsafe_to_constr (f (of_constr c)) in @@ -346,7 +359,49 @@ let iter sigma f c = let f c = f (of_constr c) in Constr.iter f (unsafe_to_constr (whd_evar sigma c)) -let iter_with_full_binders sigma g f n c = +let expand_case env _sigma (ci, u, pms, p, iv, c, bl) = + let u = EInstance.unsafe_to_instance u in + let pms = unsafe_to_constr_array pms in + let p = unsafe_to_return p in + let iv = unsafe_to_case_invert iv in + let c = unsafe_to_constr c in + let bl = unsafe_to_branches bl in + let (ci, p, iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in + let p = of_constr p in + let c = of_constr c in + let iv = of_case_invert iv in + let bl = of_constr_array bl in + (ci, p, iv, c, bl) + +let expand_branch env _sigma u pms (ind, i) (nas, _br) = + let open Declarations in + let u = EInstance.unsafe_to_instance u in + let pms = unsafe_to_constr_array pms in + let (mib, mip) = Inductive.lookup_mind_specif env ind in + let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in + let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in + let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in + let (ctx, _) = mip.mind_nf_lc.(i - 1) in + let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in + let ans = Inductive.instantiate_context u subst nas ctx in + let ans : rel_context = match Evd.MiniEConstr.unsafe_eq with Refl -> ans in + ans + +let contract_case env _sigma (ci, p, iv, c, bl) = + let p = unsafe_to_constr p in + let iv = unsafe_to_case_invert iv in + let c = unsafe_to_constr c in + let bl = unsafe_to_constr_array bl in + let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, p, iv, c, bl) in + let u = EInstance.make u in + let pms = of_constr_array pms in + let p = of_return p in + let iv = of_case_invert iv in + let c = of_constr c in + let bl = of_branches bl in + (ci, u, pms, p, iv, c, bl) + +let iter_with_full_binders env sigma g f n c = let open Context.Rel.Declaration in match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -357,7 +412,10 @@ let iter_with_full_binders sigma g f n c = | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> List.iter (fun c -> f n c) l - | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl + | Case (ci,u,pms,p,iv,c,bl) -> + (* FIXME: skip the type annotations *) + let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in + f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(lna,tl,bl)) -> Array.iter (f n) tl; @@ -566,9 +624,13 @@ let universes_of_constr sigma c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in fold sigma aux s c - | Case (_,_,CaseInvert {univs;args=_},_,_) -> + | Case (_,u,_,_,CaseInvert {univs;args=_},_,_) -> + let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in fold sigma aux s c + | Case (_, u, _, _, NoInvert, _, _) -> + let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in + fold sigma aux s c | _ -> fold sigma aux s c in aux LSet.empty c diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 882dfe2848..2add7b0b5e 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -20,6 +20,8 @@ type t = Evd.econstr type types = t type constr = t type existential = t pexistential +type case_return = t pcase_return +type case_branch = t pcase_branch type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint type unsafe_judgment = (constr, types) Environ.punsafe_judgment @@ -58,6 +60,9 @@ sig val is_empty : t -> bool end +type case_invert = (t, EInstance.t) pcase_invert +type case = (t, t, EInstance.t) pcase + type 'a puniverses = 'a * EInstance.t (** {5 Destructors} *) @@ -128,7 +133,7 @@ val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t val mkConstructU : constructor * EInstance.t -> t val mkConstructUi : (inductive * EInstance.t) * int -> t -val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t +val mkCase : case -> t val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t val mkArrow : t -> Sorts.relevance -> t -> t @@ -199,7 +204,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t val destEvar : Evd.evar_map -> t -> t pexistential val destInd : Evd.evar_map -> t -> inductive * EInstance.t val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t -val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array +val destCase : Evd.evar_map -> t -> case val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint @@ -250,14 +255,12 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool (** {6 Iterators} *) val map : Evd.evar_map -> (t -> t) -> t -> t -val map_user_view : Evd.evar_map -> (t -> t) -> t -> t val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t -val map_under_context : (t -> t) -> int -> t -> t -val map_branches : (t -> t) -> case_info -> t array -> t array -val map_return_predicate : (t -> t) -> case_info -> t -> t +val map_branches : (t -> t) -> case_branch array -> case_branch array +val map_return_predicate : (t -> t) -> case_return -> case_return val iter : Evd.evar_map -> (t -> unit) -> t -> unit val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit -val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit +val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the @@ -337,6 +340,17 @@ val fresh_global : val is_global : Evd.evar_map -> GlobRef.t -> t -> bool [@@ocaml.deprecated "Use [EConstr.isRefX] instead."] +val expand_case : Environ.env -> Evd.evar_map -> + case -> (case_info * t * case_invert * t * t array) + +val expand_branch : Environ.env -> Evd.evar_map -> + EInstance.t -> t array -> constructor -> case_branch -> rel_context +(** Given a universe instance and parameters for the inductive type, + constructs the typed context in which the branch lives. *) + +val contract_case : Environ.env -> Evd.evar_map -> + (case_info * t * case_invert * t * t array) -> case + (** {5 Extra} *) val of_existential : Constr.existential -> existential @@ -345,7 +359,7 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt -val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert +val of_case_invert : Constr.case_invert -> case_invert (** {5 Unsafe operations} *) @@ -371,7 +385,7 @@ sig val to_instance : EInstance.t -> Univ.Instance.t (** Physical identity. Does not care for normalization. *) - val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert + val to_case_invert : case_invert -> Constr.case_invert val eq : (t, Constr.t) eq (** Use for transparent cast between types. *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index ba6a9ea6d9..f9f8268507 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -144,7 +144,7 @@ let head_evar sigma c = let c = EConstr.Unsafe.to_constr c in let rec hrec c = match kind c with | Evar (evk,_) -> evk - | Case (_,_,_,c,_) -> hrec c + | Case (_, _, _, _, _, c, _) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c | Proj (p, c) -> hrec c diff --git a/engine/evd.mli b/engine/evd.mli index a6d55c2615..ec9ae6fca9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -772,8 +772,8 @@ module MiniEConstr : sig (Constr.t, Constr.types) Context.Named.Declaration.pt val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt - val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert - val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert + val of_case_invert : (constr,Univ.Instance.t) pcase_invert -> (econstr,EInstance.t) pcase_invert + val unsafe_to_case_invert : (econstr,EInstance.t) pcase_invert -> (constr,Univ.Instance.t) pcase_invert val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> diff --git a/engine/termops.ml b/engine/termops.ml index 66131e1a8f..d331ecc458 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -606,7 +606,7 @@ let map_left2 f a g b = r, s end -let map_constr_with_binders_left_to_right sigma g f l c = +let map_constr_with_binders_left_to_right env sigma g f l c = let open RelDecl in let open EConstr in match EConstr.kind sigma c with @@ -650,14 +650,16 @@ let map_constr_with_binders_left_to_right sigma g f l c = let al' = List.map_left (f l) al in if List.for_all2 (==) al' al then c else mkEvar (e, al') - | Case (ci,p,iv,b,bl) -> + | Case (ci,u,pms,p,iv,b,bl) -> + (* FIXME: skip annotations? *) + let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, b, bl) in (* In v8 concrete syntax, predicate is after the term to match! *) let b' = f l b in let iv' = map_invert (f l) iv in let p' = f l p in let bl' = Array.map_left (f l) bl in if b' == b && p' == p && iv' == iv && bl' == bl then c - else mkCase (ci, p', iv', b', bl') + else mkCase (EConstr.contract_case env sigma (ci, p', iv', b', bl')) | Fix (ln,(lna,tl,bl as fx)) -> let l' = fold_rec_types g fx l in let (tl', bl') = map_left2 (f l) tl (f l') bl in @@ -677,34 +679,8 @@ let map_constr_with_binders_left_to_right sigma g f l c = if def' == def && t' == t && ty' == ty then c else mkArray(u,t',def',ty') -let rec map_under_context_with_full_binders sigma g f l n d = - if n = 0 then f l d else - match EConstr.kind sigma d with - | LetIn (na,b,t,c) -> - let b' = f l b in - let t' = f l t in - let c' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in - if b' == b && t' == t && c' == c then d - else EConstr.mkLetIn (na,b',t',c') - | Lambda (na,t,b) -> - let t' = f l t in - let b' = map_under_context_with_full_binders sigma g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in - if t' == t && b' == b then d - else EConstr.mkLambda (na,t',b') - | _ -> CErrors.anomaly (Pp.str "Ill-formed context") - -let map_branches_with_full_binders sigma g f l ci bl = - let tags = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in - if Array.for_all2 (==) bl' bl then bl else bl' - -let map_return_predicate_with_full_binders sigma g f l ci p = - let n = List.length ci.ci_pp_info.ind_tags in - let p' = map_under_context_with_full_binders sigma g f l n p in - if p' == p then p else p' - (* strong *) -let map_constr_with_full_binders_gen userview sigma g f l cstr = +let map_constr_with_full_binders env sigma g f l cstr = let open EConstr in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ @@ -736,20 +712,14 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = | Evar (e,al) -> let al' = List.map (f l) al in if List.for_all2 (==) al al' then cstr else mkEvar (e, al') - | Case (ci,p,iv,c,bl) when userview -> - let p' = map_return_predicate_with_full_binders sigma g f l ci p in - let iv' = map_invert (f l) iv in - let c' = f l c in - let bl' = map_branches_with_full_binders sigma g f l ci bl in - if p==p' && iv'==iv && c==c' && bl'==bl then cstr else - mkCase (ci, p', iv', c', bl') - | Case (ci,p,iv,c,bl) -> + | Case (ci, u, pms, p, iv, c, bl) -> + let (ci, p, iv, c, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in let p' = f l p in let iv' = map_invert (f l) iv in let c' = f l c in let bl' = Array.map (f l) bl in if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else - mkCase (ci, p', iv', c', bl') + mkCase (EConstr.contract_case env sigma (ci, p', iv', c', bl')) | Fix (ln,(lna,tl,bl as fx)) -> let tl' = Array.map (f l) tl in let l' = fold_rec_types g fx l in @@ -770,12 +740,6 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let ty' = f l ty in if def==def' && t == t' && ty==ty' then cstr else mkArray (u,t', def',ty') -let map_constr_with_full_binders sigma g f = - map_constr_with_full_binders_gen false sigma g f - -let map_constr_with_full_binders_user_view sigma g f = - map_constr_with_full_binders_gen true sigma g f - (* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions as @@ -783,7 +747,7 @@ let map_constr_with_full_binders_user_view sigma g f = index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_full_binders sigma g f n acc c = +let fold_constr_with_full_binders env sigma g f n acc c = let open EConstr.Vars in let open Context.Rel.Declaration in match EConstr.kind sigma c with @@ -795,7 +759,9 @@ let fold_constr_with_full_binders sigma g f n acc c = | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (_,c) -> f n acc c | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl + | Case (ci, u, pms, p, iv, c, bl) -> + let (ci, p, iv, b, bl) = EConstr.expand_case env sigma (ci, u, pms, p, iv, c, bl) in + Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl | Fix (_,(lna,tl,bl)) -> let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in diff --git a/engine/termops.mli b/engine/termops.mli index 709fa361a9..12df61e4c8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -50,16 +50,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> (** {6 Generic iterators on constr} *) val map_constr_with_binders_left_to_right : - Evd.evar_map -> + Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : - Evd.evar_map -> - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr -val map_constr_with_full_binders_user_view : - Evd.evar_map -> + Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr @@ -73,7 +69,7 @@ val map_constr_with_full_binders_user_view : val fold_constr_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val fold_constr_with_full_binders : Evd.evar_map -> +val fold_constr_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 335c2e5e68..e2721b4822 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -68,6 +68,15 @@ let subst_univs_fn_constr f c = let u' = fi u in if u' == u then t else (changed := true; mkConstructU (c, u')) + | Case (ci, u, pms, p, NoInvert, c, br) -> + let u' = fi u in + if u' == u then map aux t + else (changed := true; map aux (mkCase (ci, u', pms, p, NoInvert, c, br))) + | Case (ci, u, pms, p, CaseInvert{univs;args}, c, br) -> + let u' = fi u in + let univs' = fi univs in + if u' == u && univs' == univs then map aux t + else (changed := true; map aux (mkCase (ci, u', pms, p, CaseInvert {univs = univs'; args}, c, br))) | _ -> map aux t in let c' = aux c in @@ -147,10 +156,15 @@ let nf_evars_and_universes_opt_subst f subst = | Sort (Type u) -> let u' = Univ.subst_univs_universe subst u in if u' == u then c else mkSort (sort_of_univ u') - | Case (ci,p,CaseInvert {univs;args},t,br) -> + | Case (ci, u, pms, p, NoInvert, t, br) -> + let u' = Instance.subst_fn lsubst u in + if u' == u then map aux c + else Constr.map aux (mkCase (ci, u', pms, p, NoInvert, t, br)) + | Case (ci,u,pms,p,CaseInvert {univs;args},t,br) -> + let u' = Instance.subst_fn lsubst u in let univs' = Instance.subst_fn lsubst univs in - if univs' == univs then Constr.map aux c - else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br)) + if u' == u && univs' == univs then Constr.map aux c + else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},t,br)) | Array (u,elems,def,ty) -> let u' = Univ.Instance.subst_fn lsubst u in let elems' = CArray.Smart.map aux elems in |