mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
Lit: add simple voting contract
This commit is contained in:
rheidner
parent
5422437c62
commit
75dae8b2ac
@ -195,20 +195,23 @@ Lit.Core.World.check.term(
|
||||
// log("") // DEBUG
|
||||
let result = case term {
|
||||
var:
|
||||
// log("-- var " | term.name) // DEBUG
|
||||
let var_type = context{term.name} abort false
|
||||
//log("-- var " | term.name | " " | Lit.Lang.show.type.short(var_type) | " " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
// log("-- var " | term.name | " " | Lit.Lang.show.type.short(var_type) | " " | Lit.Lang.show.type.short(type)) // DEBUG
|
||||
Lit.Core.Type.equal(var_type, type)
|
||||
create:
|
||||
//log("-- create") // DEBUG
|
||||
// log("-- create ") // DEBUG
|
||||
let ttyp = Lit.Core.World.get_type(term.type,world) abort false
|
||||
case ttyp {
|
||||
data:
|
||||
use ctor = ttyp.constructors[term.ctor] abort false
|
||||
let args = Lit.Core.World.check.many(term.vals, List.mapped!(ctor.fields)!((x) x@type), context, world, caller)
|
||||
log(Bool.show(args))
|
||||
log(Bool.show(Lit.Core.Type.equal(ttyp, type)))
|
||||
args && Lit.Core.Type.equal(ttyp, type)
|
||||
} default false
|
||||
call:
|
||||
//log("-- call") // DEBUG
|
||||
// log("-- call ") // DEBUG
|
||||
// verify owner
|
||||
let ownr = Lit.Core.World.check.owner(caller, term.func, world)
|
||||
use func = Lit.Core.World.get_func(term.func,world) abort false
|
||||
@ -217,9 +220,9 @@ Lit.Core.World.check.term(
|
||||
let cont = Lit.Core.World.check.term(term.cont, type, context{term.name} <- otyp, world, caller)
|
||||
ownr && args && cont
|
||||
match:
|
||||
//log("-- match ") // DEBUG
|
||||
// log("-- match ") // DEBUG
|
||||
let expr_type = Lit.Core.World.get_type(term.type, world) abort false
|
||||
//log("-- match2 ") // DEBUG
|
||||
// log("-- match2 ") // DEBUG
|
||||
|
||||
case expr_type {
|
||||
data:
|
||||
@ -229,7 +232,7 @@ Lit.Core.World.check.term(
|
||||
expr && cses
|
||||
} default false
|
||||
bind:
|
||||
//log("-- bind ") // DEBUG
|
||||
// log("-- bind ") // DEBUG
|
||||
// TODO: check access
|
||||
let ownr = Lit.Core.World.check.owner(caller, term.name, world)
|
||||
use func = Lit.Core.World.get_func(term.name,world) abort false
|
||||
@ -240,7 +243,7 @@ Lit.Core.World.check.term(
|
||||
let cont = Lit.Core.World.check.term(term.cont, type, context, world, caller)
|
||||
ownr && nofn && main && cont
|
||||
word:
|
||||
//log("-- word ") // DEBUG
|
||||
// log("-- word ") // DEBUG
|
||||
case type {
|
||||
word:
|
||||
true
|
||||
@ -248,7 +251,7 @@ Lit.Core.World.check.term(
|
||||
log("not word")
|
||||
false
|
||||
compare:
|
||||
//log("-- compare ") // DEBUG
|
||||
// log("-- compare ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let val1 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let iflt = Lit.Core.World.check.term(term.iflt, type, context, world, caller)
|
||||
@ -256,7 +259,7 @@ Lit.Core.World.check.term(
|
||||
let ifgt = Lit.Core.World.check.term(term.ifgt, type, context, world, caller)
|
||||
val0 && val1 && iflt && ifeq && ifgt
|
||||
operate:
|
||||
//log("-- operate ") // DEBUG
|
||||
// log("-- operate ") // DEBUG
|
||||
let val0 = Lit.Core.World.check.term(term.val0, Lit.Core.Type.word, context, world, caller)
|
||||
let val1 = Lit.Core.World.check.term(term.val1, Lit.Core.Type.word, context, world, caller)
|
||||
val0 && val1
|
||||
@ -514,6 +517,7 @@ Lit.Core.World.run.statement(
|
||||
else
|
||||
log("error: func invalid: " | func.name) none
|
||||
else
|
||||
// log(Lit.Lang.show.type(otyp, world))
|
||||
log("error: func ill-typed: " | func.name) none
|
||||
}
|
||||
} default log("error: func redefinition: " | func.name) none
|
||||
@ -676,24 +680,25 @@ Lit.Core: _
|
||||
| Lit.Lang.Nat
|
||||
| Lit.Lang.Bits
|
||||
| Lit.Lang.BitsMap
|
||||
| Lit.Lang.Voting
|
||||
// | Lit.Lang.Test
|
||||
|
||||
let code = code |
|
||||
`
|
||||
GiveUnit(): Unit
|
||||
Unit/new
|
||||
// let code = code |
|
||||
// `
|
||||
// GiveUnit(): Unit
|
||||
// Unit/new
|
||||
|
||||
TakeUnit(x: Unit): U64
|
||||
42
|
||||
// TakeUnit(x: Unit): U64
|
||||
// 42
|
||||
|
||||
do {
|
||||
call a1 = GiveUnit()
|
||||
call a2 = GiveUnit()
|
||||
call b = TakeUnit(a1)
|
||||
call c = TakeUnit(a2)
|
||||
(+ b c)
|
||||
}
|
||||
`
|
||||
// do {
|
||||
// call a1 = GiveUnit()
|
||||
// call a2 = GiveUnit()
|
||||
// call b = TakeUnit(a1)
|
||||
// call c = TakeUnit(a2)
|
||||
// (+ b c)
|
||||
// }
|
||||
// `
|
||||
|
||||
// let code = code |
|
||||
// `
|
||||
|
||||
245
base/Lit/Lang/Voting.kind
Normal file
245
base/Lit/Lang/Voting.kind
Normal file
@ -0,0 +1,245 @@
|
||||
Lit.Lang.Voting: String
|
||||
`
|
||||
type Voter {
|
||||
new{allowed: Bool, voted: Bool}
|
||||
}
|
||||
|
||||
type Candidates {
|
||||
nil
|
||||
cons{count: Nat, tail: Candidates}
|
||||
}
|
||||
|
||||
type VotingMap {
|
||||
new
|
||||
tie{val: Voter, lft: VotingMap, rgt: VotingMap}
|
||||
}
|
||||
|
||||
type VotingMap.Relation {
|
||||
new{value: Voter, map: VotingMap}
|
||||
}
|
||||
|
||||
type Pair.VotingMap {
|
||||
new{fst: VotingMap, snd: VotingMap}
|
||||
}
|
||||
|
||||
type Pair.Voter {
|
||||
new{fst: Voter, snd: Voter}
|
||||
}
|
||||
|
||||
type VoteResult {
|
||||
new {
|
||||
map: VotingMap,
|
||||
candidates: Candidates
|
||||
}
|
||||
}
|
||||
|
||||
VotingMap.set(map: VotingMap, key: Bits, value: Voter): VotingMap
|
||||
case map : VotingMap {
|
||||
new:
|
||||
case key : Bits {
|
||||
e:
|
||||
VotingMap/tie{val: value, lft: VotingMap/new, rgt: VotingMap/new}
|
||||
o:
|
||||
call ins = VotingMap.set(VotingMap/new, key.pred, value)
|
||||
VotingMap/tie{val: Voter/new{allowed: Bool/false, voted: Bool/false}, lft: ins, rgt: VotingMap/new}
|
||||
i:
|
||||
call ins = VotingMap.set(VotingMap/new, key.pred, value)
|
||||
VotingMap/tie{val: Voter/new{allowed: Bool/false, voted: Bool/false}, lft: VotingMap/new, rgt: ins}
|
||||
}
|
||||
tie:
|
||||
case key : Bits {
|
||||
e:
|
||||
VotingMap/tie{val: value, lft: VotingMap/new, rgt: VotingMap/new}
|
||||
o:
|
||||
call ins = VotingMap.set(map.lft, key.pred, value)
|
||||
VotingMap/tie{val: map.val, lft: ins, rgt: map.rgt}
|
||||
i:
|
||||
call ins = VotingMap.set(map.rgt, key.pred, value)
|
||||
VotingMap/tie{val: map.val, lft: map.lft, rgt: ins}
|
||||
}
|
||||
}
|
||||
|
||||
// TODO this function is almost useless because you need to duplicate the map to use it
|
||||
// very expensive!
|
||||
VotingMap.get(map: VotingMap, key: Bits): Voter
|
||||
case map : VotingMap {
|
||||
new:
|
||||
Voter/new{allowed: Bool/false, voted: Bool/false} // transform in maybe?
|
||||
tie:
|
||||
case key : Bits {
|
||||
e:
|
||||
map.val
|
||||
o:
|
||||
call val = VotingMap.get(map.lft, key.pred)
|
||||
val
|
||||
i:
|
||||
call val = VotingMap.get(map.rgt, key.pred)
|
||||
val
|
||||
}
|
||||
}
|
||||
|
||||
Voter.dup(v: Voter): Pair.Voter
|
||||
case v : Voter {
|
||||
new:
|
||||
Pair.Voter/new{
|
||||
fst: v,
|
||||
snd: Voter/new{allowed: v.allowed, voted: v.voted}
|
||||
}
|
||||
}
|
||||
|
||||
VotingMap.get_p(map: VotingMap, key: Bits): VotingMap.Relation
|
||||
case map : VotingMap {
|
||||
new:
|
||||
VotingMap.Relation/new{value: Voter/new{allowed: Bool/false, voted: Bool/false}, map: VotingMap/new}
|
||||
tie:
|
||||
case key : Bits {
|
||||
e:
|
||||
call dup = Voter.dup(map.val)
|
||||
case dup : Pair.Voter {
|
||||
new:
|
||||
VotingMap.Relation/new {
|
||||
value: dup.fst,
|
||||
map: VotingMap/tie {
|
||||
val: dup.snd
|
||||
lft: map.lft
|
||||
rgt: map.rgt
|
||||
}
|
||||
}
|
||||
}
|
||||
o:
|
||||
call rec = VotingMap.get_p(map.lft, key.pred)
|
||||
case rec : VotingMap.Relation {
|
||||
new:
|
||||
VotingMap.Relation/new {
|
||||
value: rec.value,
|
||||
map: VotingMap/tie {
|
||||
val: map.val
|
||||
lft: rec.map
|
||||
rgt: map.rgt
|
||||
}
|
||||
}
|
||||
}
|
||||
i:
|
||||
call rec = VotingMap.get_p(map.rgt, key.pred)
|
||||
case rec : VotingMap.Relation {
|
||||
new:
|
||||
VotingMap.Relation/new {
|
||||
value: rec.value
|
||||
map: VotingMap/tie {
|
||||
val: map.val
|
||||
lft: map.lft
|
||||
rgt: rec.map
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
VotingMap.dup(m: VotingMap): Pair.VotingMap
|
||||
case m : VotingMap {
|
||||
new:
|
||||
Pair.VotingMap/new{fst: VotingMap/new, snd: VotingMap/new}
|
||||
tie:
|
||||
call dup_voter = Voter.dup(m.val)
|
||||
call dup_lft = VotingMap.dup(m.lft)
|
||||
call dup_rgt = VotingMap.dup(m.rgt)
|
||||
case dup_voter : Pair.Voter {
|
||||
new:
|
||||
case dup_lft : Pair.VotingMap {
|
||||
new:
|
||||
case dup_rgt : Pair.VotingMap {
|
||||
new:
|
||||
Pair.VotingMap/new{
|
||||
fst: VotingMap/tie{val: dup_voter.fst, lft: dup_lft.fst, rgt: dup_rgt.fst}
|
||||
snd: VotingMap/tie{val: dup_voter.snd, lft: dup_lft.snd, rgt: dup_rgt.snd}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// should be owned by the user who deploy the contract
|
||||
// TODO using get two times and getting success
|
||||
VotingMap.allow_vote(map: VotingMap, key: Bits): VotingMap
|
||||
call voter_get = VotingMap.get_p(map, key)
|
||||
case voter_get : VotingMap.Relation {
|
||||
new:
|
||||
case voter_get.value : Voter {
|
||||
new:
|
||||
case voter_get.value.voted : Bool {
|
||||
true:
|
||||
map
|
||||
false:
|
||||
call newmap = VotingMap.set(
|
||||
voter_get.map,
|
||||
key,
|
||||
Voter/new{allowed: Bool/true, voted: voter_get.value.voted}
|
||||
)
|
||||
newmap
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Candidates.compute_vote(vote: Nat, candidates: Candidates): Candidates
|
||||
case vote : Nat {
|
||||
zero:
|
||||
case candidates : Candidates {
|
||||
nil: Candidates/nil
|
||||
cons:
|
||||
Candidates/cons{
|
||||
count: Nat/succ{pred: candidates.count},
|
||||
tail: candidates.tail
|
||||
}
|
||||
}
|
||||
succ:
|
||||
case candidates : Candidates {
|
||||
nil: Candidates/nil
|
||||
cons:
|
||||
call new_candidates = Candidates.compute_vote(vote.pred, candidates.tail)
|
||||
new_candidates
|
||||
}
|
||||
}
|
||||
|
||||
// TODO the order when making a case matter?
|
||||
VotingMap.vote(map: VotingMap, key: Bits, vote: Nat, candidates: Candidates): VoteResult
|
||||
call voter_get = VotingMap.get_p(map, key)
|
||||
case voter_get : VotingMap.Relation {
|
||||
new:
|
||||
case voter_get.value : Voter {
|
||||
new:
|
||||
case voter_get.value.allowed : Bool {
|
||||
true:
|
||||
call new_cand = Candidates.compute_vote(vote, candidates)
|
||||
call new_map = VotingMap.set(map, key, Voter/new{allowed: Bool/false, voted: Bool/true})
|
||||
VoteResult/new{map: new_map, candidates: new_cand}
|
||||
false:
|
||||
VoteResult/new{map: map, candidates: candidates}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Candidates.get_winner.aux(candidates: Candidates, index: Nat, greater: Nat): Nat
|
||||
case candidates : Candidates {
|
||||
nil: greater
|
||||
cons:
|
||||
call comp = Nat.cmp(candidates.count, greater)
|
||||
case comp : Cmp {
|
||||
ltn:
|
||||
call result = Candidates.get_winner.aux(candidates.tail, Nat/succ{pred: index}, greater)
|
||||
result
|
||||
eql:
|
||||
call result = Candidates.get_winner.aux(candidates.tail, Nat/succ{pred: index}, greater)
|
||||
result
|
||||
gtn:
|
||||
call result = Candidates.get_winner.aux(candidates.tail, Nat/succ{pred: index}, index)
|
||||
result
|
||||
}
|
||||
}
|
||||
|
||||
// TODO add case for empty list, what return?
|
||||
// can i use the same variable in differente case branchs?
|
||||
Candidates.get_winner(candidates: Candidates): Nat
|
||||
call result = Candidates.get_winner.aux(candidates, Nat/zero, Nat/zero)
|
||||
result
|
||||
`
|
||||
Loading…
Reference in New Issue
Block a user