Language/LOL/Symantic/Expr/Int.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE GADTs #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE Rank2Types #-}
   7 {-# LANGUAGE ScopedTypeVariables #-}
   8 {-# LANGUAGE TypeFamilies #-}
   9 {-# LANGUAGE UndecidableInstances #-}
  10 {-# OPTIONS_GHC -fno-warn-orphans #-}
  11 module Language.LOL.Symantic.Expr.Int where
  12
  13 import Data.Proxy (Proxy(..))
  14
  15 import Language.LOL.Symantic.AST
  16 import Language.LOL.Symantic.Type
  17 import Language.LOL.Symantic.Expr.Common
  18 import Language.LOL.Symantic.Expr.Lambda
  19 import Language.LOL.Symantic.Expr.Bool ()
  20 import Language.LOL.Symantic.Repr.Dup
  21
  22 -- * Class 'Sym_Int'
  23
  24 -- | Symantics acting on 'Int's.
  25 class Sym_Int repr where
  26         int :: Int -> repr Int
  27         neg :: repr Int -> repr Int
  28         add :: repr Int -> repr Int -> repr Int
  29
  30 instance -- Sym_Int Dup
  31  ( Sym_Int r1
  32  , Sym_Int r2
  33  ) => Sym_Int (Dup r1 r2) where
  34         int x = int x `Dup` int x
  35         neg (x1 `Dup` x2) = neg x1 `Dup` neg x2
  36         add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
  37
  38 -- * Type 'Expr_Int'
  39
  40 data Expr_Int (root:: *)
  41 type instance Root_of_Expr (Expr_Int root) = root
  42 type instance Type_of_Expr (Expr_Int root) = Type_Int
  43 type instance Sym_of_Expr (Expr_Int root) repr = Sym_Int repr
  44 type instance Error_of_Expr ast (Expr_Int root) = Error_Expr_Int ast
  45
  46 instance -- Sym_from AST Expr_Int
  47  ( Type_from AST (Type_Root_of_Expr root)
  48  , Sym_from AST root
  49
  50  , Type_Root_Lift Type_Int (Type_Root_of_Expr root)
  51  , Error_Type_Lift (Error_Type_Fun AST)
  52                    (Error_of_Type AST (Type_Root_of_Expr root))
  53  , Error_Expr_Lift (Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root))
  54                                       (                   Type_Root_of_Expr root)
  55                                       AST)
  56                    (Error_of_Expr AST root)
  57  , Error_Expr_Lift (Error_Expr_Read AST)
  58                    (Error_of_Expr AST root)
  59
  60  , Expr_Unlift (Type_Int (Type_Root_of_Expr root))
  61                (          Type_Root_of_Expr root)
  62
  63  , Root_of_Expr root ~ root
  64  -- , Root_of_Type (Type_Root_of_Expr root) ~ Type_Root_of_Expr root
  65  ) => Sym_from AST (Expr_Int root) where
  66         sym_from _px_ex ctx ast k =
  67                 case ast of
  68                  AST "int" asts ->
  69                         case asts of
  70                          [AST ast_int []] ->
  71                                 case read_safe ast_int of
  72                                  Left err -> Left $ Just $ error_expr_lift
  73                                         (Error_Expr_Read err ast :: Error_Expr_Read AST)
  74                                  Right (i::Int) ->
  75                                         k type_int $ Forall_Repr_with_Context $
  76                                                 const $ int i
  77                          _ -> Left $ Just $ error_lambda_lift $
  78                                 Error_Expr_Fun_Wrong_number_of_arguments 3 ast
  79                  AST "neg" asts -> unary_from  asts neg
  80                  AST "add" asts -> binary_from asts add
  81                  _ -> Left Nothing
  82                 where
  83                 unary_from asts
  84                  (op::forall repr. Sym_Int repr
  85                     => repr Int -> repr Int) =
  86                         case asts of
  87                          [ast_x] ->
  88                                 sym_from (Proxy::Proxy root) ctx ast_x $
  89                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
  90                                         case expr_unlift ty_x of
  91                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
  92                                                 k ty_x $ Forall_Repr_with_Context (op . x)
  93                                          _ -> Left $ Just $ error_lambda_lift $
  94                                                 Error_Expr_Fun_Argument_mismatch
  95                                                  (Exists_Type type_int)
  96                                                  (Exists_Type ty_x) ast
  97                          _ -> Left $ Just $ error_lambda_lift $
  98                                 Error_Expr_Fun_Wrong_number_of_arguments 1 ast
  99                 binary_from asts
 100                  (op::forall repr. Sym_Int repr
 101                     => repr Int -> repr Int -> repr Int) =
 102                         case asts of
 103                          [ast_x, ast_y] ->
 104                                 sym_from (Proxy::Proxy root) ctx ast_x $
 105                                  \(ty_x::Type_Root_of_Expr root h_x) (Forall_Repr_with_Context x) ->
 106                                 sym_from (Proxy::Proxy root) ctx ast_y $
 107                                  \(ty_y::Type_Root_of_Expr root h_y) (Forall_Repr_with_Context y) ->
 108                                         case expr_unlift ty_x of
 109                                          Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_x) ->
 110                                                 case expr_unlift ty_y of
 111                                                  Just (Type_Int::Type_Int (Type_Root_of_Expr root) h_y) ->
 112                                                         k ty_x $ Forall_Repr_with_Context $
 113                                                          \c -> x c `op` y c
 114                                                  Nothing -> Left $ Just $ error_lambda_lift $
 115                                                         Error_Expr_Fun_Argument_mismatch
 116                                                          (Exists_Type type_int)
 117                                                          (Exists_Type ty_y) ast
 118                                          Nothing -> Left $ Just $ error_lambda_lift $
 119                                                 Error_Expr_Fun_Argument_mismatch
 120                                                  (Exists_Type type_int)
 121                                                  (Exists_Type ty_x) ast
 122                          _ -> Left $ Just $ error_lambda_lift $
 123                                 Error_Expr_Fun_Wrong_number_of_arguments 2 ast
 124                 error_lambda_lift
 125                  :: Error_Expr_Lambda (Error_of_Type AST (Type_Root_of_Expr root)) (Type_Root_of_Expr root) AST
 126                  -> Error_of_Expr AST root
 127                 error_lambda_lift = error_expr_lift
 128
 129 -- ** Type 'Expr_Lambda_Int'
 130 -- | Convenient alias.
 131 type Expr_Lambda_Int lam = Expr_Root (Expr_Cons (Expr_Lambda lam) Expr_Int)
 132
 133 expr_lambda_int_from
 134  :: forall lam ast.
 135  Sym_from ast (Expr_Lambda_Int lam)
 136  => Proxy lam
 137  -> ast
 138  -> Either (Maybe (Error_of_Expr ast (Expr_Lambda_Int lam)))
 139            (Exists_Type_and_Repr (Type_Root_of_Expr (Expr_Lambda_Int lam))
 140                                  (Forall_Repr (Expr_Lambda_Int lam)))
 141 expr_lambda_int_from _px_lam ast =
 142         sym_from
 143          (Proxy::Proxy (Expr_Lambda_Int lam))
 144          Context_Empty ast $ \ty (Forall_Repr_with_Context repr) ->
 145                 Right $ Exists_Type_and_Repr ty $
 146                         Forall_Repr $ repr Context_Empty
 147
 148 -- * Type 'Error_Expr_Int'
 149 data Error_Expr_Int ast
 150  =   Error_Expr_Int
 151  deriving (Eq, Show)
 152