Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859(************************************************************************)(* * 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) *)(************************************************************************)
open Utilopen Genlambda
(** This file defines the lambda code generation phase of the native compiler *)
type lambda = Nativevalues.t Genlambda.lambda
(*s Constructors *)
(** Simplification of lambda expression *)
let is_value lc = match node lc with | Lval _ | Lint _ | Luint _ | Lfloat _ | Lstring _ -> true | _ -> false
let get_value lc = match node lc with | Lval v -> v | Lint tag -> Nativevalues.mk_int tag | Luint i -> Nativevalues.mk_uint i | Lfloat f -> Nativevalues.mk_float f | Lstring s -> Nativevalues.mk_string s | _ -> raise Not_found
let as_value tag args = if Array.for_all is_value args then let dummy_val = Obj.magic 0 in let args = (* Don't simplify this to Array.map, cf. the related comment in function eval_to_patch, file kernel/csymtable.ml *) let a = Array.make (Array.length args) dummy_val in Array.iteri (fun i v -> a.(i) <- get_value v) args; a in Some (Nativevalues.mk_block tag args) else None
module Val =struct type value = Nativevalues.t let as_value = as_value let check_inductive _ _ = ()end
module Lambda = Genlambda.Make(Val)
let lambda_of_constr env sigma c = let lam = Lambda.lambda_of_constr env sigma c in optimize lam