diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /checker | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'checker')
33 files changed, 8356 insertions, 0 deletions
diff --git a/checker/.depend b/checker/.depend new file mode 100644 index 00000000..09ab6bdd --- /dev/null +++ b/checker/.depend @@ -0,0 +1,58 @@ +checker.cmo: type_errors.cmi term.cmo safe_typing.cmi indtypes.cmi \ + declarations.cmi check_stat.cmi check.cmo +checker.cmx: type_errors.cmx term.cmx safe_typing.cmx indtypes.cmx \ + declarations.cmx check_stat.cmx check.cmx +check.cmo: safe_typing.cmi +check.cmx: safe_typing.cmx +check_stat.cmo: term.cmo safe_typing.cmi indtypes.cmi environ.cmo \ + declarations.cmi check_stat.cmi +check_stat.cmx: term.cmx safe_typing.cmx indtypes.cmx environ.cmx \ + declarations.cmx check_stat.cmi +closure.cmo: term.cmo environ.cmo closure.cmi +closure.cmx: term.cmx environ.cmx closure.cmi +closure.cmi: term.cmo environ.cmo +declarations.cmo: term.cmo declarations.cmi +declarations.cmx: term.cmx declarations.cmi +declarations.cmi: term.cmo +environ.cmo: term.cmo declarations.cmi +environ.cmx: term.cmx declarations.cmx +indtypes.cmo: typeops.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ + declarations.cmi indtypes.cmi +indtypes.cmx: typeops.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ + declarations.cmx indtypes.cmi +indtypes.cmi: typeops.cmi term.cmo environ.cmo declarations.cmi +inductive.cmo: type_errors.cmi term.cmo reduction.cmi environ.cmo \ + declarations.cmi inductive.cmi +inductive.cmx: type_errors.cmx term.cmx reduction.cmx environ.cmx \ + declarations.cmx inductive.cmi +inductive.cmi: term.cmo environ.cmo declarations.cmi +main.cmo: checker.cmo +main.cmx: checker.cmx +mod_checking.cmo: typeops.cmi term.cmo subtyping.cmi reduction.cmi modops.cmi \ + inductive.cmi indtypes.cmi environ.cmo declarations.cmi +mod_checking.cmx: typeops.cmx term.cmx subtyping.cmx reduction.cmx modops.cmx \ + inductive.cmx indtypes.cmx environ.cmx declarations.cmx +modops.cmo: term.cmo environ.cmo declarations.cmi modops.cmi +modops.cmx: term.cmx environ.cmx declarations.cmx modops.cmi +modops.cmi: term.cmo environ.cmo declarations.cmi +reduction.cmo: term.cmo environ.cmo closure.cmi reduction.cmi +reduction.cmx: term.cmx environ.cmx closure.cmx reduction.cmi +reduction.cmi: term.cmo environ.cmo +safe_typing.cmo: validate.cmo modops.cmi mod_checking.cmo environ.cmo \ + declarations.cmi safe_typing.cmi +safe_typing.cmx: validate.cmx modops.cmx mod_checking.cmx environ.cmx \ + declarations.cmx safe_typing.cmi +safe_typing.cmi: term.cmo environ.cmo declarations.cmi +subtyping.cmo: typeops.cmi term.cmo reduction.cmi modops.cmi inductive.cmi \ + environ.cmo declarations.cmi subtyping.cmi +subtyping.cmx: typeops.cmx term.cmx reduction.cmx modops.cmx inductive.cmx \ + environ.cmx declarations.cmx subtyping.cmi +subtyping.cmi: term.cmo environ.cmo declarations.cmi +type_errors.cmo: term.cmo environ.cmo type_errors.cmi +type_errors.cmx: term.cmx environ.cmx type_errors.cmi +type_errors.cmi: term.cmo environ.cmo +typeops.cmo: type_errors.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ + declarations.cmi typeops.cmi +typeops.cmx: type_errors.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ + declarations.cmx typeops.cmi +typeops.cmi: term.cmo environ.cmo declarations.cmi diff --git a/checker/Makefile b/checker/Makefile new file mode 100644 index 00000000..2bcc9d36 --- /dev/null +++ b/checker/Makefile @@ -0,0 +1,88 @@ +OCAMLC=ocamlc +OCAMLOPT=ocamlopt + +COQSRC=.. + +MLDIRS=-I $(COQSRC)/config -I $(COQSRC)/lib -I $(COQSRC)/kernel -I +camlp4 +BYTEFLAGS=$(MLDIRS) +OPTFLAGS=$(MLDIRS) + +CHECKERNAME=coqchk + +BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE) +MCHECKERLOCAL :=\ + declarations.cmo environ.cmo \ + closure.cmo reduction.cmo \ + type_errors.cmo \ + modops.cmo \ + inductive.cmo typeops.cmo \ + indtypes.cmo subtyping.cmo mod_checking.cmo \ +validate.cmo \ + safe_typing.cmo check.cmo \ + check_stat.cmo checker.cmo + +MCHECKER:=\ + $(COQSRC)/config/coq_config.cmo \ + $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \ + $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \ + $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \ + $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \ + $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \ + $(COQSRC)/kernel/esubst.cmo term.cmo \ + $(MCHECKERLOCAL) + +all: $(BINARIES) + +byte : ../bin/$(CHECKERNAME)$(EXE) +opt : ../bin/$(CHECKERNAME).opt$(EXE) + +check.cma: $(MCHECKERLOCAL) + ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER) + +check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx) + ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx) + +../bin/$(CHECKERNAME)$(EXE): check.cma + ocamlc $(BYTEFLAGS) -o $@ unix.cma gramlib.cma check.cma main.ml + +../bin/$(CHECKERNAME).opt$(EXE): check.cmxa + ocamlopt $(OPTFLAGS) -o $@ unix.cmxa gramlib.cmxa check.cmxa main.ml + +stats: + @echo STRUCTURE + @wc names.ml term.ml declarations.ml environ.ml type_errors.ml + @echo + @echo REDUCTION + @-wc esubst.ml closure.ml reduction.ml + @echo + @echo TYPAGE + @wc univ.ml inductive.ml indtypes.ml typeops.ml safe_typing.ml + @echo + @echo MODULES + @wc modops.ml subtyping.ml + @echo + @echo INTERFACE + @wc check*.ml main.ml + @echo + @echo TOTAL + @wc *.ml | tail -1 + +.SUFFIXES:.ml .mli .cmi .cmo .cmx + +.ml.cmo: + $(OCAMLC) -c $(BYTEFLAGS) $< + +.ml.cmx: + $(OCAMLOPT) -c $(OPTFLAGS) $< + +.mli.cmi: + $(OCAMLC) -c $(BYTEFLAGS) $< + + +depend:: + ocamldep *.ml* > .depend + +clean:: + rm -f *.cm* *.o *.a *~ $(BINARIES) + +-include .depend diff --git a/checker/check.ml b/checker/check.ml new file mode 100644 index 00000000..f8844975 --- /dev/null +++ b/checker/check.ml @@ -0,0 +1,376 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *) + +open Pp +open Util +open Names + +let pr_id id = str (string_of_id id) +let pr_dirpath dp = str (string_of_dirpath dp) +let default_root_prefix = make_dirpath [] +let split_dirpath d = + let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) +let extend_dirpath p id = make_dirpath (id :: repr_dirpath p) + +type section_path = { + dirpath : string list ; + basename : string } +let dir_of_path p = + make_dirpath + (id_of_string p.basename :: List.map id_of_string p.dirpath) +let path_of_dirpath dir = + match repr_dirpath dir with + [] -> failwith "path_of_dirpath" + | 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) +let pr_path sp = + match sp.dirpath with + [] -> str sp.basename + | sl -> pr_dirlist sl ++ str"." ++ str sp.basename + +type library_objects + +type compilation_unit_name = dir_path + +type library_disk = { + md_name : compilation_unit_name; + md_compiled : Safe_typing.compiled_library; + md_objects : library_objects; + md_deps : (compilation_unit_name * Digest.t) list; + md_imports : compilation_unit_name list } + +(************************************************************************) +(*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 + kept in the global table [libraries_table]. *) + +type library_t = { + library_name : compilation_unit_name; + library_filename : System.physical_path; + library_compiled : Safe_typing.compiled_library; + library_deps : (compilation_unit_name * Digest.t) list; + library_digest : Digest.t } + +module LibraryOrdered = + struct + type t = dir_path + let compare d1 d2 = + Pervasives.compare + (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + end + +module LibrarySet = Set.Make(LibraryOrdered) +module LibraryMap = Map.Make(LibraryOrdered) + +(* This is a map from names to loaded libraries *) +let libraries_table = ref LibraryMap.empty + +(* various requests to the tables *) + +let find_library dir = + LibraryMap.find dir !libraries_table + +let try_find_library dir = + try find_library dir + with Not_found -> + error ("Unknown library " ^ (string_of_dirpath dir)) + +let library_full_filename dir = (find_library dir).library_filename + + (* If a library is loaded several time, then the first occurrence must + be performed first, thus the libraries_loaded_list ... *) + +let register_loaded_library m = + libraries_table := LibraryMap.add m.library_name m !libraries_table + +let check_one_lib admit (dir,m) = + let file = m.library_filename in + let md = m.library_compiled in + let dig = m.library_digest in + (* Look up if the library is to be admitted correct. We could + also check if it carries a validation certificate (yet to + be implemented). *) + if LibrarySet.mem dir admit then + (Flags.if_verbose msgnl + (str "Admitting library: " ++ pr_dirpath dir); + Safe_typing.unsafe_import file md dig) + else + (Flags.if_verbose msgnl + (str "Checking library: " ++ pr_dirpath dir); + Safe_typing.import file md dig); + Flags.if_verbose msg(fnl()); + register_loaded_library m + +(*************************************************************************) +(*s Load path. Mapping from physical to logical paths etc.*) + +type logical_path = dir_path + +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 curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) + let n = String.length curdir in + if String.length p > n && String.sub p 0 n = curdir then + remove_path_dot (String.sub p n (String.length p - n)) + else + p + +let strip_path p = + let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) + let n = String.length cwd in + if String.length p > n && String.sub p 0 n = cwd then + remove_path_dot (String.sub p n (String.length p - n)) + else + remove_path_dot p + +let canonical_path_name p = + let current = Sys.getcwd () in + try + Sys.chdir p; + let p' = Sys.getcwd () in + Sys.chdir current; + p' + with Sys_error _ -> + (* We give up to find a canonical name and just simplify it... *) + strip_path p + +let find_logical_path phys_dir = + let phys_dir = canonical_path_name phys_dir in + match list_filter2 (fun p d -> p = phys_dir) !load_paths with + | _,[dir] -> dir + | _,[] -> default_root_prefix + | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + +let is_in_load_paths phys_dir = + let dir = canonical_path_name phys_dir in + let lp = get_load_paths () in + let check_p = fun p -> (String.compare dir p) == 0 in + List.exists check_p lp + +let remove_load_path dir = + load_paths := list_filter2 (fun p d -> p <> dir) !load_paths + +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 this is not the default -I . to coqtop *) + && not + (phys_path = canonical_path_name Filename.current_dir_name + && coq_path = default_root_prefix) + then + begin + (* Assume the user is concerned by library naming *) + if dir <> default_root_prefix then + Flags.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); + remove_load_path phys_path; + load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) + end + | _,[] -> + load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) + | _ -> anomaly ("Two logical paths are associated to "^phys_path) + +let physical_paths (dp,lp) = dp + +let load_paths_of_dir_path dir = + fst (list_filter2 (fun p d -> d = dir) !load_paths) + +let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +exception LibUnmappedDir +exception LibNotFound + +let locate_absolute_library dir = + (* Search in loadpath *) + let pref, base = split_dirpath dir in + let loadpath = load_paths_of_dir_path pref in + if loadpath = [] then raise LibUnmappedDir; + try + let name = string_of_id base^".vo" in + let _, file = System.where_in_path loadpath name in + (dir, file) + with Not_found -> + (* Last chance, removed from the file system but still in memory *) + try + (dir, library_full_filename dir) + with Not_found -> + raise LibNotFound + +let locate_qualified_library qid = + try + let loadpath = + (* Search library in loadpath *) + if qid.dirpath=[] then get_load_paths () + else + (* we assume dir is an absolute dirpath *) + load_paths_of_dir_path (dir_of_path qid) + in + if loadpath = [] then raise LibUnmappedDir; + let name = qid.basename^".vo" in + let path, file = System.where_in_path loadpath name in + let dir = + extend_dirpath (find_logical_path path) (id_of_string qid.basename) in + (* Look if loaded *) + try + (dir, library_full_filename dir) + with Not_found -> + (dir, file) + with Not_found -> raise LibNotFound + +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 "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) + | LibNotFound -> + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") + | e -> raise e + +let try_locate_absolute_library dir = + try + locate_absolute_library dir + with e -> + explain_locate_library_error (path_of_dirpath dir) e + +let try_locate_qualified_library qid = + try + locate_qualified_library qid + with e -> + explain_locate_library_error qid e + +(************************************************************************) +(*s Low-level interning/externing of libraries to files *) + +(*s Loading from disk to cache (preparation phase) *) + +let vo_magic_number = 08190 (* trunk *) + +let (raw_extern_library, raw_intern_library) = + System.raw_extern_intern vo_magic_number ".vo" + +let with_magic_number_check f a = + try f a + with System.Bad_magic_number fname -> + errorlabstrm "with_magic_number_check" + (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ + spc () ++ str"It is corrupted" ++ spc () ++ + str"or was compiled with another version of Coq.") + +(************************************************************************) +(* Internalise libraries *) + +let mk_library md f digest = { + library_name = md.md_name; + library_filename = f; + library_compiled = md.md_compiled; + library_deps = md.md_deps; + library_digest = digest } + +let name_clash_message dir mdir f = + str ("The file " ^ f ^ " contains library") ++ spc () ++ + pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++ + pr_dirpath dir + +(* Dependency graph *) +let depgraph = ref LibraryMap.empty + +let intern_from_file (dir, f) = + Flags.if_verbose msg (str"[intern "++str f++str" ..."); + let (md,digest) = + try + let ch = with_magic_number_check raw_intern_library f in + let (md:library_disk) = System.marshal_in ch in + let digest = System.marshal_in ch in + close_in ch; + if dir <> md.md_name then + errorlabstrm "load_physical_library" + (name_clash_message dir md.md_name f); + Flags.if_verbose msgnl(str" done]"); + md,digest + with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in + depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; + mk_library md f digest + +let get_deps (dir, f) = + try LibraryMap.find dir !depgraph + with Not_found -> + let _ = intern_from_file (dir,f) in + LibraryMap.find dir !depgraph + +(* Read a compiled library and all dependencies, in reverse order. + Do not include files that are already in the context. *) +let rec intern_library (dir, f) needed = + (* Look if in the current logical environment *) + try let _ = find_library dir in needed + with Not_found -> + (* Look if already listed and consequently its dependencies too *) + if List.mem_assoc dir needed then needed + else + (* [dir] is an absolute name which matches [f] which must be in loadpath *) + let m = intern_from_file (dir,f) in + (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed + +(* digest error with checked modules could be a warning *) +and intern_mandatory_library (dir,_) needed = + intern_library (try_locate_absolute_library dir) needed + +(* Compute the reflexive transitive dependency closure *) +let rec fold_deps ff (dir,f) s = + if LibrarySet.mem dir s then s + else + let deps = get_deps (dir,f) in + let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in + ff dir (List.fold_right (fold_deps ff) deps s) + +and fold_deps_list ff modl needed = + List.fold_right (fold_deps ff) modl needed + +let recheck_library ~norec ~admit ~check = + let ml = List.map try_locate_qualified_library check in + let nrl = List.map try_locate_qualified_library norec in + let al = List.map try_locate_qualified_library admit in + let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in + (* first compute the closure of norec, remove closure of check, + add closure of admit, and finally remove norec and 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... *) + let nochk = + List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in + (* *) + Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ + prlist + (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); + List.iter (check_one_lib nochk) needed; + Flags.if_verbose msgnl(str"Modules were successfully checked") + +open Printf + +let mem s = + let m = try_find_library s in + h 0 (str (sprintf "%dk" (size_kb m))) diff --git a/checker/check_stat.ml b/checker/check_stat.ml new file mode 100644 index 00000000..96366594 --- /dev/null +++ b/checker/check_stat.ml @@ -0,0 +1,69 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open System +open Flags +open Names +open Term +open Declarations +open Environ + +let memory_stat = ref false + +let print_memory_stat () = + if !memory_stat then begin + Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()); + Format.print_newline(); + flush_all() + end + +let output_context = ref false + +let pr_engt = function + Some ImpredicativeSet -> + str "Theory: Set is impredicative" + | None -> + str "Theory: Set is predicative" + +let cst_filter f csts = + Cmap.fold + (fun c ce acc -> if f c ce then c::acc else acc) + csts [] + +let is_ax _ cb = cb.const_body = None + +let pr_ax csts = + let axs = cst_filter is_ax csts in + if axs = [] then + str "Axioms: <none>" + else + hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Indtypes.prcon axs) + +let print_context env = + if !output_context then begin + let + {env_globals= + {env_constants=csts; env_inductives=inds; + env_modules=mods; env_modtypes=mtys}; + env_stratification= + {env_universes=univ; env_engagement=engt}} = env in + msgnl(hov 0 + (str"CONTEXT SUMMARY" ++ fnl() ++ + str"===============" ++ fnl() ++ fnl() ++ + str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_ax csts) ++ + fnl())) + end + +let stats () = + print_context (Safe_typing.get_env()); + print_memory_stat () + +let _ = at_exit stats diff --git a/checker/check_stat.mli b/checker/check_stat.mli new file mode 100644 index 00000000..7037bd46 --- /dev/null +++ b/checker/check_stat.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val memory_stat : bool ref +val output_context : bool ref + +val stats : unit -> unit diff --git a/checker/checker.ml b/checker/checker.ml new file mode 100644 index 00000000..1c7ace12 --- /dev/null +++ b/checker/checker.ml @@ -0,0 +1,376 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *) + +open Pp +open Util +open System +open Flags +open Names +open Term +open Check + +let coq_root = id_of_string "Coq" +let parse_dir s = + let len = String.length s in + let rec decoupe_dirs dirs n = + if n>=len then dirs else + let pos = + try + 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) + in + decoupe_dirs [] 0 +let dirpath_of_string s = + match parse_dir s with + [] -> invalid_arg "dirpath_of_string" + | dir -> make_dirpath (List.map id_of_string dir) +let path_of_string s = + match parse_dir s with + [] -> invalid_arg "dirpath_of_string" + | l::dir -> {dirpath=dir; basename=l} + +let (/) = Filename.concat + +let get_version_date () = + try + let ch = open_in (Coq_config.coqlib^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,Coq_config.date) + +let print_header () = + let (ver,rev) = (get_version_date ()) in + Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; + flush stdout + +(* Adding files to Coq loadpath *) + +let add_path ~unix_path:dir ~coq_root:coq_dirpath = + if exists_dir dir then + begin + Check.add_load_path (dir,coq_dirpath) + end + else + msg_warning (str ("Cannot open " ^ dir)) + +let convert_string d = + try id_of_string d + with _ -> + if_verbose warning + ("Directory "^d^" cannot be used as a Coq identifier (skipped)"); + flush_all (); + failwith "caught" + +let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = + let dirs = all_subdirs dir in + let prefix = repr_dirpath coq_dirpath in + if dirs <> [] then + let convert_dirs (lp,cp) = + (lp,Names.make_dirpath + ((List.map convert_string (List.rev cp))@prefix)) in + let dirs = map_succeed convert_dirs dirs in + begin + List.iter Check.add_load_path dirs + end + else + msg_warning (str ("Cannot open " ^ dir)) + +(* By the option -include -I or -R of the command line *) +let includes = ref [] +let push_include (s, alias) = includes := (s,alias,false) :: !includes +let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes + +let 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) + +(* Initializes the LoadPath according to COQLIB and Coq_config *) +let init_load_path () = + let coqlib = + (* variable COQLIB overrides the default library *) + getenv_else "COQLIB" + (if Coq_config.local || !Flags.boot then Coq_config.coqtop + else Coq_config.coqlib) in + let user_contrib = coqlib/"user-contrib" in + let contrib = coqlib/"contrib" in + (* first user-contrib *) + 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 standard library *) +(* List.iter + (fun (s,alias) -> + add_rec_path (coqlib/s) ([alias; coq_root])) + theories_dirs_map;*) + add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]); + (* then current directory *) + add_path "." Check.default_root_prefix; + (* additional loadpath, given with -I -include -R options *) + List.iter + (fun (s,alias,reci) -> + if reci then add_rec_path s alias else add_path s alias) + (List.rev !includes); + includes := [] + + +let set_debug () = Flags.debug := true + +let engagement = ref None +let set_engagement c = engagement := Some c +let engage () = + match !engagement with Some c -> Safe_typing.set_engagement c | None -> () + + +let admit_list = ref ([] : section_path list) +let add_admit s = + admit_list := path_of_string s :: !admit_list + +let norec_list = ref ([] : section_path list) +let add_norec s = + norec_list := path_of_string s :: !norec_list + +let compile_list = ref ([] : section_path list) +let add_compile s = + compile_list := path_of_string s :: !compile_list + +(*s Parsing of the command line. + We no longer use [Arg.parse], in order to use share [Usage.print_usage] + between coqtop and coqc. *) + +let compile_files () = + Check.recheck_library + ~norec:(List.rev !norec_list) + ~admit:(List.rev !admit_list) + ~check:(List.rev !compile_list) + +let version () = + Printf.printf "The Coq Proof Checker, version %s (%s)\n" + Coq_config.version Coq_config.date; + Printf.printf "compiled on %s\n" Coq_config.compile_date; + exit 0 + +(* print the usage of coqtop (or coqc) on channel co *) + +let print_usage_channel co command = + output_string co command; + output_string co "Coq options are:\n"; + output_string co +" -I dir add directory dir in the include path + -include dir (idem) + -R dir coqdir recursively map physical dir to logical coqdir + + -admit module load module and dependencies without checking + -norec module check module but admit dependencies without checking + + -where print Coq's standard library location and exit + -v print Coq version and exit + + -h, --help print this list of options +" + +(* print the usage on standard error *) + +let print_usage = print_usage_channel stderr + +let print_usage_coqtop () = + print_usage "Usage: coqchk <options>\n\n" + +let usage () = + print_usage_coqtop (); + flush stderr; + exit 1 + +let warning s = msg_warning (str s) + +open Type_errors + +let anomaly_string () = str "Anomaly: " +let report () = (str "." ++ spc () ++ str "Please report.") + +let print_loc loc = + if loc = dummy_loc then + (str"<unknown>") + else + let loc = unloc loc in + (int (fst loc) ++ str"-" ++ int (snd loc)) +let guill s = "\""^s^"\"" + +let where s = + if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) + +let rec explain_exn = function + | Stream.Failure -> + hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") + | Stream.Error txt -> + hov 0 (str "Syntax error: " ++ str txt) + | Token.Error txt -> + hov 0 (str "Syntax error: " ++ str txt) + | Sys_error msg -> + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) + | UserError(s,pps) -> + hov 1 (str "User error: " ++ where s ++ pps) + | Out_of_memory -> + hov 0 (str "Out of memory") + | Stack_overflow -> + hov 0 (str "Stack overflow") + | Anomaly (s,pps) -> + hov 1 (anomaly_string () ++ where s ++ pps ++ report ()) + | Match_failure(filename,pos1,pos2) -> + hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ + if Sys.ocaml_version = "3.06" then + (str " from character " ++ int pos1 ++ + str " to " ++ int pos2) + else + (str " at line " ++ int pos1 ++ + str " character " ++ int pos2) + ++ report ()) + | Not_found -> + hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) + | Failure s -> + hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ()) + | Invalid_argument s -> + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + | Sys.Break -> + hov 0 (fnl () ++ str "User interrupt.") + | Univ.UniverseInconsistency (o,u,v) -> + 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 -> "=") + ++ spc() ++ (*Univ.pr_uni v ++*) str")" + else + mt() in + hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".") + | TypeError(ctx,te) -> +(* hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx *) + (* te)*) + hov 0 (str "Type error") + + | Indtypes.InductiveError e -> + hov 0 (str "Error related to inductive types") +(* let ctx = Check.get_env() in + hov 0 + (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) + | Stdpp.Exc_located (loc,exc) -> + hov 0 ((if loc = dummy_loc then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ explain_exn exc) + | Assert_failure (s,b,e) -> + hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ + (if s <> "" then + if Sys.ocaml_version = "3.06" then + (str ("(file \"" ^ s ^ "\", characters ") ++ + int b ++ str "-" ++ int e ++ str ")") + else + (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + str ", characters " ++ int e ++ str "-" ++ + int (e+6) ++ str ")") + else + (mt ())) ++ + report ()) + | reraise -> + hov 0 (anomaly_string () ++ str "Uncaught exception " ++ + str (Printexc.to_string reraise)++report()) + +let parse_args() = + let rec parse = function + | [] -> () + | "-impredicative-set" :: rem -> + set_engagement Declarations.ImpredicativeSet; parse rem + + | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: [] -> usage () + + | "-R" :: d :: p :: rem -> + push_rec_include (d, dirpath_of_string p);parse rem + | "-R" :: ([] | [_]) -> usage () + + | "-debug" :: rem -> set_debug (); parse rem + + | "-where" :: _ -> + print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + + | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () + + | ("-v"|"--version") :: _ -> version () + + | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem + + | ("-o" | "-output-context") :: rem -> + Check_stat.output_context := true; parse rem + + | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem + + | "-admit" :: s :: rem -> add_admit s; parse rem + | "-admit" :: [] -> usage () + + | "-norec" :: s :: rem -> add_norec s; parse rem + | "-norec" :: [] -> usage () + + | "-silent" :: rem -> + Flags.make_silent true; parse rem + + | s :: _ when s<>"" && s.[0]='-' -> + msgnl (str "Unknown option " ++ str s); exit 1 + | s :: rem -> add_compile s; parse rem + in + try + parse (List.tl (Array.to_list Sys.argv)) + with + | UserError(_,s) as e -> begin + try + Stream.empty s; exit 1 + with Stream.Failure -> + msgnl (explain_exn e); exit 1 + end + | e -> begin msgnl (explain_exn e); exit 1 end + + +(* To prevent from doing the initialization twice *) +let initialized = ref false + +let init() = + if not !initialized then begin + initialized := true; + Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + try + parse_args(); + if_verbose print_header (); + init_load_path (); + engage (); + with e -> + flush_all(); + message "Error during initialization :"; + msgnl (explain_exn e); + exit 1 + end + +let run () = + try + compile_files (); + flush_all() + with e -> + (Pp.ppnl(explain_exn e); + flush_all(); + exit 1) + +let start () = init(); run(); exit 0 diff --git a/checker/closure.ml b/checker/closure.ml new file mode 100644 index 00000000..ccbfbc4c --- /dev/null +++ b/checker/closure.ml @@ -0,0 +1,1047 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *) + +open Util +open Pp +open Term +open Names +open Esubst +open Environ + +let stats = ref false +let share = ref true + +(* Profiling *) +let beta = ref 0 +let delta = ref 0 +let zeta = ref 0 +let evar = ref 0 +let iota = ref 0 +let prune = ref 0 + +let reset () = + beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 + +let stop() = + msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ + str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") + +let incr_cnt red cnt = + if red then begin + if !stats then incr cnt; + true + end else + false + +let with_stats c = + if !stats then begin + reset(); + let r = Lazy.force c in + stop(); + r + end else + Lazy.force c + +type transparent_state = Idpred.t * Cpred.t +let all_opaque = (Idpred.empty, Cpred.empty) +let all_transparent = (Idpred.full, Cpred.full) + +module type RedFlagsSig = sig + type reds + type red_kind + val fBETA : red_kind + val fDELTA : red_kind + val fIOTA : red_kind + val fZETA : red_kind + val fCONST : constant -> red_kind + val fVAR : identifier -> red_kind + val no_red : reds + val red_add : reds -> red_kind -> reds + val red_sub : reds -> red_kind -> reds + val red_add_transparent : reds -> transparent_state -> reds + val mkflags : red_kind list -> reds + val red_set : reds -> red_kind -> bool + val red_get_const : reds -> bool * evaluable_global_reference list +end + +module RedFlags = (struct + + (* [r_const=(true,cl)] means all constants but those in [cl] *) + (* [r_const=(false,cl)] means only those in [cl] *) + (* [r_delta=true] just mean [r_const=(true,[])] *) + + type reds = { + r_beta : bool; + r_delta : bool; + r_const : transparent_state; + r_zeta : bool; + r_evar : bool; + r_iota : bool } + + type red_kind = BETA | DELTA | IOTA | ZETA + | CONST of constant | VAR of identifier + let fBETA = BETA + let fDELTA = DELTA + let fIOTA = IOTA + let fZETA = ZETA + let fCONST kn = CONST kn + let fVAR id = VAR id + let no_red = { + r_beta = false; + r_delta = false; + r_const = all_opaque; + r_zeta = false; + r_evar = false; + r_iota = false } + + let red_add red = function + | BETA -> { red with r_beta = true } + | DELTA -> { red with r_delta = true; r_const = all_transparent } + | CONST kn -> + let (l1,l2) = red.r_const in + { red with r_const = l1, Cpred.add kn l2 } + | IOTA -> { red with r_iota = true } + | ZETA -> { red with r_zeta = true } + | VAR id -> + let (l1,l2) = red.r_const in + { red with r_const = Idpred.add id l1, l2 } + + let red_sub red = function + | BETA -> { red with r_beta = false } + | DELTA -> { red with r_delta = false } + | CONST kn -> + let (l1,l2) = red.r_const in + { red with r_const = l1, Cpred.remove kn l2 } + | IOTA -> { red with r_iota = false } + | ZETA -> { red with r_zeta = false } + | VAR id -> + let (l1,l2) = red.r_const in + { red with r_const = Idpred.remove id l1, l2 } + + let red_add_transparent red tr = + { red with r_const = tr } + + let mkflags = List.fold_left red_add no_red + + let red_set red = function + | BETA -> incr_cnt red.r_beta beta + | CONST kn -> + let (_,l) = red.r_const in + let c = Cpred.mem kn l in + incr_cnt c delta + | VAR id -> (* En attendant d'avoir des kn pour les Var *) + let (l,_) = red.r_const in + let c = Idpred.mem id l in + incr_cnt c delta + | ZETA -> incr_cnt red.r_zeta zeta + | IOTA -> incr_cnt red.r_iota iota + | DELTA -> (* Used for Rel/Var defined in context *) + incr_cnt red.r_delta delta + + let red_get_const red = + let p1,p2 = red.r_const in + let (b1,l1) = Idpred.elements p1 in + let (b2,l2) = Cpred.elements p2 in + if b1=b2 then + let l1' = List.map (fun x -> EvalVarRef x) l1 in + let l2' = List.map (fun x -> EvalConstRef x) l2 in + (b1, l1' @ l2') + else error "unrepresentable pair of predicate" + +end : RedFlagsSig) + +open RedFlags + +let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA] +let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] +let betaiota = mkflags [fBETA;fIOTA] +let beta = mkflags [fBETA] +let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] +let unfold_red kn = + let flag = match kn with + | EvalVarRef id -> fVAR id + | EvalConstRef kn -> fCONST kn + in (* Remove fZETA for finer behaviour ? *) + mkflags [fBETA;flag;fIOTA;fZETA] + +(************************* Obsolète +(* [r_const=(true,cl)] means all constants but those in [cl] *) +(* [r_const=(false,cl)] means only those in [cl] *) +type reds = { + r_beta : bool; + r_const : bool * constant_path list * identifier list; + r_zeta : bool; + r_evar : bool; + r_iota : bool } + +let betadeltaiota_red = { + r_beta = true; + r_const = true,[],[]; + r_zeta = true; + r_evar = true; + r_iota = true } + +let betaiota_red = { + r_beta = true; + r_const = false,[],[]; + r_zeta = false; + r_evar = false; + r_iota = true } + +let beta_red = { + r_beta = true; + r_const = false,[],[]; + r_zeta = false; + r_evar = false; + r_iota = false } + +let no_red = { + r_beta = false; + r_const = false,[],[]; + r_zeta = false; + r_evar = false; + r_iota = false } + +let betaiotazeta_red = { + r_beta = true; + r_const = false,[],[]; + r_zeta = true; + r_evar = false; + r_iota = true } + +let unfold_red kn = + let c = match kn with + | EvalVarRef id -> false,[],[id] + | EvalConstRef kn -> false,[kn],[] + in { + r_beta = true; + r_const = c; + r_zeta = true; (* false for finer behaviour ? *) + r_evar = false; + r_iota = true } + +(* Sets of reduction kinds. + Main rule: delta implies all consts (both global (= by + kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's). + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of + a LetIn expression is Letin reduction *) + +type red_kind = + BETA | DELTA | ZETA | IOTA + | CONST of constant_path list | CONSTBUT of constant_path list + | VAR of identifier | VARBUT of identifier + +let rec red_add red = function + | BETA -> { red with r_beta = true } + | DELTA -> + (match red.r_const with + | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags" + | _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true }) + | CONST cl -> + (match red.r_const with + | true,_,_ -> error "Conflict in the reduction flags" + | _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 }) + | CONSTBUT cl -> + (match red.r_const with + | false,_::_,_ | false,_,_::_ -> + error "Conflict in the reduction flags" + | _,l1,l2 -> + { red with r_const = true, list_union cl l1, l2; + r_zeta = true; r_evar = true }) + | IOTA -> { red with r_iota = true } + | ZETA -> { red with r_zeta = true } + | VAR id -> + (match red.r_const with + | true,_,_ -> error "Conflict in the reduction flags" + | _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 }) + | VARBUT cl -> + (match red.r_const with + | false,_::_,_ | false,_,_::_ -> + error "Conflict in the reduction flags" + | _,l1,l2 -> + { red with r_const = true, l1, list_union [cl] l2; + r_zeta = true; r_evar = true }) + +let red_delta_set red = + let b,_,_ = red.r_const in b + +let red_local_const = red_delta_set + +(* to know if a redex is allowed, only a subset of red_kind is used ... *) +let red_set red = function + | BETA -> incr_cnt red.r_beta beta + | CONST [kn] -> + let (b,l,_) = red.r_const in + let c = List.mem kn l in + incr_cnt ((b & not c) or (c & not b)) delta + | VAR id -> (* En attendant d'avoir des kn pour les Var *) + let (b,_,l) = red.r_const in + let c = List.mem id l in + incr_cnt ((b & not c) or (c & not b)) delta + | ZETA -> incr_cnt red.r_zeta zeta + | EVAR -> incr_cnt red.r_zeta evar + | IOTA -> incr_cnt red.r_iota iota + | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*) + (* Not for internal use *) + | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented" + +(* Gives the constant list *) +let red_get_const red = + let b,l1,l2 = red.r_const in + let l1' = List.map (fun x -> EvalConstRef x) l1 in + let l2' = List.map (fun x -> EvalVarRef x) l2 in + b, l1' @ l2' +fin obsolète **************) +(* specification of the reduction function *) + + +(* Flags of reduction and cache of constants: 'a is a type that may be + * mapped to constr. 'a infos implements a cache for constants and + * abstractions, storing a representation (of type 'a) of the body of + * this constant or abstraction. + * * i_tab is the cache table of the results + * * i_repr is the function to get the representation from the current + * state of the cache and the body of the constant. The result + * is stored in the table. + * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables + * and only those with index 1 and 3 have bodies which are c and d resp. + * * i_vars is the list of _defined_ named variables. + * + * ref_value_cache searchs in the tab, otherwise uses i_repr to + * compute the result and store it in the table. If the constant can't + * be unfolded, returns None, but does not store this failure. * This + * doesn't take the RESET into account. You mustn't keep such a table + * after a Reset. * This type is not exported. Only its two + * instantiations (cbv or lazy) are. + *) + +type table_key = + | ConstKey of constant + | VarKey of identifier + | RelKey of int + +type 'a infos = { + i_flags : reds; + i_repr : 'a infos -> constr -> 'a; + i_env : env; + i_rels : int * (int * constr) list; + i_vars : (identifier * constr) list; + i_tab : (table_key, 'a) Hashtbl.t } + +let info_flags info = info.i_flags + +let ref_value_cache info ref = + try + Some (Hashtbl.find info.i_tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let (s,l) = info.i_rels in lift n (List.assoc (s-n) l) + | VarKey id -> List.assoc id info.i_vars + | ConstKey cst -> constant_value info.i_env cst + in + let v = info.i_repr info body in + Hashtbl.add info.i_tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + +let defined_vars flags env = +(* if red_local_const (snd flags) then*) + fold_named_context + (fun (id,b,_) e -> + match b with + | None -> e + | Some body -> (id, body)::e) + (named_context env) ~init:[] +(* else []*) + +let defined_rels flags env = +(* if red_local_const (snd flags) then*) + fold_rel_context + (fun (id,b,t) (i,subs) -> + match b with + | None -> (i+1, subs) + | Some body -> (i+1, (i,body) :: subs)) + (rel_context env) ~init:(0,[]) +(* else (0,[])*) + +let mind_equiv_infos info = mind_equiv info.i_env + +let create mk_cl flgs env = + { i_flags = flgs; + i_repr = mk_cl; + i_env = env; + i_rels = defined_rels flgs env; + i_vars = defined_vars flgs env; + i_tab = Hashtbl.create 17 } + + +(**********************************************************************) +(* Lazy reduction: the one used in kernel operations *) + +(* type of shared terms. fconstr and frterm are mutually recursive. + * Clone of the constr structure, but completely mutable, and + * annotated with reduction state (reducible or not). + * - FLIFT is a delayed shift; allows sharing between 2 lifted copies + * of a given term. + * - FCLOS is a delayed substitution applied to a constr + * - FLOCKED is used to erase the content of a reference that must + * be updated. This is to allow the garbage collector to work + * before the term is computed. + *) + +(* Norm means the term is fully normalized and cannot create a redex + when substituted + Cstr means the term is in head normal form and that it can + create a redex when substituted (i.e. constructor, fix, lambda) + Whnf means we reached the head normal form and that it cannot + create a redex when substituted + Red is used for terms that might be reduced +*) +type red_state = Norm | Cstr | Whnf | Red + +let neutr = function + | (Whnf|Norm) -> Whnf + | (Red|Cstr) -> Red + +type fconstr = { + mutable norm: red_state; + mutable term: fterm } + +and fterm = + | FRel of int + | FAtom of constr (* Metas and Sorts *) + | FCast of fconstr * cast_kind * fconstr + | FFlex of table_key + | FInd of inductive + | FConstruct of constructor + | FApp of fconstr * fconstr array + | FFix of fixpoint * fconstr subs + | FCoFix of cofixpoint * fconstr subs + | FCases of case_info * fconstr * fconstr * fconstr array + | FLambda of int * (name * constr) list * constr * fconstr subs + | FProd of name * fconstr * fconstr + | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FEvar of existential_key * fconstr array + | FLIFT of int * fconstr + | FCLOS of constr * fconstr subs + | FLOCKED + +let fterm_of v = v.term +let set_norm v = v.norm <- Norm +let is_val v = v.norm = Norm + +let mk_atom c = {norm=Norm;term=FAtom c} + +(* Could issue a warning if no is still Red, pointing out that we loose + sharing. *) +let update v1 (no,t) = + if !share then + (v1.norm <- no; + v1.term <- t; + v1) + else {norm=no;term=t} + +(**********************************************************************) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) + +type stack_member = + | Zapp of fconstr array + | Zcase of case_info * fconstr * fconstr array + | Zfix of fconstr * stack + | Zshift of int + | Zupdate of fconstr + +and stack = stack_member list + +let empty_stack = [] +let append_stack v s = + if Array.length v = 0 then s else + match s with + | Zapp l :: s -> Zapp (Array.append v l) :: s + | _ -> Zapp v :: s + +(* Collapse the shifts in the stack *) +let zshift n s = + match (n,s) with + (0,_) -> s + | (_,Zshift(k)::s) -> Zshift(n+k)::s + | _ -> Zshift(n)::s + +let rec stack_args_size = function + | Zapp v :: s -> Array.length v + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + +(* When used as an argument stack (only Zapp can appear) *) +let rec decomp_stack = function + | Zapp v :: s -> + (match Array.length v with + 0 -> decomp_stack s + | 1 -> Some (v.(0), s) + | _ -> + Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) + | _ -> None +let 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 + | [] -> [] + | Zapp args :: s -> args :: (stackrec s) + | _ -> assert false + in Array.concat (stackrec s) +let rec stack_assign s p c = match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then + Zapp args :: stack_assign s (p-q) c + else + (let nargs = Array.copy args in + nargs.(p) <- c; + Zapp nargs :: s) + | _ -> s +let rec stack_tail p s = + if p = 0 then s else + match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then stack_tail (p-q) s + else Zapp (Array.sub args p (q-p)) :: s + | _ -> failwith "stack_tail" +let rec stack_nth s p = match s with + | Zapp args :: s -> + let q = Array.length args in + if p >= q then stack_nth s (p-q) + else args.(p) + | _ -> raise Not_found + +(* Lifting. Preserves sharing (useful only for cell with norm=Red). + lft_fconstr always create a new cell, while lift_fconstr avoids it + when the lift is 0. *) +let rec lft_fconstr n ft = + match ft.term with + | (FInd _|FConstruct _|FFlex(ConstKey _|VarKey _)) -> ft + | FRel i -> {norm=Norm;term=FRel(i+n)} + | FLambda(k,tys,f,e) -> {norm=Cstr; term=FLambda(k,tys,f,subs_shft(n,e))} + | FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))} + | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} + | FLIFT(k,m) -> lft_fconstr (n+k) m + | FLOCKED -> assert false + | _ -> {norm=ft.norm; term=FLIFT(n,ft)} +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 + | Inl(n,mt) -> lift_fconstr n mt + | Inr(k,None) -> {norm=Norm; term= FRel k} + | Inr(k,Some p) -> + lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)} + +(* since the head may be reducible, we might introduce lifts of 0 *) +let compact_stack head stk = + let rec strip_rec depth = function + | Zshift(k)::s -> strip_rec (depth+k) s + | Zupdate(m)::s -> + (* Be sure to create a new cell otherwise sharing would be + lost by the update operation *) + let h' = lft_fconstr depth head in + let _ = update m (h'.norm,h'.term) in + strip_rec depth s + | stk -> zshift depth stk in + strip_rec 0 stk + +(* Put an update mark in the stack, only if needed *) +let zupdate m s = + if !share & m.norm = Red + then + let s' = compact_stack m s in + let _ = m.term <- FLOCKED in + Zupdate(m)::s' + else s + +(* Closure optimization: *) +let rec compact_constr (lg, subs as s) c k = + match c with + Rel i -> + if i < k then c,s else + (try Rel (k + lg - list_index (i-k+1) subs), (lg,subs) + with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs)) + | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s + | Evar(ev,v) -> + let (v',s) = compact_vect s v k in + if v==v' then c,s else Evar(ev,v'),s + | Cast(a,ck,b) -> + let (a',s) = compact_constr s a k in + let (b',s) = compact_constr s b k in + if a==a' && b==b' then c,s else Cast(a', ck, b'), s + | App(f,v) -> + let (f',s) = compact_constr s f k in + let (v',s) = compact_vect s v k in + if f==f' && v==v' then c,s else App(f',v'), s + | Lambda(n,a,b) -> + let (a',s) = compact_constr s a k in + let (b',s) = compact_constr s b (k+1) in + if a==a' && b==b' then c,s else Lambda(n,a',b'), s + | Prod(n,a,b) -> + let (a',s) = compact_constr s a k in + let (b',s) = compact_constr s b (k+1) in + if a==a' && b==b' then c,s else Prod(n,a',b'), s + | LetIn(n,a,ty,b) -> + let (a',s) = compact_constr s a k in + let (ty',s) = compact_constr s ty k in + let (b',s) = compact_constr s b (k+1) in + if a==a' && ty==ty' && b==b' then c,s else LetIn(n,a',ty',b'), s + | Fix(fi,(na,ty,bd)) -> + let (ty',s) = compact_vect s ty k in + let (bd',s) = compact_vect s bd (k+Array.length ty) in + if ty==ty' && bd==bd' then c,s else Fix(fi,(na,ty',bd')), s + | CoFix(i,(na,ty,bd)) -> + let (ty',s) = compact_vect s ty k in + let (bd',s) = compact_vect s bd (k+Array.length ty) in + if ty==ty' && bd==bd' then c,s else CoFix(i,(na,ty',bd')), s + | Case(ci,p,a,br) -> + let (p',s) = compact_constr s p k in + let (a',s) = compact_constr s a k in + let (br',s) = compact_vect s br k in + if p==p' && a==a' && br==br' then c,s else Case(ci,p',a',br'),s +and compact_vect s v k = compact_v [] s v k (Array.length v - 1) +and compact_v acc s v k i = + if i < 0 then + let v' = Array.of_list acc in + if array_for_all2 (==) v v' then v,s else v',s + else + let (a',s') = compact_constr s v.(i) k in + compact_v (a'::acc) s' v k (i-1) + +(* Computes the minimal environment of a closure. + Idea: if the subs is not identity, the term will have to be + reallocated entirely (to propagate the substitution). So, + computing the set of free variables does not change the + complexity. *) +let optimise_closure env c = + if is_subs_id env then (env,c) else + let (c',(_,s)) = compact_constr (0,[]) c 1 in + let env' = + Array.map (fun i -> clos_rel env i) (Array.of_list s) in + (subs_cons (env', ESID 0),c') + +let mk_lambda env t = + let (env,t) = optimise_closure env t in + let (rvars,t') = decompose_lam t in + FLambda(List.length rvars, List.rev rvars, t', env) + +let destFLambda clos_fun t = + match t.term with + FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) + | FLambda(n,(na,ty)::tys,b,e) -> + (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) + | _ -> assert false + +(* Optimization: do not enclose variables in a closure. + Makes variable access much faster *) +let mk_clos e t = + match t with + | Rel i -> clos_rel e i + | Var x -> { norm = Red; term = FFlex (VarKey x) } + | Const c -> { norm = Red; term = FFlex (ConstKey c) } + | Meta _ | Sort _ -> { norm = Norm; term = FAtom t } + | Ind kn -> { norm = Norm; term = FInd kn } + | Construct kn -> { norm = Cstr; term = FConstruct kn } + | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _) -> + {norm = Red; term = FCLOS(t,e)} + +let mk_clos_vect env v = Array.map (mk_clos env) v + +(* Translate the head constructor of t from constr to fconstr. This + function is parameterized by the function to apply on the direct + subterms. + Could be used insted of mk_clos. *) +let mk_clos_deep clos_fun env t = + match t with + | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> + mk_clos env t + | Cast (a,k,b) -> + { norm = Red; + term = FCast (clos_fun env a, k, clos_fun env b)} + | App (f,v) -> + { norm = Red; + term = FApp (clos_fun env f, Array.map (clos_fun env) v) } + | Case (ci,p,c,v) -> + { norm = Red; + term = FCases (ci, clos_fun env p, clos_fun env c, + Array.map (clos_fun env) v) } + | Fix fx -> + { norm = Cstr; term = FFix (fx, env) } + | CoFix cfx -> + { norm = Cstr; term = FCoFix(cfx,env) } + | Lambda _ -> + { norm = Cstr; term = mk_lambda env t } + | Prod (n,t,c) -> + { norm = Whnf; + term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } + | LetIn (n,b,t,c) -> + { norm = Red; + term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } + | Evar(ev,args) -> + { norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) } + +(* A better mk_clos? *) +let mk_clos2 = mk_clos_deep mk_clos + +(* The inverse of mk_clos_deep: move back to constr *) +let rec to_constr constr_fun lfts v = + match v.term with + | FRel i -> Rel (reloc_rel i lfts) + | FFlex (RelKey p) -> Rel (reloc_rel p lfts) + | FFlex (VarKey x) -> Var x + | FAtom c -> exliftn lfts c + | FCast (a,k,b) -> + Cast (constr_fun lfts a, k, constr_fun lfts b) + | FFlex (ConstKey op) -> Const op + | FInd op -> Ind op + | FConstruct op -> Construct op + | FCases (ci,p,c,ve) -> + Case (ci, constr_fun lfts p, + constr_fun lfts c, + Array.map (constr_fun lfts) ve) + | FFix ((op,(lna,tys,bds)),e) -> + let n = Array.length bds in + let ftys = Array.map (mk_clos e) tys in + let fbds = Array.map (mk_clos (subs_liftn n e)) bds in + let lfts' = el_liftn n lfts in + Fix (op, (lna, Array.map (constr_fun lfts) ftys, + Array.map (constr_fun lfts') fbds)) + | FCoFix ((op,(lna,tys,bds)),e) -> + let n = Array.length bds in + let ftys = Array.map (mk_clos e) tys in + let fbds = Array.map (mk_clos (subs_liftn n e)) bds in + let lfts' = el_liftn (Array.length bds) lfts in + CoFix (op, (lna, Array.map (constr_fun lfts) ftys, + Array.map (constr_fun lfts') fbds)) + | FApp (f,ve) -> + App (constr_fun lfts f, + Array.map (constr_fun lfts) ve) + | FLambda _ -> + let (na,ty,bd) = destFLambda mk_clos2 v in + Lambda (na, constr_fun lfts ty, + constr_fun (el_lift lfts) bd) + | FProd (n,t,c) -> + Prod (n, constr_fun lfts t, + constr_fun (el_lift lfts) c) + | FLetIn (n,b,t,f,e) -> + let fc = mk_clos2 (subs_lift e) f in + LetIn (n, constr_fun lfts b, + constr_fun lfts t, + constr_fun (el_lift lfts) fc) + | FEvar (ev,args) -> Evar(ev,Array.map (constr_fun lfts) args) + | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + | FCLOS (t,env) -> + let fr = mk_clos2 env t in + let unfv = update v (fr.norm,fr.term) in + to_constr constr_fun lfts unfv + | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*) + +(* This function defines the correspondance between constr and + fconstr. When we find a closure whose substitution is the identity, + then we directly return the constr to avoid possibly huge + reallocation. *) +let term_of_fconstr = + let rec term_of_fconstr_lift lfts v = + match v.term with + | FCLOS(t,env) when is_subs_id env & is_lift_id lfts -> t + | FLambda(_,tys,f,e) when is_subs_id e & is_lift_id lfts -> + compose_lam (List.rev tys) f + | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> Fix fx + | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> CoFix cfx + | _ -> to_constr term_of_fconstr_lift lfts v in + term_of_fconstr_lift ELID + + + +(* fstrong applies unfreeze_fun recursively on the (freeze) term and + * yields a term. Assumes that the unfreeze_fun never returns a + * FCLOS term. +let rec fstrong unfreeze_fun lfts v = + to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) +*) + +let rec zip m stk = + match stk with + | [] -> m + | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s + | Zcase(ci,p,br)::s -> + let t = FCases(ci, p, m, br) in + zip {norm=neutr m.norm; term=t} s + | Zfix(fx,par)::s -> + zip fx (par @ append_stack [|m|] s) + | Zshift(n)::s -> + zip (lift_fconstr n m) s + | Zupdate(rf)::s -> + zip (update rf (m.norm,m.term)) s + +let fapp_stack (m,stk) = zip m stk + +(*********************************************************************) + +(* The assertions in the functions below are granted because they are + called only when m is a constructor, a cofix + (strip_update_shift_app), a fix (get_nth_arg) or an abstraction + (strip_update_shift, through get_arg). *) + +(* optimised for the case where there are no shifts... *) +let strip_update_shift head stk = + assert (head.norm <> Red); + let rec strip_rec h depth = function + | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s + | Zupdate(m)::s -> + strip_rec (update m (h.norm,h.term)) depth s + | stk -> (depth,stk) in + strip_rec head 0 stk + +(* optimised for the case where there are no shifts... *) +let strip_update_shift_app head stk = + assert (head.norm <> Red); + let rec strip_rec rstk h depth = function + | Zshift(k) as e :: s -> + strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s + | (Zapp args :: s) -> + strip_rec (Zapp args :: rstk) + {norm=h.norm;term=FApp(h,args)} depth s + | Zupdate(m)::s -> + strip_rec rstk (update m (h.norm,h.term)) depth s + | stk -> (depth,List.rev rstk, stk) in + strip_rec [] head 0 stk + + +let get_nth_arg head n stk = + assert (head.norm <> Red); + let rec strip_rec rstk h depth n = function + | Zshift(k) as e :: s -> + strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s + | Zapp args::s' -> + let q = Array.length args in + if n >= q + then + strip_rec (Zapp args::rstk) + {norm=h.norm;term=FApp(h,args)} depth (n-q) s' + else + let bef = Array.sub args 0 n in + let aft = Array.sub args (n+1) (q-n-1) in + let stk' = + List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in + (Some (stk', args.(n)), append_stack aft s') + | Zupdate(m)::s -> + strip_rec rstk (update m (h.norm,h.term)) depth n s + | s -> (None, List.rev rstk @ s) in + strip_rec [] head 0 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 -> + let _hd = update r (Cstr,FLambda(n,tys,f,e)) in + get_args n tys f e s + | Zshift k :: s -> + get_args n tys f (subs_shft (k,e)) s + | Zapp l :: s -> + let na = Array.length l in + if n == na then (Inl (subs_cons(l,e)),s) + else if n < na then (* more arguments *) + let args = Array.sub l 0 n in + let eargs = Array.sub l n (na-n) in + (Inl (subs_cons(args,e)), Zapp eargs :: s) + else (* more lambdas *) + let etys = list_skipn na tys in + get_args (n-na) etys f (subs_cons(l,e)) s + | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) + + +(* Iota reduction: extract the arguments to be passed to the Case + branches *) +let rec reloc_rargs_rec depth stk = + match stk with + Zapp args :: s -> + Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s + | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s + | _ -> stk + +let reloc_rargs depth stk = + if depth = 0 then stk else reloc_rargs_rec depth stk + +let rec drop_parameters depth n stk = + match stk with + Zapp args::s -> + let q = Array.length args in + if n > q then drop_parameters depth (n-q) s + else if n = q then reloc_rargs depth s + else + let aft = Array.sub args n (q-n) in + reloc_rargs depth (append_stack aft s) + | Zshift(k)::s -> drop_parameters (depth-k) n s + | [] -> assert (n=0); [] + | _ -> assert false (* we know that n < stack_args_size(stk) *) + + +(* Iota reduction: expansion of a fixpoint. + * Given a fixpoint and a substitution, returns the corresponding + * fixpoint body, and the substitution in which it should be + * evaluated: its first variables are the fixpoint bodies + * + * FCLOS(fix Fi {F0 := T0 .. Fn-1 := Tn-1}, S) + * -> (S. FCLOS(F0,S) . ... . FCLOS(Fn-1,S), Ti) + *) +(* does not deal with FLIFT *) +let contract_fix_vect fix = + let (thisbody, make_body, env, nfix) = + match fix with + | FFix (((reci,i),(_,_,bds as rdcl)),env) -> + (bds.(i), + (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), + env, Array.length bds) + | FCoFix ((i,(_,_,bds as rdcl)),env) -> + (bds.(i), + (fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }), + env, Array.length bds) + | _ -> assert false + in + (subs_cons(Array.init nfix make_body, env), thisbody) + + +(*********************************************************************) +(* A machine that inspects the head of a term until it finds an + atom or a subterm that may produce a redex (abstraction, + constructor, cofix, letin, constant), or a neutral term (product, + inductive) *) +let rec knh m stk = + match m.term with + | FLIFT(k,a) -> knh a (zshift k stk) + | FCLOS(t,e) -> knht e t (zupdate m stk) + | FLOCKED -> assert false + | FApp(a,b) -> knh a (append_stack b (zupdate m stk)) + | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk) + | FFix(((ri,n),(_,_,_)),_) -> + (match get_nth_arg m ri.(n) stk with + (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') + | (None, stk') -> (m,stk')) + | FCast(t,_,_) -> knh t stk +(* cases where knh stops *) + | (FFlex _|FLetIn _|FConstruct _|FEvar _| + FCoFix _|FLambda _|FRel _|FAtom _|FInd _|FProd _) -> + (m, stk) + +(* The same for pure terms *) +and knht e t stk = + match t with + | App(a,b) -> + knht e a (append_stack (mk_clos_vect e b) stk) + | Case(ci,p,t,br) -> + knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) + | Fix _ -> knh (mk_clos2 e t) stk + | Cast(a,_,_) -> knht e a stk + | Rel n -> knh (clos_rel e n) stk + | (Lambda _|Prod _|Construct _|CoFix _|Ind _| + LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> + (mk_clos2 e t, stk) + + +(************************************************************************) + +(* Computes a weak head normal form from the result of knh. *) +let rec knr info m stk = + match m.term with + | 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)) + | 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 + | None -> (set_norm m; (m,stk))) + | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> + (match ref_value_cache info (VarKey id) with + Some v -> kni info v stk + | None -> (set_norm m; (m,stk))) + | FFlex(RelKey k) when red_set info.i_flags fDELTA -> + (match ref_value_cache info (RelKey k) with + Some v -> kni info v stk + | None -> (set_norm m; (m,stk))) + | FConstruct(ind,c) when red_set info.i_flags fIOTA -> + (match strip_update_shift_app m stk with + (depth, args, Zcase(ci,_,br)::s) -> + assert (ci.ci_npar>=0); + let rargs = drop_parameters depth ci.ci_npar args in + kni info br.(c-1) (rargs@s) + | (_, cargs, Zfix(fx,par)::s) -> + let rarg = fapp_stack(m,cargs) in + let stk' = par @ append_stack [|rarg|] s in + let (fxe,fxbd) = contract_fix_vect fx.term in + knit info fxe fxbd stk' + | (_,args,s) -> (m,args@s)) + | FCoFix _ when red_set info.i_flags fIOTA -> + (match strip_update_shift_app m stk with + (_, args, ((Zcase _::_) as stk')) -> + let (fxe,fxbd) = contract_fix_vect m.term in + knit info fxe fxbd (args@stk') + | (_,args,s) -> (m,args@s)) + | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> + knit info (subs_cons([|v|],e)) bd stk + | _ -> (m,stk) + +(* Computes the weak head normal form of a term *) +and kni info m stk = + let (hm,s) = knh m stk in + knr info hm s +and knit info e t stk = + let (ht,s) = knht e t stk in + knr info ht s + +let kh info v stk = fapp_stack(kni info v stk) + +(************************************************************************) +(* Initialization and then normalization *) + +(* weak reduction *) +let whd_val info v = + with_stats (lazy (term_of_fconstr (kh info v []))) + +let inject = mk_clos (ESID 0) + +let whd_stack infos m stk = + let k = kni infos m stk in + let _ = fapp_stack k in (* to unlock Zupdates! *) + k + +(* cache of constants: the body is computed only when needed. *) +type clos_infos = fconstr infos + +let create_clos_infos flgs env = + create (fun _ -> inject) flgs env + +let unfold_reference = ref_value_cache diff --git a/checker/closure.mli b/checker/closure.mli new file mode 100644 index 00000000..fa302de6 --- /dev/null +++ b/checker/closure.mli @@ -0,0 +1,198 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*) + +(*i*) +open Pp +open Names +open Term +open Esubst +open Environ +(*i*) + +(* Flags for profiling reductions. *) +val stats : bool ref +val share : bool ref + +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 + a LetIn expression is Letin reduction *) + +type transparent_state = Idpred.t * Cpred.t + +val all_opaque : transparent_state +val all_transparent : transparent_state + +(* Sets of reduction kinds. *) +module type RedFlagsSig = sig + type reds + type red_kind + + (* The different kinds of reduction *) + val fBETA : red_kind + val fDELTA : red_kind + val fIOTA : red_kind + val fZETA : red_kind + val fCONST : constant -> red_kind + val fVAR : identifier -> red_kind + + (* No reduction at all *) + val no_red : reds + + (* Adds a reduction kind to a set *) + val red_add : reds -> red_kind -> reds + + (* Removes a reduction kind to a set *) + val red_sub : reds -> red_kind -> reds + + (* Adds a reduction kind to a set *) + val red_add_transparent : reds -> transparent_state -> reds + + (* Build a reduction set from scratch = iter [red_add] on [no_red] *) + val mkflags : red_kind list -> reds + + (* Tests if a reduction kind is set *) + val red_set : reds -> red_kind -> bool + + (* Gives the constant list *) + val red_get_const : reds -> bool * evaluable_global_reference list +end + +module RedFlags : RedFlagsSig +open RedFlags + +val beta : reds +val betaiota : reds +val betadeltaiota : reds +val betaiotazeta : reds +val betadeltaiotanolet : reds + +val unfold_red : evaluable_global_reference -> reds + +(***********************************************************************) +type table_key = + | ConstKey of constant + | VarKey of identifier + | RelKey of int + +type 'a infos +val ref_value_cache: 'a infos -> table_key -> 'a option +val info_flags: 'a infos -> reds +val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos + +(************************************************************************) +(*s Lazy reduction. *) + +(* [fconstr] is the type of frozen constr *) + +type fconstr + +(* [fconstr] can be accessed by using the function [fterm_of] and by + matching on type [fterm] *) + +type fterm = + | FRel of int + | FAtom of constr (* Metas and Sorts *) + | FCast of fconstr * cast_kind * fconstr + | FFlex of table_key + | FInd of inductive + | FConstruct of constructor + | FApp of fconstr * fconstr array + | FFix of fixpoint * fconstr subs + | FCoFix of cofixpoint * fconstr subs + | FCases of case_info * fconstr * fconstr * fconstr array + | FLambda of int * (name * constr) list * constr * fconstr subs + | FProd of name * fconstr * fconstr + | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FEvar of existential_key * fconstr array + | FLIFT of int * fconstr + | FCLOS of constr * fconstr subs + | FLOCKED + +(************************************************************************) +(*s A [stack] is a context of arguments, arguments are pushed by + [append_stack] one array at a time but popped with [decomp_stack] + one by one *) + +type stack_member = + | Zapp of fconstr array + | Zcase of case_info * fconstr * fconstr array + | Zfix of fconstr * stack + | Zshift of int + | Zupdate of fconstr + +and stack = stack_member list + +val empty_stack : stack +val append_stack : fconstr array -> stack -> stack + +val decomp_stack : stack -> (fconstr * stack) option +val array_of_stack : stack -> fconstr array +val stack_assign : stack -> int -> fconstr -> stack +val stack_args_size : stack -> int +val stack_tail : int -> stack -> stack +val stack_nth : stack -> int -> fconstr + +(* To lazy reduce a constr, create a [clos_infos] with + [create_clos_infos], inject the term to reduce with [inject]; then use + a reduction function *) + +val inject : constr -> fconstr +(* mk_atom: prevents a term from being evaluated *) +val mk_atom : constr -> fconstr + +val fterm_of : fconstr -> fterm +val term_of_fconstr : fconstr -> constr +val destFLambda : + (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + +(* Global and local constant cache *) +type clos_infos +val create_clos_infos : reds -> env -> clos_infos + +(* Reduction function *) + +(* [whd_val] is for weak head normalization *) +val whd_val : clos_infos -> fconstr -> constr + +(* [whd_stack] performs weak head normalization in a given stack. It + stops whenever a reduction is blocked. *) +val whd_stack : + clos_infos -> fconstr -> stack -> fconstr * stack + +(* Conversion auxiliary functions to do step by step normalisation *) + +(* [unfold_reference] unfolds references in a [fconstr] *) +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 + +(************************************************************************) +(*i This is for lazy debug *) + +val lift_fconstr : int -> fconstr -> fconstr +val lift_fconstr_vect : int -> fconstr array -> fconstr array + +val mk_clos : fconstr subs -> constr -> fconstr +val mk_clos_vect : fconstr subs -> constr array -> fconstr array +val mk_clos_deep : + (fconstr subs -> constr -> fconstr) -> + fconstr subs -> constr -> fconstr + +val kni: clos_infos -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> fconstr -> stack -> fconstr * stack + +val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr +val optimise_closure : fconstr subs -> constr -> fconstr subs * constr + +(* End of cbn debug section i*) diff --git a/checker/declarations.ml b/checker/declarations.ml new file mode 100644 index 00000000..71b6c9ca --- /dev/null +++ b/checker/declarations.ml @@ -0,0 +1,658 @@ +open Util +open Names +open Term + +(* Bytecode *) +type values +type reloc_table +type to_patch_substituted +(*Retroknowledge *) +type action +type retroknowledge + +type engagement = ImpredicativeSet + + +type polymorphic_arity = { + poly_param_levels : Univ.universe option list; + poly_level : Univ.universe; +} + +type constant_type = + | NonPolymorphicType of constr + | PolymorphicArity of rel_context * polymorphic_arity + + + +type substitution_domain = + MSI of mod_self_id + | MBI of mod_bound_id + | MPI of module_path + +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 'a subst_fun = substitution -> 'a -> 'a + +let fold_subst fs 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) +let add_mp mp1 mp2 = + Umap.add (MPI mp1) (mp2,None) + +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 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 + mp',resolve + | MPbound bid -> + let mp',resolve = Umap.find (MBI bid) sub in + mp',resolve + | MPdot (mp1,l) as mp2 -> + begin + try + let mp',resolve = Umap.find (MPI mp2) sub in + mp',resolve + with Not_found -> + let mp1',resolve = aux mp1 in + MPdot (mp1',l),resolve + end + | _ -> raise Not_found + in + try + 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' + +let subst_kn0 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 + +let subst_kn sub kn = + match subst_kn0 sub kn with + None -> kn + | Some kn' -> kn' + +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 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 rec map_kn f f' c = + let func = map_kn f f' in + match c with + | Const kn -> + (match f' kn with + None -> c + | Some const ->const) + | Ind (kn,i) -> + (match f kn with + None -> c + | Some kn' -> + Ind (kn',i)) + | Construct ((kn,i),j) -> + (match f kn with + None -> c + | Some kn' -> + Construct ((kn',i),j)) + | Case (ci,p,ct,l) -> + let ci_ind = + let (kn,i) = ci.ci_ind in + (match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in + let p' = func p in + let ct' = func ct in + let l' = array_smartmap func l in + if (ci.ci_ind==ci_ind && p'==p + && l'==l && ct'==ct)then c + else + Case ({ci with ci_ind = ci_ind}, + p',ct', l') + | Cast (ct,k,t) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else Cast (ct', k, t') + | Prod (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else Prod (na, t', ct') + | Lambda (na,t,ct) -> + let ct' = func ct in + let t'= func t in + if (t'==t && ct'==ct) then c + else Lambda (na, 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 + else LetIn (na, b', t', ct') + | 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) -> + 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 + 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 + else CoFix (ln,(lna,tl',bl')) + | _ -> c + +let subst_mps sub = + map_kn (subst_kn0 sub) (subst_con0 sub) + +let rec replace_mp_in_mp mpfrom mpto mp = + match mp with + | _ when mp = mpfrom -> mpto + | 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 + +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 + 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 + 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 + in + match newsetkey with + | None -> sub + | Some l -> + List.fold_left (fun s k -> Umap.add k (mp,None) s) + sub l + in + Umap.fold alias_subst subst1 empty_subst + + +let subst_substituted s r = + match !r with + | LSval a -> ref (LSlazy(s,a)) + | LSlazy(s',a) -> + let s'' = join s' s in + ref (LSlazy(s'',a)) + +let force_constr = force subst_mps + +type constr_substituted = constr substituted + +let subst_constr_subst = subst_substituted + +type constant_body = { + const_hyps : section_context; (* New: younger hyp at top *) + const_body : constr_substituted option; + const_type : constant_type; + const_body_code : to_patch_substituted; + (* const_type_code : Cemitcodes.to_patch; *) + const_constraints : Univ.constraints; + const_opaque : bool; + const_inline : bool} + +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' & t == t' then x else (id,copt',t') + +let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) + +type recarg = + | Norec + | Mrec of int + | Imbr of inductive + +let subst_recarg sub r = match r with + | Norec | Mrec _ -> r + | Imbr (kn,i) -> let kn' = subst_kn sub kn in + if kn==kn' then r else Imbr (kn',i) + +type wf_paths = recarg Rtree.t + +let mk_norec = Rtree.mk_node Norec [||] + +let mk_paths r recargs = + Rtree.mk_node r + (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) + +let dest_recarg p = fst (Rtree.dest_node p) + +let dest_subterms p = + let (_,cstrs) = Rtree.dest_node p in + Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs + +let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p + +(**********************************************************************) +(* Representation of mutual inductive types in the kernel *) +(* + Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 + ... + with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn +*) + +type monomorphic_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = +| Monomorphic of monomorphic_inductive_arity +| Polymorphic of polymorphic_arity + +type one_inductive_body = { + +(* Primitive datas *) + + (* Name of the type: [Ii] *) + mind_typename : identifier; + + (* Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : rel_context; + + (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) + mind_arity : inductive_arity; + + (* Names of the constructors: [cij] *) + mind_consnames : identifier array; + + (* Types of the constructors with parameters: [forall params, Tij], + where the Ik are replaced by de Bruijn index in the context + I1:forall params, U1 .. In:forall params, Un *) + mind_user_lc : constr array; + +(* Derived datas *) + + (* Number of expected real arguments of the type (no let, no params) *) + mind_nrealargs : int; + + (* List of allowed elimination sorts *) + mind_kelim : sorts_family list; + + (* Head normalized constructor types so that their conclusion is atomic *) + mind_nf_lc : constr array; + + (* Length of the signature of the constructors (with let, w/o params) *) + mind_consnrealdecls : int array; + + (* Signature of recursive arguments in the constructors *) + mind_recargs : wf_paths; + +(* Datas for bytecode compilation *) + + (* number of constant constructor *) + mind_nb_constant : int; + + (* number of no constant constructor *) + mind_nb_args : int; + + mind_reloc_tbl : reloc_table; + } + +type mutual_inductive_body = { + + (* The component of the mutual inductive block *) + mind_packets : one_inductive_body array; + + (* Whether the inductive type has been declared as a record *) + mind_record : bool; + + (* Whether the type is inductive or coinductive *) + mind_finite : bool; + + (* Number of types in the block *) + mind_ntypes : int; + + (* Section hypotheses on which the block depends *) + mind_hyps : section_context; + + (* Number of expected parameters *) + mind_nparams : int; + + (* Number of recursively uniform (i.e. ordinary) parameters *) + mind_nparams_rec : int; + + (* The context of parameters (includes let-in declaration) *) + mind_params_ctxt : rel_context; + + (* 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 subst_arity sub = function +| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) +| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + +(* TODO: should be changed to non-coping after Term.subst_mps *) +let subst_const_body sub cb = { + const_hyps = (assert (cb.const_hyps=[]); []); + const_body = Option.map (subst_constr_subst sub) cb.const_body; + const_type = subst_arity sub cb.const_type; + const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code; + (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) + const_constraints = cb.const_constraints; + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} + +let subst_arity sub = function +| Monomorphic s -> + Monomorphic { + mind_user_arity = subst_mps sub s.mind_user_arity; + mind_sort = s.mind_sort; + } +| Polymorphic s as x -> x + +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_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_kelim = mbp.mind_kelim; + 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 ; + 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 = + 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 } + +(* Modules *) + +type structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBalias of module_path * 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 + | SEBwith of struct_expr_body * with_declaration_body + +and with_declaration_body = + With_module_body of identifier list * module_path * Univ.constraints + | With_definition_body of identifier list * constant_body + +and module_body = + { mod_expr : struct_expr_body option; + mod_type : struct_expr_body option; + mod_constraints : Univ.constraints; + mod_alias : substitution; + mod_retroknowledge : action list} + +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} + + +let subst_with_body sub = function + | With_module_body(id,mp,cst) -> + With_module_body(id,subst_mp sub mp,cst) + | With_definition_body(id,cb) -> + With_definition_body( id,subst_const_body sub cb) + +let rec subst_modtype sub mtb = + let typ_expr' = subst_struct_expr sub mtb.typ_expr in + if typ_expr'==mtb.typ_expr then + mtb + else + { mtb with + typ_expr = typ_expr'} + +and subst_structure sub sign = + 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) + | SFBmodtype mtb -> + SFBmodtype (subst_modtype sub mtb) + | SFBalias (mp,cst) -> + SFBalias (subst_mp sub mp,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_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) + | SEBapply (meb1,meb2,cst)-> + SEBapply(subst_struct_expr sub meb1, + subst_struct_expr sub meb2, + cst) + | 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 new file mode 100644 index 00000000..fdea3383 --- /dev/null +++ b/checker/declarations.mli @@ -0,0 +1,212 @@ +open Util +open Names +open Term + +(* Bytecode *) +type values +type reloc_table +type to_patch_substituted +(*Retroknowledge *) +type action +type retroknowledge + +(* Engagements *) + +type engagement = ImpredicativeSet + +(* Constants *) + +type polymorphic_arity = { + poly_param_levels : Univ.universe option list; + poly_level : Univ.universe; +} + +type constant_type = + | NonPolymorphicType of constr + | PolymorphicArity of rel_context * polymorphic_arity + +type constr_substituted +val force_constr : constr_substituted -> constr +val from_val : constr -> constr_substituted + +type constant_body = { + const_hyps : section_context; (* New: younger hyp at top *) + const_body : constr_substituted option; + const_type : constant_type; + const_body_code : to_patch_substituted; + const_constraints : Univ.constraints; + const_opaque : bool; + const_inline : bool} + +(* Mutual inductives *) + +type recarg = + | Norec + | Mrec of int + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +val mk_norec : wf_paths +val mk_paths : recarg -> wf_paths list array -> wf_paths +val dest_subterms : wf_paths -> wf_paths list array + +type monomorphic_inductive_arity = { + mind_user_arity : constr; + mind_sort : sorts; +} + +type inductive_arity = +| Monomorphic of monomorphic_inductive_arity +| Polymorphic of polymorphic_arity + +type one_inductive_body = { + +(* Primitive datas *) + + (* Name of the type: [Ii] *) + mind_typename : identifier; + + (* Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : rel_context; + + (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) + mind_arity : inductive_arity; + + (* Names of the constructors: [cij] *) + mind_consnames : identifier array; + + (* Types of the constructors with parameters: [forall params, Tij], + where the Ik are replaced by de Bruijn index in the context + I1:forall params, U1 .. In:forall params, Un *) + mind_user_lc : constr array; + +(* Derived datas *) + + (* Number of expected real arguments of the type (no let, no params) *) + mind_nrealargs : int; + + (* List of allowed elimination sorts *) + mind_kelim : sorts_family list; + + (* Head normalized constructor types so that their conclusion is atomic *) + mind_nf_lc : constr array; + + (* Length of the signature of the constructors (with let, w/o params) *) + mind_consnrealdecls : int array; + + (* Signature of recursive arguments in the constructors *) + mind_recargs : wf_paths; + +(* Datas for bytecode compilation *) + + (* number of constant constructor *) + mind_nb_constant : int; + + (* number of no constant constructor *) + mind_nb_args : int; + + mind_reloc_tbl : reloc_table; + } + +type mutual_inductive_body = { + + (* The component of the mutual inductive block *) + mind_packets : one_inductive_body array; + + (* Whether the inductive type has been declared as a record *) + mind_record : bool; + + (* Whether the type is inductive or coinductive *) + mind_finite : bool; + + (* Number of types in the block *) + mind_ntypes : int; + + (* Section hypotheses on which the block depends *) + mind_hyps : section_context; + + (* Number of expected parameters *) + mind_nparams : int; + + (* Number of recursively uniform (i.e. ordinary) parameters *) + mind_nparams_rec : int; + + (* The context of parameters (includes let-in declaration) *) + mind_params_ctxt : rel_context; + + (* 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 structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBalias of module_path * 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 + | SEBwith of struct_expr_body * with_declaration_body + +and with_declaration_body = + With_module_body of identifier list * module_path * Univ.constraints + | With_definition_body of identifier list * constant_body + +and module_body = + { mod_expr : struct_expr_body option; + mod_type : struct_expr_body option; + mod_constraints : Univ.constraints; + mod_alias : substitution; + mod_retroknowledge : action list} + +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} + +(* 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 + +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 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 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 diff --git a/checker/environ.ml b/checker/environ.ml new file mode 100644 index 00000000..58f08bdd --- /dev/null +++ b/checker/environ.ml @@ -0,0 +1,206 @@ +open Util +open Names +open Univ +open Term +open Declarations + +type globals = { + env_constants : constant_body Cmap.t; + env_inductives : mutual_inductive_body KNmap.t; + env_modules : module_body MPmap.t; + env_modtypes : module_type_body MPmap.t; + env_alias : module_path MPmap.t } + +type stratification = { + env_universes : universes; + env_engagement : engagement option +} + +type env = { + env_globals : globals; + env_named_context : named_context; + env_rel_context : rel_context; + env_stratification : stratification; + env_imports : Digest.t MPmap.t } + +let empty_env = { + env_globals = + { env_constants = Cmap.empty; + env_inductives = KNmap.empty; + env_modules = MPmap.empty; + env_modtypes = MPmap.empty; + env_alias = MPmap.empty }; + env_named_context = []; + env_rel_context = []; + env_stratification = + { env_universes = Univ.initial_universes; + env_engagement = None}; + env_imports = MPmap.empty } + +let engagement env = env.env_stratification.env_engagement +let universes env = env.env_stratification.env_universes +let named_context env = env.env_named_context +let rel_context env = env.env_rel_context + +let set_engagement c env = + match env.env_stratification.env_engagement with + | Some c' -> if c=c' then env else error "Incompatible engagement" + | None -> + { env with env_stratification = + { env.env_stratification with env_engagement = Some c } } + +(* Digests *) + +let add_digest env dp digest = + { env with env_imports = MPmap.add (MPfile dp) digest env.env_imports } + +let lookup_digest env dp = + MPmap.find (MPfile dp) env.env_imports + +(* Rel context *) +let lookup_rel n env = + let rec lookup_rel n sign = + match n, sign with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup_rel (n-1) sign + | _, [] -> raise Not_found in + lookup_rel n env.env_rel_context + +let push_rel d env = + { env with + 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 = +(* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); + assert (env.env_rel_context = []); *) + { env with + env_named_context = d :: env.env_named_context } + +let lookup_named id env = + let rec lookup_named id = function + | (id',_,_ as decl) :: _ when id=id' -> decl + | _ :: sign -> lookup_named id sign + | [] -> raise Not_found in + lookup_named id env.env_named_context + +(* A local const is evaluable if it is defined *) + +let named_type id env = + let (_,_,t) = lookup_named id env in t + +(* Universe constraints *) +let add_constraints c env = + if c == Constraint.empty then + env + else + let s = env.env_stratification in + { 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 + +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 + { env with env_globals = new_globals } + +(* constant_type gives the type of a constant *) +let constant_type env kn = + let cb = lookup_constant kn env in + cb.const_type + +type const_evaluation_result = NoBody | Opaque + +exception NotEvaluableConst of const_evaluation_result + +let constant_value env kn = + let cb = lookup_constant kn env in + if cb.const_opaque then raise (NotEvaluableConst Opaque); + match cb.const_body with + | Some l_body -> force_constr l_body + | None -> raise (NotEvaluableConst NoBody) + +let constant_opt_value env cst = + try Some (constant_value env cst) + with NotEvaluableConst _ -> None + +(* A global const is evaluable if it is defined and not opaque *) +let evaluable_constant cst env = + try let _ = constant_value env cst in true + with Not_found | NotEvaluableConst _ -> false + +(* Mutual Inductives *) +let lookup_mind kn env = + KNmap.find kn env.env_globals.env_inductives + +let rec scrape_mind env kn = + match (lookup_mind kn env).mind_equiv with + | None -> kn + | Some kn' -> scrape_mind env kn' + +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 + { 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 new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in + 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 new_mods = MPmap.add mp mb env.env_globals.env_modules in + 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 = + MPmap.find mp env.env_globals.env_modules + +let lookup_modtype ln env = + MPmap.find ln env.env_globals.env_modtypes + +let lookup_alias mp env = + MPmap.find mp env.env_globals.env_alias diff --git a/checker/environ.mli b/checker/environ.mli new file mode 100644 index 00000000..a3f531dd --- /dev/null +++ b/checker/environ.mli @@ -0,0 +1,67 @@ +open Names +open Term + +type globals = { + env_constants : Declarations.constant_body Cmap.t; + env_inductives : Declarations.mutual_inductive_body KNmap.t; + env_modules : Declarations.module_body MPmap.t; + env_modtypes : Declarations.module_type_body MPmap.t; + env_alias : module_path MPmap.t; +} +type stratification = { + env_universes : Univ.universes; + env_engagement : Declarations.engagement option; +} +type env = { + env_globals : globals; + env_named_context : named_context; + env_rel_context : rel_context; + env_stratification : stratification; + env_imports : Digest.t MPmap.t; +} +val empty_env : env +val engagement : env -> Declarations.engagement option +val universes : env -> Univ.universes +val named_context : env -> named_context +val rel_context : env -> rel_context +val set_engagement : Declarations.engagement -> env -> env + +val add_digest : env -> dir_path -> Digest.t -> env +val lookup_digest : env -> dir_path -> Digest.t + +val lookup_rel : int -> env -> rel_declaration +val push_rel : rel_declaration -> env -> env +val push_rel_context : rel_context -> env -> env +val push_rec_types : name array * constr array * 'a -> env -> env + +val push_named : named_declaration -> env -> env +val lookup_named : identifier -> env -> named_declaration +val named_type : identifier -> env -> constr + +val add_constraints : Univ.constraints -> env -> env + +val lookup_constant : constant -> env -> Declarations.constant_body +val add_constant : constant -> Declarations.constant_body -> env -> env +val constant_type : env -> constant -> Declarations.constant_type +type const_evaluation_result = NoBody | Opaque +exception NotEvaluableConst of const_evaluation_result +val constant_value : env -> constant -> constr +val constant_opt_value : env -> constant -> constr option +val evaluable_constant : constant -> env -> bool + +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 + +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 +val lookup_alias : module_path -> env -> module_path diff --git a/checker/indtypes.ml b/checker/indtypes.ml new file mode 100644 index 00000000..8c84fb0f --- /dev/null +++ b/checker/indtypes.ml @@ -0,0 +1,527 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *) + +open Util +open Names +open Univ +open Term +open Inductive +open Reduction +open Typeops +open Pp +open Declarations +open Environ + +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) + +(* Same as noccur_between but may perform reductions. + Could be refined more... *) +let weaker_noccur_between env x nvars t = + if noccur_between x nvars t then Some t + else + let t' = whd_betadeltaiota env t in + if noccur_between x nvars t' then Some t' + else None + +let is_constructor_head t = + match fst(decompose_app t) with + | Rel _ -> true + | _ -> false + +let conv_ctxt_prefix env (ctx1:rel_context) ctx2 = + let rec chk env rctx1 rctx2 = + match rctx1, rctx2 with + (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' -> + conv env ty1 ty2; + chk (push_rel d1 env) rctx1' rctx2' + | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' -> + conv env ty1 ty2; + conv env bd1 bd2; + chk (push_rel d1 env) rctx1' rctx2' + | [],_ -> () + | _ -> failwith "non convertible contexts" in + chk env (List.rev ctx1) (List.rev ctx2) + +(************************************************************************) +(* Various well-formedness check for inductive declarations *) + +(* Errors related to inductive constructions *) +type inductive_error = + | NonPos of env * constr * constr + | NotEnoughArgs of env * constr * constr + | NotConstructor of env * constr * constr + | NonPar of env * constr * int * constr * constr + | SameNamesTypes of identifier + | SameNamesConstructors of identifier + | SameNamesOverlap of identifier list + | NotAnArity of identifier + | BadEntry + +exception InductiveError of inductive_error + +(************************************************************************) +(************************************************************************) + +(* Typing the arities and constructor types *) + +let rec sorts_of_constr_args env t = + let t = whd_betadeltaiota_nolet env t in + match t with + | Prod (name,c1,c2) -> + let varj = infer_type env c1 in + let env1 = push_rel (name,None,c1) env in + varj :: sorts_of_constr_args env1 c2 + | LetIn (name,def,ty,c) -> + let env1 = push_rel (name,Some def,ty) env in + sorts_of_constr_args env1 c + | _ when is_constructor_head t -> [] + | _ -> anomaly "infos_and_sort: not a positive constructor" + + +(* Prop and Set are small *) +let is_small_sort = function + | Prop _ -> true + | _ -> false + +let is_logic_sort s = (s = Prop Null) + +(* [infos] is a sequence of pair [islogic,issmall] for each type in + the product of a constructor or arity *) + +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 +*) +let is_unit constrsinfos = + match constrsinfos with (* One info = One constructor *) + | [|constrinfos|] -> is_logic_constr constrinfos + | [||] -> (* type without constructors *) true + | _ -> false + +let small_unit 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 check_arity arctxt = function + Monomorphic mar -> + let ar = mar.mind_user_arity in + let _ = infer_type env ar in + conv env (it_mkProd_or_LetIn (Sort mar.mind_sort) arctxt) ar; + ar + | Polymorphic par -> + check_polymorphic_arity env params par; + it_mkProd_or_LetIn (Sort(Type par.poly_level)) arctxt in + let env_arities = + Array.fold_left + (fun env_ar ind -> + let ar_ctxt = ind.mind_arity_ctxt in + let _ = check_ctxt env ar_ctxt in + conv_ctxt_prefix env params ar_ctxt; + (* 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 + failwith "bad number of real inductive arguments"; + (* 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 + upper universe will be generated *) + let id = ind.mind_typename in + let env_ar' = push_rel (Name id, None, arity) env_ar in + env_ar') + env + inds in + env_arities + +(* Allowed eliminations *) + +let check_predicativity env s small level = + match s, engagement env with + Type u, _ -> + let u' = fresh_local_univ () in + let cst = + merge_constraints (enforce_geq u' u Constraint.empty) + (universes env) in + if not (check_geq cst u' level) then + failwith "impredicative Type inductive type" + | Prop Pos, Some ImpredicativeSet -> () + | Prop Pos, _ -> + if not small then failwith "impredicative Set inductive type" + | Prop Null,_ -> () + + +let sort_of_ind = function + Monomorphic mar -> mar.mind_sort + | Polymorphic par -> Type par.poly_level + +let all_sorts = [InProp;InSet;InType] +let small_sorts = [InProp;InSet] +let logical_sorts = [InProp] + +let allowed_sorts issmall isunit s = + match family_of_sort s with + (* Type: all elimination allowed *) + | InType -> all_sorts + + (* Small Set is predicative: all elimination allowed *) + | InSet when issmall -> all_sorts + + (* Large Set is necessarily impredicative: forbids large elimination *) + | InSet -> small_sorts + + (* Unitary/empty Prop: elimination to all sorts are realizable *) + (* unless the type is large. If it is large, forbids large elimination *) + (* which otherwise allows to simulate the inconsistent system Type:Type *) + | InProp when isunit -> if issmall then all_sorts else small_sorts + + (* Other propositions: elimination only to Prop *) + | InProp -> logical_sorts + + + +let compute_elim_sorts env_ar params mib arity lc = + let inst = extended_rel_list 0 params in + let env_params = push_rel_context params env_ar in + let lc = Array.map + (fun c -> + hnf_prod_applist env_params (lift (rel_context_length params) c) inst) + lc in + let s = sort_of_ind arity in + let infos = Array.map (sorts_of_constr_args env_params) lc in + let (small,unit) = small_unit infos in + (* We accept recursive unit types... *) + let unit = unit && mib.mind_ntypes = 1 in + (* compute the max of the sorts of the products of the constructor type *) + let level = max_inductive_sort + (Array.concat (Array.to_list (Array.map Array.of_list infos))) in + check_predicativity env_ar s small level; + allowed_sorts small unit s + + +let typecheck_one_inductive env params mib mip = + (* mind_typename and mind_consnames not checked *) + (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *) + (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *) + (* mind_user_lc *) + let _ = Array.map (infer_type env) mip.mind_user_lc in + (* mind_nf_lc *) + let _ = Array.map (infer_type env) mip.mind_nf_lc in + array_iter2 (conv env) mip.mind_nf_lc mip.mind_user_lc; + (* mind_consnrealdecls *) + let check_cons_args c n = + let ctx,_ = decompose_prod_assum c in + if n <> rel_context_length ctx - rel_context_length params then + failwith "bad number of real constructor arguments" in + array_iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; + (* mind_kelim: checked by positivity criterion ? *) + let sorts = + compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in + if List.exists (fun s -> not (List.mem s sorts)) mip.mind_kelim then + failwith "elimination not allowed"; + (* mind_recargs: checked by positivity criterion *) + () + +(************************************************************************) +(************************************************************************) +(* Positivity *) + +type ill_formed_ind = + | LocalNonPos of int + | LocalNotEnoughArgs of int + | LocalNotConstructor + | LocalNonPar of int * int + +exception IllFormedInd of ill_formed_ind + +(* [mind_extract_params mie] extracts the params from an inductive types + declaration, and checks that they are all present (and all the same) + for all the given types. *) + +let mind_extract_params = decompose_prod_n_assum + +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 -> + raise (InductiveError (NonPos (env,c',Rel (kt+nbpar)))) + | LocalNotEnoughArgs kt -> + raise (InductiveError + (NotEnoughArgs (env,c',Rel (kt+nbpar)))) + | LocalNotConstructor -> + raise (InductiveError + (NotConstructor (env,c',Rel (ntyp+nbpar)))) + | LocalNonPar (n,l) -> + raise (InductiveError + (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) + +let failwith_non_pos n ntypes c = + for k = n to n + ntypes - 1 do + if not (noccurn k c) then raise (IllFormedInd (LocalNonPos (k-n+1))) + done + +let failwith_non_pos_vect n ntypes v = + Array.iter (failwith_non_pos n ntypes) v; + anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur" + +let failwith_non_pos_list n ntypes l = + List.iter (failwith_non_pos n ntypes) l; + anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur" + +(* Conclusion of constructors: check the inductive type is called with + the expected parameters *) +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 + raise (IllFormedInd (LocalNotEnoughArgs l)); + let (lpar,largs') = array_chop nparams largs in + let nhyps = List.length hyps in + let rec check k index = function + | [] -> () + | (_,Some _,_)::hyps -> check k (index+1) hyps + | _::hyps -> + match whd_betadeltaiota env lpar.(k) with + | 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 + 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 + recursive parameters *) + +let check_rec_par (env,n,_,_) hyps nrecp largs = + let (lpar,_) = list_chop nrecp largs in + let rec find index = + function + | ([],_) -> () + | (_,[]) -> + failwith "number of recursive parameters cannot be greater than the number of parameters." + | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps) + | (p::lp,_::hyps) -> + (match whd_betadeltaiota env p with + | Rel w when w = index -> find (index-1) (lp,hyps) + | _ -> failwith "bad number of recursive parameters") + in find (n-1) (lpar,List.rev hyps) + +let lambda_implicit_lift n a = + let lambda_implicit a = Lambda(Anonymous,Evar(0,[||]),a) in + iterate lambda_implicit n (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 + lc + else + let make_abs = + list_tabulate + (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps + in + Array.map (substl make_abs) lc + +(* [env] is the typing environment + [n] is the dB of the last inductive type + [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) + +let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = + let auxntyp = 1 in + let specif = lookup_mind_specif env mi in + let env' = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env specif) lpar) env in + 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 *) + let newidx = n + auxntyp in + (env', newidx, ntypes, ra_env') + +(* The recursive function that checks positivity and builds the list + of recursive arguments *) +let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc = + let 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 x,largs = decompose_app (whd_betadeltaiota env c) in + match x with + | Prod (na,b,d) -> + assert (largs = []); + (match weaker_noccur_between env n ntypes b with + None -> failwith_non_pos_list n ntypes [b] + | Some b -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) d) + | Rel k -> + (try + let (ra,rarg) = List.nth ra_env (k-1) in + (match ra with + Mrec _ -> check_rec_par ienv hyps nrecp largs + | _ -> ()); + if not (List.for_all (noccur_between n ntypes) largs) + then failwith_non_pos_list n ntypes largs + else rarg + with Failure _ | Invalid_argument _ -> mk_norec) + | Ind ind_kn -> + (* If the inductive type being defined appears in a + 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 -> + if noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs + then mk_norec + else failwith_non_pos_list n ntypes (x::largs) + + (* accesses to the environment are not factorised, but is it worth it? *) + and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = + 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 + (* 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 + 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 + (* Extends the environment with a variable corresponding to + the inductive def *) + 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 = + (* 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 + (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 = + let x,largs = decompose_app (whd_betadeltaiota env c) in + match x with + | Prod (na,b,d) -> + assert (largs = []); + 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 + check_correct_par ienv hyps (ntypes-i) largs + else + raise (IllFormedInd LocalNotConstructor) + else + if not (List.for_all (noccur_between n ntypes) largs) + then raise (IllFormedInd (LocalNonPos n)); + List.rev lrec + in check_constr_rec ienv [] c + in + let irecargs = + Array.map + (fun c -> + let _,rawc = mind_extract_params lparams c in + try + check_constructors ienv true rawc + with IllFormedInd err -> + explain_ind_err (ntypes-i) env lparams c err) + indlc + in mk_paths (Mrec i) irecargs + +let check_subtree (t1:'a) (t2:'a) = + if not (Rtree.compare_rtree (fun t1 t2 -> + let l1 = fst(Rtree.dest_node t1) in + let l2 = fst(Rtree.dest_node t2) in + if l1 = Norec || l1 = l2 then 0 else -1) + t1 t2) then + failwith "bad recursive trees" +(* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) + +let check_positivity env_ar params nrecp inds = + let ntypes = Array.length inds in + let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in + let lra_ind = List.rev (Array.to_list rc) in + let lparams = rel_context_length params in + let check_one i mip = + let ra_env = + list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in + let ienv = (env_ar, 1+lparams, ntypes, ra_env) in + check_positivity_one ienv params nrecp i mip.mind_nf_lc + 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 + +(************************************************************************) +(************************************************************************) + +let check_inductive env kn mib = + Flags.if_verbose msgnl (str " checking ind: " ++ prkn 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 ? *) + (* check mind_finite : always OK *) + (* check mind_ntypes *) + if Array.length mib.mind_packets <> mib.mind_ntypes then + error "not the right number of packets"; + (* check mind_hyps: should be empty *) + if mib.mind_hyps <> empty_named_context then + error "section context not empty"; + (* check mind_params_ctxt *) + let params = mib.mind_params_ctxt in + let _ = check_ctxt env params in + (* check mind_nparams *) + if rel_context_nhyps params <> mib.mind_nparams then + error "number the right number of parameters"; + (* mind_packets *) + (* - check arities *) + let env_ar = typecheck_arity env params mib.mind_packets in + (* - check constructor types *) + Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + (* check mind_nparams_rec: positivity condition *) + check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; + (* check 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/indtypes.mli b/checker/indtypes.mli new file mode 100644 index 00000000..b920315a --- /dev/null +++ b/checker/indtypes.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: indtypes.mli 9831 2007-05-17 18:55:42Z herbelin $ i*) + +(*i*) +open Names +open Univ +open Term +open Typeops +open Declarations +open Environ +(*i*) + +val prkn : kernel_name -> Pp.std_ppcmds +val prcon : constant -> Pp.std_ppcmds + +(*s The different kinds of errors that may result of a malformed inductive + definition. *) + +(* Errors related to inductive constructions *) +type inductive_error = + | NonPos of env * constr * constr + | NotEnoughArgs of env * constr * constr + | NotConstructor of env * constr * constr + | NonPar of env * constr * int * constr * constr + | SameNamesTypes of identifier + | SameNamesConstructors of identifier + | SameNamesOverlap of identifier list + | NotAnArity of identifier + | BadEntry + +exception InductiveError of inductive_error + +(*s The following function does checks on inductive declarations. *) + +val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env diff --git a/checker/inductive.ml b/checker/inductive.ml new file mode 100644 index 00000000..05ab5a84 --- /dev/null +++ b/checker/inductive.ml @@ -0,0 +1,913 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *) + +open Util +open Names +open Univ +open Term +open Reduction +open Type_errors +open Declarations +open Environ + +let inductive_of_constructor = fst +let index_of_constructor = snd +let ith_constructor_of_inductive ind i = (ind,i) + +type mind_specif = mutual_inductive_body * one_inductive_body + +(* raise Not_found if not an inductive type *) +let lookup_mind_specif env (kn,tyi) = + let mib = lookup_mind kn env in + if tyi >= Array.length mib.mind_packets then + error "Inductive.lookup_mind_specif: invalid inductive index"; + (mib, mib.mind_packets.(tyi)) + +let find_rectype env c = + let (t, l) = decompose_app (whd_betadeltaiota env c) in + match t with + | Ind ind -> (ind, l) + | _ -> raise Not_found + +let find_inductive env c = + let (t, l) = decompose_app (whd_betadeltaiota env c) in + match t with + | Ind ind + when (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + | _ -> raise Not_found + +let find_coinductive env c = + let (t, l) = decompose_app (whd_betadeltaiota env c) in + match t with + | Ind ind + when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l) + | _ -> raise Not_found + +let inductive_params (mib,_) = mib.mind_nparams + +(************************************************************************) + +(* Build the substitution that replaces Rels by the appropriate *) +(* inductives *) +let ind_subst mind mib = + let ntypes = mib.mind_ntypes in + let make_Ik k = Ind (mind,ntypes-k-1) in + list_tabulate make_Ik ntypes + +(* Instantiate inductives in constructor type *) +let constructor_instantiate mind mib c = + let s = ind_subst mind mib in + substl s c + +let instantiate_params full t args sign = + let fail () = + anomaly "instantiate_params: type, ctxt and args mismatch" in + let (rem_args, subs, ty) = + fold_rel_context + (fun (_,copt,_) (largs,subs,ty) -> + match (copt, largs, ty) with + | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) + | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t) + | (_,[],_) -> if full then fail() else ([], subs, ty) + | _ -> fail ()) + sign + ~init:(args,[],t) + in + if rem_args <> [] then fail(); + substl subs ty + +let instantiate_partial_params = instantiate_params false + +let full_inductive_instantiate mib params sign = + let dummy = Prop Null in + let t = mkArity (sign,dummy) in + fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) + +let full_constructor_instantiate ((mind,_),(mib,_),params) = + let inst_ind = constructor_instantiate mind mib in + (fun t -> + instantiate_params true (inst_ind t) params mib.mind_params_ctxt) + +(************************************************************************) +(************************************************************************) + +(* Functions to build standard types related to inductive *) + + +let number_of_inductives mib = Array.length mib.mind_packets +let number_of_constructors mip = Array.length mip.mind_consnames + +(* +Computing the actual sort of an applied or partially applied inductive type: + +I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a) +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..) +merge(..s'_k..) = ..s''_k.. +-------------------------------------------------------------------- +Gamma |- I_i uniformargs otherargs : phi(s''_i) + +where + +- if p=0, phi() = Prop +- if p=1, phi(s) = s +- if p<>1, phi(s) = sup(Set,s) + +Remark: Set (predicative) is encoded as Type(0) +*) + +let sort_as_univ = function +| Type u -> u +| Prop Null -> type0m_univ +| Prop Pos -> type0_univ + +let cons_subst u su subst = + try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst + with Not_found -> (u, su) :: subst + +let actualize_decl_level env lev t = + let sign,s = dest_arity env t in + mkArity (sign,lev) + +let polymorphism_on_non_applied_parameters = false + +(* Bind expected levels of parameters to actual levels *) +(* Propagate the new levels in the signature *) +let rec make_subst env = function + | (_,Some _,_ as t)::sign, exp, args -> + let ctx,subst = make_subst env (sign, exp, args) in + t::ctx, subst + | d::sign, None::exp, args -> + let args = match args with _::args -> args | [] -> [] in + let ctx,subst = make_subst env (sign, exp, args) in + d::ctx, subst + | d::sign, Some u::exp, a::args -> + (* We recover the level of the argument, but we don't change the *) + (* level in the corresponding type in the arity; this level in the *) + (* arity is a global level which, at typing time, will be enforce *) + (* to be greater than the level of the argument; this is probably *) + (* a useless extra constraint *) + let s = sort_as_univ (snd (dest_arity env a)) in + let ctx,subst = make_subst env (sign, exp, args) in + d::ctx, cons_subst u s subst + | (na,None,t as d)::sign, Some u::exp, [] -> + (* No more argument here: we instantiate the type with a fresh level *) + (* which is first propagated to the corresponding premise in the arity *) + (* (actualize_decl_level), then to the conclusion of the arity (via *) + (* the substitution) *) + let ctx,subst = make_subst env (sign, exp, []) in + if polymorphism_on_non_applied_parameters then + let s = fresh_local_univ () in + let t = actualize_decl_level env (Type s) t in + (na,None,t)::ctx, cons_subst u s subst + else + d::ctx, subst + | sign, [], _ -> + (* Uniform parameters are exhausted *) + sign,[] + | [], _, _ -> + assert false + +let instantiate_universes env ctx ar argsorts = + let args = Array.to_list argsorts in + let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in + let level = subst_large_constraints subst ar.poly_level in + ctx, + if is_type0m_univ level then Prop Null + else if is_type0_univ level then Prop Pos + else Type level + +let type_of_inductive_knowing_parameters env mip paramtyps = + match mip.mind_arity with + | Monomorphic s -> + s.mind_user_arity + | Polymorphic ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +(* Type of a (non applied) inductive type *) + +let type_of_inductive env (_,mip) = + type_of_inductive_knowing_parameters env mip [||] + +(* The max of an array of universes *) + +let cumulate_constructor_univ u = function + | Prop Null -> u + | Prop Pos -> sup type0_univ u + | Type u' -> sup u u' + +let max_inductive_sort = + Array.fold_left cumulate_constructor_univ type0m_univ + +(************************************************************************) +(* Type of a constructor *) + +let type_of_constructor cstr (mib,mip) = + let ind = inductive_of_constructor cstr in + let specif = mip.mind_user_lc in + let i = index_of_constructor cstr in + let nconstr = Array.length mip.mind_consnames in + 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 specif = mip.mind_nf_lc in + Array.map (constructor_instantiate kn mib) specif + + + +(************************************************************************) + +let error_elim_expln kp ki = + match kp,ki with + | (InType | InSet), InProp -> NonInformativeToInformative + | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) + | _ -> WrongArity + +(* Type of case predicates *) + +(* Get type of inductive, with parameters instantiated *) + +let inductive_sort_family mip = + match mip.mind_arity with + | Monomorphic s -> family_of_sort s.mind_sort + | Polymorphic _ -> InType + +let mind_arity mip = + mip.mind_arity_ctxt, inductive_sort_family mip + +let get_instantiated_arity (mib,mip) params = + let sign, s = mind_arity mip in + full_inductive_instantiate mib params sign, s + +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 build_dependent_inductive ind (_,mip) params = + let nrealargs = mip.mind_nrealargs in + applist + (Ind ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs)) + +(* 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 + 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 arsign,_ = get_instantiated_arity specif params in + let rec srec env pt ar = + let pt' = whd_betadeltaiota env pt in + match pt', ar with + | Prod (na1,a1,t), (_,None,a1')::ar' -> + (try conv env a1 a1' + with NotConvertible -> raise (LocalArity None)); + 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 + | _ -> raise (LocalArity None) 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; + true + | Sort s', [] -> + check_allowed_sort (family_of_sort s') specif; + false + | _ -> + raise (LocalArity None) + in + try srec env pj (List.rev arsign) + with LocalArity kinds -> + error_elim_arity env ind (elim_sorts specif) c (p,pj) kinds + + +(************************************************************************) +(* Type of case branches *) + +(* [p] is the predicate, [i] is the constructor number (starting from 0), + and [cty] is the type of the constructor (params not instantiated) *) +let build_branches_type ind (_,mip as specif) params dep p = + let build_one_branch i cty = + let typi = full_constructor_instantiate (ind,specif,params) cty in + let (args,ccl) = decompose_prod_assum typi in + let nargs = rel_context_length args in + let (_,allargs) = decompose_app ccl in + let (lparams,vargs) = list_chop (inductive_params specif) allargs in + let cargs = + if dep then + let cstr = ith_constructor_of_inductive ind (i+1) in + let dep_cstr = + applist (Construct cstr,lparams@extended_rel_list 0 args) in + vargs @ [dep_cstr] + else + vargs in + let base = beta_appvect (lift nargs p) (Array.of_list cargs) in + it_mkProd_or_LetIn base args in + Array.mapi build_one_branch mip.mind_nf_lc + +(* [p] is the predicate, [c] is the match object, [realargs] is the + list of real args of the inductive type *) +let build_case_type dep p c realargs = + let args = if dep then realargs@[c] else realargs in + 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 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 + let lc = build_branches_type ind specif params dep p in + let ty = build_case_type dep p c realargs in + (lc, ty) + + +(************************************************************************) +(* Checking the case annotation is relevent *) + +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 + (mib.mind_nparams <> ci.ci_npar) or + (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) + then raise (TypeError(env,WrongCaseInfo(indsp,ci))) + +(************************************************************************) +(************************************************************************) + +(* Guard conditions for fix and cofix-points *) + +(* 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 *) + +(* A powerful notion of subterm *) + +(* To each inductive definition corresponds an array describing the + structure of recursive arguments for each constructor, we call it + the recursive spec of the type (it has type recargs vect). For + checking the guard, we start from the decreasing argument (Rel n) + with its recursive spec. During checking the guardness condition, + we collect patterns variables corresponding to subterms of n, each + of them with its recursive spec. They are organised in a list lst + of type (int * recargs) list which is sorted with respect to the + first argument. +*) + +(*************************************************************) +(* Environment annotated with marks on recursive arguments *) + +(* tells whether it is a strict or loose subterm *) +type size = Large | Strict + +(* merging information *) +let size_glb s1 s2 = + match s1,s2 with + Strict, Strict -> Strict + | _ -> Large + +(* possible specifications for a term: + - Not_subterm: when the size of a term is not related to the + recursive argument of the fixpoint + - Subterm: when the term is a subterm of the recursive argument + the wf_paths argument specifies which subterms are recursive + - Dead_code: when the term has been built by elimination over an + empty type + *) + +type subterm_spec = + Subterm of (size * wf_paths) + | Dead_code + | Not_subterm + +let spec_of_tree t = + if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t) + +let subterm_spec_glb = + let glb2 s1 s2 = + match s1,s2 with + _, Dead_code -> s1 + | Dead_code, _ -> s2 + | Not_subterm, _ -> Not_subterm + | _, Not_subterm -> Not_subterm + | Subterm (a1,t1), Subterm (a2,t2) -> + if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1) + (* 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 *) + rel_min : int; + (* inductive of recarg of each fixpoint *) + inds : inductive array; + (* the recarg information of inductive family *) + recvec : wf_paths array; + (* dB of variables denoting subterms *) + genv : subterm_spec list; + } + +let make_renv env minds recarg (kn,tyi) = + let mib = lookup_mind kn env in + let mind_recvec = + Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in + { env = env; + rel_min = recarg+2; + inds = minds; + recvec = mind_recvec; + genv = [Subterm(Large,mind_recvec.(tyi))] } + +let push_var renv (x,ty,spec) = + { renv with + env = push_rel (x,None,ty) renv.env; + rel_min = renv.rel_min+1; + genv = spec:: renv.genv } + +let assign_var_spec renv (i,spec) = + { renv with genv = list_assign renv.genv (i-1) spec } + +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 = + try List.nth renv.genv (p-1) + with Failure _ | Invalid_argument _ -> Not_subterm + +(* Add a variable and mark it as strictly smaller with information [spec]. *) +let add_subterm renv (x,a,spec) = + push_var renv (x,a,spec_of_tree spec) + +let push_ctxt_renv renv ctxt = + let n = rel_context_length ctxt in + { 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 } + +let push_fix_renv renv (_,v,_ as recdef) = + let n = Array.length v in + { renv with + env = push_rec_types recdef renv.env; + rel_min = renv.rel_min+n; + genv = iterate (fun ge -> Not_subterm::ge) n renv.genv } + + +(******************************) +(* Computing the recursive subterms of a term (propagation of size + information through Cases). *) + +(* + c is a branch of an inductive definition corresponding to the spec + lrec. mind_recvec is the recursive spec of the inductive + definition of the decreasing argument n. + + case_branches_specif renv lrec lc will pass the lambdas + of c corresponding to pattern variables and collect possibly new + subterms variables and returns the bodies of the branches with the + correct envs and decreasing args. +*) + +let lookup_subterms env ind = + let (_,mip) = lookup_mind_specif env ind in + mip.mind_recargs + +(*********************************) + +(* Propagation of size information through Cases: if the matched + object is a recursive subterm then compute the information + associated to its own subterms. + Rq: if branch is not eta-long, then the recursive information + is not propagated to the missing abstractions *) +let case_branches_specif renv c_spec ind lbr = + let rec push_branch_args renv lrec c = + match lrec with + ra::lr -> + let c' = whd_betadeltaiota renv.env c in + (match c' with + Lambda(x,a,b) -> + let renv' = push_var renv (x,a,ra) in + push_branch_args renv' lr b + | _ -> (* branch not in eta-long form: cannot perform rec. calls *) + (renv,c')) + | [] -> (renv, c) in + match c_spec with + Subterm (_,t) -> + 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 -> + 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); + array_map2 (push_branch_args renv) sub_spec lbr + | Not_subterm -> Array.map (fun c -> (renv,c)) lbr + +(* [subterm_specif renv t] computes the recursive structure of [t] and + compare its size with the size of the initial recursive argument of + the fixpoint we are checking. [renv] collects such information + about variables. +*) + +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 + | Rel k -> subterm_var k renv + + | Case (ci,_,c,lbr) -> + if Array.length lbr = 0 then Dead_code + else + let c_spec = subterm_specif renv c in + let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in + let stl = + Array.map (fun (renv',br') -> subterm_specif renv' br') + lbr_spec in + subterm_spec_glb stl + + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> +(* when proving that the fixpoint f(x)=e is less than n, it is enough + to prove that e is less than n assuming f is less than n + furthermore when f is applied to a term which is strictly less than + n, one may assume that x itself is strictly less than n +*) + let (ctxt,clfix) = dest_prod renv.env typarray.(i) in + let oind = + let env' = push_rel_context ctxt renv.env in + try Some(fst(find_inductive env' clfix)) + with Not_found -> None in + (match oind with + None -> Not_subterm (* happens if fix is polymorphic *) + | Some ind -> + let nbfix = Array.length typarray in + let recargs = lookup_subterms renv.env ind in + (* pushing the fixpoints *) + let renv' = push_fix_renv renv recdef in + let renv' = + (* Why Strict here ? To be general, it could also be + Large... *) + assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + if List.length l < nbOfAbst then renv'' + else + let theDecrArg = List.nth l decrArg in + let arg_spec = subterm_specif renv theDecrArg in + assign_var_spec renv'' (1, arg_spec) in + subterm_specif renv'' strippedBody) + + | Lambda (x,a,b) -> + assert (l=[]); + subterm_specif (push_var_renv renv (x,a)) b + + (* Metas and evars are considered OK *) + | (Meta _|Evar _) -> Dead_code + + (* Other terms are not subterms *) + | _ -> Not_subterm + + +(* Check term c can be applied to one of the mutual fixpoints. *) +let check_is_subterm renv c = + match subterm_specif renv c with + Subterm (Strict,_) | Dead_code -> true + | _ -> false + +(************************************************************************) + +exception FixGuardError of env * guard_error + +let error_illegal_rec_call renv fx arg = + let (_,le_vars,lt_vars) = + List.fold_left + (fun (i,le,lt) sbt -> + match sbt with + (Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt) + | (Subterm(Large,_)) -> (i+1, i::le, lt) + | _ -> (i+1, le ,lt)) + (1,[],[]) renv.genv in + raise (FixGuardError (renv.env, + RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars))) + +let error_partial_apply renv fx = + raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) + +(* Check if [def] is a guarded fixpoint body with decreasing arg. + given [recpos], the decreasing arguments of each mutually defined + fixpoint. *) +let check_one_fix renv recpos def = + let nfi = Array.length recpos in + + (* Checks if [t] only make valid recursive calls *) + let rec check_rec_call renv t = + (* 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) *) + 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: *) + let glob = renv.rel_min+nfi-1-p in + (* the decreasing arg of the rec call: *) + let np = recpos.(glob) in + if List.length l <= np then error_partial_apply renv glob + else + (* Check the decreasing arg is smaller *) + let z = List.nth l np in + if not (check_is_subterm renv z) then + error_illegal_rec_call renv glob z + end + else + begin + match pi2 (lookup_rel p renv.env) with + | None -> + List.iter (check_rec_call renv) l + | Some c -> + try List.iter (check_rec_call renv) l + with FixGuardError _ -> check_rec_call renv (applist(c,l)) + end + + | Case (ci,p,c_0,lrest) -> + List.iter (check_rec_call renv) (c_0::p::l); + (* compute the recarg information for the arguments of + each branch *) + let c_spec = subterm_specif renv c_0 in + let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in + Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr + + (* 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 + in a1 ... am & + - 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 + S+{yp} in e + then f is guarded with respect to S in (g a1 ... am). + Eduardo 7/9/98 *) + + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + List.iter (check_rec_call renv) l; + Array.iter (check_rec_call renv) typarray; + let decrArg = recindxs.(i) in + let renv' = push_fix_renv renv recdef in + if (List.length l < (decrArg+1)) then + Array.iter (check_rec_call renv') bodies + else + Array.iteri + (fun j body -> + if i=j then + let theDecrArg = List.nth l decrArg in + let arg_spec = subterm_specif renv theDecrArg in + check_nested_fix_body renv' (decrArg+1) arg_spec body + else check_rec_call renv' body) + bodies + + | Const kn -> + if evaluable_constant kn renv.env then + try List.iter (check_rec_call renv) l + with (FixGuardError _ ) -> + check_rec_call renv(applist(constant_value renv.env kn, l)) + else List.iter (check_rec_call renv) l + + (* The cases below simply check recursively the condition on the + subterms *) + | Cast (a,_, b) -> + List.iter (check_rec_call renv) (a::b::l) + + | 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) -> + List.iter (check_rec_call renv) (a::l); + check_rec_call (push_var_renv renv (x,a)) b + + | CoFix (i,(_,typarray,bodies as recdef)) -> + List.iter (check_rec_call renv) l; + Array.iter (check_rec_call renv) typarray; + let renv' = push_fix_renv renv recdef in + Array.iter (check_rec_call renv') bodies + + | (Ind _ | Construct _ | Sort _) -> + List.iter (check_rec_call renv) l + + | Var id -> + begin + match pi2 (lookup_named id renv.env) with + | None -> + List.iter (check_rec_call renv) l + | Some c -> + try List.iter (check_rec_call renv) l + with (FixGuardError _) -> check_rec_call renv (applist(c,l)) + end + + (* l is not checked because it is considered as the meta's context *) + | (Evar _ | Meta _) -> () + + | (App _|LetIn _) -> assert false (* beta zeta reduction *) + + and check_nested_fix_body renv decr recArgsDecrArg body = + if decr = 0 then + check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body + else + match body with + | Lambda (x,a,b) -> + check_rec_call renv a; + let renv' = push_var_renv renv (x,a) in + check_nested_fix_body renv' (decr-1) recArgsDecrArg b + | _ -> anomaly "Not enough abstractions in fix body" + + in + check_rec_call renv def + + +let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = + let nbfix = Array.length bodies in + if nbfix = 0 + or Array.length nvect <> nbfix + or Array.length types <> nbfix + or Array.length names <> nbfix + or bodynum < 0 + or bodynum >= nbfix + then anomaly "Ill-formed fix term"; + let fixenv = push_rec_types recdef env in + 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, + gives the type of the k+1-eme abstraction (must be an inductive) *) + let rec check_occur env n def = + match (whd_betadeltaiota env def) with + | 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 + with Not_found -> + raise_err env i (RecursionNotOnInductiveType a) in + (mind, (env', b)) + else check_occur env' (n+1) b + else anomaly "check_one_fix: Bad occurrence of recursive call" + | _ -> raise_err env i NotEnoughAbstractionInFixBody in + check_occur fixenv 1 def in + (* Do it on every fixpoint *) + let rv = array_map2_i find_ind nvect bodies in + (Array.map fst rv, Array.map snd rv) + + +let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = + let (minds, rdef) = inductive_of_mutfix env fix in + for i = 0 to Array.length bodies - 1 do + let (fenv,body) = rdef.(i) in + let renv = make_renv fenv minds nvect.(i) minds.(i) in + try check_one_fix renv nvect body + with FixGuardError (fixenv,err) -> + error_ill_formed_rec_body fixenv err names i + done + +(* +let cfkey = Profile.declare_profile "check_fix";; +let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +*) + +(************************************************************************) +(* Co-fixpoints. *) + +exception CoFixGuardError of env * guard_error + +let anomaly_ill_typed () = + anomaly "check_one_cofix: too many arguments applied to constructor" + +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 + | _ -> + (try find_coinductive env b + with Not_found -> + raise (CoFixGuardError (env, CodomainNotInductiveType b))) + +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 + | Rel p when n <= p && p < n+nbfix -> + (* recursive call: must be guarded and no nested recursive + call allowed *) + if not alreadygrd then + 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 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) -> + if rar = mk_norec then + if noccur_with_meta n nbfix t + then process_args_of_constr (lr, lrar) + else raise (CoFixGuardError + (env,RecCallInNonRecArgOfConstructor t)) + else + let spec = dest_subterms rar in + check_rec_call env true n spec t; + process_args_of_constr (lr, lrar) + | [],_ -> () + | _ -> 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 + raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) + + | CoFix (j,(_,varit,vdefs as recdef)) -> + if (List.for_all (noccur_with_meta n nbfix) args) + 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 + raise (CoFixGuardError (env,RecCallInTypeOfDef c)) + else + raise (CoFixGuardError (env,UnguardedRecursiveCall c)) + + | Case (_,p,tm,vrest) -> + if (noccur_with_meta n nbfix p) then + 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 + raise (CoFixGuardError (env,RecCallInCaseFun c)) + else + raise (CoFixGuardError (env,RecCallInCaseArg c)) + else + raise (CoFixGuardError (env,RecCallInCasePred c)) + + | Meta _ -> () + | Evar _ -> + List.iter (check_rec_call env alreadygrd n vlra) args + + | _ -> 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 + satisfies the guarded condition *) + +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) -> + error_ill_formed_rec_body errenv err names i + done diff --git a/checker/inductive.mli b/checker/inductive.mli new file mode 100644 index 00000000..8e6d4ffb --- /dev/null +++ b/checker/inductive.mli @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*) + +(*i*) +open Names +open Term +open Declarations +open Environ +(*i*) + +(*s Extracting an inductive type from a construction *) + +val find_rectype : env -> constr -> inductive * constr list + +type mind_specif = mutual_inductive_body * one_inductive_body + +(*s Fetching information in the environment about an inductive type. + Raises [Not_found] if the inductive type is not found. *) +val lookup_mind_specif : env -> inductive -> mind_specif + +val type_of_inductive : env -> mind_specif -> constr + +(* Return type as quoted by the user *) +val type_of_constructor : constructor -> mind_specif -> constr + +val arities_of_specif : mutual_inductive -> mind_specif -> constr array + +(* [type_case_branches env (I,args) (p:A) c] computes useful types + about the following Cases expression: + <p>Cases (c :: (I args)) of b1..bn end + It computes the type of every branch (pattern variables are + introduced by products) and the type for the whole expression. + *) +val type_case_branches : + env -> inductive * constr list -> constr * constr -> constr + -> constr array * constr + +(* Check a [case_info] actually correspond to a Case expression on the + given inductive type. *) +val check_case_info : env -> inductive -> case_info -> unit + +(*s Guard conditions for fix and cofix-points. *) +val check_fix : env -> fixpoint -> unit +val check_cofix : env -> cofixpoint -> unit + +(*s Support for sort-polymorphic inductive types *) + +val type_of_inductive_knowing_parameters : + env -> one_inductive_body -> constr array -> constr + +val max_inductive_sort : sorts array -> Univ.universe + +val instantiate_universes : env -> rel_context -> + polymorphic_arity -> constr array -> rel_context * sorts + +(***************************************************************) +(* Debug *) + +type size = Large | Strict +type subterm_spec = + Subterm of (size * wf_paths) + | Dead_code + | Not_subterm +type guard_env = + { env : env; + (* dB of last fixpoint *) + rel_min : int; + (* inductive of recarg of each fixpoint *) + inds : inductive array; + (* the recarg information of inductive family *) + recvec : wf_paths array; + (* dB of variables denoting subterms *) + genv : subterm_spec list; + } + +val subterm_specif : guard_env -> constr -> subterm_spec +val case_branches_specif : guard_env -> subterm_spec -> inductive -> + constr array -> (guard_env * constr) array diff --git a/checker/main.ml b/checker/main.ml new file mode 100644 index 00000000..83b4ddd2 --- /dev/null +++ b/checker/main.ml @@ -0,0 +1,2 @@ + +let _ = Checker.start () diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml new file mode 100644 index 00000000..ecf8d633 --- /dev/null +++ b/checker/mod_checking.ml @@ -0,0 +1,398 @@ + +open Pp +open Util +open Names +open Term +open Inductive +open Reduction +open Typeops +open Indtypes +open Modops +open Subtyping +open Declarations +open Environ + +(************************************************************************) +(* Checking constants *) + +let refresh_arity ar = + let ctxt, hd = decompose_prod_assum ar in + match hd with + Sort (Type u) when not (Univ.is_univ_variable u) -> + let u' = Univ.fresh_local_univ() in + mkArity (ctxt,Type u'), + Univ.enforce_geq u' u Univ.Constraint.empty + | _ -> ar, Univ.Constraint.empty + +let check_constant_declaration env kn cb = + Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); + let env = add_constraints cb.const_constraints env in + let env' = check_named_ctxt env cb.const_hyps in + (match cb.const_type with + NonPolymorphicType ty -> + let ty, cu = refresh_arity ty in + let envty = add_constraints cu env' in + let _ = infer_type envty ty in + (match cb.const_body with + | Some bd -> + let j = infer env' (force_constr bd) in + conv_leq envty j ty + | None -> ()) + | PolymorphicArity(ctxt,par) -> + let _ = check_ctxt env ctxt in + check_polymorphic_arity env ctxt par); + add_constant kn cb env + +(************************************************************************) +(* Checking modules *) + + +let rec add_struct_expr_constraints env = function + | SEBident _ -> env + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb + + | SEBstruct (_,structure_body) -> + List.fold_left + (fun env (l,item) -> add_struct_elem_constraints env item) + env + structure_body + + | 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()); +*) + 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 + | 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 + | SFBalias (mp,Some cst) -> Environ.add_constraints cst env + | SFBalias (mp,None) -> env + | SFBmodtype mtb -> add_modtype_constraints env mtb + +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 -> + add_struct_expr_constraints env mtb + in + Environ.add_constraints mb.mod_constraints env + +and add_modtype_constraints env mtb = + add_struct_expr_constraints env mtb.typ_expr + +exception Not_path + +let path_of_mexpr = function + | SEBident mp -> mp + | _ -> raise Not_path + +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 rec list_fold_map2 f e = function + | [] -> (e,[],[]) + | h::t -> + let e',h1',h2' = f e h in + let e'',t1',t2' = list_fold_map2 f e' t in + e'',h1'::t1',h2'::t2' + + +let check_alias (s1:substitution) s2 = + if s1 <> s2 then failwith "Incorrect alias" + +let check_definition_sub env cb1 cb2 = + 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 + algorithm is not ready to handle. Anyway, generated types of + constants are functions of the body of the constant. If the + bodies are the same in environments that are subtypes one of + the other, the types are subtypes too (i.e. if Gamma <= Gamma', + 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 = + if isArity t2 then + let (ctx2,s2) = destArity t2 in + match s2 with + | Type v when not (Univ.is_univ_variable v) -> + (* The type in the interface is inferred and is made of algebraic + universes *) + begin try + let (ctx1,s1) = dest_arity env t1 in + match s1 with + | Type u when not (Univ.is_univ_variable u) -> + (* Both types are inferred, no need to recheck them. We + cheat and collapse the types to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Prop _ -> + (* The type in the interface is inferred, it may be the case + that the type in the implementation is smaller because + the body is more reduced. We safely collapse the upper + type to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Type _ -> + (* The type in the interface is inferred and the type in the + implementation is not inferred or is inferred but from a + more reduced body so that it is just a variable. Since + constraints of the form "univ <= max(...)" are not + expressible in the system of algebraic universes: we fail + (the user has to use an explicit type in the interface *) + raise Reduction.NotConvertible + with UserError _ (* "not an arity" *) -> + raise Reduction.NotConvertible end + | _ -> t1,t2 + else + (t1,t2) in + Reduction.conv_leq env t1 t2 + in + 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; + (match cb2 with + | {const_body=Some lc2;const_opaque=false} -> + let c2 = force_constr lc2 in + let c1 = match cb1.const_body with + | Some lc1 -> force_constr lc1 + | None -> assert false in + Reduction.conv env c1 c2 + | _ -> ()) + +let rec check_with env mtb with_decl = + 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 + +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 + | _ -> 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 env' = Modops.add_signature (MPself msid) before env in + match with_decl with + | With_definition_body ([],_) -> assert false + | With_definition_body ([id],c) -> + let cb = match spec with + SFBconst cb -> cb + | _ -> error_not_a_constant l + in + check_definition_sub env' c cb + | With_definition_body (_::_,_) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module l + in + begin + match old.mod_expr with + | None -> + let new_with_decl = match with_decl with + With_definition_body (_,c) -> + With_definition_body (idl,c) + | With_module_body (_,c,cst) -> + With_module_body (idl,c,cst) in + check_with_aux_def env' (type_of_mb env old) new_with_decl + | Some msb -> + error_a_generative_module_expected l + end + | _ -> anomaly "Modtyping:incorrect use of with" + with + 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) + | _ -> 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 initmsid + | i::r -> MPdot(mp_rec r,label_of_id i) + in + let env' = Modops.add_signature (MPself msid) before 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' + | _ -> 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 old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module l + in + begin + match old.mod_expr with + None -> + let new_with_decl = match with_decl with + With_definition_body (_,c) -> + With_definition_body (idl,c) + | With_module_body (_,c,cst) -> + With_module_body (idl,c,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 + | Some msb -> + error_a_generative_module_expected l + end + | _ -> anomaly "Modtyping:incorrect use of with" + with + Not_found -> error_no_such_label l + | 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 + +and check_module env mb = + let env' = add_module_constraints env mb in + 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 + | SFBconst cb -> + let c = make_con mp empty_dirpath lab in + (s,check_constant_declaration env c cb) + | SFBmind mib -> + let kn = make_kn mp empty_dirpath lab in + (s,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 + (add_module_constraints env msb)) + | SFBalias(mp2,cst) -> + (try + let mp2' = scrape_alias mp2 env in + let msb = lookup_module mp2' env in + (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias), + Option.fold_right add_constraints cst + (register_alias (MPdot(mp,lab)) mp2 env)) + with Not_found -> failwith "unkown aliased module") + | SFBmodtype mty -> + let kn = MPdot(mp, lab) in + check_module_type env mty; + (join s mty.typ_alias, + add_modtype kn mty (add_modtype_constraints env mty)) + +and check_modexpr env mse = match mse with + | SEBident mp -> + let mtb = lookup_modtype mp env in + mtb.typ_alias + | 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 + | 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 mp = + try scrape_alias (path_of_mexpr m) env + 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 + | 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 diff --git a/checker/modops.ml b/checker/modops.ml new file mode 100644 index 00000000..f79e52c2 --- /dev/null +++ b/checker/modops.ml @@ -0,0 +1,347 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*) + +(*i*) +open Util +open Pp +open Names +open Univ +open Term +open Declarations +open Environ +(*i*) + +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" + +let error_incompatible_modtypes _ _ = error "Incompatible module types" + +let error_not_equal _ _ = error "Not equal modules" + +let error_not_match l _ = + error ("Signature components for label "^string_of_label l^" do not match") + +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_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 + +let error_with_incorrect l = + error ("Incorrect constraint for label \""^(string_of_label l)^"\"") + +let error_a_generative_module_expected l = + error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ + "component of generative modules can be changed using the \"with\" " ^ + "construct.") + +let error_signature_expected mtb = + error "Signature expected" + +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) -> + (arg_id,arg_t,body_t) + | _ -> 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 rec eval_struct env = function + | SEBident mp -> + begin + 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,cst) -> + let mp' = scrape_alias mp env in + SFBalias (mp,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,cst) -> + With_module_body (idl,mp,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 + +and add_signature mp sign 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 + 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 + (* 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 + in + List.fold_left add_one env sign + +and add_module mp mb env = + 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 + | 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) + +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 " + +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 " + +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 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 diff --git a/checker/modops.mli b/checker/modops.mli new file mode 100644 index 00000000..17b063e2 --- /dev/null +++ b/checker/modops.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: modops.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*) + +(*i*) +open Util +open Names +open Univ +open Term +open Declarations +open Environ +(*i*) + +(* Various operations on modules and module types *) + +(* make the environment entry out of type *) +val module_body_of_type : module_type_body -> module_body + +val module_type_of_module : module_path option -> module_body -> + module_type_body + +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 + +(* adds a module and its components, but not the constraints *) +val add_module : module_path -> 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 update_subst : env -> module_body -> module_path -> bool * substitution + +val error_incompatible_modtypes : + module_type_body -> module_type_body -> 'a + +val error_not_match : label -> structure_field_body -> 'a + +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 + +val error_signature_expected : struct_expr_body -> 'a + +val error_not_a_constant : label -> 'a + +val error_not_a_module : label -> 'a + +val error_a_generative_module_expected : label -> 'a + +val error_application_to_not_path : struct_expr_body -> 'a diff --git a/checker/reduction.ml b/checker/reduction.ml new file mode 100644 index 00000000..49f05daf --- /dev/null +++ b/checker/reduction.ml @@ -0,0 +1,436 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *) + +open Util +open Names +open Term +open Univ +open Closure +open Esubst +open Environ + +let rec is_empty_stack = function + [] -> true + | Zupdate _::s -> is_empty_stack s + | Zshift _::s -> is_empty_stack s + | _ -> false + +(* Compute the lift to be performed on a term placed in a given stack *) +let el_stack el stk = + let n = + List.fold_left + (fun i z -> + match z with + Zshift n -> i+n + | _ -> i) + 0 + stk in + el_shft n el + +let compare_stack_shape stk1 stk2 = + let rec compare_rec bal stk1 stk2 = + match (stk1,stk2) with + ([],[]) -> bal=0 + | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2 + | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 + | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2 + | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 + | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) -> + bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 + | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> + bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 + | (_,_) -> false in + compare_rec 0 stk1 stk2 + +type lft_constr_stack_elt = + Zlapp of (lift * fconstr) array + | Zlfix of (lift * fconstr) * lft_constr_stack + | Zlcase of case_info * lift * fconstr * fconstr array +and lft_constr_stack = lft_constr_stack_elt list + +let rec zlapp v = function + Zlapp v2 :: s -> zlapp (Array.append v v2) s + | s -> Zlapp v :: s + +let pure_stack lfts stk = + let rec pure_rec lfts stk = + match stk with + [] -> (lfts,[]) + | zi::s -> + (match (zi,pure_rec lfts s) with + (Zupdate _,lpstk) -> lpstk + | (Zshift n,(l,pstk)) -> (el_shft n l, pstk) + | (Zapp a, (l,pstk)) -> + (l,zlapp (Array.map (fun t -> (l,t)) a) pstk) + | (Zfix(fx,a),(l,pstk)) -> + let (lfx,pa) = pure_rec l a in + (l, Zlfix((lfx,fx),pa)::pstk) + | (Zcase(ci,p,br),(l,pstk)) -> + (l,Zlcase(ci,l,p,br)::pstk)) in + snd (pure_rec lfts stk) + +(****************************************************************************) +(* Reduction Functions *) +(****************************************************************************) + +let whd_betaiotazeta env x = + match x with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + Prod _|Lambda _|Fix _|CoFix _) -> x + | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + +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 = + match t with + | (Sort _|Meta _|Evar _|Ind _|Construct _| + Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t + | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) + +(* Beta *) + +let beta_appvect c v = + let rec stacklam env t stack = + match t, stack with + Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl + | _ -> applist (substl env t, stack) in + stacklam [] c (Array.to_list v) + +(********************************************************************) +(* Conversion *) +(********************************************************************) + +(* Conversion utility functions *) +type 'a conversion_function = env -> 'a -> 'a -> unit + +exception NotConvertible +exception NotConvertibleVect of int + +let compare_stacks f fmind lft1 stk1 lft2 stk2 = + let rec cmp_rec pstk1 pstk2 = + match (pstk1,pstk2) with + | (z1::s1, z2::s2) -> + cmp_rec s1 s2; + (match (z1,z2) with + | (Zlapp a1,Zlapp a2) -> array_iter2 f a1 a2 + | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> + f fx1 fx2; cmp_rec a1 a2 + | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> + if not (fmind ci1.ci_ind ci2.ci_ind) then + raise NotConvertible; + f (l1,p1) (l2,p2); + array_iter2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 + | _ -> assert false) + | _ -> () in + if compare_stack_shape stk1 stk2 then + cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) + else raise NotConvertible + +(* Convertibility of sorts *) + +type conv_pb = + | CONV + | CUMUL + +let sort_cmp univ pb s0 s1 = + match (s0,s1) with + | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible + | (Prop c1, Type u) -> + (match pb with + CUMUL -> () + | _ -> raise NotConvertible) + | (Type u1, Type u2) -> + if not + (match pb with + | CONV -> check_eq univ u1 u2 + | CUMUL -> check_geq univ u2 u1) + then raise NotConvertible + | (_, _) -> raise NotConvertible + +let rec no_arg_available = function + | [] -> true + | Zupdate _ :: stk -> no_arg_available stk + | Zshift _ :: stk -> no_arg_available stk + | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk + | Zcase _ :: _ -> true + | Zfix _ :: _ -> true + +let rec no_nth_arg_available n = function + | [] -> true + | Zupdate _ :: stk -> no_nth_arg_available n stk + | Zshift _ :: stk -> no_nth_arg_available n stk + | Zapp v :: stk -> + let k = Array.length v in + if n >= k then no_nth_arg_available (n-k) stk + else false + | Zcase _ :: _ -> true + | Zfix _ :: _ -> true + +let rec no_case_available = function + | [] -> true + | Zupdate _ :: stk -> no_case_available stk + | Zshift _ :: stk -> no_case_available stk + | Zapp _ :: stk -> no_case_available stk + | Zcase _ :: _ -> false + | Zfix _ :: _ -> true + +let in_whnf (t,stk) = + match fterm_of t with + | (FLetIn _ | FCases _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | FLambda _ -> no_arg_available stk + | FConstruct _ -> no_case_available stk + | FCoFix _ -> no_case_available stk + | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk + | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true + | FLOCKED -> assert false + +(* Conversion between [lft1]term1 and [lft2]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) *) +and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = + Util.check_for_interrupt (); + (* First head reduce both terms *) + let rec whd_both (t1,stk1) (t2,stk2) = + let st1' = whd_stack infos t1 stk1 in + let st2' = whd_stack infos t2 stk2 in + (* Now, whd_stack on term2 might have modified st1 (due to sharing), + and st1 might not be in whnf anymore. If so, we iterate ccnv. *) + if in_whnf st1' then (st1',st2') else whd_both st1' st2' in + let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in + let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in + (* compute the lifts that apply to the head of the term (hd1 and hd2) *) + let el1 = el_stack lft1 v1 in + let el2 = el_stack lft2 v2 in + match (fterm_of hd1, fterm_of hd2) with + (* case of leaves *) + | (FAtom a1, FAtom a2) -> + (match a1, a2 with + | (Sort s1, Sort s2) -> + assert (is_empty_stack v1 && is_empty_stack v2); + sort_cmp univ cv_pb s1 s2 + | (Meta n, Meta m) -> + if n=m + then convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + | _ -> raise NotConvertible) + | (FEvar (ev1,args1), FEvar (ev2,args2)) -> + if ev1=ev2 then + (convert_stacks univ infos lft1 lft2 v1 v2; + convert_vect univ infos el1 el2 args1 args2) + else raise NotConvertible + + (* 2 index known to be bound to no constant *) + | (FRel n, FRel m) -> + if reloc_rel n el1 = reloc_rel m el2 + then convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + (* 2 constants, 2 local defined vars or 2 defined rels *) + | (FFlex fl1, FFlex fl2) -> + (try (* try first intensional equality *) + if fl1 = fl2 + then convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + with NotConvertible -> + (* else the oracle tells which constant is to be expanded *) + let (app1,app2) = + match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) + | None -> raise NotConvertible) in + eqappr univ cv_pb infos app1 app2) + + (* only one constant, defined var or defined rel *) + | (FFlex fl1, _) -> + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr univ cv_pb infos (lft1, whd_stack infos def1 v1) appr2 + | None -> raise NotConvertible) + | (_, FFlex fl2) -> + (match unfold_reference infos fl2 with + | Some def2 -> + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 v2) + | None -> raise NotConvertible) + + (* other constructors *) + | (FLambda _, FLambda _) -> + assert (is_empty_stack v1 && is_empty_stack v2); + let (_,ty1,bd1) = destFLambda mk_clos hd1 in + let (_,ty2,bd2) = destFLambda mk_clos hd2 in + ccnv univ CONV infos el1 el2 ty1 ty2; + ccnv univ CONV infos (el_lift el1) (el_lift el2) bd1 bd2 + + | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> + assert (is_empty_stack v1 && is_empty_stack v2); + (* Luo's system *) + ccnv univ CONV infos el1 el2 c1 c'1; + ccnv univ cv_pb infos (el_lift el1) (el_lift el2) c2 c'2 + + (* Inductive types: MutInd MutConstruct Fix Cofix *) + + | (FInd ind1, FInd ind2) -> + if mind_equiv_infos infos ind1 ind2 + then + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + | (FConstruct (ind1,j1), FConstruct (ind2,j2)) -> + if j1 = j2 && mind_equiv_infos infos ind1 ind2 + then + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) -> + if op1 = op2 + then + let n = Array.length cl1 in + let fty1 = Array.map (mk_clos e1) tys1 in + let fty2 = Array.map (mk_clos e2) tys2 in + 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 + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2; + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> + if op1 = op2 + then + let n = Array.length cl1 in + let fty1 = Array.map (mk_clos e1) tys1 in + let fty2 = Array.map (mk_clos e2) tys2 in + 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 + (el_liftn n el1) (el_liftn n el2) fcl1 fcl2; + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) + | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | (FLOCKED,_) | (_,FLOCKED) ) -> assert false + + (* In all other cases, terms are not convertible *) + | _ -> raise NotConvertible + +and convert_stacks univ infos lft1 lft2 stk1 stk2 = + compare_stacks + (fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2) + (mind_equiv_infos infos) + lft1 stk1 lft2 stk2 + +and convert_vect univ infos lft1 lft2 v1 v2 = + array_iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2 + +let clos_fconv cv_pb env t1 t2 = + let infos = create_clos_infos betaiotazeta env in + let univ = universes env in + ccnv univ cv_pb infos ELID ELID (inject t1) (inject t2) + +let fconv cv_pb env t1 t2 = + if eq_constr t1 t2 then () + else clos_fconv cv_pb env t1 t2 + +let conv_cmp = fconv +let conv = fconv CONV +let conv_leq = fconv CUMUL + +let conv_leq_vecti env v1 v2 = + array_fold_left2_i + (fun i _ t1 t2 -> + (try conv_leq env t1 t2 + with (NotConvertible|Invalid_argument _) -> + raise (NotConvertibleVect i)); + ()) + () + v1 + v2 + +(* option for conversion *) + +let vm_conv = ref fconv +let set_vm_conv f = vm_conv := f +let vm_conv cv_pb env t1 t2 = + try + !vm_conv cv_pb env t1 t2 + with Not_found | Invalid_argument _ -> + (* If compilation fails, fall-back to closure conversion *) + clos_fconv cv_pb env t1 t2 + +(********************************************************************) +(* Special-Purpose Reduction *) +(********************************************************************) + +(* pseudo-reduction rule: + * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * with an HNF on the first argument to produce a product. + * if this does not work, then we use the string S as part of our + * error message. *) + +let hnf_prod_app env t n = + match whd_betadeltaiota env t with + | Prod (_,_,b) -> subst1 n b + | _ -> anomaly "hnf_prod_app: Need a product" + +let hnf_prod_applist env t nl = + List.fold_left (hnf_prod_app env) t nl + +(* Dealing with arities *) + +let dest_prod env = + let rec decrec env m c = + let t = whd_betadeltaiota env c in + match t with + | Prod (n,a,c0) -> + let d = (n,None,a) in + decrec (push_rel d env) (d::m) c0 + | _ -> m,t + in + decrec env empty_rel_context + +(* The same but preserving lets *) +let dest_prod_assum env = + let rec prodec_rec env l ty = + let rty = whd_betadeltaiota_nolet env ty in + match rty with + | Prod (x,t,c) -> + let d = (x,None,t) in + prodec_rec (push_rel d env) (d::l) c + | LetIn (x,b,t,c) -> + let d = (x,Some b,t) in + prodec_rec (push_rel d env) (d::l) c + | Cast (c,_,_) -> prodec_rec env l c + | _ -> l,rty + in + prodec_rec env empty_rel_context + +let dest_arity env c = + let l, c = dest_prod_assum env c in + match c with + | Sort s -> l,s + | _ -> error "not an arity" + +let is_arity env c = + try + let _ = dest_arity env c in + true + with UserError _ -> false + diff --git a/checker/reduction.mli b/checker/reduction.mli new file mode 100644 index 00000000..eb50ae32 --- /dev/null +++ b/checker/reduction.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) + +(*i*) +open Term +open Environ +(*i*) + +(************************************************************************) +(*s Reduction functions *) + +val whd_betaiotazeta : env -> constr -> constr +val whd_betadeltaiota : env -> constr -> constr +val whd_betadeltaiota_nolet : env -> constr -> constr + +(************************************************************************) +(*s conversion functions *) + +exception NotConvertible +exception NotConvertibleVect of int +type 'a conversion_function = env -> 'a -> 'a -> unit + +type conv_pb = CONV | CUMUL + +val conv : constr conversion_function +val conv_leq : constr conversion_function +val conv_leq_vecti : constr array conversion_function + +val vm_conv : conv_pb -> constr conversion_function + +(************************************************************************) + +(* Builds an application node, reducing beta redexes it may produce. *) +val beta_appvect : constr -> constr array -> constr + +(* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) +val hnf_prod_applist : env -> constr -> constr list -> constr + + +(************************************************************************) +(*s Recognizing products and arities modulo reduction *) + +val dest_prod : env -> constr -> rel_context * constr +val dest_prod_assum : env -> constr -> rel_context * constr + +val dest_arity : env -> constr -> arity +val is_arity : env -> constr -> bool diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml new file mode 100644 index 00000000..4b156e7e --- /dev/null +++ b/checker/safe_typing.ml @@ -0,0 +1,137 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *) + +open Pp +open Util +open Names +open Declarations +open Environ +open Mod_checking + +(************************************************************************) +(* + * Global environment + *) + +let genv = ref empty_env +let reset () = genv := empty_env +let get_env () = !genv + +let set_engagement c = + genv := set_engagement c !genv + +(* 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_module_constraints env mb in + let env = Modops.add_module mp mb env in + genv := add_digest env dp digest + +(* Check that the engagement expected by a library matches the initial one *) +let check_engagement env c = + match engagement env, c with + | Some ImpredicativeSet, Some ImpredicativeSet -> () + | _, None -> () + | _, Some ImpredicativeSet -> + error "Needs option -impredicative-set" + +(* Libraries = Compiled modules *) + +let report_clash f caller dir = + let msg = + str "compiled library " ++ str(string_of_dirpath caller) ++ + spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ + str(string_of_dirpath dir) ++ fnl() in + f msg + + +let check_imports f caller env needed = + let check (dp,stamp) = + try + let actual_stamp = lookup_digest env dp in + if stamp <> actual_stamp then report_clash f caller dp + with Not_found -> + error ("Reference to unknown module " ^ (string_of_dirpath dp)) + in + List.iter check needed + + + +(* Remove the body of opaque constants in modules *) +(* also remove mod_expr ? *) +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 } + +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 + | SFBmodule m -> SFBmodule (lighten_module m) + | SFBmodtype m -> SFBmodtype + ({m with + typ_expr = lighten_modexpr m.typ_expr})) + in + List.map lighten_body struc + +and lighten_modexpr = function + | SEBfunctor (mbid,mty,mexpr) -> + SEBfunctor (mbid, + ({mty with + typ_expr = lighten_modexpr mty.typ_expr}), + lighten_modexpr mexpr) + | SEBident mp as x -> x + | SEBstruct (msid, struc) -> + SEBstruct (msid, lighten_struct struc) + | SEBapply (mexpr,marg,u) -> + SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) + | SEBwith (seb,wdcl) -> + SEBwith (lighten_modexpr seb,wdcl) + +let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) + + +type compiled_library = + dir_path * + module_body * + (dir_path * Digest.t) list * + engagement option + +(* This function should append a certificate to the .vo file. + The digest must be part of the certicate to rule out attackers + that could change the .vo file between the time it was read and + the time the stamp is written. + For the moment, .vo are not signed. *) +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 = + Validate.val_vo (Obj.repr 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 env 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 env = !genv in + check_imports (errorlabstrm"unsafe_import") dp env depends; + check_engagement env engmt; + (* We drop proofs once checked *) +(* let mb = lighten_module mb in*) + full_add_module dp mb digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli new file mode 100644 index 00000000..12fdbfce --- /dev/null +++ b/checker/safe_typing.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: safe_typing.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*) + +(*i*) +open Names +open Term +open Environ +(*i*) + +val reset : unit -> unit +val get_env : unit -> env + +(* exporting and importing modules *) +type compiled_library + +val set_engagement : Declarations.engagement -> unit +val import : + System.physical_path -> compiled_library -> Digest.t -> unit +val unsafe_import : + System.physical_path -> compiled_library -> Digest.t -> unit diff --git a/checker/subtyping.ml b/checker/subtyping.ml new file mode 100644 index 00000000..fb95b606 --- /dev/null +++ b/checker/subtyping.ml @@ -0,0 +1,388 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*) + +(*i*) +open Util +open Names +open Univ +open Term +open Declarations +open Environ +open Reduction +open Inductive +open Modops +(*i*) +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 = + | 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 + +(* adds above information about one mutual inductive: all types and + constructors *) + +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 + (fun i id map -> + Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + oib.mind_consnames + map + in + Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map + in + array_fold_right_i add_nameobjects_of_one mib.mind_packets map + + +(* creates namedobject map for the whole signature *) + +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 + | SFBmodule mb -> add_map (Module mb) + | SFBmodtype mtb -> add_map (Modtype mtb) + | SFBalias (mp,cst) -> add_map (Alias mp) + in + List.fold_right add_one list Labmap.empty + +let check_conv_error error f env a1 a2 = + try + f env a1 a2 + with + 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 error () = error_not_match l spec2 in + let check_conv f = check_conv_error error f in + let mib1 = + match info1 with + | IndType ((_,0), mib) -> mib + | _ -> error () + 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. + + 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 + universe in the conclusion of t1 has an bounding universe in + the conclusion of t2, so that we don't need to check the + subtyping of the conclusions of t1 and t2. + + Even if we'd like to recheck it, the inference of constraints + is not designed to deal with algebraic constraints of the form + max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy + to recheck it (in short, we would need the actual graph of + constraints as input while type checking is currently designed + to output a set of constraints instead) *) + + (* So we cheat and replace the subtyping problem on algebraic + constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n) + (that we know are necessary true) by trivial constraints that + the constraint generator knows how to deal with *) + + let (ctx1,s1) = dest_arity env t1 in + let (ctx2,s2) = dest_arity env t2 in + let s1,s2 = + match s1, s2 with + | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null + | (Prop _, Type _) | (Type _,Prop _) -> error () + | _ -> (s1, s2) in + check_conv conv_leq env + (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + in + + let check_packet p1 p2 = + let check f = if f p1 <> f p2 then error () in + check (fun p -> p.mind_consnames); + check (fun p -> p.mind_typename); + (* nf_lc later *) + (* nf_arity later *) + (* user_lc ignored *) + (* user_arity ignored *) + check (fun p -> p.mind_nrealargs); + (* kelim ignored *) + (* listrec ignored *) + (* finite done *) + (* nparams done *) + (* params_ctxt done because part of the inductive types *) + (* Don't check the sort of the type if polymorphic *) + check_inductive_type env + (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) + in + let check_cons_types i p1 p2 = + array_iter2 (check_conv conv env) + (arities_of_specif kn (mib1,p1)) + (arities_of_specif kn (mib2,p2)) + in + let check f = if f mib1 <> f mib2 then error () in + 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 + && Array.length mib2.mind_packets >= 1); + + (* Check that the expected numbers of uniform parameters are the same *) + (* No need to check the contexts of parameters: it is checked *) + (* at the time of checking the inductive arities in check_packet. *) + (* Notice that we don't expect the local definitions to match: only *) + (* the inductive types and constructors types have to be convertible *) + check (fun mib -> mib.mind_nparams); + + begin + match mib2.mind_equiv with + | None -> () + | 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; + (* 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 + | Prod(n,_,t) -> n::(names_prod_letin t) + | LetIn(n,_,_,t) -> n::(names_prod_letin t) + | Cast(t,_,_) -> names_prod_letin t + | _ -> [] + 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); + check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); + end; + (* we first check simple things *) + array_iter2 check_packet mib1.mind_packets mib2.mind_packets; + (* and constructor types in the end *) + let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets + in () + +let check_constant env msid1 l info1 cb2 spec2 = + let error () = error_not_match l spec2 in + let check_conv f = check_conv_error error f in + 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 + algorithm is not ready to handle. Anyway, generated types of + constants are functions of the body of the constant. If the + bodies are the same in environments that are subtypes one of + the other, the types are subtypes too (i.e. if Gamma <= Gamma', + 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 = + if isArity t2 then + let (ctx2,s2) = destArity t2 in + match s2 with + | Type v when not (is_univ_variable v) -> + (* The type in the interface is inferred and is made of algebraic + universes *) + begin try + let (ctx1,s1) = dest_arity env t1 in + match s1 with + | Type u when not (is_univ_variable u) -> + (* Both types are inferred, no need to recheck them. We + cheat and collapse the types to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Prop _ -> + (* The type in the interface is inferred, it may be the case + that the type in the implementation is smaller because + the body is more reduced. We safely collapse the upper + type to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Type _ -> + (* The type in the interface is inferred and the type in the + implementation is not inferred or is inferred but from a + more reduced body so that it is just a variable. Since + constraints of the form "univ <= max(...)" are not + expressible in the system of algebraic universes: we fail + (the user has to use an explicit type in the interface *) + error () + with UserError _ (* "not an arity" *) -> + error () end + | _ -> t1,t2 + else + (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.")); + 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 + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv conv_leq env arity1 typ2 + | IndConstr (((kn,i),j) as cstr,mind1) -> + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ + "instantiated by a constructor. Hint: you can rename the " ^ + "constructor and give a definition to map the old name to the new " ^ + "name.")); + assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; + if cb2.const_body <> None then error () ; + let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in + let ty2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv conv env ty1 ty2 + | _ -> 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 + + +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 + 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 + 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 -> + begin + match info1 with + | Module msb -> check_modules env msid1 l msb msb2 + | Alias mp ->let msb = + {mod_expr = Some (SEBident mp); + mod_type = Some (eval_struct env (SEBident mp)); + 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,_) -> + begin + match info1 with + | Alias mp1 -> check_modpath_equiv env mp mp1 + | Module msb -> + let msb1 = + {mod_expr = Some (SEBident mp); + mod_type = Some (eval_struct env (SEBident mp)); + mod_constraints = Constraint.empty; + mod_alias = (lookup_modtype mp env).typ_alias; + mod_retroknowledge = []} in + check_modules env msid1 l msb msb1 + | _ -> error_not_match l spec2 + end + | SFBmodtype mtb2 -> + let mtb1 = + match info1 with + | Modtype mtb -> mtb + | _ -> error_not_match l spec2 + in + check_modtypes env mtb1 mtb2 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), + SEBfunctor (arg_id2,arg_t2,body_t2) -> + check_modtypes env arg_t2 arg_t1 equiv; + (* contravariant *) + let env = + add_module (MPbound arg_id2) (module_body_of_type 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 + in + check_structure env (eval_struct env body_t1') + (eval_struct env body_t2) equiv + | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + in + if mtb1'== mtb2' then () + else check_structure env mtb1' mtb2' equiv + +let check_subtypes env sup super = + (*if sup<>super then*) + check_modtypes env sup super false + +let check_equal env sup super = + (*if sup<>super then*) + check_modtypes env sup super true diff --git a/checker/subtyping.mli b/checker/subtyping.mli new file mode 100644 index 00000000..10842252 --- /dev/null +++ b/checker/subtyping.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) + +(*i*) +open Univ +open Term +open Declarations +open Environ +(*i*) + +val check_subtypes : env -> module_type_body -> module_type_body -> unit +val check_equal : env -> module_type_body -> module_type_body -> unit + + diff --git a/checker/term.ml b/checker/term.ml new file mode 100644 index 00000000..45568a59 --- /dev/null +++ b/checker/term.ml @@ -0,0 +1,462 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *) + +(* This module instantiates the structure of generic deBruijn terms to Coq *) + +open Util +open Pp +open Names +open Univ +open Esubst + +(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) + +type existential_key = int +type metavariable = int + +(* This defines the strategy to use for verifiying a Cast *) + +(* This defines Cases annotations *) +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | + RegularStyle +type case_printing = + { ind_nargs : int; (* number of real args of the inductive type *) + style : case_style } +type case_info = + { ci_ind : inductive; + ci_npar : int; + ci_cstr_nargs : int array; (* number of real args of each constructor *) + ci_pp_info : case_printing (* not interpreted by the kernel *) + } + +(* Sorts. *) + +type contents = Pos | Null + +type sorts = + | Prop of contents (* proposition types *) + | Type of universe + +type sorts_family = InProp | InSet | InType + +let family_of_sort = function + | Prop Null -> InProp + | Prop Pos -> InSet + | Type _ -> InType + +(********************************************************************) +(* Constructions as implemented *) +(********************************************************************) + +(* [constr array] is an instance matching definitional [named_context] in + the same order (i.e. last argument first) *) +type 'constr pexistential = existential_key * 'constr array +type 'constr prec_declaration = + name array * 'constr array * 'constr array +type 'constr pfixpoint = + (int array * int) * 'constr prec_declaration +type 'constr pcofixpoint = + int * 'constr prec_declaration + +type cast_kind = VMcast | DEFAULTcast + +(*s*******************************************************************) +(* The type of constructions *) + +type constr = + | Rel of int + | Var of identifier + | Meta of metavariable + | Evar of constr pexistential + | Sort of sorts + | Cast of constr * cast_kind * constr + | Prod of name * constr * constr + | Lambda of name * constr * constr + | LetIn of name * constr * constr * constr + | App of constr * constr array + | Const of constant + | Ind of inductive + | Construct of constructor + | Case of case_info * constr * constr * constr array + | Fix of constr pfixpoint + | CoFix of constr pcofixpoint + +type existential = constr pexistential +type rec_declaration = constr prec_declaration +type fixpoint = constr pfixpoint +type cofixpoint = constr pcofixpoint + +let rec strip_outer_cast c = match c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c + +let rec collapse_appl c = match c with + | 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) + | _ -> App (f,cl2) + in + collapse_rec f cl + | _ -> c + +let decompose_app c = + match collapse_appl c with + | App (f,cl) -> (f, Array.to_list cl) + | _ -> (c,[]) + + +let applist (f,l) = App (f, Array.of_list l) + + +(****************************************************************************) +(* Functions for dealing with constr terms *) +(****************************************************************************) + +(*********************) +(* Occurring *) +(*********************) + +let iter_constr_with_binders g f n c = match c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> () + | Cast (c,_,t) -> f n c; f n t + | Prod (_,t,c) -> f n t; f (g n) c + | Lambda (_,t,c) -> f n t; f (g n) c + | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c + | 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)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + | CoFix (_,(_,tl,bl)) -> + Array.iter (f n) tl; + Array.iter (f (iterate g (Array.length tl) n)) bl + +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 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 + try closed_rec n c; true with LocalOccur -> false + +(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) + +let closed0 = closedn 0 + +(* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) + +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 + 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 + for n <= p < n+m *) + +let noccur_between n m term = + let rec occur_rec n c = match c with + | Rel(p) -> if n<=p && p<n+m then raise LocalOccur + | _ -> iter_constr_with_binders succ occur_rec n c + in + try occur_rec n term; true with LocalOccur -> false + +(* Checking function for terms containing existential variables. + The function [noccur_with_meta] considers the fact that + each existential variable (as well as each isevar) + in the term appears applied to its local context, + which may contain the CoFix variables. These occurrences of CoFix variables + are not considered *) + +let noccur_with_meta n m term = + let rec occur_rec n c = match c with + | Rel p -> if n<=p & p<n+m then raise LocalOccur + | App(f,cl) -> + (match f with + | (Cast (Meta _,_,_)| Meta _) -> () + | _ -> iter_constr_with_binders succ occur_rec n c) + | Evar (_, _) -> () + | _ -> iter_constr_with_binders succ occur_rec n c + in + try (occur_rec n term; true) with LocalOccur -> false + + +(*********************) +(* Lifting *) +(*********************) + +let map_constr_with_binders g f l c = match c with + | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ + | Construct _) -> c + | Cast (c,k,t) -> Cast (f l c, k, f l t) + | Prod (na,t,c) -> Prod (na, f l t, f (g l) c) + | Lambda (na,t,c) -> Lambda (na, f l t, f (g l) c) + | LetIn (na,b,t,c) -> LetIn (na, f l b, f l t, f (g l) c) + | App (c,al) -> App (f l c, Array.map (f l) al) + | Evar (e,al) -> Evar (e, Array.map (f l) al) + | Case (ci,p,c,bl) -> Case (ci, f l p, f l c, Array.map (f l) bl) + | Fix (ln,(lna,tl,bl)) -> + let l' = iterate g (Array.length tl) l in + Fix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + | CoFix(ln,(lna,tl,bl)) -> + let l' = iterate g (Array.length tl) l in + CoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) + +(* The generic lifting function *) +let rec exliftn el c = match c with + | Rel i -> Rel(reloc_rel i el) + | _ -> map_constr_with_binders el_lift exliftn el c + +(* Lifting the binding depth across k bindings *) + +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 + we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel + M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) + +(* 1st : general case *) +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo: info; sit: 'a } + +let rec lift_substituend depth s = + match s.sinfo with + | Closed -> s.sit + | Open -> lift depth s.sit + | Unknown -> + s.sinfo <- if closed0 s.sit then Closed else Open; + lift_substituend depth s + +let make_substituend c = { sinfo=Unknown; sit=c } + +let substn_many lamv n c = + let lv = Array.length lamv in + if lv = 0 then c + 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 + substrec n c + +let substnl laml n = + substn_many (Array.map make_substituend (Array.of_list laml)) n +let substl laml = substnl laml 0 +let subst1 lam = substl [lam] + + +(***************************************************************************) +(* Type of assumptions and contexts *) +(***************************************************************************) + +type named_declaration = identifier * constr option * constr +type rel_declaration = name * constr option * constr + +let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty) +let map_rel_declaration = map_named_declaration + +let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) +let fold_rel_declaration = fold_named_declaration + + +type named_context = named_declaration list +let empty_named_context = [] +let fold_named_context f l ~init = List.fold_right f l init + +type section_context = named_context + +type rel_context = rel_declaration list +let empty_rel_context = [] +let rel_context_length = List.length +let rel_context_nhyps hyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 hyps +let fold_rel_context f l ~init = List.fold_right f l init + +let map_context f l = + let map_decl (n, body_o, typ as decl) = + let body_o' = Option.smartmap f body_o in + let typ' = f typ in + if body_o' == body_o && typ' == typ then decl else + (n, body_o', typ') + in + list_smartmap map_decl l + +let map_rel_context = map_context + +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 + +(* Iterate lambda abstractions *) + +(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *) +let compose_lam l b = + let rec lamrec = function + | ([], b) -> b + | ((v,t)::l, b) -> lamrec (l, Lambda (v,t,b)) + 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 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 + lamdec_rec [] + +(* Decompose lambda abstractions and lets, until finding n + abstractions *) +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 + | 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 + +(* Iterate products, with or without lets *) + +(* Constructs either [(x:t)c] or [[x=b:t]c] *) +let mkProd_or_LetIn (na,body,t) c = + match body with + | None -> Prod (na, t, c) + | Some b -> LetIn (na, b, t, c) + +let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) + +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 + 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 = + if n=0 then l,c + 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 + prodec_rec empty_rel_context n + + +(***************************) +(* Other term constructors *) +(***************************) + +type arity = rel_context * sorts + +let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign + +let destArity = + 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 + | Sort s -> l,s + | _ -> anomaly "destArity: not an arity" + in + prodec_rec [] + +let rec isArity c = + match c with + | Prod (_,_,c) -> isArity c + | LetIn (_,b,_,c) -> isArity (subst1 b c) + | Cast (c,_,_) -> isArity c + | Sort _ -> true + | _ -> false + +(*******************************) +(* alpha conversion functions *) +(*******************************) + +(* alpha conversion : ignore print names and casts *) + +let compare_constr f t1 t2 = + match t1, t2 with + | Rel n1, Rel n2 -> n1 = n2 + | Meta m1, Meta m2 -> m1 = m2 + | Var id1, Var id2 -> id1 = id2 + | Sort s1, Sort s2 -> s1 = s2 + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2 + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2 + | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2 + | App (c1,l1), App (c2,l2) -> + 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 (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 + | 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)) -> + ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> + ln1 = ln2 & array_for_all2 f tl1 tl2 & array_for_all2 f bl1 bl2 + | _ -> false + +let rec eq_constr m n = + (m==n) or + compare_constr eq_constr m n + +let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) diff --git a/checker/term.mli b/checker/term.mli new file mode 100644 index 00000000..30a2c03a --- /dev/null +++ b/checker/term.mli @@ -0,0 +1,111 @@ +open Names + +type existential_key = int +type metavariable = int +type case_style = + LetStyle + | IfStyle + | LetPatternStyle + | MatchStyle + | RegularStyle +type case_printing = { ind_nargs : int; style : case_style; } +type case_info = { + ci_ind : inductive; + ci_npar : int; + ci_cstr_nargs : int array; + ci_pp_info : case_printing; +} +type contents = Pos | Null +type sorts = Prop of contents | Type of Univ.universe +type sorts_family = InProp | InSet | InType +val family_of_sort : sorts -> sorts_family +type 'a pexistential = existential_key * 'a array +type 'a prec_declaration = name array * 'a array * 'a array +type 'a pfixpoint = (int array * int) * 'a prec_declaration +type 'a pcofixpoint = int * 'a prec_declaration +type cast_kind = VMcast | DEFAULTcast +type constr = + Rel of int + | Var of identifier + | Meta of metavariable + | Evar of constr pexistential + | Sort of sorts + | Cast of constr * cast_kind * constr + | Prod of name * constr * constr + | Lambda of name * constr * constr + | LetIn of name * constr * constr * constr + | App of constr * constr array + | Const of constant + | Ind of inductive + | Construct of constructor + | Case of case_info * constr * constr * constr array + | Fix of constr pfixpoint + | CoFix of constr pcofixpoint +type existential = constr pexistential +type rec_declaration = constr prec_declaration +type fixpoint = constr pfixpoint +type cofixpoint = constr pcofixpoint +val strip_outer_cast : constr -> constr +val collapse_appl : constr -> constr +val decompose_app : constr -> constr * constr list +val applist : constr * constr list -> constr +val iter_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +exception LocalOccur +val closedn : int -> constr -> bool +val closed0 : constr -> bool +val noccurn : int -> constr -> bool +val noccur_between : int -> int -> constr -> bool +val noccur_with_meta : int -> int -> constr -> bool +val map_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr +val exliftn : Esubst.lift -> constr -> constr +val liftn : int -> int -> constr -> constr +val lift : int -> constr -> constr +type info = Closed | Open | Unknown +type 'a substituend = { mutable sinfo : info; sit : 'a; } +val lift_substituend : int -> constr substituend -> constr +val make_substituend : 'a -> 'a substituend +val substn_many : constr substituend array -> int -> constr -> constr +val substnl : constr list -> int -> constr -> constr +val substl : constr list -> constr -> constr +val subst1 : constr -> constr -> constr + +type named_declaration = identifier * constr option * constr +type rel_declaration = name * constr option * constr +val map_named_declaration : + (constr -> constr) -> named_declaration -> named_declaration +val map_rel_declaration : + (constr -> constr) -> rel_declaration -> rel_declaration +val fold_named_declaration : + (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a +val fold_rel_declaration : + (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a +type named_context = named_declaration list +val empty_named_context : named_context +val fold_named_context : + (named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a +type section_context = named_context +type rel_context = rel_declaration list +val empty_rel_context : rel_context +val rel_context_length : rel_context -> int +val rel_context_nhyps : rel_context -> int +val fold_rel_context : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a +val map_context : (constr -> constr) -> named_context -> named_context +val map_rel_context : (constr -> constr) -> rel_context -> rel_context +val extended_rel_list : int -> rel_context -> constr list +val compose_lam : (name * constr) list -> constr -> constr +val decompose_lam : constr -> (name * constr) list * constr +val decompose_lam_n_assum : int -> constr -> rel_context * constr +val mkProd_or_LetIn : name * constr option * constr -> constr -> constr +val it_mkProd_or_LetIn : constr -> rel_context -> constr +val decompose_prod_assum : constr -> rel_context * constr +val decompose_prod_n_assum : int -> constr -> rel_context * constr + +type arity = rel_context * sorts +val mkArity : arity -> constr +val destArity : constr -> arity +val isArity : constr -> bool +val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool +val eq_constr : constr -> constr -> bool diff --git a/checker/type_errors.ml b/checker/type_errors.ml new file mode 100644 index 00000000..a96bba6a --- /dev/null +++ b/checker/type_errors.ml @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *) + +open Names +open Term +open Environ + +type unsafe_judgment = constr * constr + +let nf_betaiota c = c + +(* Type errors. *) + +type guard_error = + (* Fixpoints *) + | NotEnoughAbstractionInFixBody + | RecursionNotOnInductiveType of constr + | RecursionOnIllegalTerm of int * constr * int list * int list + | NotEnoughArgumentsForFixCall of int + (* CoFixpoints *) + | CodomainNotInductiveType of constr + | NestedRecursiveOccurrences + | UnguardedRecursiveCall of constr + | RecCallInTypeOfAbstraction of constr + | RecCallInNonRecArgOfConstructor of constr + | RecCallInTypeOfDef of constr + | RecCallInCaseFun of constr + | RecCallInCaseArg of constr + | RecCallInCasePred of constr + | NotGuardedForm of constr + +type arity_error = + | NonInformativeToInformative + | StrongEliminationOnNonSmallType + | WrongArity + +type type_error = + | UnboundRel of int + | UnboundVar of variable + | NotAType of unsafe_judgment + | BadAssumption of unsafe_judgment + | ReferenceVariables of constr + | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + * (sorts_family * sorts_family * arity_error) option + | CaseNotInductive of unsafe_judgment + | WrongCaseInfo of inductive * case_info + | NumberBranches of unsafe_judgment * int + | IllFormedBranch of constr * int * constr * constr + | Generalization of (name * constr) * unsafe_judgment + | ActualType of unsafe_judgment * constr + | CantApplyBadType of + (int * constr * constr) * unsafe_judgment * unsafe_judgment array + | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int + | IllTypedRecBody of + int * name array * unsafe_judgment array * constr array + +exception TypeError of env * type_error + +let nfj (c,ct) = (c, nf_betaiota ct) + +let error_unbound_rel env n = + raise (TypeError (env, UnboundRel n)) + +let error_unbound_var env v = + raise (TypeError (env, UnboundVar v)) + +let error_not_type env j = + raise (TypeError (env, NotAType j)) + +let error_assumption env j = + raise (TypeError (env, BadAssumption j)) + +let error_reference_variables env id = + raise (TypeError (env, ReferenceVariables id)) + +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 = + raise (TypeError (env, CaseNotInductive j)) + +let error_number_branches env cj expn = + raise (TypeError (env, NumberBranches (nfj cj,expn))) + +let error_ill_formed_branch env c i actty expty = + raise (TypeError (env, + IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty))) + +let error_generalization env nvar c = + raise (TypeError (env, Generalization (nvar,c))) + +let error_actual_type env j expty = + raise (TypeError (env, ActualType (j,expty))) + +let error_cant_apply_not_functional env rator randl = + raise (TypeError (env, CantApplyNonFunctional (rator,randl))) + +let error_cant_apply_bad_type env t rator randl = + raise (TypeError (env, CantApplyBadType (t,rator,randl))) + +let error_ill_formed_rec_body env why lna i = + raise (TypeError (env, IllFormedRecBody (why,lna,i))) + +let error_ill_typed_rec_body env i lna vdefj vargs = + raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) + + diff --git a/checker/type_errors.mli b/checker/type_errors.mli new file mode 100644 index 00000000..2d8f8ff2 --- /dev/null +++ b/checker/type_errors.mli @@ -0,0 +1,105 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) + +(*i*) +open Names +open Term +open Environ +(*i*) + +type unsafe_judgment = constr * constr + +(* Type errors. \label{typeerrors} *) + +(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix + notation i*) +type guard_error = + (* Fixpoints *) + | NotEnoughAbstractionInFixBody + | RecursionNotOnInductiveType of constr + | RecursionOnIllegalTerm of int * constr * int list * int list + | NotEnoughArgumentsForFixCall of int + (* CoFixpoints *) + | CodomainNotInductiveType of constr + | NestedRecursiveOccurrences + | UnguardedRecursiveCall of constr + | RecCallInTypeOfAbstraction of constr + | RecCallInNonRecArgOfConstructor of constr + | RecCallInTypeOfDef of constr + | RecCallInCaseFun of constr + | RecCallInCaseArg of constr + | RecCallInCasePred of constr + | NotGuardedForm of constr + +type arity_error = + | NonInformativeToInformative + | StrongEliminationOnNonSmallType + | WrongArity + +type type_error = + | UnboundRel of int + | UnboundVar of variable + | NotAType of unsafe_judgment + | BadAssumption of unsafe_judgment + | ReferenceVariables of constr + | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + * (sorts_family * sorts_family * arity_error) option + | CaseNotInductive of unsafe_judgment + | WrongCaseInfo of inductive * case_info + | NumberBranches of unsafe_judgment * int + | IllFormedBranch of constr * int * constr * constr + | Generalization of (name * constr) * unsafe_judgment + | ActualType of unsafe_judgment * constr + | CantApplyBadType of + (int * constr * constr) * unsafe_judgment * unsafe_judgment array + | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array + | IllFormedRecBody of guard_error * name array * int + | IllTypedRecBody of + int * name array * unsafe_judgment array * constr array + +exception TypeError of env * type_error + +val error_unbound_rel : env -> int -> 'a + +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 -> + (sorts_family * sorts_family * arity_error) option -> 'a + +val error_case_not_inductive : env -> unsafe_judgment -> 'a + +val error_number_branches : env -> unsafe_judgment -> int -> 'a + +val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a + +val error_generalization : env -> name * constr -> unsafe_judgment -> 'a + +val error_actual_type : env -> unsafe_judgment -> constr -> 'a + +val error_cant_apply_not_functional : + env -> unsafe_judgment -> unsafe_judgment array -> 'a + +val error_cant_apply_bad_type : + env -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> 'a + +val error_ill_formed_rec_body : + env -> guard_error -> name array -> int -> 'a + +val error_ill_typed_rec_body : + env -> int -> name array -> unsafe_judgment array -> constr array -> 'a + diff --git a/checker/typeops.ml b/checker/typeops.ml new file mode 100644 index 00000000..1af8b2ce --- /dev/null +++ b/checker/typeops.ml @@ -0,0 +1,456 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *) + +open Util +open Names +open Univ +open Term +open Reduction +open Type_errors +open Declarations +open Inductive +open Environ + +let inductive_of_constructor = fst + +let conv_leq_vecti env v1 v2 = + array_fold_left2_i + (fun i _ t1 t2 -> + (try conv_leq env t1 t2 + with NotConvertible -> raise (NotConvertibleVect i)); ()) + () + v1 + v2 + +(* This should be a type (a priori without intension to be an assumption) *) +let type_judgment env (c,ty as j) = + match whd_betadeltaiota env ty with + | Sort s -> (c,s) + | _ -> error_not_type env j + +(* This should be a type intended to be assumed. The error message is *) +(* not as useful as for [type_judgment]. *) +let assumption_of_judgment env j = + try fst(type_judgment env j) + with TypeError _ -> + error_assumption env j + +(************************************************) +(* Incremental typing rules: builds a typing judgement given the *) +(* judgements for the subterms. *) + +(*s Type of sorts *) + +(* Prop and Set *) + +let judge_of_prop = Sort (Type type1_univ) + +(* Type of Type(i). *) + +let judge_of_type u = Sort (Type (super u)) + +(*s Type of a de Bruijn index. *) + +let judge_of_relative env n = + try + let (_,_,typ) = lookup_rel n env in + lift n typ + 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 -> + error_unbound_var env id + +(* Management of context of variables. *) + +(* Checks if a context of variable can be instantiated by the + variables of the current env *) +(* TODO: check order? *) +let rec check_hyps_inclusion env sign = + fold_named_context + (fun (id,_,ty1) () -> + let ty2 = named_type id env in + if not (eq_constr ty2 ty1) then + error "types do not match") + sign + ~init:() + + +let check_args env c hyps = + try check_hyps_inclusion env hyps + with UserError _ | Not_found -> + error_reference_variables env c + + +(* Checks if the given context of variables [hyps] is included in the + current context of [env]. *) +(* +let check_hyps id env hyps = + let hyps' = named_context env in + if not (hyps_inclusion env hyps hyps') then + error_reference_variables env id +*) +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match c with Sort (Type u) -> Some u | _ -> None + +let extract_context_levels env = + List.fold_left + (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] + +let make_polymorphic_if_arity env t = + let params, ccl = dest_prod_assum env t in + match ccl with + | Sort (Type u) -> + let param_ccls = extract_context_levels env params in + let s = { poly_param_levels = param_ccls; poly_level = u} in + PolymorphicArity (params,s) + | _ -> + NonPolymorphicType t + +(* Type of constants *) + +let type_of_constant_knowing_parameters env t paramtyps = + match t with + | NonPolymorphicType t -> t + | PolymorphicArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_type env t = + type_of_constant_knowing_parameters env t [||] + +let type_of_constant env cst = + type_of_constant_type env (constant_type env cst) + +let judge_of_constant_knowing_parameters env cst paramstyp = + let c = Const cst in + let cb = lookup_constant cst env 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 = + judge_of_constant_knowing_parameters env cst [||] + +(* Type of an application. *) + +let judge_of_apply env (f,funj) argjv = + let rec apply_rec n typ = function + | [] -> typ + | (h,hj)::restjl -> + (match whd_betadeltaiota env typ with + | Prod (_,c1,c2) -> + (try conv_leq env hj c1 + 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 + 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) *) + | (_, Prop Null) -> rangsort + (* Product rule (Prop/Set,Set,Set) *) + | (Prop _, Prop Pos) -> rangsort + (* Product rule (Type,Set,?) *) + | (Type u1, Prop Pos) -> + if engagement env = Some ImpredicativeSet then + (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) + rangsort + else + (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) + Type (sup u1 type0_univ) + (* Product rule (Prop,Type_i,Type_i) *) + | (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) *) + | (Type u1, Type u2) -> Type (sup u1 u2) + +(* Type of a type cast *) + +(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule + + env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 + --------------------------------------------------------------------- + env |- c:typ2 +*) + +let judge_of_cast env (c,cj) k tj = + let conversion = + match k with + | VMcast -> vm_conv CUMUL + | DEFAULTcast -> conv_leq in + try + conversion env cj tj + with NotConvertible -> + error_actual_type env (c,cj) tj + +(* Inductive types. *) + +(* The type is parametric over the uniform parameters whose conclusion + is in Type; to enforce the internal constraints between the + parameters and the instances of Type occurring in the type of the + constructors, we use the level variables _statically_ assigned to + the conclusions of the parameters as mediators: e.g. if a parameter + has conclusion Type(alpha), static constraints of the form alpha<=v + exist between alpha and the Type's occurring in the constructor + types; when the parameters is finally instantiated by a term of + conclusion Type(u), then the constraints u<=alpha is computed in + the App case of execute; from this constraints, the expected + dynamic constraints of the form u<=v are enforced *) + +let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) = + let c = Ind ind in + let (mib,mip) = lookup_mind_specif env ind in + check_args env c mib.mind_hyps; + type_of_inductive_knowing_parameters env mip paramstyp + +let judge_of_inductive env ind = + judge_of_inductive_knowing_parameters env ind [||] + +(* Constructors. *) + +let judge_of_constructor env c = + let constr = Construct c in + let _ = + let ((kn,_),_) = c in + let mib = lookup_mind kn env 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) = + try conv_leq_vecti env lfj explft + with + NotConvertibleVect i -> + error_ill_formed_branch env c i lfj.(i) explft.(i) + | Invalid_argument _ -> + error_number_branches env (c,cj) (Array.length explft) + +let judge_of_case env ci pj (c,cj) lfj = + let indspec = + try find_rectype env cj + with Not_found -> error_case_not_inductive env (c,cj) in + let _ = check_case_info env (fst indspec) ci in + let (bty,rslty) = type_case_branches env indspec pj c in + check_branch_types env (c,cj) (lfj,bty); + rslty + +(* Fixpoints. *) + +(* Checks the type of a general (co)fixpoint, i.e. without checking *) +(* the specific guard condition. *) + +let type_fixpoint env lna lar lbody vdefj = + let lt = Array.length vdefj in + assert (Array.length lar = lt && Array.length lbody = lt); + try + conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar) + with NotConvertibleVect i -> + let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in + error_ill_typed_rec_body env i lna vdefj lar + +(************************************************************************) +(************************************************************************) + + +let refresh_arity env ar = + let ctxt, hd = decompose_prod_assum ar in + match hd with + Sort (Type u) when not (is_univ_variable u) -> + let u' = fresh_local_univ() in + let env' = add_constraints (enforce_geq u' u Constraint.empty) env in + env', mkArity (ctxt,Type u') + | _ -> env, ar + + +(* The typing machine. *) +let rec execute env cstr = + match cstr with + (* Atomic terms *) + | Sort (Prop _) -> judge_of_prop + + | Sort (Type u) -> judge_of_type u + + | Rel n -> judge_of_relative env n + + | Var id -> judge_of_variable env id + + | Const c -> judge_of_constant env c + + (* Lambda calculus operators *) + | App (App (f,args),args') -> + execute env (App(f,Array.append args args')) + + | App (f,args) -> + let jl = execute_array env args in + let j = + match f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind jl + | 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) -> + let _ = execute_type env c1 in + let env1 = push_rel (name,None,c1) env 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 + let varj' = execute_type env1 c2 in + Sort (sort_of_product env varj varj') + + | LetIn (name,c1,c2,c3) -> + let j1 = execute env c1 in + (* /!\ c2 can be an inferred type => refresh + (but the pushed type is still c2) *) + let _ = + let env',c2' = refresh_arity env c2 in + let _ = execute_type env' c2' in + judge_of_cast env' (c1,j1) DEFAULTcast c2' in + 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 + judge_of_cast env (c,cj) k t; + t + + (* Inductive types *) + | Ind ind -> judge_of_inductive env ind + + | Construct c -> judge_of_constructor env c + + | Case (ci,p,c,lf) -> + let cj = execute env c in + 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 + check_cofix env cofix; + fix_ty + + (* Partial proofs: unsupported by the kernel *) + | Meta _ -> + anomaly "the kernel does not support metavariables" + + | Evar _ -> + anomaly "the kernel does not support existential variables" + +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 + let lara = Array.map (assumption_of_judgment env) larj in + let env1 = push_rec_types (names,lara,vdef) env in + let vdefj = execute_array env1 vdef in + type_fixpoint env1 names lara vdef vdefj; + lara.(i) + +and execute_array env = Array.map (execute env) + +and execute_list env = List.map (execute env) + +(* Derived functions *) +let infer env constr = execute env constr +let infer_type env constr = execute_type env constr +let infer_v env cv = execute_array env cv + +(* Typing of several terms. *) + +let check_ctxt env rels = + fold_rel_context (fun d env -> + match d with + (_,None,ty) -> + let _ = infer_type env ty in + push_rel d env + | (_,Some bd,ty) -> + let j1 = infer env bd in + let _ = infer env ty in + conv_leq env j1 ty; + push_rel d env) + rels ~init:env + +let check_named_ctxt env ctxt = + fold_named_context (fun (id,_,_ as d) env -> + let _ = + try + let _ = lookup_named id env in + failwith ("variable "^string_of_id id^" defined twice") + with Not_found -> () in + match d with + (_,None,ty) -> + let _ = infer_type env ty in + push_named d env + | (_,Some bd,ty) -> + let j1 = infer env bd in + let _ = infer env ty in + conv_leq env j1 ty; + push_named d env) + ctxt ~init:env + +(* Polymorphic arities utils *) + +let check_kind env ar u = + if snd (dest_prod env ar) = Sort(Type u) then () + else failwith "not the correct sort" + +let check_polymorphic_arity env params par = + let pl = par.poly_param_levels in + let rec check_p env pl params = + match pl, params with + Some u::pl, (na,None,ty)::params -> + check_kind env ty u; + check_p (push_rel (na,None,ty) env) pl params + | None::pl,d::params -> check_p (push_rel d env) pl params + | [], _ -> () + | _ -> failwith "check_poly: not the right number of params" in + check_p env pl (List.rev params) diff --git a/checker/typeops.mli b/checker/typeops.mli new file mode 100644 index 00000000..de160a79 --- /dev/null +++ b/checker/typeops.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: typeops.mli 9427 2006-12-11 18:46:35Z bgregoir $ i*) + +(*i*) +open Names +open Term +open Declarations +open Environ +(*i*) + +(*s Typing functions (not yet tagged as safe) *) + +val infer : env -> constr -> constr +val infer_type : env -> constr -> sorts +val check_ctxt : env -> rel_context -> env +val check_named_ctxt : env -> named_context -> env +val check_polymorphic_arity : + env -> rel_context -> polymorphic_arity -> unit + +val type_of_constant_type : env -> constant_type -> constr + diff --git a/checker/validate.ml b/checker/validate.ml new file mode 100644 index 00000000..86e51b7b --- /dev/null +++ b/checker/validate.ml @@ -0,0 +1,265 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *) + +(* This module defines validation functions to ensure an imported + value (using input_value) has the correct structure. *) + +let rec pr_obj_rec o = + if Obj.is_int o then + Format.print_string ("INT:"^string_of_int(Obj.magic o)) + else if Obj.is_block o then + let t = Obj.tag o in + if t > Obj.no_scan_tag then + if t = Obj.string_tag then + Format.print_string ("STR:"^Obj.magic o) + else + Format.print_string "?" + else + (let n = Obj.size o in + Format.print_string ("#"^string_of_int t^"("); + Format.open_hvbox 0; + for i = 0 to n-1 do + pr_obj_rec (Obj.field o i); + if i<>n-1 then (Format.print_string ","; Format.print_cut()) + done; + Format.close_box(); + Format.print_string ")") + else Format.print_string "?" + +let pr_obj o = pr_obj_rec o; Format.print_newline() + +(**************************************************************************) +(* Low-level validators *) + +(* data not validated *) +let no_val (o:Obj.t) = () + +(* Check that object o is a block with tag t *) +let val_tag t o = + if Obj.is_block o && Obj.tag o = t then () + else failwith ("tag "^string_of_int t) + +let val_obj s o = + if Obj.is_block o then + (if Obj.tag o > Obj.no_scan_tag then + failwith (s^". Not a normal tag")) + else failwith (s^". Not a block") + +(* Check that an object is a tuple (or a record). v is an array of + validation functions for each field. Its size corresponds to the + expected size of the object. *) +let val_tuple s v o = + let n = Array.length v in + val_obj ("tuple: "^s) o; + if Obj.size o = n then + Array.iteri (fun i f -> f (Obj.field o i)) v + else + (pr_obj o; + failwith + ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))) + +(* Check that the object is either a constant constructor of tag < cc, + or a constructed variant. each element of vv is an array of + validation functions to be applied to the constructor arguments. + The size of vv corresponds to the number of non-constant + constructors, and the size of vv.(i) is the expected arity of the + i-th non-constant constructor. *) +let val_sum s cc vv o = + if Obj.is_block o then + (val_obj ("sum: "^s) o; + let n = Array.length vv in + let i = Obj.tag o in + if i < n then val_tuple (s^"("^string_of_int i^")") vv.(i) o + else failwith ("bad tag in sum ("^s^"): "^string_of_int i)) + else if Obj.is_int o then + let (n:int) = Obj.magic o in + (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")")) + else failwith ("not a sum ("^s^")") + +let val_enum s n = val_sum s n [||] + +(* Recursive types: avoid looping by eta-expansion *) +let rec val_rec_sum s cc f o = + val_sum s cc (f (val_rec_sum s cc f)) o + +(**************************************************************************) +(* Builtin types *) + +(* Check the o is an array of values satisfying f. *) +let val_array f o = + val_obj "array" o; + for i = 0 to Obj.size o - 1 do + (f (Obj.field o i):unit) + done + +(* Integer validator *) +let val_int o = + if not (Obj.is_int o) then failwith "expected an int" + +(* String validator *) +let val_str s = val_tag Obj.string_tag s + +(* Booleans *) +let val_bool = val_enum "bool" 2 + +(* Option type *) +let val_opt f = val_sum "option" 1 [|[|f|]|] + +(* Lists *) +let val_list f = + val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|]) + +(* Reference *) +let val_ref f = val_tuple "ref" [|f|] + +(**************************************************************************) +(* Standard library types *) + +(* Sets *) +let val_set f = + val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|]) + +(* Maps *) +let rec val_map fk fv = + val_rec_sum "map" 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|]) + +(**************************************************************************) +(* Coq types *) + +let val_id = val_str + +let val_dp = val_list val_id + +let val_name = val_sum "name" 1 [|[|val_id|]|] + +let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|] + +let val_mp = + val_rec_sum "mp" 0 + (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|]) + +let val_kn = val_tuple "kn" [|val_mp;val_dp;val_id|] + +let val_ind = val_tuple "ind"[|val_kn;val_int|] +let val_cstr = val_tuple "cstr"[|val_ind;val_int|] + +let val_ci = + let val_cstyle = val_enum "case_style" 5 in + let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in + val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|] + + +let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|] +let val_univ = val_sum "univ" 0 + [|[|val_level|];[|val_list val_level;val_list val_level|]|] + +let val_cstrs = + val_set (val_tuple"univ_cstr"[|val_level;val_enum "order" 3;val_level|]) + +let val_cast = val_enum "cast_kind" 2 +let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|] +let val_sortfam = val_enum "sort_family" 3 + +let val_evar f = val_tuple "evar" [|val_int;val_array f|] + +let val_prec f = + val_tuple "prec"[|val_array val_name; val_array f; val_array f|] +let val_fix f = + val_tuple"fix1"[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|] +let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|] + + +let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| + [|val_int|]; (* Rel *) + [|val_id|]; (* Var *) + [|val_int|]; (* Meta *) + [|val_evar val_constr|]; (* Evar *) + [|val_sort|]; (* Sort *) + [|val_constr;val_cast;val_constr|]; (* Cast *) + [|val_name;val_constr;val_constr|]; (* Prod *) + [|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_ind|]; (* Ind *) + [|val_cstr|]; (* Construct *) + [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) + [|val_fix val_constr|]; (* Fix *) + [|val_cofix val_constr|] (* CoFix *) +|]) + + +let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|] +let val_rdecl = val_tuple"rdecl"[|val_name;val_opt val_constr;val_constr|] +let val_nctxt = val_list val_ndecl +let val_rctxt = val_list val_rdecl + +let val_arity = val_tuple"arity"[|val_rctxt;val_constr|] + +let val_eng = val_enum "eng" 1 + +let val_pol_arity = val_tuple"pol_arity"[|val_list(val_opt val_univ);val_univ|] +let val_cst_type = + val_sum "cst_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|] + +let val_subst_dom = + val_sum "subst_dom" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|] + + +let val_res = val_opt no_val + +let val_subst = + val_map val_subst_dom (val_tuple "subst range" [|val_mp;val_res|]) + +let val_cstr_subst = + val_ref (val_sum "cstr_subst" 0 [|[|val_constr|];[|val_subst;val_constr|]|]) + +let val_cb = val_tuple "cb" + [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs; + val_bool; val_bool |] + +let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|] + +let val_wfp = val_rec_sum "wf_paths" 0 + (fun val_wfp -> + [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|]; + [|val_int;val_array val_wfp|]|]) + +let val_mono_ind_arity = val_tuple"mono_ind_arity"[|val_constr;val_sort|] +let val_ind_arity = val_sum "ind_arity" 0 + [|[|val_mono_ind_arity|];[|val_pol_arity|]|] + +let val_one_ind = val_tuple "one_ind" + [|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|] + +let val_ind_pack = val_tuple "ind_pack" + [|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|] + +let rec val_sfb o = val_sum "sfb" 0 + [|[|val_cb|];[|val_ind_pack|];[|val_mod|]; + [|val_mp;val_opt val_cstrs|];[|val_modty|]|] o +and val_sb o = val_list (val_tuple"sb"[|val_id;val_sfb|]) o +and val_seb o = val_sum "seb" 0 + [|[|val_mp|];[|val_uid;val_modty;val_seb|];[|val_uid;val_sb|]; + [|val_seb;val_seb;val_cstrs|];[|val_seb;val_with|]|] o +and val_with o = val_sum "with" 0 + [|[|val_list val_id;val_mp;val_cstrs|]; + [|val_list val_id;val_cb|]|] o +and val_mod o = val_tuple "module_body" + [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o +and val_modty o = val_tuple "module_type_body" + [|val_seb;val_opt val_mp;val_subst|] o + +let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|]) + +let val_vo = val_tuple "vo" [|val_dp;val_mod;val_deps;val_eng|] |