From c703a92136ce579282c63c6e31fff76cc84b37ce Mon Sep 17 00:00:00 2001 From: bringert Date: Tue, 6 Dec 2005 16:33:40 +0000 Subject: Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension. --- doc/transfer-tutorial.html | 12 +- doc/transfer-tutorial.txt | 10 +- src/Transfer/CompilerAPI.hs | 2 +- transfer/examples/aggregation/aggregate.tr | 56 ---- transfer/examples/aggregation/aggregate.tra | 56 ++++ transfer/examples/aggregation/tree.tr | 23 -- transfer/examples/aggregation/tree.tra | 23 ++ transfer/examples/disjpatt.tr | 24 -- transfer/examples/disjpatt.tra | 24 ++ transfer/examples/exp.tr | 33 -- transfer/examples/exp.tra | 33 ++ transfer/examples/fib.tr | 12 - transfer/examples/fib.tra | 12 + transfer/examples/layout.tr | 9 - transfer/examples/layout.tra | 9 + transfer/examples/list.tr | 6 - transfer/examples/list.tra | 6 + transfer/examples/numerals.tr | 94 ------ transfer/examples/numerals.tra | 94 ++++++ transfer/examples/stoneage.tr | 210 ------------ transfer/examples/stoneage.tra | 210 ++++++++++++ transfer/examples/test.tr | 4 - transfer/examples/test.tra | 4 + transfer/examples/widesnake.tr | 19 -- transfer/examples/widesnake.tra | 19 ++ transfer/lib/array.tr | 9 - transfer/lib/array.tra | 9 + transfer/lib/bool.tr | 6 - transfer/lib/bool.tra | 6 + transfer/lib/nat.tr | 24 -- transfer/lib/nat.tra | 24 ++ transfer/lib/prelude.tr | 502 ---------------------------- transfer/lib/prelude.tra | 502 ++++++++++++++++++++++++++++ 33 files changed, 1043 insertions(+), 1043 deletions(-) delete mode 100644 transfer/examples/aggregation/aggregate.tr create mode 100644 transfer/examples/aggregation/aggregate.tra delete mode 100644 transfer/examples/aggregation/tree.tr create mode 100644 transfer/examples/aggregation/tree.tra delete mode 100644 transfer/examples/disjpatt.tr create mode 100644 transfer/examples/disjpatt.tra delete mode 100644 transfer/examples/exp.tr create mode 100644 transfer/examples/exp.tra delete mode 100644 transfer/examples/fib.tr create mode 100644 transfer/examples/fib.tra delete mode 100644 transfer/examples/layout.tr create mode 100644 transfer/examples/layout.tra delete mode 100644 transfer/examples/list.tr create mode 100644 transfer/examples/list.tra delete mode 100644 transfer/examples/numerals.tr create mode 100644 transfer/examples/numerals.tra delete mode 100644 transfer/examples/stoneage.tr create mode 100644 transfer/examples/stoneage.tra delete mode 100644 transfer/examples/test.tr create mode 100644 transfer/examples/test.tra delete mode 100644 transfer/examples/widesnake.tr create mode 100644 transfer/examples/widesnake.tra delete mode 100644 transfer/lib/array.tr create mode 100644 transfer/lib/array.tra delete mode 100644 transfer/lib/bool.tr create mode 100644 transfer/lib/bool.tra delete mode 100644 transfer/lib/nat.tr create mode 100644 transfer/lib/nat.tra delete mode 100644 transfer/lib/prelude.tr create mode 100644 transfer/lib/prelude.tra diff --git a/doc/transfer-tutorial.html b/doc/transfer-tutorial.html index 038ba1aca..abc3668b3 100644 --- a/doc/transfer-tutorial.html +++ b/doc/transfer-tutorial.html @@ -7,7 +7,7 @@

Transfer tutorial

Author: Björn Bringert <bringert@cs.chalmers.se>
-Last update: Tue Dec 6 17:25:21 2005 +Last update: Tue Dec 6 17:32:55 2005

@@ -85,7 +85,7 @@ This is done with the transfer grammar printer: 
   $ gf
   > i English.gf
-  > pg -printer=transfer | wf tree.tr
+  > pg -printer=transfer | wf tree.tra

@@ -95,13 +95,13 @@ abstract syntax module is not enough. FIXME: why?

The command sequence above writes a Transfer data type definition to the -file tree.tr. +file tree.tra.

Write transfer code

We write the Transfer program -aggregate.tr. +aggregate.tra.

FIXME: explain the code @@ -123,10 +123,10 @@ Here, <lib> is the path to search for any modules which you i in your Transfer program. You can give several -i flags.

-So, to compile aggregate.tr which we created above, we use: +So, to compile aggregate.tra which we created above, we use: 

-  $ transferc aggregate.tr
+  $ transferc aggregate.tra

