timl/examples/basic.timl at master · wangpengmit/timl · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
(* Basic types *)

structure Basic = struct

open Pervasive

fun fst a = __&fst a
fun snd a = __&snd a
fun not a = __&not a
val true = __&true
val false = __&false
val itrue = __&itrue
val ifalse = __&ifalse
fun nat2int {n : Nat} (a : nat {n}) = __&nat2int a
fun int2nat a = __&int2nat a
fun int2byte a = __&int2byte a
fun byte2int a = __&byte2int a
(* fun int2str a = __&int2str a *)
(* fun print a = __&print a *)

(* a datatype version of boolean that is suitable for pattern-matching *)
datatype Bool = True | False

(* indexed boolean *)
datatype iBool : {Bool} =
         ITrue of iBool {true}
         | IFalse of iBool {false}

fun b2B b = if b then True else False
fun ib2iB {i : Bool} (b : ibool {i}) return iBool {i} =
  ifdec b then
    ITrue : iBool {i}
  else
    IFalse : iBool {i}

datatype option 'a =
         NONE
         | SOME of 'a --> option 'a

datatype le {a b : Nat} =
         LE {a <= b} of le {a} {b}

(* val a = int2nat 10 *)
(* val () = __&halt a *)

end