diff options
Diffstat (limited to 'checker')
35 files changed, 517 insertions, 311 deletions
diff --git a/checker/analyze.ml b/checker/analyze.ml index df75d5b93c..7047d8a149 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -55,6 +55,55 @@ let magic_number = "\132\149\166\190" (** Memory reification *) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end = +struct + + let max_length = Sys.max_array_length + + type 'a t = 'a array array * 'a array + (** Invariants: + - All subarrays of the left array have length [max_length]. + - The right array has length < [max_length]. + *) + + let empty = [||], [||] + + let length (vl, vr) = + (max_length * Array.length vl) + Array.length vr + + let make n x = + let k = n / max_length in + let r = n mod max_length in + let vl = Array.init k (fun _ -> Array.make max_length x) in + let vr = Array.make r x in + (vl, vr) + + let get (vl, vr) n = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) + else if k == len then vr.(r) + else invalid_arg "index out of bounds" + + let set (vl, vr) n x = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) <- x + else if k == len then vr.(r) <- x + else invalid_arg "index out of bounds" + +end + type repr = | RInt of int | RBlock of (int * int) (* tag × len *) @@ -82,7 +131,7 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) end module Make(M : Input) = @@ -261,7 +310,7 @@ let parse_object chan = let parse chan = let (magic, len, _, _, size) = parse_header chan in let () = assert (magic = magic_number) in - let memory = Array.make size (Struct ((-1), [||])) in + let memory = LargeArray.make size (Struct ((-1), [||])) in let current_object = ref 0 in let fill_obj = function | RPointer n -> @@ -272,7 +321,7 @@ let parse chan = data, None | RString s -> let data = Ptr !current_object in - let () = memory.(!current_object) <- String s in + let () = LargeArray.set memory !current_object (String s) in let () = incr current_object in data, None | RBlock (tag, 0) -> @@ -282,7 +331,7 @@ let parse chan = | RBlock (tag, len) -> let data = Ptr !current_object in let nblock = Array.make len (Atm (-1)) in - let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in let () = incr current_object in data, Some nblock | RCode addr -> @@ -343,3 +392,32 @@ module PString = Make(IString) let parse_channel = PChannel.parse let parse_string s = PString.parse (s, ref 0) + +let instantiate (p, mem) = + let len = LargeArray.length mem in + let ans = LargeArray.make len (Obj.repr 0) in + (** First pass: initialize the subobjects *) + for i = 0 to len - 1 do + let obj = match LargeArray.get mem i with + | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) + | String str -> Obj.repr str + in + LargeArray.set ans i obj + done; + let get_data = function + | Int n -> Obj.repr n + | Ptr p -> LargeArray.get ans p + | Atm tag -> Obj.new_block tag 0 + | Fun _ -> assert false (** We shouldn't serialize closures *) + in + (** Second pass: set the pointers *) + for i = 0 to len - 1 do + match LargeArray.get mem i with + | Struct (_, blk) -> + let obj = LargeArray.get ans i in + for k = 0 to Array.length blk - 1 do + Obj.set_field obj k (get_data blk.(k)) + done + | String _ -> () + done; + get_data p diff --git a/checker/analyze.mli b/checker/analyze.mli index 42efcf01df..9c837643fa 100644 --- a/checker/analyze.mli +++ b/checker/analyze.mli @@ -8,8 +8,20 @@ type obj = | Struct of int * data array (* tag × data *) | String of string -val parse_channel : in_channel -> (data * obj array) -val parse_string : string -> (data * obj array) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end +(** A data structure similar to arrays but allowing to overcome the 2^22 length + limitation on 32-bit architecture. *) + +val parse_channel : in_channel -> (data * obj LargeArray.t) +val parse_string : string -> (data * obj LargeArray.t) (** {6 Functorized version} *) @@ -26,10 +38,13 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) (** Return the entry point and the reification of the memory out of a marshalled structure. *) end module Make (M : Input) : S with type input = M.t (** Functorized version of the previous code. *) + +val instantiate : data * obj LargeArray.t -> Obj.t +(** Create the OCaml object out of the reified representation. *) diff --git a/checker/check.ml b/checker/check.ml index 180ca1ece1..82341ad9b2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -22,6 +22,11 @@ let extend_dirpath p id = DirPath.make (id :: DirPath.repr p) type section_path = { dirpath : string list ; basename : string } + +type object_file = +| PhysicalFile of CUnix.physical_path +| LogicalFile of section_path + let dir_of_path p = DirPath.make (List.map Id.of_string p.dirpath) let path_of_dirpath dir = @@ -69,11 +74,6 @@ let libraries_table = ref LibraryMap.empty let find_library dir = LibraryMap.find dir !libraries_table -let try_find_library dir = - try find_library dir - with Not_found -> - user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir))) - let library_full_filename dir = (find_library dir).library_filename (* If a library is loaded several time, then the first occurrence must @@ -129,8 +129,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -let get_load_paths () = fst !load_paths - (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) @@ -227,13 +225,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in @@ -263,7 +256,17 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) | LibNotFound -> error_lib_not_found (path_of_dirpath dir) -let try_locate_qualified_library qid = +let try_locate_qualified_library lib = match lib with +| PhysicalFile f -> + let () = + if not (System.file_exists_respecting_case "" f) then + error_lib_not_found { dirpath = []; basename = f; } + in + let dir = Filename.dirname f in + let base = Filename.chop_extension (Filename.basename f) in + let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in + (dir, f) +| LogicalFile qid -> try locate_qualified_library qid with @@ -298,18 +301,27 @@ let name_clash_message dir mdir f = (* Dependency graph *) let depgraph = ref LibraryMap.empty +let marshal_in_segment f ch = + try + let stop = input_binary_int ch in + let v = Analyze.instantiate (Analyze.parse_channel ch) in + let digest = Digest.input ch in + Obj.obj v, stop, digest + with _ -> + user_err (str "Corrupted file " ++ quote (str f)) + let intern_from_file (dir, f) = Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in - let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in - let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in - let (discharging:'a option), _, _ = System.marshal_in_segment f ch in - let (tasks:'a option), _, _ = System.marshal_in_segment f ch in + let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in + let (opaque_csts:'a 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:Cic.opaque_table), pos, checksum = - System.marshal_in_segment f ch in + marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in let ch = open_in_bin f in @@ -412,9 +424,3 @@ let recheck_library ~norec ~admit ~check = (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") - -open Printf - -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk" (CObj.size_kb m))) diff --git a/checker/check.mli b/checker/check.mli new file mode 100644 index 0000000000..28ae385b5b --- /dev/null +++ b/checker/check.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CUnix +open Names + +type section_path = { + dirpath : string list; + basename : string; +} + +type object_file = +| PhysicalFile of physical_path +| LogicalFile of section_path + +type logical_path = DirPath.t + +val default_root_prefix : DirPath.t + +val add_load_path : physical_path * logical_path -> unit + +val recheck_library : + norec:object_file list -> + admit:object_file list -> + check:object_file list -> unit diff --git a/checker/check.mllib b/checker/check.mllib index 488507a13f..f79ba66e35 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,6 @@ Coq_config +Analyze Hook Terminal Canary diff --git a/checker/checker.ml b/checker/checker.ml index e960a55fd2..b8b4d5dc2c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -40,9 +40,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -95,17 +96,13 @@ let add_rec_path ~unix_path ~coq_root = (* By the option -include -I or -R of the command line *) let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +let push_include (s, alias) = includes := (s,alias) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = @@ -131,8 +128,7 @@ let init_load_path () = add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -144,15 +140,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list @@ -178,7 +174,9 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -R dir coqdir map physical dir to logical coqdir\ +" -Q dir coqdir map physical dir to logical coqdir\ +\n -R dir coqdir synonymous for -Q\ +\n\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -210,8 +208,7 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report" ++ - strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") +let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".") let guill s = str "\"" ++ str s ++ str "\"" @@ -310,6 +307,9 @@ let explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) +let deprecated flag = + Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) + let parse_args argv = let rec parse = function | [] -> () @@ -323,12 +323,15 @@ let parse_args argv = Flags.coqlib_spec := true; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: d :: p :: rem -> set_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + + | "-R" :: d :: p :: rem -> set_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem diff --git a/checker/checker.mli b/checker/checker.mli new file mode 100644 index 0000000000..ceab137747 --- /dev/null +++ b/checker/checker.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val start : unit -> unit diff --git a/checker/cic.mli b/checker/cic.mli index 753fd0fc00..95dd18f5f3 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -81,7 +81,7 @@ type 'constr pfixpoint = type 'constr pcofixpoint = int * 'constr prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -127,12 +127,12 @@ type section_context = unit type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -type delta_resolver = module_path MPmap.t * delta_hint KNmap.t +type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t type 'a umap_t = 'a MPmap.t * 'a MBImap.t -type substitution = (module_path * delta_resolver) umap_t +type substitution = (ModPath.t * delta_resolver) umap_t (** {6 Delayed constr} *) @@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet type engagement = set_predicativity +(** {6 Conversion oracle} *) + +type level = Expand | Level of int | Opaque + +type oracle = { + var_opacity : level Id.Map.t; + cst_opacity : level Cmap.t; + var_trstate : Id.Pred.t; + cst_trstate : Cpred.t; +} + (** {6 Representation of constants (Definition/Axiom) } *) @@ -194,7 +205,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : mutual_inductive; + proj_ind : MutInd.t; proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) @@ -208,7 +219,7 @@ type constant_def = | OpaqueDef of lazy_constr type constant_universes = - | Monomorphic_const of Univ.universe_context + | Monomorphic_const of Univ.ContextSet.t | Polymorphic_const of Univ.abstract_universe_context (** The [typing_flags] are instructions to the type-checker which @@ -219,6 +230,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : oracle; (** Unfolding strategies for conversion *) } type constant_body = { @@ -241,7 +253,7 @@ type recarg = type wf_paths = recarg Rtree.t -type record_body = (Id.t * constant array * projection_body array) option +type record_body = (Id.t * Constant.t array * projection_body array) option (* The body is empty for non-primitive records, otherwise we get its binder name in projections and list of projections if it is primitive. *) @@ -303,7 +315,7 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context + | Monomorphic_ind of Univ.ContextSet.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info @@ -347,12 +359,12 @@ type ('ty,'a) functorize = only for short module printing and for extraction. *) type with_declaration = - | WithMod of Id.t list * module_path + | WithMod of Id.t list * ModPath.t | WithDef of Id.t list * (constr * Univ.universe_context) type module_alg_expr = - | MEident of module_path - | MEapply of module_alg_expr * module_path + | MEident of ModPath.t + | MEapply of module_alg_expr * ModPath.t | MEwith of module_alg_expr * with_declaration (** A component of a module structure *) @@ -386,7 +398,7 @@ and module_implementation = | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) and 'a generic_module_body = - { mod_mp : module_path; (** absolute path of the module *) + { mod_mp : ModPath.t; (** absolute path of the module *) mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) diff --git a/checker/closure.ml b/checker/closure.ml index 70718bfdca..14b31e09d6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -49,13 +49,6 @@ let with_stats c = end else Lazy.force c -type transparent_state = Id.Pred.t * Cpred.t -let all_opaque = (Id.Pred.empty, Cpred.empty) -let all_transparent = (Id.Pred.full, Cpred.full) - -let is_transparent_variable (ids, _) id = Id.Pred.mem id ids -let is_transparent_constant (_, csts) cst = Cpred.mem cst csts - module type RedFlagsSig = sig type reds type red_kind @@ -63,8 +56,6 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind - val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds val mkflags : red_kind list -> reds @@ -80,51 +71,33 @@ module RedFlags = (struct type reds = { r_beta : bool; r_delta : bool; - r_const : transparent_state; r_zeta : bool; r_evar : bool; r_iota : bool } type red_kind = BETA | DELTA | IOTA | ZETA - | CONST of constant | VAR of Id.t + let fBETA = BETA let fDELTA = DELTA let fIOTA = IOTA let fZETA = ZETA - let fCONST kn = CONST kn - let fVAR id = VAR id let no_red = { r_beta = false; r_delta = false; - r_const = all_opaque; r_zeta = false; r_evar = false; r_iota = false } let red_add red = function | BETA -> { red with r_beta = true } - | DELTA -> { red with r_delta = true; r_const = all_transparent } - | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.add kn l2 } + | DELTA -> { red with r_delta = true} | IOTA -> { red with r_iota = true } | ZETA -> { red with r_zeta = true } - | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.add id l1, l2 } let mkflags = List.fold_left red_add no_red let red_set red = function | BETA -> incr_cnt red.r_beta beta - | CONST kn -> - let (_,l) = red.r_const in - let c = Cpred.mem kn l in - incr_cnt c delta - | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (l,_) = red.r_const in - let c = Id.Pred.mem id l in - incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | IOTA -> incr_cnt red.r_iota iota | DELTA -> (* Used for Rel/Var defined in context *) @@ -165,7 +138,7 @@ type 'a tableKey = | VarKey of Id.t | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey module KeyHash = struct @@ -279,11 +252,10 @@ and fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *) | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -306,7 +278,6 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack @@ -456,13 +427,10 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> Const op | FInd op -> Ind op | FConstruct op -> Construct op - | FCase (ci,p,c,ve) -> - Case (ci, constr_fun lfts p, - constr_fun lfts c, - Array.map (constr_fun lfts) ve) - | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *) - to_constr constr_fun lfts - {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)} + | FCaseT (ci,p,c,ve,e) -> + let fp = mk_clos2 e p in + let fve = mk_clos_vect e ve in + Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in let ftys = Array.map (mk_clos e) tys in @@ -532,9 +500,6 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -616,7 +581,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -708,6 +673,9 @@ let contract_fix_vect fix = in (subs_cons(Array.init nfix make_body, env), thisbody) +let unfold_projection env p = + let pb = lookup_projection p env in + Zproj (pb.proj_npars, pb.proj_arg, p) (*********************************************************************) (* A machine that inspects the head of a term until it finds an @@ -720,7 +688,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -729,10 +696,9 @@ let rec knh info m stk = | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - if red_set info.i_flags (fCONST (Projection.constant p)) then - (let pb = lookup_projection p (info.i_env) in - knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) - :: zupdate m stk)) + if red_set info.i_flags fDELTA then + let s = unfold_projection info.i_env p in + knh info c (s :: zupdate m stk) else (m,stk) (* cases where knh stops *) @@ -764,11 +730,11 @@ let rec knr info m stk = (match get_args n tys f e stk with Inl e', s -> knit info e' f s | Inr lam, s -> (lam,s)) - | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) -> + | FFlex(ConstKey kn) when red_set info.i_flags fDELTA -> (match ref_value_cache info (ConstKey kn) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> + | FFlex(VarKey id) when red_set info.i_flags fDELTA -> (match ref_value_cache info (VarKey id) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) @@ -778,10 +744,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (depth, args, Zcase(ci,_,br)::s) -> - assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - kni info br.(c-1) (rargs@s) | (depth, args, ZcaseT(ci,_,br,env)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -798,7 +760,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) @@ -835,6 +797,7 @@ 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 diff --git a/checker/closure.mli b/checker/closure.mli index ed5bb3d094..7bdc21b605 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) -type transparent_state = Id.Pred.t * Cpred.t - -val all_opaque : transparent_state -val all_transparent : transparent_state - -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool - (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -42,8 +34,6 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind - val fVAR : Id.t -> red_kind (* No reduction at all *) val no_red : reds @@ -71,7 +61,7 @@ type 'a tableKey = | VarKey of Id.t | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option @@ -98,11 +88,10 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -115,7 +104,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack @@ -133,6 +121,8 @@ val eta_expand_stack : stack -> stack val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack +val unfold_projection : env -> Projection.t -> stack_member + (* To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use a reduction function *) @@ -142,13 +132,15 @@ val inject : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (* Global and local constant cache *) type clos_infos val create_clos_infos : reds -> env -> clos_infos val infos_env : clos_infos -> env val infos_flags : clos_infos -> reds +val oracle_of_infos : clos_infos -> oracle + (* Reduction function *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 884a1ef18c..15b1f0a0c6 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -484,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true - | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 - | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 + | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2 + | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2 | _ -> false let eq_wf_paths = Rtree.equal eq_recarg diff --git a/checker/declarations.mli b/checker/declarations.mli index 6fc71bb942..7458b3e0b0 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -34,12 +34,12 @@ val empty_delta_resolver : delta_resolver type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_mbid : MBId.t -> module_path -> substitution -> substitution -val add_mp : module_path -> module_path -> substitution -> substitution -val map_mbid : MBId.t -> module_path -> substitution -val map_mp : module_path -> module_path -> substitution -val mp_in_delta : module_path -> delta_resolver -> bool -val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive +val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution +val add_mp : ModPath.t -> ModPath.t -> substitution -> substitution +val map_mbid : MBId.t -> ModPath.t -> substitution +val map_mp : ModPath.t -> ModPath.t -> substitution +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun diff --git a/checker/environ.ml b/checker/environ.ml index a0818012c7..bbd043c8e9 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -8,7 +8,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -21,7 +21,15 @@ type env = { env_globals : globals; env_rel_context : rel_context; env_stratification : stratification; - env_imports : Cic.vodigest MPmap.t } + env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : oracle; } + +let empty_oracle = { + var_opacity = Id.Map.empty; + cst_opacity = Cmap.empty; + var_trstate = Id.Pred.empty; + cst_trstate = Cpred.empty; +} let empty_env = { env_globals = @@ -34,7 +42,8 @@ let empty_env = { env_stratification = { env_universes = Univ.initial_universes; env_engagement = PredicativeSet }; - env_imports = MPmap.empty } + env_imports = MPmap.empty; + env_conv_oracle = empty_oracle } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes @@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env = { env with env_stratification = { env.env_stratification with env_engagement = c } } +let set_oracle env oracle = { env with env_conv_oracle = oracle } + (* Digests *) let add_digest env dp digest = @@ -115,7 +126,7 @@ let add_constant kn cs env = env_constants = new_constants } in { env with env_globals = new_globals } -type const_evaluation_result = NoBody | Opaque | IsProj +type const_evaluation_result = NoBody | Opaque (* Constant types *) @@ -137,18 +148,16 @@ exception NotEvaluableConst of const_evaluation_result let constant_value env (kn,u) = let cb = lookup_constant kn env in - if cb.const_proj = None then - match cb.const_body with - | Def l_body -> - let b = force_constr l_body in - begin - match cb.const_universes with - | Monomorphic_const _ -> b - | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body) - end - | OpaqueDef _ -> raise (NotEvaluableConst Opaque) - | Undef _ -> raise (NotEvaluableConst NoBody) - else raise (NotEvaluableConst IsProj) + match cb.const_body with + | Def l_body -> + let b = force_constr l_body in + begin + match cb.const_universes with + | Monomorphic_const _ -> b + | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body) + end + | OpaqueDef _ -> raise (NotEvaluableConst Opaque) + | Undef _ -> raise (NotEvaluableConst NoBody) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = diff --git a/checker/environ.mli b/checker/environ.mli index 8e8d0fd49c..36e0ea0274 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -6,7 +6,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} type stratification = { @@ -18,6 +18,7 @@ type env = { env_rel_context : rel_context; env_stratification : stratification; env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : Cic.oracle; } val empty_env : env @@ -25,6 +26,10 @@ val empty_env : env val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env +(** Oracle *) + +val set_oracle : env -> Cic.oracle -> env + (* Digests *) val add_digest : env -> DirPath.t -> Cic.vodigest -> env val lookup_digest : env -> DirPath.t -> Cic.vodigest @@ -34,7 +39,7 @@ val rel_context : env -> rel_context val lookup_rel : int -> env -> rel_declaration val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env -val push_rec_types : name array * constr array * 'a -> env -> env +val push_rec_types : Name.t array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes @@ -44,31 +49,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) -val lookup_constant : constant -> env -> Cic.constant_body -val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constr Univ.constrained -type const_evaluation_result = NoBody | Opaque | IsProj +val lookup_constant : Constant.t -> env -> Cic.constant_body +val add_constant : Constant.t -> Cic.constant_body -> env -> env +val constant_type : env -> Constant.t puniverses -> constr Univ.constrained +type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant puniverses -> constr -val evaluable_constant : constant -> env -> bool +val constant_value : env -> Constant.t puniverses -> constr +val evaluable_constant : Constant.t -> env -> bool -val is_projection : constant -> env -> bool +val is_projection : Constant.t -> env -> bool val lookup_projection : projection -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool val lookup_mind : - mutual_inductive -> env -> Cic.mutual_inductive_body + MutInd.t -> env -> Cic.mutual_inductive_body val add_mind : - mutual_inductive -> Cic.mutual_inductive_body -> env -> env + MutInd.t -> Cic.mutual_inductive_body -> env -> env (* Modules *) val add_modtype : - module_path -> Cic.module_type_body -> env -> env + ModPath.t -> Cic.module_type_body -> env -> env val shallow_add_module : - module_path -> Cic.module_body -> env -> env -val shallow_remove_module : module_path -> env -> env -val lookup_module : module_path -> env -> Cic.module_body -val lookup_modtype : module_path -> env -> Cic.module_type_body + ModPath.t -> Cic.module_body -> env -> env +val shallow_remove_module : ModPath.t -> env -> env +val lookup_module : ModPath.t -> env -> Cic.module_body +val lookup_modtype : ModPath.t -> env -> Cic.module_type_body diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 22c8438126..4de5977666 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -502,10 +502,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc indlc in mk_paths (Mrec ind) irecargs +let prrecarg = function + | Norec -> str "Norec" + | Mrec (mind,i) -> + str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + | Imbr (mind,i) -> + str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + let check_subtree t1 t2 = let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in if not (Rtree.equiv eq_recarg cmp_labels t1 t2) - then failwith "bad recursive trees" + then user_err Pp.(str "Bad recursive tree: found " ++ fnl () + ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl () + ++ Rtree.pp_tree prrecarg t2) (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) let check_positivity env_ar mind params nrecp inds = @@ -586,6 +595,8 @@ let check_inductive env kn mib = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in let env = Environ.push_context ind_ctx env in + (** Locally set the oracle for further typechecking *) + let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in (* check mind_record : TODO ? check #constructor = 1 ? *) (* check mind_finite : always OK *) (* check mind_ntypes *) @@ -593,13 +604,13 @@ let check_inductive env kn mib = user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in - let _ = check_ctxt env params in + let _ = check_ctxt env0 params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) - let env_ar = typecheck_arity env params mib.mind_packets in + let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check the inferred subtyping relation *) diff --git a/checker/indtypes.mli b/checker/indtypes.mli index b0554989ef..5d4c3ee994 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -12,8 +12,8 @@ open Cic open Environ (*i*) -val prkn : kernel_name -> Pp.t -val prcon : constant -> Pp.t +val prkn : KerName.t -> Pp.t +val prcon : Constant.t -> Pp.t (*s The different kinds of errors that may result of a malformed inductive definition. *) @@ -34,4 +34,4 @@ exception InductiveError of inductive_error (*s The following function does checks on inductive declarations. *) -val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env +val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env diff --git a/checker/inductive.ml b/checker/inductive.ml index 1271a02b0e..8d426a3c05 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -381,7 +381,7 @@ let type_case_branches env (pind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) || + 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) @@ -435,20 +435,14 @@ type subterm_spec = | Dead_code | Not_subterm -let eq_recarg r1 r2 = match r1, r2 with -| Norec, Norec -> true -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false - let eq_wf_paths = Rtree.equal eq_recarg let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 | Imbr i1, Imbr i2 -| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None -| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None +| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None | _ -> None let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec @@ -544,7 +538,7 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | (Mrec i | Imbr i) -> eq_ind ind i + | (Mrec i | Imbr i) -> eq_ind_chk ind i | Norec -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} @@ -645,7 +639,7 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> + | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' -> build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end @@ -1070,8 +1064,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/checker/inductive.mli b/checker/inductive.mli index 8f605935db..0170bbc942 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: diff --git a/checker/main.mli b/checker/main.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/checker/main.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 63e28448f9..7685863eab 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,10 +26,13 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); + (** Locally set the oracle for further typechecking *) + let oracle = env.env_conv_oracle in + let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in (** [env'] contains De Bruijn universe variables *) let env' = match cb.const_universes with - | Monomorphic_const ctx -> push_context ~strict:true ctx env + | Monomorphic_const ctx -> push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in push_context ~strict:false ctx env @@ -53,8 +56,12 @@ let check_constant_declaration env kn cb = conv_leq envty j ty) | None -> () in - if constant_is_polymorphic cb then add_constant kn cb env - else add_constant kn cb env' + let env = + if constant_is_polymorphic cb then add_constant kn cb env + else add_constant kn cb env' + in + (** Reset the value of the oracle *) + Environ.set_oracle env oracle (** {6 Checking modules } *) diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 16a3792aa1..c7af8b286a 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -6,4 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -val check_module : Environ.env -> Names.module_path -> Cic.module_body -> unit +val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit diff --git a/checker/modops.mli b/checker/modops.mli index 0efff63c82..b73557d926 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -15,7 +15,7 @@ open Environ (* Various operations on modules and module types *) val module_type_of_module : - module_path option -> module_body -> module_type_body + ModPath.t option -> module_body -> module_type_body val is_functor : ('ty,'a) functorize -> bool @@ -24,24 +24,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val add_module_type : module_path -> module_type_body -> env -> env +val add_module_type : ModPath.t -> module_type_body -> env -> env -val strengthen : module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> ModPath.t -> module_type_body -val subst_and_strengthen : module_body -> module_path -> module_body +val subst_and_strengthen : module_body -> ModPath.t -> module_body val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a -val error_not_match : label -> structure_field_body -> 'a +val error_not_match : Label.t -> structure_field_body -> 'a val error_with_module : unit -> 'a -val error_no_such_label : label -> 'a +val error_no_such_label : Label.t -> 'a val error_no_such_label_sub : - label -> module_path -> 'a + Label.t -> ModPath.t -> 'a -val error_not_a_constant : label -> 'a +val error_not_a_constant : Label.t -> 'a -val error_not_a_module : label -> 'a +val error_not_a_module : Label.t -> 'a diff --git a/checker/print.mli b/checker/print.mli new file mode 100644 index 0000000000..3b2715de92 --- /dev/null +++ b/checker/print.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Cic + +val print_pure_constr : constr -> unit diff --git a/checker/reduction.ml b/checker/reduction.ml index 6d8783d7e5..29bb8901e6 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -42,8 +42,8 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | ((ZcaseT(c1,_,_,_))::s1, + (ZcaseT(c2,_,_,_))::s2) -> bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -78,8 +78,7 @@ let pure_stack lfts stk = (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,env),(l,pstk)) -> (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + ) in snd (pure_rec lfts stk) (****************************************************************************) @@ -243,7 +242,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -256,7 +254,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -266,13 +263,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,_) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk @@ -280,16 +276,29 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false -let oracle_order fl1 fl2 = - match fl1,fl2 with - ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false - | _, ConstKey _ -> true - | _ -> false - -let unfold_projection infos p c = - let pb = lookup_projection p (infos_env infos) in - let s = Zproj (pb.proj_npars, pb.proj_arg, p) in - (c, s) +let default_level = Level 0 + +let get_strategy { var_opacity; cst_opacity } = function + | VarKey id -> + (try Names.Id.Map.find id var_opacity + with Not_found -> default_level) + | ConstKey (c, _) -> + (try Names.Cmap.find c cst_opacity + with Not_found -> default_level) + | RelKey _ -> Expand + +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, (Opaque | Level _) -> true + | (Opaque | Level _), Expand -> false + | Opaque, Opaque -> l2r + | Level _, Opaque -> true + | Opaque, Level _ -> false + | Level n1, Level n2 -> + if Int.equal n1 n2 then l2r + else n1 < n2 (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = @@ -343,7 +352,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = with NotConvertible -> (* else the oracle tells which constant is to be expanded *) let (app1,app2) = - if oracle_order fl1 fl2 then + if oracle_order infos false fl1 fl2 then match unfold_reference infos fl1 with | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) | None -> @@ -360,12 +369,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = eqappr univ cv_pb infos app1 app2) | (FProj (p1,c1), _) -> - let (def1, s1) = unfold_projection infos p1 c1 in - eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + let s1 = unfold_projection (infos_env infos) p1 in + eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2 | (_, FProj (p2,c2)) -> - let (def2, s2) = unfold_projection infos p2 c2 in - eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + let s2 = unfold_projection (infos_env infos) p2 in + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2)) (* other constructors *) | (FLambda _, FLambda _) -> @@ -504,8 +513,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) diff --git a/checker/term.mli b/checker/term.mli index 679a56ee45..2524dff189 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -38,8 +38,8 @@ val fold_rel_context_outside : 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 -val decompose_lam : constr -> (name * constr) list * constr +val compose_lam : (Name.t * constr) list -> constr -> constr +val decompose_lam : constr -> (Name.t * constr) list * constr val decompose_lam_n_assum : int -> constr -> rel_context * constr val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr diff --git a/checker/type_errors.ml b/checker/type_errors.ml index c5a69efdcd..5794d87136 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -52,14 +52,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * int * constr * constr - | Generalization of (name * constr) * unsafe_judgment + | Generalization of (Name.t * constr) * unsafe_judgment | ActualType of unsafe_judgment * constr | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * Name.t array * int | IllTypedRecBody of - int * name array * unsafe_judgment array * constr array + int * Name.t array * unsafe_judgment array * constr array | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error diff --git a/checker/type_errors.mli b/checker/type_errors.mli index b5f14c7189..f45144c234 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -54,14 +54,14 @@ type type_error = | WrongCaseInfo of inductive * case_info | NumberBranches of unsafe_judgment * int | IllFormedBranch of constr * int * constr * constr - | Generalization of (name * constr) * unsafe_judgment + | Generalization of (Name.t * constr) * unsafe_judgment | ActualType of unsafe_judgment * constr | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int + | IllFormedRecBody of guard_error * Name.t array * int | IllTypedRecBody of - int * name array * unsafe_judgment array * constr array + int * Name.t array * unsafe_judgment array * constr array | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -96,9 +96,9 @@ val error_cant_apply_bad_type : unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> name array -> int -> 'a + env -> guard_error -> Name.t array -> int -> 'a val error_ill_typed_rec_body : - env -> int -> name array -> unsafe_judgment array -> constr array -> 'a + env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a val error_unsatisfied_constraints : env -> Univ.constraints -> 'a diff --git a/checker/univ.ml b/checker/univ.ml index 4f31318132..7d01657df7 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -881,14 +881,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - module Instance : sig type t = Level.t array diff --git a/checker/univ.mli b/checker/univ.mli index 0eadc6801f..21c94d9529 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : diff --git a/checker/validate.ml b/checker/validate.ml index 8200405878..2624e6d495 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -49,8 +49,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx exception ValidObjError of string * error_context * Obj.t let fail ctx o s = raise (ValidObjError(s,ctx,o)) -type func = error_context -> Obj.t -> unit - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () diff --git a/checker/validate.mli b/checker/validate.mli new file mode 100644 index 0000000000..7eed692a0b --- /dev/null +++ b/checker/validate.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val validate : bool -> Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index 86634fbd80..313067cb6b 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 62a4037e9e584d508909d631c5e8a759 checker/cic.mli +MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli *) @@ -70,6 +70,8 @@ let v_map vk vd = let v_hset v = v_map Int (v_set v) let v_hmap vk vd = v_map Int (v_map vk vd) +let v_pred v = v_pair v_bool (v_set v) + (* lib/future *) let v_computation f = Annot ("Future.computation", @@ -199,6 +201,17 @@ let v_lazy_constr = let v_impredicative_set = v_enum "impr-set" 2 let v_engagement = v_impredicative_set +let v_conv_level = + v_sum "conv_level" 2 [|[|Int|]|] + +let v_oracle = + v_tuple "oracle" [| + v_map v_id v_conv_level; + v_hmap v_cst v_conv_level; + v_pred v_id; + v_pred v_cst; + |] + let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -213,9 +226,9 @@ let v_projbody = v_constr|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] -let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|] +let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -265,7 +278,7 @@ let v_mind_record = Annot ("mind_record", let v_ind_pack_univs = v_sum "abstract_inductive_universes" 0 - [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|] + [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|] let v_ind_pack = v_tuple "mutual_inductive_body" [|Array v_one_ind; @@ -372,22 +385,3 @@ let v_lib = let v_opaques = Array (v_computation v_constr) let v_univopaques = Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) - -(** Registering dynamic values *) - -module IntOrd = -struct - type t = int - let compare (x : t) (y : t) = compare x y -end - -module IntMap = Map.Make(IntOrd) - -let dyn_table : value IntMap.t ref = ref IntMap.empty - -let register_dyn name t = - dyn_table := IntMap.add name t !dyn_table - -let find_dyn name = - try IntMap.find name !dyn_table - with Not_found -> Any diff --git a/checker/values.mli b/checker/values.mli new file mode 100644 index 0000000000..aad8fd5f45 --- /dev/null +++ b/checker/values.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type value = + | Any + | Fail of string + | Tuple of string * value array + | Sum of string * int * value array array + | Array of value + | List of value + | Opt of value + | Int + | String + | Annot of string * value + | Dyn + +val v_univopaques : value +val v_libsum : value +val v_lib : value +val v_opaques : value +val v_stm_seg : value diff --git a/checker/votour.ml b/checker/votour.ml index 0998bb94b1..8cb97a2b1b 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,6 +10,8 @@ open Values (** {6 Interactive visit of a vo} *) +let max_string_length = 1024 + let rec read_num max = let quit () = Printf.printf "\nGoodbye!\n%!"; @@ -75,48 +77,51 @@ struct type obj = data - let memory = ref [||] - let sizes = ref [||] + let memory = ref LargeArray.empty + let sizes = ref LargeArray.empty (** size, in words *) let ws = Sys.word_size / 8 - let rec init_size seen = function - | Int _ | Atm _ | Fun _ -> 0 + let rec init_size seen k = function + | Int _ | Atm _ | Fun _ -> k 0 | Ptr p -> - if seen.(p) then 0 + if LargeArray.get seen p then k 0 else - let () = seen.(p) <- true in - match (!memory).(p) with + let () = LargeArray.set seen p true in + match LargeArray.get !memory p with | Struct (tag, os) -> - let fold accu o = accu + 1 + init_size seen o in - let size = Array.fold_left fold 1 os in - let () = (!sizes).(p) <- size in - size + let len = Array.length os in + let rec fold i accu k = + if i == len then k accu + else + init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i) + in + fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size) | String s -> let size = 2 + (String.length s / ws) in - let () = (!sizes).(p) <- size in - size + let () = LargeArray.set !sizes p size in + k size let size = function | Int _ | Atm _ | Fun _ -> 0 - | Ptr p -> (!sizes).(p) + | Ptr p -> LargeArray.get !sizes p let repr = function | Int i -> INT i | Atm t -> BLOCK (t, [||]) | Fun _ -> OTHER | Ptr p -> - match (!memory).(p) with + match LargeArray.get !memory p with | Struct (tag, os) -> BLOCK (tag, os) | String s -> STRING s let input ch = let obj, mem = parse_channel ch in let () = memory := mem in - let () = sizes := Array.make (Array.length mem) (-1) in - let seen = Array.make (Array.length mem) false in - let _ = init_size seen obj in + let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in + let seen = LargeArray.make (LargeArray.length mem) false in + let () = init_size seen ignore obj in obj let oid = function @@ -155,7 +160,8 @@ let get_string_in_tuple o = for i = 0 to Array.length o - 1 do match Repr.repr o.(i) with | STRING s -> - raise (TupleString (Printf.sprintf " [..%s..]" s)) + let len = min max_string_length (String.length s) in + raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len))) | _ -> () done; "" @@ -165,7 +171,8 @@ let get_string_in_tuple o = let rec get_details v o = match v, Repr.repr o with | (String | Any), STRING s -> - Printf.sprintf " [%s]" (String.escaped s) + let len = min max_string_length (String.length s) in + Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len)) |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o |(Sum _|Any), BLOCK (tag, _) -> Printf.sprintf " [tag=%i]" tag @@ -192,18 +199,17 @@ let access_children vs os pos = else raise Exit let access_list v o pos = - let rec loop o pos = match Repr.repr o with - | INT 0 -> [] + let rec loop o pos accu = match Repr.repr o with + | INT 0 -> List.rev accu | BLOCK (0, [|hd; tl|]) -> - (v, hd, 0 :: pos) :: loop tl (1 :: pos) + loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu) | _ -> raise Exit in - Array.of_list (loop o pos) + Array.of_list (loop o pos []) let access_block o = match Repr.repr o with | BLOCK (tag, os) -> (tag, os) | _ -> raise Exit -let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit (** raises Exit if the object has not the expected structure *) exception Forbidden @@ -227,14 +233,22 @@ let rec get_children v o pos = match v with | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] | _ -> raise Exit end - |String | Int -> [||] + | String -> + begin match Repr.repr o with + | STRING _ -> [||] + | _ -> raise Exit + end + | Int -> + begin match Repr.repr o with + | INT _ -> [||] + | _ -> raise Exit + end |Annot (s,v) -> get_children v o pos |Any -> raise Exit |Dyn -> begin match Repr.repr o with | BLOCK (0, [|id; o|]) -> - let n = access_int id in - let tpe = find_dyn n in + let tpe = Any in [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] | _ -> raise Exit end @@ -379,7 +393,7 @@ let visit_vo f = | None -> () done -let main = +let () = if not !Sys.interactive then Arg.parse [] visit_vo ("votour: guided tour of a Coq .vo or .vi file\n"^ diff --git a/checker/votour.mli b/checker/votour.mli new file mode 100644 index 0000000000..e1555ba2e2 --- /dev/null +++ b/checker/votour.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This empty file avoids a race condition that occurs when compiling a .ml file + that does not have a corresponding .mli file *) |