diff --git a/doc/transfer-tutorial.txt b/doc/transfer-tutorial.txt index 8f5c5179d..3f7c271e8 100644 --- a/doc/transfer-tutorial.txt +++ b/doc/transfer-tutorial.txt @@ -56,7 +56,7 @@ This is done with the ``transfer`` grammar printer: ``` $ gf > i English.gf -> pg -printer=transfer | wf tree.tr +> pg -printer=transfer | wf tree.tra ``` Note that you need to load a concrete syntax which uses the abstract @@ -64,13 +64,13 @@ syntax that you want to create a Transfer data type for. Loading just the abstract syntax module is not enough. FIXME: why? The command sequence above writes a Transfer data type definition to the -file [tree.tr ../transfer/examples/aggregation/tree.tr]. +file [tree.tra ../transfer/examples/aggregation/tree.tra]. = Write transfer code = We write the Transfer program -[aggregate.tr ../transfer/examples/aggregation/aggregate.tr]. +[aggregate.tra ../transfer/examples/aggregation/aggregate.tra]. FIXME: explain the code @@ -88,10 +88,10 @@ $ transferc -i Here, ```` is the path to search for any modules which you import in your Transfer program. You can give several ``-i`` flags. -So, to compile ``aggregate.tr`` which we created above, we use: +So, to compile ``aggregate.tra`` which we created above, we use: ``` -$ transferc aggregate.tr +$ transferc aggregate.tra ``` The creates the Transfer Core file ``aggregate.trc``. diff --git a/src/Transfer/CompilerAPI.hs b/src/Transfer/CompilerAPI.hs index 020393a02..38cb58dd0 100644 --- a/src/Transfer/CompilerAPI.hs +++ b/src/Transfer/CompilerAPI.hs @@ -44,7 +44,7 @@ loadModule = loadModule_ [] Ok m -> return m let load = [ i | Import (Ident i) <- is ] \\ ms let path' = directoryOf f : path - files <- mapM (findFile path' . (++".tr")) load + files <- mapM (findFile path' . (++".tra")) load dss <- mapM (loadModule_ (load++ms) path) files return $ concat (dss++[ds]) diff --git a/transfer/examples/aggregation/aggregate.tr b/transfer/examples/aggregation/aggregate.tr deleted file mode 100644 index b71ccfef2..000000000 --- a/transfer/examples/aggregation/aggregate.tr +++ /dev/null @@ -1,56 +0,0 @@ -import prelude -import tree - - --- aggreg specialized for Tree S -aggregS : Tree S -> Tree S -aggregS = aggreg S - --- For now, here's what we have to do: -aggreg : (A : Type) -> Tree A -> Tree A -aggreg _ t = - case t of - ConjS c s1 s2 -> - case (aggreg ? s1, aggreg ? s2) of - (Pred np1 vp1, Pred np2 vp2) | eq NP (eq_Tree NP) np1 np2 -> - Pred np1 (ConjVP c vp1 vp2) - (Pred np1 vp1, Pred np2 vp2) | eq VP (eq_Tree VP) vp1 vp2 -> - Pred (ConjNP c np1 np2) vp1 - (s1',s2') -> ConjS c s1' s2' - _ -> composOp ? ? compos_Tree ? aggreg t - - - - - -{- --- When the Transfer compiler gets meta variable inference, --- we can write this: -aggreg : (A : Type) -> Tree A -> Tree A -aggreg _ t = - case t of - ConjS c s1 s2 -> - case (aggreg ? s1, aggreg ? s2) of - (Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> - Pred np1 (ConjVP c vp1 vp2) - (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> - Pred (ConjNP c np1 np2) vp1 - (s1',s2') -> ConjS c s1' s2' - _ -> composOp ? ? ? ? aggreg t --} - - -{- --- If we added idden arguments, we could write something like this: -aggreg : (A : Type) => Tree A -> Tree A -aggreg t = - case t of - ConjS c s1 s2 -> - case (aggreg s1, aggreg s2) of - (Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> - Pred np1 (ConjVP c vp1 vp2) - (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> - Pred (ConjNP c np1 np2) vp1 - (s1',s2') -> ConjS c s1' s2' - _ -> composOp aggreg t --} diff --git a/transfer/examples/aggregation/aggregate.tra b/transfer/examples/aggregation/aggregate.tra new file mode 100644 index 000000000..b71ccfef2 --- /dev/null +++ b/transfer/examples/aggregation/aggregate.tra @@ -0,0 +1,56 @@ +import prelude +import tree + + +-- aggreg specialized for Tree S +aggregS : Tree S -> Tree S +aggregS = aggreg S + +-- For now, here's what we have to do: +aggreg : (A : Type) -> Tree A -> Tree A +aggreg _ t = + case t of + ConjS c s1 s2 -> + case (aggreg ? s1, aggreg ? s2) of + (Pred np1 vp1, Pred np2 vp2) | eq NP (eq_Tree NP) np1 np2 -> + Pred np1 (ConjVP c vp1 vp2) + (Pred np1 vp1, Pred np2 vp2) | eq VP (eq_Tree VP) vp1 vp2 -> + Pred (ConjNP c np1 np2) vp1 + (s1',s2') -> ConjS c s1' s2' + _ -> composOp ? ? compos_Tree ? aggreg t + + + + + +{- +-- When the Transfer compiler gets meta variable inference, +-- we can write this: +aggreg : (A : Type) -> Tree A -> Tree A +aggreg _ t = + case t of + ConjS c s1 s2 -> + case (aggreg ? s1, aggreg ? s2) of + (Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> + Pred np1 (ConjVP c vp1 vp2) + (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> + Pred (ConjNP c np1 np2) vp1 + (s1',s2') -> ConjS c s1' s2' + _ -> composOp ? ? ? ? aggreg t +-} + + +{- +-- If we added idden arguments, we could write something like this: +aggreg : (A : Type) => Tree A -> Tree A +aggreg t = + case t of + ConjS c s1 s2 -> + case (aggreg s1, aggreg s2) of + (Pred np1 vp1, Pred np2 vp2) | np1 == np2 -> + Pred np1 (ConjVP c vp1 vp2) + (Pred np1 vp1, Pred np2 vp2) | vp1 == vp2 -> + Pred (ConjNP c np1 np2) vp1 + (s1',s2') -> ConjS c s1' s2' + _ -> composOp aggreg t +-} diff --git a/transfer/examples/aggregation/tree.tr b/transfer/examples/aggregation/tree.tr deleted file mode 100644 index 5515efa21..000000000 --- a/transfer/examples/aggregation/tree.tr +++ /dev/null @@ -1,23 +0,0 @@ -import prelude ; -data Cat : Type where { - Conj : Cat ; - NP : Cat ; - S : Cat ; - VP : Cat -} ; -data Tree : Cat -> Type where { - And : Tree Conj ; - Bill : Tree NP ; - ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ; - ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ; - ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ; - John : Tree NP ; - Mary : Tree NP ; - Or : Tree Conj ; - Pred : Tree NP -> Tree VP -> Tree S ; - Run : Tree VP ; - Swim : Tree VP ; - Walk : Tree VP -} ; -derive Eq Tree ; -derive Compos Tree ; diff --git a/transfer/examples/aggregation/tree.tra b/transfer/examples/aggregation/tree.tra new file mode 100644 index 000000000..5515efa21 --- /dev/null +++ b/transfer/examples/aggregation/tree.tra @@ -0,0 +1,23 @@ +import prelude ; +data Cat : Type where { + Conj : Cat ; + NP : Cat ; + S : Cat ; + VP : Cat +} ; +data Tree : Cat -> Type where { + And : Tree Conj ; + Bill : Tree NP ; + ConjNP : Tree Conj -> Tree NP -> Tree NP -> Tree NP ; + ConjS : Tree Conj -> Tree S -> Tree S -> Tree S ; + ConjVP : Tree Conj -> Tree VP -> Tree VP -> Tree VP ; + John : Tree NP ; + Mary : Tree NP ; + Or : Tree Conj ; + Pred : Tree NP -> Tree VP -> Tree S ; + Run : Tree VP ; + Swim : Tree VP ; + Walk : Tree VP +} ; +derive Eq Tree ; +derive Compos Tree ; diff --git a/transfer/examples/disjpatt.tr b/transfer/examples/disjpatt.tr deleted file mode 100644 index 740e08a7b..000000000 --- a/transfer/examples/disjpatt.tr +++ /dev/null @@ -1,24 +0,0 @@ -data Cat : Type where - VarOrWild : Cat - Exp : Cat - Ident : Cat - -data Tree : Cat -> Type where - EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp - EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp - EVar : Tree Ident -> Tree Exp - EType : Tree Exp - EStr : String -> Tree Exp - EInt : Integer -> Tree Exp - VVar : Tree Ident -> Tree VarOrWild - VWild : Tree VarOrWild - Ident : String -> Tree Ident - - -f e = case e of - EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e - Ident i -> Ident i - _ -> catchAll - - -g (Ident x || EAbs (VWild || VVar _) t e) = x e \ No newline at end of file diff --git a/transfer/examples/disjpatt.tra b/transfer/examples/disjpatt.tra new file mode 100644 index 000000000..740e08a7b --- /dev/null +++ b/transfer/examples/disjpatt.tra @@ -0,0 +1,24 @@ +data Cat : Type where + VarOrWild : Cat + Exp : Cat + Ident : Cat + +data Tree : Cat -> Type where + EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp + EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp + EVar : Tree Ident -> Tree Exp + EType : Tree Exp + EStr : String -> Tree Exp + EInt : Integer -> Tree Exp + VVar : Tree Ident -> Tree VarOrWild + VWild : Tree VarOrWild + Ident : String -> Tree Ident + + +f e = case e of + EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e + Ident i -> Ident i + _ -> catchAll + + +g (Ident x || EAbs (VWild || VVar _) t e) = x e \ No newline at end of file diff --git a/transfer/examples/exp.tr b/transfer/examples/exp.tr deleted file mode 100644 index e54b82055..000000000 --- a/transfer/examples/exp.tr +++ /dev/null @@ -1,33 +0,0 @@ -import prelude - -data Cat : Type where - Stm : Cat - Exp : Cat - Var : Cat - Typ : Cat - ListStm : Cat - -data Tree : Cat -> Type where - SDecl : Tree Typ -> Tree Var -> Tree Stm - SAss : Tree Var -> Tree Exp -> Tree Stm - SBlock : Tree ListStm -> Tree Stm - EAdd : Tree Exp -> Tree Exp -> Tree Exp - EStm : Tree Stm -> Tree Exp - EVar : Tree Var -> Tree Exp - EInt : Integer -> Tree Exp - V : String -> Tree Var - TInt : Tree Typ - TFloat : Tree Typ - - NilStm : Tree ListStm - ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm - -derive Compos Tree - -rename : (String -> String) -> (C : Type) -> Tree C -> Tree C -rename f C t = case t of - V x -> V (f x) - _ -> composOp ? ? compos_Tree C (rename f) t - - -main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2))) \ No newline at end of file diff --git a/transfer/examples/exp.tra b/transfer/examples/exp.tra new file mode 100644 index 000000000..e54b82055 --- /dev/null +++ b/transfer/examples/exp.tra @@ -0,0 +1,33 @@ +import prelude + +data Cat : Type where + Stm : Cat + Exp : Cat + Var : Cat + Typ : Cat + ListStm : Cat + +data Tree : Cat -> Type where + SDecl : Tree Typ -> Tree Var -> Tree Stm + SAss : Tree Var -> Tree Exp -> Tree Stm + SBlock : Tree ListStm -> Tree Stm + EAdd : Tree Exp -> Tree Exp -> Tree Exp + EStm : Tree Stm -> Tree Exp + EVar : Tree Var -> Tree Exp + EInt : Integer -> Tree Exp + V : String -> Tree Var + TInt : Tree Typ + TFloat : Tree Typ + + NilStm : Tree ListStm + ConsStm : Tree Stm -> Tree ListStm -> Tree ListStm + +derive Compos Tree + +rename : (String -> String) -> (C : Type) -> Tree C -> Tree C +rename f C t = case t of + V x -> V (f x) + _ -> composOp ? ? compos_Tree C (rename f) t + + +main = rename (const ? ? "apa") Stm (SAss (V "y") (EAdd (EVar (V "x")) (EInt 2))) \ No newline at end of file diff --git a/transfer/examples/fib.tr b/transfer/examples/fib.tr deleted file mode 100644 index 43e533b1f..000000000 --- a/transfer/examples/fib.tr +++ /dev/null @@ -1,12 +0,0 @@ -import nat -import prelude - -fib : Integer -> Integer -fib 0 = 1 -fib 1 = 1 -fib n = fib (n-1) + fib (n-2) - -fibNat : Nat -> Nat -fibNat Zero = Succ Zero -fibNat (Succ Zero) = Succ Zero -fibNat (Succ (Succ n)) = plus Nat add_Nat (fibNat (Succ n)) (fibNat n) \ No newline at end of file diff --git a/transfer/examples/fib.tra b/transfer/examples/fib.tra new file mode 100644 index 000000000..43e533b1f --- /dev/null +++ b/transfer/examples/fib.tra @@ -0,0 +1,12 @@ +import nat +import prelude + +fib : Integer -> Integer +fib 0 = 1 +fib 1 = 1 +fib n = fib (n-1) + fib (n-2) + +fibNat : Nat -> Nat +fibNat Zero = Succ Zero +fibNat (Succ Zero) = Succ Zero +fibNat (Succ (Succ n)) = plus Nat add_Nat (fibNat (Succ n)) (fibNat n) \ No newline at end of file diff --git a/transfer/examples/layout.tr b/transfer/examples/layout.tr deleted file mode 100644 index ad35af376..000000000 --- a/transfer/examples/layout.tr +++ /dev/null @@ -1,9 +0,0 @@ -x : Apa -x = let x : T = y - in case y of - f -> q - _ -> a - -f = apa - -g = bepa \ No newline at end of file diff --git a/transfer/examples/layout.tra b/transfer/examples/layout.tra new file mode 100644 index 000000000..ad35af376 --- /dev/null +++ b/transfer/examples/layout.tra @@ -0,0 +1,9 @@ +x : Apa +x = let x : T = y + in case y of + f -> q + _ -> a + +f = apa + +g = bepa \ No newline at end of file diff --git a/transfer/examples/list.tr b/transfer/examples/list.tr deleted file mode 100644 index 253c29e02..000000000 --- a/transfer/examples/list.tr +++ /dev/null @@ -1,6 +0,0 @@ -import prelude - -l1 = append ? [1,2,3,5,6] [3] -l2 = 2 :: l1 - -main = rec { x = length ? l2; y = l2} diff --git a/transfer/examples/list.tra b/transfer/examples/list.tra new file mode 100644 index 000000000..253c29e02 --- /dev/null +++ b/transfer/examples/list.tra @@ -0,0 +1,6 @@ +import prelude + +l1 = append ? [1,2,3,5,6] [3] +l2 = 2 :: l1 + +main = rec { x = length ? l2; y = l2} diff --git a/transfer/examples/numerals.tr b/transfer/examples/numerals.tr deleted file mode 100644 index 31bac33ac..000000000 --- a/transfer/examples/numerals.tr +++ /dev/null @@ -1,94 +0,0 @@ -import prelude - -data Cat : Type where { - Digit : Cat ; - Numeral : Cat ; - Sub10 : Cat ; - Sub100 : Cat ; - Sub1000 : Cat ; - Sub1000000 : Cat -} ; - -data Tree : (_ : Cat)-> Type where { - n2 : Tree Digit ; - n3 : Tree Digit ; - n4 : Tree Digit ; - n5 : Tree Digit ; - n6 : Tree Digit ; - n7 : Tree Digit ; - n8 : Tree Digit ; - n9 : Tree Digit ; - num : (_ : Tree Sub1000000)-> Tree Numeral ; - pot0 : (_ : Tree Digit)-> Tree Sub10 ; - pot01 : Tree Sub10 ; - pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ; - pot1 : (_ : Tree Digit)-> Tree Sub100 ; - pot110 : Tree Sub100 ; - pot111 : Tree Sub100 ; - pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ; - pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ; - pot1to19 : (_ : Tree Digit)-> Tree Sub100 ; - pot2 : (_ : Tree Sub10)-> Tree Sub1000 ; - pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ; - pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ; - pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ; - pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000 -} - -derive Compos Tree - - -data Binary_Cat : Type where { - Bin : Binary_Cat -} ; -data Binary_Tree : (_ : Binary_Cat)-> Type where { - End : Binary_Tree Bin ; - One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ; - Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin -} - - - -monoid_plus_Int : Monoid Integer -monoid_plus_Int = rec mzero = 0 - mplus = (\x -> \y -> x + y) - - -num2int : Tree Numeral -> Integer -num2int = tree2int ? - -tree2int : (C : Cat) -> Tree C -> Integer -tree2int _ n = case n of - n2 -> 2 - n3 -> 3 - n4 -> 4 - n5 -> 5 - n6 -> 6 - n7 -> 7 - n8 -> 8 - n9 -> 9 - pot01 -> 1 - pot1 x -> 10 * tree2int ? x - pot110 -> 10 - pot111 -> 11 - pot1plus x y -> 10 * tree2int ? x + tree2int ? y - pot1to19 x -> 10 + tree2int ? x - pot2 x -> 100 * tree2int ? x - pot2as3 x -> 10 * tree2int ? x - pot2plus x y -> 100 * tree2int ? x + tree2int ? y - pot3 x -> 1000 * tree2int ? x - pot3plus x y -> 1000 * tree2int ? x + tree2int ? y - _ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n - -int2bin : Integer -> Binary_Tree Bin -int2bin = int2bin_ End - -int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin -int2bin_ b 0 = b -int2bin_ b n = let d : Integer = if n % 2 == 0 then Zero else One - q : Integer = n / 2 - in int2bin_ (d b) q - -num2bin : Tree Numeral -> Binary_Tree Bin -num2bin n = int2bin (num2int n) - diff --git a/transfer/examples/numerals.tra b/transfer/examples/numerals.tra new file mode 100644 index 000000000..31bac33ac --- /dev/null +++ b/transfer/examples/numerals.tra @@ -0,0 +1,94 @@ +import prelude + +data Cat : Type where { + Digit : Cat ; + Numeral : Cat ; + Sub10 : Cat ; + Sub100 : Cat ; + Sub1000 : Cat ; + Sub1000000 : Cat +} ; + +data Tree : (_ : Cat)-> Type where { + n2 : Tree Digit ; + n3 : Tree Digit ; + n4 : Tree Digit ; + n5 : Tree Digit ; + n6 : Tree Digit ; + n7 : Tree Digit ; + n8 : Tree Digit ; + n9 : Tree Digit ; + num : (_ : Tree Sub1000000)-> Tree Numeral ; + pot0 : (_ : Tree Digit)-> Tree Sub10 ; + pot01 : Tree Sub10 ; + pot0as1 : (_ : Tree Sub10)-> Tree Sub100 ; + pot1 : (_ : Tree Digit)-> Tree Sub100 ; + pot110 : Tree Sub100 ; + pot111 : Tree Sub100 ; + pot1as2 : (_ : Tree Sub100)-> Tree Sub1000 ; + pot1plus : (_ : Tree Digit)-> (_ : Tree Sub10)-> Tree Sub100 ; + pot1to19 : (_ : Tree Digit)-> Tree Sub100 ; + pot2 : (_ : Tree Sub10)-> Tree Sub1000 ; + pot2as3 : (_ : Tree Sub1000)-> Tree Sub1000000 ; + pot2plus : (_ : Tree Sub10)-> (_ : Tree Sub100)-> Tree Sub1000 ; + pot3 : (_ : Tree Sub1000)-> Tree Sub1000000 ; + pot3plus : (_ : Tree Sub1000)-> (_ : Tree Sub1000)-> Tree Sub1000000 +} + +derive Compos Tree + + +data Binary_Cat : Type where { + Bin : Binary_Cat +} ; +data Binary_Tree : (_ : Binary_Cat)-> Type where { + End : Binary_Tree Bin ; + One : (_ : Binary_Tree Bin)-> Binary_Tree Bin ; + Zero : (_ : Binary_Tree Bin)-> Binary_Tree Bin +} + + + +monoid_plus_Int : Monoid Integer +monoid_plus_Int = rec mzero = 0 + mplus = (\x -> \y -> x + y) + + +num2int : Tree Numeral -> Integer +num2int = tree2int ? + +tree2int : (C : Cat) -> Tree C -> Integer +tree2int _ n = case n of + n2 -> 2 + n3 -> 3 + n4 -> 4 + n5 -> 5 + n6 -> 6 + n7 -> 7 + n8 -> 8 + n9 -> 9 + pot01 -> 1 + pot1 x -> 10 * tree2int ? x + pot110 -> 10 + pot111 -> 11 + pot1plus x y -> 10 * tree2int ? x + tree2int ? y + pot1to19 x -> 10 + tree2int ? x + pot2 x -> 100 * tree2int ? x + pot2as3 x -> 10 * tree2int ? x + pot2plus x y -> 100 * tree2int ? x + tree2int ? y + pot3 x -> 1000 * tree2int ? x + pot3plus x y -> 1000 * tree2int ? x + tree2int ? y + _ -> composFold ? ? compos_Tree ? monoid_plus_Int C tree2int n + +int2bin : Integer -> Binary_Tree Bin +int2bin = int2bin_ End + +int2bin_ : Binary_Tree Bin -> Integer -> Binary_Tree Bin +int2bin_ b 0 = b +int2bin_ b n = let d : Integer = if n % 2 == 0 then Zero else One + q : Integer = n / 2 + in int2bin_ (d b) q + +num2bin : Tree Numeral -> Binary_Tree Bin +num2bin n = int2bin (num2int n) + diff --git a/transfer/examples/stoneage.tr b/transfer/examples/stoneage.tr deleted file mode 100644 index e48c519e6..000000000 --- a/transfer/examples/stoneage.tr +++ /dev/null @@ -1,210 +0,0 @@ -import prelude - -data Cat : Type where { - CN : Cat ; - NP : Cat ; - S : Cat -} ; -data Tree : (_ : Cat)-> Type where { - A : (h_ : Tree CN)-> Tree NP ; - All : (h_ : Tree CN)-> Tree NP ; - Animal : Tree CN ; - Ashes : Tree CN ; - Back : Tree CN ; - Bad : (h_ : Tree CN)-> Tree CN ; - Bark : Tree CN ; - Belly : Tree CN ; - Big : (h_ : Tree CN)-> Tree CN ; - Bird : Tree CN ; - Bite : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Black : (h_ : Tree CN)-> Tree CN ; - Blood : Tree CN ; - Blow : (h_ : Tree NP)-> Tree S ; - Bone : Tree CN ; - Breast : Tree CN ; - Breathe : (h_ : Tree NP)-> Tree S ; - Burn : (h_ : Tree NP)-> Tree S ; - Child : Tree CN ; - Cloud : Tree CN ; - Cold : (h_ : Tree CN)-> Tree CN ; - Come : (h_ : Tree NP)-> Tree S ; - Correct : (h_ : Tree CN)-> Tree CN ; - Count : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Cut : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Day : Tree CN ; - Die : (h_ : Tree NP)-> Tree S ; - Dig : (h_ : Tree NP)-> Tree S ; - Dirty : (h_ : Tree CN)-> Tree CN ; - Dog : Tree CN ; - Drink : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Dry : (h_ : Tree CN)-> Tree CN ; - Dull : (h_ : Tree CN)-> Tree CN ; - Dust : Tree CN ; - Ear : Tree CN ; - Earth : Tree CN ; - Eat : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Egg : Tree CN ; - Eye : Tree CN ; - Fall : (h_ : Tree NP)-> Tree S ; - Fat : Tree CN ; - Father : Tree CN ; - FatherOf : (h_ : Tree NP)-> Tree CN ; - Fear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Feather : Tree CN ; - Few : (h_ : Tree CN)-> Tree NP ; - Fight : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Fingernail : Tree CN ; - Fire : Tree CN ; - Fish : Tree CN ; - Five : (h_ : Tree CN)-> Tree NP ; - Float : (h_ : Tree NP)-> Tree S ; - Flow : (h_ : Tree NP)-> Tree S ; - Flower : Tree CN ; - Fly : (h_ : Tree NP)-> Tree S ; - Fog : Tree CN ; - Foot : Tree CN ; - Forest : Tree CN ; - Four : (h_ : Tree CN)-> Tree NP ; - Freeze : (h_ : Tree NP)-> Tree S ; - Fruit : Tree CN ; - Full : (h_ : Tree CN)-> Tree CN ; - Give : (h_ : Tree NP)-> (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Good : (h_ : Tree CN)-> Tree CN ; - Grass : Tree CN ; - Green : (h_ : Tree CN)-> Tree CN ; - Guts : Tree CN ; - Hair : Tree CN ; - Hand : Tree CN ; - He : Tree NP ; - Head : Tree CN ; - Hear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Heart : Tree CN ; - Heavy : (h_ : Tree CN)-> Tree CN ; - Hit : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Hold : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Horn : Tree CN ; - Hunt : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Husband : Tree CN ; - I : Tree NP ; - Ice : Tree CN ; - Kill : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Knee : Tree CN ; - Know : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Lake : Tree CN ; - Laugh : (h_ : Tree NP)-> Tree S ; - Leaf : Tree CN ; - Left : (h_ : Tree CN)-> Tree CN ; - Leg : Tree CN ; - Lie : (h_ : Tree NP)-> Tree S ; - Live : (h_ : Tree NP)-> Tree S ; - Liver : Tree CN ; - Long : (h_ : Tree CN)-> Tree CN ; - Louse : Tree CN ; - Man : Tree CN ; - Many : (h_ : Tree CN)-> Tree NP ; - Meat : Tree CN ; - Moon : Tree CN ; - Mother : Tree CN ; - MotherOf : (h_ : Tree NP)-> Tree CN ; - Mountain : Tree CN ; - Mouth : Tree CN ; - Name : Tree CN ; - Narrow : (h_ : Tree CN)-> Tree CN ; - Near : (h_ : Tree CN)-> Tree CN ; - Neck : Tree CN ; - New : (h_ : Tree CN)-> Tree CN ; - Night : Tree CN ; - Nose : Tree CN ; - Old : (h_ : Tree CN)-> Tree CN ; - One : (h_ : Tree CN)-> Tree NP ; - Other : (h_ : Tree CN)-> Tree NP ; - Person : Tree CN ; - Play : (h_ : Tree NP)-> Tree S ; - Pull : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Push : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Rain : Tree CN ; - Red : (h_ : Tree CN)-> Tree CN ; - Right : (h_ : Tree CN)-> Tree CN ; - River : Tree CN ; - Road : Tree CN ; - Root : Tree CN ; - Rope : Tree CN ; - Rotten : (h_ : Tree CN)-> Tree CN ; - Round : (h_ : Tree CN)-> Tree CN ; - Rub : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Salt : Tree CN ; - Sand : Tree CN ; - Scratch : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Sea : Tree CN ; - See : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Seed : Tree CN ; - Sew : (h_ : Tree NP)-> Tree S ; - Sharp : (h_ : Tree CN)-> Tree CN ; - Short : (h_ : Tree CN)-> Tree CN ; - Sing : (h_ : Tree NP)-> Tree S ; - Sit : (h_ : Tree NP)-> Tree S ; - Skin : Tree CN ; - Sky : Tree CN ; - Sleep : (h_ : Tree NP)-> Tree S ; - Small : (h_ : Tree CN)-> Tree CN ; - Smell : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Smoke : Tree CN ; - Smooth : (h_ : Tree CN)-> Tree CN ; - Snake : Tree CN ; - Snow : Tree CN ; - Some_Many : (h_ : Tree CN)-> Tree NP ; - Some_One : (h_ : Tree CN)-> Tree NP ; - Spit : (h_ : Tree NP)-> Tree S ; - Split : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Squeeze : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Stab : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Stand : (h_ : Tree NP)-> Tree S ; - Star : Tree CN ; - Stick : Tree CN ; - Stone : Tree CN ; - Straight : (h_ : Tree CN)-> Tree CN ; - Suck : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Sun : Tree CN ; - Swell : (h_ : Tree NP)-> Tree S ; - Swim : (h_ : Tree NP)-> Tree S ; - Tail : Tree CN ; - That : (h_ : Tree CN)-> Tree NP ; - The_Many : (h_ : Tree CN)-> Tree NP ; - The_One : (h_ : Tree CN)-> Tree NP ; - They : Tree NP ; - Thick : (h_ : Tree CN)-> Tree CN ; - Thin : (h_ : Tree CN)-> Tree CN ; - Think : (h_ : Tree NP)-> Tree S ; - This : (h_ : Tree CN)-> Tree NP ; - Three : (h_ : Tree CN)-> Tree NP ; - Throw : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Tie : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Tongue : Tree CN ; - Tooth : Tree CN ; - Tree : Tree CN ; - Turn : (h_ : Tree NP)-> Tree S ; - Two : (h_ : Tree CN)-> Tree NP ; - Vomit : (h_ : Tree NP)-> Tree S ; - Walk : (h_ : Tree NP)-> Tree S ; - Warm : (h_ : Tree CN)-> Tree CN ; - Wash : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Water : Tree CN ; - We : Tree NP ; - Wet : (h_ : Tree CN)-> Tree CN ; - White : (h_ : Tree CN)-> Tree CN ; - Wide : (h_ : Tree CN)-> Tree CN ; - Wife : Tree CN ; - Wind : Tree CN ; - Wing : Tree CN ; - Wipe : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; - Woman : Tree CN ; - Worm : Tree CN ; - Year : Tree CN ; - Yellow : (h_ : Tree CN)-> Tree CN ; - You_Many : Tree NP ; - You_One : Tree NP -} - -derive Compos Tree - -derive Eq Tree \ No newline at end of file diff --git a/transfer/examples/stoneage.tra b/transfer/examples/stoneage.tra new file mode 100644 index 000000000..e48c519e6 --- /dev/null +++ b/transfer/examples/stoneage.tra @@ -0,0 +1,210 @@ +import prelude + +data Cat : Type where { + CN : Cat ; + NP : Cat ; + S : Cat +} ; +data Tree : (_ : Cat)-> Type where { + A : (h_ : Tree CN)-> Tree NP ; + All : (h_ : Tree CN)-> Tree NP ; + Animal : Tree CN ; + Ashes : Tree CN ; + Back : Tree CN ; + Bad : (h_ : Tree CN)-> Tree CN ; + Bark : Tree CN ; + Belly : Tree CN ; + Big : (h_ : Tree CN)-> Tree CN ; + Bird : Tree CN ; + Bite : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Black : (h_ : Tree CN)-> Tree CN ; + Blood : Tree CN ; + Blow : (h_ : Tree NP)-> Tree S ; + Bone : Tree CN ; + Breast : Tree CN ; + Breathe : (h_ : Tree NP)-> Tree S ; + Burn : (h_ : Tree NP)-> Tree S ; + Child : Tree CN ; + Cloud : Tree CN ; + Cold : (h_ : Tree CN)-> Tree CN ; + Come : (h_ : Tree NP)-> Tree S ; + Correct : (h_ : Tree CN)-> Tree CN ; + Count : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Cut : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Day : Tree CN ; + Die : (h_ : Tree NP)-> Tree S ; + Dig : (h_ : Tree NP)-> Tree S ; + Dirty : (h_ : Tree CN)-> Tree CN ; + Dog : Tree CN ; + Drink : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Dry : (h_ : Tree CN)-> Tree CN ; + Dull : (h_ : Tree CN)-> Tree CN ; + Dust : Tree CN ; + Ear : Tree CN ; + Earth : Tree CN ; + Eat : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Egg : Tree CN ; + Eye : Tree CN ; + Fall : (h_ : Tree NP)-> Tree S ; + Fat : Tree CN ; + Father : Tree CN ; + FatherOf : (h_ : Tree NP)-> Tree CN ; + Fear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Feather : Tree CN ; + Few : (h_ : Tree CN)-> Tree NP ; + Fight : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Fingernail : Tree CN ; + Fire : Tree CN ; + Fish : Tree CN ; + Five : (h_ : Tree CN)-> Tree NP ; + Float : (h_ : Tree NP)-> Tree S ; + Flow : (h_ : Tree NP)-> Tree S ; + Flower : Tree CN ; + Fly : (h_ : Tree NP)-> Tree S ; + Fog : Tree CN ; + Foot : Tree CN ; + Forest : Tree CN ; + Four : (h_ : Tree CN)-> Tree NP ; + Freeze : (h_ : Tree NP)-> Tree S ; + Fruit : Tree CN ; + Full : (h_ : Tree CN)-> Tree CN ; + Give : (h_ : Tree NP)-> (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Good : (h_ : Tree CN)-> Tree CN ; + Grass : Tree CN ; + Green : (h_ : Tree CN)-> Tree CN ; + Guts : Tree CN ; + Hair : Tree CN ; + Hand : Tree CN ; + He : Tree NP ; + Head : Tree CN ; + Hear : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Heart : Tree CN ; + Heavy : (h_ : Tree CN)-> Tree CN ; + Hit : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Hold : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Horn : Tree CN ; + Hunt : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Husband : Tree CN ; + I : Tree NP ; + Ice : Tree CN ; + Kill : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Knee : Tree CN ; + Know : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Lake : Tree CN ; + Laugh : (h_ : Tree NP)-> Tree S ; + Leaf : Tree CN ; + Left : (h_ : Tree CN)-> Tree CN ; + Leg : Tree CN ; + Lie : (h_ : Tree NP)-> Tree S ; + Live : (h_ : Tree NP)-> Tree S ; + Liver : Tree CN ; + Long : (h_ : Tree CN)-> Tree CN ; + Louse : Tree CN ; + Man : Tree CN ; + Many : (h_ : Tree CN)-> Tree NP ; + Meat : Tree CN ; + Moon : Tree CN ; + Mother : Tree CN ; + MotherOf : (h_ : Tree NP)-> Tree CN ; + Mountain : Tree CN ; + Mouth : Tree CN ; + Name : Tree CN ; + Narrow : (h_ : Tree CN)-> Tree CN ; + Near : (h_ : Tree CN)-> Tree CN ; + Neck : Tree CN ; + New : (h_ : Tree CN)-> Tree CN ; + Night : Tree CN ; + Nose : Tree CN ; + Old : (h_ : Tree CN)-> Tree CN ; + One : (h_ : Tree CN)-> Tree NP ; + Other : (h_ : Tree CN)-> Tree NP ; + Person : Tree CN ; + Play : (h_ : Tree NP)-> Tree S ; + Pull : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Push : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Rain : Tree CN ; + Red : (h_ : Tree CN)-> Tree CN ; + Right : (h_ : Tree CN)-> Tree CN ; + River : Tree CN ; + Road : Tree CN ; + Root : Tree CN ; + Rope : Tree CN ; + Rotten : (h_ : Tree CN)-> Tree CN ; + Round : (h_ : Tree CN)-> Tree CN ; + Rub : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Salt : Tree CN ; + Sand : Tree CN ; + Scratch : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Sea : Tree CN ; + See : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Seed : Tree CN ; + Sew : (h_ : Tree NP)-> Tree S ; + Sharp : (h_ : Tree CN)-> Tree CN ; + Short : (h_ : Tree CN)-> Tree CN ; + Sing : (h_ : Tree NP)-> Tree S ; + Sit : (h_ : Tree NP)-> Tree S ; + Skin : Tree CN ; + Sky : Tree CN ; + Sleep : (h_ : Tree NP)-> Tree S ; + Small : (h_ : Tree CN)-> Tree CN ; + Smell : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Smoke : Tree CN ; + Smooth : (h_ : Tree CN)-> Tree CN ; + Snake : Tree CN ; + Snow : Tree CN ; + Some_Many : (h_ : Tree CN)-> Tree NP ; + Some_One : (h_ : Tree CN)-> Tree NP ; + Spit : (h_ : Tree NP)-> Tree S ; + Split : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Squeeze : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Stab : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Stand : (h_ : Tree NP)-> Tree S ; + Star : Tree CN ; + Stick : Tree CN ; + Stone : Tree CN ; + Straight : (h_ : Tree CN)-> Tree CN ; + Suck : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Sun : Tree CN ; + Swell : (h_ : Tree NP)-> Tree S ; + Swim : (h_ : Tree NP)-> Tree S ; + Tail : Tree CN ; + That : (h_ : Tree CN)-> Tree NP ; + The_Many : (h_ : Tree CN)-> Tree NP ; + The_One : (h_ : Tree CN)-> Tree NP ; + They : Tree NP ; + Thick : (h_ : Tree CN)-> Tree CN ; + Thin : (h_ : Tree CN)-> Tree CN ; + Think : (h_ : Tree NP)-> Tree S ; + This : (h_ : Tree CN)-> Tree NP ; + Three : (h_ : Tree CN)-> Tree NP ; + Throw : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Tie : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Tongue : Tree CN ; + Tooth : Tree CN ; + Tree : Tree CN ; + Turn : (h_ : Tree NP)-> Tree S ; + Two : (h_ : Tree CN)-> Tree NP ; + Vomit : (h_ : Tree NP)-> Tree S ; + Walk : (h_ : Tree NP)-> Tree S ; + Warm : (h_ : Tree CN)-> Tree CN ; + Wash : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Water : Tree CN ; + We : Tree NP ; + Wet : (h_ : Tree CN)-> Tree CN ; + White : (h_ : Tree CN)-> Tree CN ; + Wide : (h_ : Tree CN)-> Tree CN ; + Wife : Tree CN ; + Wind : Tree CN ; + Wing : Tree CN ; + Wipe : (h_ : Tree NP)-> (h_ : Tree NP)-> Tree S ; + Woman : Tree CN ; + Worm : Tree CN ; + Year : Tree CN ; + Yellow : (h_ : Tree CN)-> Tree CN ; + You_Many : Tree NP ; + You_One : Tree NP +} + +derive Compos Tree + +derive Eq Tree \ No newline at end of file diff --git a/transfer/examples/test.tr b/transfer/examples/test.tr deleted file mode 100644 index 0abb933ef..000000000 --- a/transfer/examples/test.tr +++ /dev/null @@ -1,4 +0,0 @@ -import nat -import fib - --- main = natToInt (fibNat (intToNat 10)) \ No newline at end of file diff --git a/transfer/examples/test.tra b/transfer/examples/test.tra new file mode 100644 index 000000000..0abb933ef --- /dev/null +++ b/transfer/examples/test.tra @@ -0,0 +1,4 @@ +import nat +import fib + +-- main = natToInt (fibNat (intToNat 10)) \ No newline at end of file diff --git a/transfer/examples/widesnake.tr b/transfer/examples/widesnake.tr deleted file mode 100644 index e27bd5981..000000000 --- a/transfer/examples/widesnake.tr +++ /dev/null @@ -1,19 +0,0 @@ -import bool -import stoneage - -monoid_Bool : sig { zero : Bool; plus : Bool -> Bool -> Bool } -monoid_Bool = rec - zero = False - plus = \x -> \y -> x && y - -isSnake : (A : Tree) -> Tree A -> Bool -isSnake _ x = case x of - Snake -> True - _ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x - -wideSnake : (A : Cat) -> Tree A -> Tree A -wideSnake _ x = case x of - Wide y -> let y' : CN = wideSnake ? y - in if isSnake CN y' then Thick y' else Wide y' - _ -> composOp ? ? compos_Tree ? wideSnake x - diff --git a/transfer/examples/widesnake.tra b/transfer/examples/widesnake.tra new file mode 100644 index 000000000..e27bd5981 --- /dev/null +++ b/transfer/examples/widesnake.tra @@ -0,0 +1,19 @@ +import bool +import stoneage + +monoid_Bool : sig { zero : Bool; plus : Bool -> Bool -> Bool } +monoid_Bool = rec + zero = False + plus = \x -> \y -> x && y + +isSnake : (A : Tree) -> Tree A -> Bool +isSnake _ x = case x of + Snake -> True + _ -> composFold ? ? compos_Tree Bool monoid_Bool ? isSnake x + +wideSnake : (A : Cat) -> Tree A -> Tree A +wideSnake _ x = case x of + Wide y -> let y' : CN = wideSnake ? y + in if isSnake CN y' then Thick y' else Wide y' + _ -> composOp ? ? compos_Tree ? wideSnake x + diff --git a/transfer/lib/array.tr b/transfer/lib/array.tr deleted file mode 100644 index e91fe35e7..000000000 --- a/transfer/lib/array.tr +++ /dev/null @@ -1,9 +0,0 @@ -import nat - -data Array : Type -> Nat -> Type where - Empty : (A:Type) -> Array A Zero - Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n) - -mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n -mapA A B _ f (Empty _) = Empty B -mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs) diff --git a/transfer/lib/array.tra b/transfer/lib/array.tra new file mode 100644 index 000000000..e91fe35e7 --- /dev/null +++ b/transfer/lib/array.tra @@ -0,0 +1,9 @@ +import nat + +data Array : Type -> Nat -> Type where + Empty : (A:Type) -> Array A Zero + Cell : (A:Type) -> (n:Nat) -> A -> Array A n -> Array A (Succ n) + +mapA : (A:Type) -> (B:Type) -> (n:Nat) -> (A -> B) -> Array A n -> Array B n +mapA A B _ f (Empty _) = Empty B +mapA A B (Succ n) f (Cell _ _ x xs) = Cell B n (f x) (mapA A B n f xs) diff --git a/transfer/lib/bool.tr b/transfer/lib/bool.tr deleted file mode 100644 index 2639422b7..000000000 --- a/transfer/lib/bool.tr +++ /dev/null @@ -1,6 +0,0 @@ -import prelude - -depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B -depif _ _ True x _ = x -depif _ _ False _ y = y - diff --git a/transfer/lib/bool.tra b/transfer/lib/bool.tra new file mode 100644 index 000000000..2639422b7 --- /dev/null +++ b/transfer/lib/bool.tra @@ -0,0 +1,6 @@ +import prelude + +depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B +depif _ _ True x _ = x +depif _ _ False _ y = y + diff --git a/transfer/lib/nat.tr b/transfer/lib/nat.tr deleted file mode 100644 index b13a809ed..000000000 --- a/transfer/lib/nat.tr +++ /dev/null @@ -1,24 +0,0 @@ -import prelude - -data Nat : Type where - Zero : Nat - Succ : (n:Nat) -> Nat - -add_Nat : Add Nat -add_Nat = rec zero = Zero - plus = natPlus - -natPlus : Nat -> Nat -> Nat -natPlus Zero y = y -natPlus (Succ x) y = Succ (natPlus x y) - -pred : Nat -> Nat -pred Zero = Zero -pred (Succ n) = n - -natToInt : Nat -> Integer -natToInt Zero = 0 -natToInt (Succ n) = 1 + natToInt n - -intToNat : Integer -> Nat -intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/lib/nat.tra b/transfer/lib/nat.tra new file mode 100644 index 000000000..b13a809ed --- /dev/null +++ b/transfer/lib/nat.tra @@ -0,0 +1,24 @@ +import prelude + +data Nat : Type where + Zero : Nat + Succ : (n:Nat) -> Nat + +add_Nat : Add Nat +add_Nat = rec zero = Zero + plus = natPlus + +natPlus : Nat -> Nat -> Nat +natPlus Zero y = y +natPlus (Succ x) y = Succ (natPlus x y) + +pred : Nat -> Nat +pred Zero = Zero +pred (Succ n) = n + +natToInt : Nat -> Integer +natToInt Zero = 0 +natToInt (Succ n) = 1 + natToInt n + +intToNat : Integer -> Nat +intToNat n = if n == 0 then Zero else Succ (intToNat (n-1)) diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr deleted file mode 100644 index fe2d1b296..000000000 --- a/transfer/lib/prelude.tr +++ /dev/null @@ -1,502 +0,0 @@ --- --- Prelude for the transfer language. --- - - --- --- Basic functions --- - -const : (A:Type) -> (B:Type) -> A -> B -> A -const _ _ x _ = x - -id : (A:Type) -> A -> A -id _ x = x - -flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C -flip _ _ _ f x y = f y x - -compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C -compose _ _ _ f g x = f (g x) - -otherwise : Bool -otherwise = True - - --- --- The Integer type --- - --- Instances: - -num_Integer : Num Integer -num_Integer = rec zero = 0 - plus = prim_add_Integer - minus = prim_sub_Integer - one = 1 - times = prim_mul_Integer - div = prim_div_Integer - mod = prim_mod_Integer - negate = prim_neg_Integer - eq = prim_eq_Integer - compare = prim_cmp_Integer - -show_Integer : Show Integer -show_Integer = rec show = prim_show_Integer - - --- --- The Double type --- - --- Instances: - -num_Double : Num Double -num_Double = rec zero = 0.0 - plus = prim_add_Double - minus = prim_sub_Double - one = 1.0 - times = prim_mul_Double - div = prim_div_Double - mod = prim_mod_Double - negate = prim_neg_Double - eq = prim_eq_Double - compare = prim_cmp_Double - -show_Double : Show Double -show_Double = rec show = prim_show_Double - - - --- --- The String type --- - --- Instances: - -add_String : Add String -add_String = rec zero = "" - plus = prim_add_String - - -ord_String : Ord String -ord_String = rec eq = prim_eq_Str - compare = prim_cmp_String - -show_String : Show String -show_String = rec show = prim_show_String - - --- --- The Bool type --- - -data Bool : Type where - True : Bool - False : Bool - --- derive Show Bool --- derive Eq Bool --- derive Ord Bool - -not : Bool -> Bool -not b = if b then False else True - --- Instances: - -neg_Bool : Neg Bool -neg_Bool = rec negate = not - -add_Bool : Add Bool -add_Bool = rec zero = False - plus = \x -> \y -> x || y - -mul_Bool : Add Bool -mul_Bool = rec one = True - times = \x -> \y -> x && y - - --- --- Tuples --- - -Pair : Type -> Type -> Type -Pair A B = sig { p1 : A; p2 : B } - -pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B -pair _ _ x y = rec { p1 = x; p2 = y } - -fst : (A:Type) -> (B:Type) -> Pair A B -> A -fst _ _ p = case p of Pair _ _ x _ -> x - -snd : (A:Type) -> (B:Type) -> Pair A B -> B -snd _ _ p = case p of Pair _ _ x _ -> x - -{- - - syntax: - - (x1,...,xn) => { p1 = e1; ... ; pn = en } - - where n >= 2 and x1,...,xn are expressions or patterns - --} - - --- --- The List type --- - -data List : Type -> Type where - Nil : (A:Type) -> List A - Cons : (A:Type) -> A -> List A -> List A - -foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B -foldr _ _ _ x [] = x -foldr A B f x (y::ys) = f y (foldr A B f x ys) - -length : (A:Type) -> List A -> Integer -length A = foldr A Integer (\_ -> \y -> y+1) 0 - -map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B -map _ _ _ [] = [] -map A B f (x::xs) = f x :: map A B f xs - -filter : (A:Type) -> (A -> Bool) -> List A -> List A -filter _ _ [] = [] -filter A f (x::xs) | f x = x :: filter A f xs -filter A f (x::xs) = filter A f xs - -append : (A:Type) -> List A -> List A -> List A -append A xs ys = foldr A (List A) (Cons A) ys xs - -concat : (A : Type) -> List (List A) -> List A -concat A = foldr (List A) (List A) (append A) (Nil A) - -partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A) -partition _ _ [] = ([],[]) -partition A p (x::xs) = - let r : Pair (List A) (List A) = partition A p xs - in if p x then (x :: fst r, snd r) else (fst r, x :: snd r) - - --- Instances: - -add_List : (A : Type) -> Add (List A) -add_List A = rec zero = Nil A - plus = append A - - -monad_List : Monad List -monad_list = rec return = \A -> \x -> Cons A x (Nil A) - bind = \A -> \B -> \m -> \k -> concat B (map A B k m) - - - - - --- --- The Maybe type --- - -data Maybe : Type -> Type where - Nothing : (A : Type) -> Maybe A - Just : (A : Type) -> A -> Maybe A - --- derive Show Maybe -derive Eq Maybe --- derive Ord Maybe - - -fromMaybe : (A : Type) -> A -> Maybe A -> A -fromMaybe _ x Nothing = x -fromMaybe _ _ (Just x) = x - -maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A -maybe _ _ x _ Nothing = x -maybe _ _ _ f (Just x) = f x - - --- Instances: - -monad_Maybe : Monad Maybe -monad_Maybe = - rec return = Just - bind = \A -> \B -> \m -> \k -> - case m of - Nothing _ -> Nothing B - Just _ x -> k x - - - - --- --- The Num class --- - -Num : Type -> Type -Num = sig zero : A - plus : A -> A -> A - minus : A -> A -> A - one : A - times : A -> A -> A - div : A -> A -> A - mod : A -> A -> A - negate : A -> A - eq : A -> A -> Bool - compare : A -> A -> Ordering - - - - --- --- The Add class --- - -Add : Type -> Type -Add = sig zero : A - plus : A -> A -> A - -zero : (A : Type) -> Add A -> A -zero _ d = d.zero - -plus : (A : Type) -> Add A -> A -> A -> A -plus _ d = d.plus - -sum : (A:Type) -> Add A -> List A -> A -sum A d = foldr A A d.plus d.zero - - --- Operators: - -{- - (x + y) => (plus ? ? x y) --} - - - - - --- --- The Sub class --- - -Sub : Type -> Type -Sub = sig minus : A -> A -> A - -minus : (A : Type) -> Sub A -> A -minus _ d = d.minus - - - - - --- --- The Mul class --- - -Mul : Type -> Type -Mul = sig one : A - times : A -> A -> A - -one : (A : Type) -> Mul A -> A -one _ d = d.one - -times : (A : Type) -> Mul A -> A -> A -> A -times _ d = d.times - -product : (A:Type) -> Mul A -> List A -> A -product A d = foldr A A d.times d.one - --- Operators: - -{- - (x * y) => (times ? ? x y) --} - - - - --- --- The Div class --- - -Div : Type -> Type -Div = sig div : A -> A -> A - mod : A -> A -> A - -div : (A : Type) -> Div A -> A -> A -> A -div _ d = d.div - -mod : (A : Type) -> Div A -> A -> A -> A -mod _ d = d.mod - --- Operators: - -{- - (x / y) => (div ? ? x y) - (x % y) => (mod ? ? x y) --} - - - - - --- --- The Neg class --- - -Neg : Type -> Type -Neg = sig negate : A -> A - -negate : (A : Type) -> Neg A -> A -> A -negate _ d = d.negate - --- Operators: - -{- - (-x) => negate ? ? x --} - - - - --- --- The Eq class --- - -Eq : Type -> Type -Eq A = sig eq : A -> A -> Bool - -eq : (A : Type) -> Eq A -> A -> A -> Bool -eq _ d = d.eq - -neq : (A : Type) -> Eq A -> A -> A -> Bool -neq A d x y = not (eq A d x y) - - --- Operators: - -{- - (x == y) => (eq ? ? x y) - (x /= y) => (neq ? ? x y) --} - - - - - --- --- The Ord class --- - -data Ordering : Type where - LT : Ordering - EQ : Ordering - GT : Ordering - -Ord : Type -> Type -Ord A = sig eq : A -> A -> Bool - compare : A -> A -> Ordering - -compare : (A : Type) -> Ord A -> A -> A -> Ordering -compare _ d = d.compare - -ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool -ordOp f A d x y = f (compare A d x y) - -lt : (A : Type) -> Ord A -> A -> A -> Bool -lt = ordOp (\o -> case o of { LT -> True; _ -> False }) - -le : (A : Type) -> Ord A -> A -> A -> Bool -le = ordOp (\o -> case o of { GT -> False; _ -> True }) - -ge : (A : Type) -> Ord A -> A -> A -> Bool -ge = ordOp (\o -> case o of { LT -> False; _ -> True }) - -gt : (A : Type) -> Ord A -> A -> A -> Bool -gt = ordOp (\o -> case o of { GT -> True; _ -> False }) - --- Operators: - -{- - (x < y) => (lt ? ? x y) - (x <= y) => (le ? ? x y) - (x >= y) => (ge ? ? x y) - (x > y) => (gt ? ? x y) --} - - - - - - --- --- The Show class --- - -Show : Type -> Type -Show A = sig show : A -> String - -show : (A : Type) -> Show A -> A -> String -show _ d = d.show - - - - - - --- --- The Monoid class --- - -Monoid : Type -> Type -Monoid = sig mzero : A - mplus : A -> A -> A - - - - --- --- The Compos class --- - -Compos : (C : Type) -> (C -> Type) -> Type -Compos C T = sig - composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c - composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b - -composOp : (C : Type) -> (T : C -> Type) -> (d : Compos C T) - -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c -composOp _ _ d = d.composOp - -composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B - -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b -composFold _ _ d = d.composFold - - - - - --- --- The Monad class --- - -Monad : (Type -> Type) -> Type -Monad M = sig return : (A : Type) -> M A - bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B - -return : (M : Type -> Type) -> Monad M -> M A -return _ d = d.return - -bind : (M : Type -> Type) -> Monad M - -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B -bind _ d = d.bind - --- Operators: - -{- - (x >>= y) => bind ? ? ? ? x y - (x >> y) => bind ? ? ? ? x (\_ -> y) --} - diff --git a/transfer/lib/prelude.tra b/transfer/lib/prelude.tra new file mode 100644 index 000000000..fe2d1b296 --- /dev/null +++ b/transfer/lib/prelude.tra @@ -0,0 +1,502 @@ +-- +-- Prelude for the transfer language. +-- + + +-- +-- Basic functions +-- + +const : (A:Type) -> (B:Type) -> A -> B -> A +const _ _ x _ = x + +id : (A:Type) -> A -> A +id _ x = x + +flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C +flip _ _ _ f x y = f y x + +compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C +compose _ _ _ f g x = f (g x) + +otherwise : Bool +otherwise = True + + +-- +-- The Integer type +-- + +-- Instances: + +num_Integer : Num Integer +num_Integer = rec zero = 0 + plus = prim_add_Integer + minus = prim_sub_Integer + one = 1 + times = prim_mul_Integer + div = prim_div_Integer + mod = prim_mod_Integer + negate = prim_neg_Integer + eq = prim_eq_Integer + compare = prim_cmp_Integer + +show_Integer : Show Integer +show_Integer = rec show = prim_show_Integer + + +-- +-- The Double type +-- + +-- Instances: + +num_Double : Num Double +num_Double = rec zero = 0.0 + plus = prim_add_Double + minus = prim_sub_Double + one = 1.0 + times = prim_mul_Double + div = prim_div_Double + mod = prim_mod_Double + negate = prim_neg_Double + eq = prim_eq_Double + compare = prim_cmp_Double + +show_Double : Show Double +show_Double = rec show = prim_show_Double + + + +-- +-- The String type +-- + +-- Instances: + +add_String : Add String +add_String = rec zero = "" + plus = prim_add_String + + +ord_String : Ord String +ord_String = rec eq = prim_eq_Str + compare = prim_cmp_String + +show_String : Show String +show_String = rec show = prim_show_String + + +-- +-- The Bool type +-- + +data Bool : Type where + True : Bool + False : Bool + +-- derive Show Bool +-- derive Eq Bool +-- derive Ord Bool + +not : Bool -> Bool +not b = if b then False else True + +-- Instances: + +neg_Bool : Neg Bool +neg_Bool = rec negate = not + +add_Bool : Add Bool +add_Bool = rec zero = False + plus = \x -> \y -> x || y + +mul_Bool : Add Bool +mul_Bool = rec one = True + times = \x -> \y -> x && y + + +-- +-- Tuples +-- + +Pair : Type -> Type -> Type +Pair A B = sig { p1 : A; p2 : B } + +pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B +pair _ _ x y = rec { p1 = x; p2 = y } + +fst : (A:Type) -> (B:Type) -> Pair A B -> A +fst _ _ p = case p of Pair _ _ x _ -> x + +snd : (A:Type) -> (B:Type) -> Pair A B -> B +snd _ _ p = case p of Pair _ _ x _ -> x + +{- + + syntax: + + (x1,...,xn) => { p1 = e1; ... ; pn = en } + + where n >= 2 and x1,...,xn are expressions or patterns + +-} + + +-- +-- The List type +-- + +data List : Type -> Type where + Nil : (A:Type) -> List A + Cons : (A:Type) -> A -> List A -> List A + +foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B +foldr _ _ _ x [] = x +foldr A B f x (y::ys) = f y (foldr A B f x ys) + +length : (A:Type) -> List A -> Integer +length A = foldr A Integer (\_ -> \y -> y+1) 0 + +map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B +map _ _ _ [] = [] +map A B f (x::xs) = f x :: map A B f xs + +filter : (A:Type) -> (A -> Bool) -> List A -> List A +filter _ _ [] = [] +filter A f (x::xs) | f x = x :: filter A f xs +filter A f (x::xs) = filter A f xs + +append : (A:Type) -> List A -> List A -> List A +append A xs ys = foldr A (List A) (Cons A) ys xs + +concat : (A : Type) -> List (List A) -> List A +concat A = foldr (List A) (List A) (append A) (Nil A) + +partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A) +partition _ _ [] = ([],[]) +partition A p (x::xs) = + let r : Pair (List A) (List A) = partition A p xs + in if p x then (x :: fst r, snd r) else (fst r, x :: snd r) + + +-- Instances: + +add_List : (A : Type) -> Add (List A) +add_List A = rec zero = Nil A + plus = append A + + +monad_List : Monad List +monad_list = rec return = \A -> \x -> Cons A x (Nil A) + bind = \A -> \B -> \m -> \k -> concat B (map A B k m) + + + + + +-- +-- The Maybe type +-- + +data Maybe : Type -> Type where + Nothing : (A : Type) -> Maybe A + Just : (A : Type) -> A -> Maybe A + +-- derive Show Maybe +derive Eq Maybe +-- derive Ord Maybe + + +fromMaybe : (A : Type) -> A -> Maybe A -> A +fromMaybe _ x Nothing = x +fromMaybe _ _ (Just x) = x + +maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A +maybe _ _ x _ Nothing = x +maybe _ _ _ f (Just x) = f x + + +-- Instances: + +monad_Maybe : Monad Maybe +monad_Maybe = + rec return = Just + bind = \A -> \B -> \m -> \k -> + case m of + Nothing _ -> Nothing B + Just _ x -> k x + + + + +-- +-- The Num class +-- + +Num : Type -> Type +Num = sig zero : A + plus : A -> A -> A + minus : A -> A -> A + one : A + times : A -> A -> A + div : A -> A -> A + mod : A -> A -> A + negate : A -> A + eq : A -> A -> Bool + compare : A -> A -> Ordering + + + + +-- +-- The Add class +-- + +Add : Type -> Type +Add = sig zero : A + plus : A -> A -> A + +zero : (A : Type) -> Add A -> A +zero _ d = d.zero + +plus : (A : Type) -> Add A -> A -> A -> A +plus _ d = d.plus + +sum : (A:Type) -> Add A -> List A -> A +sum A d = foldr A A d.plus d.zero + + +-- Operators: + +{- + (x + y) => (plus ? ? x y) +-} + + + + + +-- +-- The Sub class +-- + +Sub : Type -> Type +Sub = sig minus : A -> A -> A + +minus : (A : Type) -> Sub A -> A +minus _ d = d.minus + + + + + +-- +-- The Mul class +-- + +Mul : Type -> Type +Mul = sig one : A + times : A -> A -> A + +one : (A : Type) -> Mul A -> A +one _ d = d.one + +times : (A : Type) -> Mul A -> A -> A -> A +times _ d = d.times + +product : (A:Type) -> Mul A -> List A -> A +product A d = foldr A A d.times d.one + +-- Operators: + +{- + (x * y) => (times ? ? x y) +-} + + + + +-- +-- The Div class +-- + +Div : Type -> Type +Div = sig div : A -> A -> A + mod : A -> A -> A + +div : (A : Type) -> Div A -> A -> A -> A +div _ d = d.div + +mod : (A : Type) -> Div A -> A -> A -> A +mod _ d = d.mod + +-- Operators: + +{- + (x / y) => (div ? ? x y) + (x % y) => (mod ? ? x y) +-} + + + + + +-- +-- The Neg class +-- + +Neg : Type -> Type +Neg = sig negate : A -> A + +negate : (A : Type) -> Neg A -> A -> A +negate _ d = d.negate + +-- Operators: + +{- + (-x) => negate ? ? x +-} + + + + +-- +-- The Eq class +-- + +Eq : Type -> Type +Eq A = sig eq : A -> A -> Bool + +eq : (A : Type) -> Eq A -> A -> A -> Bool +eq _ d = d.eq + +neq : (A : Type) -> Eq A -> A -> A -> Bool +neq A d x y = not (eq A d x y) + + +-- Operators: + +{- + (x == y) => (eq ? ? x y) + (x /= y) => (neq ? ? x y) +-} + + + + + +-- +-- The Ord class +-- + +data Ordering : Type where + LT : Ordering + EQ : Ordering + GT : Ordering + +Ord : Type -> Type +Ord A = sig eq : A -> A -> Bool + compare : A -> A -> Ordering + +compare : (A : Type) -> Ord A -> A -> A -> Ordering +compare _ d = d.compare + +ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool +ordOp f A d x y = f (compare A d x y) + +lt : (A : Type) -> Ord A -> A -> A -> Bool +lt = ordOp (\o -> case o of { LT -> True; _ -> False }) + +le : (A : Type) -> Ord A -> A -> A -> Bool +le = ordOp (\o -> case o of { GT -> False; _ -> True }) + +ge : (A : Type) -> Ord A -> A -> A -> Bool +ge = ordOp (\o -> case o of { LT -> False; _ -> True }) + +gt : (A : Type) -> Ord A -> A -> A -> Bool +gt = ordOp (\o -> case o of { GT -> True; _ -> False }) + +-- Operators: + +{- + (x < y) => (lt ? ? x y) + (x <= y) => (le ? ? x y) + (x >= y) => (ge ? ? x y) + (x > y) => (gt ? ? x y) +-} + + + + + + +-- +-- The Show class +-- + +Show : Type -> Type +Show A = sig show : A -> String + +show : (A : Type) -> Show A -> A -> String +show _ d = d.show + + + + + + +-- +-- The Monoid class +-- + +Monoid : Type -> Type +Monoid = sig mzero : A + mplus : A -> A -> A + + + + +-- +-- The Compos class +-- + +Compos : (C : Type) -> (C -> Type) -> Type +Compos C T = sig + composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c + composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b + +composOp : (C : Type) -> (T : C -> Type) -> (d : Compos C T) + -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c +composOp _ _ d = d.composOp + +composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B + -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b +composFold _ _ d = d.composFold + + + + + +-- +-- The Monad class +-- + +Monad : (Type -> Type) -> Type +Monad M = sig return : (A : Type) -> M A + bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B + +return : (M : Type -> Type) -> Monad M -> M A +return _ d = d.return + +bind : (M : Type -> Type) -> Monad M + -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B +bind _ d = d.bind + +-- Operators: + +{- + (x >>= y) => bind ? ? ? ? x y + (x >> y) => bind ? ? ? ? x (\_ -> y) +-} + -- cgit v1.2.3