From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- checker/check.ml | 32 +-- checker/check_stat.ml | 4 +- checker/check_stat.mli | 2 +- checker/checker.ml | 138 +++++---- checker/closure.ml | 257 ++--------------- checker/closure.mli | 32 +-- checker/declarations.ml | 713 +++++++++++++++++++---------------------------- checker/declarations.mli | 48 +++- checker/environ.ml | 17 +- checker/environ.mli | 2 - checker/indtypes.ml | 19 +- checker/indtypes.mli | 4 +- checker/inductive.ml | 352 ++++++++++++----------- checker/inductive.mli | 11 +- checker/mod_checking.ml | 40 ++- checker/mod_checking.mli | 9 + checker/modops.ml | 61 ++-- checker/modops.mli | 6 +- checker/reduction.ml | 92 +++--- checker/reduction.mli | 11 +- checker/safe_typing.ml | 153 +++++++--- checker/safe_typing.mli | 21 +- checker/subtyping.ml | 57 ++-- checker/subtyping.mli | 5 +- checker/term.ml | 41 ++- checker/term.mli | 20 +- checker/type_errors.ml | 9 +- checker/type_errors.mli | 8 +- checker/typeops.ml | 43 +-- checker/typeops.mli | 4 +- checker/validate.ml | 120 ++++---- 31 files changed, 959 insertions(+), 1372 deletions(-) create mode 100644 checker/mod_checking.mli (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 40119a7e..bb42b949 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,18 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* default_root_prefix | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) -let is_in_load_paths phys_dir = - let dir = canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p = fun p -> (String.compare dir p) == 0 in - List.exists check_p lp - let remove_load_path dir = load_paths := list_filter2 (fun p d -> p <> dir) !load_paths @@ -191,13 +182,9 @@ let add_load_path (phys_path,coq_path) = load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) | _ -> anomaly ("Two logical paths are associated to "^phys_path) -let physical_paths (dp,lp) = dp - let load_paths_of_dir_path dir = fst (list_filter2 (fun p d -> d = dir) !load_paths) -let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) - (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -269,8 +256,8 @@ let try_locate_qualified_library qid = (*s Loading from disk to cache (preparation phase) *) -let (raw_extern_library, raw_intern_library) = - System.raw_extern_intern Coq_config.vo_magic_number ".vo" +let raw_intern_library = + snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo") let with_magic_number_check f a = try f a @@ -283,10 +270,10 @@ let with_magic_number_check f a = (************************************************************************) (* Internalise libraries *) -let mk_library md f digest = { +let mk_library md f table digest = { library_name = md.md_name; library_filename = f; - library_compiled = md.md_compiled; + library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled; library_deps = md.md_deps; library_digest = digest } @@ -300,20 +287,21 @@ let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = Flags.if_verbose msg (str"[intern "++str f++str" ..."); - let (md,digest) = + let (md,table,digest) = try let ch = with_magic_number_check raw_intern_library f in let (md:library_disk) = System.marshal_in ch in let digest = System.marshal_in ch in + let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in close_in ch; if dir <> md.md_name then errorlabstrm "load_physical_library" (name_clash_message dir md.md_name f); Flags.if_verbose msgnl(str" done]"); - md,digest + md,table,digest with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; - mk_library md f digest + mk_library md f table digest let get_deps (dir, f) = try LibraryMap.find dir !depgraph diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 88f2374b..5f28269e 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* if f c ce then c::acc else acc) csts [] -let is_ax _ cb = cb.const_body = None +let is_ax _ cb = not (constant_has_body cb) let pr_ax csts = let axs = cst_filter is_ax csts in diff --git a/checker/check_stat.mli b/checker/check_stat.mli index d39eb454..353edda6 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* invalid_arg "dirpath_of_string" + [] -> Check.default_root_prefix | dir -> make_dirpath (List.map id_of_string dir) let path_of_string s = match parse_dir s with - [] -> invalid_arg "dirpath_of_string" + [] -> invalid_arg "path_of_string" | l::dir -> {dirpath=dir; basename=l} let (/) = Filename.concat @@ -73,17 +72,17 @@ let convert_string d = flush_all (); failwith "caught" -let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - if exists_dir dir then - let dirs = all_subdirs dir in - let prefix = repr_dirpath coq_dirpath in +let add_rec_path ~unix_path ~coq_root = + if exists_dir unix_path then + let dirs = all_subdirs ~unix_path in + let prefix = repr_dirpath coq_root in let convert_dirs (lp,cp) = (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in List.iter Check.add_load_path dirs; - Check.add_load_path (dir,coq_dirpath) + Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str ("Cannot open " ^ unix_path)) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -92,9 +91,6 @@ let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) -let set_default_rec_include d = - let p = Check.default_root_prefix in - push_rec_include (d, p) let set_include d p = let p = dirpath_of_string p in push_include (d,p) @@ -106,24 +102,27 @@ let set_rec_include d p = let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in + let xdg_dirs = Envars.xdg_dirs in + let coqpath = Envars.coqpath in let plugins = coqlib/"plugins" in - (* first user-contrib *) - if Sys.file_exists user_contrib then - add_rec_path user_contrib Check.default_root_prefix; + (* NOTE: These directories are searched from last to first *) + (* first standard library *) + add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]); (* then plugins *) - add_rec_path plugins (Names.make_dirpath [coq_root]); - (* then standard library *) -(* List.iter - (fun (s,alias) -> - add_rec_path (coqlib/s) ([alias; coq_root])) - theories_dirs_map;*) - add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]); + (* then user-contrib *) + if Sys.file_exists user_contrib then + add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; + (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs; + (* then directories in COQPATH *) + List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) - add_path "." Check.default_root_prefix; + add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (s,alias,reci) -> - if reci then add_rec_path s alias else add_path s alias) + (fun (unix_path, coq_root, reci) -> + if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -168,43 +167,41 @@ let version () = let print_usage_channel co command = output_string co command; - output_string co "Coq options are:\n"; + output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir - -I dir map directory dir to the empty logical path - -include dir (idem) - -R dir -as coqdir recursively map physical dir to logical coqdir - -R dir coqdir (idem) - - -admit module load module and dependencies without checking - -norec module check module but admit dependencies without checking - - -where print Coq's standard library location and exit - -v print Coq version and exit - -boot boot mode - -o, --output-context print the list of assumptions - -m, --memoty print the maximum heap size - -silent disable trace of constants being checked - - -impredicative-set set sort Set impredicative - - -h, --help print this list of options -" +" -I dir -as coqdir map physical dir to logical coqdir\ +\n -I dir map directory dir to the empty logical path\ +\n -include dir (idem)\ +\n -R dir -as coqdir recursively map physical dir to logical coqdir\ +\n -R dir coqdir (idem)\ +\n\ +\n -admit module load module and dependencies without checking\ +\n -norec module check module but admit dependencies without checking\ +\n\ +\n -where print coqchk's standard library location and exit\ +\n -v print coqchk version and exit\ +\n -boot boot mode\ +\n -o, --output-context print the list of assumptions\ +\n -m, --memory print the maximum heap size\ +\n -silent disable trace of constants being checked\ +\n\ +\n -impredicative-set set sort Set impredicative\ +\n\ +\n -h, --help print this list of options\ +\n" (* print the usage on standard error *) let print_usage = print_usage_channel stderr let print_usage_coqtop () = - print_usage "Usage: coqchk \n\n" + print_usage "Usage: coqchk modules\n\n" let usage () = print_usage_coqtop (); flush stderr; exit 1 -let warning s = msg_warning (str s) - open Type_errors let anomaly_string () = str "Anomaly: " @@ -239,14 +236,9 @@ let rec explain_exn = function | Anomaly (s,pps) -> hov 1 (anomaly_string () ++ where s ++ pps ++ report ()) | Match_failure(filename,pos1,pos2) -> - hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ - if Sys.ocaml_version = "3.06" then - (str " from character " ++ int pos1 ++ - str " to " ++ int pos2) - else - (str " at line " ++ int pos1 ++ - str " character " ++ int pos2) - ++ report ()) + hov 1 (anomaly_string () ++ str "Match failure in file " ++ + str (guill filename) ++ str " at line " ++ int pos1 ++ + str " character " ++ int pos2 ++ report ()) | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) | Failure s -> @@ -274,22 +266,17 @@ let rec explain_exn = function (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) - | Stdpp.Exc_located (loc,exc) -> + | Loc.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ - (if s <> "" then - if Sys.ocaml_version = "3.06" then - (str ("(file \"" ^ s ^ "\", characters ") ++ - int b ++ str "-" ++ int e ++ str ")") - else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ - str ", characters " ++ int e ++ str "-" ++ - int (e+6) ++ str ")") - else - (mt ())) ++ + (if s = "" then mt () + else + (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + str ", characters " ++ int e ++ str "-" ++ + int (e+6) ++ str ")")) ++ report ()) | reraise -> hov 0 (anomaly_string () ++ str "Uncaught exception " ++ @@ -298,8 +285,15 @@ let rec explain_exn = function let parse_args argv = let rec parse = function | [] -> () - | "-impredicative-set" :: rem -> - set_engagement Declarations.ImpredicativeSet; parse rem + | "-impredicative-set" :: rem -> + set_engagement Declarations.ImpredicativeSet; parse rem + + | "-coqlib" :: s :: rem -> + if not (exists_dir s) then + (msgnl (str ("Directory '"^s^"' does not exist")); exit 1); + Flags.coqlib := s; + Flags.coqlib_spec := true; + parse rem | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () diff --git a/checker/closure.ml b/checker/closure.ml index da25b3b3..033e2bd7 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* red_kind val no_red : reds val red_add : reds -> red_kind -> reds - val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> transparent_state -> reds val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool - val red_get_const : reds -> bool * evaluable_global_reference list end module RedFlags = (struct @@ -114,21 +112,6 @@ module RedFlags = (struct let (l1,l2) = red.r_const in { red with r_const = Idpred.add id l1, l2 } - let red_sub red = function - | BETA -> { red with r_beta = false } - | DELTA -> { red with r_delta = false } - | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.remove kn l2 } - | IOTA -> { red with r_iota = false } - | ZETA -> { red with r_zeta = false } - | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Idpred.remove id l1, l2 } - - let red_add_transparent red tr = - { red with r_const = tr } - let mkflags = List.fold_left red_add no_red let red_set red = function @@ -146,160 +129,14 @@ module RedFlags = (struct | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta - let red_get_const red = - let p1,p2 = red.r_const in - let (b1,l1) = Idpred.elements p1 in - let (b2,l2) = Cpred.elements p2 in - if b1=b2 then - let l1' = List.map (fun x -> EvalVarRef x) l1 in - let l2' = List.map (fun x -> EvalConstRef x) l2 in - (b1, l1' @ l2') - else error "unrepresentable pair of predicate" - end : RedFlagsSig) open RedFlags let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA] let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] -let betaiota = mkflags [fBETA;fIOTA] -let beta = mkflags [fBETA] let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] -let unfold_red kn = - let flag = match kn with - | EvalVarRef id -> fVAR id - | EvalConstRef kn -> fCONST kn - in (* Remove fZETA for finer behaviour ? *) - mkflags [fBETA;flag;fIOTA;fZETA] - -(************************* Obsolète -(* [r_const=(true,cl)] means all constants but those in [cl] *) -(* [r_const=(false,cl)] means only those in [cl] *) -type reds = { - r_beta : bool; - r_const : bool * constant_path list * identifier list; - r_zeta : bool; - r_evar : bool; - r_iota : bool } - -let betadeltaiota_red = { - r_beta = true; - r_const = true,[],[]; - r_zeta = true; - r_evar = true; - r_iota = true } - -let betaiota_red = { - r_beta = true; - r_const = false,[],[]; - r_zeta = false; - r_evar = false; - r_iota = true } - -let beta_red = { - r_beta = true; - r_const = false,[],[]; - r_zeta = false; - r_evar = false; - r_iota = false } - -let no_red = { - r_beta = false; - r_const = false,[],[]; - r_zeta = false; - r_evar = false; - r_iota = false } - -let betaiotazeta_red = { - r_beta = true; - r_const = false,[],[]; - r_zeta = true; - r_evar = false; - r_iota = true } - -let unfold_red kn = - let c = match kn with - | EvalVarRef id -> false,[],[id] - | EvalConstRef kn -> false,[kn],[] - in { - r_beta = true; - r_const = c; - r_zeta = true; (* false for finer behaviour ? *) - r_evar = false; - r_iota = true } - -(* Sets of reduction kinds. - Main rule: delta implies all consts (both global (= by - kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's). - Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of - a LetIn expression is Letin reduction *) - -type red_kind = - BETA | DELTA | ZETA | IOTA - | CONST of constant_path list | CONSTBUT of constant_path list - | VAR of identifier | VARBUT of identifier - -let rec red_add red = function - | BETA -> { red with r_beta = true } - | DELTA -> - (match red.r_const with - | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags" - | _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true }) - | CONST cl -> - (match red.r_const with - | true,_,_ -> error "Conflict in the reduction flags" - | _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 }) - | CONSTBUT cl -> - (match red.r_const with - | false,_::_,_ | false,_,_::_ -> - error "Conflict in the reduction flags" - | _,l1,l2 -> - { red with r_const = true, list_union cl l1, l2; - r_zeta = true; r_evar = true }) - | IOTA -> { red with r_iota = true } - | ZETA -> { red with r_zeta = true } - | VAR id -> - (match red.r_const with - | true,_,_ -> error "Conflict in the reduction flags" - | _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 }) - | VARBUT cl -> - (match red.r_const with - | false,_::_,_ | false,_,_::_ -> - error "Conflict in the reduction flags" - | _,l1,l2 -> - { red with r_const = true, l1, list_union [cl] l2; - r_zeta = true; r_evar = true }) - -let red_delta_set red = - let b,_,_ = red.r_const in b - -let red_local_const = red_delta_set - -(* to know if a redex is allowed, only a subset of red_kind is used ... *) -let red_set red = function - | BETA -> incr_cnt red.r_beta beta - | CONST [kn] -> - let (b,l,_) = red.r_const in - let c = List.mem kn l in - incr_cnt ((b & not c) or (c & not b)) delta - | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (b,_,l) = red.r_const in - let c = List.mem id l in - incr_cnt ((b & not c) or (c & not b)) delta - | ZETA -> incr_cnt red.r_zeta zeta - | EVAR -> incr_cnt red.r_zeta evar - | IOTA -> incr_cnt red.r_iota iota - | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*) - (* Not for internal use *) - | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented" - -(* Gives the constant list *) -let red_get_const red = - let b,l1,l2 = red.r_const in - let l1' = List.map (fun x -> EvalConstRef x) l1 in - let l2' = List.map (fun x -> EvalVarRef x) l2 in - b, l1' @ l2' -fin obsolète **************) + (* specification of the reduction function *) @@ -336,8 +173,6 @@ type 'a infos = { i_vars : (identifier * constr) list; i_tab : (table_key, 'a) Hashtbl.t } -let info_flags info = info.i_flags - let ref_value_cache info ref = try Some (Hashtbl.find info.i_tab ref) @@ -447,9 +282,6 @@ and fterm = let fterm_of v = v.term let set_norm v = v.norm <- Norm -let is_val v = v.norm = Norm - -let mk_atom c = {norm=Norm;term=FAtom c} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) @@ -472,7 +304,6 @@ type stack_member = and stack = stack_member list -let empty_stack = [] let append_stack v s = if Array.length v = 0 then s else match s with @@ -486,52 +317,6 @@ let zshift n s = | (_,Zshift(k)::s) -> Zshift(n+k)::s | _ -> Zshift(n)::s -let rec stack_args_size = function - | Zapp v :: s -> Array.length v + stack_args_size s - | Zshift(_)::s -> stack_args_size s - | Zupdate(_)::s -> stack_args_size s - | _ -> 0 - -(* When used as an argument stack (only Zapp can appear) *) -let rec decomp_stack = function - | Zapp v :: s -> - (match Array.length v with - 0 -> decomp_stack s - | 1 -> Some (v.(0), s) - | _ -> - Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | _ -> None -let array_of_stack s = - let rec stackrec = function - | [] -> [] - | Zapp args :: s -> args :: (stackrec s) - | _ -> assert false - in Array.concat (stackrec s) -let rec stack_assign s p c = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then - Zapp args :: stack_assign s (p-q) c - else - (let nargs = Array.copy args in - nargs.(p) <- c; - Zapp nargs :: s) - | _ -> s -let rec stack_tail p s = - if p = 0 then s else - match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_tail (p-q) s - else Zapp (Array.sub args p (q-p)) :: s - | _ -> failwith "stack_tail" -let rec stack_nth s p = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_nth s (p-q) - else args.(p) - | _ -> raise Not_found - (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) @@ -643,7 +428,7 @@ let optimise_closure env c = let (c',(_,s)) = compact_constr (0,[]) c 1 in let env' = Array.map (fun i -> clos_rel env i) (Array.of_list s) in - (subs_cons (env', ESID 0),c') + (subs_cons (env', subs_id 0),c') let mk_lambda env t = let (env,t) = optimise_closure env t in @@ -774,7 +559,7 @@ let term_of_fconstr = | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in - term_of_fconstr_lift ELID + term_of_fconstr_lift el_id @@ -808,16 +593,6 @@ let fapp_stack (m,stk) = zip m stk (strip_update_shift_app), a fix (get_nth_arg) or an abstraction (strip_update_shift, through get_arg). *) -(* optimised for the case where there are no shifts... *) -let strip_update_shift head stk = - assert (head.norm <> Red); - let rec strip_rec h depth = function - | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s - | Zupdate(m)::s -> - strip_rec (update m (h.norm,h.term)) depth s - | stk -> (depth,stk) in - strip_rec head 0 stk - (* optimised for the case where there are no shifts... *) let strip_update_shift_app head stk = assert (head.norm <> Red); @@ -835,15 +610,15 @@ let strip_update_shift_app head stk = let get_nth_arg head n stk = assert (head.norm <> Red); - let rec strip_rec rstk h depth n = function + let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> - strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s + strip_rec (e::rstk) (lift_fconstr k h) n s | Zapp args::s' -> let q = Array.length args in if n >= q then strip_rec (Zapp args::rstk) - {norm=h.norm;term=FApp(h,args)} depth (n-q) s' + {norm=h.norm;term=FApp(h,args)} (n-q) s' else let bef = Array.sub args 0 n in let aft = Array.sub args (n+1) (q-n-1) in @@ -851,9 +626,9 @@ let get_nth_arg head n stk = List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> - strip_rec rstk (update m (h.norm,h.term)) depth n s + strip_rec rstk (update m (h.norm,h.term)) n s | s -> (None, List.rev rstk @ s) in - strip_rec [] head 0 n stk + strip_rec [] head n stk (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) @@ -876,6 +651,12 @@ let rec get_args n tys f e stk = get_args (n-na) etys f (subs_cons(l,e)) s | _ -> (Inr {norm=Cstr;term=FLambda(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 _ | Zshift _ | Zupdate _ as e) :: s -> + e :: eta_expand_stack s + | [] -> + [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]] (* Iota reduction: extract the arguments to be passed to the Case branches *) @@ -1025,7 +806,7 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (ESID 0) +let inject = mk_clos (subs_id 0) let whd_stack infos m stk = let k = kni infos m stk in diff --git a/checker/closure.mli b/checker/closure.mli index 12cee770..707a51f9 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* variable -> bool +val is_transparent_constant : transparent_state -> constant -> bool + (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -51,33 +52,20 @@ module type RedFlagsSig = sig (* Adds a reduction kind to a set *) val red_add : reds -> red_kind -> reds - (* Removes a reduction kind to a set *) - val red_sub : reds -> red_kind -> reds - - (* Adds a reduction kind to a set *) - val red_add_transparent : reds -> transparent_state -> reds - (* Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds (* Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - - (* Gives the constant list *) - val red_get_const : reds -> bool * evaluable_global_reference list end module RedFlags : RedFlagsSig open RedFlags -val beta : reds -val betaiota : reds val betadeltaiota : reds val betaiotazeta : reds val betadeltaiotanolet : reds -val unfold_red : evaluable_global_reference -> reds - (***********************************************************************) type table_key = | ConstKey of constant @@ -86,7 +74,6 @@ type table_key = type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option -val info_flags: 'a infos -> reds val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos (************************************************************************) @@ -132,23 +119,14 @@ type stack_member = and stack = stack_member list -val empty_stack : stack val append_stack : fconstr array -> stack -> stack - -val decomp_stack : stack -> (fconstr * stack) option -val array_of_stack : stack -> fconstr array -val stack_assign : stack -> int -> fconstr -> stack -val stack_args_size : stack -> int -val stack_tail : int -> stack -> stack -val stack_nth : stack -> int -> fconstr +val eta_expand_stack : stack -> stack (* 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 *) val inject : constr -> fconstr -(* mk_atom: prevents a term from being evaluated *) -val mk_atom : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr diff --git a/checker/declarations.ml b/checker/declarations.ml index 0deb80a2..890996d1 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -20,7 +20,7 @@ type polymorphic_arity = { poly_level : Univ.universe; } let val_pol_arity = - val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] + val_tuple ~name:"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|] type constant_type = | NonPolymorphicType of constr @@ -29,256 +29,164 @@ type constant_type = let val_cst_type = val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] - -type substitution_domain = - | MBI of mod_bound_id - | MPI of module_path - -let val_subst_dom = - val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|] - -module Umap = Map.Make(struct - type t = substitution_domain - let compare = Pervasives.compare - end) - +(** Substitutions, code imported from kernel/mod_subst *) type delta_hint = - Inline of constr option + | Inline of int * constr option | Equiv of kernel_name - | Prefix_equiv of module_path - -type delta_key = - KN of kernel_name - | MP of module_path -module Deltamap = Map.Make(struct - type t = delta_key - let compare = Pervasives.compare - end) -type delta_resolver = delta_hint Deltamap.t +module Deltamap = struct + type t = module_path MPmap.t * delta_hint KNmap.t + let empty = MPmap.empty, KNmap.empty + let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km) + let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km) + let remove_mp mp (mm,km) = (MPmap.remove mp mm, km) + let find_mp mp map = MPmap.find mp (fst map) + let find_kn kn map = KNmap.find kn (snd map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_kn kn map = KNmap.mem kn (snd map) + let fold_kn f map i = KNmap.fold f (snd map) i + let fold fmp fkn (mm,km) i = + MPmap.fold fmp mm (KNmap.fold fkn km i) + let join map1 map2 = fold add_mp add_kn map1 map2 +end + +type delta_resolver = Deltamap.t let empty_delta_resolver = Deltamap.empty +module MBImap = Map.Make + (struct + type t = mod_bound_id + let compare = Pervasives.compare + end) + +module Umap = struct + type 'a t = 'a MPmap.t * 'a MBImap.t + let empty = MPmap.empty, MBImap.empty + let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 + let add_mbi mbi x (m1,m2) = (m1,MBImap.add mbi x m2) + let add_mp mp x (m1,m2) = (MPmap.add mp x m1, m2) + let find_mp mp map = MPmap.find mp (fst map) + let find_mbi mbi map = MBImap.find mbi (snd map) + let mem_mp mp map = MPmap.mem mp (fst map) + let mem_mbi mbi map = MBImap.mem mbi (snd map) + let iter_mbi f map = MBImap.iter f (snd map) + let fold fmp fmbi (m1,m2) i = + MPmap.fold fmp m1 (MBImap.fold fmbi m2 i) + let join map1 map2 = fold add_mp add_mbi map1 map2 +end + type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res_dom = - val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|] +let empty_subst = Umap.empty -let val_res = - val_map ~name:"delta_resolver" - val_res_dom - (val_sum "delta_hint" 0 [|[|val_opt val_constr|];[|val_kn|];[|val_mp|]|]) +let is_empty_subst = Umap.is_empty -let val_subst = - val_map ~name:"substitution" - val_subst_dom (val_tuple "substition range" [|val_mp;val_res|]) +let val_delta_hint = + val_sum "delta_hint" 0 + [|[|val_int; val_opt val_constr|];[|val_kn|]|] +let val_res = + val_tuple ~name:"delta_resolver" + [|val_map ~name:"delta_resolver" val_mp val_mp; + val_map ~name:"delta_resolver" val_kn val_delta_hint|] -let fold_subst fb fp = - Umap.fold - (fun k (mp,_) acc -> - match k with - | MBI mbid -> fb mbid mp acc - | MPI mp1 -> fp mp1 mp acc) +let val_mp_res = val_tuple [|val_mp;val_res|] -let empty_subst = Umap.empty +let val_subst = + val_tuple ~name:"substitution" + [|val_map ~name:"substitution" val_mp val_mp_res; + val_map ~name:"substitution" val_uid val_mp_res|] -let add_mbid mbid mp = - Umap.add (MBI mbid) (mp,empty_delta_resolver) -let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,empty_delta_resolver) +let add_mbid mbid mp = Umap.add_mbi mbid (mp,empty_delta_resolver) +let add_mp mp1 mp2 = Umap.add_mp mp1 (mp2,empty_delta_resolver) let map_mbid mbid mp = add_mbid mbid mp empty_subst let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst -let add_inline_delta_resolver con = - Deltamap.add (KN(user_con con)) (Inline None) - -let add_inline_constr_delta_resolver con cstr = - Deltamap.add (KN(user_con con)) (Inline (Some cstr)) - -let add_constant_delta_resolver con = - Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) - -let add_mind_delta_resolver mind = - Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) - -let add_mp_delta_resolver mp1 mp2 = - Deltamap.add (MP mp1) (Prefix_equiv mp2) - -let mp_in_delta mp = - Deltamap.mem (MP mp) - -let con_in_delta con resolver = -try - match Deltamap.find (KN(user_con con)) resolver with - | Inline _ | Prefix_equiv _ -> false - | Equiv _ -> true -with - Not_found -> false - -let mind_in_delta mind resolver = -try - match Deltamap.find (KN(user_mind mind)) resolver with - | Inline _ | Prefix_equiv _ -> false - | Equiv _ -> true -with - Not_found -> false - -let delta_of_mp resolve mp = - try - match Deltamap.find (MP mp) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly "mod_subst: bad association in delta_resolver" - with - Not_found -> mp - -let delta_of_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> kn - -let remove_mp_delta_resolver resolver mp = - Deltamap.remove (MP mp) resolver - -exception Inline_kn +let mp_in_delta mp = + Deltamap.mem_mp mp -let rec find_prefix resolve mp = +let rec find_prefix resolve mp = let rec sub_mp = function - | MPdot(mp,l) as mp_sup -> - (try - match Deltamap.find (MP mp_sup) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found -> MPdot(sub_mp mp,l)) - | p -> - match Deltamap.find (MP p) resolve with - | Prefix_equiv mp1 -> mp1 - | _ -> anomaly - "mod_subst: bad association in delta_resolver" + | MPdot(mp,l) as mp_sup -> + (try Deltamap.find_mp mp_sup resolve + with Not_found -> MPdot(sub_mp mp,l)) + | p -> Deltamap.find_mp p resolve in - try - sub_mp mp - with - Not_found -> mp - + try sub_mp mp with Not_found -> mp + +(** Nota: the following function is slightly different in mod_subst + PL: Is it on purpose ? *) + let solve_delta_kn resolve kn = - try - match Deltamap.find (KN kn) resolve with - | Equiv kn1 -> kn1 - | Inline _ -> raise Inline_kn - | _ -> anomaly - "mod_subst: bad association in delta_resolver" - with - Not_found | Inline_kn -> - let mp,dir,l = repr_kn kn in - let new_mp = find_prefix resolve mp in - if mp == new_mp then - kn - else - make_kn new_mp dir l - + try + match Deltamap.find_kn kn resolve with + | Equiv kn1 -> kn1 + | Inline _ -> raise Not_found + with Not_found -> + let mp,dir,l = repr_kn kn in + let new_mp = find_prefix resolve mp in + if mp == new_mp then + kn + else + make_kn new_mp dir l + +let gen_of_delta resolve x kn fix_can = + try + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then x else fix_can new_kn + with _ -> x let constant_of_delta resolve con = let kn = user_con con in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn new_kn - + gen_of_delta resolve con kn (constant_of_kn_equiv kn) + let constant_of_delta2 resolve con = - let kn = canonical_con con in - let kn1 = user_con con in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - con - else - constant_of_kn_equiv kn1 new_kn + let kn, kn' = canonical_con con, user_con con in + gen_of_delta resolve con kn (constant_of_kn_equiv kn') let mind_of_delta resolve mind = let kn = user_mind mind in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn new_kn - -let mind_of_delta2 resolve mind = - let kn = canonical_mind mind in - let kn1 = user_mind mind in - let new_kn = solve_delta_kn resolve kn in - if kn == new_kn then - mind - else - mind_of_kn_equiv kn1 new_kn - + gen_of_delta resolve mind kn (mind_of_kn_equiv kn) +let mind_of_delta2 resolve mind = + let kn, kn' = canonical_mind mind, user_mind mind in + gen_of_delta resolve mind kn (mind_of_kn_equiv kn') -let inline_of_delta resolver = - let extract key hint l = - match key,hint with - |KN kn, Inline _ -> kn::l - | _,_ -> l - in - Deltamap.fold extract resolver [] +let find_inline_of_delta kn resolve = + match Deltamap.find_kn kn resolve with + | Inline (_,o) -> o + | _ -> raise Not_found -exception Not_inline - let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in - try - match Deltamap.find (KN kn2) resolve with - | Inline None -> None - | Inline (Some const) -> Some const - | _ -> raise Not_inline - with - Not_found | Not_inline -> - try match Deltamap.find (KN kn1) resolve with - | Inline None -> None - | Inline (Some const) -> Some const - | _ -> raise Not_inline - with - Not_found | Not_inline -> None + try find_inline_of_delta kn2 resolve + with Not_found -> + try find_inline_of_delta kn1 resolve + with Not_found -> None let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPfile sid -> - let mp',resolve = Umap.find (MPI (MPfile sid)) sub in - mp',resolve + | MPfile sid -> Umap.find_mp mp sub | MPbound bid -> begin - try - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve - with Not_found -> - let mp',resolve = Umap.find (MPI mp) sub in - mp',resolve + try Umap.find_mbi bid sub + with Not_found -> Umap.find_mp mp sub end | MPdot (mp1,l) as mp2 -> begin - try - let mp',resolve = Umap.find (MPI mp2) sub in - mp',resolve + try Umap.find_mp mp2 sub with Not_found -> let mp1',resolve = aux mp1 in - MPdot (mp1',l),resolve + MPdot (mp1',l),resolve end in - try - Some (aux mp) - with Not_found -> None + try Some (aux mp) with Not_found -> None let subst_mp sub mp = match subst_mp0 sub mp with @@ -305,127 +213,58 @@ type sideconstantsubst = | User | Canonical + +let gen_subst_mp f sub mp1 mp2 = + match subst_mp0 sub mp1, subst_mp0 sub mp2 with + | None, None -> raise No_subst + | Some (mp',resolve), None -> User, (f mp' mp2), resolve + | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve + | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 + let subst_ind sub mind = - let kn1,kn2 = user_mind mind,canonical_mind mind in + let kn1,kn2 = user_mind mind, canonical_mind mind in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in - try - let side,mind',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_mind_equiv mp1' mp2' dir l), resolve2 - in - match side with - |User -> - let mind = mind_of_delta resolve mind' in - mind - |Canonical -> - let mind = mind_of_delta2 resolve mind' in - mind - with - No_subst -> mind - -let subst_mind0 sub mind = - let kn1,kn2 = user_mind mind,canonical_mind mind in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in - try - let side,mind',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_mind_equiv mp1' mp2' dir l), resolve2 - in - match side with - |User -> - let mind = mind_of_delta resolve mind' in - Some mind - |Canonical -> - let mind = mind_of_delta2 resolve mind' in - Some mind - with - No_subst -> Some mind - -let subst_con sub con = - let kn1,kn2 = user_con con,canonical_con con in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in - try - let side,con',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_con_equiv mp1' mp2' dir l), resolve2 - in - match constant_of_delta_with_inline resolve con' with - None -> begin - match side with - |User -> - let con = constant_of_delta resolve con' in - con,Const con - |Canonical -> - let con = constant_of_delta2 resolve con' in - con,Const con - end - | Some t -> con',t - with No_subst -> con , Const con - + let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in + try + let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in + match side with + | User -> mind_of_delta resolve mind' + | Canonical -> mind_of_delta2 resolve mind' + with No_subst -> mind let subst_con0 sub con = let kn1,kn2 = user_con con,canonical_con con in let mp1,dir,l = repr_kn kn1 in let mp2,_,_ = repr_kn kn2 in - try - let side,con',resolve = - match subst_mp0 sub mp1,subst_mp0 sub mp2 with - None,None ->raise No_subst - | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve - | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve - | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, - (make_con_equiv mp1' mp2' dir l), resolve2 + let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in + let dup con = con, Const con in + let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in + match constant_of_delta_with_inline resolve con' with + | Some t -> con', t + | None -> + let con'' = match side with + | User -> constant_of_delta resolve con' + | Canonical -> constant_of_delta2 resolve con' in - match constant_of_delta_with_inline resolve con' with - None ->begin - match side with - |User -> - let con = constant_of_delta resolve con' in - Some (Const con) - |Canonical -> - let con = constant_of_delta2 resolve con' in - Some (Const con) - end - | t -> t - with No_subst -> Some (Const con) - + if con'' == con then raise No_subst else dup con'' let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> - (match f' kn with - None -> c - | Some const ->const) + | Const kn -> (try snd (f' kn) with No_subst -> c) | Ind (kn,i) -> - (match f kn with - None -> c - | Some kn' -> - Ind (kn',i)) + let kn' = f kn in + if kn'==kn then c else Ind (kn',i) | Construct ((kn,i),j) -> - (match f kn with - None -> c - | Some kn' -> - Construct ((kn',i),j)) + let kn' = f kn in + if kn'==kn then c else Construct ((kn',i),j) | Case (ci,p,ct,l) -> let ci_ind = let (kn,i) = ci.ci_ind in - (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in + let kn' = f kn in + if kn'==kn then ci.ci_ind else kn',i + in let p' = func p in let ct' = func ct in let l' = array_smartmap func l in @@ -476,8 +315,9 @@ let rec map_kn f f' c = else CoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_mind0 sub) (subst_con0 sub) +let subst_mps sub c = + if is_empty_subst sub then c + else map_kn (subst_ind sub) (subst_con0 sub) c type 'a lazy_subst = @@ -507,125 +347,113 @@ let rec mp_in_mp mp mp1 = | _ when mp1 = mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false - -let mp_in_key mp key = - match key with - | MP mp1 -> - mp_in_mp mp mp1 - | KN kn -> - let mp1,dir,l = repr_kn kn in - mp_in_mp mp mp1 - + let subset_prefixed_by mp resolver = - let prefixmp key hint resolv = - if mp_in_key mp key then - Deltamap.add key hint resolv - else - resolv + let mp_prefix mkey mequ rslv = + if mp_in_mp mp mkey then Deltamap.add_mp mkey mequ rslv else rslv + in + let kn_prefix kn hint rslv = + match hint with + | Inline _ -> rslv + | Equiv _ -> + if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv in - Deltamap.fold prefixmp resolver empty_delta_resolver + Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver let subst_dom_delta_resolver subst resolver = - let apply_subst key hint resolver = - match key with - (MP mp) -> - Deltamap.add (MP (subst_mp subst mp)) hint resolver - | (KN kn) -> - Deltamap.add (KN (subst_kn subst kn)) hint resolver + let mp_apply_subst mkey mequ rslv = + Deltamap.add_mp (subst_mp subst mkey) mequ rslv in - Deltamap.fold apply_subst resolver empty_delta_resolver + let kn_apply_subst kkey hint rslv = + Deltamap.add_kn (subst_kn subst kkey) hint rslv + in + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver -let subst_mp_delta sub mp key= +let subst_mp_delta sub mp mkey = match subst_mp0 sub mp with None -> empty_delta_resolver,mp - | Some (mp',resolve) -> + | Some (mp',resolve) -> let mp1 = find_prefix resolve mp' in let resolve1 = subset_prefixed_by mp1 resolve in - match key with - MP mpk -> - (subst_dom_delta_resolver - (map_mp mp1 mpk) resolve1),mp1 - | _ -> anomaly "Mod_subst: Bad association in resolver" - -let subst_codom_delta_resolver subst resolver = - let apply_subst key hint resolver = - match hint with - Prefix_equiv mp -> - let derived_resolve,mpnew = subst_mp_delta subst mp key in - Deltamap.fold Deltamap.add derived_resolve - (Deltamap.add key (Prefix_equiv mpnew) resolver) - | (Equiv kn) -> - Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver - | Inline None -> - Deltamap.add key hint resolver - | Inline (Some t) -> - Deltamap.add key (Inline (Some (subst_mps subst t))) resolver + (subst_dom_delta_resolver + (map_mp mp1 mkey) resolve1),mp1 + +let gen_subst_delta_resolver dom subst resolver = + let mp_apply_subst mkey mequ rslv = + let mkey' = if dom then subst_mp subst mkey else mkey in + let rslv',mequ' = subst_mp_delta subst mequ mkey in + Deltamap.join rslv' (Deltamap.add_mp mkey' mequ' rslv) in - Deltamap.fold apply_subst resolver empty_delta_resolver + let kn_apply_subst kkey hint rslv = + let kkey' = if dom then subst_kn subst kkey else kkey in + let hint' = match hint with + | Equiv kequ -> Equiv (subst_kn_delta subst kequ) + | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t)) + | Inline (_,None) -> hint + in + Deltamap.add_kn kkey' hint' rslv + in + Deltamap.fold mp_apply_subst kn_apply_subst resolver empty_delta_resolver + +let subst_codom_delta_resolver = gen_subst_delta_resolver false +let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true -let subst_dom_codom_delta_resolver subst resolver = - subst_dom_delta_resolver subst - (subst_codom_delta_resolver subst resolver) - let update_delta_resolver resolver1 resolver2 = - let apply_res key hint res = - try - match hint with - Prefix_equiv mp -> - let new_hint = - Prefix_equiv (find_prefix resolver2 mp) - in Deltamap.add key new_hint res - | Equiv kn -> - let new_hint = - Equiv (solve_delta_kn resolver2 kn) - in Deltamap.add key new_hint res - | _ -> Deltamap.add key hint res - with Not_found -> - Deltamap.add key hint res - in - Deltamap.fold apply_res resolver1 empty_delta_resolver + let mp_apply_rslv mkey mequ rslv = + if Deltamap.mem_mp mkey resolver2 then rslv + else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv + in + let kn_apply_rslv kkey hint rslv = + if Deltamap.mem_kn kkey resolver2 then rslv + else + let hint' = match hint with + | Equiv kequ -> Equiv (solve_delta_kn resolver2 kequ) + | _ -> hint + in + Deltamap.add_kn kkey hint' rslv + in + Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver let add_delta_resolver resolver1 resolver2 = if resolver1 == resolver2 then resolver2 + else if resolver2 = empty_delta_resolver then + resolver1 else - Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) - resolver2 + Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2 let substition_prefixed_by k mp subst = - let prefixmp key (mp_to,reso) sub = - match key with - | MPI mpk -> - if mp_in_mp mp mpk && mp <> mpk then - let new_key = replace_mp_in_mp mp k mpk in - Umap.add (MPI new_key) (mp_to,reso) sub - else - sub - | _ -> sub + let mp_prefixmp kmp (mp_to,reso) sub = + if mp_in_mp mp kmp && mp <> kmp then + let new_key = replace_mp_in_mp mp k kmp in + Umap.add_mp new_key (mp_to,reso) sub + else sub + in + let mbi_prefixmp mbi _ sub = sub in - Umap.fold prefixmp subst empty_subst + Umap.fold mp_prefixmp mbi_prefixmp subst empty_subst -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst key (mp,resolve) res = +let join subst1 subst2 = + let apply_subst mpk add (mp,resolve) res = let mp',resolve' = match subst_mp0 subst2 mp with - None -> mp, None - | Some (mp',resolve') -> mp' - ,Some resolve' in - let resolve'' : delta_resolver = + | None -> mp, None + | Some (mp',resolve') -> mp', Some resolve' in + let resolve'' = match resolve' with - Some res -> - add_delta_resolver + | Some res -> + add_delta_resolver (subst_dom_codom_delta_resolver subst2 resolve) res - | None -> + | None -> subst_codom_delta_resolver subst2 resolve in - let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in - let prefixed_subst = substition_prefixed_by k mp subst2 in - Umap.fold Umap.add prefixed_subst - (Umap.add key (mp',resolve'') res) in - let subst = Umap.fold apply_subst subst1 empty_subst in - (Umap.fold Umap.add subst2 subst) + let prefixed_subst = substition_prefixed_by mpk mp' subst2 in + Umap.join prefixed_subst (add (mp',resolve'') res) + in + let mp_apply_subst mp = apply_subst mp (Umap.add_mp mp) in + let mbi_apply_subst mbi = apply_subst (MPbound mbi) (Umap.add_mbi mbi) in + let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in + Umap.join subst2 subst let force fsubst r = match !r with @@ -650,25 +478,67 @@ let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted +(** Beware! In .vo files, lazy_constr are stored as integers + used as indexes for a separate table. The actual lazy_constr is restored + later, by [Safe_typing.LightenLibrary.load]. This allows us + to use here a different definition of lazy_constr than coqtop: + since the checker will inspect all proofs parts, even opaque + ones, no need to use Lazy.t here *) + +type lazy_constr = constr_substituted +let subst_lazy_constr = subst_substituted +let force_lazy_constr = force_constr +let lazy_constr_from_val c = c +let val_lazy_constr = val_cstr_subst + +(** Inlining level of parameters at functor applications. + This is ignored by the checker. *) + +type inline = int option + +(** A constant can have no body (axiom/parameter), or a + transparent body, or an opaque one *) + +type constant_def = + | Undef of inline + | Def of constr_substituted + | OpaqueDef of lazy_constr + +let val_cst_def = + val_sum "constant_def" 0 + [|[|val_opt val_int|]; [|val_cstr_subst|]; [|val_lazy_constr|]|] + +let subst_constant_def sub = function + | Undef inl -> Undef inl + | Def c -> Def (subst_constr_subst sub c) + | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr_substituted option; + const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - (* const_type_code : Cemitcodes.to_patch; *) - const_constraints : Univ.constraints; - const_opaque : bool; - const_inline : bool} + const_constraints : Univ.constraints } -let val_cb = val_tuple "constant_body" +let body_of_constant cb = match cb.const_body with + | Undef _ -> None + | Def c -> Some c + | OpaqueDef c -> Some c + +let constant_has_body cb = match cb.const_body with + | Undef _ -> false + | Def _ | OpaqueDef _ -> true + +let is_opaque cb = match cb.const_body with + | OpaqueDef _ -> true + | Def _ | Undef _ -> false + +let val_cb = val_tuple ~name:"constant_body" [|val_nctxt; - val_opt val_cstr_subst; + val_cst_def; val_cst_type; no_val; - val_cstrs; - val_bool; - val_bool |] - + val_cstrs|] let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in @@ -679,14 +549,14 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) type recarg = | Norec - | Mrec of int + | Mrec of inductive | Imbr of inductive let val_recarg = val_sum "recarg" 1 (* Norec *) - [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|] + [|[|val_ind|] (* Mrec *);[|val_ind|] (* Imbr *)|] let subst_recarg sub r = match r with - | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_ind sub kn in + | Norec -> r + | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -724,7 +594,7 @@ type monomorphic_inductive_arity = { mind_sort : sorts; } let val_mono_ind_arity = - val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|] + val_tuple ~name:"monomorphic_inductive_arity"[|val_constr;val_sort|] type inductive_arity = | Monomorphic of monomorphic_inductive_arity @@ -784,7 +654,7 @@ type one_inductive_body = { mind_reloc_tbl : reloc_table; } -let val_one_ind = val_tuple "one_inductive_body" +let val_one_ind = val_tuple ~name:"one_inductive_body" [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr; val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int; val_wfp;val_int;val_int;no_val|] @@ -820,7 +690,7 @@ type mutual_inductive_body = { mind_constraints : Univ.constraints; } -let val_ind_pack = val_tuple "mutual_inductive_body" +let val_ind_pack = val_tuple ~name:"mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; val_int; val_int; val_rctxt;val_cstrs|] @@ -832,13 +702,10 @@ let subst_arity sub = function (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); - const_body = Option.map (subst_constr_subst sub) cb.const_body; + const_body = subst_constant_def sub cb.const_body; const_type = subst_arity sub cb.const_type; const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code; - (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) - const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque; - const_inline = cb.const_inline} + const_constraints = cb.const_constraints} let subst_arity sub = function | Monomorphic s -> @@ -923,7 +790,7 @@ let rec val_sfb o = val_sum "struct_field_body" 0 [|val_module|]; (* SFBmodule *) [|val_modtype|] (* SFBmodtype *) |] o -and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o +and val_sb o = val_list (val_tuple ~name:"label*sfb"[|val_id;val_sfb|]) o and val_seb o = val_sum "struct_expr_body" 0 [|[|val_mp|]; (* SEBident *) [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) @@ -934,10 +801,10 @@ and val_seb o = val_sum "struct_expr_body" 0 and val_with o = val_sum "with_declaration_body" 0 [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o -and val_module o = val_tuple "module_body" +and val_module o = val_tuple ~name:"module_body" [|val_mp;val_opt val_seb;val_seb; val_opt val_seb;val_cstrs;val_res;no_val|] o -and val_modtype o = val_tuple "module_type_body" +and val_modtype o = val_tuple ~name:"module_type_body" [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o diff --git a/checker/declarations.mli b/checker/declarations.mli index b39fd6f2..90beb326 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -29,26 +29,53 @@ type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted +(** Beware! In .vo files, lazy_constr are stored as integers + used as indexes for a separate table. The actual lazy_constr is restored + later, by [Safe_typing.LightenLibrary.load]. This allows us + to use here a different definition of lazy_constr than coqtop: + since the checker will inspect all proofs parts, even opaque + ones, no need to use Lazy.t here *) + +type lazy_constr +val force_lazy_constr : lazy_constr -> constr +val lazy_constr_from_val : constr_substituted -> lazy_constr + +(** Inlining level of parameters at functor applications. + This is ignored by the checker. *) + +type inline = int option + +(** A constant can have no body (axiom/parameter), or a + transparent body, or an opaque one *) + +type constant_def = + | Undef of inline + | Def of constr_substituted + | OpaqueDef of lazy_constr + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) - const_body : constr_substituted option; + const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : Univ.constraints; - const_opaque : bool; - const_inline : bool} + const_constraints : Univ.constraints } + +val body_of_constant : constant_body -> constr_substituted option +val constant_has_body : constant_body -> bool +val is_opaque : constant_body -> bool (* Mutual inductives *) type recarg = | Norec - | Mrec of int + | Mrec of inductive | Imbr of inductive type wf_paths = recarg Rtree.t val mk_norec : wf_paths val mk_paths : recarg -> wf_paths list array -> wf_paths +val dest_recarg : wf_paths -> recarg val dest_subterms : wf_paths -> wf_paths list array type monomorphic_inductive_arity = { @@ -186,11 +213,6 @@ and module_type_body = (* Substitutions *) -val fold_subst : - (mod_bound_id -> module_path -> 'a -> 'a) -> - (module_path -> module_path -> 'a -> 'a) -> - substitution -> 'a -> 'a - type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution @@ -211,6 +233,6 @@ val subst_module : substitution -> module_body -> module_body val join : substitution -> substitution -> substitution (* Validation *) -val val_eng : Obj.t -> unit -val val_module : Obj.t -> unit -val val_modtype : Obj.t -> unit +val val_eng : Validate.func +val val_module : Validate.func +val val_modtype : Validate.func diff --git a/checker/environ.ml b/checker/environ.ml index f7dd46f8..99b36457 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -98,7 +98,7 @@ let named_type id env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then + if c == empty_constraint then env else let s = env.env_stratification in @@ -121,25 +121,16 @@ let add_constant kn cs env = env_constants = new_constants } in { env with env_globals = new_globals } -(* constant_type gives the type of a constant *) -let constant_type env kn = - let cb = lookup_constant kn env in - cb.const_type - type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result let constant_value env kn = let cb = lookup_constant kn env in - if cb.const_opaque then raise (NotEvaluableConst Opaque); match cb.const_body with - | Some l_body -> force_constr l_body - | None -> raise (NotEvaluableConst NoBody) - -let constant_opt_value env cst = - try Some (constant_value env cst) - with NotEvaluableConst _ -> None + | Def l_body -> force_constr l_body + | 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 ea446cdb..628febbb 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -50,11 +50,9 @@ val add_constraints : Univ.constraints -> env -> env (* Constants *) val lookup_constant : constant -> env -> Declarations.constant_body val add_constant : constant -> Declarations.constant_body -> env -> env -val constant_type : env -> constant -> Declarations.constant_type type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant -> constr -val constant_opt_value : env -> constant -> constr option val evaluable_constant : constant -> env -> bool (* Inductives *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 277fed30..1e773df6 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let u' = fresh_local_univ () in let cst = - merge_constraints (enforce_geq u' u Constraint.empty) + merge_constraints (enforce_geq u' u empty_constraint) (universes env) in if not (check_geq cst u' level) then failwith "impredicative Type inductive type" @@ -394,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = +let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc = let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) let rec check_pos (env, n, ntypes, ra_env as ienv) c = @@ -496,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = with IllFormedInd err -> explain_ind_err (ntypes-i) env lparams c err) indlc - in mk_paths (Mrec i) irecargs + in mk_paths (Mrec ind) irecargs let check_subtree (t1:'a) (t2:'a) = if not (Rtree.compare_rtree (fun t1 t2 -> @@ -507,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) = failwith "bad recursive trees" (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) -let check_positivity env_ar params nrecp inds = +let check_positivity env_ar mind params nrecp inds = let ntypes = Array.length inds in - let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in + let rc = + Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = List.rev (Array.to_list rc) in let lparams = rel_context_length params in let check_one i mip = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - check_positivity_one ienv params nrecp i mip.mind_nf_lc + check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in @@ -549,7 +548,7 @@ let check_inductive env kn mib = (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; (* check mind_nparams_rec: positivity condition *) - check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; + check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) (* Now we can add the inductive *) add_mind kn mib env diff --git a/checker/indtypes.mli b/checker/indtypes.mli index bca0a643..4c2b078c 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] then fail(); substl subs ty -let instantiate_partial_params = instantiate_params false - let full_inductive_instantiate mib params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in @@ -100,10 +96,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = (* Functions to build standard types related to inductive *) - -let number_of_inductives mib = Array.length mib.mind_packets -let number_of_constructors mip = Array.length mip.mind_consnames - (* Computing the actual sort of an applied or partially applied inductive type: @@ -346,14 +338,14 @@ let type_case_branches env (ind,largs) (p,pj) c = (************************************************************************) -(* Checking the case annotation is relevent *) +(* Checking the case annotation is relevant *) let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or - (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) + (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) (************************************************************************) @@ -404,8 +396,10 @@ type subterm_spec = | Dead_code | Not_subterm -let spec_of_tree t = - if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t) +let spec_of_tree t = lazy + (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec + then Not_subterm + else Subterm(Strict,Lazy.force t)) let subterm_spec_glb = let glb2 s1 s2 = @@ -440,7 +434,7 @@ let make_renv env minds recarg (kn,tyi) = rel_min = recarg+2; inds = minds; recvec = mind_recvec; - genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] } + genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] } let push_var renv (x,ty,spec) = { renv with @@ -459,10 +453,6 @@ let subterm_var p renv = try Lazy.force (List.nth renv.genv (p-1)) with Failure _ | Invalid_argument _ -> Not_subterm -(* Add a variable and mark it as strictly smaller with information [spec]. *) -let add_subterm renv (x,a,spec) = - push_var renv (x,a,lazy (spec_of_tree (Lazy.force spec))) - let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { renv with @@ -478,6 +468,15 @@ let push_fix_renv renv (_,v,_ as recdef) = genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } +(* Definition and manipulation of the stack *) +type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t + +let push_stack_closures renv l stack = + List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack + +let push_stack_args l stack = + List.fold_right (fun h b -> (SArg h)::b) l stack + (******************************) (* Computing the recursive subterms of a term (propagation of size information through Cases). *) @@ -497,60 +496,38 @@ let lookup_subterms env ind = let (_,mip) = lookup_mind_specif env ind in mip.mind_recargs -(*********************************) - -let match_trees t1 t2 = - let v1 = dest_subterms t1 in - let v2 = dest_subterms t2 in - array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2 +let match_inductive ind ra = + match ra with + | (Mrec i | Imbr i) -> eq_ind ind i + | Norec -> false -(* In {match c as z in ind y_s return P with |C_i x_s => t end} - [branches_specif renv c_spec ind] returns an array of x_s specs given - c_spec the spec of c. *) -let branches_specif renv c_spec ind = - let (_,mip) = lookup_mind_specif renv.env ind in +(* In {match c as z in ci y_s return P with |C_i x_s => t end} + [branches_specif renv c_spec ci] returns an array of x_s specs knowing + c_spec. *) +let branches_specif renv c_spec ci = let car = (* We fetch the regular tree associated to the inductive of the match. This is just to get the number of constructors (and constructor arities) that fit the match branches without forcing c_spec. Note that c_spec might be more precise than [v] below, because of nested inductive types. *) + let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in let v = dest_subterms mip.mind_recargs in Array.map List.length v in Array.mapi (fun i nca -> (* i+1-th cstructor has arity nca *) let lvra = lazy (match Lazy.force c_spec with - Subterm (_,t) when match_trees mip.mind_recargs t -> + Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) -> let vra = Array.of_list (dest_subterms t).(i) in assert (nca = Array.length vra); - Array.map spec_of_tree vra + Array.map + (fun t -> Lazy.force (spec_of_tree (lazy t))) + vra | Dead_code -> Array.create nca Dead_code | _ -> Array.create nca Not_subterm) in list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca) - car - -(* Propagation of size information through Cases: if the matched - object is a recursive subterm then compute the information - associated to its own subterms. - Rq: if branch is not eta-long, then the recursive information - is not propagated to the missing abstractions *) -let case_branches_specif renv c_spec ind lbr = - let vlrec = branches_specif renv c_spec ind in - let rec push_branch_args renv lrec c = - match lrec with - ra::lr -> - let c' = whd_betadeltaiota renv.env c in - (match c' with - Lambda(x,a,b) -> - let renv' = push_var renv (x,a,ra) in - push_branch_args renv' lr b - | _ -> (* branch not in eta-long form: cannot perform rec. calls *) - (renv,c')) - | [] -> (renv, c) in - assert (Array.length vlrec = Array.length lbr); - array_map2 (push_branch_args renv) vlrec lbr - + car (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of @@ -558,78 +535,88 @@ let case_branches_specif renv c_spec ind lbr = about variables. *) -let rec subterm_specif renv t = + +let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_betadeltaiota renv.env t) in - match f with - | Rel k -> subterm_var k renv - - | Case (ci,_,c,lbr) -> - let lbr_spec = case_subterm_specif renv ci c lbr in - let stl = - Array.map (fun (renv',br') -> subterm_specif renv' br') - lbr_spec in - subterm_spec_glb stl - - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> -(* when proving that the fixpoint f(x)=e is less than n, it is enough - to prove that e is less than n assuming f is less than n - furthermore when f is applied to a term which is strictly less than - n, one may assume that x itself is strictly less than n -*) - let (ctxt,clfix) = dest_prod renv.env typarray.(i) in - let oind = - let env' = push_rel_context ctxt renv.env in - try Some(fst(find_inductive env' clfix)) - with Not_found -> None in - (match oind with - None -> Not_subterm (* happens if fix is polymorphic *) - | Some ind -> - let nbfix = Array.length typarray in - let recargs = lookup_subterms renv.env ind in - (* pushing the fixpoints *) - let renv' = push_fix_renv renv recdef in - let renv' = - (* Why Strict here ? To be general, it could also be - Large... *) - assign_var_spec renv' - (nbfix-i, Lazy.lazy_from_val (Subterm(Strict,recargs))) in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in - (* pushing the fix parameters *) - let renv'' = push_ctxt_renv renv' sign in - let renv'' = - if List.length l < nbOfAbst then renv'' - else - let theDecrArg = List.nth l decrArg in - let arg_spec = lazy_subterm_specif renv theDecrArg in - assign_var_spec renv'' (1, arg_spec) in - subterm_specif renv'' strippedBody) - - | Lambda (x,a,b) -> - assert (l=[]); - subterm_specif (push_var_renv renv (x,a)) b - - (* Metas and evars are considered OK *) - | (Meta _|Evar _) -> Dead_code - - (* Other terms are not subterms *) - | _ -> Not_subterm - -and lazy_subterm_specif renv t = - lazy (subterm_specif renv t) - -and case_subterm_specif renv ci c lbr = - if Array.length lbr = 0 then [||] - else - let c_spec = lazy_subterm_specif renv c in - case_branches_specif renv c_spec ci.ci_ind lbr - -(* Check term c can be applied to one of the mutual fixpoints. *) -let check_is_subterm renv c = - match subterm_specif renv c with + match f with + | Rel k -> subterm_var k renv + + | Case (ci,_,c,lbr) -> + let stack' = push_stack_closures renv l stack in + let cases_spec = branches_specif renv + (lazy_subterm_specif renv [] c) ci in + let stl = + Array.mapi (fun i br' -> + let stack_br = push_stack_args (cases_spec.(i)) stack' in + subterm_specif renv stack_br br') + lbr in + subterm_spec_glb stl + + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + (* when proving that the fixpoint f(x)=e is less than n, it is enough + to prove that e is less than n assuming f is less than n + furthermore when f is applied to a term which is strictly less than + n, one may assume that x itself is strictly less than n + *) + let (ctxt,clfix) = dest_prod renv.env typarray.(i) in + let oind = + let env' = push_rel_context ctxt renv.env in + try Some(fst(find_inductive env' clfix)) + with Not_found -> None in + (match oind with + None -> Not_subterm (* happens if fix is polymorphic *) + | Some ind -> + let nbfix = Array.length typarray in + let recargs = lookup_subterms renv.env ind in + (* pushing the fixpoints *) + let renv' = push_fix_renv renv recdef in + let renv' = + (* Why Strict here ? To be general, it could also be + Large... *) + assign_var_spec renv' + (nbfix-i, lazy (Subterm(Strict,recargs))) in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let stack' = push_stack_closures renv l stack in + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + if List.length stack' < nbOfAbst then renv'' + else + let decrArg = List.nth stack' decrArg in + let arg_spec = stack_element_specif decrArg in + assign_var_spec renv'' (1, arg_spec) in + subterm_specif renv'' [] strippedBody) + + | Lambda (x,a,b) -> + assert (l=[]); + let spec,stack' = extract_stack renv a stack in + subterm_specif (push_var renv (x,a,spec)) stack' b + + (* Metas and evars are considered OK *) + | (Meta _|Evar _) -> Dead_code + + (* Other terms are not subterms *) + | _ -> Not_subterm + +and lazy_subterm_specif renv stack t = + lazy (subterm_specif renv stack t) + +and stack_element_specif = function + |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h + |SArg x -> x + +and extract_stack renv a = function + | [] -> Lazy.lazy_from_val Not_subterm , [] + | h::t -> stack_element_specif h, t + + +(* Check size x is a correct size for recursive calls. *) +let check_is_subterm x = + match Lazy.force x with Subterm (Strict,_) | Dead_code -> true | _ -> false @@ -637,7 +624,7 @@ let check_is_subterm renv c = exception FixGuardError of env * guard_error -let error_illegal_rec_call renv fx arg = +let error_illegal_rec_call renv fx (arg_renv,arg) = let (_,le_vars,lt_vars) = List.fold_left (fun (i,le,lt) sbt -> @@ -647,7 +634,8 @@ let error_illegal_rec_call renv fx arg = | _ -> (i+1, le ,lt)) (1,[],[]) renv.genv in raise (FixGuardError (renv.env, - RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars))) + RecursionOnIllegalTerm(fx,(arg_renv.env, arg), + le_vars,lt_vars))) let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) @@ -659,48 +647,57 @@ let check_one_fix renv recpos def = let nfi = Array.length recpos in (* Checks if [t] only make valid recursive calls *) - let rec check_rec_call renv t = + let rec check_rec_call renv stack t = (* if [t] does not make recursive calls, it is guarded: *) if noccur_with_meta renv.rel_min nfi t then () else - let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in + let (f,l) = decompose_app (whd_betaiotazeta t) in match f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) if renv.rel_min <= p & p < renv.rel_min+nfi then begin - List.iter (check_rec_call renv) l; + List.iter (check_rec_call renv []) l; (* the position of the invoked fixpoint: *) let glob = renv.rel_min+nfi-1-p in (* the decreasing arg of the rec call: *) let np = recpos.(glob) in - if List.length l <= np then error_partial_apply renv glob + let stack' = push_stack_closures renv l stack in + if List.length stack' <= np then error_partial_apply renv glob else (* Check the decreasing arg is smaller *) - let z = List.nth l np in - if not (check_is_subterm renv z) then - error_illegal_rec_call renv glob z + let z = List.nth stack' np in + if not (check_is_subterm (stack_element_specif z)) then + begin match z with + |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') + |SArg _ -> error_partial_apply renv glob + end end else begin match pi2 (lookup_rel p renv.env) with | None -> - List.iter (check_rec_call renv) l + List.iter (check_rec_call renv []) l | Some c -> - try List.iter (check_rec_call renv) l - with FixGuardError _ -> check_rec_call renv (applist(c,l)) + try List.iter (check_rec_call renv []) l + with FixGuardError _ -> + check_rec_call renv stack (applist(lift p c,l)) end - + | Case (ci,p,c_0,lrest) -> - List.iter (check_rec_call renv) (c_0::p::l); + List.iter (check_rec_call renv []) (c_0::p::l); (* compute the recarg information for the arguments of each branch *) - let lbr = case_subterm_specif renv ci c_0 lrest in - Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr + let case_spec = branches_specif renv + (lazy_subterm_specif renv [] c_0) ci in + let stack' = push_stack_closures renv l stack in + Array.iteri (fun k br' -> + let stack_br = push_stack_args case_spec.(k) stack' in + check_rec_call renv stack_br br') lrest (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : - if - g = Fix g/p := [y1:T1]...[yp:Tp]e & + if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e & - f is guarded with respect to the set of pattern variables S in a1 ... am & - f is guarded with respect to the set of pattern variables S @@ -710,81 +707,80 @@ let check_one_fix renv recpos def = S+{yp} in e then f is guarded with respect to S in (g a1 ... am). Eduardo 7/9/98 *) - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> - List.iter (check_rec_call renv) l; - Array.iter (check_rec_call renv) typarray; + List.iter (check_rec_call renv []) l; + Array.iter (check_rec_call renv []) typarray; let decrArg = recindxs.(i) in let renv' = push_fix_renv renv recdef in - if (List.length l < (decrArg+1)) then - Array.iter (check_rec_call renv') bodies - else + let stack' = push_stack_closures renv l stack in Array.iteri (fun j body -> - if i=j then - let theDecrArg = List.nth l decrArg in - let arg_spec = lazy_subterm_specif renv theDecrArg in - check_nested_fix_body renv' (decrArg+1) arg_spec body - else check_rec_call renv' body) + if i=j && (List.length stack' > decrArg) then + let recArg = List.nth stack' decrArg in + let arg_sp = stack_element_specif recArg in + check_nested_fix_body renv' (decrArg+1) arg_sp body + else check_rec_call renv' [] body) bodies | Const kn -> if evaluable_constant kn renv.env then - try List.iter (check_rec_call renv) l + try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - check_rec_call renv(applist(constant_value renv.env kn, l)) - else List.iter (check_rec_call renv) l - - (* The cases below simply check recursively the condition on the - subterms *) - | Cast (a,_, b) -> - List.iter (check_rec_call renv) (a::b::l) + let value = (applist(constant_value renv.env kn, l)) in + check_rec_call renv stack value + else List.iter (check_rec_call renv []) l | Lambda (x,a,b) -> - List.iter (check_rec_call renv) (a::l); - check_rec_call (push_var_renv renv (x,a)) b + assert (l = []); + check_rec_call renv [] a ; + let spec, stack' = extract_stack renv a stack in + check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> - List.iter (check_rec_call renv) (a::l); - check_rec_call (push_var_renv renv (x,a)) b + assert (l = [] && stack = []); + check_rec_call renv [] a; + check_rec_call (push_var_renv renv (x,a)) [] b | CoFix (i,(_,typarray,bodies as recdef)) -> - List.iter (check_rec_call renv) l; - Array.iter (check_rec_call renv) typarray; + List.iter (check_rec_call renv []) l; + Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in - Array.iter (check_rec_call renv') bodies + Array.iter (check_rec_call renv' []) bodies - | (Ind _ | Construct _ | Sort _) -> - List.iter (check_rec_call renv) l + | (Ind _ | Construct _) -> + List.iter (check_rec_call renv []) l | Var id -> begin match pi2 (lookup_named id renv.env) with | None -> - List.iter (check_rec_call renv) l + List.iter (check_rec_call renv []) l | Some c -> - try List.iter (check_rec_call renv) l - with (FixGuardError _) -> check_rec_call renv (applist(c,l)) + try List.iter (check_rec_call renv []) l + with (FixGuardError _) -> + check_rec_call renv stack (applist(c,l)) end + | Sort _ -> assert (l = []) + (* l is not checked because it is considered as the meta's context *) | (Evar _ | Meta _) -> () - | (App _|LetIn _) -> assert false (* beta zeta reduction *) + | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then - check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body + check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match body with | Lambda (x,a,b) -> - check_rec_call renv a; + check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in - check_nested_fix_body renv' (decr-1) recArgsDecrArg b + check_nested_fix_body renv' (decr-1) recArgsDecrArg b | _ -> anomaly "Not enough abstractions in fix body" - + in - check_rec_call renv def + check_rec_call renv [] def let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = diff --git a/checker/inductive.mli b/checker/inductive.mli index e658a798..2cf7c70d 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> subterm_spec -val case_branches_specif : guard_env -> subterm_spec Lazy.t -> inductive -> - constr array -> (guard_env * constr) array +type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t +val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec +val branches_specif : guard_env -> subterm_spec Lazy.t -> case_info -> + subterm_spec Lazy.t list array diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 95387cac..9942816d 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -21,8 +21,8 @@ let refresh_arity ar = Sort (Type u) when not (Univ.is_univ_variable u) -> let u' = Univ.fresh_local_univ() in mkArity (ctxt,Type u'), - Univ.enforce_geq u' u Univ.Constraint.empty - | _ -> ar, Univ.Constraint.empty + Univ.enforce_geq u' u Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); @@ -33,7 +33,7 @@ let check_constant_declaration env kn cb = let ty, cu = refresh_arity ty in let envty = add_constraints cu env' in let _ = infer_type envty ty in - (match cb.const_body with + (match body_of_constant cb with | Some bd -> let j = infer env' (force_constr bd) in conv_leq envty j ty @@ -58,13 +58,6 @@ let rec list_split_assoc k rev_before = function | (k',b)::after when k=k' -> rev_before,b,after | h::tail -> list_split_assoc k (h::rev_before) tail -let rec list_fold_map2 f e = function - | [] -> (e,[],[]) - | h::t -> - let e',h1',h2' = f e h in - let e'',t1',t2' = list_fold_map2 f e' t in - e'',h1'::t1',h2'::t2' - let check_definition_sub env cb1 cb2 = let check_type env t1 t2 = @@ -117,14 +110,19 @@ let check_definition_sub env cb1 cb2 = let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_type env typ1 typ2; - (match cb2 with - | {const_body=Some lc2;const_opaque=false} -> - let c2 = force_constr lc2 in - let c1 = match cb1.const_body with - | Some lc1 -> force_constr lc1 - | None -> assert false in - Reduction.conv env c1 c2 - | _ -> ()) + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) + (match cb2.const_body with + | Undef _ | OpaqueDef _ -> () + | Def lc2 -> + (match cb1.const_body with + | Def lc1 -> + let c1 = force_constr lc1 in + let c2 = force_constr lc2 in + Reduction.conv env c1 c2 + (* Coq only places transparent cb in With_definition_body *) + | _ -> assert false)) let lookup_modtype mp env = try Environ.lookup_modtype mp env @@ -259,14 +257,14 @@ and check_module env mp mb = {typ_mp=mp; typ_expr=sign; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; + typ_constraints=Univ.empty_constraint; typ_delta = mb.mod_delta;} and mtb2 = {typ_mp=mp; typ_expr=mb.mod_type; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; - typ_delta = mb.mod_delta;}; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} in let env = add_module (module_body_of_type mp mtb1) env in check_subtypes env mtb1 mtb2 diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli new file mode 100644 index 00000000..8021ed0f --- /dev/null +++ b/checker/mod_checking.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Names.module_path -> Declarations.module_body -> unit diff --git a/checker/modops.ml b/checker/modops.ml index 38aeaee2..2dc5d062 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error_not_a_functor mtb - -let is_functor = function - | SEBfunctor (arg_id,arg_t,body_t) -> true - | _ -> false - let module_body_of_type mp mtb = { mod_mp = mp; mod_type = mtb.typ_expr; @@ -75,14 +66,6 @@ let module_body_of_type mp mtb = mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else - (* let mb1=lookup_module mp1 env in - let mb2=lookup_module mp2 env in - if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) - then () - else*) error_not_equal mp1 mp2 - let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in @@ -112,23 +95,16 @@ and add_module mb env = let strengthen_const mp_from l cb resolver = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> + match cb.const_body with + | Def _ -> cb + | _ -> let con = make_con mp_from empty_dirpath l in - (* let con = constant_of_delta resolver con in*) - let const = Const con in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - } - + (* let con = constant_of_delta resolver con in*) + { cb with const_body = Def (Declarations.from_val (Const con)) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then - mb + mb else match mb.mod_type with | SEBstruct (sign) -> @@ -154,34 +130,33 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' + resolve_out,item::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in let mb_out = strengthen_mod mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out, item'::rest' - | (l,SFBmodtype mty as item) :: rest -> + resolve_out (*add_delta_resolver resolve_out mb.mod_delta*), + item':: rest' + | (l,SFBmodtype mty as item) :: rest -> let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out, item::rest' + resolve_out,item::rest' let strengthen mtb mp = match mtb.typ_expr with - | SEBstruct (sign) -> + | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig mtb.typ_mp sign mp mtb.typ_delta - in - {mtb with - typ_expr = SEBstruct(sign_out); - typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta + strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in + {mtb with + typ_expr = SEBstruct(sign_out); + typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} | SEBfunctor _ -> mtb | _ -> anomaly "Modops:the evaluation of the structure failed " let subst_and_strengthen mb mp = - strengthen_mod mb.mod_mp mp - (subst_module (map_mp mb.mod_mp mp) mb) + strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) let module_type_of_module mp mb = diff --git a/checker/modops.mli b/checker/modops.mli index 2f9f2e8c..5ed7b0ce 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* structure_body -> delta_resolver -> env -> en (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val check_modpath_equiv : env -> module_path -> module_path -> unit - val strengthen : module_type_body -> module_path -> module_type_body val subst_and_strengthen : module_body -> module_path -> module_body diff --git a/checker/reduction.ml b/checker/reduction.ml index ba8ceeef..3aeaa102 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* x - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) let whd_betadeltaiota env t = match t with @@ -107,15 +105,6 @@ let beta_appvect c v = | _ -> applist (substl env t, stack) in stacklam [] c (Array.to_list v) -let betazeta_appvect n c v = - let rec stacklam n env t stack = - if n = 0 then applist (substl env t, stack) else - match t, stack with - Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack - | _ -> anomaly "Not enough lambda/let's" in - stacklam n [] c (Array.to_list v) - (********************************************************************) (* Conversion *) (********************************************************************) @@ -219,7 +208,7 @@ let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = Util.check_for_interrupt (); (* First head reduce both terms *) - let rec whd_both (t1,stk1) (t2,stk2) = + let rec whd_both (t1,stk1) (t2,stk2) = let st1' = whd_stack infos t1 stk1 in let st2' = whd_stack infos t2 stk2 in (* Now, whd_stack on term2 might have modified st1 (due to sharing), @@ -279,20 +268,10 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = | None -> raise NotConvertible) in eqappr univ cv_pb infos app1 app2) - (* only one constant, defined var or defined rel *) - | (FFlex fl1, _) -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2 - | None -> raise NotConvertible) - | (_, FFlex fl2) -> - (match unfold_reference infos fl2 with - | Some def2 -> - eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) - | None -> raise NotConvertible) - (* other constructors *) | (FLambda _, FLambda _) -> + (* Inconsistency: we tolerate that v1, v2 contain shift and update but + we throw them away *) assert (is_empty_stack v1 && is_empty_stack v2); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in @@ -305,6 +284,32 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = ccnv univ CONV infos el1 el2 c1 c'1; ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 + (* Eta-expansion on the fly *) + | (FLambda _, _) -> + if v1 <> [] then + anomaly "conversion was given unreduced term (FLambda)"; + let (_,_ty1,bd1) = destFLambda mk_clos hd1 in + eqappr univ CONV infos + (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) + | (_, FLambda _) -> + if v2 <> [] then + anomaly "conversion was given unreduced term (FLambda)"; + let (_,_ty2,bd2) = destFLambda mk_clos hd2 in + eqappr univ CONV infos + (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) + + (* only one constant, defined var or defined rel *) + | (FFlex fl1, _) -> + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2 + | None -> raise NotConvertible) + | (_, FFlex fl2) -> + (match unfold_reference infos fl2 with + | Some def2 -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) + | None -> raise NotConvertible) + (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd ind1, FInd ind2) -> @@ -367,37 +372,18 @@ and convert_vect univ infos lft1 lft2 v1 v2 = let clos_fconv cv_pb env t1 t2 = let infos = create_clos_infos betaiotazeta env in let univ = universes env in - ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2) + ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2) let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then () else clos_fconv cv_pb env t1 t2 -let conv_cmp = fconv let conv = fconv CONV let conv_leq = fconv CUMUL -let conv_leq_vecti env v1 v2 = - array_fold_left2_i - (fun i _ t1 t2 -> - (try conv_leq env t1 t2 - with (NotConvertible|Invalid_argument _) -> - raise (NotConvertibleVect i)); - ()) - () - v1 - v2 - -(* option for conversion *) - -let vm_conv = ref fconv -let set_vm_conv f = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try - !vm_conv cv_pb env t1 t2 - with Not_found | Invalid_argument _ -> - (* If compilation fails, fall-back to closure conversion *) - clos_fconv cv_pb env t1 t2 +(* option for conversion : no compilation for the checker *) + +let vm_conv = fconv (********************************************************************) (* Special-Purpose Reduction *) @@ -452,9 +438,3 @@ let dest_arity env c = | Sort s -> l,s | _ -> error "not an arity" -let is_arity env c = - try - let _ = dest_arity env c in - true - with UserError _ -> false - diff --git a/checker/reduction.mli b/checker/reduction.mli index 8e69da44..6695fd03 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> constr +val whd_betaiotazeta : constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr @@ -31,7 +29,6 @@ type conv_pb = CONV | CUMUL val conv : constr conversion_function val conv_leq : constr conversion_function -val conv_leq_vecti : constr array conversion_function val vm_conv : conv_pb -> constr conversion_function @@ -40,9 +37,6 @@ val vm_conv : conv_pb -> constr conversion_function (* Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(* Builds an application node, reducing the [n] first beta-zeta redexes. *) -val betazeta_appvect : int -> constr -> constr array -> constr - (* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> constr -> constr list -> constr @@ -54,4 +48,3 @@ val dest_prod : env -> constr -> rel_context * constr val dest_prod_assum : env -> constr -> rel_context * constr val dest_arity : env -> constr -> arity -val is_arity : env -> constr -> bool diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index a669c5e8..bc067dc5 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,19 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ ) as x -> x - | SFBmodule m -> SFBmodule (lighten_module m) - | SFBmodtype m -> SFBmodtype - ({m with - typ_expr = lighten_modexpr m.typ_expr})) - in - List.map lighten_body struc - -and lighten_modexpr = function - | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid, - ({mty with - typ_expr = lighten_modexpr mty.typ_expr}), - lighten_modexpr mexpr) - | SEBident mp as x -> x - | SEBstruct ( struc) -> - SEBstruct ( lighten_struct struc) - | SEBapply (mexpr,marg,u) -> - SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) - | SEBwith (seb,wdcl) -> - SEBwith (lighten_modexpr seb,wdcl) - -let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) - - type compiled_library = dir_path * module_body * (dir_path * Digest.t) list * engagement option + (* Store the body of modules' opaque constants inside a table. + + This module is used during the serialization and deserialization + of vo files. + + By adding an indirection to the opaque constant definitions, we + gain the ability not to load them. As these constant definitions + are usually big terms, we save a deserialization time as well as + some memory space. *) +module LightenLibrary : sig + type table + type lightened_compiled_library + val load : table -> lightened_compiled_library -> compiled_library +end = struct + + (* The table is implemented as an array of [constr_substituted]. + Keys are hence integers. To avoid changing the [compiled_library] + type, we brutally encode integers into [lazy_constr]. This isn't + pretty, but shouldn't be dangerous since the produced structure + [lightened_compiled_library] is abstract and only meant for writing + to .vo via Marshal (which doesn't care about types). + *) + type table = constr_substituted array + let key_of_lazy_constr (c:lazy_constr) = (Obj.magic c : int) + + (* To avoid any future misuse of the lightened library that could + interpret encoded keys as real [constr_substituted], we hide + these kind of values behind an abstract datatype. *) + type lightened_compiled_library = compiled_library + + (* Map a [compiled_library] to another one by just updating + the opaque term [t] to [on_opaque_const_body t]. *) + let traverse_library on_opaque_const_body = + let rec traverse_module mb = + match mb.mod_expr with + None -> + { mb with + mod_expr = None; + mod_type = traverse_modexpr mb.mod_type; + } + | Some impl when impl == mb.mod_type-> + let mtb = traverse_modexpr mb.mod_type in + { mb with + mod_expr = Some mtb; + mod_type = mtb; + } + | Some impl -> + { mb with + mod_expr = Option.map traverse_modexpr mb.mod_expr; + mod_type = traverse_modexpr mb.mod_type; + } + and traverse_struct struc = + let traverse_body (l,body) = (l,match body with + | (SFBconst cb) when is_opaque cb -> + SFBconst {cb with const_body = on_opaque_const_body cb.const_body} + | (SFBconst _ | SFBmind _ ) as x -> + x + | SFBmodule m -> + SFBmodule (traverse_module m) + | SFBmodtype m -> + SFBmodtype ({m with typ_expr = traverse_modexpr m.typ_expr})) + in + List.map traverse_body struc + + and traverse_modexpr = function + | SEBfunctor (mbid,mty,mexpr) -> + SEBfunctor (mbid, + ({mty with + typ_expr = traverse_modexpr mty.typ_expr}), + traverse_modexpr mexpr) + | SEBident mp as x -> x + | SEBstruct (struc) -> + SEBstruct (traverse_struct struc) + | SEBapply (mexpr,marg,u) -> + SEBapply (traverse_modexpr mexpr,traverse_modexpr marg,u) + | SEBwith (seb,wdcl) -> + SEBwith (traverse_modexpr seb,wdcl) + in + fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) + + (* Loading is also a traversing that decodes the embedded keys that + are inside the [lightened_library]. If the [load_proof] flag is + set, we lookup inside the table to graft the + [constr_substituted]. Otherwise, we set the [const_body] field + to [None]. + *) + let load table lightened_library = + let decode_key = function + | Undef _ | Def _ -> assert false + | OpaqueDef k -> + let k = key_of_lazy_constr k in + let body = + try table.(k) + with _ -> error "Error while retrieving an opaque body" + in + OpaqueDef (lazy_constr_from_val body) + in + traverse_library decode_key lightened_library + +end + open Validate -let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|]) -let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|] +let val_deps = val_list (val_tuple ~name:"dep"[|val_dp;no_val|]) +let val_vo = val_tuple ~name:"vo" [|val_dp;val_module;val_deps;val_opt val_eng|] (* This function should append a certificate to the .vo file. The digest must be part of the certicate to rule out attackers @@ -124,15 +185,15 @@ let import file (dp,mb,depends,engmt as vo) digest = let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; + Mod_checking.check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) full_add_module dp mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt) digest = -(* if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*) +let unsafe_import file (dp,mb,depends,engmt as vo) digest = + if !Flags.debug then ignore vo; (*Validate.apply !Flags.debug val_vo vo;*) let env = !genv in check_imports (errorlabstrm"unsafe_import") dp env depends; check_engagement env engmt; diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 00aa1a84..cd2c06d2 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -1,20 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val get_env : unit -> env (* exporting and importing modules *) @@ -25,3 +22,19 @@ val import : System.physical_path -> compiled_library -> Digest.t -> unit val unsafe_import : System.physical_path -> compiled_library -> Digest.t -> unit + +(** Store the body of modules' opaque constants inside a table. + + This module is used during the serialization and deserialization + of vo files. +*) +module LightenLibrary : +sig + type table + type lightened_compiled_library + + (** [load table lcl] builds a compiled library from a + lightened library [lcl] by remplacing every index by its related + opaque terms inside [table]. *) + val load : table -> lightened_compiled_library -> compiled_library +end diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 4f113cf9..0c97254b 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*Start by checking types*) - let cb1 = subst_const_body subst1 cb1 in - let cb2 = subst_const_body subst2 cb2 in - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_type env typ1 typ2; - let con = make_con mp1 empty_dirpath l in - (match cb2 with - | {const_body=Some lc2;const_opaque=false} -> - let c2 = force_constr lc2 in - let c1 = match cb1.const_body with - | Some lc1 -> force_constr lc1 - | None -> Const con - in - check_conv conv env c1 c2 - | _ -> ()) + let cb1 = subst_const_body subst1 cb1 in + let cb2 = subst_const_body subst2 cb2 in + (*Start by checking types*) + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_type env typ1 typ2; + (* Now we check the bodies: + - A transparent constant can only be implemented by a compatible + transparent constant. + - In the signature, an opaque is handled just as a parameter: + anything of the right type can implement it, even if bodies differ. + *) + (match cb2.const_body with + | Undef _ | OpaqueDef _ -> () + | Def lc2 -> + (match cb1.const_body with + | Undef _ | OpaqueDef _ -> error () + | Def lc1 -> + (* NB: cb1 might have been strengthened and appear as transparent. + Anyway [check_conv] will handle that afterwards. *) + let c1 = force_constr lc1 in + let c2 = force_constr lc2 in + check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -262,7 +267,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "inductive type and give a definition to map the old name to the new " ^ "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if cb2.const_body <> None then error () ; + if constant_has_body cb2 then error () ; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 @@ -273,7 +278,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = "constructor and give a definition to map the old name to the new " ^ "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if cb2.const_body <> None then error () ; + if constant_has_body cb2 then error () ; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv env ty1 ty2 @@ -281,7 +286,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in - let mty2 = module_type_of_module None msb2 in + let mty2 = module_type_of_module None msb2 in check_modtypes env mty1 mty2 subst1 subst2 false; @@ -363,11 +368,5 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = else check_structure env mtb1' mtb2' equiv subst1 subst2 let check_subtypes env sup super = - (*if sup<>super then*) check_modtypes env (strengthen sup sup.typ_mp) super empty_subst - (map_mp super.typ_mp sup.typ_mp) false - -let check_equal env sup super = - (*if sup<>super then*) - check_modtypes env sup super empty_subst - (map_mp super.typ_mp sup.typ_mp) true + (map_mp super.typ_mp sup.typ_mp) false diff --git a/checker/subtyping.mli b/checker/subtyping.mli index d9cbe5ad..ecdf5577 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_type_body -> module_type_body -> unit -val check_equal : env -> module_type_body -> module_type_body -> unit diff --git a/checker/term.ml b/checker/term.ml index 61369586..ab40b6fa 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (fun c -> c) | el -> exliftn el @@ -313,22 +312,15 @@ let subst1 lam = substl [lam] (***************************************************************************) let val_ndecl = - val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|] + val_tuple ~name:"named_declaration"[|val_id;val_opt val_constr;val_constr|] let val_rdecl = - val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|] + val_tuple ~name:"rel_declaration"[|val_name;val_opt val_constr;val_constr|] let val_nctxt = val_list val_ndecl let val_rctxt = val_list val_rdecl type named_declaration = identifier * constr option * constr type rel_declaration = name * constr option * constr -let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty) -let map_rel_declaration = map_named_declaration - -let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) -let fold_rel_declaration = fold_named_declaration - - type named_context = named_declaration list let empty_named_context = [] let fold_named_context f l ~init = List.fold_right f l init @@ -439,7 +431,6 @@ let decompose_prod_n_assum n = (***************************) type arity = rel_context * sorts -let val_arity = val_tuple"arity"[|val_rctxt;val_constr|] let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign diff --git a/checker/term.mli b/checker/term.mli index 1367e581..0340c79b 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -12,7 +12,7 @@ type case_printing = { ind_nargs : int; style : case_style; } type case_info = { ci_ind : inductive; ci_npar : int; - ci_cstr_nargs : int array; + ci_cstr_ndecls : int array; ci_pp_info : case_printing; } type contents = Pos | Null @@ -73,14 +73,6 @@ val subst1 : constr -> constr -> constr type named_declaration = identifier * constr option * constr type rel_declaration = name * constr option * constr -val map_named_declaration : - (constr -> constr) -> named_declaration -> named_declaration -val map_rel_declaration : - (constr -> constr) -> rel_declaration -> rel_declaration -val fold_named_declaration : - (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a -val fold_rel_declaration : - (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a type named_context = named_declaration list val empty_named_context : named_context val fold_named_context : @@ -111,8 +103,8 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool val eq_constr : constr -> constr -> bool (* Validation *) -val val_sortfam : Obj.t -> unit -val val_sort : Obj.t -> unit -val val_constr : Obj.t -> unit -val val_rctxt : Obj.t -> unit -val val_nctxt : Obj.t -> unit +val val_sortfam : Validate.func +val val_sort : Validate.func +val val_constr : Validate.func +val val_rctxt : Validate.func +val val_nctxt : Validate.func diff --git a/checker/type_errors.ml b/checker/type_errors.ml index bd3bb90d..12609832 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unsafe_judgment -> int -> 'a val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a -val error_generalization : env -> name * constr -> unsafe_judgment -> 'a - val error_actual_type : env -> unsafe_judgment -> constr -> 'a val error_cant_apply_not_functional : diff --git a/checker/typeops.ml b/checker/typeops.ml index dffc9fe1..5226db53 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error_reference_variables env c - -(* Checks if the given context of variables [hyps] is included in the - current context of [env]. *) -(* -let check_hyps id env hyps = - let hyps' = named_context env in - if not (hyps_inclusion env hyps hyps') then - error_reference_variables env id -*) -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -let extract_level env p = - let _,c = dest_prod_assum env p in - match c with Sort (Type u) -> Some u | _ -> None - -let extract_context_levels env = - List.fold_left - (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] - -let make_polymorphic_if_arity env t = - let params, ccl = dest_prod_assum env t in - match ccl with - | Sort (Type u) -> - let param_ccls = extract_context_levels env params in - let s = { poly_param_levels = param_ccls; poly_level = u} in - PolymorphicArity (params,s) - | _ -> - NonPolymorphicType t - (* Type of constants *) let type_of_constant_knowing_parameters env t paramtyps = @@ -135,9 +102,6 @@ let type_of_constant_knowing_parameters env t paramtyps = let type_of_constant_type env t = type_of_constant_knowing_parameters env t [||] -let type_of_constant env cst = - type_of_constant_type env (constant_type env cst) - let judge_of_constant_knowing_parameters env cst paramstyp = let c = Const cst in let cb = @@ -291,7 +255,7 @@ let refresh_arity env ar = match hd with Sort (Type u) when not (is_univ_variable u) -> let u' = fresh_local_univ() in - let env' = add_constraints (enforce_geq u' u Constraint.empty) env in + let env' = add_constraints (enforce_geq u' u empty_constraint) env in env', mkArity (ctxt,Type u') | _ -> env, ar @@ -406,12 +370,9 @@ and execute_recdef env (names,lar,vdef) i = and execute_array env = Array.map (execute env) -and execute_list env = List.map (execute env) - (* Derived functions *) let infer env constr = execute env constr let infer_type env constr = execute_type env constr -let infer_v env cv = execute_array env cv (* Typing of several terms. *) diff --git a/checker/typeops.mli b/checker/typeops.mli index f4f29fe5..eafe4735 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f ctx) +let ext s f (ctx:error_context) = f (ctx/s) + -let ep s1 f s2 = f (s1^"/"^s2) +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 let apply debug f x = let o = Obj.repr x in - try f o - with ValidObjError(msg,obj) -> + try f mt_ec o + with ValidObjError(msg,ctx,obj) -> if debug then begin print_endline ("Validation failed: "^msg); + print_endline ("Context: "^String.concat"/"(List.rev ctx)); pr_obj obj end; failwith "vo structure validation failed" (* data not validated *) -let no_val (o:Obj.t) = () +let no_val (c:error_context) (o:Obj.t) = () (* Check that object o is a block with tag t *) -let val_tag t o = +let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () - else fail o ("expected tag "^string_of_int t) + else fail ctx o ("expected tag "^string_of_int t) -let val_block s o = +let val_block ctx o = if Obj.is_block o then (if Obj.tag o > Obj.no_scan_tag then - fail o (s^": found no scan tag")) - else fail o (s^": expected block obj") + fail ctx o "block: found no scan tag") + else fail ctx o "expected block obj" (* Check that an object is a tuple (or a record). v is an array of validation functions for each field. Its size corresponds to the expected size of the object. *) -let val_tuple s v o = +let val_tuple ?name v ctx o = + let ctx = match name with + Some n -> ctx/n + | _ -> ctx in let n = Array.length v in - val_block ("tuple: "^s) o; - if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v + let val_fld i f = + f (ctx/("fld="^string_of_int i)) (Obj.field o i) in + val_block ctx o; + if Obj.size o = n then Array.iteri val_fld v else - fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)) + fail ctx o + ("tuple size: found "^string_of_int (Obj.size o)^ + ", expected "^string_of_int n) (* Check that the object is either a constant constructor of tag < cc, or a constructed variant. each element of vv is an array of @@ -83,70 +96,79 @@ let val_tuple s v o = The size of vv corresponds to the number of non-constant constructors, and the size of vv.(i) is the expected arity of the i-th non-constant constructor. *) -let val_sum s cc vv o = +let val_sum name cc vv ctx o = + let ctx = ctx/name in if Obj.is_block o then - (val_block s o; + (val_block (ctx/name) o; let n = Array.length vv in let i = Obj.tag o in - if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o - else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i)) + let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in + if i < n then val_tuple vv.(i) ctx' o + else fail ctx' o ("sum: unexpected tag")) else if Obj.is_int o then let (n:int) = Obj.magic o in (if n<0 || n>=cc then - fail o (s^": bad constant constructor "^string_of_int n)) - else fail o ("not a sum ("^s^")") + fail ctx o ("bad constant constructor "^string_of_int n)) + else fail ctx o "not a sum" let val_enum s n = val_sum s n [||] (* Recursive types: avoid looping by eta-expansion *) -let rec val_rec_sum s cc f o = - val_sum s cc (f (val_rec_sum s cc f)) o - -let rec val_rectype f o = - f (val_rectype f) o +let rec val_rec_sum name cc f ctx o = + val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o (**************************************************************************) (* Builtin types *) (* Check the o is an array of values satisfying f. *) -let val_array ?(name="array") f o = - val_block name o; +let val_array ?(pos=false) f ctx o = + let upd_ctx = + if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in + val_block (ctx/"array") o; for i = 0 to Obj.size o - 1 do - (f (Obj.field o i):unit) + (f (upd_ctx i) (Obj.field o i):unit) done (* Integer validator *) -let val_int o = - if not (Obj.is_int o) then fail o "expected an int" +let val_int ctx o = + if not (Obj.is_int o) then fail ctx o "expected an int" (* String validator *) -let val_str o = - try val_tag Obj.string_tag o - with Failure _ -> fail o "expected a string" +let val_str ctx o = + try val_tag Obj.string_tag ctx o + with Failure _ -> fail ctx o "expected a string" (* Booleans *) let val_bool = val_enum "bool" 2 (* Option type *) -let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|] +let val_opt ?(name="option") f = + val_sum name 1 [|[|f|]|] (* Lists *) -let val_list ?(name="list") f = - val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|]) +let val_list ?(name="list") f ctx = + val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|]) + ctx (* Reference *) -let val_ref ?(name="ref") f = val_tuple name [|f|] +let val_ref ?(name="ref") f ctx = + val_tuple [|f|] (ctx/name) (**************************************************************************) (* Standard library types *) (* Sets *) let val_set ?(name="Set.t") f = - val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|]) + val_rec_sum name 1 + (fun vset -> [|[|vset;ext "elem" f; + vset;ext "bal" val_int|]|]) (* Maps *) let rec val_map ?(name="Map.t") fk fv = - val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|]) + val_rec_sum name 1 + (fun vmap -> + [|[|vmap; ext "key" fk; ext "value" fv; + vmap; ext "bal" val_int|]|]) (**************************************************************************) (* Coq types *) @@ -158,19 +180,19 @@ let val_dp = val_list ~name:"dirpath" val_id let val_name = val_sum "name" 1 [|[|val_id|]|] -let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|] +let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|] let val_mp = val_rec_sum "module_path" 0 (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) -let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] +let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|] let val_con = - val_tuple "constant/mutind" [|val_kn;val_kn|] + val_tuple ~name:"constant/mutind" [|val_kn;val_kn|] -let val_ind = val_tuple "inductive"[|val_con;val_int|] -let val_cstr = val_tuple "constructor"[|val_ind;val_int|] +let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|] +let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|] (* univ *) let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|] @@ -179,5 +201,5 @@ let val_univ = val_sum "univ" 0 let val_cstrs = val_set ~name:"Univ.constraints" - (val_tuple "univ_constraint" + (val_tuple ~name:"univ_constraint" [|val_level;val_enum "order_request" 3;val_level|]) -- cgit v1.2.3