mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
add todos
This commit is contained in:
parent
5ad103d7ae
commit
d94d865b8d
@ -233,6 +233,8 @@ Lit.Core.Type.find_ctor(name: String, type: Lit.Core.Type): Maybe<Pair<Nat,Lit.C
|
||||
none
|
||||
data:
|
||||
List.ifind!((i,f) String.eql(f@name,name), type.constructors)
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
//
|
||||
@ -341,6 +343,8 @@ Lit.Core.World.check.term(
|
||||
let val0 = Lit.Core.World.check.term(context, term.val0, Lit.Core.Type.word)
|
||||
let val1 = Lit.Core.World.check.term(context, term.val1, Lit.Core.Type.word)
|
||||
val0 && val1
|
||||
return:
|
||||
_ // TODO
|
||||
}
|
||||
//log("\n")
|
||||
result
|
||||
@ -470,6 +474,8 @@ Lit.Core.World.run.statement(
|
||||
else
|
||||
log("error: cannot redefine built-in type named 'U64'") none
|
||||
} default log("error: type redefinition: " | type.name) none
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
bond:
|
||||
use func = statement.entry.value
|
||||
@ -587,6 +593,8 @@ Lit.Core.World.run.term(
|
||||
log("bind!") // DEBUG
|
||||
let gas = gas + Lit.Core.Costs.default@bind
|
||||
Lit.Core.World.run.term.bind(world, vars, term.name, term.main, term.cont, gas)
|
||||
return:
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
Lit.Core.World.run.terms(
|
||||
@ -819,6 +827,8 @@ Lit.Core.run.term.check_sanity(term: Lit.Core.Term): Bool
|
||||
bind:
|
||||
Lit.Core.run.term.check_sanity(term.main)
|
||||
&& Lit.Core.run.term.check_sanity(term.cont)
|
||||
return:
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
// Serialization
|
||||
|
@ -47,6 +47,8 @@ Lit.Lang.show.type(type: Lit.Core.Type, world: Lit.Core.World): String
|
||||
| "}"
|
||||
))
|
||||
| " }"
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
|
||||
Lit.Lang.show.bond(bond: Lit.Core.Bond, world: Lit.Core.World): String
|
||||
@ -102,6 +104,8 @@ Lit.Lang.show.term(term: Lit.Core.Term, world: Lit.Core.World): String
|
||||
let vals = if List.is_empty!(vals) then "" else "{" | String.join(",",vals) | "}"
|
||||
return type.name | "/" | ctor.name | vals
|
||||
}
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
} <> "CREATE"
|
||||
match: Maybe {
|
||||
@ -121,6 +125,8 @@ Lit.Lang.show.term(term: Lit.Core.Term, world: Lit.Core.World): String
|
||||
term.cses)
|
||||
return "case " | name | " : " | type.name | " = " | expr | " { " | String.join(", ",vals) | " }"
|
||||
}
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
} <> "MATCH"
|
||||
call: Maybe {
|
||||
@ -180,8 +186,12 @@ Lit.Lang.parser.page(world: Lit.Core.World): Parser<Lit.Core.Page>
|
||||
define: case head.entry as entry {
|
||||
type:
|
||||
case entry.value {
|
||||
word: world
|
||||
data: world{entry.value.name} <- Lit.Core.Entry.type(entry.value)
|
||||
word:
|
||||
world
|
||||
data:
|
||||
world{entry.value.name} <- Lit.Core.Entry.type(entry.value)
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
} default world
|
||||
} default world
|
||||
@ -460,6 +470,8 @@ Lit.Lang.parser.term.match(world: Lit.Core.World): Parser<Lit.Core.Term>
|
||||
Lit.Lang.parser.text("}")
|
||||
return Lit.Core.Term.match(name, type_name, expr, cses)
|
||||
}
|
||||
effect:
|
||||
_ // TODO
|
||||
}
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user