src/Symantic/Semantics/LetInserter.hs

   1 {-# LANGUAGE DerivingStrategies #-}
   2 {-# LANGUAGE GADTs #-}
   3 {-# LANGUAGE QuantifiedConstraints #-}
   4 -- For Syn.LetRecable
   5 {-# LANGUAGE UndecidableInstances #-}
   6
   7 module Symantic.Semantics.LetInserter where
   8
   9 import Control.Applicative (liftA2, liftA3)
  10 import Control.Monad (Monad (..))
  11 import Control.Monad.Trans.State.Strict qualified as MT
  12 import Data.Bool (Bool (..), not, otherwise, (&&))
  13 import Data.Either (Either (..))
  14 import Data.Eq (Eq (..))
  15 import Data.Foldable (foldMap)
  16 import Data.Function (const, id, on, ($), (.))
  17 import Data.Functor ((<$>))
  18 import Data.Int (Int)
  19 import Data.Kind (Type)
  20 import Data.List qualified as List
  21 import Data.Maybe (Maybe (..), isNothing, maybe)
  22 import Data.Ord (Ord (..))
  23 import Data.Semigroup (Semigroup (..))
  24 import Data.Set qualified as Set
  25 import Debug.Trace qualified as Trace
  26 import Numeric.Natural (Natural)
  27 import Symantic.Syntaxes.Classes qualified as Syn
  28 import Symantic.Syntaxes.Derive qualified as Syn
  29 import Text.Show (Show (..), showListWith, showString, shows)
  30 import Unsafe.Coerce (unsafeCoerce)
  31 import Prelude (error, pred)
  32 import Prelude qualified
  33
  34 -- import Control.Monad.Trans.Class qualified as MT
  35 -- import Data.Functor.Identity (Identity(..))
  36 -- import Data.Monoid (Monoid(..))
  37 -- import Data.String (String)
  38
  39 traceShow :: Show a => a -> b -> b
  40 -- traceShow = Trace.traceShow
  41 traceShow _x a = a
  42
  43 newtype Locus = Locus Natural
  44   deriving (Eq, Ord)
  45   deriving newtype (Show)
  46
  47 {-
  48 type Locus = [Pigit]
  49 data Pigit = POne | PTwo | PThree | PLoc Locus | PNote String
  50   deriving (Eq, Ord)
  51 instance Show Pigit where
  52   showsPrec _p x =
  53     case x of
  54       POne -> shows (1::Int)
  55       PTwo -> shows (2::Int)
  56       PThree -> shows (3::Int)
  57       PLoc loc -> shows loc
  58       PNote msg -> showString msg
  59 -}
  60
  61 -- * Type 'OpenCode'
  62 newtype OpenCode code a = OpenCode {unOpenCode :: Env code -> code a}
  63 type instance Syn.Derived (OpenCode code) = code
  64
  65 -- instance Syn.Derivable (OpenCode code) where
  66 --  derive oc = unOpenCode oc mempty
  67 instance Syn.LiftDerived (OpenCode code) where
  68   liftDerived x = OpenCode (const x)
  69 instance Syn.LiftDerived1 (OpenCode code) where
  70   liftDerived1 f x = OpenCode (\env -> f (unOpenCode x env))
  71 instance Syn.LiftDerived2 (OpenCode code) where
  72   liftDerived2 f x y = OpenCode (\env -> f (unOpenCode x env) (unOpenCode y env))
  73 instance Syn.LiftDerived3 (OpenCode code) where
  74   liftDerived3 f x y z = OpenCode (\env -> f (unOpenCode x env) (unOpenCode y env) (unOpenCode z env))
  75
  76 -- instance Syn.Abstractable code => Syn.Abstractable (OpenCode code) where
  77 --  lam f = OpenCode (\env -> Syn.lam (\x -> unOpenCode f env (unOpenCode x env)))
  78 -- instance Syn.Instantiable code => Syn.Instantiable (OpenCode code)
  79 -- instance Syn.Constantable c code => Syn.Constantable c (OpenCode code)
  80 instance Syn.IfThenElseable code => Syn.IfThenElseable (OpenCode code) where
  81   ifThenElse x y z = OpenCode (\env -> Syn.ifThenElse (unOpenCode x env) (unOpenCode y env) (unOpenCode z env))
  82 instance Syn.Equalable code => Syn.Equalable (OpenCode code) where
  83   equal = OpenCode (const Syn.equal)
  84 instance Syn.Constantable c code => Syn.Constantable c (OpenCode code)
  85
  86 -- ** Type Env'
  87 type Env code = [EnvBind code]
  88
  89 -- *** Type 'Var'
  90 newtype Var a = Var {unVar :: VarName}
  91   deriving (Eq)
  92   deriving newtype (Show)
  93 type VarName = Locus
  94
  95 -- *** Type 'EnvBind'
  96 data EnvBind code where
  97   EnvBind :: !(Var a, code a) -> EnvBind code
  98 instance Show (EnvBind code) where
  99   showsPrec p (EnvBind (n, _e)) = showsPrec p n
 100
 101 lookupVar :: Var a -> OpenCode code a
 102 lookupVar (Var v) =
 103   traceShow (["lookupVar", "OpenCode"], v) $
 104     OpenCode $ \env ->
 105       traceShow (["lookupVar", "OpenCode", "find"], v, ("env", env)) $
 106         case List.find (\(EnvBind (Var v1, _)) -> v1 == v) env of
 107           Just (EnvBind (_, x)) -> unsafeCoerce x
 108           Nothing -> error ("lookupVar failure for var=(" <> show v <> ")  env=" <> show ((\(EnvBind (Var n, _v)) -> n) <$> env))
 109
 110 lookupVarLetInserter :: Var a -> LetInserter code a
 111 lookupVarLetInserter v =
 112   LetInserter $
 113     return
 114       AnnotatedCode
 115         { annotatedCodeOpenCode = lookupVar v
 116         , annotatedCodeFloatingLets = FloatingLets []
 117         , annotatedCodeFreeVars = Set.singleton (unVar v)
 118         }
 119
 120 insertVar :: Var a -> code a -> Env code -> Env code
 121 insertVar v e env =
 122   traceShow ("insertVar", v) $
 123     EnvBind (v, e) : env
 124
 125 -- * Type 'Memo'
 126 type Memo = Natural
 127
 128 -- ** Type 'MaybeMemo'
 129
 130 -- | Like a @(Maybe Memo)@ except 'Nothing' is never equal to any other value
 131 -- to implement unique memoization key.
 132 newtype MaybeMemo = MaybeMemo (Maybe Memo)
 133   deriving (Show)
 134
 135 instance Eq MaybeMemo where
 136   MaybeMemo (Just x) == MaybeMemo (Just y) = x == y
 137   _ == _ = False
 138
 139 -- * Type 'FloatingLet'
 140 data FloatingLet code where
 141   FloatingLet ::
 142     { floatingLetLocus :: !(Maybe Locus)
 143     -- ^ 'FloatingLet' are either inserted at the place of an explicit 'Locus',
 144     -- or at the binding ('lam' or 'let_') that dominates all free variables of the bound expression,
 145     -- whichever has the narrowest scope.
 146     , floatingLetMemo :: !MaybeMemo
 147     -- ^ Memoization key, either internal (unique) or user-specified.
 148     --
 149     -- The memo key defines the equivalence classes:
 150     -- expressions with the same memo key are to be shared.
 151     -- Therefore, if @('genLetMemo' k l e)@ finds that there is already a let-binding
 152     -- produced by an earlier 'genLetMemo' with the same locus @(l)@ and the same memo key @(k)@,
 153     -- @('genLetMemo' k l e) returns the code of the earlier bound variable.
 154     , floatingLetVarName :: !(Var a)
 155     , floatingLetBoundCode :: !(BoundCode code a)
 156     , floatingLetFreeVars :: !(Set.Set VarName)
 157     } ->
 158     FloatingLet code
 159 instance Show (FloatingLet code) where
 160   showsPrec _p FloatingLet{..} =
 161     showString "FloatingLet{"
 162       . showString "locus="
 163       . shows floatingLetLocus
 164       . showString ", "
 165       . showString "memo="
 166       . shows floatingLetMemo
 167       . showString ", "
 168       . showString "var="
 169       . shows floatingLetVarName
 170       . showString ", "
 171       . showString "exp="
 172       . showString (case floatingLetBoundCode of BoundCodeOpenCode{} -> "BoundCodeOpenCode"; BoundCodeLetInserter{} -> "BoundCodeLetInserter")
 173       . showString ", "
 174       . showString "fvs="
 175       . showListWith (shows) (Set.toList floatingLetFreeVars)
 176       . showString ", "
 177       . showString "}"
 178
 179 -- * Type 'VLBindings'
 180
 181 -- A virtual let-binding.
 182 -- The key idea is virtual let-bindings: whereas clet introduces an ordinary let-binding
 183 -- whose location is fixed, glet generates the code for a fresh variable accompanied by a virtual
 184 -- binding of that variable. Virtual bindings do not have (yet) a fixed location: they are
 185 -- attached to the expression that uses their bound variables and ‘float up’ when their attached
 186 -- expression is incorporated into a bigger expression. Eventually, when they reach a point that
 187 -- a metaprogrammer has marked with a dedicated primitive, virtual bindings are converted to
 188 -- real let-bindings.
 189 newtype FloatingLets code = FloatingLets {unFloatingLets :: [FloatingLet code]}
 190 instance Show (FloatingLets code) where
 191   showsPrec _p (FloatingLets l) = go l
 192     where
 193       go [] = showString "\n"
 194       go (e : es) = showString "\n  , " . shows e . go es
 195
 196 -- | Append two lists skipping the duplicates.
 197 -- The order of elements is preserved
 198 mergeFloatingLets :: FloatingLets code -> FloatingLets code -> FloatingLets code
 199 mergeFloatingLets (FloatingLets xs) (FloatingLets ys) =
 200   traceShow (["mergeFloatingLets"], xs, ys) $
 201     FloatingLets (loop (List.reverse xs) ys)
 202   where
 203     loop acc = \case
 204       [] -> List.reverse acc
 205       y@FloatingLet{floatingLetVarName = Var yv} : t ->
 206         case List.filter
 207           ( \a@FloatingLet{floatingLetVarName = Var av} ->
 208               floatingLetLocus y == floatingLetLocus a
 209                 && floatingLetMemo y == floatingLetMemo a
 210                 && yv == av
 211           )
 212           acc of
 213           [] -> loop (y : acc) t
 214           _ -> loop (acc) t
 215
 216 -- fs ->
 217 --  loop (List.concatMap (\FloatingLet{floatingLetBoundCode, floatingLetLocus, floatingLetMemo, floatingLetVarName=Var av} ->
 218 --    if av == yv
 219 --    then
 220 --    FloatingLet { floatingLetVarName=Var yv, .. }) fs <> acc) t
 221 instance Semigroup (FloatingLets code) where
 222   (<>) = mergeFloatingLets
 223
 224 -- instance Monoid (FloatingLets code) where
 225 --  mempty = FloatingLets []
 226 --  mappend = (<>)
 227
 228 -- * Type 'BoundCode'
 229
 230 -- | Bound expression
 231 data BoundCode (code :: Type -> Type) a
 232   = BoundCodeOpenCode !(OpenCode code a)
 233   | -- | In the recursive case,
 234     -- a virtual binding may carry a yet to be computed piece of code.
 235     BoundCodeLetInserter !(LetInserter code a)
 236
 237 -- * Type 'AnnotatedCode'
 238
 239 -- | A code value.
 240 -- A code value is annotated only with the type of the expression it generates,
 241 -- with no further classifiers (at present).
 242 data AnnotatedCode (code :: Type -> Type) a = AnnotatedCode
 243   { annotatedCodeOpenCode :: !(OpenCode code a)
 244   , annotatedCodeFloatingLets :: !(FloatingLets code)
 245   , annotatedCodeFreeVars :: !(Set.Set VarName)
 246   -- ^ The free variables of the code,
 247   -- used to limit the floating up of locus-less 'FloatingLet's
 248   -- at 'lam' or 'let_' level, in order to avoid scope extrusion.
 249   }
 250
 251 -- annotatedCodeFreeVars :: AnnotatedCode code a -> Set.Set VarName
 252 -- annotatedCodeFreeVars annotatedCode = foldMap floatingLetFreeVars (unFloatingLets (annotatedCodeFloatingLets annotatedCode))
 253
 254 runCD :: Syn.Letable code => AnnotatedCode code a -> code a
 255 runCD AnnotatedCode{annotatedCodeOpenCode = oc, annotatedCodeFloatingLets = FloatingLets bindingFLS} =
 256   let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
 257   in (`unOpenCode` []) $ List.foldr bindFloatingLetMemo oc bindingLFSByMemo
 258 runCD _ = error "runCD: virtual binding extrusion"
 259
 260 type instance Syn.Derived (AnnotatedCode code) = OpenCode code
 261 instance Syn.LiftDerived (AnnotatedCode code) where
 262   liftDerived x = AnnotatedCode{annotatedCodeOpenCode = x, annotatedCodeFloatingLets = FloatingLets [], annotatedCodeFreeVars = Set.empty}
 263 instance Syn.LiftDerived1 (AnnotatedCode code) where
 264   liftDerived1 f e1 =
 265     AnnotatedCode
 266       { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1)
 267       , annotatedCodeFloatingLets = annotatedCodeFloatingLets e1
 268       , annotatedCodeFreeVars = annotatedCodeFreeVars e1
 269       }
 270 instance Syn.LiftDerived2 (AnnotatedCode code) where
 271   liftDerived2 f e1 e2 =
 272     AnnotatedCode
 273       { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1) (annotatedCodeOpenCode e2)
 274       , annotatedCodeFloatingLets = mergeFloatingLets (annotatedCodeFloatingLets e1) (annotatedCodeFloatingLets e2)
 275       , annotatedCodeFreeVars = annotatedCodeFreeVars e1 <> annotatedCodeFreeVars e2
 276       }
 277 instance Syn.LiftDerived3 (AnnotatedCode code) where
 278   liftDerived3 f e1 e2 e3 =
 279     AnnotatedCode
 280       { annotatedCodeOpenCode = f (annotatedCodeOpenCode e1) (annotatedCodeOpenCode e2) (annotatedCodeOpenCode e3)
 281       , annotatedCodeFloatingLets = mergeFloatingLets (annotatedCodeFloatingLets e1) (mergeFloatingLets (annotatedCodeFloatingLets e2) (annotatedCodeFloatingLets e3))
 282       , annotatedCodeFreeVars = annotatedCodeFreeVars e1 <> annotatedCodeFreeVars e2 <> annotatedCodeFreeVars e3
 283       }
 284 instance Syn.Constantable c code => Syn.Constantable c (AnnotatedCode code)
 285 instance Syn.Instantiable code => Syn.Instantiable (AnnotatedCode code)
 286 instance Syn.IfThenElseable code => Syn.IfThenElseable (AnnotatedCode code)
 287 instance Syn.Equalable code => Syn.Equalable (AnnotatedCode code)
 288
 289 -- * Type 'LetInserter'
 290 newtype LetInserter code a = LetInserter {unR :: MT.State Natural (AnnotatedCode code a)}
 291 runLetInserter :: Syn.Letable code => LetInserter code a -> code a
 292 runLetInserter = runCD . (`MT.evalState` 0) . unR
 293
 294 type instance Syn.Derived (LetInserter code) = AnnotatedCode code
 295 instance Syn.LiftDerived (LetInserter sem) where
 296   liftDerived = LetInserter . return
 297 instance Syn.LiftDerived1 (LetInserter sem) where
 298   liftDerived1 f e1 = LetInserter (f <$> unR e1)
 299 instance Syn.LiftDerived2 (LetInserter sem) where
 300   liftDerived2 f e1 e2 = LetInserter (liftA2 f (unR e1) (unR e2))
 301 instance Syn.LiftDerived3 (LetInserter sem) where
 302   liftDerived3 f e1 e2 e3 = LetInserter (liftA3 f (unR e1) (unR e2) (unR e3))
 303 instance Syn.IfThenElseable code => Syn.IfThenElseable (LetInserter code)
 304 instance Syn.Equalable code => Syn.Equalable (LetInserter code)
 305 instance Syn.Constantable c code => Syn.Constantable c (LetInserter code)
 306 instance Syn.Instantiable code => Syn.Instantiable (OpenCode code)
 307
 308 freshNatural :: MT.State Natural Natural
 309 freshNatural = do
 310   n <- MT.get
 311   MT.put (Prelude.succ n)
 312   return n
 313
 314 -- type instance Syn.Derived (LetInserter sem) = Syn.Derived sem
 315 freshVar :: MT.State Natural (Var a)
 316 freshVar = Var . Locus <$> freshNatural
 317
 318 -- instance Syn.Constantable c sem => Syn.Constantable c (LetInserter sem) where
 319 --   constant c = LetInserter $ pure $ Syn.constant c
 320 instance Syn.Instantiable sem => Syn.Instantiable (LetInserter sem)
 321
 322 -- f .@ x = LetInserter $ Syn.liftDerived2 (Syn..@) (unR f) (unR x)
 323 -- instance Syn.Abstractable sem => Syn.Abstractable (LetInserter sem) where
 324 --   lam f = LetInserter $ \loc ->
 325 --       Syn.lam $ \x ->
 326 --       unR (f (LetInserter (\_loc -> x)))
 327 --         (PNote "lam":loc)
 328 -- instance Syn.Abstractable code => Syn.Abstractable (LetInserter (AnnotatedCode code)) where
 329 --   lam body = LetInserter $ \loc ->
 330 --     AnnotatedCode
 331 --       { annotatedCodeOpenCode = _e
 332 --       }
 333 --     -- \x -> unR (body (LetInserter (\_ -> x))) (PNote "lam":loc)
 334 -- instance Syn.Letable (LetInserter sem) where
 335 --   let_ exp body = LetInserter $ \loc ->
 336 --     let x = unR exp (POne:loc) in
 337 --     unR (body (LetInserter (\_loc -> x))) (PTwo:loc)
 338
 339 -- instance Syn.Letable code => Syn.Letable (LetInserter code) where
 340 --  let_ e body = LetInserter $ \loc ->
 341 --    let x = unR e (POne:loc) in
 342 --    unR (body (LetInserter (\_loc -> x))) (PTwo:loc)
 343
 344 -- instance Syn.Letable (LetInserter sem) where
 345 --  let_ exp body = LetInserter (\loc -> let x = unR exp (POne:loc) in unR (body (LetInserter (\_loc -> x))) (PTwo:loc))
 346 -- instance Syn.IfThenElseable code => Syn.IfThenElseable (LetInserter (AnnotatedCode code)) where
 347 --  ifThenElse =
 348 --    Syn.liftDerived3 $ \bC okC koC -> OpenCode $ \env ->
 349 --      Syn.ifThenElse (unOpenCode bC env) (unOpenCode okC env) (unOpenCode koC env)
 350 -- instance Syn.FromDerived Syn.Equalable sem => Syn.Equalable (LetInserter sem) where
 351 --   equal = LetInserter (\loc -> trace ("equal "<>show loc) $ Syn.equal)
 352
 353 -- | Check to see there are no duplicate 'VarName's in 'VLBindings'.
 354 -- This is just a safety check
 355 check_no_dup_varname :: FloatingLets code -> a -> a
 356 check_no_dup_varname = loop []
 357   where
 358     loop :: [VarName] -> FloatingLets code -> a -> a
 359     loop _found (FloatingLets []) = id
 360     loop found (FloatingLets (FloatingLet{floatingLetVarName = Var v, ..} : t))
 361       | v `List.elem` found =
 362           error ("Duplicate varname " <> show v <> ", with locus " <> show floatingLetLocus)
 363       | otherwise = loop (v : found) (FloatingLets t)
 364
 365 -- | let-bind all vlbindings with the given locus.
 366 -- This is a non-recursive case. All these let-bindings are independent
 367 -- It is up to the user to ensure the independence: if the bindings
 368 -- are dependent, the user should have introduced several loci
 369 -- Virtual let bindings are sort of free variables.
 370 -- We bind free variables later. Likewise, we bind let-bindings later.
 371 -- 'Memo' is ignored here.
 372 -- class GenLetable sem where
 373 -- instance Syn.Letable code => GenLetable (LetInserter (AnnotatedCode code)) where
 374 floatingLetVarname :: FloatingLet code -> VarName
 375 floatingLetVarname FloatingLet{floatingLetVarName = Var v} = v
 376
 377 instance
 378   ( Syn.Abstractable code
 379   , Syn.Letable code
 380   , Syn.LetRecable Int code
 381   ) =>
 382   Syn.Abstractable (LetInserter code)
 383   where
 384   lam body = LetInserter $ do
 385     vname <- freshVar
 386     unR $
 387       Syn.liftDerived1
 388         ( \bodyCD ->
 389             let (bindingFLS, passingFLS) =
 390                   List.partition
 391                     (\fl -> Set.member (unVar vname) (floatingLetFreeVars fl))
 392                     (unFloatingLets (annotatedCodeFloatingLets bodyCD))
 393             in let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
 394                in traceShow
 395                     ( "lam"
 396                     , ("vname", unVar vname)
 397                     , ("bindingFLS", FloatingLets bindingFLS)
 398                     , ("passingFLS", FloatingLets passingFLS)
 399                     , ("bodyFreeVars", annotatedCodeFreeVars bodyCD)
 400                     , ("annotatedCodeFloatingLets bodyCD", annotatedCodeFloatingLets bodyCD)
 401                     )
 402                     $ Syn.liftDerived1
 403                       ( \bodyOC ->
 404                           OpenCode $ \env ->
 405                             Syn.lam $ \x ->
 406                               (`unOpenCode` insertVar vname x env) $
 407                                 List.foldr bindFloatingLetMemo bodyOC bindingLFSByMemo
 408                       )
 409                       bodyCD
 410                         { annotatedCodeFloatingLets = FloatingLets passingFLS
 411                         , annotatedCodeFreeVars =
 412                             Set.delete (unVar vname) $
 413                               annotatedCodeFreeVars bodyCD
 414                                 `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
 415                         }
 416         )
 417         (body (lookupVarLetInserter vname))
 418 instance
 419   ( Syn.Letable code
 420   , Syn.LetRecable Int code
 421   ) =>
 422   Syn.Letable (LetInserter code)
 423   where
 424   let_ expR body = LetInserter $ do
 425     vname <- freshVar
 426     unR $
 427       Syn.liftDerived2
 428         ( \expCD bodyCD ->
 429             let (bindingFLS, passingFLS) =
 430                   List.partition
 431                     (\fl -> Set.member (unVar vname) (floatingLetFreeVars fl))
 432                     (unFloatingLets (annotatedCodeFloatingLets bodyCD))
 433             in let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
 434                in Syn.liftDerived2
 435                     ( \expOC bodyOC ->
 436                         OpenCode $ \env ->
 437                           Syn.let_ (unOpenCode expOC env) $ \x ->
 438                             (`unOpenCode` (insertVar vname x env)) $
 439                               List.foldr bindFloatingLetMemo bodyOC bindingLFSByMemo
 440                     )
 441                     expCD
 442                     bodyCD
 443                       { annotatedCodeFloatingLets = FloatingLets passingFLS
 444                       , annotatedCodeFreeVars =
 445                           Set.delete (unVar vname) $
 446                             annotatedCodeFreeVars bodyCD
 447                               `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
 448                       }
 449         )
 450         expR
 451         (body (lookupVarLetInserter vname))
 452
 453 bindLet :: Syn.Letable code => FloatingLet code -> OpenCode code a -> OpenCode code a
 454 bindLet fl2@FloatingLet{..} c =
 455   traceShow ("bindLet", fl2) $
 456     case floatingLetBoundCode of
 457       BoundCodeOpenCode oc -> OpenCode $ \env ->
 458         Syn.let_ (unOpenCode oc env) $ \x ->
 459           unOpenCode c $
 460             -- traceShow ("bindLet", floatingLetVarName) $
 461             insertVar floatingLetVarName x env
 462       _ -> error "bindLet is always called for evaluated bindings, without latent bound exp"
 463
 464 -- instance Syn.LetRecable idx (LetInserter sem) where
 465 --  letRec _idx f body =
 466 --    let self idx = LetInserter (\loc ->
 467 --          --trace ("letRec "<>show loc) $
 468 --          unR (f self idx) (PNote "fix":loc))
 469 --    in body self
 470
 471 -- mletRec :: p -> ((t1 -> LetInserter sem a) -> t1 -> LetInserter sem a) -> ((t1 -> LetInserter sem a) -> t2) -> t2
 472 -- mletRec _idx f body =
 473 --   let self idx = LetInserter $
 474 --         --trace ("letRec "<>show loc) $
 475 --         unR (f self idx)
 476 --   in body self
 477 --
 478 -- letR ::
 479 --   Syn.LetRecable Int sem =>
 480 --   (sem a -> sem a) ->
 481 --   (sem a -> sem w) ->
 482 --   sem w
 483 -- letR f body = Syn.letRec (1::Int)
 484 --   (\self _idx -> f (self 0))
 485 --   (\self -> body (self 0))
 486 -- type family MemoKey (sem:: Type -> Type) where MemoKey a = Memo
 487
 488 -- | Memoizing non-recursive genLet
 489 class MemoGenLetable sem where
 490   withLocus :: (Locus -> sem a) -> sem a
 491   genLetMemoAtMaybe :: Maybe Memo -> Maybe Locus -> sem a -> sem a
 492
 493 genLetMemo :: MemoGenLetable sem => Memo -> Locus -> sem a -> sem a
 494 genLetMemo m l = genLetMemoAtMaybe (Just m) (Just l)
 495
 496 genLet :: MemoGenLetable sem => sem a -> sem a
 497 genLet = genLetMemoAtMaybe Nothing Nothing
 498
 499 genLetAt :: MemoGenLetable sem => Locus -> sem a -> sem a
 500 genLetAt = genLetMemoAtMaybe Nothing . Just
 501
 502 instance Syn.Letable code => MemoGenLetable (LetInserter code) where
 503   withLocus body = LetInserter $ do
 504     lname <- Locus <$> freshNatural
 505     bodyCD <- unR (body lname)
 506     let fls = annotatedCodeFloatingLets bodyCD
 507     let bindingByLocusFLS = List.filter (\fl -> floatingLetLocus fl == Just lname) (unFloatingLets fls)
 508     let bindingVars = foldMap (Set.singleton . floatingLetVarname) bindingByLocusFLS
 509     let (bindingFLS, passingFLS) = List.partition (\fl -> not (Set.disjoint bindingVars (floatingLetFreeVars fl))) (unFloatingLets fls)
 510     let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
 511     return $
 512       traceShow (["withLocus"], ("bindingLFSByMemo", bindingLFSByMemo)) $
 513         -- check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
 514         AnnotatedCode
 515           { annotatedCodeOpenCode = List.foldr bindFloatingLetMemo (annotatedCodeOpenCode bodyCD) bindingLFSByMemo
 516           , annotatedCodeFloatingLets = FloatingLets passingFLS
 517           , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
 518           }
 519   genLetMemoAtMaybe keyMaybe mlname body = LetInserter $ traceShow (["genLetMemoAtMaybe"]) $ do
 520     vname <- freshVar
 521     -- mkey <- runIdentity <$> unR key
 522     bodyCD <-
 523       traceShow ("genLetMemoAtMaybe", ("vname", vname), ("key", keyMaybe)) $
 524         unR body
 525     let fvs = Set.insert (unVar vname) (annotatedCodeFreeVars bodyCD)
 526     -- if the bodyression to let-bind has itself let-bindings,
 527     -- they are straightened out
 528     -- The new binding is added at the end; it may depend on
 529     -- the bindings in evl (as is the case for the nested genLet)
 530     return $
 531       AnnotatedCode
 532         { annotatedCodeOpenCode = lookupVar vname
 533         , annotatedCodeFloatingLets =
 534             FloatingLets $
 535               unFloatingLets (annotatedCodeFloatingLets bodyCD)
 536                 <> [ FloatingLet
 537                       { floatingLetLocus = mlname
 538                       , floatingLetMemo = MaybeMemo keyMaybe
 539                       , floatingLetVarName = vname
 540                       , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode bodyCD)
 541                       , floatingLetFreeVars = fvs
 542                       }
 543                    ]
 544         , annotatedCodeFreeVars = fvs
 545         }
 546
 547 -- Bind the variables in order, preserving the dependency.
 548 -- Bind only one variable within each group, substituting the others
 549 bindFloatingLetMemo :: Syn.Letable code => [FloatingLet code] -> OpenCode code a -> OpenCode code a
 550 bindFloatingLetMemo gr oc =
 551   traceShow (["withLocus", "bindFloatingLetMemo"]) $
 552     case assertSameLocuses gr of
 553       [] -> error "bindFloatingLetMemo: empty group"
 554       [fl] -> bindLet fl oc
 555       fl@FloatingLet{floatingLetVarName = vName} : fls ->
 556         bindLet fl $ OpenCode $ \env ->
 557           let defCode = unOpenCode (lookupVar vName) env
 558           in let ext_equ env' fl2 =
 559                   reBind2 (memKey fl) defCode fl2
 560                     : env'
 561              in unOpenCode oc $ List.foldl' ext_equ env fls
 562   where
 563     memKey fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode{}} = floatingLetMemo fl
 564     memKey fl = error $ "group pust be canonical: " <> show fl
 565
 566 assertSameLocuses :: [FloatingLet code] -> [FloatingLet code]
 567 assertSameLocuses fls
 568   | Set.size (foldMap (Set.singleton . floatingLetLocus) fls) <= 1 = traceShow ("assertSameLocuses", fls) fls
 569   | otherwise = error "assertSameLocuses"
 570
 571 -- | Especially for 'Locus', all bindings have the same type.
 572 -- In any event, 'Locus' plus the 'Memo' key witness for the bindings' type.
 573 reBind2 :: MaybeMemo -> code a -> FloatingLet sem -> EnvBind code
 574 reBind2 k c fl
 575   | k == floatingLetMemo fl =
 576       traceShow (["reBind2"], ("k", k), ("fl", fl)) $
 577         EnvBind (Var (floatingLetVarname fl), c)
 578 reBind2 k _ fl = error $ "reBind2: locus/memo mismatch" <> show (("k", k), ("fl", fl))
 579
 580 {-
 581 genLetAt :: LetInserter code a -> LetInserter code a
 582 genLetAt = LetInserter $
 583   k <- freshKey
 584   genLetMemo
 585 -}
 586 -- TODO: Here genlet is a version of genlet l em e described earlier, for the case of all memo keys being distinct.
 587 -- TODO: newtype LocusRec = Locus
 588 {-
 589 genLetM = LetInserter $ \loc ->
 590   k <- freshKey
 591   genLetMemo Nothing k
 592 -}
 593
 594 -- | Unlike withLocus, we now have to evaluate expressions that
 595 -- may be present in virtual bindings.
 596 -- The rule: within an equivalence class, we evaluate only
 597 -- the bexp of its representative (the first member of the group)
 598 -- That evaluation may create more virtual bindings, which are to be merged
 599
 600 -- Pick vlbindings for the given locus and convert them to
 601
 602 -- * normal* equivalence classes.
 603
 604 -- Return the list of normal equivalence classes and the
 605 -- remaining bindings (for different loci).
 606 -- An equivalence class is called normal if its representative
 607 -- (the first binding in the group) has the BoundCodeOpenCode as the bound
 608 -- expression (that is, it is determined which future-stage expression to bind).
 609 -- If a group is not normal, that is, its representative has a not
 610 -- yet determined bound expression, we have to determine it --
 611 -- which creates more bindings to normalize (some of which could be
 612 -- members of existing groups -- but never replace the existing
 613 -- representative -- we always preserve the order!)
 614 --
 615 -- Keeping the correct order and maintain dependency is actually
 616 -- very difficult. When evaluating the expression bound to var v,
 617 -- we obtain a code value with vlbindings. Some of them mention v
 618 -- (and so should be put into the same group as v, but _after_ it),
 619 -- some are new and so should be put in a group _before_ v because
 620 -- the v binding may depend on them.
 621 -- It seems simpler to just forget about the order between groups
 622 -- and dependencies and generate one big letrec with mutually dependent clauses.
 623
 624 -- | @('groupBy' eq xs)@: partition a list @xs@
 625 -- into a list of equivalence classes quotiented by the @eq@ function
 626 --
 627 -- The order of the groups follows the order in the input list;
 628 -- within each group, the elements occur in the same order they
 629 -- do in the input list.
 630 groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
 631 groupBy eq = go []
 632   where
 633     go acc [] = List.reverse acc
 634     go acc (x : xs) = go ((x : grp) : acc) rest
 635       where
 636         (grp, rest) = List.partition (eq x) xs
 637
 638 normalizeGroup :: Locus -> FloatingLets code -> MT.State Natural ([FloatingLets code], FloatingLets code)
 639 normalizeGroup lname vl = do
 640   let (bindingFLS, passingFLS) = List.partition (\FloatingLet{..} -> floatingLetLocus == Just lname) (unFloatingLets vl)
 641   let bindingLFSByMemo = groupBy ((==) `on` floatingLetMemo) bindingFLS
 642   -- Try to find an abnormal group
 643   let (normalGroups, abnormalGroups) =
 644         let abnomality_check = \case
 645               FloatingLet{floatingLetBoundCode = BoundCodeLetInserter{}} : _ -> True
 646               _ -> False
 647         in List.break abnomality_check bindingLFSByMemo
 648   -- traceShow (["normalizeGroup"], ("lname",lname), ("bindingLFSByMemo", FloatingLets <$> bindingLFSByMemo), ("normalGroups", FloatingLets <$> normalGroups), ("abnormalGroups", FloatingLets <$> abnormalGroups), ("passingFLS", FloatingLets passingFLS)) $
 649   case abnormalGroups of
 650     -- all groups are normal
 651     [] ->
 652       return $
 653         traceShow (["normalizeGroup", "return"], ("lname", lname), ("normalGroups", FloatingLets <$> normalGroups), ("passingFLS", passingFLS)) $
 654           (FloatingLets <$> normalGroups, FloatingLets passingFLS)
 655     -- at least one group representative is abnormal
 656     (fl0@FloatingLet{floatingLetBoundCode = BoundCodeLetInserter fl0Exp, floatingLetVarName = fl0VarName} : fls0) : grps -> do
 657       fl0BodyCD <- unR fl0Exp
 658       -- The group has become normal
 659       let normalizedFL0 =
 660             FloatingLet
 661               { floatingLetLocus = floatingLetLocus fl0
 662               , floatingLetMemo = floatingLetMemo fl0
 663               , floatingLetVarName = fl0VarName
 664               , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode fl0BodyCD)
 665               , -- Update the free variables, which could not be done in 'genLetMemoRec'
 666                 -- where fl0BodyCD was not yet available.
 667                 floatingLetFreeVars = floatingLetFreeVars fl0 <> annotatedCodeFreeVars fl0BodyCD
 668               }
 669               : fls0
 670       let groups = normalGroups <> (normalizedFL0 : grps)
 671       -- New bindings
 672       -- let vl' = FloatingLets (List.concat groups) <> FloatingLets passingFLS <> annotatedCodeFloatingLets fl0BodyCD
 673       let vl' = FloatingLets $ List.concat groups <> passingFLS <> unFloatingLets (annotatedCodeFloatingLets fl0BodyCD)
 674       normalizeGroup lname vl'
 675     _ -> error "normalizeGroup: groups are always non-empty"
 676
 677 -- * Class 'MemoGenLetRecable'
 678 class MemoGenLetRecable sem where
 679   withLocusRec :: (Locus -> sem a) -> sem a
 680   genLetMemoRec :: Locus -> Memo -> sem a -> sem a
 681
 682 instance
 683   Syn.LetRecable Int code =>
 684   MemoGenLetRecable (LetInserter code)
 685   where
 686   withLocusRec body = LetInserter $ do
 687     lname <- Locus <$> freshNatural
 688     bodyCD <- unR $ body lname
 689     (bindingFLS, passingFLS) <-
 690       check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
 691         normalizeGroup lname (annotatedCodeFloatingLets bodyCD)
 692     -- Bind the variables in order, preserving the dependency
 693     return $
 694       traceShow (["withLocusRec", "return"], ("lname", lname), ("bindingFLS", bindingFLS), ("passingFLS", passingFLS)) $
 695         AnnotatedCode
 696           { annotatedCodeOpenCode = bindFloatingLetMemoRec bindingFLS (annotatedCodeOpenCode bodyCD)
 697           , annotatedCodeFloatingLets = passingFLS
 698           , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` foldMap (Set.fromList . (floatingLetVarname <$>) . unFloatingLets) bindingFLS
 699           }
 700   genLetMemoRec lname key body = LetInserter $ do
 701     vname <- freshVar
 702     -- Cannot compute all the free variables yet
 703     -- because body is not yet evaluated to a 'AnnotatedCode'
 704     let fvs = Set.singleton (unVar vname)
 705     return $
 706       traceShow (["genLetMemoRec"], ("key", key), ("vname", vname)) $
 707         AnnotatedCode
 708           { annotatedCodeOpenCode = lookupVar vname
 709           , annotatedCodeFloatingLets =
 710               FloatingLets
 711                 [ FloatingLet
 712                     { floatingLetLocus = Just lname
 713                     , floatingLetMemo = MaybeMemo (Just key)
 714                     , floatingLetVarName = vname
 715                     , floatingLetBoundCode = BoundCodeLetInserter body
 716                     , floatingLetFreeVars = fvs
 717                     }
 718                 ]
 719           , annotatedCodeFreeVars = fvs
 720           }
 721
 722 -- | Create mutually-recursive letrec bindings.
 723 -- All variables are bound at the same time.
 724 -- The binding expression is taken from the group representative.
 725 -- It has to be 'BoundCodeOpenCode': all groups assumed to be normal.
 726 bindFloatingLetMemoRec ::
 727   Syn.LetRecable Int code =>
 728   [FloatingLets code] ->
 729   OpenCode code a ->
 730   OpenCode code a
 731 bindFloatingLetMemoRec [] c = c
 732 bindFloatingLetMemoRec bindingFLS c =
 733   traceShow (["bindFloatingLetMemoRec", "OpenCode"], ("bindingFLS", bindingFLS)) $
 734     OpenCode $ \env ->
 735       traceShow (["bindFloatingLetMemoRec", "Syn.letRec"], ("bindingFLS", bindingFLS), ("env", env)) $
 736         Syn.letRec
 737           len
 738           ( \self idx ->
 739               traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds"], ("idx", idx)) $
 740                 ( traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds", "List.!!"], ("len", len), ("idx", idx), ("env", env)) $
 741                     unOpenCode (tobindOC List.!! idx)
 742                 )
 743                   ( traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "binds", "bind_all"], ("idx", idx), ("env", env)) $
 744                       bind_all self env
 745                   )
 746           )
 747           ( \self ->
 748               traceShow (["bindFloatingLetMemoRec", "Syn.letRec", "end"], ("env", env)) $
 749                 unOpenCode c (bind_all self env)
 750           )
 751   where
 752     len = List.length bindingFLS
 753     -- (label,key) of group representative
 754     lk (fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode{}} : _) = floatingLetMemo fl
 755     lk _ = error "groups must be non-empty and canonical"
 756     bind_group :: code a -> FloatingLets code -> [EnvBind code]
 757     -- Create bindings to bind all identifiers in a group
 758     bind_group ec (FloatingLets grp) =
 759       traceShow (["bindFloatingLetMemoRec", "bind_group"], ("grp", grp)) $
 760         List.map (reBind2 (lk grp) ec) (assertSameLocuses grp)
 761     bind_all self env =
 762       traceShow (["bindFloatingLetMemoRec", "bind_all"], ("bindingFLS", bindingFLS), ("env", env)) $
 763         List.concat $
 764           List.zipWith (\grp i -> bind_group (self i) grp) bindingFLS [0 :: Int .. pred len] <> [env]
 765     tobindOC =
 766       traceShow (["bindFloatingLetMemoRec", "tobindOC"], ("bindingFLS", bindingFLS)) $
 767         List.map
 768           ( \case
 769               -- TODO: avoid unwrapping
 770               FloatingLets (fl@FloatingLet{floatingLetBoundCode = BoundCodeOpenCode oc} : _) ->
 771                 traceShow (["bindFloatingLetMemoRec", "tobindOC", "map"], fl) $
 772                   unsafeCoerce (oc)
 773               _ -> error "tobindOC"
 774           )
 775           bindingFLS
 776
 777 {-
 778 genLetLocus :: Syn.Letable code => (Locus -> LetInserter code a) -> LetInserter code a
 779 genLetLocus body = LetInserter $ do
 780   lname <- Locus <$> freshNatural
 781   bodyCD <-
 782     traceShow ("genLetLocus", ("lname", lname)) $
 783     unR (body lname)
 784   let (bindingFLS, passingFLS) =
 785         List.partition (\fl -> floatingLetLocus fl == Just lname)
 786                        (unFloatingLets (annotatedCodeFloatingLets bodyCD))
 787   -- Bind the variables in order, preserving the dependency
 788   --traceShow ("genLetLocus", (bindingFLS, passingFLS)) $
 789   return $
 790     check_no_dup_varname (annotatedCodeFloatingLets bodyCD) $
 791     AnnotatedCode{ annotatedCodeOpenCode = List.foldr bindLet (annotatedCodeOpenCode bodyCD) bindingFLS
 792       , annotatedCodeFloatingLets = FloatingLets passingFLS
 793       , annotatedCodeFreeVars = annotatedCodeFreeVars bodyCD `Set.difference` Set.fromList (floatingLetVarname <$> bindingFLS)
 794       }
 795 -- In MetaOCaml, let(rec) is actually inserted either at the place
 796 -- of the explicit let locus,
 797 -- or at the binding that dominates all free variables of the bound expression,
 798 -- whichever has the narrowest scope.
 799 genLetAtMaybe :: Maybe Locus -> LetInserter code a -> LetInserter code a
 800 genLetAtMaybe mlname body = LetInserter $ do
 801   vname <- freshVar
 802   bodyCD <-
 803         traceShow ("genLet", ("vname", vname)) $
 804         unR body
 805   -- if the expression to let-bind has itself let-bindings,
 806   -- they are straightened out
 807   -- The new binding is added at the end; it may depend on
 808   -- the bindings coming before (as is the case for the nested genLet)
 809   return $
 810     traceShow (["genLet", "bodyCD"], ("vname", vname), ("bodyCDFreeVars", (annotatedCodeFreeVars bodyCD))) $
 811     AnnotatedCode
 812       { annotatedCodeOpenCode = traceShow (["genLet", "lookupVar"], ("vname", vname)) $ lookupVar vname
 813       , annotatedCodeFloatingLets = FloatingLets $
 814           --(\vls -> traceShow (["genLet", "bindings"], vls) vls) $
 815           unFloatingLets (annotatedCodeFloatingLets bodyCD) <>
 816           [ FloatingLet
 817               { floatingLetLocus = mlname
 818               , floatingLetMemo = MaybeMemo (Just 0)
 819               , floatingLetVarName = vname
 820               , floatingLetBoundCode = BoundCodeOpenCode (annotatedCodeOpenCode bodyCD)
 821               , floatingLetFreeVars = Set.insert (unVar vname) (annotatedCodeFreeVars bodyCD)
 822               }
 823           ]
 824       , annotatedCodeFreeVars = Set.insert (unVar vname) $ annotatedCodeFreeVars bodyCD
 825       }
 826 genLetAt :: Locus -> LetInserter code a -> LetInserter code a
 827 genLetAt = genLetAtMaybe . Just
 828
 829 genLet :: LetInserter code a -> LetInserter code a
 830 genLet = genLetAtMaybe Nothing
 831 -}