From a68cd282cb83d8ace42baffe0b0d3a00f3455920 Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 17:40:32 +0000 Subject: [PATCH] Transfer: reimplement operators with type classes. --- src/Transfer/Interpreter.hs | 60 +++++++++++++-------- src/Transfer/SyntaxToCore.hs | 38 ++++++++----- transfer/examples/fib.tr | 3 +- transfer/lib/bool.tr | 2 + transfer/lib/nat.tr | 16 ++++-- transfer/lib/prelude.tr | 101 ++++++++++++++++++++++++++++------- 6 files changed, 157 insertions(+), 63 deletions(-) diff --git a/src/Transfer/Interpreter.hs b/src/Transfer/Interpreter.hs index 90e3a70ca..02c28bc53 100644 --- a/src/Transfer/Interpreter.hs +++ b/src/Transfer/Interpreter.hs @@ -53,33 +53,47 @@ builtin :: Env builtin = mkEnv [(CIdent "Int",VType), (CIdent "String",VType), - mkIntUn "neg" negate, - mkIntBin "add" (+), - mkIntBin "sub" (-), - mkIntBin "mul" (*), - mkIntBin "div" div, - mkIntBin "mod" mod, - mkIntCmp "lt" (<), - mkIntCmp "le" (<=), - mkIntCmp "gt" (>), - mkIntCmp "ge" (>=), - mkIntCmp "eq" (==), - mkIntCmp "ne" (/=)] + mkIntUn "neg" negate toInt, + mkIntBin "add" (+) toInt, + mkIntBin "sub" (-) toInt, + mkIntBin "mul" (*) toInt, + mkIntBin "div" div toInt, + mkIntBin "mod" mod toInt, + mkIntBin "eq" (==) toBool, + mkIntBin "cmp" compare toOrd, + mkIntUn "show" show toStr, + mkStrBin "add" (++) toStr, + mkStrBin "eq" (==) toBool, + mkStrBin "cmp" compare toOrd, + mkStrUn "show" show toStr + ] where - mkIntUn x f = let c = CIdent ("prim_"++x++"_Int") - in (c, VPrim (\n -> appInt1 (VInt . f) n)) - mkIntBin x f = let c = CIdent ("prim_"++x++"_Int") - in (c, VPrim (\n -> VPrim (\m -> appInt2 (\n m -> VInt (f n m)) n m ))) - mkIntCmp x f = let c = CIdent ("prim_"++x++"_Int") - in (c, VPrim (\n -> VPrim (\m -> appInt2 (\n m -> toBool (f n m)) n m))) - toBool b = VCons (CIdent (if b then "True" else "False")) [] - appInt1 f x = case x of - VInt n -> f n + toInt i = VInt i + toBool b = VCons (CIdent (show b)) [] + toOrd o = VCons (CIdent (show o)) [] + toStr s = VStr s + mkIntUn x f g = let c = CIdent ("prim_"++x++"_Int") + in (c, VPrim (\n -> appInt1 f g n)) + mkIntBin x f g = let c = CIdent ("prim_"++x++"_Int") + in (c, VPrim (\n -> VPrim (\m -> appInt2 f g n m ))) + appInt1 f g x = case x of + VInt n -> g (f n) _ -> error $ printValue x ++ " is not an integer" - appInt2 f x y = case (x,y) of - (VInt n,VInt m) -> f n m + appInt2 f g x y = case (x,y) of + (VInt n,VInt m) -> g (f n m) _ -> error $ printValue x ++ " and " ++ printValue y ++ " are not both integers" + mkStrUn x f g = let c = CIdent ("prim_"++x++"_Str") + in (c, VPrim (\n -> appStr1 f g n)) + mkStrBin x f g = let c = CIdent ("prim_"++x++"_Str") + in (c, VPrim (\n -> VPrim (\m -> appStr2 f g n m ))) + appStr1 f g x = case x of + VStr n -> g (f n) + _ -> error $ printValue x ++ " is not an integer" + appStr2 f g x y = case (x,y) of + (VStr n,VStr m) -> g (f n m) + _ -> error $ printValue x ++ " and " ++ printValue y + ++ " are not both strings" addModuleEnv :: Env -> Module -> Env addModuleEnv env (Module ds) = diff --git a/src/Transfer/SyntaxToCore.hs b/src/Transfer/SyntaxToCore.hs index 3a5bdac20..ad3e68f86 100644 --- a/src/Transfer/SyntaxToCore.hs +++ b/src/Transfer/SyntaxToCore.hs @@ -28,11 +28,11 @@ declsToCore :: [Decl] -> [Decl] declsToCore m = evalState (declsToCore_ m) newState declsToCore_ :: [Decl] -> C [Decl] -declsToCore_ = numberMetas +declsToCore_ = desugar + >>> numberMetas >>> deriveDecls >>> replaceCons >>> compilePattDecls - >>> desugar >>> optimize optimize :: [Decl] -> C [Decl] @@ -361,21 +361,31 @@ desugar = return . map f EPiNoVar exp0 exp1 -> EPi VWild <| exp0 <| exp1 EOr exp0 exp1 -> andBool <| exp0 <| exp1 EAnd exp0 exp1 -> orBool <| exp0 <| exp1 - EEq exp0 exp1 -> appIntBin "eq" <| exp0 <| exp1 - ENe exp0 exp1 -> appIntBin "ne" <| exp0 <| exp1 - ELt exp0 exp1 -> appIntBin "lt" <| exp0 <| exp1 - ELe exp0 exp1 -> appIntBin "le" <| exp0 <| exp1 - EGt exp0 exp1 -> appIntBin "gt" <| exp0 <| exp1 - EGe exp0 exp1 -> appIntBin "ge" <| exp0 <| exp1 - EAdd exp0 exp1 -> appIntBin "add" <| exp0 <| exp1 - ESub exp0 exp1 -> appIntBin "sub" <| exp0 <| exp1 - EMul exp0 exp1 -> appIntBin "mul" <| exp0 <| exp1 - EDiv exp0 exp1 -> appIntBin "div" <| exp0 <| exp1 - EMod exp0 exp1 -> appIntBin "mod" <| exp0 <| exp1 - ENeg exp0 -> appIntUn "neg" <| exp0 + EEq exp0 exp1 -> overlBin "eq" <| exp0 <| exp1 + ENe exp0 exp1 -> overlBin "ne" <| exp0 <| exp1 + ELt exp0 exp1 -> overlBin "lt" <| exp0 <| exp1 + ELe exp0 exp1 -> overlBin "le" <| exp0 <| exp1 + EGt exp0 exp1 -> overlBin "gt" <| exp0 <| exp1 + EGe exp0 exp1 -> overlBin "ge" <| exp0 <| exp1 + EAdd exp0 exp1 -> overlBin "plus" <| exp0 <| exp1 + ESub exp0 exp1 -> overlBin "minus" <| exp0 <| exp1 + EMul exp0 exp1 -> overlBin "times" <| exp0 <| exp1 + EDiv exp0 exp1 -> overlBin "div" <| exp0 <| exp1 + EMod exp0 exp1 -> overlBin "mod" <| exp0 <| exp1 + ENeg exp0 -> overlUn "neg" <| exp0 _ -> composOp f x where g <| x = g (f x) +-- +-- * Use an overloaded function. +-- + +overlUn :: String -> Exp -> Exp +overlUn f e1 = apply (EVar (Ident f)) [EMeta,EVar (Ident "num_Integer"),e1] -- FIXME: hack, should be ? + +overlBin :: String -> Exp -> Exp -> Exp +overlBin f e1 e2 = apply (EVar (Ident f)) [EMeta,EVar (Ident "num_Integer"),e1,e2] -- FIXME: hack, should be ? + -- -- * Integers -- diff --git a/transfer/examples/fib.tr b/transfer/examples/fib.tr index 30513e226..988b5e772 100644 --- a/transfer/examples/fib.tr +++ b/transfer/examples/fib.tr @@ -1,6 +1,7 @@ import nat +import prelude -fib : Int -> Int +fib : Integer -> Integer fib 0 = 1 fib 1 = 1 fib n = fib (n-1) + fib (n-2) diff --git a/transfer/lib/bool.tr b/transfer/lib/bool.tr index b8c1c95a5..2639422b7 100644 --- a/transfer/lib/bool.tr +++ b/transfer/lib/bool.tr @@ -1,3 +1,5 @@ +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 index c529e5238..b13a809ed 100644 --- a/transfer/lib/nat.tr +++ b/transfer/lib/nat.tr @@ -1,18 +1,24 @@ +import prelude + data Nat : Type where Zero : Nat Succ : (n:Nat) -> Nat -plus : Nat -> Nat -> Nat -plus Zero y = y -plus (Succ x) y = Succ (plus x y) +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 -> Int +natToInt : Nat -> Integer natToInt Zero = 0 natToInt (Succ n) = 1 + natToInt n -intToNat : Int -> Nat +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 index cf2167c6d..409647a26 100644 --- a/transfer/lib/prelude.tr +++ b/transfer/lib/prelude.tr @@ -26,6 +26,35 @@ not : Bool -> Bool not b = if b then False else True +-- +-- 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 + +-- Instances: + +num_Integer : Num Integer +num_Integer = rec zero = 0 + plus = prim_add_Int + minus = prim_sub_Int + one = 1 + times = prim_mul_Int + div = prim_div_Int + mod = prim_mod_Int + negate = prim_neg_Int + eq = prim_eq_Int + compare = prim_cmp_Int -- -- The Add class @@ -53,31 +82,42 @@ sum A d (Cons _ x xs) = d.plus x (sum A d xs) -- Instances: -add_Integer : Add Integer -add_Integer = rec zero = 0 - plus = prim_add_Int +-- num_Integer add_String : Add String add_String = rec zero = "" plus = prim_add_Str +-- +-- The Sub class +-- + +Sub : Type -> Type +Sub = sig minus : A -> A -> A + +minus : (A : Type) -> Sub A -> A +minus _ d = d.minus + +-- Instances: + +-- num_Integer -- --- The Prod class +-- The Mul class -- -Prod : Type -> Type -Prod = sig one : A - times : A -> A -> A +Mul : Type -> Type +Mul = sig one : A + times : A -> A -> A -one : (A : Type) -> Prod A -> A +one : (A : Type) -> Mul A -> A one _ d = d.one -times : (A : Type) -> Prod A -> A -> A -> A +times : (A : Type) -> Mul A -> A -> A -> A times _ d = d.times -product : (A:Type) -> Prod A -> List A -> A +product : (A:Type) -> Mul A -> List A -> A product _ d (Nil _) = d.one product A d (Cons _ x xs) = d.times x (product A d xs) @@ -89,9 +129,34 @@ product A d (Cons _ x xs) = d.times x (product A d xs) -- Instances: -prod_Integer : Add Integer -prod_Integer = rec one = 1 - times = prim_mul_Int +-- num_Integer + + +-- +-- 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) +-} + +-- Instances: + +-- num_Integer + -- @@ -112,8 +177,7 @@ negate _ d = d.neg -- Instances: -neg_Integer : Neg Integer -neg_Integer = rec negate = prim_neg_Int +-- num_Integer neg_Bool : Neg Bool neg_Bool = rec negate = not @@ -143,8 +207,7 @@ neq A d x y = not (eq A d x y) -- Instances: -eq_Integer : Eq Integer -eq_Integer = rec eq = prim_eq_Int +-- num_Integer eq_String : Eq String eq_String = rec eq = prim_eq_Str @@ -193,9 +256,7 @@ gt = ordOp (\o -> case o of { GT -> True; _ -> False }) -- Instances: -ord_Integer : Ord Integer -ord_Integer = rec eq = prim_eq_Int - compare = prim_cmp_Int +-- num_Integer ord_String : Ord String ord_String = rec eq = prim_eq_Str