diff options
Diffstat (limited to 'checker')
42 files changed, 1348 insertions, 738 deletions
diff --git a/checker/Makefile b/checker/Makefile deleted file mode 100644 index 2bcc9d3656..0000000000 --- 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 new file mode 100644 index 0000000000..c48b830119 --- /dev/null +++ b/checker/analyze.ml @@ -0,0 +1,350 @@ +(** Headers *) + +let prefix_small_block = 0x80 +let prefix_small_int = 0x40 +let prefix_small_string = 0x20 + +let code_int8 = 0x00 +let code_int16 = 0x01 +let code_int32 = 0x02 +let code_int64 = 0x03 +let code_shared8 = 0x04 +let code_shared16 = 0x05 +let code_shared32 = 0x06 +let code_double_array32_little = 0x07 +let code_block32 = 0x08 +let code_string8 = 0x09 +let code_string32 = 0x0A +let code_double_big = 0x0B +let code_double_little = 0x0C +let code_double_array8_big = 0x0D +let code_double_array8_little = 0x0E +let code_double_array32_big = 0x0F +let code_codepointer = 0x10 +let code_infixpointer = 0x11 +let code_custom = 0x12 +let code_block64 = 0x13 + +type code_descr = +| CODE_INT8 +| CODE_INT16 +| CODE_INT32 +| CODE_INT64 +| CODE_SHARED8 +| CODE_SHARED16 +| CODE_SHARED32 +| CODE_DOUBLE_ARRAY32_LITTLE +| CODE_BLOCK32 +| CODE_STRING8 +| CODE_STRING32 +| CODE_DOUBLE_BIG +| CODE_DOUBLE_LITTLE +| CODE_DOUBLE_ARRAY8_BIG +| CODE_DOUBLE_ARRAY8_LITTLE +| CODE_DOUBLE_ARRAY32_BIG +| CODE_CODEPOINTER +| CODE_INFIXPOINTER +| CODE_CUSTOM +| CODE_BLOCK64 + +let code_max = 0x13 + +let magic_number = "\132\149\166\190" + +(** Memory reification *) + +type repr = +| RInt of int +| RBlock of (int * int) (* tag × len *) +| RString of string +| RPointer of int +| RCode of int + +type data = +| Int of int (* value *) +| Ptr of int (* pointer *) +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +module type Input = +sig + type t + val input_byte : t -> int + val input_binary_int : t -> int +end + +module type S = +sig + type input + val parse : input -> (data * obj array) +end + +module Make(M : Input) = +struct + +open M + +type input = M.t + +let current_offset = ref 0 + +let input_byte chan = + let () = incr current_offset in + input_byte chan + +let input_binary_int chan = + let () = current_offset := !current_offset + 4 in + input_binary_int chan + +let input_char chan = Char.chr (input_byte 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 length = input_binary_int chan in + let objects = input_binary_int chan in + let size32 = input_binary_int chan in + let size64 = input_binary_int chan in + (magic, length, size32, size64, objects) + +let input_int8s chan = + let i = input_byte chan in + if i land 0x80 = 0 + then i + else i lor ((-1) lsl 8) + +let input_int8u = input_byte + +let input_int16s chan = + let i = input_byte chan in + let j = input_byte chan in + let ans = (i lsl 8) lor j in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 16) + +let input_int16u chan = + let i = input_byte chan in + let j = input_byte chan in + (i lsl 8) lor j + +let input_int32s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +let input_int32u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l + +let input_int64s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let ans = + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 63) + +let input_int64u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + +let input_header32 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let tag = l in + let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in + (tag, len) + +let input_header64 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let tag = p in + let len = + (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor + (m lsl 14) lor (n lsl 6) lor (o lsr 2) + 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 + let tag = data land 0x0F in + let len = (data lsr 4) land 0x07 in + RBlock (tag, len) + else if prefix_small_int <= data then + RInt (data land 0x3F) + else if prefix_small_string <= data then + let len = data land 0x1F in + RString (input_string len chan) + else if data > code_max then + assert false + else match (Obj.magic data) with + | CODE_INT8 -> + RInt (input_int8s chan) + | CODE_INT16 -> + RInt (input_int16s chan) + | CODE_INT32 -> + RInt (input_int32s chan) + | CODE_INT64 -> + RInt (input_int64s chan) + | CODE_SHARED8 -> + RPointer (input_int8u chan) + | CODE_SHARED16 -> + RPointer (input_int16u chan) + | CODE_SHARED32 -> + RPointer (input_int32u chan) + | CODE_BLOCK32 -> + RBlock (input_header32 chan) + | CODE_BLOCK64 -> + RBlock (input_header64 chan) + | CODE_STRING8 -> + let len = input_int8u chan in + RString (input_string len chan) + | CODE_STRING32 -> + let len = input_int32u chan in + RString (input_string len chan) + | CODE_CODEPOINTER -> + let addr = input_int32u chan in + for i = 0 to 15 do ignore (input_byte chan); done; + RCode addr + | CODE_DOUBLE_ARRAY32_LITTLE + | CODE_DOUBLE_BIG + | CODE_DOUBLE_LITTLE + | CODE_DOUBLE_ARRAY8_BIG + | CODE_DOUBLE_ARRAY8_LITTLE + | CODE_DOUBLE_ARRAY32_BIG + | CODE_INFIXPOINTER + | CODE_CUSTOM -> + Printf.eprintf "Unhandled code %04x\n%!" data; assert false + +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 current_object = ref 0 in + let fill_obj = function + | RPointer n -> + let data = Ptr (!current_object - n) in + data, None + | RInt n -> + let data = Int n in + data, None + | RString s -> + let data = Ptr !current_object in + let () = memory.(!current_object) <- String s in + let () = incr current_object in + data, None + | RBlock (tag, 0) -> + (* Atoms are never shared *) + let data = Atm tag in + data, None + | 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 () = incr current_object in + data, Some nblock + | RCode addr -> + let data = Fun addr in + data, None + in + + let rec fill block off accu = + if Array.length block = off then + match accu with + | [] -> () + | (block, off) :: accu -> fill block off accu + else + let data, nobj = fill_obj (parse_object chan) in + let () = block.(off) <- data in + let block, off, accu = match nobj with + | None -> block, succ off, accu + | Some nblock -> nblock, 0, ((block, succ off) :: accu) + in + fill block off accu + in + let ans = [|Atm (-1)|] in + let () = fill ans 0 [] in + (ans.(0), memory) + +end + +module IChannel = +struct + type t = in_channel + let input_byte = Pervasives.input_byte + let input_binary_int = Pervasives.input_binary_int +end + +module IString = +struct + type t = (string * int ref) + + let input_byte (s, off) = + let ans = Char.code (s.[!off]) in + let () = incr off in + ans + + let input_binary_int chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +end + +module PChannel = Make(IChannel) +module PString = Make(IString) + +let parse_channel = PChannel.parse +let parse_string s = PString.parse (s, ref 0) diff --git a/checker/analyze.mli b/checker/analyze.mli new file mode 100644 index 0000000000..42efcf01df --- /dev/null +++ b/checker/analyze.mli @@ -0,0 +1,35 @@ +type data = +| Int of int +| Ptr of int +| Atm of int (* tag *) +| Fun of int (* address *) + +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) + +(** {6 Functorized version} *) + +module type Input = +sig + type t + val input_byte : t -> int + (** Input a single byte *) + val input_binary_int : t -> int + (** Input a big-endian 31-bits signed integer *) +end +(** Type of inputs *) + +module type S = +sig + type input + val parse : input -> (data * obj array) + (** 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. *) diff --git a/checker/check.ml b/checker/check.ml index 9a750858d7..11678fa6bb 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,16 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Names +let chk_pp = Pp.pp_with Format.std_formatter + let pr_dirpath dp = str (DirPath.to_string dp) let default_root_prefix = DirPath.empty let split_dirpath d = @@ -46,7 +48,7 @@ type library_t = { library_opaques : Cic.opaque_table; library_deps : Cic.library_deps; library_digest : Cic.vodigest; - library_extra_univs : Univ.constraints } + library_extra_univs : Univ.ContextSet.t } module LibraryOrdered = struct @@ -97,7 +99,7 @@ let access_opaque_univ_table dp i = let t = LibraryMap.find dp !opaque_univ_tables in assert (i < Array.length t); Future.force t.(i) - with Not_found -> Univ.empty_constraint + with Not_found -> Univ.ContextSet.empty let _ = Declarations.indirect_opaque_access := access_opaque_table @@ -111,15 +113,13 @@ let check_one_lib admit (dir,m) = also check if it carries a validation certificate (yet to be implemented). *) if LibrarySet.mem dir admit then - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Admitting library: " ++ pr_dirpath dir); Safe_typing.unsafe_import file md m.library_extra_univs dig) else - (Flags.if_verbose ppnl + (Flags.if_verbose Feedback.msg_notice (str "Checking library: " ++ pr_dirpath dir); Safe_typing.import file md m.library_extra_univs dig); - Flags.if_verbose pp (fnl()); - pp_flush (); register_loaded_library m (*************************************************************************) @@ -173,7 +173,7 @@ let remove_load_path dir = let add_load_path (phys_path,coq_path) = if !Flags.debug then - ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = canonical_path_name phys_path in let physical, logical = !load_paths in @@ -188,7 +188,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - msg_warning + Feedback.msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); @@ -248,12 +248,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 = @@ -271,32 +271,22 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) - -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) +(*s Low-level interning of libraries from files *) -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) open Cic -let mk_library md f table digest cst = { - library_name = md.md_name; +let mk_library sd md f table digest cst = { + library_name = sd.md_name; library_filename = f; library_compiled = md.md_compiled; library_opaques = table; - library_deps = md.md_deps; + library_deps = sd.md_deps; library_digest = digest; library_extra_univs = cst } @@ -309,10 +299,11 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); - let (md,table,opaque_csts,digest) = + Flags.if_verbose chk_pp (str"[intern "++str f++str" ..."); + let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in + 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 @@ -321,44 +312,44 @@ let intern_from_file (dir, f) = System.marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in - let ch = open_in f 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 <> md.md_name then - errorlabstrm "intern_from_file" - (name_clash_message dir md.md_name f); + if dir <> sd.md_name then + 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 - pp (str " (was a vio file) "); + 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; end; (* Verification of the unmarshalled values *) + Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; - Flags.if_verbose ppnl (str" done]"); pp_flush (); + Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in - md,table,opaque_csts,digest - with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in - depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; - opaque_tables := LibraryMap.add md.md_name table !opaque_tables; + sd,md,table,opaque_csts,digest + with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in + depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; + opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> opaque_univ_tables := - LibraryMap.add md.md_name opaque_csts !opaque_univ_tables) + LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) opaque_csts; let extra_cst = - Option.default Univ.empty_constraint - (Option.map (fun (_,cs,_) -> - Univ.ContextSet.constraints cs) opaque_csts) in - mk_library md f table digest extra_cst + Option.default Univ.ContextSet.empty + (Option.map (fun (_,cs,_) -> cs) opaque_csts) in + mk_library sd md f table digest extra_cst let get_deps (dir, f) = try LibraryMap.find dir !depgraph @@ -416,11 +407,11 @@ let recheck_library ~norec ~admit ~check = let nochk = List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in (* *) - Flags.if_verbose ppnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ + Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); List.iter (check_one_lib nochk) needed; - Flags.if_verbose ppnl (str"Modules were successfully checked") + Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") open Printf diff --git a/checker/check.mllib b/checker/check.mllib index 22df375623..488507a13f 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,12 +1,14 @@ Coq_config Hook +Terminal Canary Hashset Hashcons CSet CMap Int +Dyn HMap Option Store @@ -16,23 +18,29 @@ Flags Control Pp_control Loc +CList +CString Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode -Errors CObj -CList -CString CArray CStack Util -Ephemeron +Pp +Ppstyle +Xml_datatype +Richpp +Feedback +Segmenttree +Unicodetable +Unicode +CErrors +CWarnings +CEphemeron Future CUnix + +Minisys System Profile RemoteCounter diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 05a2a1b992..741f532848 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,16 +18,17 @@ let print_memory_stat () = if !memory_stat then begin Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ()); Format.print_newline(); - flush_all() + Format.print_flush() end let output_context = ref false -let pr_engt = function - Some ImpredicativeSet -> - str "Theory: Set is impredicative" - | None -> - str "Theory: Set is predicative" +let pr_engagement impr_set = + begin + match impr_set with + | ImpredicativeSet -> str "Theory: Set is impredicative" + | PredicativeSet -> str "Theory: Set is predicative" + end let cst_filter f csts = Cmap_env.fold @@ -51,12 +52,12 @@ let print_context env = env_modules=mods; env_modtypes=mtys}; env_stratification= {env_universes=univ; env_engagement=engt}} = env in - ppnl(hov 0 + Feedback.msg_notice + (hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ - str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_ax csts) ++ - fnl())); pp_flush() + str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_ax csts))); end let stats () = diff --git a/checker/check_stat.mli b/checker/check_stat.mli index 10908f0cc3..39e19d10e4 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/checker.ml b/checker/checker.ml index ffe1553197..95a9ea78b1 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open System open Flags @@ -16,8 +16,10 @@ open Check let () = at_exit flush_all +let chk_pp = Pp.pp_with Format.std_formatter + let fatal_error info anomaly = - flush_all (); pperrnl info; flush_all (); + flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) let coq_root = Id.of_string "Coq" @@ -67,13 +69,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str ("Cannot open " ^ dir)) + Feedback.msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d - with Errors.UserError _ -> - if_verbose msg_warning - (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + with CErrors.UserError _ -> + if_verbose Feedback.msg_warning + (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -90,7 +92,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ unix_path)) + Feedback.msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -123,7 +125,7 @@ let init_load_path () = add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) - (xdg_dirs ~warn:(fun x -> msg_warning (str x))); + (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x))); (* then directories in COQPATH *) List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath; (* then current directory *) @@ -138,10 +140,9 @@ let init_load_path () = let set_debug () = Flags.debug := true -let engagement = ref None -let set_engagement c = engagement := Some c -let engage () = - match !engagement with Some c -> Safe_typing.set_engagement c | None -> () +let impredicative_set = ref Cic.PredicativeSet +let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet +let engage () = Safe_typing.set_engagement (!impredicative_set) let admit_list = ref ([] : section_path list) @@ -178,11 +179,7 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -I dir -as coqdir map physical dir to logical coqdir\ -\n -I dir map directory dir to the empty logical path\ -\n -include dir (idem)\ -\n -R dir -as coqdir recursively map physical dir to logical coqdir\ -\n -R dir coqdir (idem)\ +" -R dir coqdir map physical dir to logical coqdir\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -214,17 +211,14 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") -let print_loc loc = - if loc = Loc.ghost then - (str"<unknown>") - else - let loc = Loc.unloc loc in - (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +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 @@ -233,7 +227,7 @@ let rec explain_exn = function | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() ) | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> @@ -242,14 +236,14 @@ let rec explain_exn = function hov 0 (str "Stack overflow") | Match_failure(filename,pos1,pos2) -> hov 1 (anomaly_string () ++ str "Match failure in file " ++ - str (guill filename) ++ str " at line " ++ int pos1 ++ + guill filename ++ str " at line " ++ int pos1 ++ str " character " ++ int pos2 ++ report ()) | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) | Failure s -> hov 0 (str "Failure: " ++ str s ++ report ()) | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> @@ -293,9 +287,10 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Pp.pp (Univ.pr_universes + chk_pp + (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); - str("\nCantApplyBadType at argument " ^ string_of_int n) + str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -310,21 +305,21 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + (str "(file \"" ++ str s ++ str "\", line " ++ int b ++ str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) - | e -> Errors.print e (* for anomalies and other uncaught exceptions *) + | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> - set_engagement Cic.ImpredicativeSet; parse rem + set_impredicative_set (); parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then - fatal_error (str ("Directory '"^s^"' does not exist")) false; + fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem @@ -334,15 +329,13 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; print_endline (Envars.coqlib ()); exit 0 @@ -380,7 +373,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; if_verbose print_header (); init_load_path (); engage (); diff --git a/checker/cic.mli b/checker/cic.mli index a793fefa83..3645587554 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -102,7 +102,7 @@ type constr = | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint - | Proj of constant * constr + | Proj of projection * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -111,7 +111,8 @@ type cofixpoint = constr pcofixpoint (** {6 Type of assumptions and contexts} *) -type rel_declaration = Name.t * constr option * constr +type rel_declaration = LocalAssum of Name.t * constr (* name, type *) + | LocalDef of Name.t * constr * constr (* name, value, type *) type rel_context = rel_declaration list (** The declarations below in .vo should be outside sections, @@ -165,7 +166,9 @@ type action (** Engagements *) -type engagement = ImpredicativeSet +type set_predicativity = ImpredicativeSet | PredicativeSet + +type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) @@ -208,6 +211,16 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) + check_universes : bool; (** If [false] universe constraints are not checked *) +} + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -216,7 +229,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; +} (** {6 Representation of mutual inductive types } *) @@ -312,9 +327,7 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) -(** {8 Data for native compilation } *) - - mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) + mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) } (** {6 Module declarations } *) @@ -333,7 +346,7 @@ type ('ty,'a) functorize = type with_declaration = | WithMod of Id.t list * module_path - | WithDef of Id.t list * constr + | WithDef of Id.t list * (constr * Univ.universe_context) type module_alg_expr = | MEident of module_path @@ -377,7 +390,7 @@ and module_body = (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; mod_retroknowledge : action list } @@ -407,7 +420,7 @@ type compiled_library = { comp_name : compilation_unit_name; comp_mod : module_body; comp_deps : library_deps; - comp_enga : engagement option; + comp_enga : engagement; comp_natsymbs : nativecode_symb_array } @@ -417,12 +430,16 @@ type compiled_library = { type library_objects -type library_disk = { +type summary_disk = { md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : library_deps; +} + +type library_disk = { md_compiled : compiled_library; md_objects : library_objects; - md_deps : library_deps; - md_imports : compilation_unit_name array } +} type opaque_table = constr Future.computation array type univ_table = diff --git a/checker/closure.ml b/checker/closure.ml index 356b683fa8..cef1d31a68 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,7 @@ let reset () = beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0 let stop() = - msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ + Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ str"]") @@ -217,10 +217,10 @@ let ref_value_cache info ref = let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context - (fun (id,b,t) (i,subs) -> - match b with - | None -> (i+1, subs) - | Some body -> (i+1, (i,body) :: subs)) + (fun decl (i,subs) -> + match decl with + | LocalAssum _ -> (i+1, subs) + | LocalDef (_,body,_) -> (i+1, (i,body) :: subs)) (rel_context env) ~init:(0,[]) (* else (0,[])*) @@ -276,7 +276,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array @@ -308,7 +308,7 @@ 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 * constant + | Zproj of int * int * projection | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') = let (depth, args, s) = strip_update_shift_app m s in (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in - let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (p, right) }) projs in + let hstack = + Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) + term = FProj (Projection.make p false, right) }) projs in argss, [Zapp hstack] | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) @@ -738,7 +739,7 @@ let rec knh info m stk = | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - if red_set info.i_flags (fCONST p) then + 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)) diff --git a/checker/closure.mli b/checker/closure.mli index e6b39250d6..8b1f246c28 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -95,7 +95,7 @@ type fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array @@ -117,7 +117,7 @@ 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 * constant + | Zproj of int * int * projection | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/checker/declarations.ml b/checker/declarations.ml index c6709a7852..1fe02c8b60 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -73,32 +73,32 @@ let solve_delta_kn resolve kn = | Equiv kn1 -> kn1 | Inline _ -> raise Not_found with Not_found -> - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - make_kn new_mp dir l + KerName.make new_mp dir l let gen_of_delta resolve x kn fix_can = let new_kn = solve_delta_kn resolve kn in if kn == new_kn then x else fix_can new_kn let constant_of_delta resolve con = - let kn = user_con con in - gen_of_delta resolve con kn (constant_of_kn_equiv kn) + let kn = Constant.user con in + gen_of_delta resolve con kn (Constant.make kn) let constant_of_delta2 resolve con = - let kn, kn' = canonical_con con, user_con con in - gen_of_delta resolve con kn (constant_of_kn_equiv kn') + let kn, kn' = Constant.canonical con, Constant.user con in + gen_of_delta resolve con kn (Constant.make kn') let mind_of_delta resolve mind = - let kn = user_mind mind in - gen_of_delta resolve mind kn (mind_of_kn_equiv kn) + let kn = MutInd.user mind in + gen_of_delta resolve mind kn (MutInd.make kn) let mind_of_delta2 resolve mind = - let kn, kn' = canonical_mind mind, user_mind mind in - gen_of_delta resolve mind kn (mind_of_kn_equiv kn') + let kn, kn' = MutInd.canonical mind, MutInd.user mind in + gen_of_delta resolve mind kn (MutInd.make kn') let find_inline_of_delta kn resolve = match Deltamap.find_kn kn resolve with @@ -106,7 +106,7 @@ let find_inline_of_delta kn resolve = | _ -> raise Not_found let constant_of_delta_with_inline resolve con = - let kn1,kn2 = canonical_con con,user_con con in + let kn1,kn2 = Constant.canonical con, Constant.user con in try find_inline_of_delta kn2 resolve with Not_found -> try find_inline_of_delta kn1 resolve @@ -137,17 +137,17 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (make_kn mp' dir l) + solve_delta_kn resolve (KerName.make mp' dir l) | None -> kn let subst_kn sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - make_kn mp' dir l + KerName.make mp' dir l | None -> kn exception No_subst @@ -165,14 +165,14 @@ let gen_subst_mp f sub mp1 mp2 = | Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2 let make_mind_equiv mpu mpc dir l = - let knu = make_kn mpu dir l in - if mpu == mpc then mind_of_kn knu - else mind_of_kn_equiv knu (make_kn mpc dir l) + let knu = KerName.make mpu dir l in + if mpu == mpc then MutInd.make1 knu + else MutInd.make knu (KerName.make mpc dir l) let subst_ind sub mind = - let kn1,kn2 = user_mind mind, canonical_mind mind in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in + let kn1,kn2 = MutInd.user mind, MutInd.canonical mind in + let mp1,dir,l = KerName.repr kn1 in + let mp2,_,_ = KerName.repr kn2 in let rebuild_mind mp1 mp2 = make_mind_equiv mp1 mp2 dir l in try let side,mind',resolve = gen_subst_mp rebuild_mind sub mp1 mp2 in @@ -182,14 +182,14 @@ let subst_ind sub mind = with No_subst -> mind let make_con_equiv mpu mpc dir l = - let knu = make_kn mpu dir l in - if mpu == mpc then constant_of_kn knu - else constant_of_kn_equiv knu (make_kn mpc dir l) + let knu = KerName.make mpu dir l in + if mpu == mpc then Constant.make1 knu + else Constant.make knu (KerName.make mpc dir l) let subst_con0 sub con u = - let kn1,kn2 = user_con con,canonical_con con in - let mp1,dir,l = repr_kn kn1 in - let mp2,_,_ = repr_kn kn2 in + let kn1,kn2 = Constant.user con, Constant.canonical con in + let mp1,dir,l = KerName.repr kn1 in + let mp2,_,_ = KerName.repr kn2 in let rebuild_con mp1 mp2 = make_con_equiv mp1 mp2 dir l in let dup con = con, Const (con, u) in let side,con',resolve = gen_subst_mp rebuild_con sub mp1 mp2 in @@ -206,14 +206,15 @@ let rec map_kn f f' c = let func = map_kn f f' in match c with | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) - | Proj (kn,t) -> - let kn' = - try fst (f' kn Univ.Instance.empty) - with No_subst -> kn + | Proj (p,t) -> + let p' = + Projection.map (fun kn -> + try fst (f' kn Univ.Instance.empty) + with No_subst -> kn) p in let t' = func t in - if kn' == kn && t' == t then c - else Proj (kn', t') + if p' == p && t' == t then c + else Proj (p', t') | Ind ((kn,i),u) -> let kn' = f kn in if kn'==kn then c else Ind ((kn',i),u) @@ -303,7 +304,9 @@ let subset_prefixed_by mp resolver = match hint with | Inline _ -> rslv | Equiv _ -> - if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + if mp_in_mp mp (KerName.modpath kn) + then Deltamap.add_kn kn hint rslv + else rslv in Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver @@ -425,7 +428,7 @@ let subst_lazy_constr sub = function let indirect_opaque_access = ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) let indirect_opaque_univ_access = - ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints) + ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t) let force_lazy_constr = function | Indirect (l,dp,i) -> @@ -434,7 +437,7 @@ let force_lazy_constr = function let force_lazy_constr_univs = function | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i - | _ -> Univ.empty_constraint + | _ -> Univ.ContextSet.empty let subst_constant_def sub = function | Undef inl -> Undef inl @@ -456,6 +459,8 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Def _ | Undef _ -> false +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 @@ -514,11 +519,8 @@ let map_decl_arity f g = function | RegularArity a -> RegularArity (f a) | TemplateArity a -> TemplateArity (g a) - -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_declaration sub = + Term.map_rel_decl (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -583,7 +585,7 @@ let implem_map fs fa = function let subst_with_body sub = function | WithMod(id,mp) -> WithMod(id,subst_mp sub mp) - | WithDef(id,c) -> WithDef(id,subst_mps sub c) + | WithDef(id,(c,ctx)) -> WithDef(id,(subst_mps sub c,ctx)) let rec subst_expr sub = function | MEident mp -> MEident (subst_mp sub mp) diff --git a/checker/declarations.mli b/checker/declarations.mli index 3c6db6ab71..456df83699 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -2,17 +2,18 @@ open Names open Cic val force_constr : constr_substituted -> constr -val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints +val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t val from_val : constr -> constr_substituted val indirect_opaque_access : (DirPath.t -> int -> constr) ref -val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref +val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref (** Constant_body *) 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 (* Mutual inductives *) diff --git a/checker/environ.ml b/checker/environ.ml index 710ebc7127..7b59c6b986 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,4 +1,4 @@ -open Errors +open CErrors open Util open Names open Cic @@ -14,7 +14,7 @@ type globals = { type stratification = { env_universes : Univ.universes; - env_engagement : engagement option + env_engagement : engagement } type env = { @@ -33,19 +33,23 @@ let empty_env = { env_rel_context = []; env_stratification = { env_universes = Univ.initial_universes; - env_engagement = None}; + env_engagement = PredicativeSet }; env_imports = MPmap.empty } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let rel_context env = env.env_rel_context -let set_engagement c env = - match env.env_stratification.env_engagement with - | Some c' -> if c=c' then env else error "Incompatible engagement" - | None -> - { env with env_stratification = - { env.env_stratification with env_engagement = Some c } } +let set_engagement (impr_set as c) env = + let expected_impr_set = + env.env_stratification.env_engagement in + begin + match impr_set,expected_impr_set with + | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" + | _ -> () + end; + { env with env_stratification = + { env.env_stratification with env_engagement = c } } (* Digests *) @@ -71,17 +75,24 @@ let push_rel d env = let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) -let add_constraints c env = - if c == Univ.Constraint.empty then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if c == Univ.Constraint.empty then env + else map_universes (Univ.merge_constraints c) env + +let push_context ?(strict=false) ctx env = + map_universes (Univ.merge_context strict ctx) env + +let push_context_set ?(strict=false) ctx env = + map_universes (Univ.merge_context_set strict ctx) env let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes @@ -96,7 +107,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") - (string_of_con kn); + (Constant.to_string kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in let new_globals = @@ -147,8 +158,8 @@ let evaluable_constant cst env = let is_projection cst env = not (Option.is_empty (lookup_constant cst env).const_proj) -let lookup_projection cst env = - match (lookup_constant cst env).const_proj with +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") @@ -156,12 +167,14 @@ let lookup_projection cst env = let scrape_mind env kn= try KNmap.find kn env.env_globals.env_inductives_eq - with - Not_found -> kn + with + Not_found -> kn let mind_equiv env (kn1,i1) (kn2,i2) = Int.equal i1 i2 && - KerName.equal (scrape_mind env (user_mind kn1)) (scrape_mind env (user_mind kn2)) + KerName.equal + (scrape_mind env (MutInd.user kn1)) + (scrape_mind env (MutInd.user kn2)) let lookup_mind kn env = @@ -170,9 +183,9 @@ 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") - (string_of_mind kn); + (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in - let kn1,kn2 = user_mind kn,canonical_mind kn in + let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in let new_inds_eq = if KerName.equal kn1 kn2 then env.env_globals.env_inductives_eq else @@ -189,7 +202,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") - (string_of_mp ln); + (ModPath.to_string ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = { env.env_globals with @@ -199,7 +212,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") - (string_of_mp mp); + (ModPath.to_string mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = { env.env_globals with @@ -209,7 +222,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") - (string_of_mp mp); + (ModPath.to_string mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = { env.env_globals with diff --git a/checker/environ.mli b/checker/environ.mli index d3448b127f..87f143d1bb 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -11,7 +11,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : engagement option; + env_engagement : engagement; } type env = { env_globals : globals; @@ -22,7 +22,7 @@ type env = { val empty_env : env (* Engagement *) -val engagement : env -> Cic.engagement option +val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env (* Digests *) @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) @@ -51,7 +53,7 @@ val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool val is_projection : constant -> env -> bool -val lookup_projection : constant -> env -> projection_body +val lookup_projection : projection -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool diff --git a/checker/include b/checker/include index f5bd2984ee..6bea3c91a7 100644 --- a/checker/include +++ b/checker/include @@ -31,7 +31,7 @@ open Typeops;; open Check;; open Pp;; -open Errors;; +open CErrors;; open Util;; open Names;; open Term;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2ce9f038a0..27f79e7963 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -32,11 +32,11 @@ let string_of_mp mp = if !Flags.debug then debug_string_of_mp mp else string_of_mp mp let prkn kn = - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = KerName.repr kn in str(string_of_mp mp ^ "." ^ Label.to_string l) let prcon c = - let ck = canonical_con c in - let uk = user_con c in + let ck = Constant.canonical c in + let uk = Constant.user c in if KerName.equal ck uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")") (* Same as noccur_between but may perform reductions. @@ -44,7 +44,7 @@ let prcon c = let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else - let t' = whd_betadeltaiota env t in + let t' = whd_all env t in if noccur_between x nvars t' then Some t' else None @@ -56,10 +56,10 @@ let is_constructor_head t = let conv_ctxt_prefix env (ctx1:rel_context) ctx2 = let rec chk env rctx1 rctx2 = match rctx1, rctx2 with - (_,None,ty1 as d1)::rctx1', (_,None,ty2)::rctx2' -> + (LocalAssum (_,ty1) as d1)::rctx1', LocalAssum (_,ty2)::rctx2' -> conv env ty1 ty2; chk (push_rel d1 env) rctx1' rctx2' - | (_,Some bd1,ty1 as d1)::rctx1', (_,Some bd2,ty2)::rctx2' -> + | (LocalDef (_,bd1,ty1) as d1)::rctx1', LocalDef (_,bd2,ty2)::rctx2' -> conv env ty1 ty2; conv env bd1 bd2; chk (push_rel d1 env) rctx1' rctx2' @@ -90,14 +90,14 @@ exception InductiveError of inductive_error (* Typing the arities and constructor types *) let rec sorts_of_constr_args env t = - let t = whd_betadeltaiota_nolet env t in + let t = whd_allnolet env t in match t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in varj :: sorts_of_constr_args env1 c2 | LetIn (name,def,ty,c) -> - let env1 = push_rel (name,Some def,ty) env in + let env1 = push_rel (LocalDef (name,def,ty)) env in sorts_of_constr_args env1 c | _ when is_constructor_head t -> [] | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") @@ -167,7 +167,7 @@ let typecheck_arity env params inds = full_arity is used as argument or subject to cast, an upper universe will be generated *) let id = ind.mind_typename in - let env_ar' = push_rel (Name id, None, arity) env_ar in + let env_ar' = push_rel (LocalAssum (Name id, arity)) env_ar in env_ar') env inds in @@ -184,7 +184,7 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, Some ImpredicativeSet -> () + | Prop Pos, ImpredicativeSet -> () | Prop Pos, _ -> if not small then failwith "impredicative Set inductive type" | Prop Null,_ -> () @@ -230,7 +230,6 @@ let compute_elim_sorts env_ar params mib arity lc = let infos = Array.map (sorts_of_constr_args env_params) lc in let (small,unit) = small_unit infos in (* We accept recursive unit types... *) - let unit = unit && mib.mind_ntypes = 1 in (* compute the max of the sorts of the products of the constructor type *) let level = max_inductive_sort (Array.concat (Array.to_list (Array.map Array.of_list infos))) in @@ -270,7 +269,7 @@ type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int | LocalNotConstructor - | LocalNonPar of int * int + | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -292,9 +291,9 @@ let explain_ind_err ntyp env0 nbpar c err = | LocalNotConstructor -> raise (InductiveError (NotConstructor (env,c',Rel (ntyp+nbpar)))) - | LocalNonPar (n,l) -> + | LocalNonPar (n,i,l) -> raise (InductiveError - (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) + (NonPar (env,c',n,Rel i,Rel (l+nbpar)))) let failwith_non_pos n ntypes c = for k = n to n + ntypes - 1 do @@ -320,11 +319,11 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = let nhyps = List.length hyps in let rec check k index = function | [] -> () - | (_,Some _,_)::hyps -> check k (index+1) hyps + | LocalDef _ :: hyps -> check k (index+1) hyps | _::hyps -> - match whd_betadeltaiota env lpar.(k) with + match whd_all env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) + | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' @@ -341,9 +340,9 @@ let check_rec_par (env,n,_,_) hyps nrecp largs = | ([],_) -> () | (_,[]) -> failwith "number of recursive parameters cannot be greater than the number of parameters." - | (lp,(_,Some _,_)::hyps) -> find (index-1) (lp,hyps) + | (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps) | (p::lp,_::hyps) -> - (match whd_betadeltaiota env p with + (match whd_all env p with | Rel w when w = index -> find (index-1) (lp,hyps) | _ -> failwith "bad number of recursive parameters") in find (n-1) (lpar,List.rev hyps) @@ -371,14 +370,15 @@ let abstract_mind_lc env ntyps npars lc = [lra] is the list of recursive tree of each variable *) let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = - (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + (push_rel (LocalAssum (x,a)) env, n+1, ntypes, (Norec,ra)::lra) let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let auxntyp = 1 in let specif = lookup_mind_specif env mi in let env' = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) env in + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env (specif,u)) lpar) in + push_rel decl env in let ra_env' = (Imbr mi,(Rtree.mk_rec_calls 1).(0)) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -388,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if n=0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -401,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let lparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) let rec check_pos (env, n, ntypes, ra_env as ienv) c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -470,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc and check_constructors ienv check_head c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -528,7 +528,7 @@ let check_positivity env_ar mind params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose ppnl (str " checking ind: " ++ pr_mind kn); pp_flush (); + 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 (* check mind_record : TODO ? check #constructor = 1 ? *) diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 5188f80d13..071eecbbcd 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/inductive.ml b/checker/inductive.ml index 59d1a645a5..c4ffc141ff 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) = (mib, mib.mind_packets.(tyi)) let find_rectype env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match t with | Ind (ind,_) when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l) @@ -59,16 +59,6 @@ let inductive_instance mib = UContext.instance mib.mind_universes else Instance.empty -let inductive_context mib = - if mib.mind_polymorphic then - instantiate_univ_context mib.mind_universes - else UContext.empty - -let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - subst_instance_constraints u (UContext.constraints mib.mind_universes) - else Constraint.empty - (************************************************************************) (* Build the substitution that replaces Rels by the appropriate *) @@ -88,10 +78,10 @@ let instantiate_params full t u args sign = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = fold_rel_context - (fun (_,copt,_) (largs,subs,ty) -> - match (copt, largs, ty) with - | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) - | (Some b,_,LetIn(_,_,_,t)) -> + (fun decl (largs,subs,ty) -> + match (decl, largs, ty) with + | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) + | (LocalDef (_,b,_),_,LetIn(_,_,_,t)) -> (largs, (substl subs (subst_instance_constr u b))::subs, t) | (_,[],_) -> if full then fail() else ([], subs, ty) | _ -> fail ()) @@ -103,13 +93,12 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (sign,dummy) in + let t = mkArity (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) = - let inst_ind = constructor_instantiate mind u mib in - (fun t -> - instantiate_params true (inst_ind t) u params mib.mind_params_ctxt) +let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = + let inst_ind = constructor_instantiate mind u mib t in + instantiate_params true inst_ind u params mib.mind_params_ctxt (************************************************************************) (************************************************************************) @@ -142,53 +131,58 @@ let sort_as_univ = function | Prop Null -> Univ.type0m_univ | Prop Pos -> Univ.type0_univ +(* cons_subst add the mapping [u |-> su] in subst if [u] is not *) +(* in the domain or add [u |-> sup x su] if [u] is already mapped *) +(* to [x]. *) let cons_subst u su subst = - Univ.LMap.add u su subst - -let actualize_decl_level env lev t = - let sign,s = dest_arity env t in - mkArity (sign,lev) - -let polymorphism_on_non_applied_parameters = false + try + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> Univ.LMap.add u su subst + +(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *) +(* if it is presents and returns the substitution unchanged if not.*) +let remember_subst u subst = + try + let su = Universe.make u in + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> subst (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = function - | (_,Some _,_ as t)::sign, exp, args -> - let ctx,subst = make_subst env (sign, exp, args) in - t::ctx, subst - | d::sign, None::exp, args -> - let args = match args with _::args -> args | [] -> [] in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, subst - | d::sign, Some u::exp, a::args -> - (* We recover the level of the argument, but we don't change the *) - (* level in the corresponding type in the arity; this level in the *) - (* arity is a global level which, at typing time, will be enforce *) - (* to be greater than the level of the argument; this is probably *) - (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env a)) in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, cons_subst u s subst - | (na,None,t as d)::sign, Some u::exp, [] -> - (* No more argument here: we instantiate the type with a fresh level *) - (* which is first propagated to the corresponding premise in the arity *) - (* (actualize_decl_level), then to the conclusion of the arity (via *) - (* the substitution) *) - let ctx,subst = make_subst env (sign, exp, []) in - d::ctx, subst - | sign, [], _ -> - (* Uniform parameters are exhausted *) - sign,Univ.LMap.empty - | [], _, _ -> - assert false - - -exception SingletonInductiveBecomesProp of Id.t +let rec make_subst env = + let rec make subst = function + | LocalDef _ :: sign, exp, args -> + make subst (sign, exp, args) + | d::sign, None::exp, args -> + let args = match args with _::args -> args | [] -> [] in + make subst (sign, exp, args) + | d::sign, Some u::exp, a::args -> + (* We recover the level of the argument, but we don't change the *) + (* level in the corresponding type in the arity; this level in the *) + (* arity is a global level which, at typing time, will be enforce *) + (* to be greater than the level of the argument; this is probably *) + (* a useless extra constraint *) + let s = sort_as_univ (snd (dest_arity env a)) in + make (cons_subst u s subst) (sign, exp, args) + | LocalAssum (na,t) :: sign, Some u::exp, [] -> + (* No more argument here: we add the remaining universes to the *) + (* substitution (when [u] is distinct from all other universes in the *) + (* template, it is identity substitution otherwise (ie. when u is *) + (* already in the domain of the substitution) [remember_subst] will *) + (* update its image [x] by [sup x u] in order not to forget the *) + (* dependency in [u] that remains to be fullfilled. *) + make (remember_subst u subst) (sign, exp, []) + | sign, [], _ -> + (* Uniform parameters are exhausted *) + subst + | [], _, _ -> + assert false + in + make Univ.LMap.empty let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in - let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let subst = make_subst env (ctx,ar.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -202,11 +196,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let is_prop_sort = function - | Prop Null -> true - | _ -> false - -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +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 @@ -214,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) - -let type_of_inductive env pind = - type_of_inductive_gen env pind [||] - -let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty = type_of_inductive_gen env pind [||] in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty = type_of_inductive_gen env pind args in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) + mkArity (List.rev ctx,s) let type_of_inductive_knowing_parameters env mip args = type_of_inductive_gen env mip args @@ -269,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = let type_of_constructor cstru mspec = type_of_constructor_gen cstru mspec -let type_of_constructor_in_ctx cstr (mib,mip as mspec) = - let u = Univ.UContext.instance mib.mind_universes in - let c = type_of_constructor_gen (cstr, u) mspec in - (c, mib.mind_universes) - -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib u in - (ty, cst) - let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in Array.map (constructor_instantiate kn u mib) specif @@ -313,8 +275,8 @@ let elim_sorts (_,mip) = mip.mind_kelim let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -337,15 +299,15 @@ let check_allowed_sort ksort specif = let is_correct_arity env c (p,pj) ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = - let pt' = whd_betadeltaiota env pt in + let pt' = whd_all env pt in match pt', ar with - | Prod (na1,a1,t), (_,None,a1')::ar' -> + | Prod (na1,a1,t), LocalAssum (_,a1')::ar' -> (try conv env a1 a1' with NotConvertible -> raise (LocalArity None)); - srec (push_rel (na1,None,a1) env) t ar' + srec (push_rel (LocalAssum (na1,a1)) env) t ar' | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (na1,None,a1) env in - let ksort = match (whd_betadeltaiota env' a2) with + let env' = push_rel (LocalAssum (na1,a1)) env in + let ksort = match (whd_all env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in @@ -356,8 +318,8 @@ let is_correct_arity env c (p,pj) ind specif params = | Sort s', [] -> check_allowed_sort (family_of_sort s') specif; false - | _, (_,Some _,_ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + | _, (LocalDef _ as d)::ar' -> + srec (push_rel d env) (lift 1 pt') ar' | _ -> raise (LocalArity None) in @@ -521,10 +483,10 @@ type guard_env = let make_renv env recarg tree = { env = env; rel_min = recarg+2; (* recarg = 0 ==> Rel 1 -> recarg; Rel 2 -> fix *) - genv = [Lazy.lazy_from_val(Subterm(Large,tree))] } + genv = [Lazy.from_val(Subterm(Large,tree))] } let push_var renv (x,ty,spec) = - { env = push_rel (x,None,ty) renv.env; + { env = push_rel (LocalAssum (x,ty)) renv.env; rel_min = renv.rel_min+1; genv = spec:: renv.genv } @@ -532,7 +494,7 @@ let assign_var_spec renv (i,spec) = { renv with genv = List.assign renv.genv (i-1) spec } let push_var_renv renv (x,ty) = - push_var renv (x,ty,Lazy.lazy_from_val Not_subterm) + push_var renv (x,ty,Lazy.from_val Not_subterm) (* Fetch recursive information about a variable p *) let subterm_var p renv = @@ -543,13 +505,13 @@ let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } let push_fix_renv renv (_,v,_ as recdef) = let n = Array.length v in { env = push_rec_types recdef renv.env; rel_min = renv.rel_min+n; - genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv } + genv = iterate (fun ge -> Lazy.from_val Not_subterm::ge) n renv.genv } (* Definition and manipulation of the stack *) @@ -616,20 +578,21 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,l' = decompose_app (whd_all env s) in match i with Ind _ -> true | _ -> false (* The following functions are almost duplicated from indtypes.ml, except that they carry here a poorer environment (containing less information). *) let ienv_push_var (env, lra) (x,a,ra) = -(push_rel (x,None,a) env, (Norec,ra)::lra) +(push_rel (LocalAssum (x,a)) env, (Norec,ra)::lra) let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) env + let decl = LocalAssum (Anonymous, + hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in let rc = Array.mapi (fun j t -> (Imbr (mind,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -639,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -669,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -728,7 +691,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match x with | Prod (na,b,d) -> @@ -757,7 +720,7 @@ let restrict_spec env spec p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,args = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_all env s) in match i with | Ind i -> begin match spec with @@ -779,7 +742,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) - let f,l = decompose_app (whd_betadeltaiota renv.env t) in + let f,l = decompose_app (whd_all renv.env t) in match f with | Rel k -> subterm_var k renv @@ -855,7 +818,7 @@ and stack_element_specif = function |SArg x -> x and extract_stack renv a = function - | [] -> Lazy.lazy_from_val Not_subterm , [] + | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -893,11 +856,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (rel_context_length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = - let t = whd_betadeltaiota env ar in + let t = whd_all env ar in match stack, t with | elt :: stack', Prod (n,a,c0) -> - let d = (n,None,a) in - let ty, args = decompose_app (whd_betadeltaiota env a) in + let d = LocalAssum (n,a) in + let ty, args = decompose_app (whd_all env a) in let elt = match ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -950,10 +913,10 @@ let check_one_fix renv recpos trees def = end else begin - match pi2 (lookup_rel p renv.env) with - | None -> + match lookup_rel p renv.env with + | LocalAssum _ -> List.iter (check_rec_call renv []) l - | Some c -> + | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> check_rec_call renv stack (applist(lift p c,l)) @@ -1026,6 +989,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var _ -> anomaly (Pp.str "Section variable in Coqchk !") | Sort _ -> assert (l = []) @@ -1035,8 +1002,6 @@ let check_one_fix renv recpos trees def = | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - | Proj (p, c) -> check_rec_call renv [] c - and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body @@ -1069,10 +1034,10 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match (whd_betadeltaiota env def) with + match (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in if n = k+1 then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1118,10 +1083,10 @@ let anomaly_ill_typed () = anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in + let b = whd_all env c in match b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1130,7 +1095,7 @@ let rec codomain_is_coind env c = let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then - let c,args = decompose_app (whd_betadeltaiota env t) in + let c,args = decompose_app (whd_all env t) in match c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive @@ -1162,7 +1127,7 @@ let check_one_cofix env nbfix def deftype = | Lambda (x,a,b) -> assert (args = []); if noccur_with_meta n nbfix a then - let env' = push_rel (x, None, a) env in + let env' = push_rel (LocalAssum (x,a)) env in check_rec_call env' alreadygrd (n+1) tree vlra b else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) diff --git a/checker/inductive.mli b/checker/inductive.mli index 78fb0bdd13..ed3a7b53ce 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 998e23c6e8..7f93e15609 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,19 +18,27 @@ let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in match hd with Sort (Type u) when not (Univ.is_univ_variable u) -> - let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in - mkArity (ctxt,Prop Null), - Univ.enforce_leq u u' Univ.empty_constraint - | _ -> ar, Univ.empty_constraint + 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 ppnl (str " checking cst: " ++ prcon kn); pp_flush (); - let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); + 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 = add_constraints cu env' 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 @@ -62,14 +70,14 @@ let check_constant_declaration env kn cb = let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> - failwith ("Unknown module: "^string_of_mp mp) + failwith ("Unknown module: "^ModPath.to_string mp) let mk_mtb mp sign delta = { mod_mp = mp; mod_expr = Abstract; mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.Constraint.empty; + mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = []; } diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index ae28caed09..5c7b392ffd 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/modops.ml b/checker/modops.ml index 8ccf118d3b..aba9da2fef 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names @@ -28,12 +28,12 @@ let error_not_match l _ = let error_no_such_label l = error ("No such label "^Label.to_string l) let error_no_such_label_sub l l1 = - let l1 = string_of_mp l1 in + let l1 = ModPath.to_string l1 in error ("The field "^ Label.to_string l^" is missing in "^l1^".") let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module")) + user_err ~loc (str ("\""^Label.to_string s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc Loc.ghost s @@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - (* let con = constant_of_delta resolver con in*) let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + Univ.make_abstract_instance cb.const_universes else Univ.Instance.empty in - { cb with const_body = Def (Declarations.from_val (Const (con,u))) } + { 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 diff --git a/checker/modops.mli b/checker/modops.mli index e22c2656c8..26a088f32b 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/print.ml b/checker/print.ml index 1cc48ff774..7ef752b002 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,7 +10,9 @@ open Format open Cic open Names -let print_instance i = Pp.pp (Univ.Instance.pr i) +let chk_pp = Pp.pp_with Format.std_formatter + +let print_instance i = chk_pp (Univ.Instance.pr i) let print_pure_constr csr = let rec term_display c = match c with @@ -100,7 +102,7 @@ let print_pure_constr csr = done in print_string"{"; print_fix (); print_string"}" | Proj (p, c) -> - print_string "Proj("; sp_con_display p; print_string ","; + print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; box_display c; print_string ")" and box_display c = open_hovbox 1; term_display c; close_box() @@ -108,7 +110,7 @@ let print_pure_constr csr = and sort_display = function | Prop(Pos) -> print_string "Set" | Prop(Null) -> print_string "Prop" - | Type u -> print_string "Type("; Pp.pp (Univ.pr_uni u); print_string ")" + | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")" and name_display = function | Name id -> print_string (Id.to_string id) @@ -122,7 +124,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_mind sp) + print_string (MutInd.debug_to_string sp) and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = @@ -131,7 +133,7 @@ let print_pure_constr csr = | ("Coq"::_::l) -> l | l -> l in List.iter (fun x -> print_string x; print_string ".") ls;*) - print_string (debug_string_of_con sp) + print_string (Constant.debug_to_string sp) in try diff --git a/checker/reduction.ml b/checker/reduction.ml index 185c6edfcd..ec16aa2615 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Cic open Term @@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.constant * lift + | Zlproj of Names.projection * 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 @@ -92,13 +92,13 @@ let whd_betaiotazeta x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t @@ -137,7 +137,9 @@ 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 c1 c2) then + if not (Names.eq_con_chk + (Names.Projection.constant c1) + (Names.Projection.constant c2)) then raise NotConvertible | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> if not (fmind ci1.ci_ind ci2.ci_ind) then @@ -156,7 +158,7 @@ type conv_pb = | CONV | CUMUL -let sort_cmp univ pb s0 s1 = +let sort_cmp env univ pb s0 s1 = match (s0,s1) with | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible @@ -165,11 +167,21 @@ let sort_cmp univ pb s0 s1 = CUMUL -> () | _ -> raise NotConvertible) | (Type u1, Type u2) -> - if not + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with | CONV -> Univ.check_eq univ u1 u2 | CUMUL -> Univ.check_leq univ u1 u2) - then raise NotConvertible + 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)) + end; + raise NotConvertible + end | (_, _) -> raise NotConvertible let rec no_arg_available = function @@ -251,7 +263,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (match a1, a2 with | (Sort s1, Sort s2) -> assert (is_empty_stack v1 && is_empty_stack v2); - sort_cmp univ cv_pb s1 s2 + sort_cmp (infos_env infos) univ cv_pb s1 s2 | (Meta n, Meta m) -> if n=m then convert_stacks univ infos lft1 lft2 v1 v2 @@ -465,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true * error message. *) let hnf_prod_app env t n = - match whd_betadeltaiota env t with + match whd_all env t with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -476,10 +488,10 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in match t with | Prod (n,a,c0) -> - let d = (n,None,a) in + let d = LocalAssum (n,a) in decrec (push_rel d env) (d::m) c0 | _ -> m,t in @@ -488,17 +500,17 @@ let dest_prod env = (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match rty with | Prod (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + 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_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in @@ -506,13 +518,13 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match rty with | Lambda (x,t,c) -> - let d = (x,None,t) in + let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (d::l) c | LetIn (x,b,t,c) -> - let d = (x,Some b,t) in + 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 diff --git a/checker/reduction.mli b/checker/reduction.mli index 2e87346980..15a2df1f14 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,8 +16,8 @@ open Environ (*s Reduction functions *) val whd_betaiotazeta : constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr (************************************************************************) (*s conversion functions *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 35f7f14b67..53d80c6d55 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,18 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp -open Errors +open CErrors open Util open Cic open Names open Environ +let pr_dirpath dp = str (DirPath.to_string dp) + (************************************************************************) (* * Global environment @@ -27,26 +29,29 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb univs digest = let env = !genv in - let env = add_constraints mb.mod_constraints env in - let env = add_constraints univs env in + let env = push_context_set ~strict:true mb.mod_constraints env in + let env = push_context_set ~strict:true univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest -(* Check that the engagement expected by a library matches the initial one *) -let check_engagement env c = - match engagement env, c with - | Some ImpredicativeSet, Some ImpredicativeSet -> () - | _, None -> () - | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" +(* Check that the engagement expected by a library extends the initial one *) +let check_engagement env expected_impredicative_set = + let impredicative_set = Environ.engagement env in + begin + match impredicative_set, expected_impredicative_set with + | PredicativeSet, ImpredicativeSet -> + CErrors.error "Needs option -impredicative-set." + | _ -> () + end; + () (* Libraries = Compiled modules *) let report_clash f caller dir = let msg = - str "compiled library " ++ str(DirPath.to_string caller) ++ + str "compiled library " ++ pr_dirpath caller ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(DirPath.to_string dir) ++ fnl() in + pr_dirpath dir ++ fnl() in f msg @@ -71,18 +76,19 @@ let stamp_library file digest = () warning is issued in case of mismatch *) let import file clib univs digest = let env = !genv in - check_imports msg_warning clib.comp_name env clib.comp_deps; + check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module - (add_constraints univs - (add_constraints mb.mod_constraints env)) mb.mod_mp mb; + (push_context_set ~strict:true univs + (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest (* When the module is admitted, digests *must* match *) let unsafe_import file clib univs digest = let env = !genv in - check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + if !Flags.debug then check_imports Feedback.msg_warning 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 e16e64e6a2..8724f8e014 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,6 +15,6 @@ val get_env : unit -> env val set_engagement : engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit val unsafe_import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 372c314247..7eae9b8310 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -1,13 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open Errors +open CErrors open Util open Names open Cic @@ -103,7 +103,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in - check eq_mind (fun x -> x.proj_ind); + check MutInd.equal (fun x -> x.proj_ind); check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); @@ -302,7 +302,7 @@ 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 (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = 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 (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/checker/subtyping.mli b/checker/subtyping.mli index 03242cbcfc..cc66fc5382 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/term.ml b/checker/term.ml index 93540276b7..591348cb69 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,7 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) -open Errors +open CErrors open Util open Names open Esubst @@ -222,24 +222,29 @@ let rel_context_length = List.length let rel_context_nhyps hyps = let rec nhyps acc = function | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in + | LocalAssum _ :: hyps -> nhyps (1+acc) hyps + | LocalDef _ :: hyps -> nhyps acc hyps in nhyps 0 hyps let fold_rel_context f l ~init = List.fold_right f l init -let map_rel_context f l = - let map_decl (n, body_o, typ as decl) = - let body_o' = Option.smartmap f body_o in - let typ' = f typ in - if body_o' == body_o && typ' == typ then decl else - (n, body_o', typ') - in - List.smartmap map_decl l +let map_rel_decl f = function + | LocalAssum (n, typ) as decl -> + let typ' = f typ in + if typ' == typ then decl else + LocalAssum (n, typ') + | LocalDef (n, body, typ) as decl -> + let body' = f body in + let typ' = f typ in + if body' == body && typ' == typ then decl else + LocalDef (n, body', typ') + +let map_rel_context f = + List.smartmap (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function - | (_,None,_) :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps + | LocalAssum _ :: hyps -> reln (Rel (n+p) :: l) (p+1) hyps + | LocalDef _ :: hyps -> reln l (p+1) hyps | [] -> l in reln [] 1 hyps @@ -272,8 +277,8 @@ let decompose_lam_n_assum n = 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 ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c + | 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" in @@ -282,18 +287,18 @@ let decompose_lam_n_assum n = (* Iterate products, with or without lets *) (* Constructs either [(x:t)c] or [[x=b:t]c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> Prod (na, t, c) - | Some b -> LetIn (na, b, t, c) +let mkProd_or_LetIn decl c = + match decl with + | LocalAssum (na,t) -> Prod (na, t, c) + | LocalDef (na,b,t) -> LetIn (na, b, t, c) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let decompose_prod_assum = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in @@ -305,8 +310,8 @@ let decompose_prod_n_assum n = 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 ((x,None,t) :: l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c + | 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" in @@ -324,8 +329,8 @@ let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign let destArity = let rec prodec_rec l c = match c with - | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t)::l) c + | 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") @@ -392,7 +397,7 @@ let compare_constr f t1 t2 = Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 - | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2 + | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2 | _ -> false let rec eq_constr m n = diff --git a/checker/term.mli b/checker/term.mli index ab488b2b7c..6b026d056f 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,12 +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 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 decompose_lam_n_assum : int -> constr -> rel_context * constr -val mkProd_or_LetIn : name * constr option * constr -> constr -> constr +val mkProd_or_LetIn : rel_declaration -> constr -> constr val it_mkProd_or_LetIn : constr -> rel_context -> constr val decompose_prod_assum : constr -> rel_context * constr val decompose_prod_n_assum : int -> constr -> rel_context * constr diff --git a/checker/type_errors.ml b/checker/type_errors.ml index c4c6528651..b7718e02da 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/type_errors.mli b/checker/type_errors.mli index 036ff45462..d9d1479580 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/typeops.ml b/checker/typeops.ml index 9bc4b269b8..173e19ce1b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic @@ -33,7 +33,7 @@ let check_constraints cst env = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env (c,ty as j) = - match whd_betadeltaiota env ty with + match whd_all env ty with | Sort s -> (c,s) | _ -> error_not_type env j @@ -62,7 +62,7 @@ let judge_of_type u = Sort (Type (Univ.super u)) let judge_of_relative env n = try - let (_,_,typ) = lookup_rel n env in + let LocalAssum (_,typ) | LocalDef (_,_,typ) = lookup_rel n env in lift n typ with Not_found -> error_unbound_rel env n @@ -92,7 +92,7 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = let _cb = try lookup_constant kn env with Not_found -> - failwith ("Cannot find constant: "^string_of_con kn) + failwith ("Cannot find constant: "^Constant.to_string kn) in let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in let () = check_constraints cu env in @@ -107,7 +107,7 @@ let judge_of_apply env (f,funj) argjv = let rec apply_rec n typ = function | [] -> typ | (h,hj)::restjl -> - (match whd_betadeltaiota env typ with + (match whd_all env typ with | Prod (_,c1,c2) -> (try conv_leq env hj c1 with NotConvertible -> @@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - if engagement env = Some ImpredicativeSet then + if engagement env = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort else @@ -178,7 +178,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_mind (fst ind)) + failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -192,7 +192,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_mind (fst ind)) + failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif @@ -223,7 +223,7 @@ let judge_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (c, ct) in - assert(eq_mind pb.proj_ind (fst ind)); + assert(MutInd.equal pb.proj_ind (fst ind)); let ty = subst_instance_constr u pb.proj_type in substl (c :: List.rev args) ty @@ -296,13 +296,13 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let j' = execute env1 c2 in Prod(name,c1,j') | Prod (name,c1,c2) -> let varj = execute_type env c1 in - let env1 = push_rel (name,None,c1) env in + let env1 = push_rel (LocalAssum (name,c1)) env in let varj' = execute_type env1 c2 in Sort (sort_of_product env varj varj') @@ -314,7 +314,7 @@ let rec execute env cstr = let env',c2' = (* refresh_arity env *) env, c2 in let _ = execute_type env' c2' in judge_of_cast env' (c1,j1) DEFAULTcast c2' in - let env1 = push_rel (name,Some c1,c2) env in + let env1 = push_rel (LocalDef (name,c1,c2)) env in let j' = execute env1 c3 in subst1 c1 j' @@ -378,10 +378,10 @@ let infer_type env constr = execute_type env constr let check_ctxt env rels = fold_rel_context (fun d env -> match d with - (_,None,ty) -> + | LocalAssum (_,ty) -> let _ = infer_type env ty in push_rel d env - | (_,Some bd,ty) -> + | LocalDef (_,bd,ty) -> let j1 = infer env bd in let _ = infer env ty in conv_leq env j1 ty; @@ -399,9 +399,9 @@ let check_polymorphic_arity env params par = let pl = par.template_param_levels in let rec check_p env pl params = match pl, params with - Some u::pl, (na,None,ty)::params -> + Some u::pl, LocalAssum (na,ty)::params -> check_kind env ty u; - check_p (push_rel (na,None,ty) env) pl params + check_p (push_rel (LocalAssum (na,ty)) env) pl params | None::pl,d::params -> check_p (push_rel d env) pl params | [], _ -> () | _ -> failwith "check_poly: not the right number of params" in diff --git a/checker/typeops.mli b/checker/typeops.mli index 39d6604188..db8e467a33 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/univ.ml b/checker/univ.ml index 5fed6dcd5a..668f3a0584 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -14,7 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. @@ -33,7 +33,7 @@ module type Hashconsed = sig type t val hash : t -> int - val equal : t -> t -> bool + val eq : t -> t -> bool val hcons : t -> t end @@ -51,7 +51,7 @@ struct type t = _t type u = (M.t -> M.t) let hash = function Nil -> 0 | Cons (_, h, _) -> h - let equal l1 l2 = match l1, l2 with + let eq l1 l2 = match l1, l2 with | Nil, Nil -> true | Cons (x1, _, l1), Cons (x2, _, l2) -> x1 == x2 && l1 == l2 | _ -> false @@ -131,7 +131,7 @@ module HList = struct let rec remove x = function | Nil -> nil | Cons (y, _, l) -> - if H.equal x y then l + if H.eq x y then l else cons y (remove x l) end @@ -174,6 +174,16 @@ 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 @@ -211,31 +221,31 @@ module Level = struct let hash x = x.hash - let hcons x = - let data' = RawLevel.hcons x.data in - if data' == x.data then x - else { x with data = data' } - let data x = x.data (** Hashcons on levels + their hash *) - let make = - let module Self = struct - type _t = t - type t = _t - let equal = equal - let hash = hash - end in - let module WH = Weak.Make(Self) in - let pool = WH.create 4910 in fun x -> - let x = { hash = RawLevel.hash x; data = x } in - try WH.find pool x - with Not_found -> WH.add pool x; x + 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 set = make Set let prop = make Prop - + let var i = make (Var i) + let is_small x = match data x with | Level _ -> false @@ -272,8 +282,8 @@ module Level = struct end (** Level sets and maps *) -module LSet = Set.Make (Level) -module LMap = Map.Make (Level) +module LMap = HMap.Make (Level) +module LSet = LMap.Set type 'a universe_map = 'a LMap.t @@ -310,7 +320,7 @@ struct let hashcons hdir (b,n as x) = let b' = hdir b in if b' == b then x else (b',n) - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1,l2 with | (b,n), (b',n') -> b == b' && n == n' @@ -329,7 +339,7 @@ struct let hcons = Hashcons.simple_hcons H.generate H.hcons Level.hcons let hash = ExprHash.hash - let equal x y = x == y || + let eq x y = x == y || (let (u,n) = x and (v,n') = y in Int.equal n n' && Level.equal u v) @@ -550,20 +560,26 @@ let repr g u = in repr_rec u -(* [safe_repr] also search for the canonical representative, but - if the graph doesn't contain the searched universe, we add it. *) - -let safe_repr g u = - let rec safe_repr_rec u = - match UMap.find u g with - | Equiv v -> safe_repr_rec v - | Canonical arc -> arc - in - try g, safe_repr_rec u - with Not_found -> - let can = terminal u in - enter_arc can g, can +let get_set_arc g = repr g Level.set +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -730,8 +746,8 @@ let is_lt g arcu arcv = (** First, checks on universe levels *) let check_equal g u v = - let g, arcu = safe_repr g u in - let _, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in arcu == arcv let check_eq_level g u v = u == v || check_equal g u v @@ -740,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ let check_smaller g strict u v = - let g, arcu = safe_repr g u in - let g, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if strict then is_lt g arcu arcv else @@ -891,8 +907,8 @@ let error_inconsistency o u v = (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> error_inconsistency Eq v u @@ -907,8 +923,8 @@ let enforce_univ_eq u v g = (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if is_leq g arcu arcv then g else match fast_compare g arcv arcu with @@ -919,8 +935,8 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) let enforce_univ_lt u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastLT -> g | FastLE -> fst (setlt g arcu arcv) @@ -932,7 +948,10 @@ let enforce_univ_lt u v g = | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = + let g = enter_arc (terminal Level.set) UMap.empty in + let g = enter_arc (terminal Level.prop) g in + enforce_univ_lt Level.prop Level.set g (* Constraints and sets of constraints. *) @@ -961,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd) let empty_constraint = Constraint.empty let merge_constraints c g = Constraint.fold enforce_constraint c g - + type constraints = Constraint.t (** A value with universe constraints. *) @@ -1070,7 +1089,7 @@ struct a end - let equal t1 t2 = + let eq t1 t2 = t1 == t2 || (Int.equal (Array.length t1) (Array.length t2) && let rec aux i = @@ -1137,7 +1156,7 @@ struct (** Universe contexts (variables as a list) *) let empty = (Instance.empty, Constraint.empty) - + let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst end @@ -1149,6 +1168,8 @@ struct type t = LSet.t constrained let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst + let levels (ctx, _) = ctx + let make ctx cst = (ctx, cst) end type universe_context_set = ContextSet.t @@ -1198,6 +1219,9 @@ let subst_instance_constraints s csts = (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) @@ -1229,6 +1253,20 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst +let merge_context strict ctx g = + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and + constraints due to includes *) + (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + g (UContext.instance ctx) + in merge_constraints (UContext.constraints ctx) g + +let merge_context_set strict ctx g = + let g = LSet.fold + (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) + (ContextSet.levels ctx) g + in merge_constraints (ContextSet.constraints ctx) g + (** Pretty-printing *) let pr_arc = function diff --git a/checker/univ.mli b/checker/univ.mli index 742ef91aed..7d4c629ab9 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -74,6 +74,13 @@ 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. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq @@ -117,14 +124,14 @@ type univ_inconsistency = constraint_type * universe * universe exception UniverseInconsistency of univ_inconsistency val merge_constraints : constraints -> universes -> universes - + val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) -module LMap : Map.S with type key = universe_level - +module LMap : CSig.MapS with type key = universe_level +module LSet : CSig.SetS with type elt = universe_level type 'a universe_map = 'a LMap.t (** {6 Substitution} *) @@ -177,7 +184,7 @@ sig type t val empty : t - + val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints @@ -186,6 +193,7 @@ end module ContextSet : sig type t + val make : LSet.t -> constraints -> t val empty : t val constraints : t -> constraints end @@ -193,6 +201,9 @@ module ContextSet : type universe_context = UContext.t type universe_context_set = ContextSet.t +val merge_context : bool -> universe_context -> universes -> universes +val merge_context_set : bool -> universe_context_set -> universes -> universes + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool @@ -219,6 +230,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints 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 + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/checker/validate.ml b/checker/validate.ml index 63180f055e..c434ef09d3 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/values.ml b/checker/values.ml index 3ca44b7d0f..c175aed680 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 0fbea8efeae581d87d977faa9eb2f421 checker/cic.mli +MD5 6466d8cc443b5896cb905776df0cc49e checker/cic.mli *) @@ -126,6 +126,7 @@ let v_caseinfo = v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 4 +let v_proj = v_tuple "projection" [|v_cst; v_bool|] let rec v_constr = Sum ("constr",0,[| @@ -145,7 +146,7 @@ let rec v_constr = [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) - [|v_cst;v_constr|] (* Proj *) + [|v_proj;v_constr|] (* Proj *) |]) and v_prec = Tuple ("prec_declaration", @@ -153,8 +154,8 @@ and v_prec = Tuple ("prec_declaration", and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|]) and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|]) - -let v_rdecl = v_tuple "rel_declaration" [|v_name;Opt v_constr;v_constr|] +let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|]; (* LocalAssum *) + [|v_name; v_constr; v_constr|] |] (* LocalDef *) let v_rctxt = List v_rdecl let v_section_ctxt = v_enum "emptylist" 1 @@ -192,7 +193,8 @@ let v_lazy_constr = (** kernel/declarations *) -let v_engagement = v_enum "eng" 1 +let v_impredicative_set = v_enum "impr-set" 2 +let v_engagement = v_impredicative_set let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -205,8 +207,13 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_projbody = - v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|]; - v_constr|] + v_tuple "projection_body" + [|v_cst;Int;Int;v_constr; + v_tuple "proj_eta" [|v_constr;v_constr|]; + v_constr|] + +let v_typing_flags = + v_tuple "typing_flags" [|v_bool; v_bool|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -216,7 +223,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] @@ -265,12 +273,13 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_typing_flags|] let v_with = Sum ("with_declaration_body",0, [|[|List v_id;v_mp|]; - [|List v_id;v_constr|]|]) + [|List v_id;v_tuple "with_def" [|v_constr;v_context|]|]|]) let rec v_mae = Sum ("module_alg_expr",0, @@ -302,17 +311,17 @@ and v_impl = and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) (** kernel/safe_typing *) let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |]) let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|]) let v_compiled_lib = - v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|] + v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|] (** Library objects *) @@ -321,10 +330,40 @@ let v_libobj = Tuple ("libobj", [|v_id;v_obj|]) let v_libobjs = List v_libobj let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|]) +(** STM objects *) + +let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|]) +let v_states = v_pair Any v_frozen +let v_state = Tuple ("state", [|v_states; Any; v_bool|]) + +let v_vcs = + let data = Opt Any in + let vcs = + Tuple ("vcs", + [|Any; Any; + Tuple ("dag", + [|Any; Any; v_map Any (Tuple ("state_info", + [|Any; Any; Opt v_state; v_pair data Any|])) + |]) + |]) + in + let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in + vcs + +let v_uuid = Any +let v_request id doc = + Tuple ("request", [|Any; Any; doc; Any; id; String|]) +let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool) +let v_counters = Any +let v_stm_seg = v_pair v_tasks v_counters + (** Toplevel structures in a vo (see Cic.mli) *) +let v_libsum = + Tuple ("summary", [|v_dp;Array v_dp;v_deps|]) + let v_lib = - Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) + Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) let v_opaques = Array (v_computation v_constr) let v_univopaques = @@ -332,19 +371,19 @@ let v_univopaques = (** Registering dynamic values *) -module StringOrd = +module IntOrd = struct - type t = string + type t = int let compare (x : t) (y : t) = compare x y end -module StringMap = Map.Make(StringOrd) +module IntMap = Map.Make(IntOrd) -let dyn_table : value StringMap.t ref = ref StringMap.empty +let dyn_table : value IntMap.t ref = ref IntMap.empty let register_dyn name t = - dyn_table := StringMap.add name t !dyn_table + dyn_table := IntMap.add name t !dyn_table let find_dyn name = - try StringMap.find name !dyn_table + try IntMap.find name !dyn_table with Not_found -> Any diff --git a/checker/votour.ml b/checker/votour.ml index 29593cb719..48f9f45e7e 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,11 +10,128 @@ open Values (** {6 Interactive visit of a vo} *) -(** Name of a value *) +let rec read_num max = + let quit () = + Printf.printf "\nGoodbye!\n%!"; + exit 0 in + Printf.printf "# %!"; + let l = try read_line () with End_of_file -> quit () in + if l = "u" then None + else if l = "x" then quit () + else + try + let v = int_of_string l in + 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" -> + Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!"; + read_num max + +type 'a repr = +| INT of int +| STRING of string +| BLOCK of int * 'a array +| OTHER + +module type S = +sig + type obj + val input : in_channel -> obj + val repr : obj -> obj repr + val size : obj -> int + val oid : obj -> int option +end + +module ReprObj : S = +struct + type obj = Obj.t * int list + + let input chan = + let obj = input_value chan in + let () = CObj.register_shared_size obj in + (obj, []) + + let repr (obj, pos) = + if Obj.is_block obj then + let tag = Obj.tag obj in + if tag = Obj.string_tag then STRING (Obj.magic obj) + else if tag < Obj.no_scan_tag then + let init i = (Obj.field obj i, i :: pos) in + let data = Array.init (Obj.size obj) init in + BLOCK (tag, Obj.magic data) + else OTHER + else INT (Obj.magic obj) + + let size (_, p) = CObj.shared_size_of_pos p + let oid _ = None +end + +module ReprMem : S = +struct + open Analyze + + type obj = data + + let memory = ref [||] + let sizes = ref [||] + (** size, in words *) + + let ws = Sys.word_size / 8 + + let rec init_size seen = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> + if seen.(p) then 0 + else + let () = seen.(p) <- true in + match (!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 + | String s -> + let size = 2 + (String.length s / ws) in + let () = (!sizes).(p) <- size in + size + + let size = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> (!sizes).(p) + + let repr = function + | Int i -> INT i + | Atm t -> BLOCK (t, [||]) + | Fun _ -> OTHER + | Ptr p -> + match (!memory).(p) with + | Struct (tag, os) -> BLOCK (tag, os) + | String s -> STRING s -type dyn = { dyn_tag : string; dyn_obj : Obj.t; } + 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 + obj -let to_dyn obj = (Obj.magic obj : dyn) + let oid = function + | Int _ | Atm _ | Fun _ -> None + | Ptr p -> Some p +end + +module Visit (Repr : S) : +sig + val init : unit -> unit + val visit : Values.value -> Repr.obj -> int list -> unit +end = +struct + +(** Name of a value *) let rec get_name ?(extra=false) = function |Any -> "?" @@ -32,69 +149,105 @@ 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 *) -let get_string_in_tuple v o = +let get_string_in_tuple o = try - for i = 0 to Array.length v - 1 do - if v.(i) = String then - failwith (" [.."^(Obj.magic (Obj.field o i) : string)^"..]"); + for i = 0 to Array.length o - 1 do + match Repr.repr o.(i) with + | STRING s -> + failwith (Printf.sprintf " [..%s..]" s) + | _ -> () done; "" with Failure s -> s (** Some details : tags, integer value for non-block, etc etc *) -let rec get_details v o = match v with - |String | Any when (Obj.is_block o && Obj.tag o = Obj.string_tag) -> - " [" ^ String.escaped (Obj.magic o : string) ^"]" - |Tuple (_,v) -> get_string_in_tuple v o - |(Sum _|Any) when Obj.is_block o -> - " [tag=" ^ string_of_int (Obj.tag o) ^"]" - |(Sum _|Any) -> - " [imm=" ^ string_of_int (Obj.magic o : int) ^"]" - |Int -> " [" ^ string_of_int (Obj.magic o : int) ^"]" - |Annot (s,v) -> get_details v o +let rec get_details v o = match v, Repr.repr o with + | (String | Any), STRING s -> + Printf.sprintf " [%s]" (String.escaped s) + |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o + |(Sum _|Any), BLOCK (tag, _) -> + Printf.sprintf " [tag=%i]" tag + |(Sum _|Any), INT i -> + Printf.sprintf " [imm=%i]" i + |Int, INT i -> Printf.sprintf " [imm=%i]" i + |Annot (s,v), _ -> get_details v o |_ -> "" +let get_oid obj = match Repr.oid obj with +| None -> "" +| Some id -> Printf.sprintf " [0x%08x]" id + let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (CObj.shared_size_of_pos p)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) -let access_children vs o pos = - Array.mapi (fun i v -> v, Obj.field o i, i::pos) vs +let access_children vs os pos = + if Array.length os = Array.length vs then + Array.mapi (fun i v -> v, os.(i), i::pos) vs + else raise Exit +let access_list v o pos = + let rec loop o pos = match Repr.repr o with + | INT 0 -> [] + | BLOCK (0, [|hd; tl|]) -> + (v, hd, 0 :: pos) :: loop tl (1 :: pos) + | _ -> raise Exit + in + 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 *) let rec get_children v o pos = match v with - |Tuple (_,v) -> access_children v o pos - |Sum (_,_,vv) -> - if Obj.is_block o then access_children vv.(Obj.tag o) o pos - else [||] - |Array v -> access_children (Array.make (Obj.size o) v) o pos - |List v -> - let rec loop pos = function - | [] -> [] - | o :: ol -> (v,o,0::pos) :: loop (1::pos) ol - in - Array.of_list (loop pos (Obj.magic o : Obj.t list)) + |Tuple (_, v) -> + let (_, os) = access_block o in + access_children v os pos + |Sum (_, _, vv) -> + begin match Repr.repr o with + | BLOCK (tag, os) -> access_children vv.(tag) os pos + | INT _ -> [||] + | _ -> raise Exit + end + |Array v -> + let (_, os) = access_block o in + access_children (Array.make (Array.length os) v) os pos + |List v -> access_list v o pos |Opt v -> - if Obj.is_block o then [|v,Obj.field o 0,0::pos|] else [||] + begin match Repr.repr o with + | INT 0 -> [||] + | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|] + | _ -> raise Exit + end |String | Int -> [||] |Annot (s,v) -> get_children v o pos - |Any -> - if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then - Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos)) - else [||] + |Any -> raise Exit |Dyn -> - let t = to_dyn o in - let tpe = find_dyn t.dyn_tag in - [|(String, Obj.repr t.dyn_tag, 0 :: pos); (tpe, t.dyn_obj, 1 :: pos)|] + begin match Repr.repr o with + | BLOCK (0, [|id; o|]) -> + let n = access_int id in + let tpe = find_dyn n in + [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|] + | _ -> raise Exit + end |Fail s -> failwith "forbidden" +let get_children v o pos = + try get_children v o pos + with Exit -> match Repr.repr o with + | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os + | _ -> [||] + type info = { nam : string; typ : value; - obj : Obj.t; + obj : Repr.obj; pos : int list } @@ -122,28 +275,61 @@ let rec visit v o pos = (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop)) children; Printf.printf "-------------\n"; - Printf.printf ("# %!"); - let l = read_line () in try - if l = "u" then let info = pop () in visit info.typ info.obj info.pos - else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0) - else - let v',o',pos' = children.(int_of_string l) in - push (get_name v) v o pos; - visit v' o' pos' + match read_num (Array.length children) with + | None -> let info = pop () in visit info.typ info.obj info.pos + | Some child -> + let v',o',pos' = children.(child) in + 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 | Failure _ | Invalid_argument _ -> visit v o pos +end + (** Loading the vo *) +type header = { + magic : string; + (** Magic number of the marshaller *) + length : int; + (** Size on disk in bytes *) + size32 : int; + (** Size in words when loaded on 32-bit systems *) + size64 : int; + (** Size in words when loaded on 64-bit systems *) + objects : int; + (** Number of blocks defined in the marshalled structure *) +} + +let dummy_header = { + magic = "\000\000\000\000"; + length = 0; + size32 = 0; + size64 = 0; + objects = 0; +} + +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 length = input_binary_int chan in + let objects = input_binary_int chan in + let size32 = input_binary_int chan in + let size64 = input_binary_int chan in + { magic; length; size32; size64; objects } + type segment = { name : string; mutable pos : int; typ : Values.value; + mutable header : header; } +let make_seg name typ = { name; typ; pos = 0; header = dummy_header } + let visit_vo f = Printf.printf "\nWelcome to votour !\n"; Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n"; @@ -151,12 +337,19 @@ let visit_vo f = Printf.printf "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!"; let segments = [| - {name="library"; pos=0; typ=Values.v_lib}; - {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; - {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Any}; - {name="opaque proofs"; pos=0; typ=Values.v_opaques}; + make_seg "summary" Values.v_libsum; + make_seg "library" Values.v_lib; + make_seg "univ constraints of opaque proofs" Values.v_univopaques; + make_seg "discharging info" (Opt Any); + make_seg "STM tasks" (Opt Values.v_stm_seg); + make_seg "opaque proofs" Values.v_opaques; |] in + let repr = + if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) + (** On 32-bit machines, representation may exceed the max size of arrays *) + in + let module Repr = (val repr : S) in + let module Visit = Visit(Repr) in while true do let ch = open_in_bin f in let magic = input_binary_int ch in @@ -164,22 +357,24 @@ let visit_vo f = for i=0 to Array.length segments - 1 do let pos = input_binary_int ch in segments.(i).pos <- pos_in ch; + let header = parse_header ch in + segments.(i).header <- header; seek_in ch pos; ignore(Digest.input ch); done; Printf.printf "The file has %d segments, choose the one to visit:\n" (Array.length segments); - Array.iteri (fun i { name; pos } -> - Printf.printf " %d: %s, starting at byte %d\n" i name pos) + Array.iteri (fun i { name; pos; header } -> + let size = if Sys.word_size = 64 then header.size64 else header.size32 in + Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size) segments; - Printf.printf "# %!"; - let l = read_line () in - let seg = int_of_string l in - seek_in ch segments.(seg).pos; - let o = (input_value ch : Obj.t) in - let () = CObj.register_shared_size o in - let () = init () in - visit segments.(seg).typ o [] + match read_num (Array.length segments) with + | Some seg -> + seek_in ch segments.(seg).pos; + let o = Repr.input ch in + let () = Visit.init () in + Visit.visit segments.(seg).typ o [] + | None -> () done let main = |