diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 23:33:01 +0100 |
---|---|---|
committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-15 23:33:01 +0100 |
commit | 13e847b7092d53ffec63e4cba54c67d39560e67a (patch) | |
tree | 9303e5293a739b6bf77b6557da523ab4c3b171d7 | |
parent | 97d6583a0b9a65080639fb02deba4200f6276ce6 (diff) |
CLEANUP: Simplifying the changes done in "checker/*"
-rw-r--r-- | checker/declarations.ml | 10 | ||||
-rw-r--r-- | checker/indtypes.ml | 7 | ||||
-rw-r--r-- | checker/inductive.ml | 5 | ||||
-rw-r--r-- | checker/term.ml | 26 | ||||
-rw-r--r-- | checker/term.mli | 1 |
5 files changed, 23 insertions, 26 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 2f6eeba1d..3ce312533 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -517,14 +517,8 @@ let map_decl_arity f g = function | RegularArity a -> RegularArity (f a) | TemplateArity a -> TemplateArity (g a) -let subst_rel_declaration sub = function - | LocalAssum (id,t) as x -> - let t' = subst_mps sub t in - if t == t' then x else LocalAssum (id,t') - | LocalDef (id,c,t) as x -> - let c' = subst_mps sub c in - let t' = subst_mps sub t in - if c == c' && t == t' then x else LocalDef (id,c',t') +let subst_rel_declaration sub = + Term.map_rel_decl (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index f11fa5a7a..566df673c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -319,7 +319,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | LocalDef (_,_,_) :: hyps -> check k (index+1) hyps + | LocalDef _ :: hyps -> check k (index+1) hyps | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps @@ -376,8 +376,9 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar)) env in + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in diff --git a/checker/inductive.ml b/checker/inductive.ml index 948012421..5e2e14f7f 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -634,8 +634,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (LocalAssum (Anonymous, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar)) env + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in diff --git a/checker/term.ml b/checker/term.ml index 181d292ad..56cc9cdc2 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -227,19 +227,19 @@ let rel_context_nhyps hyps = nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init -let map_rel_context f l = - let map_decl = function - | LocalAssum (n, typ) as decl -> - let typ' = f typ in - if typ' == typ then decl else - LocalAssum (n, typ') - | LocalDef (n, body, typ) as decl -> - let body' = f body in - let typ' = f typ in - if body' == body && typ' == typ then decl else - LocalDef (n, body', typ') - in - List.smartmap map_decl l +let map_rel_decl f = function + | LocalAssum (n, typ) as decl -> + let typ' = f typ in + if typ' == typ then decl else + LocalAssum (n, typ') + | LocalDef (n, body, typ) as decl -> + let body' = f body in + let typ' = f typ in + if body' == body && typ' == typ then decl else + LocalDef (n, body', typ') + +let map_rel_context f = + List.smartmap (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function diff --git a/checker/term.mli b/checker/term.mli index d6455e23f..0af83e05d 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -35,6 +35,7 @@ val rel_context_length : rel_context -> int val rel_context_nhyps : rel_context -> int val fold_rel_context : (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration val map_rel_context : (constr -> constr) -> rel_context -> rel_context val extended_rel_list : int -> rel_context -> constr list val compose_lam : (name * constr) list -> constr -> constr |