Mercurial > hg > Members > atton > agda-proofs
comparison cbc/atton-master-sample.agda @ 73:a5cac9483f91
Cleanup sample
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 01 Feb 2017 05:27:05 +0000 |
parents | dc8f140e299d |
children |
comparison
equal
deleted
inserted
replaced
72:dc8f140e299d | 73:a5cac9483f91 |
---|---|
31 ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} | 31 ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} |
32 _ : DataSegment ds1 | 32 _ : DataSegment ds1 |
33 _ = record { set = (\c d -> record c {c = (ds1.c d)}) | 33 _ = record { set = (\c d -> record c {c = (ds1.c d)}) |
34 ; get = (\c -> record { c = (Context.c c)})} | 34 ; get = (\c -> record { c = (Context.c c)})} |
35 | 35 |
36 cs2 : {{_ : DataSegment ds1}} -> CodeSegment ds1 ds1 | 36 cs2 : CodeSegment ds1 ds1 |
37 cs2 {{d}} = cs {{d}}{{d}} id | 37 cs2 = cs id |
38 | 38 |
39 cs1 : CodeSegment ds1 ds1 | 39 cs1 : CodeSegment ds1 ds1 |
40 cs1 = cs (\d -> goto cs2 d) | 40 cs1 = cs (\d -> goto cs2 d) |
41 | 41 |
42 cs0 : {{_ : DataSegment ds0}} {{_ : DataSegment ds1}} -> CodeSegment ds0 ds1 | 42 cs0 : CodeSegment ds0 ds1 |
43 cs0 {{d0}}{{d1}} = cs {{d0}}{{d1}} (\d -> goto {{d1}} {{d1}} cs1 (record {c = (ds0.a d) + (ds0.b d)})) | 43 cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) |
44 | 44 |
45 main : ds1 | 45 main : ds1 |
46 main = goto cs0 (record {a = 100 ; b = 50}) | 46 main = goto cs0 (record {a = 100 ; b = 50}) |