Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \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) *)(************************************************************************)
(* Note: don't forget to update v_primitive in checker/values.ml if the *)(* number of primitives is changed. *)
open Univopen UVars
type t = | Int63head0 | Int63tail0 | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl | Int63div21 | Int63addMulDiv | Int63eq | Int63lt | Int63le | Int63lts | Int63les | Int63compare | Int63compares | Float64opp | Float64abs | Float64eq | Float64lt | Float64le | Float64compare | Float64equal | Float64classify | Float64add | Float64sub | Float64mul | Float64div | Float64sqrt | Float64ofUint63 | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp | Float64next_up | Float64next_down | Arraymake | Arrayget | Arraydefault | Arrayset | Arraycopy | Arraylength | Stringmake | Stringlength | Stringget | Stringsub | Stringcat | Stringcompare
let parse = function | "int63_head0" -> Int63head0 | "int63_tail0" -> Int63tail0 | "int63_add" -> Int63add | "int63_sub" -> Int63sub | "int63_mul" -> Int63mul | "int63_div" -> Int63div | "int63_mod" -> Int63mod | "int63_divs" -> Int63divs | "int63_mods" -> Int63mods | "int63_lsr" -> Int63lsr | "int63_lsl" -> Int63lsl | "int63_asr" -> Int63asr | "int63_land" -> Int63land | "int63_lor" -> Int63lor | "int63_lxor" -> Int63lxor | "int63_addc" -> Int63addc | "int63_subc" -> Int63subc | "int63_addcarryc" -> Int63addCarryC | "int63_subcarryc" -> Int63subCarryC | "int63_mulc" -> Int63mulc | "int63_diveucl" -> Int63diveucl | "int63_div21" -> Int63div21 | "int63_addmuldiv" -> Int63addMulDiv | "int63_eq" -> Int63eq | "int63_lt" -> Int63lt | "int63_le" -> Int63le | "int63_lts" -> Int63lts | "int63_les" -> Int63les | "int63_compare" -> Int63compare | "int63_compares" -> Int63compares | "float64_opp" -> Float64opp | "float64_abs" -> Float64abs | "float64_eq" -> Float64eq | "float64_lt" -> Float64lt | "float64_le" -> Float64le | "float64_compare" -> Float64compare | "float64_equal" -> Float64equal | "float64_classify" -> Float64classify | "float64_add" -> Float64add | "float64_sub" -> Float64sub | "float64_mul" -> Float64mul | "float64_div" -> Float64div | "float64_sqrt" -> Float64sqrt | "float64_of_uint63" -> Float64ofUint63 | "float64_normfr_mantissa" -> Float64normfr_mantissa | "float64_frshiftexp" -> Float64frshiftexp | "float64_ldshiftexp" -> Float64ldshiftexp | "float64_next_up" -> Float64next_up | "float64_next_down" -> Float64next_down | "array_make" -> Arraymake | "array_get" -> Arrayget | "array_default" -> Arraydefault | "array_set" -> Arrayset | "array_length" -> Arraylength | "array_copy" -> Arraycopy | "string_make" -> Stringmake | "string_length" -> Stringlength | "string_get" -> Stringget | "string_sub" -> Stringsub | "string_cat" -> Stringcat | "string_compare" -> Stringcompare | _ -> raise Not_found
let equal (p1 : t) (p2 : t) = p1 == p2
let hash = function | Int63head0 -> 1 | Int63tail0 -> 2 | Int63add -> 3 | Int63sub -> 4 | Int63mul -> 5 | Int63div -> 6 | Int63mod -> 7 | Int63lsr -> 8 | Int63lsl -> 9 | Int63land -> 10 | Int63lor -> 11 | Int63lxor -> 12 | Int63addc -> 13 | Int63subc -> 14 | Int63addCarryC -> 15 | Int63subCarryC -> 16 | Int63mulc -> 17 | Int63diveucl -> 18 | Int63div21 -> 19 | Int63addMulDiv -> 20 | Int63eq -> 21 | Int63lt -> 22 | Int63le -> 23 | Int63compare -> 24 | Float64opp -> 25 | Float64abs -> 26 | Float64compare -> 27 | Float64classify -> 28 | Float64add -> 29 | Float64sub -> 30 | Float64mul -> 31 | Float64div -> 32 | Float64sqrt -> 33 | Float64ofUint63 -> 34 | Float64normfr_mantissa -> 35 | Float64frshiftexp -> 36 | Float64ldshiftexp -> 37 | Float64next_up -> 38 | Float64next_down -> 39 | Float64eq -> 40 | Float64lt -> 41 | Float64le -> 42 | Arraymake -> 43 | Arrayget -> 44 | Arraydefault -> 45 | Arrayset -> 46 | Arraycopy -> 47 | Arraylength -> 48 | Int63lts -> 49 | Int63les -> 50 | Int63divs -> 51 | Int63mods -> 52 | Int63asr -> 53 | Int63compares -> 54 | Float64equal -> 55 | Stringmake -> 56 | Stringlength -> 57 | Stringget -> 58 | Stringsub -> 59 | Stringcat -> 60 | Stringcompare -> 61
(* Should match names in nativevalues.ml *)let to_string = function | Int63head0 -> "head0" | Int63tail0 -> "tail0" | Int63add -> "add" | Int63sub -> "sub" | Int63mul -> "mul" | Int63div -> "div" | Int63mod -> "rem" | Int63divs -> "divs" | Int63mods -> "rems" | Int63lsr -> "l_sr" | Int63lsl -> "l_sl" | Int63asr -> "a_sr" | Int63land -> "l_and" | Int63lor -> "l_or" | Int63lxor -> "l_xor" | Int63addc -> "addc" | Int63subc -> "subc" | Int63addCarryC -> "addCarryC" | Int63subCarryC -> "subCarryC" | Int63mulc -> "mulc" | Int63diveucl -> "diveucl" | Int63div21 -> "div21" | Int63addMulDiv -> "addMulDiv" | Int63eq -> "eq" | Int63lt -> "lt" | Int63le -> "le" | Int63lts -> "lts" | Int63les -> "les" | Int63compare -> "compare" | Int63compares -> "compares" | Float64opp -> "fopp" | Float64abs -> "fabs" | Float64eq -> "feq" | Float64lt -> "flt" | Float64le -> "fle" | Float64compare -> "fcompare" | Float64equal -> "fequal" | Float64classify -> "fclassify" | Float64add -> "fadd" | Float64sub -> "fsub" | Float64mul -> "fmul" | Float64div -> "fdiv" | Float64sqrt -> "fsqrt" | Float64ofUint63 -> "float_of_int" | Float64normfr_mantissa -> "normfr_mantissa" | Float64frshiftexp -> "frshiftexp" | Float64ldshiftexp -> "ldshiftexp" | Float64next_up -> "next_up" | Float64next_down -> "next_down" | Arraymake -> "arraymake" | Arrayget -> "arrayget" | Arraydefault -> "arraydefault" | Arrayset -> "arrayset" | Arraycopy -> "arraycopy" | Arraylength -> "arraylength" | Stringmake -> "string_make" | Stringlength -> "string_length" | Stringget -> "string_get" | Stringsub -> "string_sub" | Stringcat -> "string_cat" | Stringcompare -> "string_compare"
type const = | Arraymaxlength | Stringmaxlength
let const_to_string = function | Arraymaxlength -> "arraymaxlength" | Stringmaxlength -> "stringmaxlength"
let const_of_string = function | "array_max_length" -> Arraymaxlength | "string_max_length" -> Stringmaxlength | _ -> raise Not_found
let const_univs = function | Arraymaxlength | Stringmaxlength -> AbstractContext.empty
type 'a prim_type = | PT_int63 : unit prim_type | PT_float64 : unit prim_type | PT_string : unit prim_type | PT_array : (Instance.t * ind_or_type) prim_type
and 'a prim_ind = | PIT_bool : unit prim_ind | PIT_carry : ind_or_type prim_ind | PIT_pair : (ind_or_type * ind_or_type) prim_ind | PIT_cmp : unit prim_ind | PIT_f_cmp : unit prim_ind | PIT_f_class : unit prim_ind
and ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type | PITT_type : 'a prim_type * 'a -> ind_or_type | PITT_param : int -> ind_or_type (* DeBruijn index referring to prenex type quantifiers *)
let one_univ = AbstractContext.make { quals = [||]; univs = Names.[|Name (Id.of_string "u")|]} PConstraints.empty
let typ_univs (type a) (t : a prim_type) = match t with | PT_int63 -> AbstractContext.empty | PT_float64 -> AbstractContext.empty | PT_string -> AbstractContext.empty | PT_array -> one_univ
type prim_type_ex = PTE : 'a prim_type -> prim_type_ex
type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex
let types = let int_ty = PITT_type (PT_int63, ()) in let float_ty = PITT_type (PT_float64, ()) in let string_ty = PITT_type (PT_string, ()) in let array_ty = PITT_type (PT_array, (Instance.of_array ([||],[|Level.var 0|]), PITT_param 1)) in function | Int63head0 | Int63tail0 -> [int_ty], int_ty | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty], int_ty | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> [int_ty; int_ty], PITT_ind (PIT_carry, int_ty) | Int63mulc | Int63diveucl -> [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty], PITT_ind (PIT_bool, ()) | Int63compare | Int63compares -> [int_ty; int_ty], PITT_ind (PIT_cmp, ()) | Int63div21 -> [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) | Int63addMulDiv -> [int_ty; int_ty; int_ty], int_ty | Float64opp | Float64abs | Float64sqrt | Float64next_up | Float64next_down -> [float_ty], float_ty | Float64ofUint63 -> [int_ty], float_ty | Float64normfr_mantissa -> [float_ty], int_ty | Float64frshiftexp -> [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty)) | Float64eq | Float64lt | Float64le | Float64equal -> [float_ty; float_ty], PITT_ind (PIT_bool, ()) | Float64compare -> [float_ty; float_ty], PITT_ind (PIT_f_cmp, ()) | Float64classify -> [float_ty], PITT_ind (PIT_f_class, ()) | Float64add | Float64sub | Float64mul | Float64div -> [float_ty; float_ty], float_ty | Float64ldshiftexp -> [float_ty; int_ty], float_ty | Arraymake -> [int_ty; PITT_param 1], array_ty | Arrayget -> [array_ty; int_ty], PITT_param 1 | Arraydefault -> [array_ty], PITT_param 1 | Arrayset -> [array_ty; int_ty; PITT_param 1], array_ty | Arraycopy -> [array_ty], array_ty | Arraylength -> [array_ty], int_ty | Stringmake -> [int_ty; int_ty], string_ty | Stringlength -> [string_ty], int_ty | Stringget -> [string_ty; int_ty], int_ty | Stringsub -> [string_ty; int_ty; int_ty], string_ty | Stringcat -> [string_ty; string_ty], string_ty | Stringcompare -> [string_ty; string_ty], PITT_ind (PIT_cmp, ())
let one_param = (* currently if there's a parameter it's always this *) let a_annot = Context.nameR (Names.Id.of_string "A") in let ty = Constr.mkType (Universe.make (Level.var 0)) in Context.Rel.Declaration.[LocalAssum (a_annot, ty)]
let params = function | Int63head0 | Int63tail0 | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl | Int63div21 | Int63addMulDiv | Int63eq | Int63lt | Int63le | Int63lts | Int63les | Int63compare | Int63compares | Float64opp | Float64abs | Float64eq | Float64lt | Float64le | Float64compare | Float64equal | Float64classify | Float64add | Float64sub | Float64mul | Float64div | Float64sqrt | Float64ofUint63 | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp | Float64next_up | Float64next_down | Stringmake | Stringlength | Stringget | Stringsub | Stringcat | Stringcompare -> []
| Arraymake | Arrayget | Arraydefault | Arrayset | Arraycopy | Arraylength -> one_param
let nparams x = List.length (params x)
let univs = function | Int63head0 | Int63tail0 | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC | Int63mulc | Int63diveucl | Int63div21 | Int63addMulDiv | Int63eq | Int63lt | Int63le | Int63lts | Int63les | Int63compare | Int63compares | Float64opp | Float64abs | Float64eq | Float64lt | Float64le | Float64compare | Float64equal | Float64classify | Float64add | Float64sub | Float64mul | Float64div | Float64sqrt | Float64ofUint63 | Float64normfr_mantissa | Float64frshiftexp | Float64ldshiftexp | Float64next_up | Float64next_down | Stringmake | Stringlength | Stringget | Stringsub | Stringcat | Stringcompare -> AbstractContext.empty
| Arraymake | Arrayget | Arraydefault | Arrayset | Arraycopy | Arraylength -> one_univ
type arg_kind = | Kparam (* not needed for the evaluation of the primitive when it reduces *) | Kwhnf (* need to be reduced in whnf before reducing the primitive *) | Karg (* no need to be reduced in whnf. example: [v] in [Array.set t i v] *)
type args_red = arg_kind list
(* Invariant only argument of type int63, float or an inductive can have kind Kwhnf *)
let arity t = nparams t + List.length (fst (types t))
let kind t = let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in params (nparams t) @ List.map args (fst (types t))
let types t = let args_ty, ret_ty = types t in params t, args_ty, ret_ty
(** Special Entries for Register **)
type op_or_type = | OT_op of t | OT_type : 'a prim_type -> op_or_type | OT_const of const
let prim_ind_to_string (type a) (p : a prim_ind) = match p with | PIT_bool -> "bool" | PIT_carry -> "carry" | PIT_pair -> "pair" | PIT_cmp -> "cmp" | PIT_f_cmp -> "f_cmp" | PIT_f_class -> "f_class"
let prim_type_to_string (type a) (ty : a prim_type) = match ty with | PT_int63 -> "int63_type" | PT_float64 -> "float64_type" | PT_string -> "string_type" | PT_array -> "array_type"
let op_or_type_to_string = function | OT_op op -> to_string op | OT_type t -> prim_type_to_string t | OT_const c -> const_to_string c
let prim_type_of_string = function | "int63_type" -> PTE PT_int63 | "float64_type" -> PTE PT_float64 | "string_type" -> PTE PT_string | "array_type" -> PTE PT_array | _ -> raise Not_found
let op_or_type_of_string s = match prim_type_of_string s with | PTE ty -> OT_type ty | exception Not_found -> begin try OT_op (parse s) with Not_found -> OT_const (const_of_string s) end
let parse_op_or_type ?loc s = try op_or_type_of_string s with Not_found -> CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist."))
let op_or_type_univs = function | OT_op t -> univs t | OT_type t -> typ_univs t | OT_const c -> const_univs c
let body_of_prim_const = function | Arraymaxlength -> Constr.mkInt (Parray.max_length) | Stringmaxlength -> Constr.mkInt (Pstring.max_length)