diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/dune | 27 | ||||
| -rw-r--r-- | checker/include | 1 | ||||
| -rw-r--r-- | checker/validate.ml | 8 | ||||
| -rw-r--r-- | checker/values.ml | 27 | ||||
| -rw-r--r-- | checker/values.mli | 19 |
5 files changed, 30 insertions, 52 deletions
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/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 8f6b24ec26..0de8a3e03f 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 = @@ -122,8 +110,7 @@ let v_cstrs = let v_variance = v_enum "variance" 3 let v_instance = Annot ("instance", Array v_level) -let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] -let v_abs_context = v_context (* only for clarity *) +let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|] let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] 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 |