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. --- 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 +++ 22 files changed, 490 insertions(+), 490 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 (limited to 'transfer/examples') 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 + -- cgit v1.2.3