diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | checker/closure.ml | 80 | ||||
| -rw-r--r-- | checker/closure.mli | 4 | ||||
| -rw-r--r-- | checker/indtypes.ml | 46 | ||||
| -rw-r--r-- | checker/inductive.ml | 33 | ||||
| -rw-r--r-- | checker/reduction.ml | 15 | ||||
| -rw-r--r-- | checker/subtyping.ml | 8 |
7 files changed, 104 insertions, 84 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 139fa765b4..173ad1e325 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,3 @@ -Coq_config - Analyze Hook Terminal diff --git a/checker/closure.ml b/checker/closure.ml index 5706011607..138499b0e6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -121,9 +121,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables * and only those with index 1 and 3 have bodies which are c and d resp. * @@ -156,33 +153,6 @@ end module KeyTable = Hashtbl.Make(KeyHash) -type 'a infos = { - i_flags : reds; - i_repr : 'a infos -> constr -> 'a; - i_env : env; - i_rels : int * (int * constr) list; - i_tab : 'a KeyTable.t } - -let ref_value_cache info ref = - try - Some (KeyTable.find info.i_tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) - | VarKey id -> raise Not_found - | ConstKey cst -> constant_value info.i_env cst - in - let v = info.i_repr info body in - KeyTable.add info.i_tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context @@ -193,16 +163,6 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = mind_equiv info.i_env - -let create mk_cl flgs env = - { i_flags = flgs; - i_repr = mk_cl; - i_env = env; - i_rels = defined_rels flgs env; - i_tab = KeyTable.create 17 } - - (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -255,6 +215,12 @@ and fterm = | FCLOS of constr * fconstr subs | FLOCKED +type clos_infos = { + i_flags : reds; + i_env : env; + i_rels : int * (int * constr) list; + i_tab : fconstr KeyTable.t } + let fterm_of v = v.term let set_norm v = v.norm <- Norm @@ -372,6 +338,30 @@ let mk_clos e t = let mk_clos_vect env v = Array.map (mk_clos env) v +let inject = mk_clos (subs_id 0) + +let ref_value_cache info ref = + try + Some (KeyTable.find info.i_tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) + | VarKey id -> raise Not_found + | ConstKey cst -> constant_value info.i_env cst + in + let v = inject body in + KeyTable.add info.i_tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + +let mind_equiv_infos info = mind_equiv info.i_env + (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct subterms. @@ -783,21 +773,19 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (subs_id 0) - let whd_stack infos m stk = let k = kni infos m stk in let _ = fapp_stack k in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let infos_env x = x.i_env let infos_flags x = x.i_flags let oracle_of_infos x = x.i_env.env_conv_oracle let create_clos_infos flgs env = - create (fun _ -> inject) flgs env + { i_flags = flgs; + i_env = env; + i_rels = defined_rels flgs env; + i_tab = KeyTable.create 17 } let unfold_reference = ref_value_cache diff --git a/checker/closure.mli b/checker/closure.mli index cec785699d..4c6643754b 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -61,10 +61,6 @@ val betadeltaiotanolet : reds type table_key = Constant.t puniverses tableKey -type 'a infos -val ref_value_cache: 'a infos -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos - (************************************************************************) (*s Lazy reduction. *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 0478765a81..50e65ef587 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -310,25 +310,31 @@ let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") -(* Conclusion of constructors: check the inductive type is called with - the expected parameters *) -let check_correct_par (env,n,ntypes,_) hyps l largs = - let nparams = rel_context_nhyps hyps in - let largs = Array.of_list largs in - if Array.length largs < nparams then - raise (IllFormedInd (LocalNotEnoughArgs l)); - let (lpar,largs') = Array.chop nparams largs in - let nhyps = List.length hyps in - let rec check k index = function +(* Check the inductive type is called with the expected parameters *) +(* [n] is the index of the last inductive type in [env] *) +let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = + let nparams = rel_context_nhyps paramdecls in + let args = Array.of_list args in + if Array.length args < nparams then + raise (IllFormedInd (LocalNotEnoughArgs ind_index)); + let (params,realargs) = Array.chop nparams args in + let nparamdecls = List.length paramdecls in + let rec check param_index paramdecl_index = function | [] -> () - | LocalDef _ :: hyps -> check k (index+1) hyps - | _::hyps -> - match whd_all env lpar.(k) with - | Rel w when w = index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l))) - in check (nparams-1) (n-nhyps) hyps; - if not (Array.for_all (noccur_between n ntypes) largs') then - failwith_non_pos_vect n ntypes largs' + | LocalDef _ :: paramdecls -> + check param_index (paramdecl_index+1) paramdecls + | _::paramdecls -> + match whd_all env params.(param_index) with + | Rel w when Int.equal w paramdecl_index -> + check (param_index-1) (paramdecl_index+1) paramdecls + | _ -> + let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in + let err = + LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in + raise (IllFormedInd err) + in check (nparams-1) (n-nparamdecls) paramdecls; + if not (Array.for_all (noccur_between n ntypes) realargs) then + failwith_non_pos_vect n ntypes realargs (* Arguments of constructor: check the number of recursive parameters nrecp. the first parameters which are constant in recursive arguments @@ -412,8 +418,8 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc | Some b -> check_pos (ienv_push_var ienv (na, b, mk_norec)) d) | Rel k -> - (try - let (ra,rarg) = List.nth ra_env (k-1) in + (try let (ra,rarg) = List.nth ra_env (k-1) in + let largs = List.map (whd_all env) largs in (match ra with Mrec _ -> check_rec_par ienv hyps nrecp largs | _ -> ()); diff --git a/checker/inductive.ml b/checker/inductive.ml index d15380643f..5e34f04f51 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -282,6 +282,11 @@ let get_instantiated_arity (ind,u) (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim +let is_primitive_record (mib,_) = + match mib.mind_record with + | PrimRecord _ -> true + | NotRecord | FakeRecord -> false + let extended_rel_list n hyps = let rec reln l p = function | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps @@ -381,12 +386,13 @@ let type_case_branches env (pind,largs) (p,pj) c = (* Checking the case annotation is relevant *) let check_case_info env indsp ci = - let (mib,mip) = lookup_mind_specif env indsp in + let mib, mip as spec = lookup_mind_specif env indsp in if not (eq_ind_chk indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || - (mip.mind_consnrealargs <> ci.ci_cstr_nargs) + (mip.mind_consnrealargs <> ci.ci_cstr_nargs) || + is_primitive_record spec then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) @@ -801,10 +807,23 @@ let rec subterm_specif renv stack t = subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) - | (Meta _|Evar _) -> Dead_code - - (* Other terms are not subterms *) - | _ -> Not_subterm + | (Meta _|Evar _) -> Dead_code + + | Proj (p, c) -> + let subt = subterm_specif renv stack c in + (match subt with + | Subterm (_s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let n = Projection.arg p in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) + + (* Other terms are not subterms *) + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ + | Construct _ | CoFix _ -> Not_subterm and lazy_subterm_specif renv stack t = lazy (subterm_specif renv stack t) @@ -856,6 +875,8 @@ let filter_stack_domain env p stack = match stack, t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in + let ctx, a = dest_prod_assum env a in + let env = push_rel_context ctx env in let ty, args = decompose_app (whd_all env a) in let elt = match ty with | Ind ind -> diff --git a/checker/reduction.ml b/checker/reduction.ml index d36c0ef2c9..58a3f4e410 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -280,17 +280,26 @@ let get_strategy { var_opacity; cst_opacity } = function with Not_found -> default_level) | RelKey _ -> Expand +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + let oracle_order infos l2r k1 k2 = let o = Closure.oracle_of_infos infos in match get_strategy o k1, get_strategy o k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let eq_table_key univ = diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 0916d98ddf..e2c605dde8 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -198,9 +198,11 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= assert (Array.length mib2.mind_packets = 1); assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); - check - (fun l1 l2 -> List.equal Name.equal l1 l2) - (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); + check (List.equal Name.equal) + (fun mib -> + let nparamdecls = List.length mib.mind_params_ctxt in + let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in + snd (List.chop nparamdecls names)) end; (* we first check simple things *) Array.iter2 check_packet mib1.mind_packets mib2.mind_packets; |