diff options
| -rw-r--r-- | checker/closure.ml | 27 | ||||
| -rw-r--r-- | checker/environ.ml | 6 | ||||
| -rw-r--r-- | checker/indtypes.ml | 15 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 9 |
5 files changed, 42 insertions, 17 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 6744269ec..6248b440f 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -165,16 +165,35 @@ type table_key = | VarKey of Id.t | RelKey of int +module KeyHash = +struct + type t = table_key + let equal k1 k2 = match k1, k2 with + | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 + | VarKey id1, VarKey id2 -> Id.equal id1 id2 + | RelKey i1, RelKey i2 -> Int.equal i1 i2 + | (ConstKey _ | VarKey _ | RelKey _), _ -> false + + open Hashset.Combine + + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +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 : (table_key, 'a) Hashtbl.t } + i_tab : 'a KeyTable.t } let ref_value_cache info ref = try - Some (Hashtbl.find info.i_tab ref) + Some (KeyTable.find info.i_tab ref) with Not_found -> try let body = @@ -185,7 +204,7 @@ let ref_value_cache info ref = | ConstKey cst -> constant_value info.i_env cst in let v = info.i_repr info body in - Hashtbl.add info.i_tab ref v; + KeyTable.add info.i_tab ref v; Some v with | Not_found (* List.assoc *) @@ -214,7 +233,7 @@ let create mk_cl flgs env = i_repr = mk_cl; i_env = env; i_rels = defined_rels flgs env; - i_tab = Hashtbl.create 17 } + i_tab = KeyTable.create 17 } (**********************************************************************) diff --git a/checker/environ.ml b/checker/environ.ml index be6bdec11..eb084a910 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -126,8 +126,8 @@ let scrape_mind env kn= Not_found -> kn let mind_equiv env (kn1,i1) (kn2,i2) = - i1 = i2 && - scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2) + Int.equal i1 i2 && + KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2)) let lookup_mind kn env = @@ -139,7 +139,7 @@ let add_mind kn mib env = (string_of_mind kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = user_mind kn,canonical_mind kn in - let new_inds_eq = if kn1=kn2 then + let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq else KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 9f0f5844b..a64232442 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -38,7 +38,7 @@ let prkn kn = let prcon c = let ck = canonical_con c in let uk = user_con c in - if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") + if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. Could be refined more... *) @@ -109,7 +109,9 @@ let is_small_sort = function | Prop _ -> true | _ -> false -let is_logic_sort s = (s = Prop Null) +let is_logic_sort = function +| Prop Null -> true +| _ -> false (* [infos] is a sequence of pair [islogic,issmall] for each type in the product of a constructor or arity *) @@ -402,7 +404,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let x,largs = decompose_app (whd_betadeltaiota env c) in match x with | Prod (na,b,d) -> - assert (largs = []); + assert (List.is_empty largs); (match weaker_noccur_between env n ntypes b with None -> failwith_non_pos_list n ntypes [b] | Some b -> @@ -471,16 +473,17 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let x,largs = decompose_app (whd_betadeltaiota env c) in match x with | Prod (na,b,d) -> - assert (largs = []); + assert (List.is_empty largs); let recarg = check_pos ienv b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' (recarg::lrec) d | hd -> if check_head then - if hd = Rel (n+ntypes-i-1) then + match hd with + | Rel j when j = (n + ntypes - i - 1) -> check_correct_par ienv hyps (ntypes-i) largs - else + | _ -> raise (IllFormedInd LocalNotConstructor) else if not (List.for_all (noccur_between n ntypes) largs) diff --git a/checker/reduction.ml b/checker/reduction.ml index e07a3128b..54d79484e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -320,7 +320,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> - if j1 = j2 && mind_equiv_infos infos ind1 ind2 + if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible diff --git a/checker/values.ml b/checker/values.ml index f73f83d16..b3c070b19 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 96dc15ee04e3baa6502b4d78c35d4b76 checker/cic.mli +MD5 c0f79d23d0eb5d2e4cfb53ead514fcf5 checker/cic.mli *) @@ -65,6 +65,9 @@ let v_map vk vd = [|[|m; Annot("key",vk); Annot("data",vd); m; Annot("bal",Int)|]|]) in m +let v_hset v = v_map Int (v_set v) +let v_hmap vk vd = v_map Int (v_map vk vd) + (* lib/future *) let v_computation f = Annot ("Future.computation", @@ -82,7 +85,7 @@ let rec v_mp = Sum("module_path",0, [|[|v_dp|]; [|v_uid|]; [|v_mp;v_id|]|]) -let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id|] +let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;Int|] let v_cons = v_tuple "constructor" [|v_ind;Int|] @@ -157,7 +160,7 @@ let v_delta_hint = let v_resolver = v_tuple "delta_resolver" [|v_map v_mp v_mp; - v_map v_kn v_delta_hint|] + v_hmap v_kn v_delta_hint|] let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|] |