misc cleanup
This commit is contained in:
@@ -1,24 +0,0 @@
|
||||
module Auto
|
||||
|
||||
pfunc i2s : Int -> String := `(i) => ''+i`
|
||||
pfunc _++_ : String -> String -> String := `(a,b) => a + b`
|
||||
|
||||
infixl 4 _++_
|
||||
|
||||
-- We need sugar and marking as class/instance on all of this
|
||||
|
||||
data Show : U -> U where
|
||||
MkShow : { A : U } -> ((show : A) -> String) -> Show A
|
||||
|
||||
-- FIXME - we'd like to inline this, so `show _ {{showInt}} a` ends up as `i2s a`
|
||||
show : {A : U} {{myshow : Show A}} -> A -> String
|
||||
show {_} {{MkShow foo}} a = foo a
|
||||
|
||||
showInt : Show Int
|
||||
showInt = MkShow i2s
|
||||
|
||||
ptype World
|
||||
pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)`
|
||||
|
||||
main : Int -> World
|
||||
main _ = log ("answer: " ++ show 42)
|
||||
@@ -1,38 +0,0 @@
|
||||
module Auto2
|
||||
|
||||
ptype World
|
||||
pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)`
|
||||
|
||||
|
||||
pfunc i_plus : Int -> Int -> Int := `(x,y) => x + y`
|
||||
|
||||
data Nat : U where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z x = x
|
||||
plus (S k) x = S (plus k x)
|
||||
|
||||
-- a type class
|
||||
data Add : U -> U where
|
||||
MkAdd : {A : U} -> (A -> A -> A) -> Add A
|
||||
|
||||
infixl 8 _+_
|
||||
_+_ : {A : U} -> {{myadd : Add A}} -> A -> A -> A
|
||||
_+_ {_} {{MkAdd adder}} x y = adder x y
|
||||
|
||||
-- Two instances
|
||||
addInt : Add Int
|
||||
addInt = MkAdd i_plus
|
||||
|
||||
addNat : Add Nat
|
||||
addNat = MkAdd plus
|
||||
|
||||
-- sequencing hack
|
||||
infixl 2 _>>_
|
||||
_>>_ : {a b : U} -> a -> b -> b
|
||||
a >> b = b
|
||||
|
||||
main : World -> World
|
||||
main _ = log (40 + 2) >> log (Z + Z)
|
||||
@@ -1,2 +1,2 @@
|
||||
0
|
||||
3
|
||||
0
|
||||
|
||||
@@ -60,8 +60,6 @@ and = \ x y => case x of
|
||||
True => y
|
||||
False => False
|
||||
|
||||
-- FIXME - a case is evaluated here, and I don't know why.
|
||||
|
||||
nand : Bool -> Bool -> Bool
|
||||
nand = \ x y => not (case x of
|
||||
True => y
|
||||
|
||||
Reference in New Issue
Block a user