{-# LANGUAGE TupleSections, NamedFieldPuns #-}

module Extract where

{- extract to Fomega

Examples:
---------

MiniAgda

  data Vec (A : Set) : Nat -> Set
  { vnil  : Vec A zero
  ; vcons : [n : Nat] -> (head : A) -> (tail : Vec A n) -> Vec A (suc n)
  } fields head, tail

  fun length : [A : Set] -> [n : Nat] -> Vec A n -> <n : Nat>
  { length .A .zero    (vnil A)         = zero
  ; length .A .(suc n) (vcons A n a as) = suc (length A n as)
  }

Fomega

  data Vec (A : Set) : Set
  { vnil  : Vec A
  ; vcons : (head : A) -> (tail : Vec A) -> Vec A
  }

  fun head : [A : Set] -> Vec A -> A
  { head (vcons 'head 'tail) = 'head
  }

  fun tail : [A : Set] -> Vec A -> A
  { head (vcons 'head 'tail) = 'tail
  }

  fun length : [A : Set] -> Vec A -> Nat
  { length [A]  vnil             = zero
  ; length [A] (vcons [.A] a as) = suc (length [A] as)
  }


Bidirectional extraction
========================

Types

  Base ::= D As         data type
         | ?            inexpressible type

  A,B ::= Base | A -> B | [x:K] -> B | [] -> B  with erasure markers
  A0, B0 ::= Base | A0 -> B0 | [x:K0] -> B0     without erasure markers

  |.| erase erasure markers

Inference mode:

  Term extraction:  Gamma |- t :> A  --> e    |Gamma| |- e : |A|
  Type extraction:  Gamma |- T :> K  --> A    |Gamma| |- A : |K|
  Kind extraction:  Gamma |- U :> [] --> K    |Gamma| |- K : []

Checking mode:

  Term extraction:  Gamma |- t <: A  --> e    |Gamma| |- e : |A|
  Type extraction:  Gamma |- T <: K  --> A    |Gamma| |- A : |K|
  Kind extraction:  Gamma |- U <: [] --> K    |Gamma| |- K : []

Type and kind extraction keep erasure markers!

Checking abstraction:

  Relevant abstraction:
  Gamma, x:A |- t <: B --> e
  --------------------------------
  Gamma |- \x.t <: A -> B --> \x.e

  Type abstraction:
  Gamma, x:K |- t <: B --> e : B0
  ----------------------------------------
  Gamma |- \[x].t <: [x:K] -> B --> \[x].e
      also \xt

  Irrelevant abstraction:
  Gamma |- t : B --> e
  -------------------------------
  Gamma |- \[x].t : [] -> B --> e
      also \xt

  Relevant abstraction at unknown type:
  Gamma, x:? |- t : ? --> e
  --------------------------
  Gamma |- \x.t : ? --> \x.e

  Irrelevant abstraction at unknown type:
  Gamma |- t : ? --> e
  -------------------------
  Gamma |- \[x].t : ? --> e

Checking by inference:

  Gamma |- t :> A --> e    e : |A| <: |B| --> e'
  ----------------------------------------------
  Gamma |- t <: B --> e' : B0

Casting:

  ------------------ A0 does not contain ?
  e : A0 <: A0 --> e

  ----------------------- A0 != B0 or one does contain ?
  e : A0 <: B0 --> cast e

Inferring variable:

  ----------------------------
  Gamma |- x :> Gamma(x) --> x

Inferring application:

  Relevant application:
  Gamma |- t :> A -> B --> f     Gamma |- u <: A --> e
  ----------------------------------------------------
  Gamma |- t u :> B --> f e

  Type application:
  Gamma |- t :> [x:K] -> B --> f   Gamma |- u <: K --> A
  ------------------------------------------------------
  Gamma |- t [u] :> : B[A/x] --> f [A]
      also  t u

  Irrelevant application:
  Gamma |- t :> [] -> B --> f
  ---------------------------
  Gamma |- t [u] :> B --> f
      also  t u

  Relevant application at unknown type:
  Gamma |- t :> ? --> f     Gamma |- u <: ? --> e
  -----------------------------------------------
  Gamma |- t u :> ? --> f e

  Irrelevant application at unknown type:
  Gamma |- t :> ? --> f
  -------------------------
  Gamma |- t [u] :> ? --> f



-}

import Prelude hiding (pi, null)

import Control.Applicative
import Control.Monad
import Control.Monad.Error
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State

import Data.Char
import Data.Traversable (Traversable)
import qualified Data.Traversable as Traversable
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe

import Text.PrettyPrint

import Polarity as Pol
import Abstract
import Value
import Eval
import TCM
import TraceError
import Util

traceExtrM s = return ()

runExtract sig k = runErrorT (runReaderT (runStateT k (initWithSig sig)) emptyContext)

-- extraction

type FExpr        = Expr
type FDeclaration = Declaration
type FClause      = Clause
type FPattern     = Pattern
type FConstructor = Constructor
type FTypeSig     = TypeSig
type FFun         = Fun
type FTelescope   = Telescope

type FTVal        = TVal

extractDecls :: [EDeclaration] -> TypeCheck [FDeclaration]
extractDecls ds = concat <$> mapM extractDecl ds

extractDecl :: EDeclaration -> TypeCheck [FDeclaration]
extractDecl d =
  case d of
    MutualDecl _ ds -> extractDecls ds -- TODO!
    OverrideDecl{} -> fail $ "extractDecls internal error: overrides impossible"
    MutualFunDecl _ co funs -> extractFuns co funs
    FunDecl co fun -> extractFun co fun
    LetDecl evl x tel (Just t) e | null tel -> extractLet evl x t e
    PatternDecl{}    -> return []
    DataDecl n _ co _ tel ty cs fields -> extractDataDecl n co tel ty cs

extractFuns :: Co -> [Fun] -> TypeCheck [FDeclaration]
extractFuns co funs = do
  funs <- concat <$> mapM extractFunTypeSig funs
  concat <$> mapM (extractFun co) funs

extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
extractFun co (Fun (TypeSig n t) n' ar cls) = do
  tv <- whnf' t
  cls <- concat <$> mapM (extractClause n tv) cls
  return [ FunDecl co $ Fun (TypeSig n t) n' ar cls
         -- , LetDecl False (TypeSig n' t) (Var n)  -- no longer needed, since n and n' print the same
         ]

{- OLD
extractFun :: Co -> Fun -> TypeCheck [FDeclaration]
extractFun co (TypeSig n t, (ar, cls)) = extractIfTerm n $ do
  tv0 <- whnf' t
  t <- extractType tv0
  setExtrTyp n t
  let n' = mkExtName n
  setExtrTyp n' t
  tv <- whnf' t
  cls <- concat <$> mapM (extractClause n tv) cls
  return [ FunDecl co (TypeSig n t, (ar, cls))
         , LetDecl False (TypeSig n' t) (Var n)
         ]
-}
{-
extractFunTypeSigs :: [Fun] -> TypeCheck [Fun]
extractFunTypeSigs = mapM extractFunTypeSig
-}

-- only extract type sigs
extractFunTypeSig :: Fun -> TypeCheck [Fun]
extractFunTypeSig (Fun ts@(TypeSig n t) n' ar cls) = extractIfTerm n $ do
  ts@(TypeSig n t) <- extractTypeSig ts
  setExtrTyp n' t
  return [Fun ts n' ar cls]

extractLet :: Bool -> Name -> Type -> Expr -> TypeCheck [FDeclaration]
extractLet evl n t e = extractIfTerm n $ do
  TypeSig n t <- extractTypeSig (TypeSig n t)
  e <- extractCheck e =<< whnf' t
  return [LetDecl evl n emptyTel (Just t) e]

extractTypeSig :: TypeSig -> TypeCheck FTypeSig
extractTypeSig (TypeSig n t) = do
  t <- extractType =<< whnf' t
  setExtrTyp n t
  return $ TypeSig n t

extractIfTerm :: Name -> TypeCheck [a] -> TypeCheck [a]
extractIfTerm n cont = do
  k <- symbolKind <$> lookupSymb n
  if k == NoKind || lowerKind k == SortC Tm then cont else return []

extractDataDecl :: Name -> Co -> Telescope -> Type -> [Constructor] -> TypeCheck [FDeclaration]
extractDataDecl n co tel ty cs = do
  -- k    <- extrTyp <$> lookupSymb n
  tel' <- extractKindTel tel
  Just core <- addBinds tel $ extractKind =<< whnf' ty
  -- (_, core) = typeToTele' (length tel') k
  cs   <- mapM (extractConstructor tel) cs
  return [DataDecl n NotSized co [] tel' core cs []]

extractConstructor :: Telescope -> Constructor -> TypeCheck FConstructor
extractConstructor tel0 (Constructor n pars t) = do
{- fails for HEq
  -- 2012-01-22: remove irrelevant parameters
  let tel = filter (\ (TBind _ dom) -> not $ erased $ decor dom)  tel0
-}
  let tel = tel0
  -- compute full extracted constructor type and add to the signature
  t' <- extractType =<< whnf emptyEnv (teleToTypeErase tel t)
  setExtrTypQ n t'
  let (tel',core) = typeToTele' (size tel) t'
  return $ Constructor n pars core
  -- compute type minus telescope
  -- TypeSig n <$> (extractType =<< whnf' t)

extractClause :: Name -> FTVal -> Clause -> TypeCheck [FClause]
extractClause f tv (Clause _ pl Nothing) = return [] -- discard absurd clauses
extractClause f tv cl@(Clause vtel pl (Just rhs)) = do
  traceM ("extracting clause " ++ render (prettyClause f cl)
          ++ "\n at type " ++ show tv)
{-
  tel <- introPatterns pl tv0 $ \ _ _ -> do
           vtel <- getContextTele
           extractTeleVal vtel
  addBinds tel $
-}
  introPatVars pl $
    extractPatterns tv pl $ \ pl tv -> do
      rhs <- extractCheck rhs tv
      return [Clause vtel pl (Just rhs)] -- TODO: return FTelescope (type!)

-- the pattern variables are already in context
extractPatterns :: FTVal -> [Pattern] ->
                   ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
extractPatterns tv [] cont = cont [] tv
extractPatterns tv (p:ps) cont =
  extractPattern tv p $ \ pl tv ->
    extractPatterns tv ps $ \ ps tv ->
      cont (pl ++ ps) tv

extractPattern :: FTVal -> Pattern ->
                  ([FPattern] -> FTVal -> TypeCheck a) -> TypeCheck a
extractPattern tv p cont = do
  traceM ("extracting pattern " ++ render (pretty p) ++ " at type " ++ show tv)
  fv <- funView tv
  case fv of
    EraseArg tv -> cont [] tv  -- skip erased patterns

    Forall x dom fv -> do
      xv <- whnf' (patternToExpr p) -- pattern variables are already in scope
      bv <- app fv xv -- TODO!
      case p of
        ErasedP (VarP y) -> setTypeOfName y dom $ cont [] bv
        _ -> cont [] bv
{-
    Forall x ki env t -> new x ki $ \ xv ->
      cont [] =<< whnf (update env x xv) t -- TODO!
-}
    Arrow av bv -> extractPattern' av p (flip cont bv)

extractPattern' :: FTVal -> Pattern ->
                  ([FPattern] -> TypeCheck a) -> TypeCheck a
extractPattern' av p cont =
      case p of
        VarP y -> setTypeOfName y (defaultDomain av) $
          cont [VarP y]
        PairP p1 p2 -> do
          view <- prodView av
          -- hack to avoid IMPOSSIBLE
          let (av1, av2) = case view of
                             Prod av1 av2 -> (av1, av2)
                             _ -> (av, av) -- HACK
          extractPattern' av1 p1 $ \ ps1 -> do
            extractPattern' av2 p2 $ \ ps2 ->
               let ps [] ps2    = ps2
                   ps ps1 []    = ps1
                   ps [p1] [p2] = [PairP p1 p2]
               in  cont $ ps ps1 ps2

{-
          case view of
            Prod av1 av2 ->
              extractPattern' av1 p1 $ \ [p1] -> do
                extractPattern' av2 p2 $ \ [p2] -> cont [PairP p1 p2]
            _ -> fail $ "extractPattern': IMPOSSIBLE: pattern " ++
                          show p ++ " : " ++ show av
-}
        ConP pi n ps -> do
--          tv <- whnf' =<< extrTyp <$> lookupSymb n
          tv <- extrConType n av
          extractPatterns tv ps $ \ ps _ ->
            cont [ConP pi n ps]
        _ -> cont []

extrConType :: QName -> FTVal -> TypeCheck FTVal
extrConType c av = do
  ConSig { conPars, extrTyp, dataPars } <- lookupSymbQ c
  traceExtrM ("extrConType " ++ show c ++ " has extrTyp = " ++ show extrTyp)
  tv <- whnf' extrTyp
  numPars <- maybe (return dataPars) (const $ fail $ "NYI: extrConType for pattern parameters") conPars
  case numPars of
   0 -> return tv
   _ -> do
    case av of
      VApp (VDef (DefId DatK d)) vs -> do
        DataSig { positivity } <- lookupSymbQ d
        traceExtrM ("extrConType " ++ show c ++ "; data type has positivity = " ++ show positivity)
        let pars 0 pols vs = []
            pars n (pol:pols) vs | erased pol = VIrr : pars (n-1) pols vs
            pars n (pol:pols) (v:vs) = v : pars (n-1) pols vs
            pars n pols vs = error $ "pars " ++ show n ++ show pols ++ show vs
        piApps tv $ pars numPars positivity $ vs ++ repeat VIrr
{-
        let (pars, inds) = splitAt numPars vs
        piApps tv pars
-}
      _ -> piApps tv $ replicate numPars VIrr
--      _ -> fail $ "extrConType " ++ show c ++ ": expected datatype, found " ++ show av

-- extracting a term from a term -------------------------------------

extractInfer :: Expr -> TypeCheck (FExpr, FTVal)
extractInfer e = do
  case e of

    Var x -> (Var x,) . typ . domain <$> lookupName1 x

    App f e0 -> do
      let (er, e) = isErasedExpr e0
      (f, tv) <- extractInfer f
      fv <- funView tv
      case fv of
        EraseArg bv -> return (f,bv)
        Forall x dom fv -> do
          e <- extractTypeAt e (typ dom)
          bv <- app fv =<< whnf' e
          return $ (App f (erasedExpr e), bv)
        Arrow av bv -> return (if er then f else App f e, bv)
        NotFun -> return (if er then f else castExpr f `App` e, VIrr)

    Def f -> (Def f,) <$> do (whnf' . extrTyp) =<< lookupSymbQ (idName f)

    Pair{} -> fail $ "extractInfer: IMPOSSIBLE: pair " ++ show e
    -- other expressions are erased or types

    _ -> return (Irr, VIrr)

extractCheck :: Expr -> FTVal -> TypeCheck (FExpr)
extractCheck e tv = do
  case e of
    Lam dec y e -> do
      fv <- funView tv
      case fv of
        EraseArg bv        -> extractCheck e bv -- discard lambda
        Forall x dom fv    ->
          Lam (decor dom) y <$> do
            newWithGen y dom $ \ i xv ->
              extractCheck e =<< app fv (VGen i) -- no eta-expansion
        Arrow av bv        ->
          if erased dec then extractCheck e bv
           else Lam dec y <$> do
             new' y (defaultDomain av) $
               extractCheck e bv
        NotFun            -> castExpr <$>
          if erased dec then extractCheck e VIrr
           else Lam dec y <$> do
             new' y (defaultDomain VIrr) $
               extractCheck e VIrr

    LLet (TBind x dom0) tel e1 e2 | null tel -> do
      let dom = fmap Maybe.fromJust dom0
      if erased (decor dom) then extractCheck e2 tv else do -- discard let
       vdom <- Traversable.mapM whnf' dom         -- MiniAgda type val
       dom  <- Traversable.mapM extractType vdom  -- Fomega type
       vdom <- Traversable.mapM whnf' dom         -- Fomega type val
       e1  <- extractCheck e1 (typ vdom)
       LLet (TBind x (fmap Just dom)) emptyTel e1 <$> do
         new' x vdom $ extractCheck e2 tv

    Pair e1 e2 -> do
      view <- prodView tv
      let (av1,av2) = case view of
                        Prod av1 av2 -> (av1, av2)
                        _ -> (tv,tv) -- HACK!!
      Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
{-
      case view of
        Prod av1 av2 -> Pair <$> extractCheck e1 av1 <*> extractCheck e2 av2
        _ -> fail $ "extractCheck: tuple type expected " ++ show e ++ " : " ++ show tv
-}

    -- TODO: case

    _ -> fallback
  where
    fallback = do
      (e,tv') <- extractInfer e
      insertCast e tv tv'

insertCast :: FExpr -> FTVal -> FTVal -> TypeCheck FExpr
insertCast e tv1 tv2 = loop tv1 tv2 where
  loop tv1 tv2 =
    case (tv1,tv2) of
      (VIrr,_) -> return $ castExpr e
      (_,VIrr) -> return $ castExpr e
      _  -> return e -- TODO!

funView :: FTVal -> TypeCheck FunView
funView tv =
  case tv of
    -- erasure mark
    VQuant Pi x dom fv | erased (decor dom) && typ dom == VIrr ->
      EraseArg <$> app fv VIrr
    -- forall
    VQuant Pi x dom fv | erased (decor dom) ->
      return $ Forall x dom fv
    -- function type
    VQuant Pi x dom fv ->
      Arrow (typ dom) <$> app fv VIrr
    -- any other type can be a function type, but this needs casts!
    _ -> return NotFun -- $ Arrow VIrr VIrr

data FunView
  = Arrow    FTVal FTVal            -- A -> B
  | Forall   Name Domain FTVal      -- forall X:K. A
  | EraseArg FTVal                  -- [] -> B
  | NotFun                          -- ()

prodView :: FTVal -> TypeCheck ProdView
prodView tv =
  case tv of
    VQuant Sigma x dom fv -> Prod (typ dom) <$> app fv VIrr
    _                     -> return $ NotProd

data ProdView
  = Prod FTVal FTVal -- A * B
  | NotProd

-- extracting a kind from a value ------------------------------------

type FKind = Expr -- FKind ::= Set | FKind -> FKind | [Irr] -> FKind

star :: FKind
star = Sort $ Set Zero

extractSet :: Sort Val -> Maybe FKind
extractSet s =
  case s of
    SortC _ -> Nothing
    Set _   -> Just $ star
    CoSet _ -> Just $ star

-- keep irrelevant entries
extractKindTel :: Telescope -> TypeCheck FTelescope
extractKindTel (Telescope tel) = Telescope <$> loop tel where
  loop [] = return []
  loop (TBind x dom : tel) = do
    dom  <- Traversable.mapM whnf' dom
    dom' <- extractKindDom dom
    if erased (decor dom') then
      newIrr x $
        (TBind x dom' :) <$> loop tel
     else newTyVar x (typ dom') $ \ i -> do
        x <- nameOfGen i
        (TBind x dom' :) <$> loop tel

{-
-- keep irrelevant entries
extractKindTel :: Telescope -> TypeCheck FTelescope
extractKindTel tel = do
  tv     <- whnf' (teleToType tel star)
  Just k <- extractKind tv
  let (tel, s) = typeToTele k
  return tel
  -- throw away erasure marks
  -- return $ filter (\ tb -> not $ erased $ decor $ boundDom tb) tel
-}

extractKindDom :: Domain -> TypeCheck (Dom FKind)
extractKindDom dom =
  maybe (defaultIrrDom Irr) defaultDomain <$>
    if erased (decor dom) then return Nothing
     else extractKind (typ dom)

extractKind :: TVal -> TypeCheck (Maybe FKind)
extractKind tv =
  case tv of
    VSort s -> return $ extractSet s
    VMeasured mu vb -> extractKind vb
    VGuard beta vb -> extractKind vb
    VQuant Pi x dom fv -> new' x dom $ do
       bv  <- app fv VIrr
       mk' <- extractKind bv
       case mk' of
         Nothing -> return Nothing
         Just k' -> do
           dom' <- extractKindDom dom
           let x = fresh ""
           return $ Just $ pi (TBind x dom') k'
    _ -> return Nothing

-- extracting a type constructor from a value ------------------------

type FType = Expr
{- FType ::= Irr                 -- not expressible in Fomega
           | D FTypes            -- data type
           | X FTypes            -- type variable
           | FType -> FType      -- function type
           | [X:FKind] -> FType  -- polymorphic type
           | [Irr] -> FType      -- erasure marker
 -}

-- tyVarName i = fresh $ "a" ++ show i

newTyVar :: Name -> FKind -> (Int -> TypeCheck a) -> TypeCheck a
newTyVar x k cont = newWithGen x (defaultDomain (VClos emptyEnv k)) $
  \ i _ -> cont i                  -- store kinds unevaluated

addFKindTel :: FTelescope -> TypeCheck a -> TypeCheck a
addFKindTel (Telescope tel) = loop tel where
  loop []                  cont = cont
  loop (TBind x dom : tel) cont = newTyVar x (typ dom) $ \ _ ->
    loop tel cont

extractTeleVal :: TeleVal -> TypeCheck FTelescope
extractTeleVal = Telescope <.> loop where
  loop []          = return []
  loop (tb : vtel) = do
    tb <- Traversable.mapM extractType tb
    addBind tb $ do
      (tb :) <$> loop vtel

extractType :: TVal -> TypeCheck FType
extractType = extractTypeAt star

extractTypeAt :: FKind -> TVal -> TypeCheck FType
extractTypeAt k tv = do
  case (tv,k) of

    (VMeasured mu vb, _) -> extractTypeAt k vb
    (VGuard beta vb, _) -> extractTypeAt k vb

    -- relevant function space / sigma type --> non-dependent
    (VQuant pisig x dom fv, _) | not (erased (decor dom)) -> do
      a <- extractType (typ dom)
      -- new' x dom $ do
      bv <- app fv VIrr
      b  <- extractType bv
      let x = fresh ""
      return $ piSig pisig (TBind x (defaultDomain a)) b

    -- irrelevant function space --> forall or erasure marker
    (VQuant Pi x dom fv, _) | erased (decor dom) -> do
      mk <- extractKind (typ dom)
      case mk of
        Nothing -> do -- new' x dom $ do
          bv <- app fv VIrr
          b  <- extractType bv
          let x = fresh ""
          return $ pi (TBind x (defaultIrrDom Irr)) b
        Just k' -> do
          newTyVar x k' $ \ i -> do
            bv <- app fv $ VGen i
            b  <- extractType bv
            x  <- nameOfGen i
            return $ pi (TBind x (defaultIrrDom k')) b

    (VApp (VDef (DefId DatK n)) vs, _) -> do
      k  <- extrTyp <$> lookupSymbQ n  -- get kind of dname from signature
      as <- extractTypes k vs  -- turn vs into types as at kind k
      return $ foldl App (Def (DefId DatK n)) as

    (VGen i,_) -> do
--      VClos _ k <- (typ . fromOne . domain) <$> lookupGen i  -- get kind of var from cxt
      Var <$> nameOfGen i
      -- return $ Var (tyVarName i)

    (VApp (VGen i) vs,_) -> do
      VClos _ k <- (typ . fromOne . domain) <$> lookupGen i  -- get kind of var from cxt
      as <- extractTypes k vs  -- turn vs into types as at kind k
      x <- nameOfGen i
      return $ foldl App (Var x) as

    (VLam x env e, Quant Pi (TBind _ dom) k) | erased (decor dom) -> do
      tv <- whnf (update env x VIrr) e
      extractTypeAt k tv

    (VLam x env e, Quant Pi (TBind _ dom) k) -> newTyVar x (typ dom) $ \ i -> do
      tv <- whnf (update env x (VGen i)) e
      x  <- nameOfGen i
      Lam defaultDec x <$> extractTypeAt k tv

    (VLam{},_) -> error $ "panic! extractTypeAt " ++ show (tv,k)

    (VSing _ tv,_) -> extractTypeAt k tv

    (VUp v _,_)    -> extractTypeAt k v

    _ -> return Irr

extractTypes :: FKind -> [TVal] -> TypeCheck [FType]
extractTypes k vs =
  case (k,vs) of
    (_, []) -> return []
    (Quant Pi (TBind _ dom) k, v:vs) | erased (decor dom) -> extractTypes k vs
    (Quant Pi (TBind _ dom) k, v:vs) -> do
      v  <- whnfClos v
      a  <- extractTypeAt (typ dom) v
      as <- extractTypes k vs
      return $ a : as
    _ -> error $ "panic! extractTypes  " ++ show k ++ "  " ++ show vs

-- auxiliary functions -----------------------------------------------

{- this is setExtrTyp
addFTypeSig :: Name -> FType -> TypeCheck ()
addFTypeSig n t = modifySig n (\ item -> item { extrTyp = t })
-}