Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/atton-master-sample.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 module atton-master-sample where 1 module atton-master-sample where
2 2
3 open import Data.Nat 3 open import Data.Nat
4 open import Data.Unit 4 open import Data.Unit
5 open import Function 5 open import Function
6 Int = @$\mathbb{N}$@ 6 Int = !$\mathbb{N}$!
7 7
8 record Context : Set where 8 record Context : Set where
9 field 9 field
10 a : Int 10 a : Int
11 b : Int 11 b : Int
25 field 25 field
26 c : Int 26 c : Int
27 27
28 instance 28 instance
29 _ : DataSegment ds0 29 _ : DataSegment ds0
30 _ = record { set = (\c d @$\rightarrow$@ record c {a = (ds0.a d) ; b = (ds0.b d)}) 30 _ = record { set = (\c d !$\rightarrow$! record c {a = (ds0.a d) ; b = (ds0.b d)})
31 ; get = (\c @$\rightarrow$@ record { a = (Context.a c) ; b = (Context.b c)})} 31 ; get = (\c !$\rightarrow$! record { a = (Context.a c) ; b = (Context.b c)})}
32 _ : DataSegment ds1 32 _ : DataSegment ds1
33 _ = record { set = (\c d @$\rightarrow$@ record c {c = (ds1.c d)}) 33 _ = record { set = (\c d !$\rightarrow$! record c {c = (ds1.c d)})
34 ; get = (\c @$\rightarrow$@ record { c = (Context.c c)})} 34 ; get = (\c !$\rightarrow$! record { c = (Context.c c)})}
35 35
36 cs2 : CodeSegment ds1 ds1 36 cs2 : CodeSegment ds1 ds1
37 cs2 = cs id 37 cs2 = cs id
38 38
39 cs1 : CodeSegment ds1 ds1 39 cs1 : CodeSegment ds1 ds1
40 cs1 = cs (\d @$\rightarrow$@ goto cs2 d) 40 cs1 = cs (\d !$\rightarrow$! goto cs2 d)
41 41
42 cs0 : CodeSegment ds0 ds1 42 cs0 : CodeSegment ds0 ds1
43 cs0 = cs (\d @$\rightarrow$@ goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) 43 cs0 = cs (\d !$\rightarrow$! 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})