diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 33 | ||||
| -rw-r--r-- | checker/checker.ml | 15 | ||||
| -rw-r--r-- | checker/dune | 27 | ||||
| -rw-r--r-- | checker/include | 1 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 23 | ||||
| -rw-r--r-- | checker/validate.ml | 8 | ||||
| -rw-r--r-- | checker/values.ml | 26 | ||||
| -rw-r--r-- | checker/values.mli | 19 |
8 files changed, 55 insertions, 97 deletions
diff --git a/checker/check.ml b/checker/check.ml index e3a4bda8ec..30437e8bd0 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -136,36 +136,9 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -(* 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: "./" *) - let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p let find_logical_path phys_dir = - let phys_dir = canonical_path_name phys_dir in + let phys_dir = CUnix.canonical_path_name phys_dir in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir @@ -180,14 +153,14 @@ let add_load_path (phys_path,coq_path) = if !Flags.debug then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); - let phys_path = canonical_path_name phys_path in + let phys_path = CUnix.canonical_path_name phys_path in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_path) physical logical with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = canonical_path_name Filename.current_dir_name + (phys_path = CUnix.canonical_path_name Filename.current_dir_name && coq_path = default_root_prefix) then begin diff --git a/checker/checker.ml b/checker/checker.ml index 346ae5fffb..da6a61de1c 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -138,13 +138,16 @@ let set_debug () = Flags.debug := true let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet -let engage = Safe_typing.set_engagement (!impredicative_set) -let disable_compilers senv = +let indices_matter = ref false + +let make_senv () = + let senv = Safe_typing.empty_environment in + let senv = Safe_typing.set_engagement !impredicative_set senv in + let senv = Safe_typing.set_indices_matter !indices_matter senv in let senv = Safe_typing.set_VM false senv in Safe_typing.set_native_compiler false senv - let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list @@ -318,6 +321,9 @@ let parse_args argv = | "-impredicative-set" :: rem -> set_impredicative_set (); parse rem + | "-indices-matter" :: rem -> + indices_matter:=true; parse rem + | "-coqlib" :: s :: rem -> if not (exists_dir s) then fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; @@ -377,8 +383,7 @@ let init_with_argv argv = Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); - let senv = Safe_typing.empty_environment in - disable_compilers (engage senv) + make_senv () with e -> fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e) diff --git a/checker/dune b/checker/dune index 35a35a1f82..ee427d26c5 100644 --- a/checker/dune +++ b/checker/dune @@ -1,26 +1,3 @@ -(copy_files# - %{project_root}/kernel/{names,esubst,declarations,environ,constr,term,univ,evar,sorts,uGraph,context}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{mod_subst,vars,opaqueproof,conv_oracle,reduction,typeops,inductive,indtypes,declareops,type_errors}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{modops,mod_typing,}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{cClosure,cPrimitives,csymtable,vconv,vm,uint31,cemitcodes,vmvalues,cbytecodes,cinstr,retroknowledge,copcodes}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{cbytegen,clambda,nativeinstr,nativevalues,nativeconv,nativecode,nativelib,nativelibrary,nativelambda}.ml{,i}) - -(copy_files# - %{project_root}/kernel/{subtyping,term_typing,safe_typing,entries,cooking}.ml{,i}) - -; VM stuff - -(copy_files# - %{project_root}/kernel/byterun/{*.c,*.h}) - ; Careful with bug https://github.com/ocaml/odoc/issues/148 ; ; If we don't pack checker we will have a problem here due to @@ -30,10 +7,8 @@ (public_name coq.checklib) (synopsis "Coq's Standalone Proof Checker") (modules :standard \ coqchk votour) - (modules_without_implementation cinstr nativeinstr) - (c_names coq_fix_code coq_memory coq_values coq_interp) (wrapped true) - (libraries coq.lib)) + (libraries coq.kernel)) (executable (name coqchk) diff --git a/checker/include b/checker/include index da0346359b..3ffc301724 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp5";; #load "unix.cma";; #load"threads.cma";; diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index ed617d73c2..77f4cea0c6 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -3,7 +3,6 @@ open Util open Names open Reduction open Typeops -open Subtyping open Declarations open Environ @@ -65,17 +64,17 @@ let rec check_module env mp mb = check_signature env mb.mod_type mb.mod_mp mb.mod_delta in let optsign = match mb.mod_expr with - |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta) + |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta) |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta) |Abstract|FullStruct -> None in match optsign with |None -> () - |Some sign -> - let mtb1 = mk_mtb mp sign mb.mod_delta + |Some (sign,delta) -> + let mtb1 = mk_mtb mp sign delta and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in let env = Modops.add_module_type mp mtb1 env in - let cu = check_subtypes env mtb1 mtb2 in + let cu = Subtyping.check_subtypes env mtb1 mtb2 in if not (Environ.check_constraints cu env) then CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); @@ -103,15 +102,17 @@ and check_structure_field env mp lab res = function and check_mexpr env mse mp_mse res = match mse with | MEident mp -> let mb = lookup_module mp env in - (Modops.strengthen_and_subst_mb mb mp_mse false).mod_type + let mb = Modops.strengthen_and_subst_mb mb mp_mse false in + mb.mod_type, mb.mod_delta | MEapply (f,mp) -> - let sign = check_mexpr env f mp_mse res in + let sign, delta = check_mexpr env f mp_mse res in let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mtb = Modops.module_type_of_module (lookup_module mp env) in - let cu = check_subtypes env mtb farg_b in + let cu = Subtyping.check_subtypes env mtb farg_b in if not (Environ.check_constraints cu env) then CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping"); - Modops.subst_signature (Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver) fbody_b + let subst = Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver in + Modops.subst_signature subst fbody_b, Mod_subst.subst_codom_delta_resolver subst delta | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation") @@ -119,8 +120,8 @@ and check_mexpression env sign mp_mse res = match sign with | MoreFunctor (arg_id, mtb, body) -> check_module_type env mtb; let env' = Modops.add_module_type (MPbound arg_id) mtb env in - let body = check_mexpression env' body mp_mse res in - MoreFunctor(arg_id,mtb,body) + let body, delta = check_mexpression env' body mp_mse res in + MoreFunctor(arg_id,mtb,body), delta | NoFunctor me -> check_mexpr env me mp_mse res and check_signature env sign mp_mse res = match sign with diff --git a/checker/validate.ml b/checker/validate.ml index c214409a2c..b85944f94f 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -143,10 +143,8 @@ let validate debug v x = let o = Obj.repr x in try val_gen v mt_ec o with ValidObjError(msg,ctx,obj) -> - if debug then begin + (if debug then let ctx = List.rev_map print_frame ctx in - print_endline ("Validation failed: "^msg); print_endline ("Context: "^String.concat"/"ctx); - pr_obj obj - end; - failwith "vo structure validation failed" + pr_obj obj); + failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")") diff --git a/checker/values.ml b/checker/values.ml index e21acd8179..628089433a 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -10,28 +10,15 @@ (** Abstract representations of values in a vo *) -(** NB: UPDATE THIS FILE EACH TIME cic.mli IS MODIFIED ! +(** NB: This needs updating when the types in declarations.ml and + their dependencies are changed. *) -To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli -with a copy we maintain here: - -MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli - -*) - -(** We reify here the types of values present in a vo (see cic.mli), +(** We reify here the types of values present in a vo. in order to validate its structure. Maybe this reification could become automatically generated someday ? - - [Any] stands for a value that we won't check, - - [Fail] means a value that shouldn't be there at all, - - [Tuple] provides a name and sub-values in this block - - [Sum] provides a name, a number of constant constructors, - and sub-values at each position of each possible constructed - variant - - [List] and [Opt] could have been defined via [Sum], but - having them here helps defining some recursive values below - - [Annot] is a no-op, just there for improving debug messages *) + See values.mli for the meaning of each constructor. +*) type value = | Any @@ -45,6 +32,7 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref let fix (f : value -> value) : value = @@ -229,7 +217,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/checker/values.mli b/checker/values.mli index 1b1437a469..616b69907f 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -10,17 +10,36 @@ type value = | Any + (** A value that we won't check, *) + | Fail of string + (** A value that shouldn't be there at all, *) + | Tuple of string * value array + (** A debug name and sub-values in this block *) + | Sum of string * int * value array array + (** A debug name, a number of constant constructors, and sub-values + at each position of each possible constructed variant *) + | Array of value | List of value | Opt of value | Int | String + (** Builtin Ocaml types. *) + | Annot of string * value + (** Adds a debug note to the inner value *) + | Dyn + (** Coq's Dyn.t *) + | Proxy of value ref + (** Same as the inner value, used to define recursive types *) + +(** NB: List and Opt have their own constructors to make it easy to + define eg [let rec foo = List foo]. *) val v_univopaques : value val v_libsum : value |