File: clambda.mli

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (31 lines) | stat: -rw-r--r-- 1,227 bytes parent folder | download
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
open Names
open Cinstr
open Environ

exception TooLargeInductive of Pp.t

val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda

val decompose_Llam : lambda -> Name.t array * lambda

val get_alias : env -> Constant.t -> Constant.t

val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda

(** spiwack: this function contains the information needed to perform
            the static compilation of int31 (trying and obtaining
            a 31-bit integer in processor representation at compile time) *)
val compile_structured_int31 : bool -> Constr.t array -> lambda

(** this function contains the information needed to perform
        the dynamic compilation of int31 (trying and obtaining a
        31-bit integer in processor representation at runtime when
        it failed at compile time *)
val dynamic_int31_compilation : bool -> lambda array -> lambda

(*spiwack: compiling function to insert dynamic decompilation before
           matching integers (in case they are in processor representation) *)
val int31_escape_before_match : bool -> lambda -> lambda

(** Dump the VM lambda code after compilation (for debugging purposes) *)
val dump_lambda : bool ref