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

107 lines (81 sloc) 2.503 kB
%% Various test functions for the VM
%% Jesper Louis Andersen, 2009
%{
The following pgm_1 encodes a gauss addition, i.e. gauss 3 = 1+2+3 = 6, by
recursive calls to ourselves.
}%
f = fun-id/ z.
tri = fun-id/ z.
b0 = [pb] f-hd (f-tl/z pb).
b1 = [pb] f-hd (f-tl/s (f-tl/z pb)).
b2 = [pb] f-hd (f-tl/s (f-tl/s (f-tl/z pb))).
b3 = [pb] f-hd (f-tl/s (f-tl/s (f-tl/s (f-tl/z pb)))).
pgm_1 = pgm/ (defs/s tri
(fun-decl/parm ([n]
fun-decl/body
(insn/letrec
([pb] (l-def-list/cons
(l-def/body (insn/let (op/cmp-lt n (cst/n 1))
([r : cst tp/bool] (insn/brc r (b1 pb) cst-list/nil (b2 pb) cst-list/nil))))
(l-def-list/cons
(l-def/body (insn/br (b3 pb) (cst-list/cons (cst/n 0) cst-list/nil)))
(l-def-list/cons
(l-def/body
(insn/let (op/mone n (cst/n 1))
([sub : cst tp/nat] (insn/call tri (cst-list/cons sub cst-list/nil)
([call : cst tp/nat] insn/let (op/plus call n)
([plus] insn/br (b3 pb) (cst-list/cons plus cst-list/nil)))))))
(l-def-list/cons
(l-def/phi [retval]
(l-def/body (insn/return retval)))
l-def-list/nil)))))
([pb] insn/br (b0 pb) cst-list/nil))))
defs/z)
(insn/call tri (cst-list/cons (cst/n 3) cst-list/nil)
([r] insn/return r)).
pgm_2 = pgm/ (defs/s f
(fun-decl/parm
([n] fun-decl/body
(insn/let (op/plus n (cst/n 1))
([plus] insn/return plus))))
defs/z)
(insn/call f (cst-list/cons (cst/n 2) cst-list/nil)
([r] insn/return r)).
pgm_3 = pgm/ (defs/s f
(fun-decl/parm
([n] fun-decl/body
(insn/return (cst/n 1))))
defs/z)
(insn/call f (cst-list/cons (cst/n 2) cst-list/nil)
([r] insn/return r)).
step2 : pgm -> pgm -> type.
step2/ : step2 P P'
<- step-pgm P P''
<- step-pgm P'' P'.
step3 : pgm -> pgm -> type.
step3/ : step3 P1 P4
<- step-pgm P1 P2
<- step-pgm P2 P3
<- step-pgm P3 P4.
step4 : pgm -> pgm -> type.
step4/ : step4 P1 P4
<- step3 P1 P3
<- step-pgm P3 P4.
step5 : pgm -> pgm -> type.
step5/ : step5 P1 P4
<- step4 P1 P3
<- step-pgm P3 P4.
step6 : pgm -> pgm -> type.
step6/ : step6 P1 P4
<- step5 P1 P3
<- step-pgm P3 P4.
%query 1 2 (step2 pgm_3 X).
%query 1 2 (step3 pgm_2 X).
%query 1 2 (step-pgm pgm_1 X).
%query 1 2 (step2 pgm_1 X).
%query 1 2 (step3 pgm_1 X).
%query 1 2 (step4 pgm_1 X).
%query 1 2 (step5 pgm_1 X).
%query 1 2 (step6 pgm_1 X).
%query 1 1 (wf-pgm pgm_1).
%query 1 2 (steps-to pgm_1 X).
Jump to Line
Something went wrong with that request. Please try again.