diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-05 19:51:04 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | de61c7d77e49286622c4aebd56f2e87b0df93903 (patch) | |
| tree | d7038f72ed54e3cdebae620c458e3ca93294f49f /kernel/nativeinstr.mli | |
| parent | 5bcfa8cab56798f2b575b839fd92b0f743c3d453 (diff) | |
Had to split Nativelambda in two files because of Retroknowledge
dependencies.
Diffstat (limited to 'kernel/nativeinstr.mli')
| -rw-r--r-- | kernel/nativeinstr.mli | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli new file mode 100644 index 000000000..4e0291ed9 --- /dev/null +++ b/kernel/nativeinstr.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Term +open Nativevalues + +(** This file defines the lambda code for the native compiler. It has been +extracted from Nativelambda.ml because of the retroknowledge architecture. *) + +type lambda = + | Lrel of name * int + | Lvar of identifier + | Lmeta of metavariable * lambda (* type *) + | Levar of existential * lambda (* type *) + | Lprod of lambda * lambda + | Llam of name array * lambda + | Llet of name * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of string * constant (* prefix, constant name *) + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of string * constructor * int * lambda array + (* prefix, constructor name, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of string * constructor (* prefix, constructor name *) + (* A partially applied constructor *) + | Luint of Uint31.t + | Lval of Nativevalues.t + | Lsort of sorts + | Lind of string * inductive (* prefix, inductive name *) + | Llazy + | Lforce + +and lam_branches = (constructor * name array * lambda) array + +and fix_decl = name array * lambda array * lambda array |