mirror of
https://github.com/anoma/juvix.git
synced 2024-08-17 04:01:05 +03:00
Update juvix-stdlib to remove non-ASCII indentifiers (#2857)
This PR updates the juvix-stdlib to the current main commit which includes: * https://github.com/anoma/juvix-stdlib/issues/59 * https://github.com/anoma/juvix-stdlib/issues/101 All the Juvix test suite files and examples in this repo have been updated to be compatible with the new stdlib.
This commit is contained in:
parent
6d24d7186d
commit
b8cd84170b
@ -43,11 +43,11 @@ sort {A} {{Ord A}} : List A → List A
|
||||
printNatListLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printNatListLn xs;
|
||||
printNat x >>> printString " :: " >>> printNatListLn xs;
|
||||
|
||||
main : IO :=
|
||||
printStringLn "Hello!"
|
||||
>> printNatListLn (preorder (mirror tree))
|
||||
>> printNatListLn (sort (preorder (mirror tree)))
|
||||
>> printNatLn (log2 3)
|
||||
>> printNatLn (log2 130);
|
||||
>>> printNatListLn (preorder (mirror tree))
|
||||
>>> printNatListLn (sort (preorder (mirror tree)))
|
||||
>>> printNatLn (log2 3)
|
||||
>>> printNatLn (log2 130);
|
||||
|
@ -34,7 +34,7 @@ open Token;
|
||||
|
||||
--- This module defines the type for balances and its associated operations.
|
||||
module Balances;
|
||||
Balances : Type := List (Field × Nat);
|
||||
Balances : Type := List (Pair Field Nat);
|
||||
|
||||
--- Increments the amount associated with a certain ;Field;.
|
||||
increment : Field -> Nat -> Balances -> Balances
|
||||
|
@ -12,8 +12,8 @@ collatz : Nat → Nat
|
||||
|
||||
terminating
|
||||
run (f : Nat → Nat) : Nat → IO
|
||||
| (suc zero) := printNatLn 1 >> printStringLn "Finished!"
|
||||
| n := printNatLn n >> run f (f n);
|
||||
| (suc zero) := printNatLn 1 >>> printStringLn "Finished!"
|
||||
| n := printNatLn n >>> run f (f n);
|
||||
|
||||
welcome : String :=
|
||||
"Collatz calculator\n------------------\n\nType a number then ENTER";
|
||||
@ -22,7 +22,7 @@ resultHeading : String := "Collatz sequence:";
|
||||
|
||||
main : IO :=
|
||||
printStringLn welcome
|
||||
>> readLn
|
||||
>>> readLn
|
||||
λ {s :=
|
||||
printStringLn resultHeading
|
||||
>> run collatz (stringToNat s)};
|
||||
>>> run collatz (stringToNat s)};
|
||||
|
@ -8,4 +8,5 @@ fib : Nat → Nat → Nat → Nat
|
||||
|
||||
fibonacci (n : Nat) : Nat := fib n 0 1;
|
||||
|
||||
main : IO := readLn (printNatLn ∘ fibonacci ∘ stringToNat);
|
||||
main : IO :=
|
||||
readLn (stringToNat >> fibonacci >> printNatLn);
|
||||
|
@ -17,7 +17,7 @@ prompt (x : GameState) : String :=
|
||||
++str ": ";
|
||||
|
||||
nextMove (s : GameState) : String → GameState :=
|
||||
flip playMove s ∘ validMove ∘ stringToNat;
|
||||
stringToNat >> validMove >> flip playMove s;
|
||||
|
||||
--- Main loop
|
||||
terminating
|
||||
@ -30,12 +30,13 @@ run : GameState → IO
|
||||
++str msg)
|
||||
| (state b p (continue msg)) :=
|
||||
printString (msg ++str prompt (state b p noError))
|
||||
>> readLn (run ∘ nextMove (state b p noError))
|
||||
| x := printString (prompt x) >> readLn (run ∘ nextMove x);
|
||||
>>> readLn (run << nextMove (state b p noError))
|
||||
| x :=
|
||||
printString (prompt x) >>> readLn (run << nextMove x);
|
||||
|
||||
--- The welcome message
|
||||
welcome : String :=
|
||||
"MiniTicTacToe\n-------------\n\nType a number then ENTER to make a move";
|
||||
|
||||
--- The entry point of the program
|
||||
main : IO := printStringLn welcome >> run beginState;
|
||||
main : IO := printStringLn welcome >>> run beginState;
|
||||
|
@ -1 +1 @@
|
||||
Subproject commit 73ecbc57738f4bde6f4f39636436ba38504b33f6
|
||||
Subproject commit 00f6f503dbc2cfa72bd469fb8ce7edd0e9730639
|
@ -327,7 +327,7 @@ tests =
|
||||
$(mkRelFile "test050.juvix")
|
||||
$(mkRelFile "out/test050.out"),
|
||||
posTest
|
||||
"Test051: Local recursive function using IO >>"
|
||||
"Test051: Local recursive function using IO >>>"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test051.juvix")
|
||||
$(mkRelFile "out/test051.out"),
|
||||
|
@ -14,7 +14,7 @@ import Stdlib.Debug.Trace open;
|
||||
|
||||
main : Nat :=
|
||||
trace (mod 3 2)
|
||||
>>> trace (div 18 4)
|
||||
>>> trace (mod 18 4)
|
||||
>>> trace (div 16 4)
|
||||
>>> mod 16 4;
|
||||
>-> trace (div 18 4)
|
||||
>-> trace (mod 18 4)
|
||||
>-> trace (div 16 4)
|
||||
>-> mod 16 4;
|
||||
|
@ -10,5 +10,5 @@ loop : Nat := loop;
|
||||
main : Bool :=
|
||||
trace
|
||||
(if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
|
||||
>>> trace (2 > 0 || loop == 0)
|
||||
>>> 2 < 0 && loop == 0;
|
||||
>-> trace (2 > 0 || loop == 0)
|
||||
>-> 2 < 0 && loop == 0;
|
||||
|
@ -20,11 +20,11 @@ lst : List Nat := 0 :: 1 :: nil;
|
||||
|
||||
main : List Nat :=
|
||||
trace (null lst)
|
||||
>>> trace (null (nil {Nat}))
|
||||
>>> trace (head 1 lst)
|
||||
>>> trace (tail lst)
|
||||
>>> trace (head 0 (tail lst))
|
||||
>>> trace (map ((+) 1) lst)
|
||||
>>> map' ((+) 1) lst
|
||||
>-> trace (null (nil {Nat}))
|
||||
>-> trace (head 1 lst)
|
||||
>-> trace (tail lst)
|
||||
>-> trace (head 0 (tail lst))
|
||||
>-> trace (map ((+) 1) lst)
|
||||
>-> map' ((+) 1) lst
|
||||
-- TODO: Restore when anoma backend supports strings
|
||||
-- >>> runPartial λ {{{_}} := map'' ((+) 1) lst};
|
||||
-- >-> runPartial λ {{{_}} := map'' ((+) 1) lst};
|
||||
|
@ -18,6 +18,6 @@ fact : Nat → Nat := fact' 1;
|
||||
|
||||
main (n : Nat) : Nat :=
|
||||
trace (sum n)
|
||||
>>> trace (fact 5)
|
||||
>>> trace (fact 10)
|
||||
>>> fact 12;
|
||||
>-> trace (fact 5)
|
||||
>-> trace (fact 10)
|
||||
>-> fact 12;
|
||||
|
@ -12,5 +12,5 @@ fib : Nat → Nat := fib' 0 1;
|
||||
|
||||
main : Nat :=
|
||||
trace (fib 10)
|
||||
>>> trace (fib 100)
|
||||
>>> fib 1000;
|
||||
>-> trace (fib 100)
|
||||
>-> fib 1000;
|
||||
|
@ -32,7 +32,7 @@ combineDigits (xs : List Nat) : Nat := for (acc := 0) (x in xs) acc * 10 + x;
|
||||
|
||||
main : Nat :=
|
||||
trace (combineDigits (preorder (gen 3)))
|
||||
>>> trace (combineDigits (preorder (gen 4)))
|
||||
>>> trace (combineDigits (preorder (gen 5)))
|
||||
>>> trace (combineDigits (preorder (gen 6)))
|
||||
>>> combineDigits (preorder (gen 7));
|
||||
>-> trace (combineDigits (preorder (gen 4)))
|
||||
>-> trace (combineDigits (preorder (gen 5)))
|
||||
>-> trace (combineDigits (preorder (gen 6)))
|
||||
>-> combineDigits (preorder (gen 7));
|
||||
|
@ -16,6 +16,6 @@ f : Nat → Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (f 5 6)
|
||||
>>> trace (f 6 5)
|
||||
>>> trace (f 10 5)
|
||||
>>> f 11 5;
|
||||
>-> trace (f 6 5)
|
||||
>-> trace (f 10 5)
|
||||
>-> f 11 5;
|
||||
|
@ -24,13 +24,13 @@ vy : Nat := 7;
|
||||
|
||||
main : Nat :=
|
||||
trace (func (div y x))
|
||||
>>> -- 17 div 5 + 4 = 7
|
||||
>-> -- 17 div 5 + 4 = 7
|
||||
trace
|
||||
(y + x * z)
|
||||
>>> -- 17
|
||||
>-> -- 17
|
||||
trace
|
||||
(vx + vy * (z + 1))
|
||||
>>> -- 37
|
||||
>-> -- 37
|
||||
f
|
||||
(h g 2 3)
|
||||
4;
|
||||
|
@ -23,19 +23,19 @@ h : Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (f 100 500)
|
||||
>>> -- 600
|
||||
>-> -- 600
|
||||
trace
|
||||
(f 5 0)
|
||||
>>> -- 25
|
||||
>-> -- 25
|
||||
trace
|
||||
(f 5 5)
|
||||
>>> -- 30
|
||||
>-> -- 30
|
||||
trace
|
||||
(h 10)
|
||||
>>> -- 45
|
||||
>-> -- 45
|
||||
trace
|
||||
(g 10 h)
|
||||
>>> -- 55
|
||||
>-> -- 55
|
||||
g
|
||||
3
|
||||
(f 10);
|
||||
|
@ -16,11 +16,11 @@ subp : Nat → Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (f91 101)
|
||||
>>> trace (f91 95)
|
||||
>>> trace (f91 16)
|
||||
>>> trace (f91 5)
|
||||
>>> trace (subp 101 1)
|
||||
>>> trace (subp 11 5)
|
||||
>>> trace (subp 10 4)
|
||||
>>> trace (subp 1000 600)
|
||||
>>> subp 10000 6000;
|
||||
>-> trace (f91 95)
|
||||
>-> trace (f91 16)
|
||||
>-> trace (f91 5)
|
||||
>-> trace (subp 101 1)
|
||||
>-> trace (subp 11 5)
|
||||
>-> trace (subp 10 4)
|
||||
>-> trace (subp 1000 600)
|
||||
>-> subp 10000 6000;
|
||||
|
@ -18,4 +18,4 @@ power' : Nat → Nat → Nat → Nat
|
||||
power : Nat → Nat → Nat := power' 1;
|
||||
|
||||
main : Nat :=
|
||||
trace (power 2 3) >>> trace (power 3 7) >>> power 5 11;
|
||||
trace (power 2 3) >-> trace (power 3 7) >-> power 5 11;
|
||||
|
@ -17,12 +17,12 @@ sum' : Nat → Nat
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (h :: t) :=
|
||||
printNat h >> printString " :: " >> printListNatLn t;
|
||||
printNat h >>> printString " :: " >>> printListNatLn t;
|
||||
|
||||
main (n : Nat) : Nat :=
|
||||
trace (gen 10)
|
||||
>>> trace (reverse (gen 10))
|
||||
>>> trace (filter ((<) 5) (gen 10))
|
||||
>>> trace (reverse (map (flip sub 1) (gen 10)))
|
||||
>>> trace (sum n)
|
||||
>>> sum' n;
|
||||
>-> trace (reverse (gen 10))
|
||||
>-> trace (filter ((<) 5) (gen 10))
|
||||
>-> trace (reverse (map (flip sub 1) (gen 10)))
|
||||
>-> trace (sum n)
|
||||
>-> sum' n;
|
||||
|
@ -17,4 +17,4 @@ terminating
|
||||
h : Nat → Nat
|
||||
| x := if (x < 1) 1 (x * f (sub x 1));
|
||||
|
||||
main : Nat := trace (f 5) >>> trace (f 10) >>> f 20;
|
||||
main : Nat := trace (f 5) >-> trace (f 10) >-> f 20;
|
||||
|
@ -11,7 +11,7 @@ gcd : Nat → Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (gcd (3 * 7 * 2) (7 * 2 * 11))
|
||||
>>> trace (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5))
|
||||
>>> trace (gcd 3 7)
|
||||
>>> trace (gcd 7 3)
|
||||
>>> gcd (11 * 7 * 3) (2 * 5 * 13);
|
||||
>-> trace (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5))
|
||||
>-> trace (gcd 3 7)
|
||||
>-> trace (gcd 7 3)
|
||||
>-> gcd (11 * 7 * 3) (2 * 5 * 13);
|
||||
|
@ -30,7 +30,7 @@ drop_front : {A : Type} → Queue A → Queue A
|
||||
| nil := queue (reverse (qsnd q')) nil
|
||||
| _ := q';
|
||||
|
||||
pop_front {A} : Queue A -> Maybe (A × Queue A)
|
||||
pop_front {A} : Queue A -> Maybe (Pair A (Queue A))
|
||||
| (queue xs ys) :=
|
||||
case xs of
|
||||
| h :: t := just (h, queue t ys)
|
||||
|
@ -10,17 +10,17 @@ czero : Num
|
||||
| {_} f x := x;
|
||||
|
||||
csuc : Num → Num
|
||||
| n {_} f := f ∘ n {_} f;
|
||||
| n {_} f := f << n {_} f;
|
||||
|
||||
num : Nat → Num
|
||||
| zero := czero
|
||||
| (suc n) := csuc (num n);
|
||||
|
||||
add : Num → Num → Num
|
||||
| n m {_} f := n {_} f ∘ m {_} f;
|
||||
| n m {_} f := n {_} f << m {_} f;
|
||||
|
||||
mul : Num → Num → Num
|
||||
| n m {_} := n {_} ∘ m {_};
|
||||
| n m {_} := n {_} << m {_};
|
||||
|
||||
isZero : Num → Bool
|
||||
| n := n {_} (const false) true;
|
||||
@ -30,5 +30,5 @@ toNat : Num → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (toNat (num 7))
|
||||
>>> trace (toNat (add (num 7) (num 3)))
|
||||
>>> toNat (mul (num 7) (num 3));
|
||||
>-> trace (toNat (add (num 7) (num 3)))
|
||||
>-> toNat (mul (num 7) (num 3));
|
||||
|
@ -45,4 +45,4 @@ primes : Unit → Stream := eratostenes (numbers 2);
|
||||
|
||||
main (n1 n2 : Nat) : Nat :=
|
||||
trace (snth n1 primes)
|
||||
>>> snth n2 primes;
|
||||
>-> snth n2 primes;
|
||||
|
@ -11,7 +11,7 @@ ack : Nat → Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (ack 0 7)
|
||||
>>> trace (ack 1 7)
|
||||
>>> trace (ack 1 13)
|
||||
>>> trace (ack 2 7)
|
||||
>>> ack 2 13;
|
||||
>-> trace (ack 1 7)
|
||||
>-> trace (ack 1 13)
|
||||
>-> trace (ack 2 7)
|
||||
>-> ack 2 13;
|
||||
|
@ -8,7 +8,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A
|
||||
-- clauses with differing number of patterns not yet supported
|
||||
-- iterate f zero x := x;
|
||||
| f zero := id
|
||||
| f (suc n) := f ∘ iterate f n;
|
||||
| f (suc n) := f << iterate f n;
|
||||
|
||||
plus : Nat → Nat → Nat := iterate suc;
|
||||
|
||||
@ -23,6 +23,6 @@ ackermann : Nat → Nat → Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (plus 3 7)
|
||||
>>> trace (mult 3 7)
|
||||
>>> trace (exp 3 7)
|
||||
>>> ackermann 1 13;
|
||||
>-> trace (mult 3 7)
|
||||
>-> trace (exp 3 7)
|
||||
>-> ackermann 1 13;
|
||||
|
@ -4,7 +4,7 @@ module test032;
|
||||
import Stdlib.Prelude open;
|
||||
import Stdlib.Debug.Trace open;
|
||||
|
||||
split : {A : Type} → Nat → List A → List A × List A
|
||||
split : {A : Type} → Nat → List A → Pair (List A) (List A)
|
||||
| zero xs := nil, xs
|
||||
| (suc n) nil := nil, nil
|
||||
| (suc n) (x :: xs) :=
|
||||
@ -46,5 +46,5 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat)
|
||||
|
||||
main : List Nat :=
|
||||
trace (take 10 (uniq (sort (flatten (gen2 nil 6 10)))))
|
||||
>>> trace (take 10 (uniq (sort (flatten (gen2 nil 7 10)))))
|
||||
>>> take 10 (uniq (sort (flatten (gen2 nil 6 20))));
|
||||
>-> trace (take 10 (uniq (sort (flatten (gen2 nil 7 10)))))
|
||||
>-> take 10 (uniq (sort (flatten (gen2 nil 6 20))));
|
||||
|
@ -10,24 +10,24 @@ f : (Nat → Nat) → Nat
|
||||
f' : Nat → Nat
|
||||
| x := f ((+) x);
|
||||
|
||||
g : (Nat → Nat × Nat) → Nat × Nat
|
||||
g : (Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 2;
|
||||
|
||||
g' : Nat → Nat × Nat
|
||||
g' : Nat → Pair Nat Nat
|
||||
| x := g ((,) x);
|
||||
|
||||
f1' : Nat → Nat → Nat
|
||||
| x y := f ((+) (div x y));
|
||||
|
||||
g1' : Nat → Nat → Nat × Nat
|
||||
g1' : Nat → Nat → Pair Nat Nat
|
||||
| x y := g ((,) (div x y));
|
||||
|
||||
h : (Nat → Nat → Nat × Nat) → Nat × Nat
|
||||
h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 1 2;
|
||||
|
||||
main : Nat × Nat :=
|
||||
main : Pair Nat Nat :=
|
||||
trace (f' 7)
|
||||
>>> trace (g' 7)
|
||||
>>> trace (f1' 7 2)
|
||||
>>> trace (g1' 7 2)
|
||||
>>> h (,);
|
||||
>-> trace (g' 7)
|
||||
>-> trace (f1' 7 2)
|
||||
>-> trace (g1' 7 2)
|
||||
>-> h (,);
|
||||
|
@ -22,8 +22,8 @@ mutrec : Nat :=
|
||||
terminating
|
||||
h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
|
||||
in trace (f 5)
|
||||
>>> trace (f 10)
|
||||
>>> trace (g 5)
|
||||
>>> h 5;
|
||||
>-> trace (f 10)
|
||||
>-> trace (g 5)
|
||||
>-> h 5;
|
||||
|
||||
main : Nat := trace (sum 1000) >>> mutrec;
|
||||
main : Nat := trace (sum 1000) >-> mutrec;
|
||||
|
@ -43,8 +43,8 @@ h : Nat -> Nat
|
||||
|
||||
main : Nat :=
|
||||
trace (sum2 (lgen 5))
|
||||
>>> trace (f (gen 10))
|
||||
>>> trace (f (gen 15))
|
||||
>>> trace (f (gen 16))
|
||||
>>> trace (h 5)
|
||||
>>> h 3;
|
||||
>-> trace (f (gen 10))
|
||||
>-> trace (f (gen 15))
|
||||
>-> trace (f (gen 16))
|
||||
>-> trace (h 5)
|
||||
>-> h 3;
|
||||
|
@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A
|
||||
f : Nat → Nat := suc;
|
||||
|
||||
g : Nat → Nat → Nat
|
||||
| z := f ∘ flip sub z;
|
||||
| z := f << flip sub z;
|
||||
|
||||
g' : Nat → Nat → Nat
|
||||
| z := f ∘ λ {x := sub x z};
|
||||
| z := f << λ {x := sub x z};
|
||||
|
||||
h : Nat → Nat := f ∘ g 3;
|
||||
h : Nat → Nat := f << g 3;
|
||||
|
||||
j : Nat → Nat → Nat := g';
|
||||
|
||||
|
@ -15,4 +15,4 @@ main : Bool :=
|
||||
| zero := true
|
||||
| (suc n) := not (odd n);
|
||||
plusOne (n : Ty) : Ty := n + 1;
|
||||
in trace (odd (plusOne 13)) >>> even (plusOne 12);
|
||||
in trace (odd (plusOne 13)) >-> even (plusOne 12);
|
||||
|
@ -10,22 +10,22 @@ f : Int -> Nat
|
||||
|
||||
main : Int :=
|
||||
trace (ofNat 1)
|
||||
>>> trace (ofNat (suc zero))
|
||||
>>> trace (f -1)
|
||||
>>> trace (f (ofNat (suc zero)))
|
||||
>>> trace (f (negSuc (suc zero)))
|
||||
>>> trace (1 == -1)
|
||||
>>> trace (neg -1)
|
||||
>>> trace
|
||||
>-> trace (ofNat (suc zero))
|
||||
>-> trace (f -1)
|
||||
>-> trace (f (ofNat (suc zero)))
|
||||
>-> trace (f (negSuc (suc zero)))
|
||||
>-> trace (1 == -1)
|
||||
>-> trace (neg -1)
|
||||
>-> trace
|
||||
(let
|
||||
g : Int -> Int := neg;
|
||||
in g -1)
|
||||
>>> trace (-2 * -2)
|
||||
>>> trace (nonNeg 0)
|
||||
>>> trace (nonNeg -1)
|
||||
>>> trace (0 < 0)
|
||||
>>> trace (0 <= 0)
|
||||
>>> trace (0 < 1)
|
||||
>>> trace (-1 <= 0)
|
||||
>>> trace (mod 4 -3)
|
||||
>>> div -6 -3;
|
||||
>-> trace (-2 * -2)
|
||||
>-> trace (nonNeg 0)
|
||||
>-> trace (nonNeg -1)
|
||||
>-> trace (0 < 0)
|
||||
>-> trace (0 <= 0)
|
||||
>-> trace (0 < 1)
|
||||
>-> trace (-1 <= 0)
|
||||
>-> trace (mod 4 -3)
|
||||
>-> div -6 -3;
|
||||
|
@ -36,12 +36,12 @@ myfor2
|
||||
syntax iterator myzip2 {init := 2; range := 2};
|
||||
myzip2
|
||||
: {A A' B C : Type}
|
||||
→ (A → A' → B → C → A × A')
|
||||
→ (A → A' → B → C → Pair A A')
|
||||
→ A
|
||||
→ A'
|
||||
→ List B
|
||||
→ List C
|
||||
→ A × A'
|
||||
→ Pair A A'
|
||||
| f a b xs ys :=
|
||||
myfor (acc, acc' := a, b) (x, y in zip xs ys)
|
||||
f acc acc' x y;
|
||||
|
@ -3,9 +3,9 @@ module test055;
|
||||
|
||||
import Stdlib.Prelude open;
|
||||
|
||||
type Pair :=
|
||||
| pair : Nat -> Nat -> Pair;
|
||||
type Pair' :=
|
||||
| pair : Nat -> Nat -> Pair';
|
||||
|
||||
main : List (Pair × Nat) × List Pair :=
|
||||
main : Pair (List (Pair Pair' Nat)) (List Pair') :=
|
||||
(pair 1 2, 3) :: (pair 2 3, 4) :: nil
|
||||
, pair 1 2 :: pair 2 3 :: nil;
|
||||
|
@ -10,13 +10,13 @@ type Triple (A B C : Type) :=
|
||||
thd : C
|
||||
};
|
||||
|
||||
type Pair (A B : Type) :=
|
||||
type Pair' (A B : Type) :=
|
||||
mkPair {
|
||||
fst : A;
|
||||
snd : B
|
||||
};
|
||||
|
||||
mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
|
||||
mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
|
||||
| mkPair@{fst := mkPair@{fst; snd := nil};
|
||||
snd := zero :: _} := fst
|
||||
| x := case x of {_ := false};
|
||||
|
@ -60,18 +60,18 @@ f5 {A} {{T A}} (n : Nat) (a : A) : Nat := n + T.toNat a;
|
||||
|
||||
main : Nat :=
|
||||
trace (T.toNat true)
|
||||
>>> trace (f false)
|
||||
>>> trace (T.toNat 3)
|
||||
>>> trace (T.toNat (g {Nat}))
|
||||
>>> trace (T.toNat [true; false])
|
||||
>>> trace (T.toNat [1; 2; 3])
|
||||
>>> trace
|
||||
>-> trace (f false)
|
||||
>-> trace (T.toNat 3)
|
||||
>-> trace (T.toNat (g {Nat}))
|
||||
>-> trace (T.toNat [true; false])
|
||||
>-> trace (T.toNat [1; 2; 3])
|
||||
>-> trace
|
||||
(let
|
||||
f (_ : Unit) : Nat := 5;
|
||||
in T.toNat f)
|
||||
>>> trace (f' [1; 2])
|
||||
>>> trace (f'' [true; false])
|
||||
>>> trace (f'3 [just true; nothing; just false])
|
||||
>>> trace (f'4 [just [1]; nothing; just [2; 3]])
|
||||
>>> trace (f'3 true)
|
||||
>>> f5 1 [0; 1; 1];
|
||||
>-> trace (f' [1; 2])
|
||||
>-> trace (f'' [true; false])
|
||||
>-> trace (f'3 [just true; nothing; just false])
|
||||
>-> trace (f'4 [just [1]; nothing; just [2; 3]])
|
||||
>-> trace (f'3 true)
|
||||
>-> f5 1 [0; 1; 1];
|
||||
|
@ -78,10 +78,10 @@ h {A} {{U2 A}} : A -> A := f;
|
||||
|
||||
main : Nat :=
|
||||
trace (T1.pp 0)
|
||||
>>> trace (T2.pp 1)
|
||||
>>> trace (T3.pp 2)
|
||||
>>> trace (T4.pp 3)
|
||||
>>> trace (U.pp 4)
|
||||
>>> trace (f 5)
|
||||
>>> trace (g {{mkU1 id}} 6)
|
||||
>>> h 7;
|
||||
>-> trace (T2.pp 1)
|
||||
>-> trace (T3.pp 2)
|
||||
>-> trace (T4.pp 3)
|
||||
>-> trace (U.pp 4)
|
||||
>-> trace (f 5)
|
||||
>-> trace (g {{mkU1 id}} 6)
|
||||
>-> h 7;
|
||||
|
@ -3,7 +3,7 @@ module test069;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -3,7 +3,7 @@ module test071;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -16,6 +16,6 @@ type Monad (f : Type -> Type) :=
|
||||
|
||||
open Monad public;
|
||||
|
||||
syntax operator >> bind;
|
||||
>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
syntax operator >>> bind;
|
||||
>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
A) (y : M B) : M B := x >>= λ {_ := y};
|
||||
|
@ -10,7 +10,7 @@ instance
|
||||
Reader-Functor {R : Type} : Functor (Reader R) :=
|
||||
mkFunctor@{
|
||||
<$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B
|
||||
| (mkReader ra) := mkReader (f ∘ ra)
|
||||
| (mkReader ra) := mkReader (f << ra)
|
||||
};
|
||||
|
||||
instance
|
||||
|
@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}}
|
||||
monad := ReaderT-Monad;
|
||||
ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s};
|
||||
reader {A : Type} (f : S → A) : ReaderT S M A :=
|
||||
mkReaderT (MMonad.return ∘ f)
|
||||
mkReaderT (MMonad.return << f)
|
||||
};
|
||||
|
||||
import MonadState open;
|
||||
import StateT open;
|
||||
import Identity open;
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
liftReaderT {R A : Type} {M : Type → Type} (m : M A)
|
||||
: ReaderT R M A := mkReaderT (const m);
|
||||
@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat :=
|
||||
monadic : ReaderT Nat (StateT Nat Identity) Nat :=
|
||||
askNat
|
||||
>>= λ {n :=
|
||||
liftReaderT (modify λ {m := m * n}) >> liftReaderT get};
|
||||
liftReaderT (modify λ {m := m * n}) >>> liftReaderT get};
|
||||
|
||||
main : Nat :=
|
||||
runIdentity (evalState 2 (runReader 5 monadic));
|
||||
@ -87,6 +87,6 @@ main : Nat :=
|
||||
-- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) :=
|
||||
-- mkMonadReader@{
|
||||
-- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}};
|
||||
-- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader;
|
||||
-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader;
|
||||
-- ask : StateT S M R := liftStateT MonadReader.ask;
|
||||
-- };
|
||||
|
@ -2,7 +2,7 @@ module State;
|
||||
|
||||
import Monad open;
|
||||
import Functor open;
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
type State (S A : Type) := mkState {runState : S -> A × S};
|
||||
|
||||
|
@ -4,15 +4,15 @@ import Monad open;
|
||||
import Monad open using {module Monad as MMonad};
|
||||
import Functor open;
|
||||
import Functor open using {module Functor as MFunctor};
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
type StateT (S : Type) (M : Type → Type) (A : Type) :=
|
||||
mkStateT {runStateT : S → M (A × S)};
|
||||
mkStateT {runStateT : S → M (Pair A S)};
|
||||
|
||||
runState {S A : Type} {M : Type → Type} (s : S) (m : StateT
|
||||
S
|
||||
M
|
||||
A) : M (A × S) := StateT.runStateT m s;
|
||||
A) : M (Pair A S) := StateT.runStateT m s;
|
||||
|
||||
evalState {S A : Type} {M : Type → Type} {{Functor
|
||||
M}} (s : S) (m : StateT S M A) : M A :=
|
||||
|
@ -7,4 +7,4 @@ builtin anoma-get
|
||||
axiom anomaGet : {Value Key : Type} -> Key -> Value;
|
||||
|
||||
main (k1 : Nat) (k2 : List Nat) : List Nat :=
|
||||
trace (anomaGet {Nat} k1) >>> anomaGet k2;
|
||||
trace (anomaGet {Nat} k1) >-> anomaGet k2;
|
||||
|
@ -10,8 +10,8 @@ main : Nat :=
|
||||
-- jam 0 == 2
|
||||
trace (anomaEncode 0)
|
||||
-- jam [1 2 0] == 84081
|
||||
>>> trace (anomaEncode [1;2])
|
||||
>-> trace (anomaEncode [1;2])
|
||||
-- jam [1 2] == 4657
|
||||
>>> trace (anomaEncode (1 , 2))
|
||||
>-> trace (anomaEncode (1 , 2))
|
||||
-- jam 1 == 12
|
||||
>>> anomaEncode false;
|
||||
>-> anomaEncode false;
|
||||
|
@ -10,8 +10,8 @@ main : Bool :=
|
||||
-- cue 2 == 0
|
||||
trace (anomaDecode {Nat} 2)
|
||||
-- cue 84081 == [1 2 0]
|
||||
>>> trace (anomaDecode {List Nat} 84081)
|
||||
>-> trace (anomaDecode {List Nat} 84081)
|
||||
-- cue 4657 == [1 2]
|
||||
>>> trace (anomaDecode {Nat × Nat} 4657)
|
||||
>-> trace (anomaDecode {Pair Nat Nat} 4657)
|
||||
-- cue 12 == 1
|
||||
>>> anomaDecode {Bool} 12;
|
||||
>-> anomaDecode {Bool} 12;
|
||||
|
@ -7,7 +7,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A
|
||||
-- clauses with differing number of patterns not yet supported
|
||||
-- iterate f zero x := x;
|
||||
| f zero := id
|
||||
| f (suc n) := f ∘ iterate f n;
|
||||
| f (suc n) := f << iterate f n;
|
||||
|
||||
plus : Nat → Nat → Nat := iterate suc;
|
||||
|
||||
|
@ -3,7 +3,7 @@ module test032;
|
||||
|
||||
import Stdlib.Prelude open;
|
||||
|
||||
split : {A : Type} → Nat → List A → List A × List A
|
||||
split : {A : Type} → Nat → List A → Pair (List A) (List A)
|
||||
| zero xs := nil, xs
|
||||
| (suc n) nil := nil, nil
|
||||
| (suc n) (x :: xs) :=
|
||||
@ -46,7 +46,7 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat)
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printListNatLn xs;
|
||||
printNat x >>> printString " :: " >>> printListNatLn xs;
|
||||
|
||||
sum : List Nat → Nat
|
||||
| nil := 0
|
||||
|
@ -9,19 +9,19 @@ f : (Nat → Nat) → Nat
|
||||
f' : Nat → Nat
|
||||
| x := f ((+) x);
|
||||
|
||||
g : (Nat → Nat × Nat) → Nat × Nat
|
||||
g : (Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 2;
|
||||
|
||||
g' : Nat → Nat × Nat
|
||||
g' : Nat → Pair Nat Nat
|
||||
| x := g ((,) x);
|
||||
|
||||
f1' : Nat → Nat → Nat
|
||||
| x y := f ((+) (div x y));
|
||||
|
||||
g1' : Nat → Nat → Nat × Nat
|
||||
g1' : Nat → Nat → Pair Nat Nat
|
||||
| x y := g ((,) (div x y));
|
||||
|
||||
h : (Nat → Nat → Nat × Nat) → Nat × Nat
|
||||
h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 1 2;
|
||||
|
||||
main : Nat :=
|
||||
|
@ -44,7 +44,7 @@ h : Nat -> Nat
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printListNatLn xs;
|
||||
printNat x >>> printString " :: " >>> printListNatLn xs;
|
||||
|
||||
main : Nat :=
|
||||
head 0 (sum2 (lgen 5))
|
||||
|
@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A
|
||||
f : Nat → Nat := suc;
|
||||
|
||||
g : Nat → Nat → Nat
|
||||
| z := f ∘ flip sub z;
|
||||
| z := f << flip sub z;
|
||||
|
||||
g' : Nat → Nat → Nat
|
||||
| z := f ∘ λ {x := sub x z};
|
||||
| z := f << λ {x := sub x z};
|
||||
|
||||
h : Nat → Nat := f ∘ g 3;
|
||||
h : Nat → Nat := f << g 3;
|
||||
|
||||
j : Nat → Nat → Nat := g';
|
||||
|
||||
|
@ -36,12 +36,12 @@ myfor2
|
||||
syntax iterator myzip2 {init := 2; range := 2};
|
||||
myzip2
|
||||
: {A A' B C : Type}
|
||||
→ (A → A' → B → C → A × A')
|
||||
→ (A → A' → B → C → Pair A A')
|
||||
→ A
|
||||
→ A'
|
||||
→ List B
|
||||
→ List C
|
||||
→ A × A'
|
||||
→ Pair A A'
|
||||
| f a b xs ys :=
|
||||
myfor (acc, acc' := a, b) (x, y in zip xs ys)
|
||||
f acc acc' x y;
|
||||
|
@ -10,7 +10,7 @@ type Triple (A B C : Type) :=
|
||||
thd : C
|
||||
};
|
||||
|
||||
type Pair (A B : Type) :=
|
||||
type Pair' (A B : Type) :=
|
||||
mkPair {
|
||||
fst : A;
|
||||
snd : B
|
||||
@ -19,7 +19,7 @@ type Pair (A B : Type) :=
|
||||
sum : Triple Nat Nat Nat → Nat
|
||||
| mkTriple@{fst; snd; thd} := fst + snd + thd;
|
||||
|
||||
mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
|
||||
mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
|
||||
| mkPair@{fst := mkPair@{fst; snd := nil};
|
||||
snd := zero :: _} := fst
|
||||
| x := case x of {_ := false};
|
||||
@ -34,7 +34,7 @@ main : Nat :=
|
||||
};
|
||||
f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
|
||||
(@Triple{fst := fst * 10});
|
||||
in sum $ if
|
||||
in sum <| if
|
||||
(mf
|
||||
mkPair@{
|
||||
fst := mkPair true nil;
|
||||
|
@ -3,7 +3,7 @@ module test069;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -3,7 +3,7 @@ module test071;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -16,6 +16,6 @@ type Monad (f : Type -> Type) :=
|
||||
|
||||
open Monad public;
|
||||
|
||||
syntax operator >> bind;
|
||||
>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
syntax operator >>> bind;
|
||||
>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
A) (y : M B) : M B := x >>= λ {_ := y};
|
||||
|
@ -10,7 +10,7 @@ instance
|
||||
Reader-Functor {R : Type} : Functor (Reader R) :=
|
||||
mkFunctor@{
|
||||
<$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B
|
||||
| (mkReader ra) := mkReader (f ∘ ra)
|
||||
| (mkReader ra) := mkReader (f << ra)
|
||||
};
|
||||
|
||||
instance
|
||||
|
@ -52,13 +52,13 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}}
|
||||
monad := ReaderT-Monad;
|
||||
ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s};
|
||||
reader {A : Type} (f : S → A) : ReaderT S M A :=
|
||||
mkReaderT (MMonad.return ∘ f)
|
||||
mkReaderT (MMonad.return << f)
|
||||
};
|
||||
|
||||
import MonadState open;
|
||||
import StateT open;
|
||||
import Identity open;
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
liftReaderT {R A : Type} {M : Type → Type} (m : M A)
|
||||
: ReaderT R M A := mkReaderT (const m);
|
||||
@ -76,7 +76,7 @@ askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat :=
|
||||
monadic : ReaderT Nat (StateT Nat Identity) Nat :=
|
||||
askNat
|
||||
>>= λ {n :=
|
||||
liftReaderT (modify λ {m := m * n}) >> liftReaderT get};
|
||||
liftReaderT (modify λ {m := m * n}) >>> liftReaderT get};
|
||||
|
||||
main : Nat :=
|
||||
runIdentity (evalState 2 (runReader 5 monadic));
|
||||
@ -87,6 +87,6 @@ main : Nat :=
|
||||
-- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) :=
|
||||
-- mkMonadReader@{
|
||||
-- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}};
|
||||
-- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader;
|
||||
-- reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader;
|
||||
-- ask : StateT S M R := liftStateT MonadReader.ask;
|
||||
-- };
|
||||
|
@ -2,7 +2,7 @@ module State;
|
||||
|
||||
import Monad open;
|
||||
import Functor open;
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
type State (S A : Type) := mkState {runState : S -> A × S};
|
||||
|
||||
|
@ -4,15 +4,15 @@ import Monad open;
|
||||
import Monad open using {module Monad as MMonad};
|
||||
import Functor open;
|
||||
import Functor open using {module Functor as MFunctor};
|
||||
import Stdlib.Data.Product open;
|
||||
import Stdlib.Data.Pair open;
|
||||
|
||||
type StateT (S : Type) (M : Type → Type) (A : Type) :=
|
||||
mkStateT {runStateT : S → M (A × S)};
|
||||
mkStateT {runStateT : S → M (Pair A S)};
|
||||
|
||||
runState {S A : Type} {M : Type → Type} (s : S) (m : StateT
|
||||
S
|
||||
M
|
||||
A) : M (A × S) := StateT.runStateT m s;
|
||||
A) : M (Pair A S) := StateT.runStateT m s;
|
||||
|
||||
evalState {S A : Type} {M : Type → Type} {{Functor
|
||||
M}} (s : S) (m : StateT S M A) : M A :=
|
||||
|
@ -23,13 +23,13 @@ type ComplianceResult :=
|
||||
y : Field
|
||||
};
|
||||
|
||||
count : List (Field × Bool) -> Field
|
||||
count : List (Pair Field Bool) -> Field
|
||||
| [] := 0
|
||||
| ((h, b) :: t) := if b (h + count t) (count t);
|
||||
|
||||
main
|
||||
(input : Resource)
|
||||
(path : List (Field × Bool))
|
||||
(path : List (Pair Field Bool))
|
||||
: ComplianceResult :=
|
||||
mkResult@{
|
||||
cnt := count path;
|
||||
@ -44,7 +44,7 @@ main
|
||||
{-
|
||||
main
|
||||
(input : Resource)
|
||||
(path : List (Field × Bool))
|
||||
(path : List (Pair Field Bool))
|
||||
: Field :=
|
||||
count path;
|
||||
-}
|
||||
|
@ -13,7 +13,7 @@ import Stdlib.Prelude open;
|
||||
|
||||
main : IO :=
|
||||
printNatLn (mod 3 2)
|
||||
>> printNatLn (div 18 4)
|
||||
>> printNatLn (mod 18 4)
|
||||
>> printNatLn (div 16 4)
|
||||
>> printNatLn (mod 16 4);
|
||||
>>> printNatLn (div 18 4)
|
||||
>>> printNatLn (mod 18 4)
|
||||
>>> printNatLn (div 16 4)
|
||||
>>> printNatLn (mod 16 4);
|
||||
|
@ -5,8 +5,8 @@ import Stdlib.Prelude open;
|
||||
|
||||
main : IO :=
|
||||
printNat 1
|
||||
>> printNat 2
|
||||
>> printNat 3
|
||||
>> printNat 4
|
||||
>> printNat 5
|
||||
>> printString "\n";
|
||||
>>> printNat 2
|
||||
>>> printNat 3
|
||||
>>> printNat 4
|
||||
>>> printNat 5
|
||||
>>> printString "\n";
|
||||
|
@ -9,5 +9,5 @@ loop : Nat := loop;
|
||||
main : IO :=
|
||||
printNatLn
|
||||
(if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
|
||||
>> printBoolLn (2 > 0 || loop == 0)
|
||||
>> printBoolLn (2 < 0 && loop == 0);
|
||||
>>> printBoolLn (2 > 0 || loop == 0)
|
||||
>>> printBoolLn (2 < 0 && loop == 0);
|
||||
|
@ -18,17 +18,17 @@ lst : List Nat := 0 :: 1 :: nil;
|
||||
printNatList : List Nat → IO
|
||||
| nil := printString "nil"
|
||||
| (h :: t) :=
|
||||
printNat h >> printString " :: " >> printNatList t;
|
||||
printNat h >>> printString " :: " >>> printNatList t;
|
||||
|
||||
printNatListLn (lst : List Nat) : IO :=
|
||||
printNatList lst >> printString "\n";
|
||||
printNatList lst >>> printString "\n";
|
||||
|
||||
main : IO :=
|
||||
printBoolLn (null lst)
|
||||
>> printBoolLn (null (nil {Nat}))
|
||||
>> printNatLn (head 1 lst)
|
||||
>> printNatListLn (tail lst)
|
||||
>> printNatLn (head 0 (tail lst))
|
||||
>> printNatListLn (map ((+) 1) lst)
|
||||
>> printNatListLn (map' ((+) 1) lst)
|
||||
>> printNatListLn (runPartial (λ{{{_}} := map'' ((+) 1) lst}));
|
||||
>>> printBoolLn (null (nil {Nat}))
|
||||
>>> printNatLn (head 1 lst)
|
||||
>>> printNatListLn (tail lst)
|
||||
>>> printNatLn (head 0 (tail lst))
|
||||
>>> printNatListLn (map ((+) 1) lst)
|
||||
>>> printNatListLn (map' ((+) 1) lst)
|
||||
>>> printNatListLn (runPartial (λ{{{_}} := map'' ((+) 1) lst}));
|
||||
|
@ -17,6 +17,6 @@ fact : Nat → Nat := fact' 1;
|
||||
|
||||
main : IO :=
|
||||
printNatLn (sum 10000)
|
||||
>> printNatLn (fact 5)
|
||||
>> printNatLn (fact 10)
|
||||
>> printNatLn (fact 12);
|
||||
>>> printNatLn (fact 5)
|
||||
>>> printNatLn (fact 10)
|
||||
>>> printNatLn (fact 12);
|
||||
|
@ -11,5 +11,5 @@ fib : Nat → Nat := fib' 0 1;
|
||||
|
||||
main : IO :=
|
||||
printNatLn (fib 10)
|
||||
>> printNatLn (fib 100)
|
||||
>> printNatLn (fib 1000);
|
||||
>>> printNatLn (fib 100)
|
||||
>>> printNatLn (fib 1000);
|
||||
|
@ -20,19 +20,19 @@ gen : Nat → Tree
|
||||
|
||||
preorder : Tree → IO
|
||||
| leaf := printNat 0
|
||||
| (node1 c) := printNat 1 >> preorder c
|
||||
| (node2 l r) := printNat 2 >> preorder l >> preorder r
|
||||
| (node1 c) := printNat 1 >>> preorder c
|
||||
| (node2 l r) := printNat 2 >>> preorder l >>> preorder r
|
||||
| (node3 l m r) :=
|
||||
printNat 3 >> preorder l >> preorder m >> preorder r;
|
||||
printNat 3 >>> preorder l >>> preorder m >>> preorder r;
|
||||
|
||||
main : IO :=
|
||||
preorder (gen 3)
|
||||
>> printString "\n"
|
||||
>> preorder (gen 4)
|
||||
>> printString "\n"
|
||||
>> preorder (gen 5)
|
||||
>> printString "\n"
|
||||
>> preorder (gen 6)
|
||||
>> printString "\n"
|
||||
>> preorder (gen 7)
|
||||
>> printString "\n";
|
||||
>>> printString "\n"
|
||||
>>> preorder (gen 4)
|
||||
>>> printString "\n"
|
||||
>>> preorder (gen 5)
|
||||
>>> printString "\n"
|
||||
>>> preorder (gen 6)
|
||||
>>> printString "\n"
|
||||
>>> preorder (gen 7)
|
||||
>>> printString "\n";
|
||||
|
@ -15,6 +15,6 @@ f : Nat → Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (f 5 6)
|
||||
>> printNatLn (f 6 5)
|
||||
>> printNatLn (f 10 5)
|
||||
>> printNatLn (f 11 5);
|
||||
>>> printNatLn (f 6 5)
|
||||
>>> printNatLn (f 10 5)
|
||||
>>> printNatLn (f 11 5);
|
||||
|
@ -23,13 +23,13 @@ vy : Nat := 7;
|
||||
|
||||
main : IO :=
|
||||
printNatLn (func (div y x))
|
||||
>> -- 17 div 5 + 4 = 7
|
||||
>>> -- 17 div 5 + 4 = 7
|
||||
printNatLn
|
||||
(y + x * z)
|
||||
>> -- 17
|
||||
>>> -- 17
|
||||
printNatLn
|
||||
(vx + vy * (z + 1))
|
||||
>> -- 37
|
||||
>>> -- 37
|
||||
f
|
||||
(h g 2 3)
|
||||
4;
|
||||
|
@ -21,18 +21,18 @@ h : Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (f 100 500)
|
||||
>> -- 600
|
||||
>>> -- 600
|
||||
printNatLn
|
||||
(f 5 0)
|
||||
>> -- 25
|
||||
>>> -- 25
|
||||
printNatLn
|
||||
(f 5 5)
|
||||
>> -- 30
|
||||
>>> -- 30
|
||||
printNatLn
|
||||
(h 10)
|
||||
>> -- 45
|
||||
>>> -- 45
|
||||
printNatLn
|
||||
(g 10 h)
|
||||
>> -- 55
|
||||
>>> -- 55
|
||||
printNatLn
|
||||
(g 3 (f 10));
|
||||
|
@ -15,11 +15,11 @@ subp : Nat → Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (f91 101)
|
||||
>> printNatLn (f91 95)
|
||||
>> printNatLn (f91 16)
|
||||
>> printNatLn (f91 5)
|
||||
>> printNatLn (subp 101 1)
|
||||
>> printNatLn (subp 11 5)
|
||||
>> printNatLn (subp 10 4)
|
||||
>> printNatLn (subp 1000 600)
|
||||
>> printNatLn (subp 10000 6000);
|
||||
>>> printNatLn (f91 95)
|
||||
>>> printNatLn (f91 16)
|
||||
>>> printNatLn (f91 5)
|
||||
>>> printNatLn (subp 101 1)
|
||||
>>> printNatLn (subp 11 5)
|
||||
>>> printNatLn (subp 10 4)
|
||||
>>> printNatLn (subp 1000 600)
|
||||
>>> printNatLn (subp 10000 6000);
|
||||
|
@ -15,5 +15,5 @@ power : Nat → Nat → Nat := power' 1;
|
||||
|
||||
main : IO :=
|
||||
printNatLn (power 2 3)
|
||||
>> printNatLn (power 3 7)
|
||||
>> printNatLn (power 5 11);
|
||||
>>> printNatLn (power 3 7)
|
||||
>>> printNatLn (power 5 11);
|
||||
|
@ -16,13 +16,13 @@ sum' : Nat → Nat
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (h :: t) :=
|
||||
printNat h >> printString " :: " >> printListNatLn t;
|
||||
printNat h >>> printString " :: " >>> printListNatLn t;
|
||||
|
||||
main : IO :=
|
||||
printListNatLn (gen 10)
|
||||
>> printListNatLn (reverse (gen 10))
|
||||
>> printListNatLn (filter ((<) 5) (gen 10))
|
||||
>> printListNatLn (reverse (map (flip sub 1) (gen 10)))
|
||||
>> printNatLn (sum 10000)
|
||||
>> printNatLn (sum' 10000);
|
||||
>>> printListNatLn (reverse (gen 10))
|
||||
>>> printListNatLn (filter ((<) 5) (gen 10))
|
||||
>>> printListNatLn (reverse (map (flip sub 1) (gen 10)))
|
||||
>>> printNatLn (sum 10000)
|
||||
>>> printNatLn (sum' 10000);
|
||||
|
||||
|
@ -18,6 +18,6 @@ h : Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (f 5)
|
||||
>> printNatLn (f 10)
|
||||
>> printNatLn (f 20);
|
||||
>>> printNatLn (f 10)
|
||||
>>> printNatLn (f 20);
|
||||
|
||||
|
@ -13,8 +13,8 @@ gcd : Nat → Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (gcd (3 * 7 * 2) (7 * 2 * 11))
|
||||
>> printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5))
|
||||
>> printNatLn (gcd 3 7)
|
||||
>> printNatLn (gcd 7 3)
|
||||
>> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13));
|
||||
>>> printNatLn (gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5))
|
||||
>>> printNatLn (gcd 3 7)
|
||||
>>> printNatLn (gcd 7 3)
|
||||
>>> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13));
|
||||
|
||||
|
@ -52,7 +52,7 @@ f {{Partial}} : Nat → Queue Nat → List Nat
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (h :: t) :=
|
||||
printNat h >> printString " :: " >> printListNatLn t;
|
||||
printNat h >>> printString " :: " >>> printListNatLn t;
|
||||
|
||||
main : IO :=
|
||||
printListNatLn (runPartial λ {{{_}} := f 100 empty});
|
||||
|
@ -9,17 +9,17 @@ czero : Num
|
||||
| {_} f x := x;
|
||||
|
||||
csuc : Num → Num
|
||||
| n {_} f := f ∘ n {_} f;
|
||||
| n {_} f := f << n {_} f;
|
||||
|
||||
num : Nat → Num
|
||||
| zero := czero
|
||||
| (suc n) := csuc (num n);
|
||||
|
||||
add : Num → Num → Num
|
||||
| n m {_} f := n {_} f ∘ m {_} f;
|
||||
| n m {_} f := n {_} f << m {_} f;
|
||||
|
||||
mul : Num → Num → Num
|
||||
| n m {_} := n {_} ∘ m {_};
|
||||
| n m {_} := n {_} << m {_};
|
||||
|
||||
isZero : Num → Bool
|
||||
| n := n {_} (const false) true;
|
||||
@ -29,5 +29,5 @@ toNat : Num → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (toNat (num 7))
|
||||
>> printNatLn (toNat (add (num 7) (num 3)))
|
||||
>> printNatLn (toNat (mul (num 7) (num 3)));
|
||||
>>> printNatLn (toNat (add (num 7) (num 3)))
|
||||
>>> printNatLn (toNat (mul (num 7) (num 3)));
|
||||
|
@ -43,6 +43,6 @@ primes : Unit → Stream := eratostenes (numbers 2);
|
||||
|
||||
main : IO :=
|
||||
printNatLn (snth 10 primes)
|
||||
>> printNatLn (snth 50 primes)
|
||||
>> printNatLn (snth 100 primes)
|
||||
>> printNatLn (snth 200 primes);
|
||||
>>> printNatLn (snth 50 primes)
|
||||
>>> printNatLn (snth 100 primes)
|
||||
>>> printNatLn (snth 200 primes);
|
||||
|
@ -10,8 +10,8 @@ ack : Nat → Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (ack 0 7)
|
||||
>> printNatLn (ack 1 7)
|
||||
>> printNatLn (ack 1 13)
|
||||
>> printNatLn (ack 2 7)
|
||||
>> printNatLn (ack 2 13)
|
||||
>> printNatLn (ack 3 7);
|
||||
>>> printNatLn (ack 1 7)
|
||||
>>> printNatLn (ack 1 13)
|
||||
>>> printNatLn (ack 2 7)
|
||||
>>> printNatLn (ack 2 13)
|
||||
>>> printNatLn (ack 3 7);
|
||||
|
@ -7,7 +7,7 @@ iterate : {A : Type} → (A → A) → Nat → A → A
|
||||
-- clauses with differing number of patterns not yet supported
|
||||
-- iterate f zero x := x;
|
||||
| f zero := id
|
||||
| f (suc n) := f ∘ iterate f n;
|
||||
| f (suc n) := f << iterate f n;
|
||||
|
||||
plus : Nat → Nat → Nat := iterate suc;
|
||||
|
||||
@ -22,7 +22,7 @@ ackermann : Nat → Nat → Nat
|
||||
|
||||
main : IO :=
|
||||
printNatLn (plus 3 7)
|
||||
>> printNatLn (mult 3 7)
|
||||
>> printNatLn (exp 3 7)
|
||||
>> printNatLn (ackermann 3 7);
|
||||
>>> printNatLn (mult 3 7)
|
||||
>>> printNatLn (exp 3 7)
|
||||
>>> printNatLn (ackermann 3 7);
|
||||
|
||||
|
@ -14,6 +14,6 @@ mklst2 : Nat → List (List Nat)
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printListNatLn xs;
|
||||
printNat x >>> printString " :: " >>> printListNatLn xs;
|
||||
|
||||
main : IO := printListNatLn (flatten (mklst2 4));
|
||||
|
@ -3,7 +3,7 @@ module test032;
|
||||
|
||||
import Stdlib.Prelude open;
|
||||
|
||||
split : {A : Type} → Nat → List A → List A × List A
|
||||
split : {A : Type} → Nat → List A → Pair (List A) (List A)
|
||||
| zero xs := nil, xs
|
||||
| (suc n) nil := nil, nil
|
||||
| (suc n) (x :: xs) :=
|
||||
@ -46,12 +46,12 @@ gen2 : List (List Nat) → Nat → Nat → List (List Nat)
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printListNatLn xs;
|
||||
printNat x >>> printString " :: " >>> printListNatLn xs;
|
||||
|
||||
main : IO :=
|
||||
printListNatLn
|
||||
(take 10 (uniq (sort (flatten (gen2 nil 6 40)))))
|
||||
>> printListNatLn
|
||||
>>> printListNatLn
|
||||
(take 10 (uniq (sort (flatten (gen2 nil 9 80)))))
|
||||
>> printListNatLn
|
||||
>>> printListNatLn
|
||||
(take 10 (uniq (sort (flatten (gen2 nil 6 80)))));
|
||||
|
@ -9,33 +9,32 @@ f : (Nat → Nat) → Nat
|
||||
f' : Nat → Nat
|
||||
| x := f ((+) x);
|
||||
|
||||
g : (Nat → Nat × Nat) → Nat × Nat
|
||||
g : (Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 2;
|
||||
|
||||
g' : Nat → Nat × Nat
|
||||
g' : Nat → Pair Nat Nat
|
||||
| x := g ((,) x);
|
||||
|
||||
f1' : Nat → Nat → Nat
|
||||
| x y := f ((+) (div x y));
|
||||
|
||||
g1' : Nat → Nat → Nat × Nat
|
||||
g1' : Nat → Nat → Pair Nat Nat
|
||||
| x y := g ((,) (div x y));
|
||||
|
||||
h : (Nat → Nat → Nat × Nat) → Nat × Nat
|
||||
h : (Nat → Nat → Pair Nat Nat) → Pair Nat Nat
|
||||
| f := f 1 2;
|
||||
|
||||
printPairNatLn : Nat × Nat → IO
|
||||
printPairNatLn : Pair Nat Nat → IO
|
||||
| (x, y) :=
|
||||
printString "("
|
||||
>> printNat x
|
||||
>> printString ", "
|
||||
>> printNat y
|
||||
>> printStringLn ")";
|
||||
>>> printNat x
|
||||
>>> printString ", "
|
||||
>>> printNat y
|
||||
>>> printStringLn ")";
|
||||
|
||||
main : IO :=
|
||||
printNatLn (f' 7)
|
||||
>> printPairNatLn (g' 7)
|
||||
>> printNatLn (f1' 7 2)
|
||||
>> printPairNatLn (g1' 7 2)
|
||||
>> printPairNatLn (h (,));
|
||||
|
||||
>>> printPairNatLn (g' 7)
|
||||
>>> printNatLn (f1' 7 2)
|
||||
>>> printPairNatLn (g1' 7 2)
|
||||
>>> printPairNatLn (h (,));
|
||||
|
@ -21,8 +21,8 @@ mutrec : IO :=
|
||||
terminating
|
||||
h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
|
||||
in printNatLn (f 5)
|
||||
>> printNatLn (f 10)
|
||||
>> printNatLn (g 5)
|
||||
>> printNatLn (h 5);
|
||||
>>> printNatLn (f 10)
|
||||
>>> printNatLn (g 5)
|
||||
>>> printNatLn (h 5);
|
||||
|
||||
main : IO := printNatLn (sum 10000) >> mutrec;
|
||||
main : IO := printNatLn (sum 10000) >>> mutrec;
|
||||
|
@ -43,16 +43,16 @@ h : Nat -> Nat
|
||||
printListNatLn : List Nat → IO
|
||||
| nil := printStringLn "nil"
|
||||
| (x :: xs) :=
|
||||
printNat x >> printString " :: " >> printListNatLn xs;
|
||||
printNat x >>> printString " :: " >>> printListNatLn xs;
|
||||
|
||||
main : IO :=
|
||||
printListNatLn (sum2 (lgen 5))
|
||||
>> printNatLn (f (gen 10))
|
||||
>> printNatLn (f (gen 15))
|
||||
>> printNatLn (f (gen 16))
|
||||
>> printNatLn (f (gen 17))
|
||||
>> printNatLn (f (gen 18))
|
||||
>> printNatLn (f (gen 20))
|
||||
>> printNatLn (h 5)
|
||||
>> printNatLn (h 3);
|
||||
>>> printNatLn (f (gen 10))
|
||||
>>> printNatLn (f (gen 15))
|
||||
>>> printNatLn (f (gen 16))
|
||||
>>> printNatLn (f (gen 17))
|
||||
>>> printNatLn (f (gen 18))
|
||||
>>> printNatLn (f (gen 20))
|
||||
>>> printNatLn (h 5)
|
||||
>>> printNatLn (h 3);
|
||||
|
||||
|
@ -9,12 +9,12 @@ expand : {A : Type} → A → Nat → A
|
||||
f : Nat → Nat := suc;
|
||||
|
||||
g : Nat → Nat → Nat
|
||||
| z := f ∘ flip sub z;
|
||||
| z := f << flip sub z;
|
||||
|
||||
g' : Nat → Nat → Nat
|
||||
| z := f ∘ λ {x := sub x z};
|
||||
| z := f << λ {x := sub x z};
|
||||
|
||||
h : Nat → Nat := f ∘ g 3;
|
||||
h : Nat → Nat := f << g 3;
|
||||
|
||||
j : Nat → Nat → Nat := g';
|
||||
|
||||
|
@ -15,4 +15,4 @@ main : IO :=
|
||||
| (suc n) := not (odd n);
|
||||
plusOne (n : Ty) : Ty := n + 1;
|
||||
in printBoolLn (odd (plusOne 13))
|
||||
>> printBoolLn (even (plusOne 12));
|
||||
>>> printBoolLn (even (plusOne 12));
|
||||
|
@ -9,39 +9,39 @@ f : Int -> Nat
|
||||
|
||||
main : IO :=
|
||||
printStringLn (intToString 1)
|
||||
>> printStringLn (intToString -1)
|
||||
>> printIntLn (ofNat 1)
|
||||
>> printIntLn (negSuc 0)
|
||||
>> printIntLn (ofNat (suc zero))
|
||||
>> printIntLn (negSuc zero)
|
||||
>> printStringLn (natToString (f 1))
|
||||
>> printNatLn (f -1)
|
||||
>> printNatLn (f (ofNat (suc zero)))
|
||||
>> printNatLn (f (negSuc (suc zero)))
|
||||
>> printBoolLn (-1 == -2)
|
||||
>> printBoolLn (-1 == -1)
|
||||
>> printBoolLn (1 == 1)
|
||||
>> printBoolLn (-1 == 1)
|
||||
>> printIntLn (-1 + 1)
|
||||
>> printIntLn (negNat (suc zero))
|
||||
>> printIntLn
|
||||
>>> printStringLn (intToString -1)
|
||||
>>> printIntLn (ofNat 1)
|
||||
>>> printIntLn (negSuc 0)
|
||||
>>> printIntLn (ofNat (suc zero))
|
||||
>>> printIntLn (negSuc zero)
|
||||
>>> printStringLn (natToString (f 1))
|
||||
>>> printNatLn (f -1)
|
||||
>>> printNatLn (f (ofNat (suc zero)))
|
||||
>>> printNatLn (f (negSuc (suc zero)))
|
||||
>>> printBoolLn (-1 == -2)
|
||||
>>> printBoolLn (-1 == -1)
|
||||
>>> printBoolLn (1 == 1)
|
||||
>>> printBoolLn (-1 == 1)
|
||||
>>> printIntLn (-1 + 1)
|
||||
>>> printIntLn (negNat (suc zero))
|
||||
>>> printIntLn
|
||||
(let
|
||||
g : Nat -> Int := negNat;
|
||||
in g (suc zero))
|
||||
>> printIntLn (neg -1)
|
||||
>> printIntLn
|
||||
>>> printIntLn (neg -1)
|
||||
>>> printIntLn
|
||||
(let
|
||||
g : Int -> Int := neg;
|
||||
in g -1)
|
||||
>> printIntLn (-2 * 2)
|
||||
>> printIntLn (div 4 -2)
|
||||
>> printIntLn (2 - 2)
|
||||
>> printBoolLn (nonNeg 0)
|
||||
>> printBoolLn (nonNeg -1)
|
||||
>> printIntLn (mod -5 -2)
|
||||
>> printBoolLn (0 < 0)
|
||||
>> printBoolLn (0 <= 0)
|
||||
>> printBoolLn (0 < 1)
|
||||
>> printBoolLn (1 <= 0)
|
||||
>> printIntLn (mod 5 -3)
|
||||
>> printIntLn (div 5 -3);
|
||||
>>> printIntLn (-2 * 2)
|
||||
>>> printIntLn (div 4 -2)
|
||||
>>> printIntLn (2 - 2)
|
||||
>>> printBoolLn (nonNeg 0)
|
||||
>>> printBoolLn (nonNeg -1)
|
||||
>>> printIntLn (mod -5 -2)
|
||||
>>> printBoolLn (0 < 0)
|
||||
>>> printBoolLn (0 <= 0)
|
||||
>>> printBoolLn (0 < 1)
|
||||
>>> printBoolLn (1 <= 0)
|
||||
>>> printIntLn (mod 5 -3)
|
||||
>>> printIntLn (div 5 -3);
|
||||
|
@ -1,4 +1,4 @@
|
||||
-- local recursive function using IO >>
|
||||
-- local recursive function using IO >>>
|
||||
module test051;
|
||||
|
||||
import Stdlib.Prelude open;
|
||||
@ -7,5 +7,5 @@ main : IO :=
|
||||
let
|
||||
f : Nat -> IO
|
||||
| zero := printStringLn ""
|
||||
| (suc n) := printString "*" >> f n;
|
||||
| (suc n) := printString "*" >>> f n;
|
||||
in f 3;
|
||||
|
@ -36,12 +36,12 @@ myfor2
|
||||
syntax iterator myzip2 {init := 2; range := 2};
|
||||
myzip2
|
||||
: {A A' B C : Type}
|
||||
→ (A → A' → B → C → A × A')
|
||||
→ (A → A' → B → C → Pair A A')
|
||||
→ A
|
||||
→ A'
|
||||
→ List B
|
||||
→ List C
|
||||
→ A × A'
|
||||
→ Pair A A'
|
||||
| f a b xs ys :=
|
||||
myfor (acc, acc' := a, b) (x, y in zip xs ys)
|
||||
f acc acc' x y;
|
||||
|
@ -3,9 +3,9 @@ module test055;
|
||||
|
||||
import Stdlib.Prelude open;
|
||||
|
||||
type Pair :=
|
||||
| pair : Nat -> Nat -> Pair;
|
||||
type Pair' :=
|
||||
| pair : Nat -> Nat -> Pair';
|
||||
|
||||
main : List (Pair × Nat) × List Pair :=
|
||||
main : Pair (List (Pair Pair' Nat)) (List Pair') :=
|
||||
(pair 1 2, 3) :: (pair 2 3, 4) :: nil
|
||||
, pair 1 2 :: pair 2 3 :: nil;
|
||||
|
@ -10,13 +10,13 @@ type Triple (A B C : Type) :=
|
||||
thd : C
|
||||
};
|
||||
|
||||
type Pair (A B : Type) :=
|
||||
type Pair' (A B : Type) :=
|
||||
mkPair {
|
||||
fst : A;
|
||||
snd : B
|
||||
};
|
||||
|
||||
mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
|
||||
mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
|
||||
| mkPair@{fst := mkPair@{fst; snd := nil};
|
||||
snd := zero :: _} := fst
|
||||
| x := case x of _ := false;
|
||||
|
@ -66,7 +66,7 @@ showBoolFunI : Show (Bool → Bool) := mkShow@{
|
||||
};
|
||||
|
||||
instance
|
||||
showPairI {A B} {{Show A}} {{Show' B}} : Show' (A × B) :=
|
||||
showPairI {A B} {{Show A}} {{Show' B}} : Show' (Pair A B) :=
|
||||
mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y};
|
||||
|
||||
trait
|
||||
@ -79,19 +79,19 @@ instance
|
||||
tFunI {A} {{T A}} : T (A -> A) := mkT \ { a := a };
|
||||
|
||||
main : IO :=
|
||||
printStringLn (Show.show true) >>
|
||||
printStringLn (f false) >>
|
||||
printStringLn (Show.show 3) >>
|
||||
printStringLn (Show.show (g {Nat})) >>
|
||||
printStringLn (Show.show [true; false]) >>
|
||||
printStringLn (Show.show [1; 2; 3]) >>
|
||||
printStringLn (f' [1; 2]) >>
|
||||
printStringLn (f'' [true; false]) >>
|
||||
printStringLn (f'3 [just true; nothing; just false]) >>
|
||||
printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>
|
||||
printStringLn (f'3 "abba") >>
|
||||
printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>
|
||||
printStringLn (f5 "abba" 3) >>
|
||||
printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >>
|
||||
printStringLn (Show.show (λ{x := not x})) >>
|
||||
printStringLn (Show.show true) >>>
|
||||
printStringLn (f false) >>>
|
||||
printStringLn (Show.show 3) >>>
|
||||
printStringLn (Show.show (g {Nat})) >>>
|
||||
printStringLn (Show.show [true; false]) >>>
|
||||
printStringLn (Show.show [1; 2; 3]) >>>
|
||||
printStringLn (f' [1; 2]) >>>
|
||||
printStringLn (f'' [true; false]) >>>
|
||||
printStringLn (f'3 [just true; nothing; just false]) >>>
|
||||
printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>>
|
||||
printStringLn (f'3 "abba") >>>
|
||||
printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>>
|
||||
printStringLn (f5 "abba" 3) >>>
|
||||
printStringLn (Show.show {{_}} ["a"; "b"; "c"; "d"]) >>>
|
||||
printStringLn (Show.show (λ{x := not x})) >>>
|
||||
printStringLn (Show.show (3, [1; 2 + T.a 0]));
|
||||
|
@ -77,10 +77,10 @@ h {A} {{U2 A}} : A -> A := f;
|
||||
|
||||
main : IO :=
|
||||
printStringLn (T1.pp "a")
|
||||
>> printStringLn (T2.pp "b")
|
||||
>> printStringLn (T3.pp "c")
|
||||
>> printStringLn (T4.pp "d")
|
||||
>> printStringLn (U.pp "e")
|
||||
>> printStringLn (f "f")
|
||||
>> printStringLn (g {{mkU1 id}} "g")
|
||||
>> printStringLn (h "h");
|
||||
>>> printStringLn (T2.pp "b")
|
||||
>>> printStringLn (T3.pp "c")
|
||||
>>> printStringLn (T4.pp "d")
|
||||
>>> printStringLn (U.pp "e")
|
||||
>>> printStringLn (f "f")
|
||||
>>> printStringLn (g {{mkU1 id}} "g")
|
||||
>>> printStringLn (h "h");
|
||||
|
@ -3,7 +3,7 @@ module test069;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -3,7 +3,7 @@ module test071;
|
||||
|
||||
import Stdlib.Data.Nat open hiding {Ord; mkOrd};
|
||||
import Stdlib.Data.Nat.Ord as Ord;
|
||||
import Stdlib.Data.Product as Ord;
|
||||
import Stdlib.Data.Pair as Ord;
|
||||
import Stdlib.Data.Bool.Base open;
|
||||
import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT};
|
||||
|
||||
|
@ -16,6 +16,6 @@ type Monad (f : Type -> Type) :=
|
||||
|
||||
open Monad public;
|
||||
|
||||
syntax operator >> bind;
|
||||
>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
syntax operator >>> bind;
|
||||
>>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
|
||||
A) (y : M B) : M B := x >>= λ {_ := y};
|
||||
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user