extremely basic Rlp2Core

This commit is contained in:
crumbtoo
2024-04-07 14:17:41 -06:00
parent dd93b76b69
commit 2944025327
8 changed files with 106 additions and 20 deletions

View File

@@ -9,6 +9,7 @@ module Rlp.AltSyntax
, pattern IntT, pattern TypeT
, Core.Rec(..)
, TypedRlpExpr'
, AnnotatedRlpExpr, TypedRlpExpr
, TypeF(..)
@@ -27,6 +28,7 @@ module Rlp.AltSyntax
-- * Misc
, serialiseCofree
, fixCofree
)
where
--------------------------------------------------------------------------------
@@ -40,7 +42,7 @@ import GHC.Generics ( Generic, Generic1
import Data.Hashable
import Data.Hashable.Lifted
import GHC.Exts (IsString)
import Control.Lens hiding ((.=))
import Control.Lens hiding ((.=), (:<))
import Data.Functor.Extend
import Data.Functor.Foldable.TH
@@ -58,6 +60,7 @@ import Core.Syntax qualified as Core
type RlpExpr' = RlpExpr PsName
type RlpExprF' = RlpExprF PsName
type AnnotatedRlpExpr' = Cofree (RlpExprF PsName)
type TypedRlpExpr' = TypedRlpExpr PsName
type Type' = Type PsName
type AnnotatedRlpExpr b = Cofree (RlpExprF b)
@@ -313,3 +316,11 @@ serialiseCofree = cata \case
ann :<$ e -> object [ "ann" .= ann
, "val" .= toJSON1 e ]
--------------------------------------------------------------------------------
fixCofree :: (Functor f, Functor g)
=> Iso (Fix f) (Fix g) (Cofree f ()) (Cofree g b)
fixCofree = iso sa bt where
sa = foldFix (() :<)
bt (_ :< f) = Fix (bt <$> f)

View File

@@ -144,15 +144,6 @@ gather (InR (CaseEF (te,je) as)) = do
j = je <> foldOf (each . _2) as' <> eqs
pure (t,j)
-- gather (InR (CaseEF (te,je) [Alter (ConP' n bs) (ta,ja)])) = do
-- -- let tc' be the type of the saturated type constructor
-- tc' <- freshTv
-- bs <- for bs (\b -> (b ^. singular _VarP,) <$> freshTv)
-- let tbs = bs ^.. each . _2
-- tc = foldr (:->) tc' tbs
-- j = equal te tc' <> je <> assume n tc <> forBinds elim bs ja
-- pure (ta,j)
gatherAlter :: (Unique :> es)
=> Type'
-> Alter PsName (Type', Judgement)