diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /vernac/assumptions.ml | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'vernac/assumptions.ml')
| -rw-r--r-- | vernac/assumptions.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 792f07bb89..9c5f111e28 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -176,7 +176,10 @@ let fold_with_full_binders 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 mib = lookup_mind (fst ci.ci_ind) in + let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (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 @@ -201,12 +204,11 @@ let rec traverse current ctx accu t = | Construct (((mind, _), _) as cst, _) -> traverse_inductive accu mind (ConstructRef cst) | Meta _ | Evar _ -> assert false -| Case (_,oty,_,c,[||]) -> +| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty -> (* non dependent match on an inductive with no constructors *) - begin match Constr.(kind oty, kind c) with - | Lambda(_,_,oty), Const (kn, _) - when Vars.noccurn 1 oty && - not (Declareops.constant_has_body (lookup_constant kn)) -> + begin match Constr.kind c with + | Const (kn, _) + when not (Declareops.constant_has_body (lookup_constant kn)) -> let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) |