package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/src/coq-core.kernel/vmlambda.ml.html
Source file vmlambda.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
open Util open Declarations open Genlambda open Vmvalues type lval = int * structured_values (* keep the hash *) type lambda = lval Genlambda.lambda let get_lval (_, v) = v (** Simplification of lambda expression *) (*s Translation from [constr] to [lambda] *) (* Translation of constructor *) let is_value lc = match lc with | Lval _ | Lint _ | Luint _ | Lfloat _ -> true | _ -> false let get_value lc = match lc with | Luint i -> val_of_uint i | Lval (_, v) -> v | Lint i -> val_of_int i | Lfloat f -> val_of_float f | _ -> assert false let hash_block tag args = let open Hashset.Combine in let fold accu v = let h = match v with | Luint i -> Uint63.hash i | Lint i -> Hashtbl.hash (i : int) | Lfloat f -> Float64.hash f | Lval (h, _) -> h | _ -> assert false in combine accu h in combine tag (Array.fold_left fold 0 args) module HashBlock = struct type t = int * structured_values array * structured_values (* tag, block, value *) let eq (tag1, args1, _) (tag2, args2, _) = Int.equal tag1 tag2 && CArray.equal (==) args1 args2 end module HashsetBlock = Hashset.Make(HashBlock) let block_table = HashsetBlock.create 97 let as_value tag args = if Array.for_all is_value args then let h = hash_block tag args in (* Don't simplify this to Array.map because of flat float arrays *) let args = let dummy_val = Obj.magic 0 in let ans = Array.make (Array.length args) dummy_val in let () = Array.iteri (fun i v -> ans.(i) <- get_value v) args in ans in if tag < Obj.last_non_constant_constructor_tag then let block = val_of_block tag args in let (_, _, block) = HashsetBlock.repr h (tag, args, block) block_table in Some (h, block) else let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in let block = val_of_block Obj.last_non_constant_constructor_tag args in let (_, _, block) = HashsetBlock.repr h (tag, args, block) block_table in Some (h, block) else None module Val = struct type value = int * structured_values let as_value = as_value let check_inductive (_, i) mb = let { mind_typename=name; mind_nb_args; mind_nb_constant; _ } = mb.mind_packets.(i) in Vmerrors.check_compilable_ind ~name ~mind_nb_args ~mind_nb_constant end module Lambda = Genlambda.Make(Val) (*********************************) let dump_lambda = ref false let lambda_of_constr env sigma c = let lam = Lambda.lambda_of_constr env sigma c in let lam = optimize lam in if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>