diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 12 | ||||
| -rw-r--r-- | checker/checkInductive.ml | 3 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 7 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
4 files changed, 10 insertions, 16 deletions
diff --git a/checker/check.ml b/checker/check.ml index 76f40dbac2..c5bc59e72a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -50,6 +50,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t +type seg_univ = Univ.ContextSet.t * bool type seg_proofs = Constr.constr option array type library_t = { @@ -90,7 +91,6 @@ let register_loaded_library m = (* Map from library names to table of opaque terms *) let opaque_tables = ref LibraryMap.empty -let opaque_univ_tables = ref LibraryMap.empty let access_opaque_table dp i = let t = @@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) = let ch = System.with_magic_number_check raw_intern_library f in let (sd:summary_disk), _, digest = marshal_in_segment f ch in let (md:library_disk), _, digest = marshal_in_segment f ch in - let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in + let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in let (discharging:'a option), _, _ = marshal_in_segment f ch in let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:seg_proofs option), pos, checksum = @@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) = (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin Flags.if_verbose chk_pp (str " (was a vio file) "); - Option.iter (fun (_,_,b) -> if not b then + Option.iter (fun (_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; @@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) = with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table; - Option.iter (fun (opaque_csts,_,_) -> - opaque_univ_tables := - LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) - opaque_csts; let extra_cst = Option.default Univ.ContextSet.empty - (Option.map (fun (_,cs,_) -> cs) opaque_csts) in + (Option.map (fun (cs,_) -> cs) opaque_csts) in mk_library sd md f table digest extra_cst let get_deps (dir, f) = diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4f4527ca12..b66e198234 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -75,8 +75,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> false -let check_kelim k1 k2 = - List.for_all (fun x -> List.mem_f Sorts.family_equal x k2) k1 +let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost the knowledge of who is the canonical version. diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 1cf07e7cc7..ccce0bd9a7 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -13,7 +13,6 @@ let set_indirect_accessor f = get_proof := f let indirect_accessor = { Opaqueproof.access_proof = (fun dp n -> !get_proof dp n); - Opaqueproof.access_constraints = (fun _ _ -> assert false); } let check_constant_declaration env kn cb = @@ -24,19 +23,19 @@ let check_constant_declaration env kn cb = (* [env'] contains De Bruijn universe variables *) let poly, env' = match cb.const_universes with - | Monomorphic ctx -> false, push_context_set ~strict:true ctx env + | Monomorphic ctx -> false, env | Polymorphic auctx -> let ctx = Univ.AUContext.repr auctx in let env = push_context ~strict:false ctx env in true, env in + let ty = cb.const_type in + let _ = infer_type env' ty in let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with | None, _ -> env' | Some local, (OpaqueDef _, true) -> push_subgraph local env' | Some _, _ -> assert false in - let ty = cb.const_type in - let _ = infer_type env' ty in let otab = Environ.opaque_tables env in let body = match cb.const_body with | Undef _ | Primitive _ -> None diff --git a/checker/values.ml b/checker/values.ml index 4b651cafb6..031f05dd6b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -257,7 +257,7 @@ let v_one_ind = v_tuple "one_inductive_body" Array v_constr; Int; Int; - List v_sortfam; + v_sortfam; Array (v_pair v_rctxt v_constr); Array Int; Array Int; @@ -385,4 +385,4 @@ let v_lib = let v_opaques = Array (Opt v_constr) let v_univopaques = - Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|])) + Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |