Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Tree: 8514018bf8
Fetching contributors…

Cannot retrieve contributors at this time

156 lines (106 sloc) 3.999 kB
%{
******** Type System ********
}%
%% Primitive types
tp : type. %name tp Tp.
tp/nat : tp.
tp/bool : tp.
%% Lists of primitive types
tp-list : type. %name tp-list TpL.
tp-list/nil : tp-list.
tp-list/cons : tp -> tp-list -> tp-list.
%% Basic-block types
l-tp : type. %name l-tp LTp.
%% There is only way to introduce a function type.
l-tp/ : tp-list -> tp -> l-tp.
l-tp-list : type. %name l-tp-list LTpL.
l-tp-list/nil : l-tp-list.
l-tp-list/cons : l-tp -> l-tp-list -> l-tp-list.
%{
******** Syntax ********
}%
%{
Constants is a family of either constants or register. But as variables
are captured by HOAS, we do not need to specify them.
}%
cst : tp -> type. %name cst C c.
cst/n : nat -> cst tp/nat.
cst/b : nat -> cst tp/bool.
%{
We will need lists of registers/constants when one makes function
calls and when one jumps to other basic blocks. Hence, we define them
here
}%
cst-list : tp-list -> type. %name cst-list CL.
cst-list/nil : cst-list tp-list/nil.
cst-list/cons : cst T -> cst-list TL -> cst-list (tp-list/cons T TL).
%{ Introduction of function bundles.
Function names
Function bundles
A pbundle is used a reference point in an letrec introduction,
ie, letrec PB = (d, ...) in B.
pbundle+ and bname is used to implement the l^k notation.
}%
bname : l-tp -> type. %name bname Bname.
pbundle : l-tp-list -> type.
pbundle+ : l-tp-list -> type.
%{ This constant only exists to appease Twelfs splitter in the input coverage }%
pbundle0 : pbundle l-tp-list/nil.
%{ When referring to a given entry in a letrec, we utilize a
construction of the form
l^k in the operational semantics notation. Here we define, e.g., l^2 as
f-hd (f-tl/s (f-tl/s (f-tl/z FN))) for access to the second entry.
This construction let us define a way to intrinsically define branches
to other basic blocks }%
f-hd : pbundle+ (l-tp-list/cons FT FTL) -> bname FT.
f-tl/z : pbundle FTL -> pbundle+ FTL.
f-tl/s : pbundle+ (l-tp-list/cons FT FTL) -> pbundle+ FTL.
%{ Operations }%
op : tp -> type.
%{ Instructions. Either assigning to a register, a return or a branch.
These take care of control flow }%
insn : tp -> type.
%{ Syntactic operation equality }%
op-eq : op T -> op T -> type.
op-eq/refl : op-eq T T.
%{ Function call identifiers. Carries type information }%
fun-id : tp -> tp-list -> type.
fun-id/ : nat -> fun-id T TL.
%{ Basic block definitions }%
l-def : l-tp -> type.
%{ HOAS encoding of phi-parameters to a basic block }%
l-def/body : insn T -> (l-def (l-tp/ tp-list/nil T)).
l-def/phi : (cst T0 -> l-def (l-tp/ TL T))
-> l-def (l-tp/ (tp-list/cons T0 TL) T).
%{ Lists of basic block definitions. These are used in letrec-blocks }%
l-def-list : l-tp-list -> type.
l-def-list/nil : l-def-list l-tp-list/nil.
l-def-list/cons : l-def FT -> l-def-list FTL
-> l-def-list (l-tp-list/cons FT FTL).
%{ Operations. }%
%{ Primitive constants }%
op/cst : cst T -> op T.
%{ Operations on registers }%
op/plus : cst tp/nat -> cst tp/nat -> op tp/nat.
op/cmp-lt : cst tp/nat -> cst tp/nat -> op tp/bool.
op/mone : cst tp/nat -> cst tp/nat -> op tp/nat.
insn/return : cst T -> insn T.
insn/br : bname (l-tp/ TL T) -> cst-list TL -> insn T.
insn/brc : cst tp/bool -> bname (l-tp/ TL T) -> cst-list TL
-> bname (l-tp/ TL1 T) -> cst-list TL1 -> insn T.
insn/let : op T1 -> (cst T1 -> insn T) -> insn T.
insn/letrec : (pbundle FTL -> l-def-list FTL)
-> (pbundle FTL -> insn T) -> insn T.
insn/do : insn T' -> (cst T' -> insn T) -> insn T. %% Only internally used
insn/call : fun-id T TL -> cst-list TL -> (cst T -> insn T) -> insn T.
%{ **** Functions **** }%
fun-decl : tp -> tp-list -> type.
fun-decl/parm : (cst T -> fun-decl R TL) -> fun-decl R (tp-list/cons T TL).
fun-decl/body : insn T -> fun-decl T tp-list/nil.
%{ Function definition lists }%
defs : type.
defs/z : defs.
defs/s : fun-id T TL -> fun-decl T TL -> defs -> defs.
%{ Programs }%
pgm : type.
pgm/ : defs -> insn T -> pgm.
Jump to Line
Something went wrong with that request. Please try again.