package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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
open Util open Esubst open Declarations open Genlambda open Vmvalues type lambda = structured_values Genlambda.lambda (** Simplification of lambda expression *) (* TODO: make the VM and native agree *) let can_subst lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Luint _ | Lval _ | Lsort _ | Lind _ -> true | _ -> false let simplify subst lam = simplify can_subst subst lam (*s Translation from [constr] to [lambda] *) (* Translation of constructor *) let is_value lc = match lc with | Lval _ | Lint _ | Luint _ -> true | _ -> false let get_value lc = match lc with | Luint i -> val_of_uint i | Lval v -> v | Lint i -> val_of_int i | _ -> raise Not_found let as_value tag args = if Array.for_all is_value args then if tag < Obj.last_non_constant_constructor_tag then Some (val_of_block tag (Array.map get_value args)) else let args = Array.map get_value args in let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in Some (val_of_block Obj.last_non_constant_constructor_tag args) else None module Val = struct type value = 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 let get_constant knu _ = Lconst knu end module Lambda = Genlambda.Make(Val) (*********************************) let dump_lambda = ref false let optimize_lambda lam = let subst_id = subs_id 0 in let lam = simplify subst_id lam in remove_let subst_id lam let lambda_of_constr ~optimize env sigma c = let lam = Lambda.lambda_of_constr env sigma c in let lam = if optimize then optimize_lambda lam else lam in if !dump_lambda then Feedback.msg_debug (pp_lam lam); lam
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>