From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- checker/check.ml | 36 +- checker/check.mllib | 34 ++ checker/check_stat.ml | 6 +- checker/checker.ml | 108 +++--- checker/closure.ml | 52 ++- checker/closure.mli | 5 +- checker/declarations.ml | 875 +++++++++++++++++++++++++++++++---------------- checker/declarations.mli | 69 ++-- checker/environ.ml | 109 +++--- checker/environ.mli | 16 +- checker/include | 24 +- checker/indtypes.ml | 120 +++---- checker/inductive.ml | 164 ++++----- checker/mod_checking.ml | 305 ++++++++--------- checker/modops.ml | 405 ++++++++-------------- checker/modops.mli | 32 +- checker/reduction.ml | 51 +-- checker/reduction.mli | 5 +- checker/safe_typing.ml | 40 +-- checker/subtyping.ml | 252 +++++++------- checker/term.ml | 82 ++--- checker/type_errors.ml | 4 +- checker/type_errors.mli | 12 +- checker/typeops.ml | 66 ++-- checker/validate.ml | 16 +- 25 files changed, 1516 insertions(+), 1372 deletions(-) create mode 100644 checker/check.mllib (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 82df62b4..b2aa6555 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -24,10 +24,10 @@ type section_path = { basename : string } let dir_of_path p = make_dirpath (List.map id_of_string p.dirpath) -let path_of_dirpath dir = +let path_of_dirpath dir = match repr_dirpath dir with [] -> failwith "path_of_dirpath" - | l::dir -> + | l::dir -> {dirpath=List.map string_of_id dir;basename=string_of_id l} let pr_dirlist dp = prlist_with_sep (fun _ -> str".") str (List.rev dp) @@ -40,7 +40,7 @@ type library_objects type compilation_unit_name = dir_path -type library_disk = { +type library_disk = { md_name : compilation_unit_name; md_compiled : Safe_typing.compiled_library; md_objects : library_objects; @@ -48,7 +48,7 @@ type library_disk = { md_imports : compilation_unit_name list } (************************************************************************) -(*s Modules on disk contain the following informations (after the magic +(*s Modules on disk contain the following informations (after the magic number, and before the digest). *) (*s Modules loaded in memory contain the following informations. They are @@ -61,7 +61,7 @@ type library_t = { library_deps : (compilation_unit_name * Digest.t) list; library_digest : Digest.t } -module LibraryOrdered = +module LibraryOrdered = struct type t = dir_path let compare d1 d2 = @@ -121,7 +121,7 @@ let load_paths = ref ([],[] : System.physical_path list * logical_path list) let get_load_paths () = fst !load_paths (* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = +let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) let n = String.length curdir in if String.length p > n && String.sub p 0 n = curdir then @@ -139,7 +139,7 @@ let strip_path p = let canonical_path_name p = let current = Sys.getcwd () in - try + try Sys.chdir p; let p' = Sys.getcwd () in Sys.chdir current; @@ -148,7 +148,7 @@ let canonical_path_name p = (* We give up to find a canonical name and just simplify it... *) strip_path p -let find_logical_path phys_dir = +let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in match list_filter2 (fun p d -> p = phys_dir) !load_paths with | _,[dir] -> dir @@ -159,7 +159,7 @@ 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 + List.exists check_p lp let remove_load_path dir = load_paths := list_filter2 (fun p d -> p <> dir) !load_paths @@ -171,7 +171,7 @@ let add_load_path (phys_path,coq_path) = let phys_path = canonical_path_name phys_path in match list_filter2 (fun p d -> p = phys_path) !load_paths with | _,[dir] -> - if coq_path <> dir + if coq_path <> dir (* If this is not the default -I . to coqtop *) && not (phys_path = canonical_path_name Filename.current_dir_name @@ -195,7 +195,7 @@ 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) (************************************************************************) @@ -235,8 +235,8 @@ let locate_qualified_library qid = let dir = extend_dirpath (find_logical_path path) (id_of_string qid.basename) in (* Look if loaded *) - try - (dir, library_full_filename dir) + try + (dir, library_full_filename dir) with Not_found -> (dir, file) with Not_found -> raise LibNotFound @@ -245,7 +245,7 @@ let explain_locate_library_error qid = function | LibUnmappedDir -> let prefix = qid.dirpath in errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ + (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) | LibNotFound -> errorlabstrm "load_absolute_library_from" @@ -261,7 +261,7 @@ let try_locate_absolute_library dir = let try_locate_qualified_library qid = try locate_qualified_library qid - with e -> + with e -> explain_locate_library_error qid e (************************************************************************) @@ -300,7 +300,7 @@ 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,digest) = try let ch = with_magic_number_check raw_intern_library f in let (md:library_disk) = System.marshal_in ch in @@ -312,7 +312,7 @@ let intern_from_file (dir, f) = Flags.if_verbose msgnl(str" done]"); md,digest with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in - depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; + depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; mk_library md f digest let get_deps (dir, f) = @@ -366,7 +366,7 @@ let recheck_library ~norec ~admit ~check = let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in let nochk = fold_deps_list LibrarySet.remove ml nochk in let nochk = fold_deps_list LibrarySet.add al nochk in - (* explicitely required modules cannot be skipped... *) + (* explicitly required modules cannot be skipped... *) let nochk = List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in (* *) diff --git a/checker/check.mllib b/checker/check.mllib new file mode 100644 index 00000000..08dd78bc --- /dev/null +++ b/checker/check.mllib @@ -0,0 +1,34 @@ +Coq_config +Pp_control +Pp +Compat +Flags +Segmenttree +Unicodetable +Util +Option +Hashcons +System +Envars +Predicate +Rtree +Names +Univ +Esubst +Validate +Term +Declarations +Environ +Closure +Reduction +Type_errors +Modops +Inductive +Typeops +Indtypes +Subtyping +Mod_checking +Safe_typing +Check +Check_stat +Checker diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 6ea153a3..170ac638 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -17,7 +17,7 @@ open Environ let memory_stat = ref false -let print_memory_stat () = +let print_memory_stat () = if !memory_stat then begin Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()); Format.print_newline(); @@ -33,11 +33,11 @@ let pr_engt = function str "Theory: Set is predicative" let cst_filter f csts = - Cmap.fold + Cmap_env.fold (fun c ce acc -> if f c ce then c::acc else acc) csts [] -let is_ax _ cb = cb.const_body = None +let is_ax _ cb = cb.const_body = None let pr_ax csts = let axs = cst_filter is_ax csts in diff --git a/checker/checker.ml b/checker/checker.ml index 70e2eb97..e15c37e6 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -23,14 +23,14 @@ let parse_dir s = if n>=len then dirs else let pos = try - String.index_from s n '.' + String.index_from s n '.' with Not_found -> len in let dir = String.sub s n (pos-n) in - decoupe_dirs (dir::dirs) (pos+1) + decoupe_dirs (dir::dirs) (pos+1) in decoupe_dirs [] 0 -let dirpath_of_string s = +let dirpath_of_string s = match parse_dir s with [] -> invalid_arg "dirpath_of_string" | dir -> make_dirpath (List.map id_of_string dir) @@ -43,7 +43,7 @@ let (/) = Filename.concat let get_version_date () = try - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib () in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -67,8 +67,8 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try id_of_string d - with _ -> - if_verbose warning + with _ -> + if_verbose warning ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); flush_all (); failwith "caught" @@ -90,45 +90,38 @@ let includes = ref [] let push_include (s, alias) = includes := (s,alias,false) :: !includes let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes -let check_coq_overwriting p = - if string_of_id (list_last (repr_dirpath p)) = "Coq" then - error "The \"Coq\" logical root directory is reserved for the Coq library" - 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 - check_coq_overwriting p; push_rec_include (d, p) let set_include d p = let p = dirpath_of_string p in - check_coq_overwriting p; push_include (d,p) let set_rec_include d p = let p = dirpath_of_string p in - check_coq_overwriting p; push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in - let contrib = coqlib/"contrib" in + let plugins = coqlib/"plugins" in (* first user-contrib *) - if Sys.file_exists user_contrib then + if Sys.file_exists user_contrib then add_rec_path user_contrib Check.default_root_prefix; - (* then contrib *) - add_rec_path contrib (Names.make_dirpath [coq_root]); + (* then plugins *) + add_rec_path plugins (Names.make_dirpath [coq_root]); (* then standard library *) -(* List.iter +(* List.iter (fun (s,alias) -> - add_rec_path (coqlib/s) ([alias; coq_root])) + add_rec_path (coqlib/s) ([alias; coq_root])) theories_dirs_map;*) add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]); (* then current directory *) add_path "." Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) - List.iter + List.iter (fun (s,alias,reci) -> if reci then add_rec_path s alias else add_path s alias) (List.rev !includes); @@ -163,7 +156,7 @@ let compile_files () = Check.recheck_library ~norec:(List.rev !norec_list) ~admit:(List.rev !admit_list) - ~check:(List.rev !compile_list) + ~check:(List.rev !compile_list) let version () = Printf.printf "The Coq Proof Checker, version %s (%s)\n" @@ -180,7 +173,7 @@ let print_usage_channel co command = " -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 -as coqdir recursively map physical dir to logical coqdir -R dir coqdir (idem) -admit module load module and dependencies without checking @@ -189,9 +182,10 @@ let print_usage_channel co command = -where print Coq's standard library location and exit -v print Coq version and exit -boot boot mode - -o print the list of assumptions - -m print the maximum heap size - + -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 @@ -217,9 +211,9 @@ let anomaly_string () = str "Anomaly: " let report () = (str "." ++ spc () ++ str "Please report.") let print_loc loc = - if loc = dummy_loc then + if loc = dummy_loc then (str"") - else + else let loc = unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) let guill s = "\""^s^"\"" @@ -228,41 +222,41 @@ let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) let rec explain_exn = function - | Stream.Failure -> + | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") - | Stream.Error txt -> + | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) - | Token.Error txt -> + | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt) - | Sys_error msg -> + | Sys_error msg -> hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) - | UserError(s,pps) -> + | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) - | Out_of_memory -> + | Out_of_memory -> hov 0 (str "Out of memory") - | Stack_overflow -> + | Stack_overflow -> hov 0 (str "Stack overflow") - | Anomaly (s,pps) -> + | 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) ++ + 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 " from character " ++ int pos1 ++ str " to " ++ int pos2) else (str " at line " ++ int pos1 ++ str " character " ++ int pos2) ++ report ()) - | Not_found -> + | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) - | Failure s -> + | Failure s -> hov 0 (str "Failure: " ++ str s ++ report ()) - | Invalid_argument s -> + | Invalid_argument s -> hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) - | Sys.Break -> + | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> - let msg = + let msg = if !Flags.debug (*!Constrextern.print_universes*) then spc() ++ str "(cannot enforce" ++ spc() ++ (*Univ.pr_uni u ++*) spc() ++ str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=") @@ -270,12 +264,12 @@ let rec explain_exn = function else mt() in hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") - | TypeError(ctx,te) -> + | TypeError(ctx,te) -> (* hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *) (* te)*) hov 0 (str "Type error") - | Indtypes.InductiveError e -> + | Indtypes.InductiveError e -> hov 0 (str "Error related to inductive types") (* let ctx = Check.get_env() in hov 0 @@ -286,9 +280,9 @@ let rec explain_exn = function ++ explain_exn exc) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ - (if s <> "" then + (if s <> "" then if Sys.ocaml_version = "3.06" then - (str ("(file \"" ^ s ^ "\", characters ") ++ + (str ("(file \"" ^ s ^ "\", characters ") ++ int b ++ str "-" ++ int e ++ str ")") else (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ @@ -298,13 +292,13 @@ let rec explain_exn = function (mt ())) ++ report ()) | reraise -> - hov 0 (anomaly_string () ++ str "Uncaught exception " ++ + hov 0 (anomaly_string () ++ str "Uncaught exception " ++ str (Printexc.to_string reraise)++report()) -let parse_args() = +let parse_args argv = let rec parse = function | [] -> () - | "-impredicative-set" :: rem -> + | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem @@ -325,7 +319,7 @@ let parse_args() = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -346,8 +340,8 @@ let parse_args() = | s :: rem -> add_compile s; parse rem in try - parse (List.tl (Array.to_list Sys.argv)) - with + parse (List.tl (Array.to_list argv)) + with | UserError(_,s) as e -> begin try Stream.empty s; exit 1 @@ -360,12 +354,12 @@ let parse_args() = (* To prevent from doing the initialization twice *) let initialized = ref false -let init() = +let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) try - parse_args(); + parse_args argv; if_verbose print_header (); init_load_path (); engage (); @@ -376,13 +370,15 @@ let init() = exit 1 end +let init() = init_with_argv Sys.argv + let run () = - try + try compile_files (); flush_all() with e -> (Pp.ppnl(explain_exn e); - flush_all(); + flush_all(); exit 1) let start () = init(); run(); Check_stat.stats(); exit 0 diff --git a/checker/closure.ml b/checker/closure.ml index ccbfbc4c..7ccf06b9 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -38,7 +38,7 @@ let incr_cnt red cnt = if red then begin if !stats then incr cnt; true - end else + end else false let with_stats c = @@ -127,13 +127,13 @@ module RedFlags = (struct { red with r_const = Idpred.remove id l1, l2 } let red_add_transparent red tr = - { red with r_const = tr } + { red with r_const = tr } let mkflags = List.fold_left red_add no_red let red_set red = function | BETA -> incr_cnt red.r_beta beta - | CONST kn -> + | CONST kn -> let (_,l) = red.r_const in let c = Cpred.mem kn l in incr_cnt c delta @@ -165,7 +165,7 @@ 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 unfold_red kn = let flag = match kn with | EvalVarRef id -> fVAR id | EvalConstRef kn -> fCONST kn @@ -187,7 +187,7 @@ let betadeltaiota_red = { r_const = true,[],[]; r_zeta = true; r_evar = true; - r_iota = true } + r_iota = true } let betaiota_red = { r_beta = true; @@ -195,7 +195,7 @@ let betaiota_red = { r_zeta = false; r_evar = false; r_iota = true } - + let beta_red = { r_beta = true; r_const = false,[],[]; @@ -231,7 +231,7 @@ let unfold_red kn = (* 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 + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) type red_kind = @@ -278,7 +278,7 @@ 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] -> + | 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 @@ -339,7 +339,7 @@ type 'a infos = { let info_flags info = info.i_flags let ref_value_cache info ref = - try + try Some (Hashtbl.find info.i_tab ref) with Not_found -> try @@ -360,7 +360,7 @@ let ref_value_cache info ref = let defined_vars flags env = (* if red_local_const (snd flags) then*) - fold_named_context + fold_named_context (fun (id,b,_) e -> match b with | None -> e @@ -370,7 +370,7 @@ let defined_vars flags env = let defined_rels flags env = (* if red_local_const (snd flags) then*) - fold_rel_context + fold_rel_context (fun (id,b,t) (i,subs) -> match b with | None -> (i+1, subs) @@ -380,6 +380,11 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env +let eq_table_key k1 k2 = + match k1,k2 with + | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 + | _,_ -> k1=k2 + let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; @@ -417,8 +422,8 @@ let neutr = function | (Whnf|Norm) -> Whnf | (Red|Cstr) -> Red -type fconstr = { - mutable norm: red_state; +type fconstr = { + mutable norm: red_state; mutable term: fterm } and fterm = @@ -456,7 +461,7 @@ let update v1 (no,t) = else {norm=no;term=t} (**********************************************************************) -(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) type stack_member = | Zapp of fconstr array @@ -496,9 +501,6 @@ let rec decomp_stack = function | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) | _ -> None -let rec decomp_stackn = function - | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s) - | _ -> assert false let array_of_stack s = let rec stackrec = function | [] -> [] @@ -507,7 +509,7 @@ let array_of_stack s = in Array.concat (stackrec s) let rec stack_assign s p c = match s with | Zapp args :: s -> - let q = Array.length args in + let q = Array.length args in if p >= q then Zapp args :: stack_assign s (p-q) c else @@ -515,7 +517,7 @@ let rec stack_assign s p c = match s with nargs.(p) <- c; Zapp nargs :: s) | _ -> s -let rec stack_tail p s = +let rec stack_tail p s = if p = 0 then s else match s with | Zapp args :: s -> @@ -547,8 +549,6 @@ let lift_fconstr k f = if k=0 then f else lft_fconstr k f let lift_fconstr_vect k v = if k=0 then v else Array.map (fun f -> lft_fconstr k f) v -let lift_fconstr_list k l = - if k=0 then l else List.map (fun f -> lft_fconstr k f) l let clos_rel e i = match expand_rel i e with @@ -780,7 +780,7 @@ let term_of_fconstr = (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a - * FCLOS term. + * FCLOS term. let rec fstrong unfreeze_fun lfts v = to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) *) @@ -857,12 +857,6 @@ let get_nth_arg 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 *) -let get_arg h stk = - let (depth,stk') = strip_update_shift h stk in - match decomp_stack stk' with - Some (v, s') -> (Some (depth,v), s') - | None -> (None, zshift depth stk') - let rec get_args n tys f e stk = match stk with Zupdate r :: s -> @@ -979,7 +973,7 @@ let rec knr info m stk = | FLambda(n,tys,f,e) when red_set info.i_flags fBETA -> (match get_args n tys f e stk with Inl e', s -> knit info e' f s - | Inr lam, s -> (lam,s)) + | Inr lam, s -> (lam,s)) | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info (ConstKey kn) with Some v -> kni info v stk diff --git a/checker/closure.mli b/checker/closure.mli index fa302de6..4d302add 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -24,7 +24,7 @@ val with_stats: 'a Lazy.t -> 'a (*s Delta implies all consts (both global (= by [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's. - Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) type transparent_state = Idpred.t * Cpred.t @@ -102,7 +102,7 @@ type fconstr type fterm = | FRel of int | FAtom of constr (* Metas and Sorts *) - | FCast of fconstr * cast_kind * fconstr + | FCast of fconstr * cast_kind * fconstr | FFlex of table_key | FInd of inductive | FConstruct of constructor @@ -177,6 +177,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool +val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/checker/declarations.ml b/checker/declarations.ml index c6a7b4b4..699f6c90 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -30,356 +30,623 @@ let val_cst_type = val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] -type substitution_domain = - MSI of mod_self_id +type substitution_domain = | MBI of mod_bound_id | MPI of module_path let val_subst_dom = - val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|] + val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|] -module Umap = Map.Make(struct +module Umap = Map.Make(struct type t = substitution_domain let compare = Pervasives.compare end) -type resolver -type substitution = (module_path * resolver option) Umap.t +type delta_hint = + Inline of 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 + +let empty_delta_resolver = Deltamap.empty + +type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res = val_opt no_val +let val_res_dom = + val_sum "delta_key" 0 [|[|val_kn|];[|val_mp|]|] + +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 val_subst = val_map ~name:"substitution" val_subst_dom (val_tuple "substition range" [|val_mp;val_res|]) -let fold_subst fs fb fp = +let fold_subst fb fp = Umap.fold (fun k (mp,_) acc -> match k with - MSI msid -> fs msid mp acc | MBI mbid -> fb mbid mp acc | MPI mp1 -> fp mp1 mp acc) let empty_subst = Umap.empty -let add_msid msid mp = - Umap.add (MSI msid) (mp,None) let add_mbid mbid mp = - Umap.add (MBI mbid) (mp,None) + Umap.add (MBI mbid) (mp,empty_delta_resolver) let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,None) + Umap.add (MPI mp1) (mp2,empty_delta_resolver) -let map_msid msid mp = add_msid msid mp empty_subst 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 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" + in + try + sub_mp mp + with + Not_found -> mp + +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 + + +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 + +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 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 + + + +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 [] + +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 + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPself sid -> - let mp',resolve = Umap.find (MSI sid) sub in + | MPfile sid -> + let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve + 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 + end | MPdot (mp1,l) as mp2 -> begin - try + try let mp',resolve = Umap.find (MPI mp2) sub in mp',resolve - with Not_found -> + with Not_found -> let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try - Some (aux mp) + Some (aux mp) with Not_found -> None - - -let subst_mp0 sub mp = (* 's like subst *) - let rec aux mp = - match mp with - | MPself sid -> fst (Umap.find (MSI sid) sub) - | MPbound bid -> fst (Umap.find (MBI bid) sub) - | MPdot (mp1,l) as mp2 -> - begin - try fst (Umap.find (MPI mp2) sub) - with Not_found -> MPdot (aux mp1,l) - end - - | _ -> raise Not_found - in - try Some (aux mp) with Not_found -> None - let subst_mp sub mp = match subst_mp0 sub mp with None -> mp - | Some mp' -> mp' + | Some (mp',_) -> mp' -let subst_kn0 sub kn = +let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with - Some mp' -> - Some (make_kn mp' dir l) - | None -> None + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> kn' + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + make_kn mp' dir l + | None -> kn + +exception No_subst + +type sideconstantsubst = + | User + | Canonical + +let subst_ind 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 + 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 mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> con - | Some mp' -> make_con mp' dir l + 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 subst_con0 sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> None - | Some mp' -> - let con' = make_con mp' dir l in - Some (Const 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 + Some (Const con) + |Canonical -> + let con = constant_of_delta2 resolve con' in + Some (Const con) + end + | t -> t + with No_subst -> Some (Const con) -let rec map_kn f f' c = + +let rec map_kn f f' c = let func = map_kn f f' in match c with - | Const kn -> + | Const kn -> (match f' kn with None -> c | Some const ->const) - | Ind (kn,i) -> + | Ind (kn,i) -> (match f kn with None -> c | Some kn' -> Ind (kn',i)) - | Construct ((kn,i),j) -> + | Construct ((kn,i),j) -> (match f kn with None -> c | Some kn' -> Construct ((kn',i),j)) - | Case (ci,p,ct,l) -> + | 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 p' = func p in let ct' = func ct in let l' = array_smartmap func l in - if (ci.ci_ind==ci_ind && p'==p + if (ci.ci_ind==ci_ind && p'==p && l'==l && ct'==ct)then c - else + else Case ({ci with ci_ind = ci_ind}, - p',ct', l') - | Cast (ct,k,t) -> + p',ct', l') + | Cast (ct,k,t) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else Cast (ct', k, t') - | Prod (na,t,ct) -> + | Prod (na,t,ct) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else Prod (na, t', ct') - | Lambda (na,t,ct) -> + | Lambda (na,t,ct) -> let ct' = func ct in let t'= func t in - if (t'==t && ct'==ct) then c + if (t'==t && ct'==ct) then c else Lambda (na, t', ct') - | LetIn (na,b,t,ct) -> + | LetIn (na,b,t,ct) -> let ct' = func ct in let t'= func t in let b'= func b in - if (t'==t && ct'==ct && b==b') then c + if (t'==t && ct'==ct && b==b') then c else LetIn (na, b', t', ct') - | App (ct,l) -> + | App (ct,l) -> let ct' = func ct in let l' = array_smartmap func l in if (ct'== ct && l'==l) then c else App (ct',l') - | Evar (e,l) -> + | Evar (e,l) -> let l' = array_smartmap func l in if (l'==l) then c else Evar (e,l') | Fix (ln,(lna,tl,bl)) -> let tl' = array_smartmap func tl in let bl' = array_smartmap func bl in - if (bl == bl'&& tl == tl') then c + if (bl == bl'&& tl == tl') then c else Fix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> let tl' = array_smartmap func tl in let bl' = array_smartmap func bl in - if (bl == bl'&& tl == tl') then c + if (bl == bl'&& tl == tl') then c else CoFix (ln,(lna,tl',bl')) | _ -> c -let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) +let subst_mps sub = + map_kn (subst_mind0 sub) (subst_con0 sub) + + +type 'a lazy_subst = + | LSval of 'a + | LSlazy of substitution list * 'a + +type 'a substituted = 'a lazy_subst ref + +let val_substituted val_a = + val_ref + (val_sum "constr_substituted" 0 + [|[|val_a|];[|val_list val_subst;val_a|]|]) +let from_val a = ref (LSval a) + let rec replace_mp_in_mp mpfrom mpto mp = match mp with | _ when mp = mpfrom -> mpto - | MPdot (mp1,l) -> + | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1==mp1' then mp else MPdot (mp1',l) | _ -> mp -let replace_mp_in_con mpfrom mpto kn = - let mp,dir,l = kn in - let mp'' = replace_mp_in_mp mpfrom mpto mp in - if mp==mp'' then kn - else (mp'', dir, l) - -type 'a lazy_subst = - | LSval of 'a - | LSlazy of substitution * 'a +let rec mp_in_mp mp mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_in_mp mp mp2 + | _ -> false -type 'a substituted = 'a lazy_subst ref - -let from_val a = ref (LSval a) - -let force fsubst r = - match !r with - | LSval a -> a - | LSlazy(s,a) -> - let a' = fsubst s a in - r := LSval a'; - a' - - - -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - let subst = Umap.mapi (apply_subst subst2) subst1 in - (Umap.fold Umap.add subst2 subst) - -let subst_key subst1 subst2 = - let replace_in_key key mp sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst1 mp1 with - | None -> None - | Some mp2 -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key mp sub - | Some mpi -> Umap.add mpi mp sub +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 in - Umap.fold replace_in_key subst2 empty_subst - -let update_subst_alias subst1 subst2 = - let subst_inv key (mp,_) sub = - let newmp = - match key with - | MBI msid -> Some (MPbound msid) - | MSI msid -> Some (MPself msid) - | _ -> None - in - match newmp with - | None -> sub - | Some mpi -> match mp with - | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub - | MPself msid -> Umap.add (MSI msid) (mpi,None) sub - | _ -> Umap.add (MPI mp) (mpi,None) sub - in - let subst_mbi = Umap.fold subst_inv subst2 empty_subst in - let alias_subst key (mp,_) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst_mbi mp1 with - | None -> None - | Some mp2 -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,None) sub - | Some mpi -> Umap.add mpi (mp,None) sub + Deltamap.fold prefixmp 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 in - Umap.fold alias_subst subst1 empty_subst - -let join_alias (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - Umap.mapi (apply_subst subst2) subst1 - - -let update_subst subst1 subst2 = - let subst_inv key (mp,_) l = - let newmp = - match key with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - match mp with - | MPbound mbid -> ((MBI mbid),newmp)::l - | MPself msid -> ((MSI msid),newmp)::l - | _ -> ((MPI mp),newmp)::l - in - let subst_mbi = Umap.fold subst_inv subst2 [] in - let alias_subst key (mp,_) sub= - let newsetkey = - match key with - | MPI mp1 -> - let compute_set_newkey l (k,mp') = - let mp_from_key = match k with - | MBI msid -> MPbound msid - | MSI msid -> MPself msid - | MPI mp -> mp - in - let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1)::l - in - begin - match List.fold_left compute_set_newkey [] subst_mbi with - | [] -> None - | l -> Some (l) - end - | _ -> None + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_mp_delta sub mp key= + match subst_mp0 sub mp with + None -> empty_delta_resolver,mp + | 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 + in + Deltamap.fold apply_subst resolver empty_delta_resolver + +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 - match newsetkey with - | None -> sub - | Some l -> - List.fold_left (fun s k -> Umap.add k (mp,None) s) - sub l + Deltamap.fold apply_res resolver1 empty_delta_resolver + +let add_delta_resolver resolver1 resolver2 = + if resolver1 == resolver2 then + resolver2 + else + Deltamap.fold Deltamap.add (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 in - Umap.fold alias_subst subst1 empty_subst + Umap.fold prefixmp subst empty_subst +let join (subst1 : substitution) (subst2 : substitution) = + let apply_subst key (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 = + match resolve' with + Some res -> + add_delta_resolver + (subst_dom_codom_delta_resolver subst2 resolve) res + | 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 force fsubst r = + match !r with + | LSval a -> a + | LSlazy(s,a) -> + let subst = List.fold_left join empty_subst (List.rev s) in + let a' = fsubst subst a in + r := LSval a'; + a' let subst_substituted s r = match !r with - | LSval a -> ref (LSlazy(s,a)) + | LSval a -> ref (LSlazy([s],a)) | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) + ref (LSlazy(s::s',a)) -let force_constr = force subst_mps +let force_constr = force subst_mps type constr_substituted = constr substituted -let val_cstr_subst = - val_ref - (val_sum "constr_substituted" 0 - [|[|val_constr|];[|val_subst;val_constr|]|]) +let val_cstr_subst = val_substituted val_constr let subst_constr_subst = subst_substituted @@ -390,12 +657,17 @@ type constant_body = { const_body_code : to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : Univ.constraints; - const_opaque : bool; + const_opaque : bool; const_inline : bool} let val_cb = val_tuple "constant_body" - [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs; - val_bool; val_bool |] + [|val_nctxt; + val_opt val_cstr_subst; + val_cst_type; + no_val; + val_cstrs; + val_bool; + val_bool |] let subst_rel_declaration sub (id,copt,t as x) = @@ -405,21 +677,21 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) -type recarg = - | Norec - | Mrec of int +type recarg = + | Norec + | Mrec of int | Imbr of inductive let val_recarg = val_sum "recarg" 1 (* Norec *) [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|] let subst_recarg sub r = match r with | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_kn sub kn in + | 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 let val_wfp = val_rec_sum "wf_paths" 0 - (fun val_wfp -> + (fun val_wfp -> [|[|val_int;val_int|]; (* Rtree.Param *) [|val_recarg;val_array val_wfp|]; (* Rtree.Node *) [|val_int;val_array val_wfp|] (* Rtree.Rec *) @@ -454,7 +726,7 @@ type monomorphic_inductive_arity = { let val_mono_ind_arity = val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|] -type inductive_arity = +type inductive_arity = | Monomorphic of monomorphic_inductive_arity | Polymorphic of polymorphic_arity let val_ind_arity = val_sum "inductive_arity" 0 @@ -486,6 +758,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; @@ -506,13 +781,13 @@ type one_inductive_body = { (* number of no constant constructor *) mind_nb_args : int; - mind_reloc_tbl : reloc_table; + mind_reloc_tbl : reloc_table; } let val_one_ind = val_tuple "one_inductive_body" [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr; - val_int; val_list val_sortfam;val_array val_constr;val_array val_int; - val_wfp; val_int; val_int; no_val|] + val_int;val_int;val_list val_sortfam;val_array val_constr;val_array val_int; + val_wfp;val_int;val_int;no_val|] type mutual_inductive_body = { @@ -544,12 +819,10 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } let val_ind_pack = val_tuple "mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; - val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|] + val_int; val_int; val_rctxt;val_cstrs|] let subst_arity sub = function @@ -565,7 +838,7 @@ let subst_const_body sub cb = { (*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_inline = cb.const_inline} let subst_arity sub = function | Monomorphic s -> @@ -575,152 +848,158 @@ let subst_arity sub = function } | Polymorphic s as x -> x -let subst_mind_packet sub mbp = +let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_arity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; + mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; - mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind sub mib = - { mind_record = mib.mind_record ; +let subst_mind sub mib = + { mind_record = mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (assert (mib.mind_hyps=[]); []) ; mind_nparams = mib.mind_nparams; mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = + mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints ; - mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } + mind_constraints = mib.mind_constraints } (* Modules *) (* Whenever you change these types, please do update the validation functions below *) -type structure_field_body = +type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * Univ.constraints + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * - struct_expr_body option * Univ.constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body - -and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + +and module_body = + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : Univ.constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : action list} -and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} +and module_type_body = + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + typ_delta :delta_resolver} (* the validation functions: *) let rec val_sfb o = val_sum "struct_field_body" 0 [|[|val_cb|]; (* SFBconst *) [|val_ind_pack|]; (* SFBmind *) [|val_module|]; (* SFBmodule *) - [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *) [|val_modtype|] (* SFBmodtype *) |] o and val_sb o = val_list (val_tuple"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 *) - [|val_uid;val_sb|]; (* SEBstruct *) [|val_seb;val_seb;val_cstrs|]; (* SEBapply *) + [|val_sb|]; (* SEBstruct *) [|val_seb;val_with|] (* SEBwith *) |] o and val_with o = val_sum "with_declaration_body" 0 - [|[|val_list val_id;val_mp;val_cstrs|]; + [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o and val_module o = val_tuple "module_body" - [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o + [|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" - [|val_seb;val_opt val_mp;val_subst|] o + [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o + - let rec subst_with_body sub = function - | With_module_body(id,mp,typ_opt,cst) -> - With_module_body(id,subst_mp sub mp, - Option.smartmap (subst_struct_expr sub) typ_opt,cst) + | With_module_body(id,mp) -> + With_module_body(id,subst_mp sub mp) | With_definition_body(id,cb) -> With_definition_body( id,subst_const_body sub cb) -and subst_modtype sub mtb = +and subst_modtype sub mtb= let typ_expr' = subst_struct_expr sub mtb.typ_expr in - if typ_expr'==mtb.typ_expr then - mtb + let typ_alg' = + Option.smartmap + (subst_struct_expr sub) mtb.typ_expr_alg in + let mp = subst_mp sub mtb.typ_mp + in + if typ_expr'==mtb.typ_expr && + typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then + mtb else - { mtb with - typ_expr = typ_expr'} - + {mtb with + typ_mp = mp; + typ_expr = typ_expr'; + typ_expr_alg = typ_alg'} + and subst_structure sub sign = - let subst_body = function + let subst_body = function SFBconst cb -> SFBconst (subst_const_body sub cb) | SFBmind mib -> SFBmind (subst_mind sub mib) | SFBmodule mb -> - SFBmodule (subst_module sub mb) + SFBmodule (subst_module sub mb) | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,typ_opt ,cst) -> - SFBalias (subst_mp sub mp,Option.smartmap (subst_struct_expr sub) typ_opt,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = - let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in - (* This is similar to the previous case. In this case we have - a module M in a signature that is knows to be equivalent to a module M' - (because the signature is "K with Module M := M'") and we are substituting - M' with some M''. *) - let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in - let mb_alias = join_alias mb.mod_alias sub in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mb_alias == mb.mod_alias - then mb else - { mod_expr = me'; - mod_type=mtb'; - mod_constraints=mb.mod_constraints; - mod_alias = mb_alias; - mod_retroknowledge=mb.mod_retroknowledge} +and subst_module sub mb = + let mtb' = subst_struct_expr sub mb.mod_type in + let typ_alg' = Option.smartmap + (subst_struct_expr sub ) mb.mod_type_alg in + let me' = Option.smartmap + (subst_struct_expr sub) mb.mod_expr in + let mp = subst_mp sub mb.mod_mp in + if mtb'==mb.mod_type && mb.mod_expr == me' + && mp == mb.mod_mp + then mb else + { mb with + mod_mp = mp; + mod_expr = me'; + mod_type_alg = typ_alg'; + mod_type=mtb'} and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (msid, mtb, meb') -> - SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') - | SEBstruct (msid,str)-> - SEBstruct(msid, subst_structure sub str) + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (mbid, mtb, meb') -> + SEBfunctor(mbid,subst_modtype sub mtb + ,subst_struct_expr sub meb') + | SEBstruct (str)-> + SEBstruct( subst_structure sub str) | SEBapply (meb1,meb2,cst)-> SEBapply(subst_struct_expr sub meb1, subst_struct_expr sub meb2, @@ -728,7 +1007,5 @@ and subst_struct_expr sub = function | SEBwith (meb,wdb)-> SEBwith(subst_struct_expr sub meb, subst_with_body sub wdb) - -let subst_signature_msid msid mp = - subst_structure (map_msid msid mp) + diff --git a/checker/declarations.mli b/checker/declarations.mli index d71e625f..b39fd6f2 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -25,7 +25,7 @@ type constant_type = | NonPolymorphicType of constr | PolymorphicArity of rel_context * polymorphic_arity -type constr_substituted +type constr_substituted val force_constr : constr_substituted -> constr val from_val : constr -> constr_substituted @@ -35,14 +35,14 @@ type constant_body = { const_type : constant_type; const_body_code : to_patch_substituted; const_constraints : Univ.constraints; - const_opaque : bool; + const_opaque : bool; const_inline : bool} (* Mutual inductives *) -type recarg = - | Norec - | Mrec of int +type recarg = + | Norec + | Mrec of int | Imbr of inductive type wf_paths = recarg Rtree.t @@ -56,7 +56,7 @@ type monomorphic_inductive_arity = { mind_sort : sorts; } -type inductive_arity = +type inductive_arity = | Monomorphic of monomorphic_inductive_arity | Polymorphic of polymorphic_arity @@ -86,6 +86,9 @@ type one_inductive_body = { (* Number of expected real arguments of the type (no let, no params) *) mind_nrealargs : int; + (* Length of realargs context (with let, no params) *) + mind_nrealargs_ctxt : int; + (* List of allowed elimination sorts *) mind_kelim : sorts_family list; @@ -106,7 +109,7 @@ type one_inductive_body = { (* number of no constant constructor *) mind_nb_args : int; - mind_reloc_tbl : reloc_table; + mind_reloc_tbl : reloc_table; } type mutual_inductive_body = { @@ -138,53 +141,52 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } (* Modules *) type substitution +type delta_resolver +val empty_delta_resolver : delta_resolver -type structure_field_body = +type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option - * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * Univ.constraints + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * - struct_expr_body option * Univ.constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body - -and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + +and module_body = + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : Univ.constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : action list} -and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} +and module_type_body = + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + typ_delta :delta_resolver} (* Substitutions *) val fold_subst : - (mod_self_id -> module_path -> 'a -> 'a) -> (mod_bound_id -> module_path -> 'a -> 'a) -> (module_path -> module_path -> 'a -> 'a) -> substitution -> 'a -> 'a @@ -192,26 +194,21 @@ val fold_subst : type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_msid : mod_self_id -> module_path -> substitution -> substitution val add_mbid : mod_bound_id -> module_path -> substitution -> substitution val add_mp : module_path -> module_path -> substitution -> substitution -val map_msid : mod_self_id -> module_path -> substitution val map_mbid : mod_bound_id -> module_path -> substitution val map_mp : module_path -> module_path -> substitution +val mp_in_delta : module_path -> delta_resolver -> bool +val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun val subst_modtype : substitution -> module_type_body -> module_type_body val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body val subst_structure : substitution -> structure_body -> structure_body -val subst_signature_msid : - mod_self_id -> module_path -> structure_body -> structure_body +val subst_module : substitution -> module_body -> module_body val join : substitution -> substitution -> substitution -val join_alias : substitution -> substitution -> substitution -val update_subst_alias : substitution -> substitution -> substitution -val update_subst : substitution -> substitution -> substitution -val subst_key : substitution -> substitution -> substitution (* Validation *) val val_eng : Obj.t -> unit diff --git a/checker/environ.ml b/checker/environ.ml index 4bdbeee6..a72aae91 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -5,11 +5,11 @@ open Term open Declarations type globals = { - env_constants : constant_body Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_body Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; + env_inductives_eq : kernel_name KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; @@ -25,11 +25,11 @@ type env = { let empty_env = { env_globals = - { env_constants = Cmap.empty; - env_inductives = KNmap.empty; + { env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_inductives_eq = KNmap.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty; - env_alias = MPmap.empty }; + env_modtypes = MPmap.empty}; env_named_context = []; env_rel_context = []; env_stratification = @@ -71,17 +71,17 @@ let push_rel d env = env_rel_context = d :: env.env_rel_context } let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x - + let push_rec_types (lna,typarray,_) env = let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Named context *) -let push_named d env = +let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) - { env with + { env with env_named_context = d :: env.env_named_context } let lookup_named id env = @@ -98,30 +98,30 @@ let named_type id env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then - env + if c == Constraint.empty then + env else let s = env.env_stratification in - { env with env_stratification = + { env with env_stratification = { s with env_universes = merge_constraints c s.env_universes } } (* Global constants *) let lookup_constant kn env = - Cmap.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.env_constants let add_constant kn cs env = - let new_constants = - Cmap.add kn cs env.env_globals.env_constants in - let new_globals = - { env.env_globals with - env_constants = new_constants } in + let new_constants = + Cmap_env.add kn cs env.env_globals.env_constants in + let new_globals = + { env.env_globals with + 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 + cb.const_type type const_evaluation_result = NoBody | Opaque @@ -144,60 +144,53 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false (* Mutual Inductives *) -let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives +let scrape_mind env kn= + try + KNmap.find kn env.env_globals.env_inductives_eq + with + Not_found -> kn + +let mind_equiv env (kn1,i1) (kn2,i2) = + i1 = i2 && + scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2) -let rec scrape_mind env kn = - match (lookup_mind kn env).mind_equiv with - | None -> kn - | Some kn' -> scrape_mind env kn' + +let lookup_mind kn env = + Mindmap_env.find kn env.env_globals.env_inductives let add_mind kn mib env = - let new_inds = KNmap.add kn mib env.env_globals.env_inductives in - let new_globals = - { env.env_globals with - env_inductives = new_inds } in + let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in + let kn1,kn2 = user_mind kn,canonical_mind kn in + let new_inds_eq = if kn1=kn2 then + env.env_globals.env_inductives_eq + else + KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in + let new_globals = + { env.env_globals with + env_inductives = new_inds; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } -let rec mind_equiv env (kn1,i1) (kn2,i2) = - let rec equiv kn1 kn2 = - kn1 = kn2 || - scrape_mind env kn1 = scrape_mind env kn2 in - i1 = i2 && equiv kn1 kn2 - (* Modules *) -let add_modtype ln mtb env = +let add_modtype ln mtb env = let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in - let new_globals = - { env.env_globals with + let new_globals = + { env.env_globals with env_modtypes = new_modtypes } in { env with env_globals = new_globals } -let shallow_add_module mp mb env = +let shallow_add_module mp mb env = let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = - { env.env_globals with + let new_globals = + { env.env_globals with env_modules = new_mods } in { env with env_globals = new_globals } -let register_alias mp1 mp2 env = - let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in - let new_globals = - { env.env_globals with - env_alias = new_alias } in - { env with env_globals = new_globals } - -let rec scrape_alias mp env = - try - let mp1 = MPmap.find mp env.env_globals.env_alias in - scrape_alias mp1 env - with - Not_found -> mp -let lookup_module mp env = +let lookup_module mp env = MPmap.find mp env.env_globals.env_modules -let lookup_modtype ln env = +let lookup_modtype ln env = MPmap.find ln env.env_globals.env_modtypes diff --git a/checker/environ.mli b/checker/environ.mli index 1541bf0d..023acd0b 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -4,12 +4,11 @@ open Term (* Environments *) type globals = { - env_constants : Declarations.constant_body Cmap.t; - env_inductives : Declarations.mutual_inductive_body KNmap.t; + env_constants : Declarations.constant_body Cmap_env.t; + env_inductives : Declarations.mutual_inductive_body Mindmap_env.t; + env_inductives_eq : kernel_name KNmap.t; env_modules : Declarations.module_body MPmap.t; - env_modtypes : Declarations.module_type_body MPmap.t; - env_alias : module_path MPmap.t; -} + env_modtypes : Declarations.module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; env_engagement : Declarations.engagement option; @@ -59,19 +58,18 @@ val constant_opt_value : env -> constant -> constr option val evaluable_constant : constant -> env -> bool (* Inductives *) +val mind_equiv : env -> inductive -> inductive -> bool + val lookup_mind : mutual_inductive -> env -> Declarations.mutual_inductive_body -val scrape_mind : env -> mutual_inductive -> mutual_inductive + val add_mind : mutual_inductive -> Declarations.mutual_inductive_body -> env -> env -val mind_equiv : env -> inductive -> inductive -> bool (* Modules *) val add_modtype : module_path -> Declarations.module_type_body -> env -> env val shallow_add_module : module_path -> Declarations.module_body -> env -> env -val register_alias : module_path -> module_path -> env -> env -val scrape_alias : module_path -> env -> module_path val lookup_module : module_path -> env -> Declarations.module_body val lookup_modtype : module_path -> env -> Declarations.module_type_body diff --git a/checker/include b/checker/include index 331eb45c..b7d46d4b 100644 --- a/checker/include +++ b/checker/include @@ -8,20 +8,26 @@ (mainly run_l and norec). *) -#cd ".." +#cd "..";; #directory "lib";; #directory "kernel";; #directory "checker";; +#directory "+camlp4";; +#directory "+camlp5";; #load "unix.cma";; #load "str.cma";; #load "gramlib.cma";; +(*#load "toplevellib.cma";; + +#directory "/usr/lib/ocaml/compiler-libs/utils";; +let _ = Clflags.recursive_types:=true;; +*) #load "check.cma";; open Typeops;; open Check;; - open Pp;; open Util;; open Names;; @@ -70,10 +76,11 @@ let prenv e = pp pe;; *) +(* let prsub s = let string_of_mp mp = let s = string_of_mp mp in - (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in + (match mp with MPbound _ -> "#bound."|_->"")^s in pp (hv 0 (fold_subst (fun msid mp strm -> @@ -86,6 +93,7 @@ let prsub s = str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++ str (string_of_mp mp) ++ fnl() ++ strm) s (mt()))) ;; +*) #install_printer prid;; #install_printer prcon;; @@ -100,10 +108,10 @@ let prsub s = #install_printer prcstrs;; (*#install_printer prus;;*) (*#install_printer prenv;;*) -(*#install_printer prenvu;;*) -#install_printer prsub;; +(*#install_printer prenvu;; +#install_printer prsub;;*) -Checker.init();; +Checker.init_with_argv [|""|];; Flags.make_silent false;; Flags.debug := true;; Sys.catch_break true;; @@ -114,7 +122,7 @@ let module_of_file f = ;; let mod_access m fld = match m.mod_expr with - Some(SEBstruct(msid,l)) -> List.assoc fld l + Some(SEBstruct l) -> List.assoc fld l | _ -> failwith "bad structure type" ;; @@ -153,7 +161,7 @@ let read_mod s f = engagement option);; let deref_mod md s = - let (Some (SEBstruct(msid,l))) = md.mod_expr in + let (Some (SEBstruct l)) = md.mod_expr in List.assoc (label_of_id(id_of_string s)) l ;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 4c9b3d61..de57c50a 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -22,13 +22,11 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPself uid -> "self("^string_of_msid uid^")" - | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l + | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_mbid uid - | MPself uid -> string_of_msid uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l let string_of_mp mp = @@ -38,8 +36,9 @@ let prkn kn = let (mp,_,l) = repr_kn kn in str(string_of_mp mp ^ "." ^ string_of_label l) let prcon c = - let (mp,_,l) = repr_con c in - str(string_of_mp mp ^ "." ^ string_of_label l) + let ck = canonical_con c in + let uk = user_con c in + if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. Could be refined more... *) @@ -119,23 +118,24 @@ let is_small_constr infos = List.for_all (fun s -> is_small_sort s) infos let is_logic_constr infos = List.for_all (fun s -> is_logic_sort s) infos (* An inductive definition is a "unit" if it has only one constructor - and that all arguments expected by this constructor are - logical, this is the case for equality, conjunction of logical properties + and that all arguments expected by this constructor are + logical, this is the case for equality, conjunction of logical properties *) let is_unit constrsinfos = match constrsinfos with (* One info = One constructor *) - | [|constrinfos|] -> is_logic_constr constrinfos + | [|constrinfos|] -> is_logic_constr constrinfos | [||] -> (* type without constructors *) true | _ -> false let small_unit constrsinfos = - let issmall = array_for_all is_small_constr constrsinfos + let issmall = array_for_all is_small_constr constrsinfos and isunit = is_unit constrsinfos in issmall, isunit (* check information related to inductive arity *) let typecheck_arity env params inds = let nparamargs = rel_context_nhyps params in + let nparamdecls = rel_context_length params in let check_arity arctxt = function Monomorphic mar -> let ar = mar.mind_user_arity in @@ -154,8 +154,12 @@ let typecheck_arity env params inds = (* Arities (with params) are typed-checked here *) let arity = check_arity ar_ctxt ind.mind_arity in (* mind_nrealargs *) - if ind.mind_nrealargs <> rel_context_nhyps ar_ctxt - nparamargs then + let nrealargs = rel_context_nhyps ar_ctxt - nparamargs in + if ind.mind_nrealargs <> nrealargs then failwith "bad number of real inductive arguments"; + let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in + if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then + failwith "bad length of real inductive arguments signature"; (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, full_arity is used as argument or subject to cast, an @@ -273,20 +277,20 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err ntyp env0 nbpar c err = +let explain_ind_err ntyp env0 nbpar c err = let (lpar,c') = mind_extract_params nbpar c in let env = push_rel_context lpar env0 in match err with - | LocalNonPos kt -> + | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',Rel (kt+nbpar)))) - | LocalNotEnoughArgs kt -> - raise (InductiveError + | LocalNotEnoughArgs kt -> + raise (InductiveError (NotEnoughArgs (env,c',Rel (kt+nbpar)))) | LocalNotConstructor -> - raise (InductiveError + raise (InductiveError (NotConstructor (env,c',Rel (ntyp+nbpar)))) | LocalNonPar (n,l) -> - raise (InductiveError + raise (InductiveError (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) let failwith_non_pos n ntypes c = @@ -307,7 +311,7 @@ let failwith_non_pos_list n ntypes l = let check_correct_par (env,n,ntypes,_) hyps l largs = let nparams = rel_context_nhyps hyps in let largs = Array.of_list largs in - if Array.length largs < nparams then + if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); let (lpar,largs') = array_chop nparams largs in let nhyps = List.length hyps in @@ -319,18 +323,18 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | Rel w when w = index -> check (k-1) (index+1) hyps | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) in check (nparams-1) (n-nhyps) hyps; - if not (array_for_all (noccur_between n ntypes) largs') then + if not (array_for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' (* Arguments of constructor: check the number of recursive parameters nrecp. - the first parameters which are constant in recursive arguments - n is the current depth, nmr is the maximum number of possible + the first parameters which are constant in recursive arguments + n is the current depth, nmr is the maximum number of possible recursive parameters *) -let check_rec_par (env,n,_,_) hyps nrecp largs = +let check_rec_par (env,n,_,_) hyps nrecp largs = let (lpar,_) = list_chop nrecp largs in - let rec find index = - function + let rec find index = + function | ([],_) -> () | (_,[]) -> failwith "number of recursive parameters cannot be greater than the number of parameters." @@ -347,14 +351,14 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) -let abstract_mind_lc env ntyps npars lc = - if npars = 0 then +let abstract_mind_lc env ntyps npars lc = + if npars = 0 then lc - else - let make_abs = + else + let make_abs = list_tabulate - (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps - in + (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps + in Array.map (substl make_abs) lc (* [env] is the typing environment @@ -362,7 +366,7 @@ let abstract_mind_lc env ntyps npars lc = [ntypes] is the number of inductive types in the definition (i.e. range of inductives is [n; n+ntypes-1]) [lra] is the list of recursive tree of each variable - *) + *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) @@ -372,7 +376,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let env' = push_rel (Anonymous,None, hnf_prod_applist env (type_of_inductive env specif) lpar) env in - let ra_env' = + let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in (* New index of the inductive types *) @@ -384,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i 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 = + let rec check_pos (env, n, ntypes, ra_env as ienv) c = let x,largs = decompose_app (whd_betadeltaiota env c) in match x with | Prod (na,b,d) -> @@ -395,7 +399,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = check_pos (ienv_push_var ienv (na, b, mk_norec)) d) | Rel k -> (try - let (ra,rarg) = List.nth ra_env (k-1) in + let (ra,rarg) = List.nth ra_env (k-1) in (match ra with Mrec _ -> check_rec_par ienv hyps nrecp largs | _ -> ()); @@ -408,9 +412,9 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = parameter, then we have an imbricated type *) if List.for_all (noccur_between n ntypes) largs then mk_norec else check_positive_imbr ienv (ind_kn, largs) - | err -> + | err -> if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + List.for_all (noccur_between n ntypes) largs then mk_norec else failwith_non_pos_list n ntypes (x::largs) @@ -419,14 +423,14 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mib.mind_nparams_rec in let (lpar,auxlargs) = - try list_chop auxnpar largs - with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in + try list_chop auxnpar largs + with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in (* If the inductive appears in the args (non params) then the definition is not positive. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then raise (IllFormedInd (LocalNonPos n)); (* We do not deal with imbricated mutual inductive types *) - let auxntyp = mib.mind_ntypes in + let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in @@ -435,30 +439,30 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in (* Parameters expressed in env' *) let lpar' = List.map (lift auxntyp) lpar in - let irecargs = + let irecargs = (* fails if the inductive type occurs non positively *) - (* when substituted *) - Array.map - (function c -> - let c' = hnf_prod_applist env' c lpar' in - check_constructors ienv' false c') - auxlcvect in + (* when substituted *) + Array.map + (function c -> + let c' = hnf_prod_applist env' c lpar' in + check_constructors ienv' false c') + auxlcvect in (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) - + (* check the inductive types occur positively in the products of C, if check_head=true, also check the head corresponds to a constructor of - the ith type *) - - and check_constructors ienv check_head c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = + the ith type *) + + and check_constructors ienv check_head c = + let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = let x,largs = decompose_app (whd_betadeltaiota env c) in match x with - | Prod (na,b,d) -> + | Prod (na,b,d) -> assert (largs = []); - let recarg = check_pos ienv b in + let recarg = check_pos ienv b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' (recarg::lrec) d - + | hd -> if check_head then if hd = Rel (n+ntypes-i-1) then @@ -477,7 +481,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = let _,rawc = mind_extract_params lparams c in try check_constructors ienv true rawc - with IllFormedInd err -> + with IllFormedInd err -> explain_ind_err (ntypes-i) env lparams c err) indlc in mk_paths (Mrec i) irecargs @@ -500,9 +504,9 @@ let check_positivity env_ar params nrecp inds = 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 i mip.mind_nf_lc in - let irecargs = Array.mapi check_one inds in + let irecargs = Array.mapi check_one inds in let wfp = Rtree.mk_rec irecargs in array_iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp @@ -510,7 +514,7 @@ let check_positivity env_ar params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose msgnl (str " checking ind: " ++ prkn kn); + Flags.if_verbose msgnl (str " checking ind: " ++ pr_mind kn); (* check mind_constraints: should be consistent with env *) let env = add_constraints mib.mind_constraints env in (* check mind_record : TODO ? check #constructor = 1 ? *) @@ -535,8 +539,6 @@ let check_inductive env kn mib = (* check mind_nparams_rec: positivity condition *) check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) - if mib.mind_equiv <> None then - msg_warning (str"TODO: mind_equiv not checked"); (* Now we can add the inductive *) add_mind kn mib env diff --git a/checker/inductive.ml b/checker/inductive.ml index 05ab5a84..19c7a6cf 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams (* inductives *) let ind_subst mind mib = let ntypes = mib.mind_ntypes in - let make_Ik k = Ind (mind,ntypes-k-1) in + let make_Ik k = Ind (mind,ntypes-k-1) in list_tabulate make_Ik ntypes (* Instantiate inductives in constructor type *) @@ -67,7 +67,7 @@ let constructor_instantiate mind mib c = substl s c let instantiate_params full t args sign = - let fail () = + let fail () = anomaly "instantiate_params: type, ctxt and args mismatch" in let (rem_args, subs, ty) = fold_rel_context @@ -78,7 +78,7 @@ let instantiate_params full t args sign = | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) sign - ~init:(args,[],t) + ~init:(args,[],t) in if rem_args <> [] then fail(); substl subs ty @@ -104,11 +104,11 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = 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: I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a) -uniformargs : utyps +uniformargs : utyps otherargs : otyps I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj s'_k = max(..s_kj..) @@ -221,7 +221,7 @@ let type_of_constructor cstr (mib,mip) = if i > nconstr then error "Not enough constructors in the type"; constructor_instantiate (fst ind) mib specif.(i-1) -let arities_of_specif kn (mib,mip) = +let arities_of_specif kn (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn mib) specif @@ -241,7 +241,7 @@ let error_elim_expln kp ki = let inductive_sort_family mip = match mip.mind_arity with - | Monomorphic s -> family_of_sort s.mind_sort + | Monomorphic s -> family_of_sort s.mind_sort | Polymorphic _ -> InType let mind_arity mip = @@ -253,26 +253,30 @@ let get_instantiated_arity (mib,mip) params = let elim_sorts (_,mip) = mip.mind_kelim -let rel_list n m = - let rec reln l p = - if p>m then l else reln (Rel(n+p)::l) (p+1) - in - reln [] 1 +let extended_rel_list n hyps = + let rec reln l p = function + | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | [] -> l + in + reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let nrealargs = mip.mind_nrealargs in - applist - (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + applist + (Ind ind, + List.map (lift mip.mind_nrealargs_ctxt) params + @ extended_rel_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option let check_allowed_sort ksort specif = - if not (List.exists ((=) ksort) (elim_sorts specif)) then + if not (List.exists ((=) ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_expln ksort s))) -let is_correct_arity env c (p,pj) ind specif params = +let is_correct_arity env c (p,pj) ind specif params = let arsign,_ = get_instantiated_arity specif params in let rec srec env pt ar = let pt' = whd_betadeltaiota env pt in @@ -283,9 +287,9 @@ let is_correct_arity env c (p,pj) ind specif params = srec (push_rel (na1,None,a1) env) t ar' | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *) let ksort = match (whd_betadeltaiota env a2) with - | Sort s -> family_of_sort s + | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in + let dep_ind = build_dependent_inductive ind specif params in (try conv env a1 dep_ind with NotConvertible -> raise (LocalArity None)); check_allowed_sort ksort specif; @@ -295,7 +299,7 @@ let is_correct_arity env c (p,pj) ind specif params = false | _ -> raise (LocalArity None) - in + in try srec env pj (List.rev arsign) with LocalArity kinds -> error_elim_arity env ind (elim_sorts specif) c (p,pj) kinds @@ -332,7 +336,7 @@ let build_case_type dep p c realargs = beta_appvect p (Array.of_list args) let type_case_branches env (ind,largs) (p,pj) c = - let specif = lookup_mind_specif env ind in + let specif = lookup_mind_specif env ind in let nparams = inductive_params specif in let (params,realargs) = list_chop nparams largs in let dep = is_correct_arity env c (p,pj) ind specif params in @@ -347,7 +351,7 @@ let type_case_branches env (ind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (mind_equiv env indsp ci.ci_ind) or + not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) @@ -357,7 +361,7 @@ let check_case_info env indsp ci = (* Guard conditions for fix and cofix-points *) -(* Check if t is a subterm of Rel n, and gives its specification, +(* Check if t is a subterm of Rel n, and gives its specification, assuming lst already gives index of subterms with corresponding specifications of recursive arguments *) @@ -415,7 +419,7 @@ let subterm_spec_glb = (* branches do not return objects with same spec *) else Not_subterm in Array.fold_left glb2 Dead_code - + type guard_env = { env : env; (* dB of last fixpoint *) @@ -439,7 +443,7 @@ let make_renv env minds recarg (kn,tyi) = genv = [Subterm(Large,mind_recvec.(tyi))] } let push_var renv (x,ty,spec) = - { renv with + { renv with env = push_rel (x,None,ty) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -451,7 +455,7 @@ let push_var_renv renv (x,ty) = push_var renv (x,ty,Not_subterm) (* Fetch recursive information about a variable p *) -let subterm_var p renv = +let subterm_var p renv = try List.nth renv.genv (p-1) with Failure _ | Invalid_argument _ -> Not_subterm @@ -461,7 +465,7 @@ let add_subterm renv (x,a,spec) = let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in - { renv with + { renv with env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> Not_subterm::ge) n renv.genv } @@ -500,8 +504,8 @@ let lookup_subterms env ind = 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 rec push_branch_args renv lrec c = +let case_branches_specif renv c_spec ind lbr = + let rec push_branch_args renv lrec c = match lrec with ra::lr -> let c' = whd_betadeltaiota renv.env c in @@ -517,7 +521,7 @@ let case_branches_specif renv c_spec ind lbr = let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in assert (Array.length sub_spec = Array.length lbr); array_map2 (push_branch_args renv) sub_spec lbr - | Dead_code -> + | Dead_code -> let t = dest_subterms (lookup_subterms renv.env ind) in let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in assert (Array.length sub_spec = Array.length lbr); @@ -530,10 +534,10 @@ let case_branches_specif renv c_spec ind lbr = about variables. *) -let rec subterm_specif renv t = +let rec subterm_specif renv t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_betadeltaiota renv.env t) in - match f with + match f with | Rel k -> subterm_var k renv | Case (ci,_,c,lbr) -> @@ -545,7 +549,7 @@ let rec subterm_specif renv t = 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 @@ -568,7 +572,7 @@ let rec subterm_specif renv t = (* Why Strict here ? To be general, it could also be Large... *) assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in - let decrArg = recindxs.(i) 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 @@ -582,7 +586,7 @@ let rec subterm_specif renv t = assign_var_spec renv'' (1, arg_spec) in subterm_specif renv'' strippedBody) - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> assert (l=[]); subterm_specif (push_var_renv renv (x,a)) b @@ -594,7 +598,7 @@ let rec subterm_specif renv t = (* Check term c can be applied to one of the mutual fixpoints. *) -let check_is_subterm renv c = +let check_is_subterm renv c = match subterm_specif renv c with Subterm (Strict,_) | Dead_code -> true | _ -> false @@ -622,21 +626,21 @@ let error_partial_apply renv fx = given [recpos], the decreasing arguments of each mutually defined fixpoint. *) let check_one_fix renv recpos def = - let nfi = Array.length recpos in + 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 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 match f with - | Rel p -> - (* Test if [p] is a fixpoint (recursive call) *) + | 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; - (* the position of the invoked fixpoint: *) + (* 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 @@ -668,9 +672,9 @@ let check_one_fix renv recpos def = (* Enables to traverse Fixpoint definitions in a more intelligent way, ie, the rule : if - g = Fix g/p := [y1:T1]...[yp:Tp]e & - - f is guarded with respect to the set of pattern variables S + - 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 + - f is guarded with respect to the set of pattern variables S in T1 ... Tp & - ap is a sub-term of the formal argument of f & - f is guarded with respect to the set of pattern variables @@ -682,10 +686,10 @@ let check_one_fix renv recpos def = 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 + let renv' = push_fix_renv renv recdef in if (List.length l < (decrArg+1)) then Array.iter (check_rec_call renv') bodies - else + else Array.iteri (fun j body -> if i=j then @@ -695,8 +699,8 @@ let check_one_fix renv recpos def = else check_rec_call renv' body) bodies - | Const kn -> - if evaluable_constant kn renv.env then + | Const kn -> + if evaluable_constant kn renv.env then try List.iter (check_rec_call renv) l with (FixGuardError _ ) -> check_rec_call renv(applist(constant_value renv.env kn, l)) @@ -704,14 +708,14 @@ let check_one_fix renv recpos def = (* The cases below simply check recursively the condition on the subterms *) - | Cast (a,_, b) -> + | Cast (a,_, b) -> List.iter (check_rec_call renv) (a::b::l) | Lambda (x,a,b) -> List.iter (check_rec_call renv) (a::l); check_rec_call (push_var_renv renv (x,a)) b - | Prod (x,a,b) -> + | Prod (x,a,b) -> List.iter (check_rec_call renv) (a::l); check_rec_call (push_var_renv renv (x,a)) b @@ -755,9 +759,9 @@ let check_one_fix renv recpos def = let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in + let nbfix = Array.length bodies in if nbfix = 0 - or Array.length nvect <> nbfix + or Array.length nvect <> nbfix or Array.length types <> nbfix or Array.length names <> nbfix or bodynum < 0 @@ -767,18 +771,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = let raise_err env i err = error_ill_formed_rec_body env err names i in (* Check the i-th definition with recarg k *) - let find_ind i k def = - (* check fi does not appear in the k+1 first abstractions, + let find_ind i k def = + (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) - let rec check_occur env n def = + let rec check_occur env n def = match (whd_betadeltaiota env def) with - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in if n = k+1 then (* get the inductive type of the fixpoint *) - let (mind, _) = - try find_inductive env a + let (mind, _) = + try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) @@ -818,17 +822,17 @@ let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in match b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b - | _ -> + codomain_is_coind (push_rel (x, None, a) env) b + | _ -> (try find_coinductive env b with Not_found -> raise (CoFixGuardError (env, CodomainNotInductiveType b))) -let check_one_cofix env nbfix def deftype = +let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n vlra t = if not (noccur_with_meta n nbfix t) then let c,args = decompose_app (whd_betadeltaiota env t) in - match c with + match c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive call allowed *) @@ -836,14 +840,14 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - + | Construct (_,i as cstr_kn) -> - let lra = vlra.(i-1) in + let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in let (mib,mip) = lookup_mind_specif env mI in let realargs = list_skipn mib.mind_nparams args in let rec process_args_of_constr = function - | (t::lr), (rar::lrar) -> + | (t::lr), (rar::lrar) -> if rar = mk_norec then if noccur_with_meta n nbfix t then process_args_of_constr (lr, lrar) @@ -854,26 +858,26 @@ let check_one_cofix env nbfix def deftype = check_rec_call env true n spec t; process_args_of_constr (lr, lrar) | [],_ -> () - | _ -> anomaly_ill_typed () + | _ -> anomaly_ill_typed () in process_args_of_constr (realargs, lra) - + | Lambda (x,a,b) -> assert (args = []); if noccur_with_meta n nbfix a then let env' = push_rel (x, None, a) env in check_rec_call env' alreadygrd (n+1) vlra b - else + else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - + | CoFix (j,(_,varit,vdefs as recdef)) -> if (List.for_all (noccur_with_meta n nbfix) args) - then + then let nbfix = Array.length vdefs in if (array_for_all (noccur_with_meta n nbfix) varit) then let env' = push_rec_types recdef env in (Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs; List.iter (check_rec_call env alreadygrd n vlra) args) - else + else raise (CoFixGuardError (env,RecCallInTypeOfDef c)) else raise (CoFixGuardError (env,UnguardedRecursiveCall c)) @@ -883,31 +887,31 @@ let check_one_cofix env nbfix def deftype = if (noccur_with_meta n nbfix tm) then if (List.for_all (noccur_with_meta n nbfix) args) then Array.iter (check_rec_call env alreadygrd n vlra) vrest - else + else raise (CoFixGuardError (env,RecCallInCaseFun c)) - else + else raise (CoFixGuardError (env,RecCallInCaseArg c)) - else + else raise (CoFixGuardError (env,RecCallInCasePred c)) - + | Meta _ -> () | Evar _ -> List.iter (check_rec_call env alreadygrd n vlra) args - - | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + + | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let (mind, _) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in check_rec_call env false 1 (dest_subterms vlra) def -(* The function which checks that the whole block of definitions +(* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in +let check_cofix env (bodynum,(names,types,bodies as recdef)) = + let nbfix = Array.length bodies in for i = 0 to nbfix-1 do let fixenv = push_rec_types recdef env in try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> + with CoFixGuardError (errenv,err) -> error_ill_formed_rec_body errenv err names i done diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 24000591..23ba4893 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -31,7 +31,7 @@ let check_constant_declaration env kn cb = (match cb.const_type with NonPolymorphicType ty -> let ty, cu = refresh_arity ty in - let envty = add_constraints cu env' in + let envty = add_constraints cu env' in let _ = infer_type envty ty in (match cb.const_body with | Some bd -> @@ -58,19 +58,15 @@ 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 +let rec list_fold_map2 f e = function | [] -> (e,[],[]) - | h::t -> + | 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_alias (s1:substitution) s2 = - if s1 <> s2 then failwith "Incorrect alias" - let check_definition_sub env cb1 cb2 = - let check_type env t1 t2 = + let check_type env t1 t2 = (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -81,7 +77,7 @@ let check_definition_sub env cb1 cb2 = Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). Hence they don't have to be checked again *) - let t1,t2 = + let t1,t2 = if isArity t2 then let (ctx2,s2) = destArity t2 in match s2 with @@ -135,38 +131,38 @@ let lookup_modtype mp env = with Not_found -> failwith ("Unknown module type: "^string_of_mp mp) - -let rec check_with env mtb with_decl = +let rec check_with env mtb with_decl mp= match with_decl with - | With_definition_body _ -> - check_with_aux_def env mtb with_decl; - empty_subst - | With_module_body _ -> - check_with_aux_mod env mtb with_decl + | With_definition_body _ -> + check_with_aux_def env mtb with_decl mp; + mtb + | With_module_body _ -> + check_with_aux_mod env mtb with_decl mp; + mtb -and check_with_aux_def env mtb with_decl = - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> - msid,sig_b +and check_with_aux_def env mtb with_decl mp = + let sig_b = match mtb with + | SEBstruct(sig_b) -> + sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> + let id,idl = match with_decl with + | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false + | With_definition_body ([],_) | With_module_body ([],_) -> assert false in let l = label_of_id id in try let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in - let env' = Modops.add_signature (MPself msid) before env in + let env' = Modops.add_signature mp before empty_delta_resolver env in match with_decl with | With_definition_body ([],_) -> assert false - | With_definition_body ([id],c) -> + | With_definition_body ([id],c) -> let cb = match spec with SFBconst cb -> cb | _ -> error_not_a_constant l - in + in check_definition_sub env' c cb | With_definition_body (_::_,_) -> let old = match spec with @@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl = let new_with_decl = match with_decl with With_definition_body (_,c) -> With_definition_body (idl,c) - | With_module_body (_,c,t,cst) -> - With_module_body (idl,c,t,cst) in - check_with_aux_def env' (type_of_mb env old) new_with_decl + | With_module_body (_,c) -> + With_module_body (idl,c) in + check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end @@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl = Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl = - let initmsid,msid,sig_b = - match eval_struct env mtb with - | SEBstruct(msid,sig_b) -> - let msid'=(refresh_msid msid) in - msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) +and check_with_aux_mod env mtb with_decl mp = + let sig_b = + match mtb with + | SEBstruct(sig_b) -> + sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> + let id,idl = match with_decl with + | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false + | With_definition_body ([],_) | With_module_body ([],_) -> assert false in let l = label_of_id id in try let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in let rec mp_rec = function - | [] -> MPself initmsid + | [] -> mp | i::r -> MPdot(mp_rec r,label_of_id i) - in - let env' = Modops.add_signature (MPself msid) before env in + in + let env' = Modops.add_signature mp before empty_delta_resolver env in match with_decl with - | With_module_body ([],_,_,_) -> assert false - | With_module_body ([id], mp,_,_) -> - let old,alias = match spec with - SFBmodule msb -> Some msb,None - | SFBalias (mp',_,_) -> None,Some mp' + | With_module_body ([],_) -> assert false + | With_module_body ([id], mp1) -> + let _ = match spec with + SFBmodule msb -> msb | _ -> error_not_a_module l in - let mtb' = lookup_modtype mp env' in - let _ = - match old,alias with - Some msb,None -> () - | None,Some mp' -> - check_modpath_equiv env' mp mp' - | _,_ -> - anomaly "Mod_typing:no implementation and no alias" - in - join (map_mp (mp_rec [id]) mp) mtb'.typ_alias - | With_module_body (_::_,mp,_,_) -> + let _ = (lookup_module mp1 env) in () + | With_module_body (_::_,mp) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -238,14 +223,12 @@ and check_with_aux_mod env mtb with_decl = match old.mod_expr with None -> let new_with_decl = match with_decl with - With_definition_body (_,c) -> + With_definition_body (_,c) -> With_definition_body (idl,c) - | With_module_body (_,c,t,cst) -> - With_module_body (idl,c,t,cst) in - let sub = - check_with_aux_mod env' - (type_of_mb env old) new_with_decl in - join (map_mp (mp_rec idl) mp) sub + | With_module_body (_,c) -> + With_module_body (idl,c) in + check_with_aux_mod env' + old.mod_type new_with_decl (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end @@ -255,113 +238,111 @@ and check_with_aux_mod env mtb with_decl = | Reduction.NotConvertible -> error_with_incorrect l and check_module_type env mty = - if mty.typ_strength <> None then - failwith "strengthening of module types not supported"; - let sub = check_modexpr env mty.typ_expr in - check_alias mty.typ_alias sub + let _ = check_modtype env mty.typ_expr mty.typ_mp in () -and check_module env mb = - let sub = - match mb.mod_expr, mb.mod_type with - | None, None -> - anomaly "Mod_typing.translate_module: empty type and expr in module entry" - | None, Some mtb -> check_modexpr env mtb - - | Some mexpr, _ -> - let sub1 = check_modexpr env mexpr in - (match mb.mod_type with - | None -> sub1 - | Some mte -> - let sub2 = check_modexpr env mte in - check_subtypes env - {typ_expr = mexpr; - typ_strength = None; - typ_alias = sub1;} - {typ_expr = mte; - typ_strength = None; - typ_alias = sub2;}; - sub2) in - check_alias mb.mod_alias sub - -and check_structure_field (s,env) mp lab = function + +and check_module env mp mb = + match mb.mod_expr, mb.mod_type with + | None,mtb -> + let _ = check_modtype env mtb mb.mod_mp in () + | Some mexpr, mtb when mtb==mexpr -> + let _ = check_modtype env mtb mb.mod_mp in () + | Some mexpr, _ -> + let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in + let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in + check_subtypes env + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;} + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;}; + +and check_structure_field env mp lab res = function | SFBconst cb -> let c = make_con mp empty_dirpath lab in - (s,check_constant_declaration env c cb) + check_constant_declaration env c cb | SFBmind mib -> - let kn = make_kn mp empty_dirpath lab in - (s,Indtypes.check_inductive env kn mib) + let kn = make_mind mp empty_dirpath lab in + let kn = mind_of_delta res kn in + Indtypes.check_inductive env kn mib | SFBmodule msb -> - check_module env msb; - let mp1 = MPdot(mp,lab) in - let is_fun, sub = Modops.update_subst env msb mp1 in - ((if is_fun then s else join s sub), - Modops.add_module (MPdot(mp,lab)) msb env) - | SFBalias(mp2,_,cst) -> - (* cf Safe_typing.add_alias *) - (try - let mp' = MPdot(mp,lab) in - let mp2' = scrape_alias mp2 env in - let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in - let sub = update_subst sub (map_mp mp' mp2') in - let sub = join_alias sub (map_mp mp' mp2') in - let sub = add_mp mp' mp2' sub in - (join s sub, register_alias mp' mp2 env) - with Not_found -> failwith "unknown aliased module") + let _= check_module env (MPdot(mp,lab)) msb in + Modops.add_module msb env | SFBmodtype mty -> - let kn = MPdot(mp, lab) in check_module_type env mty; - (join s mty.typ_alias, add_modtype kn mty env) - -and check_modexpr env mse = match mse with + add_modtype (MPdot(mp,lab)) mty env + +and check_modexpr env mse mp_mse res = match mse with + | SEBident mp -> + let mb = lookup_module mp env in + (subst_and_strengthen mb mp_mse env).mod_type + | SEBfunctor (arg_id, mtb, body) -> + check_module_type env mtb ; + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let sign = check_modexpr env' body mp_mse res in + SEBfunctor (arg_id, mtb, sign) + | SEBapply (f,m,cst) -> + let sign = check_modexpr env f mp_mse res in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mp = + try (path_of_mexpr m) + with Not_path -> error_application_to_not_path m + (* place for nondep_supertype *) in + let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + check_subtypes env mtb farg_b; + (subst_struct_expr (map_mbid farg_id mp) fbody_b) + | SEBwith(mte, with_decl) -> + let sign = check_modexpr env mte mp_mse res in + let sign = check_with env sign with_decl mp_mse in + sign + | SEBstruct(msb) -> + let _ = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab res mb) env msb in + SEBstruct(msb) + +and check_modtype env mse mp_mse res = match mse with | SEBident mp -> - let mp = scrape_alias mp env in let mtb = lookup_modtype mp env in - mtb.typ_alias + mtb.typ_expr | SEBfunctor (arg_id, mtb, body) -> check_module_type env mtb; - let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in - let sub = check_modexpr env' body in - sub + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let body = check_modtype env' body mp_mse res in + SEBfunctor(arg_id,mtb,body) | SEBapply (f,m,cst) -> - let sub1 = check_modexpr env f in - let f'= eval_struct env f in - let farg_id, farg_b, fbody_b = destr_functor env f' in + let sign = check_modtype env f mp_mse res in + let farg_id, farg_b, fbody_b = destr_functor env sign in let mp = - try scrape_alias (path_of_mexpr m) env + try (path_of_mexpr m) with Not_path -> error_application_to_not_path m - (* place for nondep_supertype *) in - let mtb = lookup_modtype mp env in - check_subtypes env mtb farg_b; - let sub2 = match eval_struct env m with - | SEBstruct (msid,sign) -> - join_alias - (subst_key (map_msid msid mp) mtb.typ_alias) - (map_msid msid mp) - | _ -> mtb.typ_alias in - let sub3 = join_alias sub1 (map_mbid farg_id mp) in - let sub4 = update_subst sub2 sub3 in - join sub3 sub4 + (* place for nondep_supertype *) in + let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + check_subtypes env mtb farg_b; + subst_struct_expr (map_mbid farg_id mp) fbody_b | SEBwith(mte, with_decl) -> - let sub1 = check_modexpr env mte in - let sub2 = check_with env mte with_decl in - join sub1 sub2 - | SEBstruct(msid,msb) -> - let mp = MPself msid in - let (sub,_) = - List.fold_left (fun env (lab,mb) -> - check_structure_field env mp lab mb) (empty_subst,env) msb in - sub - + let sign = check_modtype env mte mp_mse res in + let sign = check_with env sign with_decl mp_mse in + sign + | SEBstruct(msb) -> + let _ = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab res mb) env msb in + SEBstruct(msb) + (* -let rec add_struct_expr_constraints env = function + let rec add_struct_expr_constraints env = function | SEBident _ -> env - - | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb | SEBstruct (_,structure_body) -> - List.fold_left + List.fold_left (fun env (l,item) -> add_struct_elem_constraints env item) env structure_body @@ -369,20 +350,20 @@ let rec add_struct_expr_constraints env = function | SEBapply (meb1,meb2,cst) -> (* let g = Univ.merge_constraints cst Univ.initial_universes in msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ - Univ.pr_universes g++str"============="++fnl()); + Univ.pr_universes g++str"============="++fnl()); *) - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) + Environ.add_constraints cst + (add_struct_expr_constraints + (add_struct_expr_constraints env meb1) meb2) | SEBwith(meb,With_definition_body(_,cb))-> Environ.add_constraints cb.const_constraints (add_struct_expr_constraints env meb) | SEBwith(meb,With_module_body(_,_,cst))-> Environ.add_constraints cst - (add_struct_expr_constraints env meb) - -and add_struct_elem_constraints env = function + (add_struct_expr_constraints env meb) + +and add_struct_elem_constraints env = function | SFBconst cb -> Environ.add_constraints cb.const_constraints env | SFBmind mib -> Environ.add_constraints mib.mind_constraints env | SFBmodule mb -> add_module_constraints env mb @@ -390,18 +371,18 @@ and add_struct_elem_constraints env = function | SFBalias (mp,None) -> env | SFBmodtype mtb -> add_modtype_constraints env mtb -and add_module_constraints env mb = +and add_module_constraints env mb = let env = match mb.mod_expr with | None -> env | Some meb -> add_struct_expr_constraints env meb in let env = match mb.mod_type with | None -> env - | Some mtb -> + | Some mtb -> add_struct_expr_constraints env mtb in Environ.add_constraints mb.mod_constraints env -and add_modtype_constraints env mtb = +and add_modtype_constraints env mtb = add_struct_expr_constraints env mtb.typ_expr *) diff --git a/checker/modops.ml b/checker/modops.ml index 498bd775..458c84d8 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -18,7 +18,7 @@ open Declarations open Environ (*i*) -let error_not_a_constant l = +let error_not_a_constant l = error ("\""^(string_of_label l)^"\" is not a constant") let error_not_a_functor _ = error "Application of not a functor" @@ -32,13 +32,12 @@ let error_not_match l _ = let error_no_such_label l = error ("No such label "^string_of_label l) -let error_no_such_label_sub l l1 l2 = - let l1 = string_of_msid l1 in - let l2 = string_of_msid l2 in - error (l1^" is not a subtype of "^l2^".\nThe field "^ - string_of_label l^" is missing (or invisible) in "^l1^".") +let error_no_such_label_sub l l1 = + let l1 = string_of_mp l1 in + error ("The field "^ + string_of_label l^" is missing in "^l1^".") -let error_not_a_module_loc loc s = +let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc dummy_loc s @@ -56,38 +55,6 @@ let error_signature_expected mtb = let error_application_to_not_path _ = error "Application to not path" - -let module_body_of_type mtb = - { mod_type = Some mtb.typ_expr; - mod_expr = None; - mod_constraints = Constraint.empty; - mod_alias = mtb.typ_alias; - mod_retroknowledge = []} - -let module_type_of_module mp mb = - {typ_expr = - (match mb.mod_type with - | Some expr -> expr - | None -> (match mb.mod_expr with - | Some expr -> expr - | None -> - anomaly "Modops: empty expr and type")); - typ_alias = mb.mod_alias; - typ_strength = mp - } - - - -let rec list_split_assoc k rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail - -let path_of_seb = function - | SEBident mp -> mp - | _ -> anomaly "Modops: evaluation failed." - - let destr_functor env mtb = match mtb with | SEBfunctor (arg_id,arg_t,body_t) -> @@ -95,254 +62,152 @@ let destr_functor env mtb = | _ -> error_not_a_functor mtb -let rec check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else - let mp1 = scrape_alias mp1 env in - let mp2 = scrape_alias mp2 env in - if mp1=mp2 then () - else - error_not_equal mp1 mp2 - - - -let strengthen_const env mp l cb = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> - let const = Const (make_con mp empty_dirpath l) in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false - } - -let strengthen_mind env mp l mib = match mib.mind_equiv with - | Some _ -> mib - | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} +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; + mod_type_alg = mtb.typ_expr_alg; + mod_expr = None; + mod_constraints = mtb.typ_constraints; + mod_delta = mtb.typ_delta; + mod_retroknowledge = []} -let rec eval_struct env = function - | SEBident mp -> - begin - let mp = scrape_alias mp env in - let mtb =lookup_modtype mp env in - match mtb.typ_expr,mtb.typ_strength with - mtb,None -> eval_struct env mtb - | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) - end - | SEBapply (seb1,seb2,_) -> - let svb1 = eval_struct env seb1 in - let farg_id, farg_b, fbody_b = destr_functor env svb1 in - let mp = path_of_seb seb2 in - let mp = scrape_alias mp env in - let sub_alias = (lookup_modtype mp env).typ_alias in - let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias - | _ -> sub_alias in - let sub_alias = update_subst_alias sub_alias - (map_mbid farg_id mp) in - eval_struct env (subst_struct_expr - (join sub_alias (map_mbid farg_id mp)) fbody_b) - | SEBwith (mtb,(With_definition_body _ as wdb)) -> - merge_with env mtb wdb empty_subst - | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) -> - let alias_in_mp = - (lookup_modtype mp env).typ_alias in - merge_with env mtb wdb alias_in_mp -(* | SEBfunctor(mbid,mtb,body) -> - let env = add_module (MPbound mbid) (module_body_of_type mtb) env in - SEBfunctor(mbid,mtb,eval_struct env body) *) - | mtb -> mtb - -and type_of_mb env mb = - match mb.mod_type,mb.mod_expr with - None,Some b -> eval_struct env b - | Some t, _ -> eval_struct env t - | _,_ -> anomaly - "Modops: empty type and empty expr" - -and merge_with env mtb with_decl alias= - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> msid,sig_b - | _ -> error_signature_expected mtb - in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false - in - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc l [] sig_b in - let before = List.rev rev_before in - let rec mp_rec = function - | [] -> MPself msid - | i::r -> MPdot(mp_rec r,label_of_id i) - in - let new_spec,subst = match with_decl with - | With_definition_body ([],_) - | With_module_body ([],_,_,_) -> assert false - | With_definition_body ([id],c) -> - SFBconst c,None - | With_module_body ([id], mp,typ_opt,cst) -> - let mp' = scrape_alias mp env in - SFBalias (mp,typ_opt,Some cst), - Some(join (map_mp (mp_rec [id]) mp') alias) - | With_definition_body (_::_,_) - | With_module_body (_::_,_,_,_) -> - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - let new_with_decl,subst1 = - match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,t,cst) -> - With_module_body (idl,mp,t,cst), - Some(map_mp (mp_rec idc) mp) - in - let subst = Option.fold_right join subst1 alias in - let modtype = - merge_with env (type_of_mb env old) new_with_decl alias in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_constraints = old.mod_constraints; - mod_alias = subst; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb),Some subst - in - SEBstruct(msid, before@(l,new_spec):: - (Option.fold_right subst_structure subst after)) - with - Not_found -> error_no_such_label l +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 -and add_signature mp sign env = +let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in - let con = make_con mp empty_dirpath l in + let con = constant_of_kn kn in + let mind = mind_of_delta resolver (mind_of_kn kn) in match elem with - | SFBconst cb -> Environ.add_constant con cb env - | SFBmind mib -> Environ.add_mind kn mib env - | SFBmodule mb -> - add_module (MPdot (mp,l)) mb env + | SFBconst cb -> + (* let con = constant_of_delta resolver con in*) + Environ.add_constant con cb env + | SFBmind mib -> + (* let mind = mind_of_delta resolver mind in*) + Environ.add_mind mind mib env + | SFBmodule mb -> add_module mb env (* adds components as well *) - | SFBalias (mp1,_,cst) -> - Environ.register_alias (MPdot(mp,l)) mp1 env - | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) - mtb env + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in List.fold_left add_one env sign -and add_module mp mb env = +and add_module mb env = + let mp = mb.mod_mp in let env = Environ.shallow_add_module mp mb env in - let env = - Environ.add_modtype mp (module_type_of_module (Some mp) mb) env - in - let mod_typ = type_of_mb env mb in - match mod_typ with - | SEBstruct (msid,sign) -> - add_signature mp (subst_signature_msid msid mp sign) env + match mb.mod_type with + | SEBstruct (sign) -> + add_signature mp sign mb.mod_delta env | SEBfunctor _ -> env | _ -> anomaly "Modops:the evaluation of the structure failed " - -and constants_of_specification env mp sign = - let aux (env,res) (l,elem) = - match elem with - | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SFBmind _ -> env,res - | SFBmodule mb -> - let new_env = add_module (MPdot (mp,l)) mb env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (type_of_mb env mb)) @ res - | SFBalias (mp1,_,cst) -> - let new_env = register_alias (MPdot (mp,l)) mp1 env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (eval_struct env (SEBident mp1))) @ res - | SFBmodtype mtb -> - (* module type dans un module type. - Il faut au moins mettre mtb dans l'environnement (avec le bon - kn pour pouvoir continuer aller deplier les modules utilisant ce - mtb - ex: - Module Type T1. - Module Type T2. - .... - End T2. - ..... - Declare Module M : T2. - End T2 - si on ne rajoute pas T2 dans l'environement de typage - on va exploser au moment du Declare Module - *) - let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in - new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res - in - snd (List.fold_left aux (env,[]) sign) +let strengthen_const env mp_from l cb resolver = + match cb.const_opaque, cb.const_body with + | false, Some _ -> cb + | true, Some _ + | _, None -> + 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; + } + -and constants_of_modtype env mp modtype = - match (eval_struct env modtype) with - SEBstruct (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | SEBfunctor _ -> [] - | _ -> anomaly "Modops:the evaluation of the structure failed " +let rec strengthen_mod env mp_from mp_to mb = + if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then + mb + else + match mb.mod_type with + | SEBstruct (sign) -> + let resolve_out,sign_out = + strengthen_sig env mp_from sign mp_to mb.mod_delta in + { mb with + mod_expr = Some (SEBident mp_to); + mod_type = SEBstruct(sign_out); + mod_type_alg = mb.mod_type_alg; + mod_constraints = mb.mod_constraints; + mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to + (add_delta_resolver mb.mod_delta resolve_out)*); + mod_retroknowledge = mb.mod_retroknowledge} + | SEBfunctor _ -> mb + | _ -> anomaly "Modops:the evaluation of the structure failed " + +and strengthen_sig env mp_from sign mp_to resolver = + match sign with + | [] -> empty_delta_resolver,[] + | (l,SFBconst cb) :: rest -> + let item' = + l,SFBconst (strengthen_const env mp_from l cb resolver) in + let resolve_out,rest' = + strengthen_sig env mp_from rest mp_to resolver in + resolve_out,item'::rest' + | (_,SFBmind _ as item):: rest -> + let resolve_out,rest' = + strengthen_sig env mp_from rest mp_to resolver in + 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 env mp_from' mp_to' mb in + let item' = l,SFBmodule (mb_out) in + let env' = add_module mb_out env in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + resolve_out + (*add_delta_resolver resolve_out mb.mod_delta*), + item':: rest' + | (l,SFBmodtype mty as item) :: rest -> + let env' = add_modtype + (MPdot(mp_from,l)) mty env + in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + resolve_out,item::rest' -and strengthen_mtb env mp mtb = - let mtb1 = eval_struct env mtb in - match mtb1 with - | SEBfunctor _ -> mtb1 - | SEBstruct (msid,sign) -> - SEBstruct (msid,strengthen_sig env msid sign mp) - | _ -> anomaly "Modops:the evaluation of the structure failed " +let strengthen env mtb mp = + match mtb.typ_expr with + | SEBstruct (sign) -> + let resolve_out,sign_out = + strengthen_sig env 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 " -and strengthen_mod env mp mb = - let mod_typ = type_of_mb env mb in - { mod_expr = mb.mod_expr; - mod_type = Some (strengthen_mtb env mp mod_typ); - mod_constraints = mb.mod_constraints; - mod_alias = mb.mod_alias; - mod_retroknowledge = mb.mod_retroknowledge} - -and strengthen_sig env msid sign mp = match sign with - | [] -> [] - | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const env mp l cb) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SFBmind mib) :: rest -> - let item' = l,SFBmind (strengthen_mind env mp l mib) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SFBmodule mb) :: rest -> - let mp' = MPdot (mp,l) in - let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) mb env in - let rest' = strengthen_sig env' msid rest mp in - item':: rest' - | ((l,SFBalias (mp1,_,cst)) as item) :: rest -> - let env' = register_alias (MPdot(MPself msid,l)) mp1 env in - let rest' = strengthen_sig env' msid rest mp in - item::rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot((MPself msid),l)) - mty - env - in - let rest' = strengthen_sig env' msid rest mp in - item::rest' +let subst_and_strengthen mb mp env = + strengthen_mod env mb.mod_mp mp + (subst_module (map_mp mb.mod_mp mp) mb) - -let strengthen env mtb mp = strengthen_mtb env mp mtb -let update_subst env mb mp = - match type_of_mb env mb with - | SEBstruct(msid,str) -> false, join_alias - (subst_key (map_msid msid mp) mb.mod_alias) - (map_msid msid mp) - | _ -> true, mb.mod_alias +let module_type_of_module env mp mb = + match mp with + Some mp -> + strengthen env { + typ_mp = mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} mp + + | None -> + {typ_mp = mb.mod_mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} diff --git a/checker/modops.mli b/checker/modops.mli index 17b063e2..4476013c 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -19,35 +19,27 @@ open Environ (* Various operations on modules and module types *) -(* make the environment entry out of type *) -val module_body_of_type : module_type_body -> module_body +(* make the envirconment entry out of type *) +val module_body_of_type : module_path -> module_type_body -> module_body -val module_type_of_module : module_path option -> module_body -> - module_type_body +val module_type_of_module : env -> module_path option -> module_body -> + module_type_body -val destr_functor : +val destr_functor : env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body -(* Evaluation functions *) -val eval_struct : env -> struct_expr_body -> struct_expr_body - -val type_of_mb : env -> module_body -> struct_expr_body - -(* [add_signature mp sign env] assumes that the substitution [msid] - $\mapsto$ [mp] has already been performed (or is not necessary, like - when [mp = MPself msid]) *) -val add_signature : module_path -> structure_body -> env -> env +val add_signature : module_path -> structure_body -> delta_resolver -> env -> env (* adds a module and its components, but not the constraints *) -val add_module : module_path -> module_body -> env -> env +val add_module : module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val strengthen : env -> module_type_body -> module_path -> module_type_body -val update_subst : env -> module_body -> module_path -> bool * substitution +val subst_and_strengthen : module_body -> module_path -> env -> module_body -val error_incompatible_modtypes : +val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a val error_not_match : label -> structure_field_body -> 'a @@ -57,13 +49,13 @@ val error_with_incorrect : label -> 'a val error_no_such_label : label -> 'a val error_no_such_label_sub : - label -> mod_self_id -> mod_self_id -> 'a + label -> module_path -> 'a val error_signature_expected : struct_expr_body -> 'a val error_not_a_constant : label -> 'a -val error_not_a_module : label -> 'a +val error_not_a_module : label -> 'a val error_a_generative_module_expected : label -> 'a diff --git a/checker/reduction.ml b/checker/reduction.ml index c398f0a4..54b8fd48 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -86,13 +86,13 @@ let whd_betaiotazeta env x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) -let whd_betadeltaiota env t = +let whd_betadeltaiota env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_betadeltaiota_nolet env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t @@ -107,6 +107,15 @@ 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 *) (********************************************************************) @@ -139,8 +148,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = (* Convertibility of sorts *) -type conv_pb = - | CONV +type conv_pb = + | CONV | CUMUL let sort_cmp univ pb s0 s1 = @@ -202,7 +211,7 @@ let oracle_order fl1 fl2 = | _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) -let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = +let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) @@ -224,7 +233,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* case of leaves *) | (FAtom a1, FAtom a2) -> (match a1, a2 with - | (Sort s1, Sort s2) -> + | (Sort s1, Sort s2) -> assert (is_empty_stack v1 && is_empty_stack v2); sort_cmp univ cv_pb s1 s2 | (Meta n, Meta m) -> @@ -247,7 +256,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if fl1 = fl2 + if eq_table_key fl1 fl2 then convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible with NotConvertible -> @@ -272,15 +281,15 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* only one constant, defined var or defined rel *) | (FFlex fl1, _) -> (match unfold_reference infos fl1 with - | Some def1 -> + | 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 -> + | Some def2 -> eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) | None -> raise NotConvertible) - + (* other constructors *) | (FLambda _, FLambda _) -> assert (is_empty_stack v1 && is_empty_stack v2); @@ -318,7 +327,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in convert_vect univ infos el1 el2 fty1 fty2; - convert_vect univ infos + convert_vect univ infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2; convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible @@ -341,7 +350,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false - + (* In all other cases, terms are not convertible *) | _ -> raise NotConvertible @@ -368,9 +377,9 @@ let conv = fconv CONV let conv_leq = fconv CUMUL let conv_leq_vecti env v1 v2 = - array_fold_left2_i + array_fold_left2_i (fun i _ t1 t2 -> - (try conv_leq env t1 t2 + (try conv_leq env t1 t2 with (NotConvertible|Invalid_argument _) -> raise (NotConvertibleVect i)); ()) @@ -382,13 +391,13 @@ let conv_leq_vecti env v1 v2 = let vm_conv = ref fconv let set_vm_conv f = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try +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 - + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) @@ -404,12 +413,12 @@ let hnf_prod_app env t n = | Prod (_,_,b) -> subst1 n b | _ -> anomaly "hnf_prod_app: Need a product" -let hnf_prod_applist env t nl = +let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl (* Dealing with arities *) -let dest_prod env = +let dest_prod env = let rec decrec env m c = let t = whd_betadeltaiota env c in match t with @@ -417,11 +426,11 @@ let dest_prod env = let d = (n,None,a) in decrec (push_rel d env) (d::m) c0 | _ -> m,t - in + in decrec env empty_rel_context (* The same but preserving lets *) -let dest_prod_assum env = +let dest_prod_assum env = let rec prodec_rec env l ty = let rty = whd_betadeltaiota_nolet env ty in match rty with diff --git a/checker/reduction.mli b/checker/reduction.mli index eb50ae32..81c93ee5 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -37,9 +37,12 @@ val vm_conv : conv_pb -> constr conversion_function (************************************************************************) -(* Builds an application node, reducing beta redexes it may produce. *) +(* 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 diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index f4ffb302..8f5d4573 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -30,9 +30,8 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb digest = let env = !genv in - let mp = MPfile dp in let env = add_constraints mb.mod_constraints env in - let env = Modops.add_module mp mb env in + let env = Modops.add_module mb env in genv := add_digest env dp digest (* Check that the engagement expected by a library matches the initial one *) @@ -58,7 +57,7 @@ let check_imports f caller env needed = try let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp - with Not_found -> + with Not_found -> error ("Reference to unknown module " ^ (string_of_dirpath dp)) in List.iter check needed @@ -66,46 +65,46 @@ let check_imports f caller env needed = (* Remove the body of opaque constants in modules *) -(* also remove mod_expr ? *) +(* also remove mod_expr ? Good idea!*) let rec lighten_module mb = { mb with mod_expr = Option.map lighten_modexpr mb.mod_expr; - mod_type = Option.map lighten_modexpr mb.mod_type } + mod_type = lighten_modexpr mb.mod_type } -and lighten_struct struc = +and lighten_struct struc = let lighten_body (l,body) = (l,match body with | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x + | (SFBconst _ | SFBmind _ ) as x -> x | SFBmodule m -> SFBmodule (lighten_module m) - | SFBmodtype m -> SFBmodtype - ({m with + | 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 + SEBfunctor (mbid, + ({mty with typ_expr = lighten_modexpr mty.typ_expr}), lighten_modexpr mexpr) | SEBident mp as x -> x - | SEBstruct (msid, struc) -> - SEBstruct (msid, lighten_struct struc) + | 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) - + SEBwith (lighten_modexpr seb,wdcl) + let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) -type compiled_library = +type compiled_library = dir_path * module_body * (dir_path * Digest.t) list * engagement option - + 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|] @@ -119,20 +118,21 @@ let stamp_library file digest = () (* When the module is checked, digests do not need to match, but a warning is issued in case of mismatch *) -let import file (dp,mb,depends,engmt as vo) digest = +let import file (dp,mb,depends,engmt as vo) digest = Validate.apply !Flags.debug val_vo vo; Flags.if_verbose msgnl (str "*** vo structure validated ***"); let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module (add_constraints mb.mod_constraints env) mb; + 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 = +let unsafe_import file (dp,mb,depends,engmt as vo) digest = +(* if !Flags.debug then 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/subtyping.ml b/checker/subtyping.ml index 7a6868fe..3a100c01 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -19,29 +19,28 @@ open Reduction open Inductive open Modops (*i*) -open Pp +open Pp (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in inductive types *) -type namedobject = +type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) -let add_nameobjects_of_mib ln mib map = +let add_nameobjects_of_mib ln mib map = let add_nameobjects_of_one j oib map = let ip = (ln,j) in - let map = - array_fold_right_i + let map = + array_fold_right_i (fun i id map -> Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames @@ -54,19 +53,19 @@ let add_nameobjects_of_mib ln mib map = (* creates namedobject map for the whole signature *) -let make_label_map mp list = - let add_one (l,e) map = +let make_label_map mp list = + let add_one (l,e) map = let add_map obj = Labmap.add l obj map in match e with | SFBconst cb -> add_map (Constant cb) | SFBmind mib -> - add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map + add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,t,cst) -> add_map (Alias (mp,t)) in List.fold_right add_one list Labmap.empty + let check_conv_error error f env a1 a2 = try f env a1 a2 @@ -74,20 +73,21 @@ let check_conv_error error f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive env msid1 l info1 mib2 spec2 = - let kn = make_kn (MPself msid1) empty_dirpath l in +let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= + let kn = make_mind mp1 empty_dirpath l in let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let mib1 = + let mib1 = match info1 with | IndType ((_,0), mib) -> mib | _ -> error () in + let mib2 = subst_mind subst2 mib2 in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. + of the types of the constructors. By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each @@ -114,7 +114,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null | (Prop _, Type _) | (Type _,Prop _) -> error () | _ -> (s1, s2) in - check_conv conv_leq env + check_conv conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in @@ -145,7 +145,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = check (fun mib -> mib.mind_finite); check (fun mib -> mib.mind_ntypes); assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]); - assert (Array.length mib1.mind_packets >= 1 + assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); (* Check that the expected numbers of uniform parameters are the same *) @@ -155,30 +155,30 @@ let check_inductive env msid1 l info1 mib2 spec2 = (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - begin + (*begin match mib2.mind_equiv with | None -> () - | Some kn2' -> + | Some kn2' -> let kn2 = scrape_mind env kn2' in let kn1 = match mib1.mind_equiv with None -> kn | Some kn1' -> scrape_mind env kn1' in if kn1 <> kn2 then error () - end; + end;*) (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record); - if mib1.mind_record then begin - let rec names_prod_letin t = match t with + if mib1.mind_record then begin + let rec names_prod_letin t = match t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) | Cast(t,_,_) -> names_prod_letin t | _ -> [] - in + in assert (Array.length mib1.mind_packets = 1); assert (Array.length mib2.mind_packets = 1); - assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); - assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); + assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); end; (* we first check simple things *) @@ -187,10 +187,10 @@ let check_inductive env msid1 l info1 mib2 spec2 = let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env msid1 l info1 cb2 spec2 = +let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = + let check_type env t1 t2 = (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -201,7 +201,7 @@ let check_constant env msid1 l info1 cb2 spec2 = Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). Hence they don't have to be checked again *) - let t1,t2 = + let t1,t2 = if isArity t2 then let (ctx2,s2) = destArity t2 in match s2 with @@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 = (t1,t2) in check_conv conv_leq env t1 t2 in - - match info1 with - | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*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; - let con = make_con (MPself msid1) 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 - | _ -> ()) - | IndType ((kn,i),mind1) -> - ignore (Util.error ( - "The kernel does not recognize yet that a parameter can be " ^ - "instantiated by an inductive type. Hint: you can rename the " ^ - "inductive type and give a definition to map the old name to the new " ^ - "name.")); + match info1 with + | Constant cb1 -> + 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 + | _ -> ()) + | IndType ((kn,i),mind1) -> + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ + "instantiated by an inductive type. Hint: you can rename the " ^ + "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 () ; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in @@ -278,111 +279,96 @@ let check_constant env msid1 l info1 cb2 spec2 = check_conv conv env ty1 ty2 | _ -> error () -let rec check_modules env msid1 l msb1 msb2 = - let mp = (MPdot(MPself msid1,l)) in - let mty1 = module_type_of_module (Some mp) msb1 in - let mty2 = module_type_of_module None msb2 in - check_modtypes env mty1 mty2 false - +let rec check_modules env msb1 msb2 subst1 subst2 = + let mty1 = module_type_of_module env None msb1 in + let mty2 = module_type_of_module env None msb2 in + check_modtypes env mty1 mty2 subst1 subst2 false; + -and check_signatures env (msid1,sig1) alias (msid2,sig2') = - let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env in - let alias = update_subst_alias alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias sig2' in - let sig2 = subst_signature_msid msid2 mp1 sig2 in +and check_signatures env mp1 sig1 sig2 subst1 subst2 = let map1 = make_label_map mp1 sig1 in - let check_one_body (l,spec2) = - let info1 = - try - Labmap.find l map1 - with - Not_found -> error_no_such_label_sub l msid1 msid2 + let check_one_body (l,spec2) = + let info1 = + try + Labmap.find l map1 + with + Not_found -> error_no_such_label_sub l mp1 in match spec2 with | SFBconst cb2 -> - check_constant env msid1 l info1 cb2 spec2 - | SFBmind mib2 -> - check_inductive env msid1 l info1 mib2 spec2 - | SFBmodule msb2 -> + check_constant env mp1 l info1 cb2 spec2 subst1 subst2 + | SFBmind mib2 -> + check_inductive env mp1 l info1 mib2 spec2 subst1 subst2 + | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules env msid1 l msb msb2 - | Alias (mp,typ_opt) ->let msb = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb2 - | _ -> error_not_match l spec2 - end - | SFBalias (mp,typ_opt,_) -> - begin - match info1 with - | Alias (mp1,_) -> check_modpath_equiv env mp mp1 - | Module msb -> - let msb1 = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb1 + | Module msb -> check_modules env msb msb2 + subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> - let mtb1 = + let mtb1 = match info1 with | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - check_modtypes env mtb1 mtb2 true + let env = add_module (module_body_of_type mtb2.typ_mp mtb2) + (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in + check_modtypes env mtb1 mtb2 subst1 subst2 true in List.iter check_one_body sig2 -and check_modtypes env mtb1 mtb2 equiv = - if mtb1==mtb2 then () else (* just in case :) *) - let mtb1',mtb2'= - (match mtb1.typ_strength with - None -> eval_struct env mtb1.typ_expr, - eval_struct env mtb2.typ_expr - | Some mp -> strengthen env mtb1.typ_expr mp, - eval_struct env mtb2.typ_expr) in - let rec check_structure env str1 str2 equiv = - match str1, str2 with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - check_signatures env - (msid1,list1) mtb1.typ_alias (msid2,list2); - if equiv then - check_signatures env - (msid2,list2) mtb2.typ_alias (msid1,list1) - | SEBfunctor (arg_id1,arg_t1,body_t1), +and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 then () else + let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in + let rec check_structure env str1 str2 equiv subst1 subst2 = + match str1,str2 with + | SEBstruct (list1), + SEBstruct (list2) -> + check_signatures env + mtb1.typ_mp list1 list2 subst1 subst2; + if equiv then + check_signatures env + mtb2.typ_mp list2 list1 subst1 subst2 + else + () + | SEBfunctor (arg_id1,arg_t1,body_t1), SEBfunctor (arg_id2,arg_t2,body_t2) -> - check_modtypes env arg_t2 arg_t1 equiv; + check_modtypes env + arg_t2 arg_t1 + (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2 + equiv ; (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + let env = add_module + (module_body_of_type (MPbound arg_id2) arg_t2) env in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_struct_expr - (map_mbid arg_id1 (MPbound arg_id2)) - body_t1 + let env = match body_t1 with + SEBstruct str -> + add_module {mod_mp = mtb1.typ_mp; + mod_expr = None; + mod_type = body_t1; + mod_type_alg= None; + mod_constraints=mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + | _ -> env in - check_structure env (eval_struct env body_t1') - (eval_struct env body_t2) equiv + check_structure env body_t1 body_t2 equiv + (join (map_mbid arg_id1 (MPbound arg_id2)) subst1) + subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 - in + in if mtb1'== mtb2' then () - else check_structure env mtb1' mtb2' equiv + else check_structure env mtb1' mtb2' equiv subst1 subst2 -let check_subtypes env sup super = +let check_subtypes env sup super = (*if sup<>super then*) - check_modtypes env sup super false - -let check_equal env sup super = + let env = add_module + (module_body_of_type sup.typ_mp sup) env in + check_modtypes env (strengthen env 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 true + check_modtypes env sup super empty_subst + (map_mp super.typ_mp sup.typ_mp) true diff --git a/checker/term.ml b/checker/term.ml index f245d155..be70b864 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -28,7 +28,7 @@ type metavariable = int type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } type case_info = { ci_ind : inductive; @@ -81,7 +81,7 @@ let val_fix f = [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|] let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|] -type cast_kind = VMcast | DEFAULTcast +type cast_kind = VMcast | DEFAULTcast let val_cast = val_enum "cast_kind" 2 (*s*******************************************************************) @@ -116,7 +116,7 @@ let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| [|val_name;val_constr;val_constr|]; (* Lambda *) [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *) [|val_constr;val_array val_constr|]; (* App *) - [|val_kn|]; (* Const *) + [|val_con|]; (* Const *) [|val_ind|]; (* Ind *) [|val_cstr|]; (* Construct *) [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) @@ -135,7 +135,7 @@ let rec strip_outer_cast c = match c with | _ -> c let rec collapse_appl c = match c with - | App (f,cl) -> + | App (f,cl) -> let rec collapse_rec f cl2 = match (strip_outer_cast f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) @@ -171,7 +171,7 @@ let iter_constr_with_binders g f n c = match c with | App (c,l) -> f n c; Array.iter (f n) l | Evar (_,l) -> Array.iter (f n) l | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl - | Fix (_,(_,tl,bl)) -> + | Fix (_,(_,tl,bl)) -> Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl | CoFix (_,(_,tl,bl)) -> @@ -183,11 +183,11 @@ exception LocalOccur (* (closedn n M) raises FreeVar if a variable of height greater than n occurs in M, returns () otherwise *) -let closedn n c = +let closedn n c = let rec closed_rec n c = match c with | Rel m -> if m>n then raise LocalOccur | _ -> iter_constr_with_binders succ closed_rec n c - in + in try closed_rec n c; true with LocalOccur -> false (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) @@ -196,21 +196,21 @@ let closed0 = closedn 0 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) -let noccurn n term = +let noccurn n term = let rec occur_rec n c = match c with | Rel m -> if m = n then raise LocalOccur | _ -> iter_constr_with_binders succ occur_rec n c - in + in try occur_rec n term; true with LocalOccur -> false -(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M +(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M for n <= p < n+m *) -let noccur_between n m term = +let noccur_between n m term = let rec occur_rec n c = match c with | Rel(p) -> if n<=p && p iter_constr_with_binders succ occur_rec n c - in + in try occur_rec n term; true with LocalOccur -> false (* Checking function for terms containing existential variables. @@ -220,7 +220,7 @@ let noccur_between n m term = which may contain the CoFix variables. These occurrences of CoFix variables are not considered *) -let noccur_with_meta n m term = +let noccur_with_meta n m term = let rec occur_rec n c = match c with | Rel p -> if n<=p & p @@ -261,18 +261,18 @@ let rec exliftn el c = match c with (* Lifting the binding depth across k bindings *) -let liftn k n = +let liftn k n = match el_liftn (pred n) (el_shft k ELID) with | ELID -> (fun c -> c) | el -> exliftn el - + let lift k = liftn k 1 (*********************) (* Substituting *) (*********************) -(* (subst1 M c) substitutes M for Rel(1) in c +(* (subst1 M c) substitutes M for Rel(1) in c we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) @@ -291,15 +291,15 @@ let rec lift_substituend depth s = let make_substituend c = { sinfo=Unknown; sit=c } let substn_many lamv n c = - let lv = Array.length lamv in + let lv = Array.length lamv in if lv = 0 then c - else + else let rec substrec depth c = match c with | Rel k -> if k<=depth then c else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1) else Rel (k-lv) - | _ -> map_constr_with_binders succ substrec depth c in + | _ -> map_constr_with_binders succ substrec depth c in substrec n c let substnl laml n = @@ -362,7 +362,7 @@ let extended_rel_list n hyps = | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps | (_,Some _,_) :: hyps -> reln l (p+1) hyps | [] -> l - in + in reln [] 1 hyps (* Iterate lambda abstractions *) @@ -372,17 +372,17 @@ let compose_lam l b = let rec lamrec = function | ([], b) -> b | ((v,t)::l, b) -> lamrec (l, Lambda (v,t,b)) - in + in lamrec (l,b) (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) -let decompose_lam = +let decompose_lam = let rec lamdec_rec l c = match c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c - in + in lamdec_rec [] (* Decompose lambda abstractions and lets, until finding n @@ -390,15 +390,15 @@ let decompose_lam = let decompose_lam_n_assum n = if n < 0 then error "decompose_lam_n_assum: integer parameter must be positive"; - let rec lamdec_rec l n c = - if n=0 then l,c - else match c with + let rec lamdec_rec l n c = + if n=0 then l,c + else match c with | Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" - in - lamdec_rec empty_rel_context n + in + lamdec_rec empty_rel_context n (* Iterate products, with or without lets *) @@ -410,27 +410,27 @@ let mkProd_or_LetIn (na,body,t) c = let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) -let decompose_prod_assum = +let decompose_prod_assum = let rec prodec_rec l c = match c with | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c - in + in prodec_rec empty_rel_context let decompose_prod_n_assum n = if n < 0 then error "decompose_prod_n_assum: integer parameter must be positive"; - let rec prodec_rec l n c = + let rec prodec_rec l n c = if n=0 then l,c - else match c with + else match c with | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" - in + in prodec_rec empty_rel_context n @@ -443,7 +443,7 @@ let val_arity = val_tuple"arity"[|val_rctxt;val_constr|] let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign -let destArity = +let destArity = let rec prodec_rec l c = match c with | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c @@ -451,7 +451,7 @@ let destArity = | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly "destArity: not an arity" - in + in prodec_rec [] let rec isArity c = @@ -463,7 +463,7 @@ let rec isArity c = | _ -> false (*******************************) -(* alpha conversion functions *) +(* alpha conversion functions *) (*******************************) (* alpha conversion : ignore print names and casts *) @@ -483,15 +483,15 @@ let compare_constr f t1 t2 = if Array.length l1 = Array.length l2 then f c1 c2 & array_for_all2 f l1 l2 else - let (h1,l1) = decompose_app t1 in + let (h1,l1) = decompose_app t1 in let (h2,l2) = decompose_app t2 in if List.length l1 = List.length l2 then f h1 h2 & List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> c1 = c2 - | Ind c1, Ind c2 -> c1 = c2 - | Construct c1, Construct c2 -> c1 = c2 + | Const c1, Const c2 -> eq_con_chk c1 c2 + | Ind c1, Ind c2 -> eq_ind_chk c1 c2 + | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> @@ -500,7 +500,7 @@ let compare_constr f t1 t2 = ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 | _ -> false -let rec eq_constr m n = +let rec eq_constr m n = (m==n) or compare_constr eq_constr m n diff --git a/checker/type_errors.ml b/checker/type_errors.ml index a96bba6a..7c014105 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -81,10 +81,10 @@ let error_assumption env j = let error_reference_variables env id = raise (TypeError (env, ReferenceVariables id)) -let error_elim_arity env ind aritylst c pj okinds = +let error_elim_arity env ind aritylst c pj okinds = raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds))) -let error_case_not_inductive env j = +let error_case_not_inductive env j = raise (TypeError (env, CaseNotInductive j)) let error_number_branches env cj expn = diff --git a/checker/type_errors.mli b/checker/type_errors.mli index 2d8f8ff2..0482f2f2 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -73,11 +73,11 @@ val error_unbound_var : env -> variable -> 'a val error_not_type : env -> unsafe_judgment -> 'a val error_assumption : env -> unsafe_judgment -> 'a - + val error_reference_variables : env -> constr -> 'a -val error_elim_arity : - env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> +val error_elim_arity : + env -> inductive -> sorts_family list -> constr -> unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a @@ -90,11 +90,11 @@ val error_generalization : env -> name * constr -> unsafe_judgment -> 'a val error_actual_type : env -> unsafe_judgment -> constr -> 'a -val error_cant_apply_not_functional : +val error_cant_apply_not_functional : env -> unsafe_judgment -> unsafe_judgment array -> 'a -val error_cant_apply_bad_type : - env -> int * constr * constr -> +val error_cant_apply_bad_type : + env -> int * constr * constr -> unsafe_judgment -> unsafe_judgment array -> 'a val error_ill_formed_rec_body : diff --git a/checker/typeops.ml b/checker/typeops.ml index 1832ebec..e5cf6a6d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -21,9 +21,9 @@ open Environ let inductive_of_constructor = fst let conv_leq_vecti env v1 v2 = - array_fold_left2_i + array_fold_left2_i (fun i _ t1 t2 -> - (try conv_leq env t1 t2 + (try conv_leq env t1 t2 with NotConvertible -> raise (NotConvertibleVect i)); ()) () v1 @@ -57,18 +57,18 @@ let judge_of_prop = Sort (Type type1_univ) let judge_of_type u = Sort (Type (super u)) (*s Type of a de Bruijn index. *) - -let judge_of_relative env n = + +let judge_of_relative env n = try let (_,_,typ) = lookup_rel n env in lift n typ - with Not_found -> + with Not_found -> error_unbound_rel env n (* Type of variables *) let judge_of_variable env id = try named_type id env - with Not_found -> + with Not_found -> error_unbound_var env id (* Management of context of variables. *) @@ -115,7 +115,7 @@ let extract_context_levels env = let make_polymorphic_if_arity env t = let params, ccl = dest_prod_assum env t in match ccl with - | Sort (Type u) -> + | 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) @@ -141,10 +141,10 @@ let type_of_constant env cst = let judge_of_constant_knowing_parameters env cst paramstyp = let c = Const cst in let cb = - try lookup_constant cst env + try lookup_constant cst env with Not_found -> failwith ("Cannot find constant: "^string_of_con cst) in - let _ = check_args env c cb.const_hyps in + let _ = check_args env c cb.const_hyps in type_of_constant_knowing_parameters env cb.const_type paramstyp let judge_of_constant env cst = @@ -159,19 +159,19 @@ let judge_of_apply env (f,funj) argjv = (match whd_betadeltaiota env typ with | Prod (_,c1,c2) -> (try conv_leq env hj c1 - with NotConvertible -> + with NotConvertible -> error_cant_apply_bad_type env (n,c1, hj) (f,funj) argjv); apply_rec (n+1) (subst1 h c2) restjl | _ -> error_cant_apply_not_functional env (f,funj) argjv) - in + in apply_rec 1 funj (Array.to_list argjv) (* Type of product *) let sort_of_product env domsort rangsort = match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) + (* Product rule (s,Prop,Prop) *) | (_, Prop Null) -> rangsort (* Product rule (Prop/Set,Set,Set) *) | (Prop _, Prop Pos) -> rangsort @@ -187,7 +187,7 @@ let sort_of_product env domsort rangsort = | (Prop Pos, Type u2) -> Type (sup type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) + (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (sup u1 u2) (* Type of a type cast *) @@ -204,7 +204,7 @@ let judge_of_cast env (c,cj) k tj = match k with | VMcast -> vm_conv CUMUL | DEFAULTcast -> conv_leq in - try + try conversion env cj tj with NotConvertible -> error_actual_type env (c,cj) tj @@ -228,7 +228,7 @@ let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) = let (mib,mip) = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in + failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in check_args env c mib.mind_hyps; type_of_inductive_knowing_parameters env mip paramstyp @@ -241,17 +241,17 @@ let judge_of_constructor env c = let constr = Construct c in let _ = let ((kn,_),_) = c in - let mib = + let mib = try lookup_mind kn env with Not_found -> - failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in - check_args env constr mib.mind_hyps in + failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in + check_args env constr mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in type_of_constructor c specif (* Case. *) -let check_branch_types env (c,cj) (lfj,explft) = +let check_branch_types env (c,cj) (lfj,explft) = try conv_leq_vecti env lfj explft with NotConvertibleVect i -> @@ -321,22 +321,22 @@ let rec execute env cstr = | Ind ind -> (* Sort-polymorphism of inductive types *) judge_of_inductive_knowing_parameters env ind jl - | Const cst -> + | Const cst -> (* Sort-polymorphism of constant *) judge_of_constant_knowing_parameters env cst jl - | _ -> + | _ -> (* No sort-polymorphism *) execute env f in let jl = array_map2 (fun c ty -> c,ty) args jl in judge_of_apply env (f,j) jl - - | Lambda (name,c1,c2) -> + + | Lambda (name,c1,c2) -> let _ = execute_type env c1 in let env1 = push_rel (name,None,c1) env in - let j' = execute env1 c2 in + let j' = execute env1 c2 in Prod(name,c1,j') - + | Prod (name,c1,c2) -> let varj = execute_type env c1 in let env1 = push_rel (name,None,c1) env in @@ -354,7 +354,7 @@ let rec execute env cstr = let env1 = push_rel (name,Some c1,c2) env in let j' = execute env1 c3 in subst1 c1 j' - + | Cast (c,k,t) -> let cj = execute env c in let _ = execute_type env t in @@ -371,13 +371,13 @@ let rec execute env cstr = let pj = execute env p in let lfj = execute_array env lf in judge_of_case env ci (p,pj) (c,cj) lfj - + | Fix ((_,i as vni),recdef) -> let fix_ty = execute_recdef env recdef i in let fix = (vni,recdef) in check_fix env fix; fix_ty - + | CoFix (i,recdef) -> let fix_ty = execute_recdef env recdef i in let cofix = (i,recdef) in @@ -391,10 +391,10 @@ let rec execute env cstr = | Evar _ -> anomaly "the kernel does not support existential variables" -and execute_type env constr = +and execute_type env constr = let j = execute env constr in snd (type_judgment env (constr,j)) - + and execute_recdef env (names,lar,vdef) i = let larj = execute_array env lar in let larj = array_map2 (fun c ty -> c,ty) lar larj in @@ -406,7 +406,7 @@ and execute_recdef env (names,lar,vdef) i = and execute_array env = Array.map (execute env) -and execute_list env = List.map (execute env) +and execute_list env = List.map (execute env) (* Derived functions *) let infer env constr = execute env constr @@ -418,7 +418,7 @@ let infer_v env cv = execute_array env cv let check_ctxt env rels = fold_rel_context (fun d env -> match d with - (_,None,ty) -> + (_,None,ty) -> let _ = infer_type env ty in push_rel d env | (_,Some bd,ty) -> @@ -436,7 +436,7 @@ let check_named_ctxt env ctxt = failwith ("variable "^string_of_id id^" defined twice") with Not_found -> () in match d with - (_,None,ty) -> + (_,None,ty) -> let _ = infer_type env ty in push_named d env | (_,Some bd,ty) -> diff --git a/checker/validate.ml b/checker/validate.ml index 804bf7df..ab17aa7f 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -41,6 +41,8 @@ let pr_obj o = pr_obj_rec o; Format.print_newline() exception ValidObjError of string * Obj.t let fail o s = raise (ValidObjError(s,o)) +let ep s1 f s2 = f (s1^"/"^s2) + let apply debug f x = let o = Obj.repr x in try f o @@ -49,7 +51,7 @@ let apply debug f x = print_endline ("Validation failed: "^msg); pr_obj obj end; - failwith "validation failed" + failwith "vo structure validation failed" (* data not validated *) let no_val (o:Obj.t) = () @@ -71,8 +73,7 @@ let val_block s o = let val_tuple s v o = 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 + if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v else fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)) @@ -88,7 +89,7 @@ let val_sum s cc vv 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^": max is "^string_of_int i)) + else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i)) else if Obj.is_int o then let (n:int) = Obj.magic o in (if n<0 || n>=cc then @@ -161,11 +162,14 @@ let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|] let val_mp = val_rec_sum "module_path" 0 - (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|]) + (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] -let val_ind = val_tuple "inductive"[|val_kn;val_int|] +let val_con = + val_tuple "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|] (* univ *) -- cgit v1.2.3