systemqfw

system Q F omega elaborator
git clone git://git.rr3.xyz/systemqfw
Log | Files | Refs | Submodules | README | LICENSE

Value.hs (5488B)

      1 module Value where
      2 import Data.Maybe (fromMaybe)
      3 
      4 import Algebra
      5 import Common
      6 import Environment (Value (..), Env)
      7 import qualified Environment as Env
      8 import qualified Core as C
      9 
     10 --------------------------------------------------------------------------------
     11 -- Types
     12 
     13 newtype TypeLvl = TypeLvl Int deriving (Eq, Show, IsInt)
     14 
     15 type TypeEnv q = Env C.TypeIdx (Type q)
     16 
     17 data TypeClosure q = TypeClosure (TypeEnv q) (C.Type q)
     18 
     19 data Type q
     20     = TypeGeneric TypeLvl
     21 
     22     | TypeTArrow (Type q) (Type q)
     23     | TypeTForall Kind (TypeClosure q)
     24 
     25     | TypeQ q
     26     | TypeQAdd (Type q) (Type q)
     27     | TypeQMul (Type q) (Type q)
     28 
     29     | TypeQTPair (Type q) (Type q)
     30     | TypeQTFst (Type q)
     31     | TypeQTSnd (Type q)
     32 
     33     | TypeArrowAbs (TypeClosure q)
     34     | TypeArrowApp (Type q) (Type q)
     35 
     36 instance AddMonoid q => AddMonoid (Type q) where
     37     zero = TypeQ zero
     38 
     39     x <+> y = case (x, y) of
     40         (TypeQ q, TypeQ r) -> TypeQ (q <+> r)
     41         (x, y) -> TypeQAdd x y
     42 
     43 instance MulScalar q => MulScalar (Type q) where
     44     one = TypeQ one
     45 
     46 instance (MulAction q, MulActionScalar q ~ q) => MulAction (Type q) where
     47     type MulActionScalar (Type q) = Type q
     48 
     49     x <⋅> y = case (x, y) of
     50         (TypeQ q, TypeQ r) -> TypeQ (q <⋅> r)
     51         (x, y) -> TypeQMul x y
     52 
     53 instance Value (Type q) where
     54     type Level (Type q) = TypeLvl
     55     generic = TypeGeneric
     56 
     57 qGeq :: QuantityAlgebra q => Type q -> Type q -> Bool
     58 x `qGeq` y = case (x, y) of
     59     (TypeQ q, TypeQ r) -> q ?>= r
     60     _ -> False
     61 
     62 qtFst :: QuantityAlgebra q => Type q -> Type q
     63 qtFst = \case
     64     TypeQTPair q _ -> q
     65     x -> TypeQTFst x
     66 
     67 qtSnd :: QuantityAlgebra q => Type q -> Type q
     68 qtSnd = \case
     69     TypeQTPair _ a -> a
     70     x -> TypeQTSnd x
     71 
     72 applyClosure :: QuantityAlgebra q => TypeClosure q -> Type q -> Type q
     73 applyClosure (TypeClosure env abs) arg =
     74     let (_, env') = Env.bindAndDefine arg env
     75     in evalType env' abs
     76 
     77 evalType :: QuantityAlgebra q => TypeEnv q -> C.Type q -> Type q
     78 evalType env a =
     79     let eval = evalType env in
     80     case a of
     81         C.TypeVar idx ->
     82             let lvl = Env.idxToLvl idx env in
     83             fromMaybe (TypeGeneric lvl) (Env.subst lvl env)
     84         C.TypeTArrow dom cod -> TypeTArrow (eval dom) (eval cod)
     85         C.TypeTForall k body -> TypeTForall k (TypeClosure env body)
     86         C.TypeQ q -> TypeQ q
     87         C.TypeQAdd q r -> (eval q) <+> (eval r)
     88         C.TypeQMul q r -> (eval q) <⋅> (eval r)
     89         C.TypeQTPair q a -> TypeQTPair (eval q) (eval a)
     90         C.TypeQTFst qa -> qtFst (eval qa)
     91         C.TypeQTSnd qa -> qtSnd (eval qa)
     92         C.TypeArrowAbs body -> TypeArrowAbs (TypeClosure env body)
     93         C.TypeArrowApp fun arg ->
     94             let varg = eval arg in
     95             case eval fun of
     96                 TypeArrowAbs body -> applyClosure body varg
     97                 vfun -> TypeArrowApp vfun varg
     98 
     99 quoteType :: QuantityAlgebra q => TypeEnv q -> Type q -> C.Type q
    100 quoteType env a =
    101     let quote = quoteType env in
    102     case a of
    103         TypeGeneric lvl -> C.TypeVar $ Env.lvlToIdx lvl env
    104         TypeTArrow dom cod -> C.TypeTArrow (quote dom) (quote cod)
    105         TypeTForall k body -> C.TypeTForall k $ quoteTypeClosure env body
    106         TypeQ q -> C.TypeQ q
    107         TypeQAdd q r -> C.TypeQAdd (quote q) (quote r)
    108         TypeQMul q r -> C.TypeQMul (quote q) (quote r)
    109         TypeQTPair q a -> C.TypeQTPair (quote q) (quote a)
    110         TypeQTFst qa -> C.TypeQTFst (quote qa)
    111         TypeQTSnd qa -> C.TypeQTFst (quote qa)
    112         TypeArrowAbs body -> C.TypeArrowAbs $ quoteTypeClosure env body
    113         TypeArrowApp fun arg -> C.TypeArrowApp (quote fun) (quote arg)
    114 
    115 quoteTypeClosure :: QuantityAlgebra q => TypeEnv q -> TypeClosure q -> C.Type q
    116 quoteTypeClosure env clo =
    117     let (lvl, env') = Env.bind env in
    118     quoteType env' $ applyClosure clo (TypeGeneric lvl)
    119 
    120 convType :: QuantityAlgebra q => TypeEnv q -> Type q -> Type q -> Bool
    121 convType env x y =
    122     let conv = convType env in
    123     case (x, y) of
    124         (TypeGeneric xlvl, TypeGeneric ylvl) -> xlvl == ylvl
    125         (TypeTArrow xdom xcod, TypeTArrow ydom ycod) -> conv xdom ydom && conv xcod ycod
    126         (TypeTForall xk xclo, TypeTForall yk yclo) -> xk == yk && convTypeClosure env xclo yclo
    127         (TypeQ q, TypeQ r) -> q == r
    128         (TypeQAdd xq xr, TypeQAdd yq yr) -> conv xq yq && conv xr yr
    129         (TypeQMul xq xr, TypeQMul yq yr) -> conv xq yq && conv xr yr
    130         (TypeQTPair q a, TypeQTPair r b) -> conv q r && conv a b
    131         (TypeQTFst qa, TypeQTFst rb) -> conv qa rb
    132         (TypeQTSnd qa, TypeQTSnd rb) -> conv qa rb
    133         (TypeArrowAbs xclo, TypeArrowAbs yclo) -> convTypeClosure env xclo yclo
    134         (TypeArrowApp xfun xarg, TypeArrowApp yfun yarg) -> conv xfun yfun && conv xarg yarg
    135         (_, _) -> False
    136 
    137 convTypeClosure :: QuantityAlgebra q => TypeEnv q -> TypeClosure q -> TypeClosure q -> Bool
    138 convTypeClosure env xclo yclo =
    139     let (lvl, env') = Env.bind env
    140         arg = TypeGeneric lvl
    141     in convType env' (applyClosure xclo arg) (applyClosure yclo arg)
    142 
    143 --------------------------------------------------------------------------------
    144 -- Terms
    145 
    146 newtype TermLvl = TermLvl Int deriving (Eq, Show, IsInt)
    147 
    148 type TermEnv q = Env C.TermIdx (Term q)
    149 
    150 data TermClosure q = TermClosure (TypeEnv q) (C.Term q)
    151 
    152 data Term q
    153    = TermGeneric TermLvl
    154  
    155    | TermArrowAbs (TermClosure q)
    156    | TermArrowApp (Term q) (Term q)
    157 
    158    | TermForallAbs (TermClosure q)
    159    | TermForallApp (Term q) (Type q)
    160 
    161 instance Value (Term q) where
    162     type Level (Term q) = TermLvl
    163     generic = TermGeneric