cli/Hcompta/Expr/Bool.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 -- {-# LANGUAGE KindSignatures #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE NoImplicitPrelude #-}
   7 {-# LANGUAGE OverloadedStrings #-}
   8 {-# LANGUAGE Rank2Types #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# OPTIONS_GHC -fno-warn-tabs #-}
  11 {-# OPTIONS_GHC -fno-warn-orphans #-}
  12
  13 module Hcompta.Expr.Bool where
  14
  15 import Data.Bool
  16 -- import Data.Either (Either(..))
  17 -- import Data.Function (($), (.))
  18 -- import Data.Maybe (Maybe(..))
  19 -- import Data.Monoid ((<>))
  20 -- import Data.Proxy (Proxy(..))
  21 -- import Data.String (String)
  22 -- import Data.Type.Equality ((:~:)(Refl))
  23 -- import Text.Show (Show(..))
  24
  25 import Hcompta.Expr.Dup
  26 -- import Hcompta.Expr.Fun
  27 -- import Hcompta.Expr.Lit
  28
  29 -- * Class 'Expr_Bool'
  30
  31 -- | /Tagless-final symantics/ for usual logical boolean operators.
  32 class Expr_Bool repr where
  33         neg :: repr Bool -> repr Bool
  34         and :: repr Bool -> repr Bool -> repr Bool
  35         or  :: repr Bool -> repr Bool -> repr Bool
  36         xor :: repr Bool -> repr Bool -> repr Bool
  37         xor x y = (x `or` y) `and` neg (x `and` y)
  38
  39 instance -- Expr_Bool Dup
  40  ( Expr_Bool r1
  41  , Expr_Bool r2
  42  ) => Expr_Bool (Dup r1 r2) where
  43         neg (x1 `Dup` x2)               = neg x1    `Dup` neg x2
  44         and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
  45         or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
  46
  47 {-
  48 instance -- Expr_from Tree
  49  ( Expr_Bool repr
  50  , Type_from Tree next
  51  , Expr_from Tree repr next (Type_Lit Bool repr next)
  52  ) => Expr_from Tree repr   (Type_Lit Bool repr next)
  53                             (Type_Fun_Lit Bool repr next) where
  54         expr_from _pty pvar ctx (Raw "And" [raw_x, raw_y]) k =
  55                 expr_from pvar pvar ctx raw_x $ \ty_x (x::Repr_HO repr _ctx _h_x) ->
  56                 expr_from pvar pvar ctx raw_y $ \ty_y (y::Repr_HO repr _ctx _h_y) ->
  57                         case (ty_x, ty_y) of
  58                          (  Type_Fun_Next Type_Int
  59                           , Type_Fun_Next Type_Int ) ->
  60                                 k (Type_Fun_Next Type_Int) $ \c -> and (x c) (y c)
  61                          _ -> Left "Error: And: at least one operand is not an Int"
  62         expr_from _pty pvar ctx raw k =
  63                 expr_from (Proxy::Proxy next) pvar ctx raw k
  64 -}
  65
  66 {-
  67 -- * Type 'Type_Bool'
  68
  69 -- | GADT for boolean type:
  70 --
  71 -- * singleton (bijective mapping between Haskell type @h@ and the GADT's terms),
  72 -- * and extensible (through @next@).
  73 data Type_Bool (next:: * -> *) h where
  74         Type_Bool      :: Type_Bool next Bool
  75         Type_Bool_Next :: next h -> Type_Bool next h
  76 type Type_Fun_Lit_Bool repr next = Type_Fun repr (Type_Bool next)
  77 type Type_Fun_Lit_Bool_End repr  = Type_Fun_Lit_Bool repr Type_Bool_End
  78
  79 instance -- Type_Eq
  80  Type_Eq next =>
  81  Type_Eq (Type_Bool next) where
  82         type_eq Type_Bool
  83                 Type_Bool = Just Refl
  84         type_eq (Type_Bool_Next x)
  85                 (Type_Bool_Next y) = x `type_eq` y
  86         type_eq _ _ = Nothing
  87 instance -- Type_from Tree
  88  Type_from Tree next =>
  89  Type_from Tree (Type_Bool next) where
  90         type_from (Tree "Bool" []) k = k Type_Bool
  91         type_from raw k = type_from raw $ k . Type_Bool_Next
  92 instance -- From_Type String
  93  From_Type String next =>
  94  From_Type String (Type_Bool next) where
  95         from_type Type_Bool = "Bool"
  96         from_type (Type_Bool_Next t) = from_type t
  97 --instance -- Show
  98 -- From_Type String next =>
  99 -- Show (Type_Bool next h) where
 100 --      show = from_type
 101
 102 -- ** Type 'Type_Bool_End'
 103
 104 data Type_Bool_End h where
 105         Type_Bool_End :: Type_Bool_End ()
 106
 107 instance -- Type_Eq
 108  Type_Eq Type_Bool_End where
 109         type_eq Type_Bool_End
 110                 Type_Bool_End = Just Refl
 111 instance -- Type_from Tree
 112  Type_from Tree Type_Bool_End where
 113         type_from _ k = k Type_Bool_End
 114 instance -- Expr_from Tree
 115  Show raw =>
 116  Expr_from raw repr Type_Bool_End (Type_Fun_Lit_Bool repr Type_Bool_End) where
 117         expr_from _pty _pvar _ctx raw _k =
 118                 Left $ "Error: invalid: " <> show raw
 119
 120
 121 fun_lit_bool_from
 122  :: forall next raw repr ret.
 123  ( Expr_from raw repr (Type_Fun_Lit_Bool repr next) (Type_Fun_Lit_Bool repr next)
 124  -- , Expr_from raw repr next (Type_Fun_Lit_Bool repr next)
 125  , Expr_Fun repr
 126  , Expr_Lit repr
 127  , Type_from raw next
 128  )
 129  => Proxy next
 130  -> raw
 131  -> (forall h. Type_Fun_Lit_Bool repr next h -> repr h -> Either Error_Type ret)
 132  -> Either Error_Type ret
 133 fun_lit_bool_from _pty raw k =
 134         expr_from
 135          (Proxy::Proxy (Type_Fun_Lit_Bool repr next))
 136          (Proxy::Proxy (Type_Fun_Lit_Bool repr next))
 137          Context_Type_Empty raw $ \ty repr ->
 138                 k ty $ repr Context_Type_Empty
 139 -}