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 /kernel/vars.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 'kernel/vars.ml')
| -rw-r--r-- | kernel/vars.ml | 37 |
1 files changed, 29 insertions, 8 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml index a446fa413c..0f71057787 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -253,12 +253,21 @@ let subst_univs_level_constr subst c = if u' == u then t else (changed := true; mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> - if Univ.Instance.is_empty univs then Constr.map aux t + | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t else + let u' = f u in let univs' = f univs in - if univs' == univs then Constr.map aux t - else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))) + if u' == u && univs' == univs then Constr.map aux t + else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))) | Array (u,elems,def,ty) -> let u' = f u in @@ -305,10 +314,19 @@ let subst_instance_constr subst c = if u' == u then t else (mkSort (Sorts.sort_of_univ u')) - | Case (ci,p,CaseInvert {univs;args},c,br) -> + | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) -> + let u' = f u in let univs' = f univs in - if univs' == univs then Constr.map aux t - else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)) + if u' == u && univs' == univs then Constr.map aux t + else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)) + + | Case (ci, u, pms, p, NoInvert, c, br) -> + if Univ.Instance.is_empty u then Constr.map aux t + else + let u' = f u in + if u' == u then Constr.map aux t + else + Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)) | Array (u,elems,def,ty) -> let u' = f u in @@ -348,8 +366,11 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c - | Case (_,_,CaseInvert {univs;args=_},_,_) -> + | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) -> + let s = LSet.fold LSet.add (Instance.levels u) s in let s = LSet.fold LSet.add (Instance.levels univs) s in Constr.fold aux s c + | Case (_, u, _, _, NoInvert, _, _) -> + Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c | _ -> Constr.fold aux s c in aux LSet.empty c |