From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- checker/Makefile | 88 -------- checker/analyze.ml | 101 +++++++-- checker/analyze.mli | 21 +- checker/check.ml | 86 ++++---- checker/check.mli | 32 +++ checker/check.mllib | 1 + checker/check_stat.ml | 10 +- checker/check_stat.mli | 10 +- checker/checker.ml | 115 +++++----- checker/checker.mli | 11 + checker/cic.mli | 82 ++++--- checker/closure.ml | 131 ++++------- checker/closure.mli | 48 ++-- checker/declarations.ml | 54 ++--- checker/declarations.mli | 13 +- checker/environ.ml | 69 +++--- checker/environ.mli | 37 ++-- checker/include | 3 +- checker/indtypes.ml | 112 ++++++++-- checker/indtypes.mli | 16 +- checker/inductive.ml | 74 +++---- checker/inductive.mli | 16 +- checker/main.mli | 12 + checker/mod_checking.ml | 60 ++--- checker/mod_checking.mli | 12 +- checker/modops.ml | 58 ++--- checker/modops.mli | 28 +-- checker/print.ml | 166 +++++--------- checker/print.mli | 13 ++ checker/reduction.ml | 196 ++++++++++++----- checker/reduction.mli | 10 +- checker/safe_typing.ml | 16 +- checker/safe_typing.mli | 10 +- checker/subtyping.ml | 175 +++++---------- checker/subtyping.mli | 10 +- checker/term.ml | 72 +++--- checker/term.mli | 8 +- checker/type_errors.ml | 16 +- checker/type_errors.mli | 20 +- checker/typeops.ml | 49 +---- checker/typeops.mli | 13 +- checker/univ.ml | 563 +++++++++++++++++------------------------------ checker/univ.mli | 95 ++++++-- checker/validate.ml | 12 +- checker/validate.mli | 11 + checker/values.ml | 81 ++++--- checker/values.mli | 28 +++ checker/votour.ml | 104 +++++---- checker/votour.mli | 12 + 49 files changed, 1516 insertions(+), 1464 deletions(-) delete mode 100644 checker/Makefile create mode 100644 checker/check.mli create mode 100644 checker/checker.mli create mode 100644 checker/main.mli create mode 100644 checker/print.mli create mode 100644 checker/validate.mli create mode 100644 checker/values.mli create mode 100644 checker/votour.mli (limited to 'checker') diff --git a/checker/Makefile b/checker/Makefile deleted file mode 100644 index 2bcc9d36..00000000 --- a/checker/Makefile +++ /dev/null @@ -1,88 +0,0 @@ -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/analyze.ml b/checker/analyze.ml index c48b8301..7047d8a1 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -4,6 +4,7 @@ let prefix_small_block = 0x80 let prefix_small_int = 0x40 let prefix_small_string = 0x20 +[@@@ocaml.warning "-32"] let code_int8 = 0x00 let code_int16 = 0x01 let code_int32 = 0x02 @@ -25,6 +26,7 @@ let code_infixpointer = 0x11 let code_custom = 0x12 let code_block64 = 0x13 +[@@@ocaml.warning "-37"] type code_descr = | CODE_INT8 | CODE_INT16 @@ -53,6 +55,55 @@ let magic_number = "\132\149\166\190" (** Memory reification *) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end = +struct + + let max_length = Sys.max_array_length + + type 'a t = 'a array array * 'a array + (** Invariants: + - All subarrays of the left array have length [max_length]. + - The right array has length < [max_length]. + *) + + let empty = [||], [||] + + let length (vl, vr) = + (max_length * Array.length vl) + Array.length vr + + let make n x = + let k = n / max_length in + let r = n mod max_length in + let vl = Array.init k (fun _ -> Array.make max_length x) in + let vr = Array.make r x in + (vl, vr) + + let get (vl, vr) n = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) + else if k == len then vr.(r) + else invalid_arg "index out of bounds" + + let set (vl, vr) n x = + let k = n / max_length in + let r = n mod max_length in + let len = Array.length vl in + if k < len then vl.(k).(r) <- x + else if k == len then vr.(r) <- x + else invalid_arg "index out of bounds" + +end + type repr = | RInt of int | RBlock of (int * int) (* tag × len *) @@ -80,7 +131,7 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) end module Make(M : Input) = @@ -101,11 +152,11 @@ let input_binary_int chan = input_binary_int chan let input_char chan = Char.chr (input_byte chan) +let input_string len chan = String.init len (fun _ -> input_char chan) let parse_header chan = let () = current_offset := 0 in - let magic = String.create 4 in - let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let magic = input_string 4 chan in let length = input_binary_int chan in let objects = input_binary_int chan in let size32 = input_binary_int chan in @@ -204,13 +255,6 @@ let input_header64 chan = in (tag, len) -let input_string len chan = - let ans = String.create len in - for i = 0 to pred len do - ans.[i] <- input_char chan; - done; - ans - let parse_object chan = let data = input_byte chan in if prefix_small_block <= data then @@ -251,7 +295,7 @@ let parse_object chan = RString (input_string len chan) | CODE_CODEPOINTER -> let addr = input_int32u chan in - for i = 0 to 15 do ignore (input_byte chan); done; + for _i = 0 to 15 do ignore (input_byte chan); done; RCode addr | CODE_DOUBLE_ARRAY32_LITTLE | CODE_DOUBLE_BIG @@ -266,7 +310,7 @@ let parse_object chan = let parse chan = let (magic, len, _, _, size) = parse_header chan in let () = assert (magic = magic_number) in - let memory = Array.make size (Struct ((-1), [||])) in + let memory = LargeArray.make size (Struct ((-1), [||])) in let current_object = ref 0 in let fill_obj = function | RPointer n -> @@ -277,7 +321,7 @@ let parse chan = data, None | RString s -> let data = Ptr !current_object in - let () = memory.(!current_object) <- String s in + let () = LargeArray.set memory !current_object (String s) in let () = incr current_object in data, None | RBlock (tag, 0) -> @@ -287,7 +331,7 @@ let parse chan = | RBlock (tag, len) -> let data = Ptr !current_object in let nblock = Array.make len (Atm (-1)) in - let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in let () = incr current_object in data, Some nblock | RCode addr -> @@ -348,3 +392,32 @@ module PString = Make(IString) let parse_channel = PChannel.parse let parse_string s = PString.parse (s, ref 0) + +let instantiate (p, mem) = + let len = LargeArray.length mem in + let ans = LargeArray.make len (Obj.repr 0) in + (** First pass: initialize the subobjects *) + for i = 0 to len - 1 do + let obj = match LargeArray.get mem i with + | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) + | String str -> Obj.repr str + in + LargeArray.set ans i obj + done; + let get_data = function + | Int n -> Obj.repr n + | Ptr p -> LargeArray.get ans p + | Atm tag -> Obj.new_block tag 0 + | Fun _ -> assert false (** We shouldn't serialize closures *) + in + (** Second pass: set the pointers *) + for i = 0 to len - 1 do + match LargeArray.get mem i with + | Struct (_, blk) -> + let obj = LargeArray.get ans i in + for k = 0 to Array.length blk - 1 do + Obj.set_field obj k (get_data blk.(k)) + done + | String _ -> () + done; + get_data p diff --git a/checker/analyze.mli b/checker/analyze.mli index 42efcf01..9c837643 100644 --- a/checker/analyze.mli +++ b/checker/analyze.mli @@ -8,8 +8,20 @@ type obj = | Struct of int * data array (* tag × data *) | String of string -val parse_channel : in_channel -> (data * obj array) -val parse_string : string -> (data * obj array) +module LargeArray : +sig + type 'a t + val empty : 'a t + val length : 'a t -> int + val make : int -> 'a -> 'a t + val get : 'a t -> int -> 'a + val set : 'a t -> int -> 'a -> unit +end +(** A data structure similar to arrays but allowing to overcome the 2^22 length + limitation on 32-bit architecture. *) + +val parse_channel : in_channel -> (data * obj LargeArray.t) +val parse_string : string -> (data * obj LargeArray.t) (** {6 Functorized version} *) @@ -26,10 +38,13 @@ end module type S = sig type input - val parse : input -> (data * obj array) + val parse : input -> (data * obj LargeArray.t) (** Return the entry point and the reification of the memory out of a marshalled structure. *) end module Make (M : Input) : S with type input = M.t (** Functorized version of the previous code. *) + +val instantiate : data * obj LargeArray.t -> Obj.t +(** Create the OCaml object out of the reified representation. *) diff --git a/checker/check.ml b/checker/check.ml index 8b299bf2..4bb485d2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - error ("Unknown library " ^ (DirPath.to_string dir)) - let library_full_filename dir = (find_library dir).library_filename (* If a library is loaded several time, then the first occurrence must @@ -129,8 +131,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.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: "./" *) @@ -165,7 +165,7 @@ let find_logical_path phys_dir = match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir | _,[] -> default_root_prefix - | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir)) + | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^".")) let remove_load_path dir = let physical, logical = !load_paths in @@ -197,7 +197,7 @@ let add_load_path (phys_path,coq_path) = end | _,[] -> load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) - | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path)) + | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^".")) let load_paths_of_dir_path dir = let physical, logical = !load_paths in @@ -227,13 +227,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = 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 @@ -248,12 +243,12 @@ let locate_qualified_library qid = let error_unmapped_dir qid = let prefix = qid.dirpath in - errorlabstrm "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) let error_lib_not_found qid = - errorlabstrm "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -263,7 +258,17 @@ let try_locate_absolute_library dir = | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) | LibNotFound -> error_lib_not_found (path_of_dirpath dir) -let try_locate_qualified_library qid = +let try_locate_qualified_library lib = match lib with +| PhysicalFile f -> + let () = + if not (System.file_exists_respecting_case "" f) then + error_lib_not_found { dirpath = []; basename = f; } + in + let dir = Filename.dirname f in + let base = Filename.chop_extension (Filename.basename f) in + let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in + (dir, f) +| LogicalFile qid -> try locate_qualified_library qid with @@ -298,34 +303,43 @@ let name_clash_message dir mdir f = (* Dependency graph *) let depgraph = ref LibraryMap.empty +let marshal_in_segment f ch = + try + let stop = input_binary_int ch in + let v = Analyze.instantiate (Analyze.parse_channel ch) in + let digest = Digest.input ch in + Obj.obj v, stop, digest + with _ -> + user_err (str "Corrupted file " ++ quote (str f)) + let intern_from_file (dir, f) = Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in - let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in - let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in - let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in - let (discharging:'a option), _, _ = System.marshal_in_segment f ch in - let (tasks:'a option), _, _ = System.marshal_in_segment f ch in + let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in + let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in + let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in + let (discharging:'a option), _, _ = marshal_in_segment f ch in + let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:Cic.opaque_table), pos, checksum = - System.marshal_in_segment f ch in + marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then - errorlabstrm "intern_from_file" (str "Checksum mismatch"); + user_err ~hdr:"intern_from_file" (str "Checksum mismatch"); let () = close_in ch in if dir <> sd.md_name then - errorlabstrm "intern_from_file" + user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then - errorlabstrm "intern_from_file" + user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin chk_pp (str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then - errorlabstrm "intern_from_file" + user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; Validate.validate !Flags.debug Values.v_univopaques opaque_csts; @@ -412,9 +426,3 @@ let recheck_library ~norec ~admit ~check = (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") - -open Printf - -let mem s = - let m = try_find_library s in - h 0 (str (sprintf "%dk" (CObj.size_kb m))) diff --git a/checker/check.mli b/checker/check.mli new file mode 100644 index 00000000..eb6404a1 --- /dev/null +++ b/checker/check.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit + +val recheck_library : + norec:object_file list -> + admit:object_file list -> + check:object_file list -> unit diff --git a/checker/check.mllib b/checker/check.mllib index 488507a1..f79ba66e 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,6 @@ Coq_config +Analyze Hook Terminal Canary diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 741f5328..3f00f924 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* pp fmt (i,x)) a let fatal_error info anomaly = - flush_all (); Feedback.msg_error info; flush_all (); + flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -41,9 +42,10 @@ let dirpath_of_string s = [] -> Check.default_root_prefix | dir -> DirPath.make (List.map Id.of_string dir) let path_of_string s = - match parse_dir s with + if Filename.check_suffix s ".vo" then PhysicalFile s + else match parse_dir s with [] -> invalid_arg "path_of_string" - | l::dir -> {dirpath=dir; basename=l} + | l::dir -> LogicalFile {dirpath=dir; basename=l} let ( / ) = Filename.concat @@ -74,7 +76,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -96,17 +98,13 @@ let add_rec_path ~unix_path ~coq_root = (* 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 push_include (s, alias) = includes := (s,alias) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = @@ -132,8 +130,7 @@ let init_load_path () = add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -145,15 +142,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet let engage () = Safe_typing.set_engagement (!impredicative_set) -let admit_list = ref ([] : section_path list) +let admit_list = ref ([] : object_file list) let add_admit s = admit_list := path_of_string s :: !admit_list -let norec_list = ref ([] : section_path list) +let norec_list = ref ([] : object_file list) let add_norec s = norec_list := path_of_string s :: !norec_list -let compile_list = ref ([] : section_path list) +let compile_list = ref ([] : object_file list) let add_compile s = compile_list := path_of_string s :: !compile_list @@ -179,7 +176,9 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -R dir coqdir map physical dir to logical coqdir\ +" -Q dir coqdir map physical dir to logical coqdir\ +\n -R dir coqdir synonymous for -Q\ +\n\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -211,15 +210,16 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report" ++ - strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") +let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".") let guill s = str "\"" ++ str s ++ str "\"" -let where s = +let where = function +| None -> mt () +| Some s -> if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) -let rec explain_exn = function +let explain_exn = function | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> @@ -269,26 +269,26 @@ let rec explain_exn = function | Generalization _ -> str"Generalization" | ActualType _ -> str"ActualType" | CantApplyBadType ((n,a,b),(hd,hdty),args) -> - Format.printf "====== ill-typed term ====@\n"; - Format.printf "@[application head=@ "; - Print.print_pure_constr hd; - Format.printf "@]@\n@[head type=@ "; - Print.print_pure_constr hdty; - Format.printf "@]@\narguments:@\n@["; - Array.iteri (fun i (t,ty) -> - Format.printf "@[arg %d=@ " (i+1); - Print.print_pure_constr t; - Format.printf "@ type=@ "; - Print.print_pure_constr ty) args; - Format.printf "@]@\n====== type error ====@\n"; - Print.print_pure_constr b; - Format.printf "@\nis not convertible with@\n"; - Print.print_pure_constr a; - Format.printf "@\n====== universes ====@\n"; - chk_pp - (Univ.pr_universes - (ctx.Environ.env_stratification.Environ.env_universes)); - str "\nCantApplyBadType at argument " ++ int n + (* This mix of printf / pp was here before... *) + let fmt = Format.std_formatter in + let open Format in + let open Print in + fprintf fmt "====== ill-typed term ====@\n"; + fprintf fmt "@[application head=@ %a@]@\n" print_pure_constr hd; + fprintf fmt "@[head type=@ %a@]@\n" print_pure_constr hdty; + let pp_arg fmt (i,(t,ty)) = fprintf fmt "@[@[<1>arg %d=@ @[%a@]@]@,@[<1>type=@ @[%a@]@]@]@\n@," (i+1) + print_pure_constr t print_pure_constr ty + in + fprintf fmt "arguments:@\n@[%a@]@\n" (pp_arrayi pp_arg) args; + fprintf fmt "====== type error ====@\n"; + fprintf fmt "%a@\n" print_pure_constr b; + fprintf fmt "is not convertible with@\n"; + fprintf fmt "%a@\n" print_pure_constr a; + fprintf fmt "====== universes ====@\n"; + fprintf fmt "%a@\n%!" Pp.pp_with + (Univ.pr_universes + (ctx.Environ.env_stratification.Environ.env_universes)); + str "CantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -309,6 +309,9 @@ let rec explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) +let deprecated flag = + Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) + let parse_args argv = let rec parse = function | [] -> () @@ -322,25 +325,28 @@ let parse_args argv = Flags.coqlib_spec := true; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: d :: p :: rem -> set_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + + | "-R" :: d :: p :: rem -> set_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:CErrors.error; + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -352,7 +358,7 @@ let parse_args argv = | "-norec" :: [] -> usage () | "-silent" :: rem -> - Flags.make_silent true; parse rem + Flags.quiet := true; parse rem | s :: _ when s<>"" && s.[0]='-' -> fatal_error (str "Unknown option " ++ str s) false @@ -364,15 +370,18 @@ let parse_args argv = (* To prevent from doing the initialization twice *) let initialized = ref false +(* XXX: At some point we need to either port the checker to use the + feedback system or to remove its use completely. *) let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:CErrors.error; - if_verbose print_header (); + Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> diff --git a/checker/checker.mli b/checker/checker.mli new file mode 100644 index 00000000..582f4258 --- /dev/null +++ b/checker/checker.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* unit diff --git a/checker/cic.mli b/checker/cic.mli index 36455875..c4b00d0d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge (*************************************************************************) (** {4 From safe_typing.ml} *) diff --git a/checker/closure.ml b/checker/closure.ml index cef1d31a..b9ae4daa 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* red_kind - val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds val mkflags : red_kind list -> reds @@ -80,51 +73,33 @@ module RedFlags = (struct 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 Id.t + 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 } + | DELTA -> { red with r_delta = true} | 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 = Id.Pred.add id l1, l2 } 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 = Id.Pred.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 *) @@ -160,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * instantiations (cbv or lazy) are. *) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int +type table_key = Constant.t puniverses tableKey + -type table_key = constant puniverses tableKey +let eq_pconstant_key (c,u) (c',u') = + eq_constant_key c c' && Univ.Instance.equal u u' module KeyHash = struct type t = table_key - let equal k1 k2 = match k1, k2 with - | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 - && Univ.Instance.equal u1 u2 - | VarKey id1, VarKey id2 -> Id.equal id1 id2 - | RelKey i1, RelKey i2 -> Int.equal i1 i2 - | (ConstKey _ | VarKey _ | RelKey _), _ -> false + let equal = Names.eq_table_key eq_pconstant_key open Hashset.Combine @@ -226,8 +195,6 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env -let eq_table_key = KeyHash.equal - let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; @@ -276,14 +243,13 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *) | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -306,9 +272,8 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * projection + | Zproj of int * int * Projection.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -328,6 +293,12 @@ let zshift n s = | (_,Zshift(k)::s) -> Zshift(n+k)::s | _ -> Zshift(n)::s +let rec stack_args_size = function + | Zapp v :: s -> Array.length v + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + (* 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. *) @@ -450,13 +421,10 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> Const op | FInd op -> Ind op | FConstruct op -> Construct op - | FCase (ci,p,c,ve) -> - Case (ci, constr_fun lfts p, - constr_fun lfts c, - Array.map (constr_fun lfts) ve) - | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *) - to_constr constr_fun lfts - {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)} + | FCaseT (ci,p,c,ve,e) -> + let fp = mk_clos2 e p in + let fve = mk_clos_vect e ve in + Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in let ftys = Array.map (mk_clos e) tys in @@ -526,9 +494,6 @@ 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 = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -610,7 +575,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -651,22 +616,6 @@ let drop_parameters depth n argstk = (** Projections and eta expansion *) -let rec get_parameters depth n argstk = - match argstk with - Zapp args::s -> - let q = Array.length args in - if n > q then Array.append args (get_parameters depth (n-q) s) - else if Int.equal n q then [||] - else Array.sub args 0 n - | Zshift(k)::s -> - get_parameters (depth-k) n s - | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) - if Int.equal n 0 then [||] - else raise Not_found (* Trying to eta-expand a partial application..., should do - eta expansion first? *) - | _ -> assert false - (* strip_update_shift_app only produces Zapp and Zshift items *) - let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.mind_record with @@ -718,6 +667,9 @@ let contract_fix_vect fix = in (subs_cons(Array.init nfix make_body, env), thisbody) +let unfold_projection env p = + let pb = lookup_projection p env in + Zproj (pb.proj_npars, pb.proj_arg, p) (*********************************************************************) (* A machine that inspects the head of a term until it finds an @@ -730,7 +682,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -739,10 +690,9 @@ let rec knh info m stk = | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - if red_set info.i_flags (fCONST (Projection.constant p)) then - (let pb = lookup_projection p (info.i_env) in - knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) - :: zupdate m stk)) + if red_set info.i_flags fDELTA then + let s = unfold_projection info.i_env p in + knh info c (s :: zupdate m stk) else (m,stk) (* cases where knh stops *) @@ -774,11 +724,11 @@ let rec knr info m stk = (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 (fst kn)) -> + | FFlex(ConstKey kn) when red_set info.i_flags fDELTA -> (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) -> + | FFlex(VarKey id) when red_set info.i_flags fDELTA -> (match ref_value_cache info (VarKey id) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) @@ -788,10 +738,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) 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) | (depth, args, ZcaseT(ci,_,br,env)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -808,7 +754,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) @@ -845,6 +791,7 @@ type clos_infos = fconstr infos let infos_env x = x.i_env let infos_flags x = x.i_flags +let oracle_of_infos x = x.i_env.env_conv_oracle let create_clos_infos flgs env = create (fun _ -> inject) flgs env diff --git a/checker/closure.mli b/checker/closure.mli index 8b1f246c..49b07f73 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) -type transparent_state = Id.Pred.t * Cpred.t - -val all_opaque : transparent_state -val all_transparent : transparent_state - -val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool - (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -42,8 +36,6 @@ module type RedFlagsSig = sig val fDELTA : red_kind val fIOTA : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind - val fVAR : Id.t -> red_kind (* No reduction at all *) val no_red : reds @@ -66,12 +58,8 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int -type table_key = constant puniverses tableKey +type table_key = Constant.t puniverses tableKey type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option @@ -95,14 +83,13 @@ type fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) - | FLambda of int * (name * constr) list * constr * fconstr subs - | FProd of name * fconstr * fconstr - | FLetIn of name * fconstr * fconstr * constr * fconstr subs + | FLambda of int * (Name.t * constr) list * constr * fconstr subs + | FProd of Name.t * fconstr * fconstr + | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs | FEvar of existential_key * fconstr array | FLIFT of int * fconstr | FCLOS of constr * fconstr subs @@ -115,9 +102,8 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * projection + | Zproj of int * int * Projection.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -125,11 +111,16 @@ type stack_member = and stack = stack_member list val append_stack : fconstr array -> stack -> stack + +val stack_args_size : stack -> int + val eta_expand_stack : stack -> stack val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack +val unfold_projection : env -> Projection.t -> stack_member + (* 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 *) @@ -139,13 +130,15 @@ val inject : constr -> fconstr val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : - (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr + (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (* Global and local constant cache *) type clos_infos val create_clos_infos : reds -> env -> clos_infos val infos_env : clos_infos -> env val infos_flags : clos_infos -> reds +val oracle_of_infos : clos_infos -> oracle + (* Reduction function *) @@ -165,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool -val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/checker/declarations.ml b/checker/declarations.ml index 1fe02c8b..d2c3f203 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -6,6 +6,7 @@ open Term (** Substitutions, code imported from kernel/mod_subst *) module Deltamap = struct + [@@@ocaml.warning "-32-34"] type t = delta_resolver let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -25,6 +26,7 @@ end let empty_delta_resolver = Deltamap.empty module Umap = struct + [@@@ocaml.warning "-32-34"] type 'a t = 'a umap_t let empty = MPmap.empty, MBImap.empty let is_empty (m1,m2) = MPmap.is_empty m1 && MBImap.is_empty m2 @@ -194,7 +196,7 @@ let subst_con0 sub con u = let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in match constant_of_delta_with_inline resolve con' with - | Some t -> con', t + | Some t -> con', subst_instance_constr u t | None -> let con'' = match side with | User -> constant_of_delta resolve con' @@ -461,13 +463,6 @@ let is_opaque cb = match cb.const_body with let opaque_univ_context cb = force_lazy_constr_univs cb.const_body -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) - let subst_recarg sub r = match r with | Norec -> r | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in @@ -489,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true - | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 - | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 + | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2 + | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2 | _ -> false let eq_wf_paths = Rtree.equal eq_recarg @@ -515,27 +510,22 @@ let subst_decl_arity f g sub ar = if x' == x then ar else TemplateArity x' -let map_decl_arity f g = function - | RegularArity a -> RegularArity (f a) - | TemplateArity a -> TemplateArity (g a) - let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - -let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true (* TODO: should be changed to non-coping after Term.subst_mps *) (* NB: we leave bytecode and native code fields untouched *) let subst_const_body sub cb = { cb with const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type } + const_type = subst_mps sub cb.const_type } let subst_regular_ind_arity sub s = @@ -583,34 +573,36 @@ let implem_map fs fa = function | Algebraic a -> Algebraic (fa a) | impl -> impl -let subst_with_body sub = function - | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) - | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx)) - let rec subst_expr sub = function | MEident mp -> MEident (subst_mp sub mp) | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2) - | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd) + | MEwith (me,wd)-> MEwith (subst_expr sub me, wd) let rec subst_expression sub me = - functor_map (subst_module sub) (subst_expr sub) me + functor_map (subst_module_type sub) (subst_expr sub) me and subst_signature sub sign = - functor_map (subst_module sub) (subst_structure sub) sign + functor_map (subst_module_type sub) (subst_structure sub) sign and subst_structure sub struc = 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_module sub mtb) + | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb) in List.map (fun (l,b) -> (l,subst_body b)) struc -and subst_module sub mb = +and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun subst_impl sub mb -> { mb with mod_mp = subst_mp sub mb.mod_mp; - mod_expr = - implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr; + mod_expr = subst_impl sub mb.mod_expr; mod_type = subst_signature sub mb.mod_type; mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg } + +and subst_module sub mb = + subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb + +and subst_module_type sub mb = + subst_body (fun _ () -> ()) sub mb diff --git a/checker/declarations.mli b/checker/declarations.mli index 456df836..7458b3e0 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool val opaque_univ_context : constant_body -> Univ.ContextSet.t +val constant_is_polymorphic : constant_body -> bool (* Mutual inductives *) @@ -33,12 +34,12 @@ val empty_delta_resolver : delta_resolver type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_mbid : MBId.t -> module_path -> substitution -> substitution -val add_mp : module_path -> module_path -> substitution -> substitution -val map_mbid : MBId.t -> module_path -> substitution -val map_mp : module_path -> module_path -> substitution -val mp_in_delta : module_path -> delta_resolver -> bool -val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive +val add_mbid : MBId.t -> ModPath.t -> substitution -> substitution +val add_mp : ModPath.t -> ModPath.t -> substitution -> substitution +val map_mbid : MBId.t -> ModPath.t -> substitution +val map_mp : ModPath.t -> ModPath.t -> substitution +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val mind_of_delta : delta_resolver -> MutInd.t -> MutInd.t val subst_const_body : constant_body subst_fun val subst_mind : mutual_inductive_body subst_fun diff --git a/checker/environ.ml b/checker/environ.ml index 7b59c6b9..bbd043c8 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -8,7 +8,7 @@ open Declarations type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -21,7 +21,15 @@ type env = { env_globals : globals; env_rel_context : rel_context; env_stratification : stratification; - env_imports : Cic.vodigest MPmap.t } + env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : oracle; } + +let empty_oracle = { + var_opacity = Id.Map.empty; + cst_opacity = Cmap.empty; + var_trstate = Id.Pred.empty; + cst_trstate = Cpred.empty; +} let empty_env = { env_globals = @@ -34,7 +42,8 @@ let empty_env = { env_stratification = { env_universes = Univ.initial_universes; env_engagement = PredicativeSet }; - env_imports = MPmap.empty } + env_imports = MPmap.empty; + env_conv_oracle = empty_oracle } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes @@ -45,12 +54,14 @@ let set_engagement (impr_set as c) env = env.env_stratification.env_engagement in begin match impr_set,expected_impr_set with - | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" + | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement") | _ -> () end; { env with env_stratification = { env.env_stratification with env_engagement = c } } +let set_oracle env oracle = { env with env_conv_oracle = oracle } + (* Digests *) let add_digest env dp digest = @@ -106,7 +117,7 @@ let anomaly s = anomaly (Pp.str s) let add_constant kn cs env = if Cmap_env.mem kn env.env_globals.env_constants then - Printf.ksprintf anomaly ("Constant %s is already defined") + Printf.ksprintf anomaly ("Constant %s is already defined.") (Constant.to_string kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in @@ -120,35 +131,33 @@ type const_evaluation_result = NoBody | Opaque (* Constant types *) let constraints_of cb u = - let univs = cb.const_universes in - Univ.subst_instance_constraints u (Univ.UContext.constraints univs) - -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false + match cb.const_universes with + | Monomorphic_const _ -> Univ.Constraint.empty + | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - if cb.const_polymorphic then - let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) - else cb.const_type, Univ.Constraint.empty + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty + | Polymorphic_const ctx -> + let csts = constraints_of cb u in + (subst_instance_constr u cb.const_type, csts) exception NotEvaluableConst of const_evaluation_result let constant_value env (kn,u) = let cb = lookup_constant kn env in - match cb.const_body with - | Def l_body -> - let b = force_constr l_body in - if cb.const_polymorphic then - subst_instance_constr u (force_constr l_body) - else b - | OpaqueDef _ -> raise (NotEvaluableConst Opaque) - | Undef _ -> raise (NotEvaluableConst NoBody) + match cb.const_body with + | Def l_body -> + let b = force_constr l_body in + begin + match cb.const_universes with + | Monomorphic_const _ -> b + | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body) + end + | OpaqueDef _ -> raise (NotEvaluableConst Opaque) + | Undef _ -> raise (NotEvaluableConst NoBody) (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant cst env = @@ -161,7 +170,7 @@ let is_projection cst env = let lookup_projection p env = match (lookup_constant (Projection.constant p) env).const_proj with | Some pb -> pb - | None -> anomaly ("lookup_projection: constant is not a projection") + | None -> anomaly ("lookup_projection: constant is not a projection.") (* Mutual Inductives *) let scrape_mind env kn= @@ -182,7 +191,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined") + Printf.ksprintf anomaly ("Inductive %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in @@ -201,7 +210,7 @@ let add_mind kn mib env = let add_modtype ln mtb env = if MPmap.mem ln env.env_globals.env_modtypes then - Printf.ksprintf anomaly ("Module type %s is already defined") + Printf.ksprintf anomaly ("Module type %s is already defined.") (ModPath.to_string ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = @@ -211,7 +220,7 @@ let add_modtype ln mtb env = let shallow_add_module mp mb env = if MPmap.mem mp env.env_globals.env_modules then - Printf.ksprintf anomaly ("Module %s is already defined") + Printf.ksprintf anomaly ("Module %s is already defined.") (ModPath.to_string mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = @@ -221,7 +230,7 @@ let shallow_add_module mp mb env = let shallow_remove_module mp env = if not (MPmap.mem mp env.env_globals.env_modules) then - Printf.ksprintf anomaly ("Module %s is unknown") + Printf.ksprintf anomaly ("Module %s is unknown.") (ModPath.to_string mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = diff --git a/checker/environ.mli b/checker/environ.mli index 87f143d1..81da8387 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -6,7 +6,7 @@ open Cic type globals = { env_constants : constant_body Cmap_env.t; env_inductives : mutual_inductive_body Mindmap_env.t; - env_inductives_eq : kernel_name KNmap.t; + env_inductives_eq : KerName.t KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} type stratification = { @@ -18,6 +18,7 @@ type env = { env_rel_context : rel_context; env_stratification : stratification; env_imports : Cic.vodigest MPmap.t; + env_conv_oracle : Cic.oracle; } val empty_env : env @@ -25,6 +26,10 @@ val empty_env : env val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env +(** Oracle *) + +val set_oracle : env -> Cic.oracle -> env + (* Digests *) val add_digest : env -> DirPath.t -> Cic.vodigest -> env val lookup_digest : env -> DirPath.t -> Cic.vodigest @@ -34,7 +39,7 @@ val rel_context : env -> rel_context 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_rec_types : Name.t array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes @@ -44,31 +49,31 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) -val lookup_constant : constant -> env -> Cic.constant_body -val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constant_type Univ.constrained +val lookup_constant : Constant.t -> env -> Cic.constant_body +val add_constant : Constant.t -> Cic.constant_body -> env -> env +val constant_type : env -> Constant.t puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant puniverses -> constr -val evaluable_constant : constant -> env -> bool +val constant_value : env -> Constant.t puniverses -> constr +val evaluable_constant : Constant.t -> env -> bool -val is_projection : constant -> env -> bool -val lookup_projection : projection -> env -> projection_body +val is_projection : Constant.t -> env -> bool +val lookup_projection : Projection.t -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool val lookup_mind : - mutual_inductive -> env -> Cic.mutual_inductive_body + MutInd.t -> env -> Cic.mutual_inductive_body val add_mind : - mutual_inductive -> Cic.mutual_inductive_body -> env -> env + MutInd.t -> Cic.mutual_inductive_body -> env -> env (* Modules *) val add_modtype : - module_path -> Cic.module_type_body -> env -> env + ModPath.t -> Cic.module_type_body -> env -> env val shallow_add_module : - module_path -> Cic.module_body -> env -> env -val shallow_remove_module : module_path -> env -> env -val lookup_module : module_path -> env -> Cic.module_body -val lookup_modtype : module_path -> env -> Cic.module_type_body + ModPath.t -> Cic.module_body -> env -> env +val shallow_remove_module : ModPath.t -> env -> env +val lookup_module : ModPath.t -> env -> Cic.module_body +val lookup_modtype : ModPath.t -> env -> Cic.module_type_body diff --git a/checker/include b/checker/include index 6bea3c91..da034635 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp4";; #directory "+camlp5";; #load "unix.cma";; @@ -116,7 +115,7 @@ let prsub s = #install_printer prsub;;*) Checker.init_with_argv [|"";"-coqlib";"."|];; -Flags.make_silent false;; +Flags.quiet := false;; Flags.debug := true;; Sys.catch_break true;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 27f79e79..916934a8 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [] - | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") + | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor.") (* Prop and Set are small *) @@ -302,11 +304,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_vect" (Pp.str "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 ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur.") (* Conclusion of constructors: check the inductive type is called with the expected parameters *) @@ -502,10 +504,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc indlc in mk_paths (Mrec ind) irecargs +let prrecarg = function + | Norec -> str "Norec" + | Mrec (mind,i) -> + str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + | Imbr (mind,i) -> + str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]" + let check_subtree t1 t2 = let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in if not (Rtree.equiv eq_recarg cmp_labels t1 t2) - then failwith "bad recursive trees" + then user_err Pp.(str "Bad recursive tree: found " ++ fnl () + ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl () + ++ Rtree.pp_tree prrecarg t2) (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*) let check_positivity env_ar mind params nrecp inds = @@ -524,29 +535,104 @@ let check_positivity env_ar mind params nrecp inds = let wfp = Rtree.mk_rec irecargs in Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp +(* Check arities and constructors *) +let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity = + let numchecked = ref 0 in + let basic_check ev tp = + if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp); + numchecked := !numchecked + 1 + in + let check_typ typ typ_env = + match typ with + | LocalAssum (_, typ') -> + begin + try + basic_check typ_env typ'; Environ.push_rel typ typ_env + with NotConvertible -> + anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation") + end + | _ -> anomaly (Pp.str "") + in + let typs, codom = dest_prod env arcn in + let last_env = fold_rel_context_outside check_typ typs ~init:env in + if not is_arity then basic_check last_env codom else () + +(* Check that the subtyping information inferred for inductive types in the block is correct. *) +(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) +let check_subtyping cumi paramsctxt env inds = + let open Univ in + let numparams = rel_context_nhyps paramsctxt in + (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available. + We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n] + and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together + with the cumulativity constraints [ cumul_cst ]. *) + let uctx = ACumulativityInfo.univ_context cumi in + let len = AUContext.size uctx in + let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in + + let other_context = ACumulativityInfo.univ_context cumi in + let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in + let cumul_cst = + Array.fold_left_i (fun i csts var -> + match var with + | Variance.Irrelevant -> csts + | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts + | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts) + Constraint.empty (ACumulativityInfo.variance cumi) + in + let env = Environ.push_context uctx_other env in + let env = Environ.add_constraints cumul_cst env in + + (* process individual inductive types: *) + Array.iter (fun { mind_user_lc = lc; mind_arity = arity } -> + match arity with + | RegularArity { mind_user_arity = full_arity} -> + check_subtyping_arity_constructor env inst full_arity numparams true; + Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc + | TemplateArity _ -> () + ) inds + (************************************************************************) (************************************************************************) let check_inductive env kn mib = Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); (* check mind_constraints: should be consistent with env *) - let env = add_constraints (Univ.UContext.constraints mib.mind_universes) env in + let env0 = + match mib.mind_universes with + | Monomorphic_ind _ -> env + | Polymorphic_ind auctx -> + let uctx = Univ.AUContext.repr auctx in + Environ.push_context uctx env + | Cumulative_ind cumi -> + let uctx = Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi) in + Environ.push_context uctx env + in + (** Locally set the oracle for further typechecking *) + let env0 = Environ.set_oracle env0 mib.mind_typing_flags.conv_oracle 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"; + user_err Pp.(str "not the right number of packets"); (* check mind_params_ctxt *) let params = mib.mind_params_ctxt in - let _ = check_ctxt env params in + let _ = check_ctxt env0 params in (* check mind_nparams *) if rel_context_nhyps params <> mib.mind_nparams then - error "number the right number of parameters"; + user_err Pp.(str "number the right number of parameters"); (* mind_packets *) (* - check arities *) - let env_ar = typecheck_arity env params mib.mind_packets in + let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + (* check the inferred subtyping relation *) + let () = + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> () + | Cumulative_ind acumi -> + check_subtyping acumi params env_ar mib.mind_packets + in (* check mind_nparams_rec: positivity condition *) check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 071eecbb..baaa66a6 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds -val prcon : constant -> Pp.std_ppcmds +val prkn : KerName.t -> Pp.t +val prcon : Constant.t -> Pp.t (*s The different kinds of errors that may result of a malformed inductive definition. *) @@ -34,4 +36,4 @@ exception InductiveError of inductive_error (*s The following function does checks on inductive declarations. *) -val check_inductive : env -> mutual_inductive -> mutual_inductive_body -> env +val check_inductive : env -> MutInd.t -> mutual_inductive_body -> env diff --git a/checker/inductive.ml b/checker/inductive.ml index c4ffc141..e1c6b135 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* = Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -54,10 +56,17 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let inductive_instance mib = - if mib.mind_polymorphic then - UContext.instance mib.mind_universes - else Instance.empty +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (************************************************************************) @@ -75,7 +84,7 @@ let constructor_instantiate mind u mib c = let instantiate_params full t u args sign = let fail () = - anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch.") in let (rem_args, subs, ty) = fold_rel_context (fun decl (largs,subs,ty) -> @@ -93,7 +102,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (subst_instance_context u sign,dummy) in + let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = @@ -149,7 +158,7 @@ let remember_subst u subst = (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = +let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) @@ -199,7 +208,7 @@ let instantiate_universes env ctx ar argsorts = let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> - if not mib.mind_polymorphic then a.mind_user_arity + if not (inductive_is_polymorphic mib) then a.mind_user_arity else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in @@ -232,7 +241,7 @@ let type_of_constructor_subst cstr u (mib,mip) = 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."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = @@ -374,7 +383,7 @@ let type_case_branches env (pind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (eq_ind indsp ci.ci_ind) || + not (eq_ind_chk indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || (mip.mind_consnrealargs <> ci.ci_cstr_nargs) @@ -428,27 +437,14 @@ type subterm_spec = | Dead_code | Not_subterm -let eq_recarg r1 r2 = match r1, r2 with -| Norec, Norec -> true -| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 -| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 -| _ -> false - let eq_wf_paths = Rtree.equal eq_recarg -let pp_recarg = function - | Norec -> Pp.str "Norec" - | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i)) - | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i)) - -let pp_wf_paths = Rtree.pp_tree pp_recarg - let inter_recarg r1 r2 = match r1, r2 with | Norec, Norec -> Some r1 | Mrec i1, Mrec i2 | Imbr i1, Imbr i2 -| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None -| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None +| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None +| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None | _ -> None let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec @@ -544,7 +540,7 @@ let lookup_subterms env ind = let match_inductive ind ra = match ra with - | (Mrec i | Imbr i) -> eq_ind ind i + | (Mrec i | Imbr i) -> eq_ind_chk ind i | Norec -> false (* In {match c as z in ci y_s return P with |C_i x_s => t end} @@ -645,7 +641,7 @@ let get_recargs_approx env tree ind args = (* When the inferred tree allows it, we consider that we have a potential nested inductive type *) begin match dest_recarg tree with - | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' -> + | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' -> build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end @@ -993,7 +989,7 @@ let check_one_fix renv recpos trees def = List.iter (check_rec_call renv []) l; check_rec_call renv [] c - | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") + | Var _ -> anomaly (Pp.str "Section variable in Coqchk!") | Sort _ -> assert (l = []) @@ -1011,7 +1007,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly (Pp.str "Not enough abstractions in fix body") + | _ -> anomaly (Pp.str "Not enough abstractions in fix body.") in check_rec_call renv [] def @@ -1025,7 +1021,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || Array.length names <> nbfix || bodynum < 0 || bodynum >= nbfix - then anomaly (Pp.str "Ill-formed fix term"); + then anomaly (Pp.str "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 @@ -1046,7 +1042,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -1070,8 +1066,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) @@ -1080,7 +1076,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor.") let rec codomain_is_coind env c = let b = whd_all env c in diff --git a/checker/inductive.mli b/checker/inductive.mli index ed3a7b53..0ca0d14a 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* inductive -> mind_specif -val inductive_instance : mutual_inductive_body -> Univ.universe_instance +val inductive_is_polymorphic : mutual_inductive_body -> bool + +val inductive_is_cumulative : mutual_inductive_body -> bool val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: diff --git a/checker/main.mli b/checker/main.mli new file mode 100644 index 00000000..9db9ecd1 --- /dev/null +++ b/checker/main.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* - let ul = Univ.Level.make DirPath.empty 1 in - let u' = Univ.Universe.make ul in - let cst = Univ.enforce_leq u u' Univ.empty_constraint in - let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in - mkArity (ctxt,Prop Null), ctx - | _ -> ar, Univ.ContextSet.empty - let check_constant_declaration env kn cb = - Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); + Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn); + (** Locally set the oracle for further typechecking *) + let oracle = env.env_conv_oracle in + let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in + (** [env'] contains De Bruijn universe variables *) let env' = - if cb.const_polymorphic then - let inst = Univ.make_abstract_instance cb.const_universes in - let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in - push_context ~strict:false ctx env - else push_context ~strict:true cb.const_universes env - in - let envty, ty = - match cb.const_type with - RegularArity ty -> - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in envty, ty - | TemplateArity(ctxt,par) -> - let _ = check_ctxt env' ctxt in - check_polymorphic_arity env' ctxt par; - env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + match cb.const_universes with + | Monomorphic_const ctx -> push_context_set ~strict:true ctx env + | Polymorphic_const auctx -> + let ctx = Univ.AUContext.repr auctx in + push_context ~strict:false ctx env in + let ty = cb.const_type in + let () = ignore(infer_type env' ty) in let () = match body_of_constant cb with | Some bd -> (match cb.const_proj with - | None -> let j = infer envty bd in - conv_leq envty j ty + | None -> let j = infer env' bd in + conv_leq env' j ty | Some pb -> let env' = add_constant kn cb env' in let j = infer env' bd in - conv_leq envty j ty) + conv_leq env' j ty) | None -> () in - if cb.const_polymorphic then add_constant kn cb env - else add_constant kn cb env' + let env = + if constant_is_polymorphic cb then add_constant kn cb env + else add_constant kn cb env' + in + (** Reset the value of the oracle *) + Environ.set_oracle env oracle (** {6 Checking modules } *) @@ -74,12 +60,12 @@ let lookup_module mp env = let mk_mtb mp sign delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; mod_delta = delta; - mod_retroknowledge = []; } + mod_retroknowledge = ModTypeRK; } let rec check_module env mp mb = let (_:module_signature) = diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 5c7b392f..c9e7f9a1 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Names.module_path -> Cic.module_body -> unit +val check_module : Environ.env -> Names.ModPath.t -> Cic.module_body -> unit diff --git a/checker/modops.ml b/checker/modops.ml index b720fb62..c7ad0977 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true @@ -49,7 +51,7 @@ let destr_functor = function | NoFunctor _ -> error_not_a_functor () let module_body_of_type mp mtb = - { mtb with mod_mp = mp; mod_expr = Abstract } + { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] } let rec add_structure mp sign resolver env = let add_one env (l,elem) = @@ -83,27 +85,29 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - let u = - if cb.const_polymorphic then - Univ.make_abstract_instance cb.const_universes - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const auctx -> Univ.make_abstract_instance auctx in { cb with const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb - else strengthen_body true mp_from mp_to mb + else + let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in + strengthen_body mk_expr mp_from mp_to mb -and strengthen_body is_mod mp_from mp_to mb = +and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun mk_expr mp_from mp_to mb -> match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta in { mb with - mod_expr = - (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract); + mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } @@ -130,7 +134,7 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item::rest' let strengthen mtb mp = - strengthen_body false mtb.mod_mp mp mtb + strengthen_body ignore mtb.mod_mp mp mtb let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) @@ -138,9 +142,9 @@ let subst_and_strengthen mb mp = let module_type_of_module mp mb = let mtb = { mb with - mod_expr = Abstract; + mod_expr = (); mod_type_alg = None; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } in match mp with | Some mp -> strengthen {mtb with mod_mp = mp} mp diff --git a/checker/modops.mli b/checker/modops.mli index 26a088f3..9f6f7811 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_body -> module_type_body + ModPath.t option -> module_body -> module_type_body val is_functor : ('ty,'a) functorize -> bool @@ -24,24 +26,24 @@ val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize (* adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val add_module_type : module_path -> module_type_body -> env -> env +val add_module_type : ModPath.t -> module_type_body -> env -> env -val strengthen : module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> ModPath.t -> module_type_body -val subst_and_strengthen : module_body -> module_path -> module_body +val subst_and_strengthen : module_body -> ModPath.t -> module_body val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a -val error_not_match : label -> structure_field_body -> 'a +val error_not_match : Label.t -> structure_field_body -> 'a val error_with_module : unit -> 'a -val error_no_such_label : label -> 'a +val error_no_such_label : Label.t -> 'a val error_no_such_label_sub : - label -> module_path -> 'a + Label.t -> ModPath.t -> 'a -val error_not_a_constant : label -> 'a +val error_not_a_constant : Label.t -> 'a -val error_not_a_module : label -> 'a +val error_not_a_module : Label.t -> 'a diff --git a/checker/print.ml b/checker/print.ml index 7ef752b0..fc9cd687 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -1,146 +1,96 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* pp fmt (i,x)) a +let pp_instance fmt i = chk_pp fmt (Univ.Instance.pr i) +let pp_id fmt id = fprintf fmt "%s" (Id.to_string id) -let print_instance i = chk_pp (Univ.Instance.pr i) - -let print_pure_constr csr = - let rec term_display c = match c with - | Rel n -> print_string "#"; print_int n - | Meta n -> print_string "Meta("; print_int n; print_string ")" - | Var id -> print_string (Id.to_string id) - | Sort s -> sort_display s - | Cast (c,_, t) -> open_hovbox 1; - print_string "("; (term_display c); print_cut(); - print_string "::"; (term_display t); print_string ")"; close_box() +let print_pure_constr fmt csr = + let rec pp_term fmt c = match c with + | Rel n -> fprintf fmt "#%d" n + | Meta n -> fprintf fmt "Meta(%d)" n + | Var id -> pp_id fmt id + | Sort s -> pp_sort fmt s + | Cast (c,_, t) -> + fprintf fmt "@[(%a@;::%a)@]" pp_term c pp_term t | Prod (Name(id),t,c) -> - open_hovbox 1; - print_string"("; print_string (Id.to_string id); - print_string ":"; box_display t; - print_string ")"; print_cut(); - box_display c; close_box() + fprintf fmt "@[(%a:%a)@;@[%a@]@]" pp_id id pp_term t pp_term c | Prod (Anonymous,t,c) -> - print_string"("; box_display t; print_cut(); print_string "->"; - box_display c; print_string ")"; + fprintf fmt "(%a@,->@[%a@])" pp_term t pp_term c | Lambda (na,t,c) -> - print_string "["; name_display na; - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a:@[%a@]]@,@[%a@]" pp_name na pp_term t pp_term c | LetIn (na,b,t,c) -> - print_string "["; name_display na; print_string "="; - box_display b; print_cut(); - print_string ":"; box_display t; print_string "]"; - print_cut(); box_display c; + fprintf fmt "[%a=@[%a@]@,:@[%a@]]@,@[%a@]" pp_name na pp_term b pp_term t pp_term c | App (c,l) -> - print_string "("; - box_display c; - Array.iter (fun x -> print_space (); box_display x) l; - print_string ")" - | Evar _ -> print_string "Evar#" - | Const (c,u) -> print_string "Cons("; - sp_con_display c; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "(@[%a@]@, @[%a@])" pp_term c (pp_arrayi (fun _ (_,s) -> fprintf fmt "@[%a@]@," pp_term s)) l; + | Evar _ -> pp_print_string fmt "Evar#" + | Const (c,u) -> + fprintf fmt "Cons(@[%a,%a@])" sp_con_display c pp_instance u | Ind ((sp,i),u) -> - print_string "Ind("; - sp_display sp; - print_string ","; print_int i; - print_string ","; print_instance u; - print_string ")" + fprintf fmt "Ind(@[%a,%d,%a@])" sp_display sp i pp_instance u | Construct (((sp,i),j),u) -> - print_string "Constr("; - sp_display sp; - print_string ","; - print_int i; print_string ","; print_int j; - print_string ","; print_instance u; print_string ")" + fprintf fmt "Constr(%a,%d,%d,%a)" sp_display sp i j pp_instance u | Case (ci,p,c,bl) -> - open_vbox 0; - print_string "<"; box_display p; print_string ">"; - print_cut(); print_string "Case"; - print_space(); box_display c; print_space (); print_string "of"; - open_vbox 0; - Array.iter (fun x -> print_cut(); box_display x) bl; - close_box(); - print_cut(); - print_string "end"; - close_box() + let pp_match fmt (_,mc) = fprintf fmt " @[%a@]" pp_term mc in + fprintf fmt "@[<@[%a@]>@,Case@ @[%a@]@ of@[%a@]@,end@]" pp_term p pp_term c (pp_arrayi pp_match) bl | Fix ((t,i),(lna,tl,bl)) -> - print_string "Fix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 0; - name_display lna.(k); print_string "/"; - print_int t.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut() - done - in print_string"{"; print_fix(); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[ %a/%d@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) t.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "Fix(%d)@,@[{%a}@]" i (pp_arrayi pp_fixc) tl | CoFix(i,(lna,tl,bl)) -> - print_string "CoFix("; print_int i; print_string ")"; - print_cut(); - open_vbox 0; - let print_fix () = - for k = 0 to (Array.length tl) - 1 do - open_vbox 1; - name_display lna.(k); print_cut(); print_string ":"; - box_display tl.(k) ; print_cut(); print_string ":="; - box_display bl.(k); close_box (); - print_cut(); - done - in print_string"{"; print_fix (); print_string"}" + let pp_fixc fmt (k,_) = + fprintf fmt "@[ %a@,:@[%a@]@,:=@[%a@]@]@," pp_name lna.(k) pp_term tl.(k) pp_term bl.(k) in + fprintf fmt "CoFix(%d)@,@[{%a}@]" i (pp_arrayi pp_fixc) tl | Proj (p, c) -> - print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; - box_display c; print_string ")" + fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c - and box_display c = open_hovbox 1; term_display c; close_box() + and pp_sort fmt = function + | Prop(Pos) -> pp_print_string fmt "Set" + | Prop(Null) -> pp_print_string fmt "Prop" + | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) - and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" + and pp_name fmt = function + | Name id -> pp_id fmt id + | Anonymous -> pp_print_string fmt "_" - and name_display = function - | Name id -> print_string (Id.to_string id) - | Anonymous -> print_string "_" (* Remove the top names for library and Scratch to avoid long names *) - and sp_display sp = -(* let dir,l = decode_kn sp in + and sp_display fmt sp = +(* let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (MutInd.debug_to_string sp) - and sp_con_display sp = -(* let dir,l = decode_kn sp in + pp_print_string fmt (MutInd.debug_to_string sp) + + and sp_con_display fmt sp = + (* + let dir,l = decode_kn sp in let ls = match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (Constant.debug_to_string sp) + pp_print_string fmt (Constant.debug_to_string sp) in - try - box_display csr; print_flush() - with e -> - print_string (Printexc.to_string e);print_flush (); - raise e - - - + try + fprintf fmt "@[%a@]%!" pp_term csr + with e -> + pp_print_string fmt (Printexc.to_string e); + print_flush (); + raise e diff --git a/checker/print.mli b/checker/print.mli new file mode 100644 index 00000000..da1362ca --- /dev/null +++ b/checker/print.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* constr -> unit diff --git a/checker/reduction.ml b/checker/reduction.ml index ec16aa26..4e508dc7 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,11 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | ((ZcaseT(c1,_,_,_))::s1, + (ZcaseT(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 @@ -52,7 +55,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.projection * lift + | Zlproj of Names.Projection.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -78,8 +81,7 @@ let pure_stack lfts stk = (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,env),(l,pstk)) -> (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + ) in snd (pure_rec lfts stk) (****************************************************************************) @@ -117,6 +119,10 @@ let beta_appvect c v = (* Conversion *) (********************************************************************) +type conv_pb = + | CONV + | CUMUL + (* Conversion utility functions *) type 'a conversion_function = env -> 'a -> 'a -> unit @@ -137,7 +143,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Names.eq_con_chk + if not (Names.Constant.UserOrd.equal (Names.Projection.constant c1) (Names.Projection.constant c2)) then raise NotConvertible @@ -152,11 +158,55 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) else raise NotConvertible -(* Convertibility of sorts *) +let convert_inductive_instances cv_pb cumi u u' univs = + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in + if not ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let variance = Univ.ACumulativityInfo.variance cumi in + let comp_cst = + match cv_pb with + | CONV -> + Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty + | CUMUL -> + Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty + in + if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible + +let convert_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 univs = + match mind.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 + | Cumulative_ind cumi -> + let num_param_arity = + mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + convert_universes univs u1 u2 + else + convert_inductive_instances cv_pb cumi u1 u2 univs + +let convert_constructors + (mind, ind, cns) u1 sv1 u2 sv2 univs = + match mind.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 + | Cumulative_ind cumi -> + let num_cnstr_args = + let nparamsctxt = + mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs + in + nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + convert_universes univs u1 u2 + else + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + () -type conv_pb = - | CONV - | CUMUL +(* Convertibility of sorts *) let sort_cmp env univ pb s0 s1 = match (s0,s1) with @@ -176,9 +226,9 @@ let sort_cmp env univ pb s0 s1 = then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds - (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ)) + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) end; raise NotConvertible end @@ -190,7 +240,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -203,7 +252,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -213,13 +261,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,_) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk @@ -227,16 +274,34 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false -let oracle_order fl1 fl2 = - match fl1,fl2 with - ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false - | _, ConstKey _ -> true - | _ -> false - -let unfold_projection infos p c = - let pb = lookup_projection p (infos_env infos) in - let s = Zproj (pb.proj_npars, pb.proj_arg, p) in - (c, s) +let default_level = Level 0 + +let get_strategy { var_opacity; cst_opacity } = function + | VarKey id -> + (try Names.Id.Map.find id var_opacity + with Not_found -> default_level) + | ConstKey (c, _) -> + (try Names.Cmap.find c cst_opacity + with Not_found -> default_level) + | RelKey _ -> Expand + +let oracle_order infos l2r k1 k2 = + let o = Closure.oracle_of_infos infos in + match get_strategy o k1, get_strategy o k2 with + | Expand, Expand -> l2r + | Expand, (Opaque | Level _) -> true + | (Opaque | Level _), Expand -> false + | Opaque, Opaque -> l2r + | Level _, Opaque -> true + | Opaque, Level _ -> false + | Level n1, Level n2 -> + if Int.equal n1 n2 then l2r + else n1 < n2 + +let eq_table_key univ = + Names.eq_table_key (fun (c1,u1) (c2,u2) -> + Constant.UserOrd.equal c1 c2 && + Univ.Instance.check_eq univ u1 u2) (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = @@ -284,13 +349,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if eq_table_key fl1 fl2 + if eq_table_key univ 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) = - if oracle_order fl1 fl2 then + if oracle_order infos false fl1 fl2 then match unfold_reference infos fl1 with | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2) | None -> @@ -307,12 +372,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = eqappr univ cv_pb infos app1 app2) | (FProj (p1,c1), _) -> - let (def1, s1) = unfold_projection infos p1 c1 in - eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2 + let s1 = unfold_projection (infos_env infos) p1 in + eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2 | (_, FProj (p2,c2)) -> - let (def2, s2) = unfold_projection infos p2 c2 in - eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2)) + let s2 = unfold_projection (infos_env infos) p2 in + eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2)) (* other constructors *) | (FLambda _, FLambda _) -> @@ -333,13 +398,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr univ CONV infos (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) | (_, FLambda _) -> if v2 <> [] then - anomaly (Pp.str "conversion was given unreduced term (FLambda)"); + anomaly (Pp.str "conversion was given unreduced term (FLambda)."); let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr univ CONV infos (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) @@ -375,18 +440,37 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> - if mind_equiv_infos infos ind1 ind2 - then - (let () = convert_universes univ u1 u2 in - convert_stacks univ infos lft1 lft2 v1 v2) - else raise NotConvertible - - | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 - then - (let () = convert_universes univ u1 u2 in - convert_stacks univ infos lft1 lft2 v1 v2) - else raise NotConvertible + if mind_equiv_infos infos ind1 ind2 then + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + begin + convert_universes univ u1 u2; + convert_stacks univ infos lft1 lft2 v1 v2 + end + else + let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in + let () = + convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1) + u2 (stack_args_size v2) univ + in + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible + + | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> + if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then + if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then + begin + convert_universes univ u1 u2; + convert_stacks univ infos lft1 lft2 v1 v2 + end + else + let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in + let () = + convert_constructors + (mind, snd ind1, j1) u1 (stack_args_size v1) + u2 (stack_args_size v2) univ + in + convert_stacks univ infos lft1 lft2 v1 v2 + else raise NotConvertible (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> @@ -432,8 +516,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) @@ -479,7 +563,7 @@ let vm_conv cv_pb = fconv cv_pb true let hnf_prod_app env t n = match whd_all env t with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl @@ -508,7 +592,6 @@ let dest_prod_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in prodec_rec (push_rel d env) (d::l) c - | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty @@ -526,7 +609,6 @@ let dest_lam_assum env = | LetIn (x,b,t,c) -> let d = LocalDef (x,b,t) in lamec_rec (push_rel d env) (d::l) c - | Cast (c,_,_) -> lamec_rec env l c | _ -> l,rty in lamec_rec env empty_rel_context @@ -536,5 +618,5 @@ 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" + | _ -> user_err Pp.(str "not an arity") diff --git a/checker/reduction.mli b/checker/reduction.mli index 15a2df1f..3bbf4654 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end; () @@ -61,7 +63,7 @@ let check_imports f caller env needed = 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 " ^ (DirPath.to_string dp)) + user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp))) in Array.iter check needed @@ -89,6 +91,6 @@ let import file clib univs digest = let unsafe_import file clib univs digest = let env = !genv in if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps - else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + else check_imports (user_err ~hdr:"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 8724f8e0..51e5ca32 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* error () +let check_polymorphic_instance error env auctx1 auctx2 = + if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then + error () + else if not (Univ.check_subtype (Environ.universes env) auctx2 auctx1) then + error () + else + Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env + (* for now we do not allow reorderings *) let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let kn = MutInd.make2 mp1 l in @@ -88,18 +97,31 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_conv f = check_conv_error error f in let mib1 = match info1 with - | IndType ((_,0), mib) -> mib + | IndType ((_,0), mib) -> subst_mind subst1 mib | _ -> error () in let mib2 = subst_mind subst2 mib2 in let check eq f = if not (eq (f mib1) (f mib2)) then error () in - let bool_equal (x : bool) (y : bool) = x = y in - let u = - check bool_equal (fun x -> x.mind_polymorphic); - if mib1.mind_polymorphic then ( - check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes); - Univ.UContext.instance mib1.mind_universes) - else Univ.Instance.empty + let env, u = + match mib1.mind_universes, mib2.mind_universes with + | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty + | Polymorphic_ind auctx, Polymorphic_ind auctx' -> + let env = check_polymorphic_instance error env auctx auctx' in + env, Univ.make_abstract_instance auctx' + | Cumulative_ind cumi, Cumulative_ind cumi' -> + (** Currently there is no way to control variance of inductive types, but + just in case we require that they are in a subtyping relation. *) + let () = + let v = Univ.ACumulativityInfo.variance cumi in + let v' = Univ.ACumulativityInfo.variance cumi' in + if not (Array.for_all2 Univ.Variance.check_subtype v' v) then + CErrors.anomaly Pp.(str "Variance mismatch for " ++ MutInd.print kn) + in + let auctx = Univ.ACumulativityInfo.univ_context cumi in + let auctx' = Univ.ACumulativityInfo.univ_context cumi' in + let env = check_polymorphic_instance error env auctx auctx' in + env, Univ.make_abstract_instance auctx' + | _ -> error () in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -111,40 +133,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (eq_constr) (fun x -> snd x.proj_eta); check (eq_constr) (fun x -> x.proj_body); true 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_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in let check_packet p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in @@ -163,8 +152,8 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (* 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),u)) (type_of_inductive env ((mib2,p2),u)) + check_inductive_type + (type_of_inductive env ((mib1,p1), u)) (type_of_inductive env ((mib2,p2),u)) in let check_cons_types i p1 p2 = Array.iter2 (check_conv conv env) @@ -201,7 +190,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= | Some None, Some None -> true | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) -> Id.equal id1 id2 && - Array.for_all2 eq_con_chk p1 p2 && + Array.for_all2 Constant.UserOrd.equal p1 p2 && Array.for_all2 eq_projection_body pb1 pb2 | _, _ -> false in @@ -230,59 +219,25 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = - - (* 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 *) - error () - with UserError _ (* "not an arity" *) -> - error () end - | _ -> t1,t2 - else - (t1,t2) in - check_conv conv_leq env t1 t2 - in + let check_type env t1 t2 = check_conv conv_leq env t1 t2 in match info1 with | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in - (*Start by checking types*) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in + (*Start by checking universes *) + let env = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> env + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + check_polymorphic_instance error env auctx1 auctx2 + | Monomorphic_const _, Polymorphic_const _ -> + error () + | Polymorphic_const _, Monomorphic_const _ -> + error () + in + (* Now check types *) + let typ1 = cb1.const_type in + let typ2 = cb2.const_type in check_type env typ1 typ2; (* Now we check the bodies: - A transparent constant can only be implemented by a compatible @@ -302,27 +257,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.error ( + CErrors.user_err (Pp.str ( "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.")); - if constant_has_body cb2 then error () ; - let u = inductive_instance mind1 in - let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) 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 (CErrors.error ( + "name.")) + | IndConstr (((kn,i),j),mind1) -> + CErrors.user_err (Pp.str ( "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.")); - if constant_has_body cb2 then error () ; - let u1 = inductive_instance mind1 in - let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv conv env ty1 ty2 + "name.")) let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in @@ -390,7 +335,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = mod_type = body_t1; mod_type_alg = None; mod_constraints = mtb1.mod_constraints; - mod_retroknowledge = []; + mod_retroknowledge = ModBodyRK []; mod_delta = mtb1.mod_delta} env in check_structure env body_t1 body_t2 equiv diff --git a/checker/subtyping.mli b/checker/subtyping.mli index cc66fc53..bb867186 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 = closedn 0 @@ -227,6 +229,8 @@ let rel_context_nhyps hyps = nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init +let fold_rel_context_outside f l ~init = List.fold_right f l init + let map_rel_decl f = function | LocalAssum (n, typ) as decl -> let typ' = f typ in @@ -273,14 +277,14 @@ let decompose_lam = abstractions *) let decompose_lam_n_assum n = if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match c with | Lambda (x,t,c) -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec empty_rel_context n @@ -306,14 +310,14 @@ let decompose_prod_assum = let decompose_prod_n_assum n = if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else match c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec empty_rel_context n @@ -333,7 +337,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity.") in prodec_rec [] @@ -386,7 +390,7 @@ let compare_constr f t1 t2 = f h1 h2 && List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Const c1, Const c2 -> eq_puniverses Constant.UserOrd.equal c1 c2 | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 && Univ.Instance.equal u1 u2 @@ -414,35 +418,33 @@ let subst_instance_constr subst c = if Univ.Instance.is_empty subst then c else let f u = Univ.subst_instance_instance subst u in - let changed = ref false in - let rec aux t = + let rec aux t = match t with - | Const (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Const (c, u')) + | Const (c, u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Const (c, u')) | Ind (i, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Ind (i, u')) + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Ind (i, u')) | Construct (c, u) -> - if Univ.Instance.is_empty u then t - else - let u' = f u in - if u' == u then t - else (changed := true; Construct (c, u')) - | Sort (Type u) -> + if Univ.Instance.is_empty u then t + else + let u' = f u in + if u' == u then t + else (Construct (c, u')) + | Sort (Type u) -> let u' = Univ.subst_instance_universe subst u in - if u' == u then t else - (changed := true; Sort (sort_of_univ u')) + if u' == u then t else + (Sort (sort_of_univ u')) | _ -> map_constr aux t in - let c' = aux c in - if !changed then c' else c + aux c let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/checker/term.mli b/checker/term.mli index 0af83e05..2524dff1 100644 --- a/checker/term.mli +++ b/checker/term.mli @@ -4,8 +4,6 @@ open Cic val family_of_sort : sorts -> sorts_family val family_equal : sorts_family -> sorts_family -> bool -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 : @@ -35,11 +33,13 @@ 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 fold_rel_context_outside : + (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration 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 compose_lam : (Name.t * constr) list -> constr -> constr +val decompose_lam : constr -> (Name.t * constr) list * constr val decompose_lam_n_assum : int -> constr -> rel_context * constr val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr diff --git a/checker/type_errors.ml b/checker/type_errors.ml index b7718e02..50796437 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unsafe_judgment array -> 'a val error_ill_formed_rec_body : - env -> guard_error -> name array -> int -> 'a + env -> guard_error -> Name.t array -> int -> 'a val error_ill_typed_rec_body : - env -> int -> name array -> unsafe_judgment array -> constr array -> 'a + env -> int -> Name.t array -> unsafe_judgment array -> constr array -> 'a val error_unsatisfied_constraints : env -> Univ.constraints -> 'a diff --git a/checker/typeops.ml b/checker/typeops.ml index 173e19ce..18f07dc0 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t - | TemplateArity (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_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = +let judge_of_constant env (kn,u as cst) = let _cb = try lookup_constant kn env with Not_found -> failwith ("Cannot find constant: "^Constant.to_string kn) in - let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -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 = @@ -265,7 +245,7 @@ let rec execute env cstr = | Rel n -> judge_of_relative env n - | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") + | Var _ -> anomaly (Pp.str "Section variable in Coqchk!") | Const c -> judge_of_constant env c @@ -278,13 +258,9 @@ let rec execute env cstr = 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 *) + (* No template polymorphism *) execute env f in let jl = Array.map2 (fun c ty -> c,ty) args jl in @@ -334,7 +310,6 @@ let rec execute env cstr = let pj = execute env p in let lfj = execute_array env lf in judge_of_case env ci (p,pj) (c,cj) lfj - | Fix ((_,i as vni),recdef) -> let fix_ty = execute_recdef env recdef i in let fix = (vni,recdef) in @@ -349,10 +324,10 @@ let rec execute env cstr = (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") + anomaly (Pp.str "the kernel does not support metavariables.") | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") + anomaly (Pp.str "the kernel does not support existential variables.") and execute_type env constr = let j = execute env constr in diff --git a/checker/typeops.mli b/checker/typeops.mli index db8e467a..c2d7d19c 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* constr -> sorts val check_ctxt : env -> rel_context -> env val check_polymorphic_arity : env -> rel_context -> template_arity -> unit - -val type_of_constant_type : env -> constant_type -> constr - diff --git a/checker/univ.ml b/checker/univ.ml index 668f3a05..1619010c 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* int - val eq : t -> t -> bool - val hcons : t -> t -end - -module HashedList (M : Hashconsed) : -sig - type t = private Nil | Cons of M.t * int * t - val nil : t - val cons : M.t -> t -> t -end = -struct - type t = Nil | Cons of M.t * int * t - module Self = - struct - type _t = t - type t = _t - type u = (M.t -> M.t) - let hash = function Nil -> 0 | Cons (_, h, _) -> h - let eq l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 - | _ -> false - let hashcons hc = function - | Nil -> Nil - | Cons (x, h, l) -> Cons (hc x, h, l) - end - module Hcons = Hashcons.Make(Self) - let hcons = Hashcons.simple_hcons Hcons.generate Hcons.hcons M.hcons - (** No recursive call: the interface guarantees that all HLists from this - program are already hashconsed. If we get some external HList, we can - still reconstruct it by traversing it entirely. *) - let nil = Nil - let cons x l = - let h = M.hash x in - let hl = match l with Nil -> 0 | Cons (_, h, _) -> h in - let h = Hashset.Combine.combine h hl in - hcons (Cons (x, h, l)) -end - -module HList = struct - - module type S = sig - type elt - type t = private Nil | Cons of elt * int * t - val hash : t -> int - val nil : t - val cons : elt -> t -> t - val tip : elt -> t - val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a - val map : (elt -> elt) -> t -> t - val smartmap : (elt -> elt) -> t -> t - val exists : (elt -> bool) -> t -> bool - val for_all : (elt -> bool) -> t -> bool - val for_all2 : (elt -> elt -> bool) -> t -> t -> bool - val remove : elt -> t -> t - val to_list : t -> elt list - end - - module Make (H : Hashconsed) : S with type elt = H.t = - struct - type elt = H.t - include HashedList(H) - - let hash = function Nil -> 0 | Cons (_, h, _) -> h - - let tip e = cons e nil - - let rec fold f l accu = match l with - | Nil -> accu - | Cons (x, _, l) -> fold f l (f x accu) - - let rec map f = function - | Nil -> nil - | Cons (x, _, l) -> cons (f x) (map f l) - - let smartmap = map - (** Apriori hashconsing ensures that the map is equal to its argument *) - - let rec exists f = function - | Nil -> false - | Cons (x, _, l) -> f x || exists f l - - let rec for_all f = function - | Nil -> true - | Cons (x, _, l) -> f x && for_all f l - - let rec for_all2 f l1 l2 = match l1, l2 with - | Nil, Nil -> true - | Cons (x1, _, l1), Cons (x2, _, l2) -> f x1 x2 && for_all2 f l1 l2 - | _ -> false - - let rec to_list = function - | Nil -> [] - | Cons (x, _, l) -> x :: to_list l - - let rec remove x = function - | Nil -> nil - | Cons (y, _, l) -> - if H.eq x y then l - else cons y (remove x l) - - end -end - module RawLevel = struct open Names @@ -174,24 +68,6 @@ struct | _, Level _ -> 1 | Var n, Var m -> Int.compare n m - let hequal x y = - x == y || - match x, y with - | Prop, Prop -> true - | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' - | Var n, Var n' -> n == n' - | _ -> false - - let hcons = function - | Prop as x -> x - | Set as x -> x - | Level (n,d) as x -> - let d' = Names.DirPath.hcons d in - if d' == d then x else Level (n,d') - | Var n as x -> x - open Hashset.Combine let hash = function @@ -223,24 +99,7 @@ module Level = struct let data x = x.data - (** Hashcons on levels + their hash *) - - module Self = struct - type _t = t - type t = _t - type u = unit - let eq x y = x.hash == y.hash && RawLevel.hequal x.data y.data - let hash x = x.hash - let hashcons () x = - let data' = RawLevel.hcons x.data in - if x.data == data' then x else { x with data = data' } - end - - let hcons = - let module H = Hashcons.Make(Self) in - Hashcons.simple_hcons H.generate H.hcons () - - let make l = hcons { hash = RawLevel.hash l; data = l } + let make l = { hash = RawLevel.hash l; data = l } let set = make Set let prop = make Prop @@ -277,7 +136,7 @@ module Level = struct let pr u = str (to_string u) - let make m n = make (Level (n, Names.DirPath.hcons m)) + let make m n = make (Level (n, m)) end @@ -310,48 +169,12 @@ struct module Expr = struct type t = Level.t * int - type _t = t - (* Hashing of expressions *) - module ExprHash = - struct - type t = _t - type u = Level.t -> Level.t - let hashcons hdir (b,n as x) = - let b' = hdir b in - if b' == b then x else (b',n) - let eq l1 l2 = - l1 == l2 || - match l1,l2 with - | (b,n), (b',n') -> b == b' && n == n' - - let hash (x, n) = n + Level.hash x - - end - - module HExpr = - struct - - module H = Hashcons.Make(ExprHash) - - type t = ExprHash.t - - let hcons = - Hashcons.simple_hcons H.generate H.hcons Level.hcons - let hash = ExprHash.hash - let eq x y = x == y || - (let (u,n) = x and (v,n') = y in - Int.equal n n' && Level.equal u v) - - end + let make l = (l, 0) - let hcons = HExpr.hcons - - let make l = hcons (l, 0) - - let prop = make Level.prop - let set = make Level.set - let type1 = hcons (Level.set, 1) + let prop = (Level.prop, 0) + let set = (Level.set, 0) + let type1 = (Level.set, 1) let is_prop = function | (l,0) -> Level.is_prop l @@ -361,22 +184,15 @@ struct (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) - let leq (u,n) (v,n') = - let cmp = Level.compare u v in - if Int.equal cmp 0 then n <= n' - else if n <= n' then - (Level.is_prop u && Level.is_small v) - else false - let successor (u,n) = if Level.is_prop u then type1 - else hcons (u, n + 1) + else (u, n + 1) let addn k (u,n as x) = if k = 0 then x else if Level.is_prop u then - hcons (Level.set,n+k) - else hcons (u,n+k) + (Level.set,n+k) + else (u,n+k) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in @@ -401,31 +217,29 @@ struct let v' = f v in if v' == v then x else if Level.is_prop v' && n != 0 then - hcons (Level.set, n) - else hcons (v', n) + (Level.set, n) + else (v', n) end - - module Huniv = HList.Make(Expr.HExpr) - type t = Huniv.t - open Huniv - - let equal x y = x == y || - (Huniv.hash x == Huniv.hash y && - Huniv.for_all2 Expr.equal x y) - let make l = Huniv.tip (Expr.make l) - let tip x = Huniv.tip x - + type t = Expr.t list + + let tip u = [u] + let cons u v = u :: v + + let equal x y = x == y || List.equal Expr.equal x y + + let make l = tip (Expr.make l) + let pr l = match l with - | Cons (u, _, Nil) -> Expr.pr u + | [u] -> Expr.pr u | _ -> str "max(" ++ hov 0 - (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ + (prlist_with_sep pr_comma Expr.pr l) ++ str ")" let level l = match l with - | Cons (l, _, Nil) -> Expr.level l + | [l] -> Expr.level l | _ -> None (* The lower predicative level of the hierarchy that contains (impredicative) @@ -445,16 +259,16 @@ struct (* Returns the formal universe that lies juste above the universe variable u. Used to type the sort u. *) let super l = - Huniv.map (fun x -> Expr.successor x) l + List.map (fun x -> Expr.successor x) l let addn n l = - Huniv.map (fun x -> Expr.addn n x) l + List.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with - | Nil, _ -> l2 - | _, Nil -> l1 - | Cons (h1, _, t1), Cons (h2, _, t2) -> + | [], _ -> l2 + | _, [] -> l1 + | h1 :: t1, h2 :: t2 -> (match Expr.super h1 h2 with | Inl true (* h1 < h2 *) -> merge_univs t1 l2 | Inl false -> merge_univs l1 t2 @@ -466,28 +280,28 @@ struct let sort u = let rec aux a l = match l with - | Cons (b, _, l') -> + | b :: l' -> (match Expr.super a b with | Inl false -> aux a l' | Inl true -> l | Inr c -> if c <= 0 then cons a l else cons b (aux a l')) - | Nil -> cons a l + | [] -> cons a l in - fold (fun a acc -> aux a acc) u nil + List.fold_right (fun a acc -> aux a acc) u [] (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y - let empty = nil + let empty = [] - let exists = Huniv.exists + let exists = List.exists - let for_all = Huniv.for_all + let for_all = List.for_all - let smartmap = Huniv.smartmap + let smartmap = List.smartmap end @@ -552,7 +366,7 @@ let repr g u = let a = try UMap.find u g with Not_found -> anomaly ~label:"Univ.repr" - (str"Universe " ++ Level.pr u ++ str" undefined") + (str"Universe " ++ Level.pr u ++ str" undefined.") in match a with | Equiv v -> repr_rec v @@ -775,9 +589,9 @@ let check_equal_expr g x y = let check_eq_univs g l1 l2 = let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in - Huniv.for_all (fun x1 -> exists x1 l2) l1 - && Huniv.for_all (fun x2 -> exists x2 l1) l2 + let exists x1 l = List.exists (fun x2 -> f x1 x2) l in + List.for_all (fun x1 -> exists x1 l2) l1 + && List.for_all (fun x2 -> exists x2 l1) l2 let check_eq g u v = Universe.equal u v || check_eq_univs g u v @@ -791,11 +605,11 @@ let check_smaller_expr g (u,n) (v,m) = | _ -> false let exists_bigger g ul l = - Huniv.exists (fun ul' -> + Universe.exists (fun ul' -> check_smaller_expr g ul ul') l let real_check_leq g u v = - Huniv.for_all (fun ul -> exists_bigger g ul v) u + Universe.for_all (fun ul -> exists_bigger g ul v) u let check_leq g u v = Universe.equal u v || @@ -855,7 +669,7 @@ let merge g arcu arcv = else (max_rank, old_max_rank, best_arc, arc::rest) in match between g arcu arcv with - | [] -> anomaly (str "Univ.between") + | [] -> anomaly (str "Univ.between.") | arc::rest -> let (max_rank, old_max_rank, best_arc, rest) = List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in @@ -918,7 +732,7 @@ let enforce_univ_eq u v g = | FastLT -> error_inconsistency Eq u v | FastLE -> merge g arcv arcu | FastNLE -> merge_disc g arcu arcv - | FastEQ -> anomaly (Pp.str "Univ.compare")) + | FastEQ -> anomaly (Pp.str "Univ.compare.")) (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) @@ -931,7 +745,7 @@ let enforce_univ_leq u v g = | FastLT -> error_inconsistency Le u v | FastLE -> merge g arcv arcu | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") + | FastEQ -> anomaly (Pp.str "Univ.compare.") (* enforce_univ_lt u v will force u match fast_compare_neq false g arcv arcu with FastNLE -> fst (setlt g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") + | FastEQ -> anomaly (Pp.str "Univ.compare.") | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) @@ -975,7 +789,23 @@ struct else Level.compare v v' end -module Constraint = Set.Make(UConstraintOrd) +let pr_constraint_type op = + let op_str = match op with + | Lt -> " < " + | Le -> " <= " + | Eq -> " = " + in str op_str + +module Constraint = +struct + module S = Set.Make(UConstraintOrd) + include S + + let pr prl c = + fold (fun (u1,op,u2) pp_std -> + pp_std ++ prl u1 ++ pr_constraint_type op ++ + prl u2 ++ fnl () ) c (str "") +end let empty_constraint = Constraint.empty let merge_constraints c g = @@ -990,41 +820,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -let constraint_add_leq v u c = - (* We just discard trivial constraints like u<=u *) - if Expr.equal v u then c - else - match v, u with - | (x,n), (y,m) -> - let j = m - n in - if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then - Constraint.add (x,Lt,y) c - else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then - if Level.equal x y then (* u+(k+1) <= u *) - raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u)) - else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints") - else if j = 0 then - Constraint.add (x,Le,y) c - else (* j >= 1 *) (* m = n + k, u <= v+k *) - if Level.equal x y then c (* u <= u+k, trivial *) - else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *) - else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints") - -let check_univ_leq_one u v = Universe.exists (Expr.leq u) v - -let check_univ_leq u v = - Universe.for_all (fun u -> check_univ_leq_one u v) u - -let enforce_leq u v c = - match v with - | Universe.Huniv.Cons (v, _, Universe.Huniv.Nil) -> - Universe.Huniv.fold (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable") - -let enforce_leq u v c = - if check_univ_leq u v then c - else enforce_leq u v c - let check_constraint g (l,d,r) = match d with | Eq -> check_equal g l r @@ -1046,14 +841,6 @@ type universe_level_subst = universe_level universe_map (** A full substitution might involve algebraic universes *) type universe_subst = universe universe_map -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - module Instance : sig type t = Level.t array @@ -1062,68 +849,27 @@ module Instance : sig val equal : t -> t -> bool val subst_fn : universe_level_subst_fn -> t -> t val subst : universe_level_subst -> t -> t - val pr : t -> Pp.std_ppcmds - val check_eq : t check_function + val pr : t -> Pp.t + val check_eq : t check_function + val length : t -> int + val append : t -> t -> t + val of_array : Level.t array -> t end = struct type t = Level.t array - let empty : t = [||] - - module HInstancestruct = - struct - type _t = t - type t = _t - type u = Level.t -> Level.t - - let hashcons huniv a = - let len = Array.length a in - if Int.equal len 0 then empty - else begin - for i = 0 to len - 1 do - let x = Array.unsafe_get a i in - let x' = huniv x in - if x == x' then () - else Array.unsafe_set a i x' - done; - a - end - - let eq t1 t2 = - t1 == t2 || - (Int.equal (Array.length t1) (Array.length t2) && - let rec aux i = - (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1)) - in aux 0) - - let hash a = - let accu = ref 0 in - for i = 0 to Array.length a - 1 do - let l = Array.unsafe_get a i in - let h = Level.hash l in - accu := Hashset.Combine.combine !accu h; - done; - (* [h] must be positive. *) - let h = !accu land 0x3FFFFFFF in - h - end - - module HInstance = Hashcons.Make(HInstancestruct) - - let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons - - let empty = hcons [||] + let empty = [||] let is_empty x = Int.equal (Array.length x) 0 let subst_fn fn t = let t' = CArray.smartmap fn t in - if t' == t then t else hcons t' + if t' == t then t else t' let subst s t = let t' = CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t - in if t' == t then t else hcons t' + in if t' == t then t else t' let pr = prvect_with_sep spc Level.pr @@ -1142,8 +888,41 @@ struct (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1)) in aux 0) + let length = Array.length + + let append = Array.append + + let of_array i = i + end +(** Substitute instance inst for ctx in csts *) + +let subst_instance_level s l = + match l.Level.data with + | Level.Var n -> s.(n) + | _ -> l + +let subst_instance_instance s i = + Array.smartmap (fun l -> subst_instance_level s l) i + +let subst_instance_universe s u = + let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in + let u' = Universe.smartmap f u in + if u == u' then u + else Universe.sort u' + +let subst_instance_constraint s (u,d,v as c) = + let u' = subst_instance_level s u in + let v' = subst_instance_level s v in + if u' == u && v' == v then c + else (u',d,v') + +let subst_instance_constraints s csts = + Constraint.fold + (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) + csts Constraint.empty + type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t @@ -1159,10 +938,80 @@ struct let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst + let size (univs, _) = Instance.length univs + + let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst + let pr prl (univs, cst as ctx) = + if is_empty ctx then mt() else + h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) end type universe_context = UContext.t +module AUContext = +struct + include UContext + + let repr (inst, cst) = + (Array.mapi (fun i l -> Level.var i) inst, cst) + + let instantiate inst (u, cst) = + assert (Array.length u = Array.length inst); + subst_instance_constraints inst cst + +end + +type abstract_universe_context = AUContext.t + +module Variance = +struct + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + + let check_subtype x y = match x, y with + | (Irrelevant | Covariant | Invariant), Irrelevant -> true + | Irrelevant, Covariant -> false + | (Covariant | Invariant), Covariant -> true + | (Irrelevant | Covariant), Invariant -> false + | Invariant, Invariant -> true + + let leq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant -> Constraint.add (u, Le, u') csts + | Invariant -> Constraint.add (u, Eq, u') csts + + let eq_constraint csts variance u u' = + match variance with + | Irrelevant -> csts + | Covariant | Invariant -> Constraint.add (u, Eq, u') csts + + let leq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 leq_constraint csts variance u u' + + let eq_constraints variance u u' csts = + let len = Array.length u in + assert (len = Array.length u' && len = Array.length variance); + Array.fold_left3 eq_constraint csts variance u u' +end + +module CumulativityInfo = +struct + type t = universe_context * Variance.t array + + let univ_context (univcst, subtypcst) = univcst + let variance (univs, variance) = variance + +end + +module ACumulativityInfo = CumulativityInfo +type abstract_cumulativity_info = ACumulativityInfo.t + module ContextSet = struct type t = LSet.t constrained @@ -1173,6 +1022,18 @@ struct end type universe_context_set = ContextSet.t +(** Instance subtyping *) + +let check_subtype univs ctxT ctx = + if AUContext.size ctx == AUContext.size ctx then + let (inst, cst) = AUContext.repr ctx in + let cstT = UContext.constraints (AUContext.repr ctxT) in + let push accu v = add_universe v false accu in + let univs = Array.fold_left push univs inst in + let univs = merge_constraints cstT univs in + check_constraints cst univs + else false + (** Substitutions. *) let is_empty_subst = LMap.is_empty @@ -1192,43 +1053,9 @@ let subst_univs_level_universe subst u = if u == u' then u else Universe.sort u' -(** Substitute instance inst for ctx in csts *) - -let subst_instance_level s l = - match l.Level.data with - | Level.Var n -> s.(n) - | _ -> l - -let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i - -let subst_instance_universe s u = - let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in - if u == u' then u - else Universe.sort u' - -let subst_instance_constraint s (u,d,v as c) = - let u' = subst_instance_level s u in - let v' = subst_instance_level s v in - if u' == u && v' == v then c - else (u',d,v') - -let subst_instance_constraints s csts = - Constraint.fold - (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) - csts Constraint.empty - let make_abstract_instance (ctx, _) = Array.mapi (fun i l -> Level.var i) ctx -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -let instantiate_univ_constraints u (_, csts) = - subst_instance_constraints u csts - (** With level to universe substitutions. *) type universe_subst_fn = universe_level -> universe @@ -1239,7 +1066,7 @@ let subst_univs_expr_opt fn (l,n) = let subst_univs_universe fn ul = let subst, nosubst = - Universe.Huniv.fold (fun u (subst,nosubst) -> + List.fold_right (fun u (subst,nosubst) -> try let a' = subst_univs_expr_opt fn u in (a' :: subst, nosubst) with Not_found -> (subst, u :: nosubst)) @@ -1250,7 +1077,7 @@ let subst_univs_universe fn ul = let substs = List.fold_left Universe.merge_univs Universe.empty subst in - List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) + List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u)) substs nosubst let merge_context strict ctx g = @@ -1269,6 +1096,10 @@ let merge_context_set strict ctx g = (** Pretty-printing *) +let pr_constraints prl = Constraint.pr prl + +let pr_universe_context = UContext.pr + let pr_arc = function | _, Canonical {univ=u; lt=[]; le=[]} -> mt () diff --git a/checker/univ.mli b/checker/univ.mli index 7d4c629a..473159c0 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t + + val pr : t -> Pp.t + (** Pretty-printing *) + val equal : t -> t -> bool end @@ -48,7 +55,7 @@ type universe = Universe.t (** Alias name. *) -val pr_uni : universe -> Pp.std_ppcmds +val pr_uni : universe -> Pp.t (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) @@ -71,11 +78,13 @@ type 'a check_function = universes -> 'a -> 'a -> bool val check_leq : universe check_function val check_eq : universe check_function + + (** The initial graph of universes: Prop < Set *) val initial_universes : universes (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared @@ -99,8 +108,6 @@ type 'a constrained = 'a * constraints type 'a constraint_function = 'a -> 'a -> constraints -> constraints -val enforce_leq : universe constraint_function - (** {6 ... } *) (** Merge of constraints in a universes graph. The function [merge_constraints] merges a set of constraints in a given @@ -143,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : @@ -157,7 +162,6 @@ sig val is_empty : t -> bool val equal : t -> t -> bool - (** Equality (note: instances are hash-consed, this is O(1)) *) val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) @@ -165,11 +169,19 @@ sig val subst : universe_level_subst -> t -> t (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing, no comments *) val check_eq : t check_function (** Check equality of instances w.r.t. a universe graph *) + + val length : t -> int + (** Compute the length of the instance *) + + val of_array : Level.t array -> t + + val append : t -> t -> t + (** Append two universe instances *) end type universe_instance = Instance.t @@ -187,9 +199,49 @@ sig val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints + val is_empty : t -> bool + +end + +type universe_context = UContext.t + +module AUContext : +sig + type t + + val size : t -> int + + val instantiate : Instance.t -> t -> Constraint.t + val repr : t -> UContext.t end +type abstract_universe_context = AUContext.t + +module Variance : +sig + (** A universe position in the instance given to a cumulative + inductive can be the following. Note there is no Contravariant + case because [forall x : A, B <= forall x : A', B'] requires [A = + A'] as opposed to [A' <= A]. *) + type t = Irrelevant | Covariant | Invariant + val check_subtype : t -> t -> bool + val leq_constraints : t array -> Instance.t constraint_function + val eq_constraints : t array -> Instance.t constraint_function +end + + +module ACumulativityInfo : +sig + type t + + val univ_context : t -> abstract_universe_context + val variance : t -> Variance.t array + +end + +type abstract_cumulativity_info = ACumulativityInfo.t + module ContextSet : sig type t @@ -198,7 +250,6 @@ module ContextSet : val constraints : t -> constraints end -type universe_context = UContext.t type universe_context_set = ContextSet.t val merge_context : bool -> universe_context -> universes -> universes @@ -221,18 +272,20 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_constraints : universe_instance -> constraints -> constraints (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_context -> universe_context -val instantiate_univ_constraints : universe_instance -> universe_context -> constraints - (** Build the relative instance corresponding to the context *) -val make_abstract_instance : universe_context -> universe_instance - +val make_abstract_instance : abstract_universe_context -> universe_instance + +(** Check instance subtyping *) +val check_subtype : universes -> AUContext.t -> AUContext.t -> bool + (** {6 Pretty-printing of universes. } *) -val pr_universes : universes -> Pp.std_ppcmds +val pr_constraint_type : constraint_type -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t + +val pr_universes : universes -> Pp.t diff --git a/checker/validate.ml b/checker/validate.ml index c434ef09..f831875d 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Obj.t -> unit - (* Check that object o is a block with tag t *) let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () diff --git a/checker/validate.mli b/checker/validate.mli new file mode 100644 index 00000000..6c2ab8d3 --- /dev/null +++ b/checker/validate.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Values.value -> 'a -> unit diff --git a/checker/values.ml b/checker/values.ml index c175aed6..1ac8d7ce 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Any diff --git a/checker/values.mli b/checker/values.mli new file mode 100644 index 00000000..20b9d54a --- /dev/null +++ b/checker/values.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* if v < 0 || v >= max then let () = Printf.printf "Out-of-range input! (only %d children)\n%!" max in read_num max else Some v - with Failure "int_of_string" -> + | exception Failure _ -> Printf.printf "Unrecognized input! enters the -th child, u goes up 1 level, x exits\n%!"; read_num max @@ -75,48 +79,51 @@ struct type obj = data - let memory = ref [||] - let sizes = ref [||] + let memory = ref LargeArray.empty + let sizes = ref LargeArray.empty (** size, in words *) let ws = Sys.word_size / 8 - let rec init_size seen = function - | Int _ | Atm _ | Fun _ -> 0 + let rec init_size seen k = function + | Int _ | Atm _ | Fun _ -> k 0 | Ptr p -> - if seen.(p) then 0 + if LargeArray.get seen p then k 0 else - let () = seen.(p) <- true in - match (!memory).(p) with + let () = LargeArray.set seen p true in + match LargeArray.get !memory p with | Struct (tag, os) -> - let fold accu o = accu + 1 + init_size seen o in - let size = Array.fold_left fold 1 os in - let () = (!sizes).(p) <- size in - size + let len = Array.length os in + let rec fold i accu k = + if i == len then k accu + else + init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i) + in + fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size) | String s -> let size = 2 + (String.length s / ws) in - let () = (!sizes).(p) <- size in - size + let () = LargeArray.set !sizes p size in + k size let size = function | Int _ | Atm _ | Fun _ -> 0 - | Ptr p -> (!sizes).(p) + | Ptr p -> LargeArray.get !sizes p let repr = function | Int i -> INT i | Atm t -> BLOCK (t, [||]) | Fun _ -> OTHER | Ptr p -> - match (!memory).(p) with + match LargeArray.get !memory p with | Struct (tag, os) -> BLOCK (tag, os) | String s -> STRING s let input ch = let obj, mem = parse_channel ch in let () = memory := mem in - let () = sizes := Array.make (Array.length mem) (-1) in - let seen = Array.make (Array.length mem) false in - let _ = init_size seen obj in + let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in + let seen = LargeArray.make (LargeArray.length mem) false in + let () = init_size seen ignore obj in obj let oid = function @@ -149,22 +156,25 @@ let rec get_name ?(extra=false) = function (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) +exception TupleString of string let get_string_in_tuple o = try for i = 0 to Array.length o - 1 do match Repr.repr o.(i) with | STRING s -> - failwith (Printf.sprintf " [..%s..]" s) + let len = min max_string_length (String.length s) in + raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len))) | _ -> () done; "" - with Failure s -> s + with TupleString s -> s (** Some details : tags, integer value for non-block, etc etc *) let rec get_details v o = match v, Repr.repr o with | (String | Any), STRING s -> - Printf.sprintf " [%s]" (String.escaped s) + let len = min max_string_length (String.length s) in + Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len)) |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o |(Sum _|Any), BLOCK (tag, _) -> Printf.sprintf " [tag=%i]" tag @@ -191,20 +201,20 @@ let access_children vs os pos = else raise Exit let access_list v o pos = - let rec loop o pos = match Repr.repr o with - | INT 0 -> [] + let rec loop o pos accu = match Repr.repr o with + | INT 0 -> List.rev accu | BLOCK (0, [|hd; tl|]) -> - (v, hd, 0 :: pos) :: loop tl (1 :: pos) + loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu) | _ -> raise Exit in - Array.of_list (loop o pos) + Array.of_list (loop o pos []) let access_block o = match Repr.repr o with | BLOCK (tag, os) -> (tag, os) | _ -> raise Exit -let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit (** raises Exit if the object has not the expected structure *) +exception Forbidden let rec get_children v o pos = match v with |Tuple (_, v) -> let (_, os) = access_block o in @@ -225,18 +235,26 @@ let rec get_children v o pos = match v with | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] | _ -> raise Exit end - |String | Int -> [||] + | String -> + begin match Repr.repr o with + | STRING _ -> [||] + | _ -> raise Exit + end + | Int -> + begin match Repr.repr o with + | INT _ -> [||] + | _ -> raise Exit + end |Annot (s,v) -> get_children v o pos |Any -> raise Exit |Dyn -> begin match Repr.repr o with | BLOCK (0, [|id; o|]) -> - let n = access_int id in - let tpe = find_dyn n in + let tpe = Any in [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] | _ -> raise Exit end - |Fail s -> failwith "forbidden" + |Fail s -> raise Forbidden let get_children v o pos = try get_children v o pos @@ -257,9 +275,10 @@ let init () = stk := [] let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk +exception EmptyStack let pop () = match !stk with | i::s -> stk := s; i - | _ -> failwith "empty stack" + | _ -> raise EmptyStack let rec visit v o pos = Printf.printf "\nDepth %d Pos %s Context %s\n" @@ -283,8 +302,8 @@ let rec visit v o pos = push (get_name v) v o pos; visit v' o' pos' with - | Failure "empty stack" -> () - | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos + | EmptyStack -> () + | Forbidden -> let info = pop () in visit info.typ info.obj info.pos | Failure _ | Invalid_argument _ -> visit v o pos end @@ -313,8 +332,7 @@ let dummy_header = { } let parse_header chan = - let magic = String.create 4 in - let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let magic = really_input_string chan 4 in let length = input_binary_int chan in let objects = input_binary_int chan in let size32 = input_binary_int chan in @@ -377,7 +395,7 @@ let visit_vo f = | None -> () done -let main = +let () = if not !Sys.interactive then Arg.parse [] visit_vo ("votour: guided tour of a Coq .vo or .vi file\n"^ diff --git a/checker/votour.mli b/checker/votour.mli new file mode 100644 index 00000000..9db9ecd1 --- /dev/null +++ b/checker/votour.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(*