module DDC.Core.Tetra.Prim.OpFun
( OpFun (..)
, readOpFun
, typeOpFun)
where
import DDC.Core.Tetra.Prim.TyConTetra
import DDC.Core.Tetra.Prim.Base
import DDC.Type.Compounds
import DDC.Type.Exp
import DDC.Base.Pretty
import Control.DeepSeq
import Data.Char
import Data.List
instance NFData OpFun where
rnf op
= case op of
OpFunCurry n -> rnf n
OpFunApply n -> rnf n
OpFunCReify -> ()
OpFunCCurry n -> rnf n
OpFunCExtend n -> rnf n
OpFunCApply n -> rnf n
instance Pretty OpFun where
ppr pf
= case pf of
OpFunCurry n
-> text "curry" <> int n <> text "#"
OpFunApply n
-> text "apply" <> int n <> text "#"
OpFunCReify
-> text "creify#"
OpFunCCurry n
-> text "ccurry" <> int n <> text "#"
OpFunCExtend n
-> text "cextend" <> int n <> text "#"
OpFunCApply n
-> text "capply" <> int n <> text "#"
readOpFun :: String -> Maybe OpFun
readOpFun str
| Just rest <- stripPrefix "curry" str
, (ds, "#") <- span isDigit rest
, not $ null ds
, n <- read ds
, n >= 0
= Just $ OpFunCurry n
| Just rest <- stripPrefix "apply" str
, (ds, "#") <- span isDigit rest
, not $ null ds
, n <- read ds
, n >= 1
= Just $ OpFunApply n
| "creify#" <- str
= Just $ OpFunCReify
| Just rest <- stripPrefix "ccurry" str
, (ds, "#") <- span isDigit rest
, not $ null ds
, n <- read ds
, n >= 0
= Just $ OpFunCCurry n
| Just rest <- stripPrefix "cextend" str
, (ds, "#") <- span isDigit rest
, not $ null ds
, n <- read ds
, n >= 1
= Just $ OpFunCExtend n
| Just rest <- stripPrefix "capply" str
, (ds, "#") <- span isDigit rest
, not $ null ds
, n <- read ds
, n >= 0
= Just $ OpFunCApply n
| otherwise
= Nothing
typeOpFun :: OpFun -> Type Name
typeOpFun op
= case op of
OpFunCurry n
-> tForalls (replicate (n + 1) kData)
$ \ts ->
let tLast : tsFront' = reverse ts
tsFront = reverse tsFront'
Just tF = tFunOfList ts
Just result
= tFunOfList
( tFunValue tF
: tsFront ++ [tLast])
in result
OpFunApply n
-> tForalls (replicate (n + 1) kData)
$ \ts ->
let Just tF = tFunOfList ts
Just result = tFunOfList (tF : ts)
in result
OpFunCReify
-> tForalls [kData, kData]
$ \[tA, tB] -> (tA `tFun` tB) `tFun` tFunValue (tA `tFun` tB)
OpFunCCurry n
-> tForalls (replicate (n + 1) kData)
$ \ts ->
let tLast : tsFront' = reverse ts
tsFront = reverse tsFront'
Just tF = tFunOfList ts
Just result
= tFunOfList
( tFunValue tF
: tsFront ++ [tCloValue tLast])
in result
OpFunCExtend n
-> tForalls (replicate (n + 1) kData)
$ \ts ->
let tLast : tsFront' = reverse ts
tsFront = reverse tsFront'
Just tF = tFunOfList ts
Just result
= tFunOfList
( tCloValue tF
: tsFront ++ [tCloValue tLast])
in result
OpFunCApply n
-> tForalls (replicate (n + 1) kData)
$ \ts ->
let tLast : tsFront' = reverse ts
tsFront = reverse tsFront'
Just tF = tFunOfList ts
Just result
= tFunOfList
( tCloValue tF
: tsFront ++ [tLast])
in result