diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_instruct.h | 67 | ||||
| -rw-r--r-- | kernel/byterun/dune | 7 | ||||
| -rwxr-xr-x | kernel/byterun/make_jumptbl.sh | 3 | ||||
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 7 | ||||
| -rw-r--r-- | kernel/dune | 9 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 193 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 6 | ||||
| -rw-r--r-- | kernel/inductive.ml | 10 | ||||
| -rw-r--r-- | kernel/inductive.mli | 2 | ||||
| -rw-r--r-- | kernel/make-opcodes | 3 | ||||
| -rwxr-xr-x | kernel/make_opcodes.sh | 4 | ||||
| -rw-r--r-- | kernel/write_uint63.ml | 12 |
13 files changed, 231 insertions, 94 deletions
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h deleted file mode 100644 index c7abedaed6..0000000000 --- a/kernel/byterun/coq_instruct.h +++ /dev/null @@ -1,67 +0,0 @@ -/***********************************************************************/ -/* */ -/* Coq Compiler */ -/* */ -/* Benjamin Gregoire, projets Logical and Cristal */ -/* INRIA Rocquencourt */ -/* */ -/* */ -/***********************************************************************/ - -#ifndef _COQ_INSTRUCT_ -#define _COQ_INSTRUCT_ - -/* Nota: this list of instructions is parsed to produce derived files */ -/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ -/* and alone on lines starting by two spaces. */ -/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ -/* with the arity of the instruction and maybe coq_tcode_of_code. */ - -enum instructions { - ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, - PUSH, - PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4, - PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, - POP, - ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC, - PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC, - PUSH_RETADDR, - APPLY, APPLY1, APPLY2, APPLY3, APPLY4, - APPTERM, APPTERM1, APPTERM2, APPTERM3, - RETURN, RESTART, GRAB, GRABREC, - CLOSURE, CLOSUREREC, CLOSURECOFIX, - OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE, - PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, - PUSHOFFSETCLOSURE, - GETGLOBAL, PUSHGETGLOBAL, - MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4, - SWITCH, PUSHFIELDS, - GETFIELD0, GETFIELD1, GETFIELD, - SETFIELD0, SETFIELD1, SETFIELD, - PROJ, - ENSURESTACKCAPACITY, - CONST0, CONST1, CONST2, CONST3, CONSTINT, - PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, - ACCUMULATE, - MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, -/* spiwack: */ - BRANCH, - CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63, - CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63, - CHECKMULINT63, CHECKMULCINT63, - CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63, - CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63, - CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63, - CHECKLSLINT63CONST1, CHECKLSRINT63CONST1, - - CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63, - CHECKCOMPAREINT63, - - CHECKHEAD0INT63, CHECKTAIL0INT63, - - ISINT, AREINT2, - - STOP -}; - -#endif /* _COQ_INSTRUCT_ */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index c3c44670be..20bdf28e54 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -5,6 +5,9 @@ (c_names coq_fix_code coq_memory coq_values coq_interp)) (rule + (targets coq_instruct.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) + +(rule (targets coq_jumptbl.h) - (deps (:h-file coq_instruct.h) make_jumptbl.sh) - (action (bash "./make_jumptbl.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) diff --git a/kernel/byterun/make_jumptbl.sh b/kernel/byterun/make_jumptbl.sh deleted file mode 100755 index eacd4daac8..0000000000 --- a/kernel/byterun/make_jumptbl.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/usr/bin/env bash - -sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' -e '/^}/q' ${1} > ${2} diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6777e0c223..567850645e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -166,7 +166,7 @@ type one_inductive_body = { mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) - mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) + mind_nf_lc : (rel_context * types) array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) mind_consnrealargs : int array; (** Number of expected proper arguments of the constructors (w/o params) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9e0230c3ba..d56502a095 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -214,7 +214,7 @@ let subst_mind_packet sub mbp = mind_consnrealdecls = mbp.mind_consnrealdecls; mind_consnrealargs = mbp.mind_consnrealargs; mind_typename = mbp.mind_typename; - mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.Smart.map (fun (ctx, c) -> Context.Rel.map (subst_mps sub) ctx, subst_mps sub c) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc; @@ -299,9 +299,8 @@ let hcons_ind_arity = let hcons_mind_packet oib = let user = Array.Smart.map Constr.hcons oib.mind_user_lc in - let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in - (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) - let nf = if Array.equal (==) user nf then user else nf in + let map (ctx, c) = Context.Rel.map Constr.hcons ctx, Constr.hcons c in + let nf = Array.Smart.map map oib.mind_nf_lc in { oib with mind_typename = Names.Id.hcons oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; diff --git a/kernel/dune b/kernel/dune index 1f2d696a36..a8a87a3e95 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,13 +3,16 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ uint63_x86 uint63_amd64 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_x86 uint63_amd64 write_uint63)) (libraries lib byterun)) +(executable + (name genOpcodeFiles) + (modules genOpcodeFiles)) + (rule (targets copcodes.ml) - (deps (:h-file byterun/coq_instruct.h) make-opcodes make_opcodes.sh) - (action (bash "./make_opcodes.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml)))) (executable (name write_uint63) diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml new file mode 100644 index 0000000000..6564954dfd --- /dev/null +++ b/kernel/genOpcodeFiles.ml @@ -0,0 +1,193 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** List of opcodes. + + It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and + [copcodes.ml] files. + + If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c + with the arity of the instruction and maybe coq_tcode_of_code. +*) +let opcodes = + [| + "ACC0"; + "ACC1"; + "ACC2"; + "ACC3"; + "ACC4"; + "ACC5"; + "ACC6"; + "ACC7"; + "ACC"; + "PUSH"; + "PUSHACC0"; + "PUSHACC1"; + "PUSHACC2"; + "PUSHACC3"; + "PUSHACC4"; + "PUSHACC5"; + "PUSHACC6"; + "PUSHACC7"; + "PUSHACC"; + "POP"; + "ENVACC1"; + "ENVACC2"; + "ENVACC3"; + "ENVACC4"; + "ENVACC"; + "PUSHENVACC1"; + "PUSHENVACC2"; + "PUSHENVACC3"; + "PUSHENVACC4"; + "PUSHENVACC"; + "PUSH_RETADDR"; + "APPLY"; + "APPLY1"; + "APPLY2"; + "APPLY3"; + "APPLY4"; + "APPTERM"; + "APPTERM1"; + "APPTERM2"; + "APPTERM3"; + "RETURN"; + "RESTART"; + "GRAB"; + "GRABREC"; + "CLOSURE"; + "CLOSUREREC"; + "CLOSURECOFIX"; + "OFFSETCLOSUREM2"; + "OFFSETCLOSURE0"; + "OFFSETCLOSURE2"; + "OFFSETCLOSURE"; + "PUSHOFFSETCLOSUREM2"; + "PUSHOFFSETCLOSURE0"; + "PUSHOFFSETCLOSURE2"; + "PUSHOFFSETCLOSURE"; + "GETGLOBAL"; + "PUSHGETGLOBAL"; + "MAKEBLOCK"; + "MAKEBLOCK1"; + "MAKEBLOCK2"; + "MAKEBLOCK3"; + "MAKEBLOCK4"; + "SWITCH"; + "PUSHFIELDS"; + "GETFIELD0"; + "GETFIELD1"; + "GETFIELD"; + "SETFIELD0"; + "SETFIELD1"; + "SETFIELD"; + "PROJ"; + "ENSURESTACKCAPACITY"; + "CONST0"; + "CONST1"; + "CONST2"; + "CONST3"; + "CONSTINT"; + "PUSHCONST0"; + "PUSHCONST1"; + "PUSHCONST2"; + "PUSHCONST3"; + "PUSHCONSTINT"; + "ACCUMULATE"; + "MAKESWITCHBLOCK"; + "MAKEACCU"; + "MAKEPROD"; + "BRANCH"; + "CHECKADDINT63"; + "ADDINT63"; + "CHECKADDCINT63"; + "CHECKADDCARRYCINT63"; + "CHECKSUBINT63"; + "SUBINT63"; + "CHECKSUBCINT63"; + "CHECKSUBCARRYCINT63"; + "CHECKMULINT63"; + "CHECKMULCINT63"; + "CHECKDIVINT63"; + "CHECKMODINT63"; + "CHECKDIVEUCLINT63"; + "CHECKDIV21INT63"; + "CHECKLXORINT63"; + "CHECKLORINT63"; + "CHECKLANDINT63"; + "CHECKLSLINT63"; + "CHECKLSRINT63"; + "CHECKADDMULDIVINT63"; + "CHECKLSLINT63CONST1"; + "CHECKLSRINT63CONST1"; + "CHECKEQINT63"; + "CHECKLTINT63"; + "LTINT63"; + "CHECKLEINT63"; + "LEINT63"; + "CHECKCOMPAREINT63"; + "CHECKHEAD0INT63"; + "CHECKTAIL0INT63"; + "ISINT"; + "AREINT2"; + "STOP" + |] + +let pp_c_comment fmt = + Format.fprintf fmt "/* %a */" + +let pp_ocaml_comment fmt = + Format.fprintf fmt "(* %a *)" + +let pp_header isOcaml fmt = + Format.fprintf fmt "%a" + (fun fmt -> + (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt + Format.pp_print_string) + "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml" + +let pp_with_commas fmt k = + Array.iteri (fun n s -> + Format.fprintf fmt " %a%s@." + k s + (if n + 1 < Array.length opcodes + then "," else "") + ) opcodes + +let pp_coq_instruct_h fmt = + let line = Format.fprintf fmt "%s@." in + pp_header false fmt; + line "#pragma once"; + line "enum instructions {"; + pp_with_commas fmt Format.pp_print_string; + line "};" + +let pp_coq_jumptbl_h fmt = + pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") + +let pp_copcodes_ml fmt = + pp_header true fmt; + Array.iteri (fun n s -> + Format.fprintf fmt "let op%s = %d@.@." s n + ) opcodes + +let usage () = + Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0); + exit 1 + +let main () = + match Sys.argv.(1) with + | "enum" -> pp_coq_instruct_h Format.std_formatter + | "jump" -> pp_coq_jumptbl_h Format.std_formatter + | "copml" -> pp_copcodes_ml Format.std_formatter + | _ -> usage () + | exception Invalid_argument _ -> usage () + +let () = main () diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8f06e1e4b8..457c17907e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -416,7 +416,9 @@ let compute_projections (kn, i as ind) mib = let pkt = mib.mind_packets.(i) in let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in + let (ctx, cty) = pkt.mind_nf_lc.(0) in + let cty = it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (substl subst cty) in let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not @@ -475,7 +477,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite (* Check one inductive *) let build_one_packet (id,cnames) ((arity,lc),(indices,splayed_lc),kelim) recarg = (* Type of constructors in normal form *) - let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b (d@paramsctxt)) splayed_lc in + let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in let consnrealdecls = Array.map (fun (d,_) -> Context.Rel.length d) splayed_lc in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 848ae65c51..f4c2483c14 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -251,7 +251,11 @@ let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - Array.map (constructor_instantiate kn u mib) specif + let map (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in + constructor_instantiate kn u mib cty + in + Array.map map specif let arities_of_constructors ind specif = arities_of_specif (fst (fst ind), snd ind) specif @@ -342,7 +346,8 @@ let is_correct_arity env c pj ind specif params = (* [p] is the predicate, [i] is the constructor number (starting from 0), and [cty] is the type of the constructor (params not instantiated) *) let build_branches_type (ind,u) (_,mip as specif) params p = - let build_one_branch i cty = + let build_one_branch i (ctx, c) = + let cty = Term.it_mkProd_or_LetIn c ctx in let typi = full_constructor_instantiate (ind,u,specif,params) cty in let (cstrsign,ccl) = Term.decompose_prod_assum typi in let nargs = Context.Rel.length cstrsign in @@ -597,6 +602,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc ntyps npars lc = + let lc = Array.map (fun (ctx, c) -> Term.it_mkProd_or_LetIn c ctx) lc in if Int.equal npars 0 then lc else diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 3c1464c6c9..ad35c16c22 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> constr array -> constr array +val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array diff --git a/kernel/make-opcodes b/kernel/make-opcodes deleted file mode 100644 index e1371b3d0c..0000000000 --- a/kernel/make-opcodes +++ /dev/null @@ -1,3 +0,0 @@ -$1=="enum" {n=0; next; } - {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); - for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/make_opcodes.sh b/kernel/make_opcodes.sh deleted file mode 100755 index bb8aba2f07..0000000000 --- a/kernel/make_opcodes.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash - -script_dir="$(dirname "$0")" -tr -d "\r" < "${1}" | sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' | awk -f "$script_dir"/make-opcodes > "${2}" diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml index 0fcaf4f10a..beb59ce205 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.ml @@ -1,10 +1,18 @@ -(** Equivalent of rm -f *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(** Equivalent of rm -f *) let safe_remove f = try Unix.chmod f 0o644; Sys.remove f with _ -> () (** * Generate an implementation of 63-bit arithmetic *) - let ml_file_copy input output = safe_remove output; let i = open_in input in |