content: {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE DeriveAnyClass        #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE UndecidableInstances  #-}
  {-# LANGUAGE StandaloneDeriving    #-}
  
  -- | A higher-ordered surface language that supports Rank-1 parametric
  -- polymorphism.
  module Gibbon.L0.Syntax
    ( module Gibbon.L0.Syntax,
      module Gibbon.Language,
    )
  where
  
  import           Control.Monad.State ( MonadState )
  import           Control.DeepSeq (NFData)
  import qualified Data.List as L
  import qualified Data.Loc as Loc
  import           GHC.Generics
  import           Text.PrettyPrint.GenericPretty
  import           Text.PrettyPrint.HughesPJ as PP
  import qualified Data.Set as S
  import qualified Data.Map as M
  import qualified Safe as Sf
  
  import           Gibbon.Common as C
  import           Gibbon.Language hiding (UrTy(..))
  
  --------------------------------------------------------------------------------
  
  -- In L0, type information may be held in locations, as locations don't exist
  type Exp0     = PreExp E0Ext Ty0 Ty0
  type DDefs0   = DDefs Ty0
  type DDef0    = DDef Ty0
  type FunDef0  = FunDef Var Exp0
  type FunDefs0 = FunDefs Var Exp0
  type Prog0    = Prog Var Exp0
  
  --------------------------------------------------------------------------------
  
  -- | The extension point for L0.
  data E0Ext loc dec =
     LambdaE [(Var,dec)] -- Variable tagged with type
             (PreExp E0Ext loc dec)
     -- unused for much of L0, may be due to a bug
   | PolyAppE (PreExp E0Ext loc dec) -- Operator
              (PreExp E0Ext loc dec) -- Operand
   | FunRefE [loc] Var -- Reference to a function (toplevel or lambda),
                       -- along with its tyapps.
   | BenchE Var [loc] [(PreExp E0Ext loc dec)] Bool
   | ParE0 [(PreExp E0Ext loc dec)]
   | PrintPacked dec (PreExp E0Ext loc dec) -- ^ Print a packed value to standard out.
   | CopyPacked dec (PreExp E0Ext loc dec) -- ^ Copy a packed value.
   | TravPacked dec (PreExp E0Ext loc dec) -- ^ Traverse a packed value.
   | L Loc.Loc (PreExp E0Ext loc dec)
   | LinearExt (LinearExt loc dec)
   deriving (Show, Ord, Eq, Read, Generic, NFData)
  
  -- | Linear types primitives.
  data LinearExt loc dec =
      -- (&) :: a %1 -> (a %1 -> b) %1 -> b
    ReverseAppE (PreExp E0Ext loc dec) (PreExp E0Ext loc dec)
  
  -- lseq :: a %1-> b %1-> b
    | LseqE (PreExp E0Ext loc dec) (PreExp E0Ext loc dec)
  
  -- unsafeAlias :: a %1-> (a,a)
    | AliasE (PreExp E0Ext loc dec)
  
  -- unsafeToLinear :: (a %p-> b) %1-> (a %1-> b)
    | ToLinearE (PreExp E0Ext loc dec)
    deriving (Show, Ord, Eq, Read, Generic, NFData)
  
  --------------------------------------------------------------------------------
  -- Helper methods to integrate the Data.Loc with Gibbon
  
  deriving instance Generic Loc.Loc
  deriving instance Generic Loc.Pos
  deriving instance NFData  Loc.Pos
  deriving instance NFData  Loc.Loc
  
  -- | Orphaned instance: read without source locations.
  instance Read t => Read (Loc.L t) where
    readsPrec n str = [ (Loc.L Loc.NoLoc a,s) | (a,s) <- readsPrec n str ]
  
  instance Out Loc.Loc where
    docPrec _ loc = doc loc
  
    doc loc =
      case loc of
        Loc.Loc start _end -> doc start
        Loc.NoLoc -> PP.empty
  
  instance Out Loc.Pos where
    docPrec _ pos = doc pos
    doc (Loc.Pos path line col _) = hcat [doc path, colon, doc line, colon, doc col]
  
  --------------------------------------------------------------------------------
  -- Instances for E0Ext
  
  instance FreeVars (E0Ext l d) where
    gFreeVars e =
      case e of
        LambdaE args bod -> foldr S.delete (gFreeVars bod) (map fst args)
        PolyAppE f d     -> gFreeVars f `S.union` gFreeVars d
        FunRefE _ f      -> S.singleton f
        BenchE _ _ args _-> S.unions (map gFreeVars args)
        ParE0 ls         -> S.unions (map gFreeVars ls)
        PrintPacked _ e1 -> gFreeVars e1
        CopyPacked _ e1  -> gFreeVars e1
        TravPacked _ e1  -> gFreeVars e1
        L _ e1           -> gFreeVars e1
        LinearExt ext      -> gFreeVars ext
  
  instance (Out l, Out d, Show l, Show d) => Expression (E0Ext l d) where
    type LocOf (E0Ext l d) = l
    type TyOf (E0Ext l d)  = d
    isTrivial _ = False
  
  instance (Show l, Out l) => Flattenable (E0Ext l Ty0) where
      gFlattenGatherBinds _ddfs _env ex = return ([], ex)
      gFlattenExp _ddfs _env ex = return ex
  
  instance HasSubstitutableExt E0Ext l d => SubstitutableExt (PreExp E0Ext l d) (E0Ext l d) where
    gSubstExt old new ext =
      case ext of
        LambdaE args bod -> LambdaE args (gSubst old new bod)
        PolyAppE a b     -> PolyAppE (gSubst old new a) (gSubst old new b)
        FunRefE{}        -> ext
        BenchE fn tyapps args b -> BenchE fn tyapps (map (gSubst old new) args) b
        ParE0 ls -> ParE0 $ map (gSubst old new) ls
        PrintPacked ty e1 -> PrintPacked ty (gSubst old new e1)
        CopyPacked ty e1 -> CopyPacked ty (gSubst old new e1)
        TravPacked ty e1 -> TravPacked ty (gSubst old new e1)
        L p e1   -> L p (gSubst old new e1)
        LinearExt e -> LinearExt (gSubstExt old new e)
  
    gSubstEExt old new ext =
      case ext of
        LambdaE args bod -> LambdaE args (gSubstE old new bod)
        PolyAppE a b     -> PolyAppE (gSubstE old new a) (gSubstE old new b)
        FunRefE{}        -> ext
        BenchE fn tyapps args b -> BenchE fn tyapps (map (gSubstE old new) args) b
        ParE0 ls -> ParE0 $ map (gSubstE old new) ls
        PrintPacked ty e -> PrintPacked ty $ (gSubstE old new e)
        CopyPacked ty e -> CopyPacked ty $ (gSubstE old new e)
        TravPacked ty e -> TravPacked ty $ (gSubstE old new e)
        L p e    -> L p $ (gSubstE old new e)
        LinearExt e -> LinearExt (gSubstEExt old new e)
  
  instance HasRenamable E0Ext l d => Renamable (E0Ext l d) where
    gRename env ext =
      case ext of
        LambdaE args bod -> LambdaE (map (\(a,b) -> (go a, go b)) args) (go bod)
        PolyAppE a b     -> PolyAppE (go a) (go b)
        FunRefE tyapps a -> FunRefE (map go tyapps) (go a)
        BenchE fn tyapps args b -> BenchE fn (map go tyapps) (map go args) b
        ParE0 ls -> ParE0 $ map (gRename env) ls
        PrintPacked ty e -> PrintPacked ty (gRename env e)
        CopyPacked ty e -> CopyPacked ty (gRename env e)
        TravPacked ty e -> TravPacked ty (gRename env e)
        L p e    -> L p (gRename env e)
        LinearExt e -> LinearExt (gRename env e)
      where
        go :: forall a. Renamable a => a -> a
        go = gRename env
  
  instance (Out l, Out d) => Out (E0Ext l d)
  instance Out Ty0
  instance Out TyScheme
  
  --------------------------------------------------------------------------------
  -- Instances for LinearExt
  
  instance FreeVars (LinearExt l d) where
    gFreeVars e =
      case e of
        ReverseAppE fn arg -> gFreeVars fn `S.union` (gFreeVars arg)
        LseqE a b   -> gFreeVars a `S.union` gFreeVars b
        AliasE a    -> gFreeVars a
        ToLinearE a -> gFreeVars a
  
  instance (Out l, Out d, Show l, Show d) => Expression (LinearExt l d) where
    type LocOf (LinearExt l d) = l
    type TyOf (LinearExt l d)  = d
    isTrivial _ = False
  
  instance (Show l, Out l) => Flattenable (LinearExt l Ty0) where
      gFlattenGatherBinds _ddfs _env ex = return ([], ex)
      gFlattenExp _ddfs _env ex = return ex
  
  instance HasSubstitutableExt E0Ext l d => SubstitutableExt (PreExp E0Ext l d) (LinearExt l d) where
    gSubstExt old new ext =
      case ext of
        ReverseAppE fn arg -> ReverseAppE (gSubst old new fn) (gSubst old new arg)
        LseqE a b   -> LseqE (gSubst old new a) (gSubst old new b)
        AliasE a    -> AliasE (gSubst old new a)
        ToLinearE a -> ToLinearE (gSubst old new a)
  
    gSubstEExt old new ext =
      case ext of
        ReverseAppE fn arg -> ReverseAppE (gSubstE old new fn) (gSubstE old new arg)
        LseqE a b   -> LseqE (gSubstE old new a) (gSubstE old new b)
        AliasE a    -> AliasE (gSubstE old new a)
        ToLinearE a -> ToLinearE (gSubstE old new a)
  
  instance HasRenamable E0Ext l d => Renamable (LinearExt l d) where
    gRename env ext =
      case ext of
        ReverseAppE fn arg -> ReverseAppE (go fn) (go arg)
        LseqE a b   -> LseqE (go a) (go b)
        AliasE a    -> AliasE (go a)
        ToLinearE a -> ToLinearE (go a)
      where
        go :: forall a. Renamable a => a -> a
        go = gRename env
  
  instance (Out l, Out d) => Out (LinearExt l d)
  
  --------------------------------------------------------------------------------
  
  data MetaTv = Meta Int
    deriving (Read, Show, Eq, Ord, Generic, NFData)
  
  instance Out MetaTv where
    doc (Meta i) = text "$" PP.<> doc i
    docPrec _ v = doc v
  
  newMetaTv :: MonadState Int m => m MetaTv
  newMetaTv = Meta <$> newUniq
  
  newMetaTy :: MonadState Int m => m Ty0
  newMetaTy = MetaTv <$> newMetaTv
  
  newTyVar :: MonadState Int m => m TyVar
  newTyVar = BoundTv <$> genLetter
  
  data Ty0
   = IntTy
   | CharTy
   | FloatTy
   | SymTy0
   | BoolTy
   | TyVar TyVar   -- Rigid/skolem type variables
   | MetaTv MetaTv -- Unification variables
   | ProdTy [Ty0]
   | SymDictTy (Maybe Var) Ty0
   | PDictTy Ty0 Ty0
   | SymSetTy
   | SymHashTy
   | IntHashTy
   | ArrowTy [Ty0] Ty0
   | PackedTy TyCon [Ty0] -- Type arguments to the type constructor
   | VectorTy Ty0
   | ListTy Ty0
   | ArenaTy
    deriving (Show, Read, Eq, Ord, Generic, NFData)
  
  instance FunctionTy Ty0 where
    type ArrowTy Ty0 = TyScheme
    inTys  = arrIns
    outTy  = arrOut
  
  instance Renamable TyVar where
    gRename env tv =
      case tv of
        BoundTv v  -> BoundTv (gRename env v)
        SkolemTv{} -> tv
        UserTv v   -> UserTv (gRename env v)
  
  instance Renamable Ty0 where
    gRename env ty =
      case ty of
        IntTy  -> IntTy
        CharTy -> CharTy
        FloatTy-> FloatTy
        SymTy0 -> SymTy0
        BoolTy -> BoolTy
        TyVar tv  -> TyVar (go tv)
        MetaTv{}  -> ty
        ProdTy ls -> ProdTy (map go ls)
        SymDictTy a t     -> SymDictTy a (go t)
        PDictTy k v       -> PDictTy (go k) (go v)
        ArrowTy args ret  -> ArrowTy (map go args) ret
        PackedTy tycon ls -> PackedTy tycon (map go ls)
        VectorTy a        -> VectorTy (go a)
        ListTy a          -> ListTy (go a)
        ArenaTy           -> ArenaTy
        SymSetTy          -> SymSetTy
        SymHashTy         -> SymHashTy
        IntHashTy         -> IntHashTy
      where
        go :: forall a. Renamable a => a -> a
        go = gRename env
  
  -- | Straightforward parametric polymorphism.
  data TyScheme = ForAll [TyVar] Ty0
   deriving (Show, Read, Eq, Ord, Generic, NFData)
  
  -- instance FreeVars TyScheme where
  --   gFreeVars (ForAll tvs ty) = gFreeVars ty `S.difference` (S.fromList tvs)
  
  arrIns :: TyScheme -> [Ty0]
  arrIns (ForAll _ (ArrowTy i _)) = i
  arrIns err = error $ "arrIns: Not an arrow type: " ++ show err
  
  arrOut :: TyScheme -> Ty0
  arrOut (ForAll _ (ArrowTy _ o)) = o
  arrOut err = error $ "arrOut: Not an arrow type: " ++ show err
  
  arrIns' :: Ty0 -> [Ty0]
  arrIns' (ArrowTy i _) = i
  arrIns' err = error $ "arrIns': Not an arrow type: " ++ show err
  
  tyFromScheme :: TyScheme -> Ty0
  tyFromScheme (ForAll _ a) = a
  
  tyVarsFromScheme :: TyScheme -> [TyVar]
  tyVarsFromScheme (ForAll a _) = a
  
  isFunTy :: Ty0 -> Bool
  isFunTy ArrowTy{} = True
  isFunTy _ = False
  
  isCallUnsaturated :: TyScheme -> [Exp0] -> Bool
  isCallUnsaturated sigma args = length args < length (arrIns sigma)
  
  saturateCall :: MonadState Int m => TyScheme -> Exp0 -> m Exp0
  saturateCall sigma ex =
    case ex of
      AppE f [] args -> do
        -- # args needed to saturate this call-site.
        let args_wanted = length (arrIns sigma) - length args
        new_args <- mapM (\_ -> gensym "sat_arg_") [0..(args_wanted-1)]
        new_tys  <- mapM (\_ -> newMetaTy) new_args
        pure $
          Ext (LambdaE (zip new_args new_tys)
                 (AppE f [] (args ++ (map VarE new_args))))
  
      AppE _ tyapps _ ->
        error $ "saturateCall: Expected tyapps to be [], got: " ++ sdoc tyapps
      _ -> error $ "saturateCall: " ++ sdoc ex ++ " is not a call-site."
  
  -- | Get the free TyVars from types; no duplicates in result.
  tyVarsInTy :: Ty0 -> [TyVar]
  tyVarsInTy ty = tyVarsInTys [ty]
  
  -- | Like 'tyVarsInTy'.
  tyVarsInTys :: [Ty0] -> [TyVar]
  tyVarsInTys tys = foldr (go []) [] tys
    where
      go :: [TyVar] -> Ty0 -> [TyVar] -> [TyVar]
      go bound ty acc =
        case ty of
          IntTy  -> acc
          CharTy -> acc
          FloatTy-> acc
          SymTy0 -> acc
          BoolTy -> acc
          TyVar tv -> if (tv `elem` bound) || (tv `elem` acc)
                      then acc
                      else tv : acc
          MetaTv _ -> acc
          ProdTy tys1     -> foldr (go bound) acc tys1
          SymDictTy _ ty1   -> go bound ty1 acc
          PDictTy k v -> foldr (go bound) acc [k,v]
          ArrowTy tys1 b  -> foldr (go bound) (go bound b acc) tys1
          PackedTy _ tys1 -> foldr (go bound) acc tys1
          VectorTy ty1 -> go bound ty1 acc
          ListTy ty1 -> go bound ty1 acc
          ArenaTy -> acc
          SymSetTy -> acc
          SymHashTy -> acc
          IntHashTy -> acc
  
  -- | Get the MetaTvs from a type; no duplicates in result.
  metaTvsInTy :: Ty0 -> [MetaTv]
  metaTvsInTy ty = metaTvsInTys [ty]
  
  -- | Like 'metaTvsInTy'.
  metaTvsInTys :: [Ty0] -> [MetaTv]
  metaTvsInTys tys = foldr go [] tys
    where
      go :: Ty0 -> [MetaTv] -> [MetaTv]
      go ty acc =
        case ty of
          MetaTv tv -> if tv `elem` acc
                       then acc
                       else tv : acc
          IntTy   -> acc
          CharTy  -> acc
          FloatTy -> acc
          SymTy0  -> acc
          BoolTy  -> acc
          TyVar{} -> acc
          ProdTy tys1     -> foldr go acc tys1
          SymDictTy _ ty1   -> go ty1 acc
          PDictTy k v -> go v (go k acc)
          ArrowTy tys1 b  -> go b (foldr go acc tys1)
          PackedTy _ tys1 -> foldr go acc tys1
          VectorTy ty1 -> go ty1 acc
          ListTy ty1 -> go ty1 acc
          ArenaTy -> acc
          SymSetTy -> acc
          SymHashTy -> acc
          IntHashTy -> acc
  
  -- | Like 'tyVarsInTy'.
  tyVarsInTyScheme :: TyScheme -> [TyVar]
  tyVarsInTyScheme (ForAll tyvars ty) = tyVarsInTy ty L.\\ tyvars
  
  -- | Like 'metaTvsInTy'.
  metaTvsInTyScheme :: TyScheme -> [MetaTv]
  metaTvsInTyScheme (ForAll _ ty) = metaTvsInTy ty -- ForAll binds TyVars only
  
  -- | Like 'metaTvsInTys'.
  metaTvsInTySchemes :: [TyScheme] -> [MetaTv]
  metaTvsInTySchemes tys = concatMap metaTvsInTyScheme tys
  
  arrowTysInTy :: Ty0 -> [Ty0]
  arrowTysInTy = go []
    where
      go acc ty =
        case ty of
          IntTy    -> acc
          CharTy   -> acc
          FloatTy  -> acc
          SymTy0   -> acc
          BoolTy   -> acc
          ArenaTy  -> acc
          TyVar{}  -> acc
          MetaTv{} -> acc
          ProdTy tys -> foldl go acc tys
          SymDictTy _ a -> go acc a
          PDictTy k v   -> go (go acc k) v
          ArrowTy tys b -> go (foldl go acc tys) b ++ [ty]
          PackedTy _ vs -> foldl go acc vs
          VectorTy a -> go acc a
          ListTy a  -> go acc a
          SymSetTy  -> acc
          SymHashTy -> acc
          IntHashTy -> acc
  
  -- | Replace the specified quantified type variables by
  -- given meta type variables.
  substTyVar :: M.Map TyVar Ty0 -> Ty0 -> Ty0
  substTyVar mp ty =
    case ty of
      IntTy    -> ty
      CharTy   -> ty
      FloatTy  -> ty
      SymTy0   -> ty
      BoolTy   -> ty
      TyVar v  -> M.findWithDefault ty v mp
      MetaTv{} -> ty
      ProdTy tys  -> ProdTy (map go tys)
      SymDictTy v t -> SymDictTy v (go t)
      PDictTy k v -> PDictTy (go k) (go v)
      ArrowTy tys b  -> ArrowTy (map go tys) (go b)
      PackedTy t tys -> PackedTy t (map go tys)
      VectorTy t -> VectorTy (go t)
      ListTy t -> ListTy (go t)
      ArenaTy -> ty
      SymSetTy -> ty
      SymHashTy -> ty
      IntHashTy -> ty
    where
      go = substTyVar mp
  
  isScalarTy0 :: Ty0 -> Bool
  isScalarTy0 IntTy  = True
  isScalarTy0 CharTy = True
  isScalarTy0 SymTy0 = True
  isScalarTy0 BoolTy = True
  isScalarTy0 FloatTy= True
  isScalarTy0 _      = False
  
  voidTy0 :: Ty0
  voidTy0 = ProdTy []
  
  -- | Lists of scalars or flat products of scalars are allowed.
  isValidListElemTy0 :: Ty0 -> Bool
  isValidListElemTy0 ty
    | isScalarTy0 ty = True
    | otherwise = case ty of
                    ProdTy tys -> all isScalarTy0 tys
                    _ -> False
  
  -- Hack: in the specializer, we sometimes want to know the type of
  -- an expression. However, we cannot derive Typeable for L0.
  --
  -- Typeable is based on 'UrTy' which is used by the L1, L2 and L3 IR's, but *not* L0.
  -- L0 uses it's own type (Ty0) representation.
  --
  -- Can we merge 'Ty0' and 'UrTy' ? We could, but we would end up polluting 'UrTy'
  -- with type variables and function types and such, which are unused after L0.
  -- Or we can have a special function just for L0, which is what recoverType is.
  -- ¯\_(ツ)_/¯
  --
  recoverType :: DDefs0 -> Env2 Var Ty0 -> Exp0 -> Ty0
  recoverType ddfs env2 ex =
    case ex of
      VarE v       -> M.findWithDefault (error $ "recoverType: Unbound variable " ++ show v) v (vEnv env2)
      LitE _       -> IntTy
      CharE _      -> CharTy
      FloatE{}     -> FloatTy
      LitSymE _    -> IntTy
      AppE v tyapps _ -> let (ForAll tyvars (ArrowTy _ retty)) = fEnv env2 # v
                         in substTyVar (M.fromList (fragileZip tyvars tyapps)) retty
      -- PrimAppE (DictInsertP ty) ((L _ (VarE v)):_) -> SymDictTy (Just v) ty
      -- PrimAppE (DictEmptyP  ty) ((L _ (VarE v)):_) -> SymDictTy (Just v) ty
      PrimAppE p _ -> primRetTy1 p
      LetE (v,_,t,_) e -> recoverType ddfs (extendVEnv v t env2) e
      IfE _ e _        -> recoverType ddfs env2 e
      MkProdE es       -> ProdTy $ map (recoverType ddfs env2) es
      DataConE (ProdTy locs) c _ -> PackedTy (getTyOfDataCon ddfs c) locs
      DataConE loc c _ -> PackedTy (getTyOfDataCon ddfs c) [loc]
      TimeIt e _ _     -> recoverType ddfs env2 e
      MapE _ e         -> recoverType ddfs env2 e
      FoldE _ _ e      -> recoverType ddfs env2 e
      ProjE i e ->
        case recoverType ddfs env2 e of
          (ProdTy tys) -> tys !! i
          oth -> error$ "typeExp: Cannot project fields from this type: "++show oth
                        ++"\nExpression:\n  "++ sdoc ex
                        ++"\nEnvironment:\n  "++sdoc (vEnv env2)
      SpawnE v tyapps _ -> let (ForAll tyvars (ArrowTy _ retty)) = fEnv env2 # v
                           in substTyVar (M.fromList (fragileZip tyvars tyapps)) retty
      SyncE -> voidTy0
      CaseE _ mp ->
        let (c,args,e) = Sf.headErr mp
            args' = map fst args
        in recoverType ddfs (extendsVEnv (M.fromList (zip args' (lookupDataCon ddfs c))) env2) e
      WithArenaE{} -> error "recoverType: WithArenaE not handled."
      Ext ext ->
        case ext of
          LambdaE args bod ->
            recoverType ddfs (extendsVEnv (M.fromList args) env2) bod
          FunRefE _ f ->
            case (M.lookup f (vEnv env2), M.lookup f (fEnv env2)) of
              (Nothing, Nothing) -> error $ "recoverType: Unbound function " ++ show f
              (Just ty, _) -> ty
              (_, Just ty) -> tyFromScheme ty -- CSK: Not sure if this is what we want?
          PolyAppE{}  -> error "recoverTypeep: TODO PolyAppE"
          BenchE fn _ _ _ -> outTy $ fEnv env2 # fn
          PrintPacked _ arg -> recoverType ddfs env2 arg
          CopyPacked _ arg -> recoverType ddfs env2 arg
          TravPacked _ _ -> voidTy0
          ParE0 ls -> ProdTy $ map (recoverType ddfs env2) ls
          LinearExt lin ->
            case lin of
              ReverseAppE fn _args -> case recoverType ddfs env2 fn of
                                        ArrowTy _ ty -> ty
                                        oth -> error $ "recoverType: ReverseAppE expected a function type, got: " ++ sdoc oth
              LseqE _ b -> recoverType ddfs env2 b
              AliasE a  -> let ty = recoverType ddfs env2 a
                           in ProdTy [ty,ty]
              ToLinearE a -> recoverType ddfs env2 a
  
          L _ e    -> recoverType ddfs env2 e
    where
      -- Return type for a primitive operation.
      primRetTy1 :: Prim Ty0 -> Ty0
      primRetTy1 p =
        case p of
          AddP -> IntTy
          SubP -> IntTy
          MulP -> IntTy
          DivP -> IntTy
          ModP -> IntTy
          ExpP -> IntTy
          RandP-> IntTy
          FAddP -> FloatTy
          FSubP -> FloatTy
          FMulP -> FloatTy
          FDivP -> FloatTy
          FExpP -> FloatTy
          FSqrtP-> FloatTy
          FRandP-> FloatTy
          FTanP -> FloatTy
          FloatToIntP -> IntTy
          IntToFloatP -> FloatTy
          EqSymP  -> BoolTy
          EqBenchProgP _ -> BoolTy
          EqIntP  -> BoolTy
          EqFloatP-> BoolTy
          EqCharP -> BoolTy
          LtP  -> BoolTy
          GtP  -> BoolTy
          OrP  -> BoolTy
          LtEqP-> BoolTy
          GtEqP-> BoolTy
          FLtP  -> BoolTy
          FGtP  -> BoolTy
          FLtEqP-> BoolTy
          FGtEqP-> BoolTy
          AndP -> BoolTy
          MkTrue  -> BoolTy
          MkFalse -> BoolTy
          Gensym  -> SymTy0
          SizeParam      -> IntTy
          IsBig          -> BoolTy
          DictHasKeyP _  -> BoolTy
          DictEmptyP ty  -> SymDictTy Nothing ty
          DictInsertP ty -> SymDictTy Nothing ty
          DictLookupP ty -> ty
          VAllocP elty   -> VectorTy elty
          VFreeP _elty   -> ProdTy []
          VFree2P _elty  -> ProdTy []
          VLengthP _elty -> IntTy
          VNthP elty     -> elty
          VSliceP elty   -> VectorTy elty
          InplaceVUpdateP elty -> VectorTy elty
          VConcatP elty  -> VectorTy elty
          VSortP elty        -> VectorTy elty
          InplaceVSortP elty -> VectorTy elty
          VMergeP elty -> VectorTy elty
          PDictInsertP kty vty -> PDictTy kty vty
          PDictLookupP _kty vty -> vty
          PDictAllocP kty vty -> PDictTy kty vty
          PDictHasKeyP _kty _vty -> BoolTy
          PDictForkP kty vty -> ProdTy [PDictTy kty vty, PDictTy kty vty]
          PDictJoinP kty vty -> PDictTy kty vty
          LLAllocP elty -> ListTy elty
          LLIsEmptyP _elty -> BoolTy
          LLConsP elty  -> ListTy elty
          LLHeadP elty  -> elty
          LLTailP elty  -> ListTy elty
          LLFreeP _elty   -> ProdTy []
          LLFree2P _elty  -> ProdTy []
          LLCopyP elty -> ListTy elty
          GetNumProcessors -> IntTy
          (ErrorP _ ty)  -> ty
          ReadPackedFile _ _ _ ty -> ty
          WritePackedFile{} -> ProdTy []
          ReadArrayFile _ ty      -> ty
          PrintInt     -> ProdTy []
          PrintChar    -> ProdTy []
          PrintFloat   -> ProdTy []
          PrintBool    -> ProdTy []
          PrintSym     -> ProdTy []
          ReadInt      -> IntTy
          RequestSizeOf-> error "primRetTy1: RequestSizeOf not handled yet"
          RequestEndOf -> error "primRetTy1: RequestEndOf not handled yet"
          SymSetEmpty  -> error "primRetTy1: SymSetEmpty not handled yet"
          SymSetContains-> error "primRetTy1: SymSetContains not handled yet"
          SymSetInsert -> error "primRetTy1: SymSetInsert not handled yet"
          SymHashEmpty -> error "primRetTy1: SymHashEmpty not handled yet"
          SymHashInsert-> error "primRetTy1: SymHashInsert not handled yet"
          SymHashLookup-> error "primRetTy1: SymHashLookup not handled yet"
          SymHashContains-> error "primRetTy1: SymHashLookup not handled yet"
          IntHashEmpty -> error "primRetTy1: IntHashEmpty not handled yet"
          IntHashInsert-> error "primRetTy1: IntHashInsert not handled yet"
          IntHashLookup-> error "primRetTy1: IntHashLookup not handled yet"
          Write3dPpmFile{}-> error "primRetTy1: Write3dPpmFile not handled yet"
  
  
  {-
  
  -- | Variable definitions
  
  -- ^ Monomorphic version
  data VarDef a ex = VarDef { varName :: Var
                            , varTy   :: a
                            , varBody :: ex }
    deriving (Show, Eq, Ord, Generic, NFData)
  
  type VarDefs a ex = M.Map Var (VarDef a ex)
  
  type FunDefs0 = M.Map Var FunDef0
  
  type FunDef0 = FunDef (L Exp0)
  
  instance FunctionTy Ty0 where
    type ArrowTy Ty0 = (Ty0 , Ty0)
    inTy = fst
    outTy = snd
  
  -- ^ Polymorphic version
  
  data PVDef a ex = PVDef { vName :: Var
                          , vTy   :: Scheme a
                          , vBody :: ex }
    deriving (Show, Read, Eq, Ord, Generic, NFData)
  
  type PVDefs a ex = M.Map Var (PVDef a ex)
  
  -- | for now, using a specialized DDef for L0
  -- this enables the DDefs to have type variables
  type PDDefs a = M.Map Var (PDDef a)
  
  data PDDef a = PDDef { dName :: Var
                       , dCons :: [(DataCon,[(IsBoxed,Scheme a)])] } -- ^ Polymorphic data constructors
    deriving (Read,Show,Eq,Ord, Generic)
  
  
  -- | for now, using a specialized FunDef for L0
  -- theoretically these should disappear after monomorphization
  -- this enables the FunDefs to have type schemes
  type PFDefs a ex = M.Map Var (PFDef a ex)
  
  data PFDef a ex  = PFDef { fName :: Var
                           , fArg  :: Var
                           , fTy   :: Scheme a -- ^ the type will be a ForAll
                           , fBody :: ex }
    deriving (Read,Show,Eq,Ord, Functor, Generic)
  
  -- ^ Polymorphic program
  data PProg = PProg { pddefs    :: PDDefs Ty0
                     , pfundefs  :: PFDefs Ty0 (L Exp0)
                     , pvardefs  :: PVDefs Ty0 (L Exp0)
                     , pmainExp  :: Maybe (L Exp0)
                     }
    deriving (Show, Eq, Ord, Generic)
  
  -- ^ Monomorphic program
  data MProg = MProg { ddefs    :: DDefs Ty0
                     , fundefs  :: FunDefs0
                     , vardefs  :: VarDefs Ty0 (L Exp0)
                     , mainExp  :: Maybe (L Exp0)
                     }
    deriving (Show, Eq, Ord, Generic)
  
  -- | some type defns to make things look cleaner
  type Exp = (L Exp0)
  
  -- | we now have curried functions and curried calls
  -- curried functions are these variable defns
  -- but curried calls vs function calls are PolyAppE vs AppE
  type CurFun  = VarDef Ty0 Exp
  type CCall = Exp
  
  -- | Monomorphized functions
  type L0Fun = FunDef0
  type FCall = Exp
  
  arrIn :: Ty0 -> Ty0
  arrIn (ArrowTy i _) = i
  arrIn err = error $ "arrIn: Not an arrow type: " ++ show err
  
  arrOut :: Ty0 -> Ty0
  arrOut (ArrowTy _ o) = o
  arrOut err = error $ "arrOut: Not an arrow type: " ++ show err
  
  typeFromScheme :: Scheme a -> a
  typeFromScheme (ForAll _ a) = a
  
  initFunEnv :: PFDefs Ty0 Exp -> FunEnv Ty0
  initFunEnv fds = M.foldr (\fn acc -> let fnTy = typeFromScheme (fTy fn)
                                           fntyin  = arrIn fnTy
                                           fntyout = arrOut fnTy
                                       in M.insert (fName fn) (fntyin, fntyout) acc)
                   M.empty fds
  
  initVarEnv :: PVDefs Ty0 Exp -> M.Map Var Ty0
  initVarEnv vds = M.foldr (\v acc -> M.insert (vName v) (typeFromScheme (vTy v)) acc)
                   M.empty vds
  -}
  