From f8c8fc44de59d34c5634b66311391438030e6b5b Mon Sep 17 00:00:00 2001 From: Julien Moutinho <julm+symantic@autogeree.net> Date: Mon, 14 Nov 2016 20:56:05 +0100 Subject: [PATCH] Eq, Ord --- Language/Symantic/AST/Test.hs | 20 +++++-- Language/Symantic/Expr/Applicative.hs | 2 + Language/Symantic/Expr/Bool.hs | 22 +++---- Language/Symantic/Expr/Eq.hs | 31 ++++++---- Language/Symantic/Expr/If.hs | 4 ++ Language/Symantic/Expr/Integral.hs | 29 ++++----- Language/Symantic/Expr/Lambda.hs | 11 ++++ Language/Symantic/Expr/List.hs | 6 +- Language/Symantic/Expr/Monad.hs | 7 +-- Language/Symantic/Expr/Num.hs | 30 ++++------ Language/Symantic/Expr/Ord.hs | 86 ++++++++++++++++++++++++--- Language/Symantic/Repr/Text.hs | 43 ++++---------- 12 files changed, 174 insertions(+), 117 deletions(-) diff --git a/Language/Symantic/AST/Test.hs b/Language/Symantic/AST/Test.hs index 548f206..9e0848d 100644 --- a/Language/Symantic/AST/Test.hs +++ b/Language/Symantic/AST/Test.hs @@ -15,6 +15,7 @@ module AST.Test where import Test.Tasty -- import Test.Tasty.HUnit +import qualified Data.Ord as Ord import qualified Data.List as List import Data.Proxy (Proxy(..)) import Data.Text (Text) @@ -42,16 +43,16 @@ instance Show AST where case ast of AST _ [] -> showString n AST "->" [a] -> - showParen (p >= prec_arrow) $ + showParen (p Ord.>= prec_arrow) $ showString ("("++n++") ") . showsPrec prec_arrow a AST "->" [a, b] -> - showParen (p >= prec_arrow) $ + showParen (p Ord.>= prec_arrow) $ showsPrec prec_arrow a . showString (" "++n++" ") . showsPrec prec_arrow b AST "\\" [var, ty, body] -> - showParen (p >= prec_lambda) $ + showParen (p Ord.>= prec_lambda) $ showString ("\\(") . showsPrec prec_lambda var . showString (":") . @@ -59,7 +60,7 @@ instance Show AST where showString (") -> ") . showsPrec prec_lambda body AST "$" [fun, arg] -> - showParen (p >= prec_app) $ + showParen (p Ord.>= prec_app) $ showsPrec prec_app fun . showString (" $ ") . showsPrec prec_app arg @@ -755,11 +756,13 @@ instance -- Expr_From AST Expr_Eq ) => Expr_From AST (Expr_Eq root) where expr_from ex ast ctx k = case ast of - AST "==" asts -> from_ast2 asts eq_from ex ast ctx k + AST "==" asts -> from_ast2 asts (eq_from (Expr.==)) ex ast ctx k + AST "/=" asts -> from_ast2 asts (eq_from (Expr./=)) ex ast ctx k _ -> Left $ error_expr_unsupported ex ast instance -- Expr_From AST Expr_Ord ( Expr_From AST root , Type0_Eq (Type_Root_of_Expr root) + , Type0_Lift Type_Bool (Type_of_Expr root) , Type0_Lift Type_Ordering (Type_of_Expr root) , Type0_Constraint Ord (Type_Root_of_Expr root) , Error_Expr_Lift (Error_Expr_of_Root AST root) (Error_of_Expr AST root) @@ -767,8 +770,15 @@ instance -- Expr_From AST Expr_Ord , IBool (Is_Last_Expr (Expr_Ord root) root) ) => Expr_From AST (Expr_Ord root) where expr_from ex ast ctx k = + let c = (Proxy :: Proxy Ord) in case ast of AST "compare" asts -> from_ast2 asts compare_from ex ast ctx k + AST "<" asts -> from_ast2 asts (ord_from (Expr.<)) ex ast ctx k + AST "<=" asts -> from_ast2 asts (ord_from (Expr.<=)) ex ast ctx k + AST ">" asts -> from_ast2 asts (ord_from (Expr.>)) ex ast ctx k + AST ">=" asts -> from_ast2 asts (ord_from (Expr.>=)) ex ast ctx k + AST "min" asts -> class_op2_from_AST Expr.min c asts ex ast ctx k + AST "max" asts -> class_op2_from_AST Expr.max c asts ex ast ctx k _ -> Left $ error_expr_unsupported ex ast instance -- Expr_From AST Expr_List ( Expr_From AST root diff --git a/Language/Symantic/Expr/Applicative.hs b/Language/Symantic/Expr/Applicative.hs index b03964f..ff97f90 100644 --- a/Language/Symantic/Expr/Applicative.hs +++ b/Language/Symantic/Expr/Applicative.hs @@ -56,6 +56,8 @@ instance Sym_Applicative Repr_Text where Repr_Text $ \p v -> let p' = precedence_LtStarGt in paren p p' $ fg p' v <> " <*> " <> fa p' v +precedence_LtStarGt :: Precedence +precedence_LtStarGt = Precedence 4 instance ( Sym_Applicative r1 , Sym_Applicative r2 diff --git a/Language/Symantic/Expr/Bool.hs b/Language/Symantic/Expr/Bool.hs index e045257..286a050 100644 --- a/Language/Symantic/Expr/Bool.hs +++ b/Language/Symantic/Expr/Bool.hs @@ -34,13 +34,16 @@ class Sym_Bool repr where default not :: Trans t repr => t repr Bool -> t repr Bool default (&&) :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool default (||) :: Trans t repr => t repr Bool -> t repr Bool -> t repr Bool + bool = trans_lift . bool not = trans_map1 not (&&) = trans_map2 (&&) (||) = trans_map2 (||) + infixr 2 || infixr 2 `xor` infixr 3 && + instance Sym_Bool Repr_Host where bool = Repr_Host not = liftM Bool.not @@ -51,20 +54,11 @@ instance Sym_Bool Repr_Text where Text.pack (show a) not (Repr_Text x) = Repr_Text $ \p v -> - let p' = precedence_Not in - paren p p' $ "!" <> x p' v - (&&) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_And in - paren p p' $ x p' v <> " && " <> y p' v - (||) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Or in - paren p p' $ x p' v <> " || " <> y p' v - xor (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Xor in - paren p p' $ "xor " <> x p' v <> " " <> y p' v + let p' = Precedence 9 in + paren p p' $ "not " <> x p' v + (&&) = repr_text_infix "&&" (Precedence 6) + (||) = repr_text_infix "||" (Precedence 5) + xor = repr_text_infix "`xor`" (Precedence 5) instance ( Sym_Bool r1 , Sym_Bool r2 diff --git a/Language/Symantic/Expr/Eq.hs b/Language/Symantic/Expr/Eq.hs index 9140489..8d4a02c 100644 --- a/Language/Symantic/Expr/Eq.hs +++ b/Language/Symantic/Expr/Eq.hs @@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -13,10 +14,9 @@ module Language.Symantic.Expr.Eq where import Control.Monad import qualified Data.Eq as Eq -import Data.Monoid import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) -import Prelude hiding ((==)) +import Prelude hiding ((==), (/=)) import Language.Symantic.Type import Language.Symantic.Repr @@ -29,23 +29,29 @@ import Language.Symantic.Trans.Common -- | Symantic. class Sym_Eq repr where (==) :: Eq a => repr a -> repr a -> repr Bool - default (==) :: (Trans t repr, Eq a) - => t repr a -> t repr a -> t repr Bool + (/=) :: Eq a => repr a -> repr a -> repr Bool + + default (==) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool + default (/=) :: (Trans t repr, Eq a) => t repr a -> t repr a -> t repr Bool + (==) = trans_map2 (==) + (/=) = trans_map2 (/=) + infix 4 == +infix 4 /= + instance Sym_Eq Repr_Host where (==) = liftM2 (Eq.==) + (/=) = liftM2 (Eq./=) instance Sym_Eq Repr_Text where - (==) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Eq in - paren p p' $ - x p' v <> " == " <> y p' v + (==) = repr_text_infix "==" (Precedence 4) + (/=) = repr_text_infix "/=" (Precedence 4) instance ( Sym_Eq r1 , Sym_Eq r2 ) => Sym_Eq (Dup r1 r2) where (==) (x1 `Dup` x2) (y1 `Dup` y2) = (==) x1 y1 `Dup` (==) x2 y2 + (/=) (x1 `Dup` x2) (y1 `Dup` y2) = (/=) x1 y1 `Dup` (/=) x2 y2 -- * Type 'Expr_Eq' -- | Expression. @@ -65,9 +71,10 @@ eq_from (Error_of_Expr ast root) , Root_of_Expr root ~ root , Type0_Constraint Eq ty - ) => ast -> ast + ) => (forall repr a. (Sym_Eq repr, Eq a) => repr a -> repr a -> repr Bool) + -> ast -> ast -> ExprFrom ast (Expr_Eq root) hs ret -eq_from ast_x ast_y ex ast ctx k = +eq_from test ast_x ast_y ex ast ctx k = expr_from (Proxy::Proxy root) ast_x ctx $ \(ty_x::ty h_x) (Forall_Repr_with_Context x) -> expr_from (Proxy::Proxy root) ast_y ctx $ @@ -75,4 +82,4 @@ eq_from ast_x ast_y ex ast ctx k = check_type0_eq ex ast ty_x ty_y $ \Refl -> check_type0_constraint ex (Proxy::Proxy Eq) ast ty_x $ \Dict -> k type_bool $ Forall_Repr_with_Context $ - \c -> x c == y c + \c -> x c `test` y c diff --git a/Language/Symantic/Expr/If.hs b/Language/Symantic/Expr/If.hs index 740bd6c..cc2061c 100644 --- a/Language/Symantic/Expr/If.hs +++ b/Language/Symantic/Expr/If.hs @@ -35,6 +35,10 @@ instance Sym_If Repr_Text where "if " <> cond p' v <> " then " <> ok p' v <> " else " <> ko p' v + +precedence_If :: Precedence +precedence_If = Precedence 2 + instance ( Sym_If r1 , Sym_If r2 diff --git a/Language/Symantic/Expr/Integral.hs b/Language/Symantic/Expr/Integral.hs index 1cb2b9e..1ee665b 100644 --- a/Language/Symantic/Expr/Integral.hs +++ b/Language/Symantic/Expr/Integral.hs @@ -8,10 +8,10 @@ module Language.Symantic.Expr.Integral where import Control.Monad -import Data.Monoid import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) -import Prelude hiding (quot, rem, div, mod, quotRem, divMod, toInteger) +import Prelude hiding (Integral(..)) +import Prelude (Integral) import qualified Prelude import Language.Symantic.Type @@ -47,10 +47,12 @@ class Sym_Integral repr where quotRem = trans_map2 quotRem divMod = trans_map2 divMod toInteger = trans_map1 toInteger + infixl 7 `quot` infixl 7 `rem` infixl 7 `div` infixl 7 `mod` + instance Sym_Integral Repr_Host where quot = liftM2 Prelude.quot rem = liftM2 Prelude.rem @@ -60,22 +62,10 @@ instance Sym_Integral Repr_Host where divMod = liftM2 Prelude.divMod toInteger = liftM Prelude.toInteger instance Sym_Integral Repr_Text where - quot (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Integral in - paren p p' $ x p' v <> " `quot` " <> y p' v - rem (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Integral in - paren p p' $ x p' v <> " `rem` " <> y p' v - div (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Integral in - paren p p' $ x p' v <> " `div` " <> y p' v - mod (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Integral in - paren p p' $ x p' v <> " `mod` " <> y p' v + quot = repr_text_infix "`quot`" (Precedence 7) + div = repr_text_infix "`div`" (Precedence 7) + rem = repr_text_infix "`rem`" (Precedence 7) + mod = repr_text_infix "`mod`" (Precedence 7) quotRem = repr_text_app2 "quotRem" divMod = repr_text_app2 "divMod" toInteger = repr_text_app1 "toInteger" @@ -91,6 +81,9 @@ instance divMod (x1 `Dup` x2) (y1 `Dup` y2) = divMod x1 y1 `Dup` divMod x2 y2 toInteger (x1 `Dup` x2) = toInteger x1 `Dup` toInteger x2 +precedence_Integral :: Precedence +precedence_Integral = Precedence 7 + -- * Type 'Expr_Integral' -- | Expression. data Expr_Integral (root:: *) diff --git a/Language/Symantic/Expr/Lambda.hs b/Language/Symantic/Expr/Lambda.hs index ba7e9f3..c10bf4f 100644 --- a/Language/Symantic/Expr/Lambda.hs +++ b/Language/Symantic/Expr/Lambda.hs @@ -53,13 +53,16 @@ class Sym_Lambda repr where const :: repr a -> repr b -> repr a const a b = lam (lam . Fun.const) $$ a $$ b + -- | /Lambda composition/. (#) :: repr (b -> c) -> repr (a -> b) -> repr a -> repr c (#) f g a = f $$ (g $$ a) flip :: repr (a -> b -> c) -> repr b -> repr a -> repr c flip f b a = f $$ a $$ b + infixl 0 $$ infixr 9 # + instance Sym_Lambda Repr_Host where ($$) = (Applicative.<*>) lam f = Repr_Host (unRepr_Host . f . Repr_Host) @@ -82,6 +85,14 @@ instance Sym_Lambda Repr_Text where paren p p' $ "let" <> " " <> x <> " = " <> unRepr_Text e p (succ v) <> " in " <> unRepr_Text (in_ (Repr_Text $ \_p _v -> x)) p (succ v) + +precedence_Lambda :: Precedence +precedence_Lambda = Precedence 1 +precedence_Let :: Precedence +precedence_Let = Precedence 3 +precedence_Composition :: Precedence +precedence_Composition = Precedence 9 + instance ( Sym_Lambda r1 , Sym_Lambda r2 diff --git a/Language/Symantic/Expr/List.hs b/Language/Symantic/Expr/List.hs index 43d2535..ee686ee 100644 --- a/Language/Symantic/Expr/List.hs +++ b/Language/Symantic/Expr/List.hs @@ -57,11 +57,10 @@ instance Sym_List Repr_Host where list_zipWith = liftM3 List.zipWith list_reverse = liftM List.reverse instance Sym_List Repr_Text where - list_empty = Repr_Text $ \_p _v -> - "[]" + list_empty = Repr_Text $ \_p _v -> "[]" list_cons (Repr_Text x) (Repr_Text xs) = Repr_Text $ \p v -> - let p' = precedence_List_Cons in + let p' = Precedence 5 in paren p p' $ x p' v <> ":" <> xs p' v list l = Repr_Text $ \_p v -> let p' = precedence_Toplevel in @@ -69,6 +68,7 @@ instance Sym_List Repr_Text where list_filter = repr_text_app2 "list_filter" list_zipWith = repr_text_app3 "list_zipWith" list_reverse = repr_text_app1 "list_reverse" + instance ( Sym_List r1 , Sym_List r2 diff --git a/Language/Symantic/Expr/Monad.hs b/Language/Symantic/Expr/Monad.hs index a1555f7..1c17e37 100644 --- a/Language/Symantic/Expr/Monad.hs +++ b/Language/Symantic/Expr/Monad.hs @@ -15,7 +15,6 @@ module Language.Symantic.Expr.Monad where import Control.Monad (Monad) import qualified Control.Monad as Monad import qualified Data.Function as Fun -import Data.Monoid import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding ((<$>), Monad(..)) @@ -48,10 +47,8 @@ instance Sym_Monad Repr_Host where (>>=) = Monad.liftM2 (Monad.>>=) instance Sym_Monad Repr_Text where return = repr_text_app1 "return" - (>>=) (Repr_Text g) (Repr_Text ma) = - Repr_Text $ \p v -> - let p' = precedence_Bind in - paren p p' $ g p' v <> " >>= " <> ma p' v + (>>=) = repr_text_infix ">>=" (Precedence 1) + instance ( Sym_Monad r1 , Sym_Monad r2 diff --git a/Language/Symantic/Expr/Num.hs b/Language/Symantic/Expr/Num.hs index b14e3b1..05b5c62 100644 --- a/Language/Symantic/Expr/Num.hs +++ b/Language/Symantic/Expr/Num.hs @@ -8,8 +8,8 @@ module Language.Symantic.Expr.Num where import Control.Monad -import Data.Monoid -import Prelude hiding ((+), (-), (*), abs, mod, negate) +import Prelude hiding (Num(..)) +import Prelude (Num) import qualified Prelude import Language.Symantic.Type @@ -27,19 +27,23 @@ class Sym_Num repr where (+) :: Num n => repr n -> repr n -> repr n (-) :: Num n => repr n -> repr n -> repr n (*) :: Num n => repr n -> repr n -> repr n + default abs :: (Trans t repr, Num n) => t repr n -> t repr n default negate :: (Trans t repr, Num n) => t repr n -> t repr n default (+) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n default (-) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n default (*) :: (Trans t repr, Num n) => t repr n -> t repr n -> t repr n + abs = trans_map1 abs negate = trans_map1 negate (+) = trans_map2 (+) (-) = trans_map2 (-) (*) = trans_map2 (*) + infixl 6 + infixl 6 - infixl 7 * + instance Sym_Num Repr_Host where abs = liftM Prelude.abs negate = liftM Prelude.negate @@ -47,23 +51,11 @@ instance Sym_Num Repr_Host where (-) = liftM2 (Prelude.-) (*) = liftM2 (Prelude.*) instance Sym_Num Repr_Text where - abs = repr_text_app1 "abs" - negate (Repr_Text x) = - Repr_Text $ \p v -> - let p' = precedence_Neg in - paren p p' $ "-" <> x p' v - (+) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Add in - paren p p' $ x p' v <> " + " <> y p' v - (-) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Sub in - paren p p' $ x p' v <> " - " <> y p' v - (*) (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Mul in - paren p p' $ x p' v <> " * " <> y p' v + abs = repr_text_app1 "abs" + negate = repr_text_app1 "negate" + (+) = repr_text_infix "+" (Precedence 6) + (-) = repr_text_infix "-" (Precedence 6) + (*) = repr_text_infix "-" (Precedence 7) instance ( Sym_Num r1 , Sym_Num r2 diff --git a/Language/Symantic/Expr/Ord.hs b/Language/Symantic/Expr/Ord.hs index 4292ace..a324a3c 100644 --- a/Language/Symantic/Expr/Ord.hs +++ b/Language/Symantic/Expr/Ord.hs @@ -3,6 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -11,11 +12,11 @@ module Language.Symantic.Expr.Ord where import Control.Monad -import Data.Monoid import qualified Data.Ord as Ord import Data.Proxy (Proxy(..)) import Data.Type.Equality ((:~:)(Refl)) -import Prelude hiding (compare) +import Data.Ord (Ord) +import Prelude hiding (Ord(..)) import Language.Symantic.Type import Language.Symantic.Repr @@ -29,22 +30,68 @@ import Language.Symantic.Trans.Common -- | Symantic. class Sym_Eq repr => Sym_Ord repr where compare :: Ord a => repr a -> repr a -> repr Ordering + (<) :: Ord a => repr a -> repr a -> repr Bool + (<=) :: Ord a => repr a -> repr a -> repr Bool + (>) :: Ord a => repr a -> repr a -> repr Bool + (>=) :: Ord a => repr a -> repr a -> repr Bool + max :: Ord a => repr a -> repr a -> repr a + min :: Ord a => repr a -> repr a -> repr a + default compare :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Ordering - compare = trans_map2 compare + default (<) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool + default (<=) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool + default (>) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool + default (>=) :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr Bool + default max :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr a + default min :: (Trans t repr, Ord a) => t repr a -> t repr a -> t repr a + + compare = trans_map2 compare + (<) = trans_map2 (<) + (<=) = trans_map2 (<=) + (>) = trans_map2 (>) + (>=) = trans_map2 (>=) + min = trans_map2 min + max = trans_map2 max + +infix 4 < +infix 4 <= +infix 4 > +infix 4 >= + instance Sym_Ord Repr_Host where compare = liftM2 Ord.compare + (<) = liftM2 (Ord.<) + (<=) = liftM2 (Ord.<=) + (>) = liftM2 (Ord.>) + (>=) = liftM2 (Ord.>=) + min = liftM2 Ord.min + max = liftM2 Ord.max instance Sym_Ord Repr_Text where - compare (Repr_Text x) (Repr_Text y) = - Repr_Text $ \p v -> - let p' = precedence_Eq in - paren p p' $ - "compare " <> x p' v <> " " <> y p' v + compare = repr_text_app2 "compare" + (<) = repr_text_infix "<" (Precedence 4) + (<=) = repr_text_infix "<=" (Precedence 4) + (>) = repr_text_infix ">" (Precedence 4) + (>=) = repr_text_infix ">=" (Precedence 4) + min = repr_text_app2 "min" + max = repr_text_app2 "max" instance ( Sym_Ord r1 , Sym_Ord r2 ) => Sym_Ord (Dup r1 r2) where compare (x1 `Dup` x2) (y1 `Dup` y2) = compare x1 y1 `Dup` compare x2 y2 + (<) (x1 `Dup` x2) (y1 `Dup` y2) = + (<) x1 y1 `Dup` (<) x2 y2 + (<=) (x1 `Dup` x2) (y1 `Dup` y2) = + (<=) x1 y1 `Dup` (<=) x2 y2 + (>) (x1 `Dup` x2) (y1 `Dup` y2) = + (>) x1 y1 `Dup` (>) x2 y2 + (>=) (x1 `Dup` x2) (y1 `Dup` y2) = + (>=) x1 y1 `Dup` (>=) x2 y2 + min (x1 `Dup` x2) (y1 `Dup` y2) = + min x1 y1 `Dup` min x2 y2 + max (x1 `Dup` x2) (y1 `Dup` y2) = + max x1 y1 `Dup` max x2 y2 -- * Type 'Expr_Ord' -- | Expression. @@ -75,3 +122,26 @@ compare_from ast_x ast_y ex ast ctx k = check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict -> k type_ordering $ Forall_Repr_with_Context $ \c -> x c `compare` y c + +ord_from + :: forall root ty ast hs ret. + ( ty ~ Type_Root_of_Expr (Expr_Ord root) + , Type0_Lift Type_Bool (Type_of_Expr root) + , Type0_Eq ty + , Expr_From ast root + , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast) + (Error_of_Expr ast root) + , Root_of_Expr root ~ root + , Type0_Constraint Ord ty + ) => (forall repr a. (Sym_Ord repr, Ord a) => repr a -> repr a -> repr Bool) + -> ast -> ast + -> ExprFrom ast (Expr_Ord root) hs ret +ord_from test ast_x ast_y ex ast ctx k = + expr_from (Proxy::Proxy root) ast_x ctx $ + \(ty_x::ty h_x) (Forall_Repr_with_Context x) -> + expr_from (Proxy::Proxy root) ast_y ctx $ + \(ty_y::ty h_y) (Forall_Repr_with_Context y) -> + check_type0_eq ex ast ty_x ty_y $ \Refl -> + check_type0_constraint ex (Proxy::Proxy Ord) ast ty_x $ \Dict -> + k type_bool $ Forall_Repr_with_Context $ + \c -> x c `test` y c diff --git a/Language/Symantic/Repr/Text.hs b/Language/Symantic/Repr/Text.hs index 18a5874..e98317a 100644 --- a/Language/Symantic/Repr/Text.hs +++ b/Language/Symantic/Repr/Text.hs @@ -70,6 +70,15 @@ repr_text_app3 name (Repr_Text a1) (Repr_Text a2) (Repr_Text a3) = <> " " <> a1 p' v <> " " <> a2 p' v <> " " <> a3 p' v +repr_text_infix + :: Text + -> Precedence + -> Repr_Text a1 + -> Repr_Text a2 + -> Repr_Text h +repr_text_infix name p' (Repr_Text a1) (Repr_Text a2) = + Repr_Text $ \p v -> + paren p p' $ a1 p' v <> " " <> name <> " " <> a2 p' v -- ** Type 'Precedence' @@ -87,39 +96,7 @@ paren prec prec' x = precedence_Toplevel :: Precedence precedence_Toplevel = Precedence 0 -precedence_Lambda :: Precedence -precedence_Lambda = Precedence 1 -precedence_Bind :: Precedence -precedence_Bind = precedence_Lambda -precedence_If :: Precedence -precedence_If = Precedence 2 -precedence_Let :: Precedence -precedence_Let = Precedence 3 -precedence_Eq :: Precedence -precedence_Eq = Precedence 4 -precedence_LtStarGt :: Precedence -precedence_LtStarGt = precedence_Eq -precedence_Or :: Precedence -precedence_Or = Precedence 5 -precedence_List_Cons :: Precedence -precedence_List_Cons = Precedence 5 -precedence_Xor :: Precedence -precedence_Xor = precedence_Or -precedence_And :: Precedence -precedence_And = Precedence 6 -precedence_Add :: Precedence -precedence_Add = precedence_And -precedence_Sub :: Precedence -precedence_Sub = precedence_Add -precedence_Mul :: Precedence -precedence_Mul = Precedence 7 -precedence_Integral :: Precedence -precedence_Integral = precedence_Mul precedence_App :: Precedence -precedence_App = Precedence 8 -precedence_Not :: Precedence -precedence_Not = Precedence 9 -precedence_Neg :: Precedence -precedence_Neg = precedence_Not +precedence_App = Precedence 10 precedence_Atomic :: Precedence precedence_Atomic = Precedence maxBound -- 2.47.2