-- |
-- Module      :  Cryptol.TypeCheck.InferTypes
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- This module contains types used during type inference.

{-# LANGUAGE Safe #-}

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.InferTypes where

import           Control.Monad(guard)

import           Cryptol.Parser.Position
import           Cryptol.ModuleSystem.Name (asPrim,nameLoc,nameIdent)
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.PP
import           Cryptol.TypeCheck.Subst
import           Cryptol.TypeCheck.TypePat
import           Cryptol.TypeCheck.SimpType(tMax)
import           Cryptol.Utils.Ident (PrimIdent(..), preludeName)
import           Cryptol.Utils.Panic(panic)
import           Cryptol.Utils.Misc(anyJust)

import           Data.List(mapAccumL,partition)
import           Data.Maybe(mapMaybe)
import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap

import GHC.Generics (Generic)
import Control.DeepSeq

data SolverConfig = SolverConfig
  { SolverConfig -> FilePath
solverPath    :: FilePath   -- ^ The SMT solver to invoke
  , SolverConfig -> [FilePath]
solverArgs    :: [String]   -- ^ Additional arguments to pass to the solver
  , SolverConfig -> Int
solverVerbose :: Int        -- ^ How verbose to be when type-checking
  , SolverConfig -> [FilePath]
solverPreludePath :: [FilePath]
    -- ^ Look for the solver prelude in these locations.
  , SolverConfig -> Maybe FilePath
solverSmtFile :: Maybe FilePath
    -- ^ The optional file to record SMT solver interactions in the type
    -- checker. If 'Nothing', this will print to @stdout@ instead.
  } deriving (Int -> SolverConfig -> ShowS
[SolverConfig] -> ShowS
SolverConfig -> FilePath
(Int -> SolverConfig -> ShowS)
-> (SolverConfig -> FilePath)
-> ([SolverConfig] -> ShowS)
-> Show SolverConfig
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SolverConfig -> ShowS
showsPrec :: Int -> SolverConfig -> ShowS
$cshow :: SolverConfig -> FilePath
show :: SolverConfig -> FilePath
$cshowList :: [SolverConfig] -> ShowS
showList :: [SolverConfig] -> ShowS
Show, (forall x. SolverConfig -> Rep SolverConfig x)
-> (forall x. Rep SolverConfig x -> SolverConfig)
-> Generic SolverConfig
forall x. Rep SolverConfig x -> SolverConfig
forall x. SolverConfig -> Rep SolverConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SolverConfig -> Rep SolverConfig x
from :: forall x. SolverConfig -> Rep SolverConfig x
$cto :: forall x. Rep SolverConfig x -> SolverConfig
to :: forall x. Rep SolverConfig x -> SolverConfig
Generic, SolverConfig -> ()
(SolverConfig -> ()) -> NFData SolverConfig
forall a. (a -> ()) -> NFData a
$crnf :: SolverConfig -> ()
rnf :: SolverConfig -> ()
NFData)


-- | A default configuration for using Z3, where
--   the solver prelude is expected to be found
--   in the given search path.
defaultSolverConfig :: [FilePath] -> SolverConfig
defaultSolverConfig :: [FilePath] -> SolverConfig
defaultSolverConfig [FilePath]
searchPath =
  SolverConfig
  { solverPath :: FilePath
solverPath = FilePath
"z3"
  , solverArgs :: [FilePath]
solverArgs = [ FilePath
"-smt2", FilePath
"-in" ]
  , solverVerbose :: Int
solverVerbose = Int
0
  , solverPreludePath :: [FilePath]
solverPreludePath = [FilePath]
searchPath
  , solverSmtFile :: Maybe FilePath
solverSmtFile = Maybe FilePath
forall a. Maybe a
Nothing
  }

-- | The types of variables in the environment.
data VarType = ExtVar Schema
               -- ^ Known type

             | CurSCC {- LAZY -} Expr Type
               {- ^ Part of current SCC.  The expression will replace the
               variable, after we are done with the SCC.  In this way a
               variable that gets generalized is replaced with an appropriate
               instantiation of itself. -}

data Goals = Goals
  { Goals -> Set Goal
goalSet :: Set Goal
    -- ^ A bunch of goals, not including the ones in 'literalGoals'.

  , Goals -> Set Prop
saturatedPropSet :: Set Prop
    -- ^ The set of nonliteral goals, saturated by all superclass implications

  , Goals -> Map TVar Goal
literalGoals :: Map TVar LitGoal
    -- ^ An entry @(a,t)@ corresponds to @Literal t a@.

  , Goals -> Map TVar Goal
literalLessThanGoals :: Map TVar LitGoal
    -- ^ An entry @(a,t)@ corresponds to @LiteralLessThan t a@.

  } deriving (Int -> Goals -> ShowS
[Goals] -> ShowS
Goals -> FilePath
(Int -> Goals -> ShowS)
-> (Goals -> FilePath) -> ([Goals] -> ShowS) -> Show Goals
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Goals -> ShowS
showsPrec :: Int -> Goals -> ShowS
$cshow :: Goals -> FilePath
show :: Goals -> FilePath
$cshowList :: [Goals] -> ShowS
showList :: [Goals] -> ShowS
Show)

-- | This abuses the type 'Goal' a bit. The 'goal' field contains
-- only the numeric part of the Literal constraint.  For example,
-- @(a, Goal { goal = t })@ representats the goal for @Literal t a@
type LitGoal = Goal

litGoalToGoal :: (TVar,LitGoal) -> Goal
litGoalToGoal :: (TVar, Goal) -> Goal
litGoalToGoal (TVar
a,Goal
g) = Goal
g { goal = pLiteral (goal g) (TVar a) }

goalToLitGoal :: Goal -> Maybe (TVar,LitGoal)
goalToLitGoal :: Goal -> Maybe (TVar, Goal)
goalToLitGoal Goal
g =
  do (Prop
tn,TVar
a) <- Match (Prop, TVar) -> Maybe (Prop, TVar)
forall a. Match a -> Maybe a
matchMaybe (Match (Prop, TVar) -> Maybe (Prop, TVar))
-> Match (Prop, TVar) -> Maybe (Prop, TVar)
forall a b. (a -> b) -> a -> b
$ do (Prop
tn,Prop
b) <- Pat Prop (Prop, Prop)
aLiteral (Goal -> Prop
goal Goal
g)
                               TVar
a      <- Pat Prop TVar
aTVar Prop
b
                               (Prop, TVar) -> Match (Prop, TVar)
forall a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
     (TVar, Goal) -> Maybe (TVar, Goal)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal = tn })


litLessThanGoalToGoal :: (TVar,LitGoal) -> Goal
litLessThanGoalToGoal :: (TVar, Goal) -> Goal
litLessThanGoalToGoal (TVar
a,Goal
g) = Goal
g { goal = pLiteralLessThan (goal g) (TVar a) }

goalToLitLessThanGoal :: Goal -> Maybe (TVar,LitGoal)
goalToLitLessThanGoal :: Goal -> Maybe (TVar, Goal)
goalToLitLessThanGoal Goal
g =
  do (Prop
tn,TVar
a) <- Match (Prop, TVar) -> Maybe (Prop, TVar)
forall a. Match a -> Maybe a
matchMaybe (Match (Prop, TVar) -> Maybe (Prop, TVar))
-> Match (Prop, TVar) -> Maybe (Prop, TVar)
forall a b. (a -> b) -> a -> b
$ do (Prop
tn,Prop
b) <- Pat Prop (Prop, Prop)
aLiteralLessThan (Goal -> Prop
goal Goal
g)
                               TVar
a      <- Pat Prop TVar
aTVar Prop
b
                               (Prop, TVar) -> Match (Prop, TVar)
forall a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop
tn,TVar
a)
     (TVar, Goal) -> Maybe (TVar, Goal)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
a, Goal
g { goal = tn })


emptyGoals :: Goals
emptyGoals :: Goals
emptyGoals  =
  Goals
  { goalSet :: Set Goal
goalSet = Set Goal
forall a. Set a
Set.empty
  , saturatedPropSet :: Set Prop
saturatedPropSet = Set Prop
forall a. Set a
Set.empty
  , literalGoals :: Map TVar Goal
literalGoals = Map TVar Goal
forall k a. Map k a
Map.empty
  , literalLessThanGoals :: Map TVar Goal
literalLessThanGoals = Map TVar Goal
forall k a. Map k a
Map.empty
  }

nullGoals :: Goals -> Bool
nullGoals :: Goals -> Bool
nullGoals Goals
gs =
  Set Goal -> Bool
forall a. Set a -> Bool
Set.null (Goals -> Set Goal
goalSet Goals
gs) Bool -> Bool -> Bool
&&
  Map TVar Goal -> Bool
forall k a. Map k a -> Bool
Map.null (Goals -> Map TVar Goal
literalGoals Goals
gs) Bool -> Bool -> Bool
&&
  Map TVar Goal -> Bool
forall k a. Map k a -> Bool
Map.null (Goals -> Map TVar Goal
literalLessThanGoals Goals
gs)

fromGoals :: Goals -> [Goal]
fromGoals :: Goals -> [Goal]
fromGoals Goals
gs = ((TVar, Goal) -> Goal) -> [(TVar, Goal)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Goal) -> Goal
litGoalToGoal (Map TVar Goal -> [(TVar, Goal)]
forall k a. Map k a -> [(k, a)]
Map.toList (Goals -> Map TVar Goal
literalGoals Goals
gs)) [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++
               ((TVar, Goal) -> Goal) -> [(TVar, Goal)] -> [Goal]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Goal) -> Goal
litLessThanGoalToGoal (Map TVar Goal -> [(TVar, Goal)]
forall k a. Map k a -> [(k, a)]
Map.toList (Goals -> Map TVar Goal
literalLessThanGoals Goals
gs)) [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++
               Set Goal -> [Goal]
forall a. Set a -> [a]
Set.toList (Goals -> Set Goal
goalSet Goals
gs)

goalsFromList :: [Goal] -> Goals
goalsFromList :: [Goal] -> Goals
goalsFromList = (Goal -> Goals -> Goals) -> Goals -> [Goal] -> Goals
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal -> Goals -> Goals
insertGoal Goals
emptyGoals

insertGoal :: Goal -> Goals -> Goals
insertGoal :: Goal -> Goals -> Goals
insertGoal Goal
g Goals
gls
  | Just (TVar
a,Goal
newG) <- Goal -> Maybe (TVar, Goal)
goalToLitGoal Goal
g =
       -- XXX: here we are arbitrarily using the info of the first goal,
       -- which could lead to a confusing location for a constraint.
       let jn :: Goal -> Goal -> Goal
jn Goal
g1 Goal
g2 = Goal
g1 { goal = tMax (goal g1) (goal g2) } in
       Goals
gls { literalGoals = Map.insertWith jn a newG (literalGoals gls)
           , saturatedPropSet = Set.insert (pFin (TVar a)) (saturatedPropSet gls)
           }

  | Just (TVar
a,Goal
newG) <- Goal -> Maybe (TVar, Goal)
goalToLitLessThanGoal Goal
g =
       let jn :: Goal -> Goal -> Goal
jn Goal
g1 Goal
g2 = Goal
g1 { goal = tMax (goal g1) (goal g2) } in
       Goals
gls { literalLessThanGoals = Map.insertWith jn a newG (literalLessThanGoals gls)
           }

  -- If the goal is already implied by some other goal, skip it
  | Prop -> Set Prop -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Goal -> Prop
goal Goal
g) (Goals -> Set Prop
saturatedPropSet Goals
gls) = Goals
gls

  -- Otherwise, it is not already implied, add it and saturate
  | Bool
otherwise =
       Goals
gls { goalSet = gs', saturatedPropSet = sps'  }

       where
       ips :: Set Prop
ips  = Prop -> Set Prop
superclassSet (Goal -> Prop
goal Goal
g)
       igs :: Set Goal
igs  = (Prop -> Goal) -> Set Prop -> Set Goal
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\Prop
p -> Goal
g{ goal = p}) Set Prop
ips

       -- remove all the goals that are implied by ips
       gs' :: Set Goal
gs'  = Goal -> Set Goal -> Set Goal
forall a. Ord a => a -> Set a -> Set a
Set.insert Goal
g (Set Goal -> Set Goal -> Set Goal
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Goals -> Set Goal
goalSet Goals
gls) Set Goal
igs)

       -- add the goal and all its implied toals to the saturated set
       sps' :: Set Prop
sps' = Prop -> Set Prop -> Set Prop
forall a. Ord a => a -> Set a -> Set a
Set.insert (Goal -> Prop
goal Goal
g) (Set Prop -> Set Prop -> Set Prop
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Goals -> Set Prop
saturatedPropSet Goals
gls) Set Prop
ips)


-- | Something that we need to find evidence for.
data Goal = Goal
  { Goal -> ConstraintSource
goalSource :: ConstraintSource  -- ^ What it is about
  , Goal -> Range
goalRange  :: Range             -- ^ Part of source code that caused goal
  , Goal -> Prop
goal       :: Prop              -- ^ What needs to be proved
  } deriving (Int -> Goal -> ShowS
[Goal] -> ShowS
Goal -> FilePath
(Int -> Goal -> ShowS)
-> (Goal -> FilePath) -> ([Goal] -> ShowS) -> Show Goal
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Goal -> ShowS
showsPrec :: Int -> Goal -> ShowS
$cshow :: Goal -> FilePath
show :: Goal -> FilePath
$cshowList :: [Goal] -> ShowS
showList :: [Goal] -> ShowS
Show, (forall x. Goal -> Rep Goal x)
-> (forall x. Rep Goal x -> Goal) -> Generic Goal
forall x. Rep Goal x -> Goal
forall x. Goal -> Rep Goal x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Goal -> Rep Goal x
from :: forall x. Goal -> Rep Goal x
$cto :: forall x. Rep Goal x -> Goal
to :: forall x. Rep Goal x -> Goal
Generic, Goal -> ()
(Goal -> ()) -> NFData Goal
forall a. (a -> ()) -> NFData a
$crnf :: Goal -> ()
rnf :: Goal -> ()
NFData)

instance Eq Goal where
  Goal
x == :: Goal -> Goal -> Bool
== Goal
y = Goal -> Prop
goal Goal
x Prop -> Prop -> Bool
forall a. Eq a => a -> a -> Bool
== Goal -> Prop
goal Goal
y

instance Ord Goal where
  compare :: Goal -> Goal -> Ordering
compare Goal
x Goal
y = Prop -> Prop -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Goal -> Prop
goal Goal
x) (Goal -> Prop
goal Goal
y)

data HasGoal = HasGoal
  { HasGoal -> Int
hasName :: !Int -- ^ This is the "name" of the constraint,
                    -- used to find the solution for ellaboration.
  , HasGoal -> Goal
hasGoal :: Goal
  } deriving Int -> HasGoal -> ShowS
[HasGoal] -> ShowS
HasGoal -> FilePath
(Int -> HasGoal -> ShowS)
-> (HasGoal -> FilePath) -> ([HasGoal] -> ShowS) -> Show HasGoal
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HasGoal -> ShowS
showsPrec :: Int -> HasGoal -> ShowS
$cshow :: HasGoal -> FilePath
show :: HasGoal -> FilePath
$cshowList :: [HasGoal] -> ShowS
showList :: [HasGoal] -> ShowS
Show


-- | A solution for a 'HasGoal'
data HasGoalSln = HasGoalSln
  { HasGoalSln -> Expr -> Expr
hasDoSelect :: Expr -> Expr
    -- ^ Select a specific field from the input expsression.

  , HasGoalSln -> Expr -> Expr -> Expr
hasDoSet    :: Expr -> Expr -> Expr
    -- ^ Set a field of the first expression to the second expression
  }


-- | Delayed implication constraints, arising from user-specified type sigs.
data DelayedCt = DelayedCt
  { DelayedCt -> Maybe Name
dctSource :: Maybe Name   -- ^ Signature that gave rise to this constraint
                              -- Nothing means module top-level
  , DelayedCt -> [TParam]
dctForall :: [TParam]
  , DelayedCt -> [Prop]
dctAsmps  :: [Prop]
  , DelayedCt -> [Goal]
dctGoals  :: [Goal]
  } deriving (Int -> DelayedCt -> ShowS
[DelayedCt] -> ShowS
DelayedCt -> FilePath
(Int -> DelayedCt -> ShowS)
-> (DelayedCt -> FilePath)
-> ([DelayedCt] -> ShowS)
-> Show DelayedCt
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DelayedCt -> ShowS
showsPrec :: Int -> DelayedCt -> ShowS
$cshow :: DelayedCt -> FilePath
show :: DelayedCt -> FilePath
$cshowList :: [DelayedCt] -> ShowS
showList :: [DelayedCt] -> ShowS
Show, (forall x. DelayedCt -> Rep DelayedCt x)
-> (forall x. Rep DelayedCt x -> DelayedCt) -> Generic DelayedCt
forall x. Rep DelayedCt x -> DelayedCt
forall x. DelayedCt -> Rep DelayedCt x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DelayedCt -> Rep DelayedCt x
from :: forall x. DelayedCt -> Rep DelayedCt x
$cto :: forall x. Rep DelayedCt x -> DelayedCt
to :: forall x. Rep DelayedCt x -> DelayedCt
Generic, DelayedCt -> ()
(DelayedCt -> ()) -> NFData DelayedCt
forall a. (a -> ()) -> NFData a
$crnf :: DelayedCt -> ()
rnf :: DelayedCt -> ()
NFData)

-- | Information about how a constraint came to be, used in error reporting.
data ConstraintSource
  = CtComprehension       -- ^ Computing shape of list comprehension
  | CtSplitPat            -- ^ Use of a split pattern
  | CtTypeSig             -- ^ A type signature in a pattern or expression
  | CtInst Expr           -- ^ Instantiation of this expression
  | CtSelector
  | CtExactType
  | CtEnumeration
  | CtDefaulting          -- ^ Just defaulting on the command line
  | CtPartialTypeFun Name -- ^ Use of a partial type function.
  | CtImprovement
  | CtPattern TypeSource  -- ^ Constraints arising from type-checking patterns
  | CtModuleInstance Range -- ^ Instantiating a parametrized module
  | CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
  | CtFFI Name            -- ^ Constraints on a foreign declaration required
                          --   by the FFI (e.g. sequences must be finite)
    deriving (Int -> ConstraintSource -> ShowS
[ConstraintSource] -> ShowS
ConstraintSource -> FilePath
(Int -> ConstraintSource -> ShowS)
-> (ConstraintSource -> FilePath)
-> ([ConstraintSource] -> ShowS)
-> Show ConstraintSource
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstraintSource -> ShowS
showsPrec :: Int -> ConstraintSource -> ShowS
$cshow :: ConstraintSource -> FilePath
show :: ConstraintSource -> FilePath
$cshowList :: [ConstraintSource] -> ShowS
showList :: [ConstraintSource] -> ShowS
Show, (forall x. ConstraintSource -> Rep ConstraintSource x)
-> (forall x. Rep ConstraintSource x -> ConstraintSource)
-> Generic ConstraintSource
forall x. Rep ConstraintSource x -> ConstraintSource
forall x. ConstraintSource -> Rep ConstraintSource x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ConstraintSource -> Rep ConstraintSource x
from :: forall x. ConstraintSource -> Rep ConstraintSource x
$cto :: forall x. Rep ConstraintSource x -> ConstraintSource
to :: forall x. Rep ConstraintSource x -> ConstraintSource
Generic, ConstraintSource -> ()
(ConstraintSource -> ()) -> NFData ConstraintSource
forall a. (a -> ()) -> NFData a
$crnf :: ConstraintSource -> ()
rnf :: ConstraintSource -> ()
NFData)

selSrc :: Selector -> TypeSource
selSrc :: Selector -> TypeSource
selSrc Selector
l = case Selector
l of
             RecordSel Ident
la Maybe [Ident]
_ -> Ident -> TypeSource
TypeOfRecordField Ident
la
             TupleSel Int
n Maybe Int
_   -> Int -> TypeSource
TypeOfTupleField Int
n
             ListSel Int
_ Maybe Int
_    -> TypeSource
TypeOfSeqElement





instance TVars ConstraintSource where
  apSubst :: Subst -> ConstraintSource -> ConstraintSource
apSubst Subst
su ConstraintSource
src =
    case ConstraintSource
src of
      ConstraintSource
CtComprehension -> ConstraintSource
src
      ConstraintSource
CtSplitPat      -> ConstraintSource
src
      ConstraintSource
CtTypeSig       -> ConstraintSource
src
      CtInst Expr
e        -> Expr -> ConstraintSource
CtInst (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
      ConstraintSource
CtSelector      -> ConstraintSource
src
      ConstraintSource
CtExactType     -> ConstraintSource
src
      ConstraintSource
CtEnumeration   -> ConstraintSource
src
      ConstraintSource
CtDefaulting    -> ConstraintSource
src
      CtPartialTypeFun Name
_ -> ConstraintSource
src
      ConstraintSource
CtImprovement    -> ConstraintSource
src
      CtPattern TypeSource
_      -> ConstraintSource
src
      CtModuleInstance Range
_ -> ConstraintSource
src
      CtPropGuardsExhaustive Name
_ -> ConstraintSource
src
      CtFFI Name
_          -> ConstraintSource
src


instance FVS Goal where
  fvs :: Goal -> Set TVar
fvs Goal
g = Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Goal -> Prop
goal Goal
g)

instance FVS DelayedCt where
  fvs :: DelayedCt -> Set TVar
fvs DelayedCt
d = ([Prop], [Goal]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
d, DelayedCt -> [Goal]
dctGoals DelayedCt
d) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference`
                            [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
d))


instance TVars Goals where
  -- XXX: could be more efficient
  apSubst :: Subst -> Goals -> Goals
apSubst Subst
su Goals
gs = case (Goal -> Maybe Goal) -> [Goal] -> Maybe [Goal]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust Goal -> Maybe Goal
apG (Goals -> [Goal]
fromGoals Goals
gs) of
                    Maybe [Goal]
Nothing  -> Goals
gs
                    Just [Goal]
gs1 -> [Goal] -> Goals
goalsFromList ((Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
norm [Goal]
gs1)
    where
    norm :: Goal -> [Goal]
norm Goal
g = [ Goal
g { goal = p } | Prop
p <- Prop -> [Prop]
pSplitAnd (Goal -> Prop
goal Goal
g) ]
    apG :: Goal -> Maybe Goal
apG Goal
g  = Goal -> Prop -> Goal
mk Goal
g (Prop -> Goal) -> Maybe Prop -> Maybe Goal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst -> Prop -> Maybe Prop
apSubstMaybe Subst
su (Goal -> Prop
goal Goal
g)
    mk :: Goal -> Prop -> Goal
mk Goal
g Prop
p = Goal
g { goal = p }


instance TVars Goal where
  apSubst :: Subst -> Goal -> Goal
apSubst Subst
su Goal
g = Goal { goalSource :: ConstraintSource
goalSource = Subst -> ConstraintSource -> ConstraintSource
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Goal -> ConstraintSource
goalSource Goal
g)
                      , goalRange :: Range
goalRange  = Goal -> Range
goalRange Goal
g
                      , goal :: Prop
goal       = Subst -> Prop -> Prop
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Goal -> Prop
goal Goal
g)
                      }

instance TVars HasGoal where
  apSubst :: Subst -> HasGoal -> HasGoal
apSubst Subst
su HasGoal
h = HasGoal
h { hasGoal = apSubst su (hasGoal h) }

instance TVars DelayedCt where
  apSubst :: Subst -> DelayedCt -> DelayedCt
apSubst Subst
su DelayedCt
g
    | Set TVar -> Bool
forall a. Set a -> Bool
Set.null Set TVar
captured =
       DelayedCt { dctSource :: Maybe Name
dctSource = DelayedCt -> Maybe Name
dctSource DelayedCt
g
                 , dctForall :: [TParam]
dctForall = DelayedCt -> [TParam]
dctForall DelayedCt
g
                 , dctAsmps :: [Prop]
dctAsmps  = Subst -> [Prop] -> [Prop]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Prop]
dctAsmps DelayedCt
g)
                 , dctGoals :: [Goal]
dctGoals  = Subst -> [Goal] -> [Goal]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (DelayedCt -> [Goal]
dctGoals DelayedCt
g)
                 }

    | Bool
otherwise = FilePath -> [FilePath] -> DelayedCt
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"Cryptol.TypeCheck.Subst.apSubst (DelayedCt)"
                    [ FilePath
"Captured quantified variables:"
                    , FilePath
"Substitution: " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Subst -> FilePath
forall a. Show a => a -> FilePath
show Subst
su
                    , FilePath
"Variables:    " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Set TVar -> FilePath
forall a. Show a => a -> FilePath
show Set TVar
captured
                    , FilePath
"Constraint:   " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ DelayedCt -> FilePath
forall a. Show a => a -> FilePath
show DelayedCt
g
                    ]

    where
    captured :: Set TVar
captured = [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
g))
               Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection`
               Set TVar
subVars
    subVars :: Set TVar
subVars = [Set TVar] -> Set TVar
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                ([Set TVar] -> Set TVar) -> [Set TVar] -> Set TVar
forall a b. (a -> b) -> a -> b
$ (TVar -> Set TVar) -> [TVar] -> [Set TVar]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Prop -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (Maybe Prop -> Set TVar)
-> (TVar -> Maybe Prop) -> TVar -> Set TVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> TVar -> Maybe Prop
applySubstToVar Subst
su)
                ([TVar] -> [Set TVar]) -> [TVar] -> [Set TVar]
forall a b. (a -> b) -> a -> b
$ Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
used
    used :: Set TVar
used = ([Prop], [Prop]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
g, (Goal -> Prop) -> [Goal] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Prop
goal (DelayedCt -> [Goal]
dctGoals DelayedCt
g)) Set TVar -> Set TVar -> Set TVar
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference`
                [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
tpVar (DelayedCt -> [TParam]
dctForall DelayedCt
g))

-- | For use in error messages
cppKind :: Kind -> Doc
cppKind :: Kind -> Doc
cppKind Kind
ki =
  case Kind
ki of
    Kind
KNum  -> FilePath -> Doc
text FilePath
"a numeric type"
    Kind
KType -> FilePath -> Doc
text FilePath
"a value type"
    Kind
KProp -> FilePath -> Doc
text FilePath
"a constraint"
    Kind
_     -> Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
ki

addTVarsDescsAfter :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter :: forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsAfter NameMap
nm t
t = NameMap -> Set TVar -> Doc -> Doc
addTVarsDescsAfterFVS NameMap
nm (t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs t
t)

addTVarsDescsAfterFVS :: NameMap -> Set TVar -> Doc -> Doc
addTVarsDescsAfterFVS :: NameMap -> Set TVar -> Doc -> Doc
addTVarsDescsAfterFVS NameMap
nm Set TVar
vs Doc
d
  | Set TVar -> Bool
forall a. Set a -> Bool
Set.null Set TVar
vs = Doc
d
-- TODO? use `hang` here instead to indent things after "where"
  | Bool
otherwise   = Doc
d Doc -> Doc -> Doc
$$ FilePath -> Doc
text FilePath
"where" Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat ((TVar -> Doc) -> [TVar] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
vs))
  where
  desc :: TVar -> Doc
desc TVar
v = NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> TVarInfo -> Doc
forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)


addTVarsDescsBefore :: FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore :: forall t. FVS t => NameMap -> t -> Doc -> Doc
addTVarsDescsBefore NameMap
nm t
t Doc
d = [Doc] -> Doc
vcat ([Doc]
frontMsg [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
d] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
backMsg)
  where
  (Set TVar
vs1,Set TVar
vs2)  = (TVar -> Bool) -> Set TVar -> (Set TVar, Set TVar)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition TVar -> Bool
isFreeTV (t -> Set TVar
forall t. FVS t => t -> Set TVar
fvs t
t)

  frontMsg :: [Doc]
frontMsg | Set TVar -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVar
vs1  = []
           | Bool
otherwise = [Doc -> Int -> Doc -> Doc
hang Doc
"Failed to infer the following types:"
                             Int
2 ([Doc] -> Doc
vcat ((TVar -> Doc) -> [TVar] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc1 (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
vs1)))]
  desc1 :: TVar -> Doc
desc1 TVar
v    = Doc
"•" Doc -> Doc -> Doc
<+> NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<.> Doc
comma Doc -> Doc -> Doc
<+> TVarInfo -> Doc
forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)

  backMsg :: [Doc]
backMsg  | Set TVar -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVar
vs2  = []
           | Bool
otherwise = [Doc -> Int -> Doc -> Doc
hang Doc
"where"
                             Int
2 ([Doc] -> Doc
vcat ((TVar -> Doc) -> [TVar] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TVar -> Doc
desc2 (Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList Set TVar
vs2)))]
  desc2 :: TVar -> Doc
desc2 TVar
v    = NameMap -> TVar -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm TVar
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> TVarInfo -> Doc
forall a. PP a => a -> Doc
pp (TVar -> TVarInfo
tvInfo TVar
v)



instance PP ConstraintSource where
  ppPrec :: Int -> ConstraintSource -> Doc
ppPrec Int
_ ConstraintSource
src =
    case ConstraintSource
src of
      ConstraintSource
CtComprehension -> Doc
"list comprehension"
      ConstraintSource
CtSplitPat      -> Doc
"split (#) pattern"
      ConstraintSource
CtTypeSig       -> Doc
"type signature"
      CtInst Expr
e        -> Doc
"use of" Doc -> Doc -> Doc
<+> Expr -> Doc
ppUse Expr
e
      ConstraintSource
CtSelector      -> Doc
"use of selector"
      ConstraintSource
CtExactType     -> Doc
"matching types"
      ConstraintSource
CtEnumeration   -> Doc
"list enumeration"
      ConstraintSource
CtDefaulting    -> Doc
"defaulting"
      CtPartialTypeFun Name
f -> Doc
"use of partial type function" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
f
      ConstraintSource
CtImprovement   -> Doc
"examination of collected goals"
      CtPattern TypeSource
ad    -> Doc
"checking a pattern:" Doc -> Doc -> Doc
<+> TypeSource -> Doc
forall a. PP a => a -> Doc
pp TypeSource
ad
      CtModuleInstance Range
r -> Doc
"module instantiation at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r
      CtPropGuardsExhaustive Name
n -> Doc
"exhaustion check for prop guards used in defining" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
n
      CtFFI Name
f         -> Doc
"declaration of foreign function" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
f

ppUse :: Expr -> Doc
ppUse :: Expr -> Doc
ppUse Expr
expr =
  case Expr
expr of
    EVar (Name -> Maybe Text
isPrelPrim -> Just Text
prim)
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"number"       -> Doc
"literal or demoted expression"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fraction"     -> Doc
"fractional literal"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"infFrom"      -> Doc
"infinite enumeration"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"infFromThen"  -> Doc
"infinite enumeration (with step)"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fromTo"       -> Doc
"finite enumeration"
      | Text
prim Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"fromThenTo"   -> Doc
"finite enumeration"
    Expr
_                          -> Doc
"expression" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
expr
  where
  isPrelPrim :: Name -> Maybe Text
isPrelPrim Name
x = do PrimIdent ModName
p Text
i <- Name -> Maybe PrimIdent
asPrim Name
x
                    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (ModName
p ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
preludeName)
                    Text -> Maybe Text
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
i

instance PP (WithNames Goal) where
  ppPrec :: Int -> WithNames Goal -> Doc
ppPrec Int
_ (WithNames Goal
g NameMap
names) =
      Doc -> Int -> Doc -> Doc
hang (NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
names (Goal -> Prop
goal Goal
g))
         Int
2 (FilePath -> Doc
text FilePath
"arising from" Doc -> Doc -> Doc
$$
            ConstraintSource -> Doc
forall a. PP a => a -> Doc
pp (Goal -> ConstraintSource
goalSource Goal
g)   Doc -> Doc -> Doc
$$
            FilePath -> Doc
text FilePath
"at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp (Goal -> Range
goalRange Goal
g))

instance PP (WithNames DelayedCt) where
  ppPrec :: Int -> WithNames DelayedCt -> Doc
ppPrec Int
_ (WithNames DelayedCt
d NameMap
names) =
    Doc
sig Doc -> Doc -> Doc
$$
    Doc -> Int -> Doc -> Doc
hang Doc
"we need to show that"
    
       Int
2 (Doc -> Doc
explain ([Doc] -> Doc
vcat ( [Doc]
vars [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
asmps [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
               [ Doc -> Int -> Doc -> Doc
hang Doc
"the following constraints hold:"
                    Int
2 ([Doc] -> Doc
vcat
                       ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
bullets
                       ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Goal -> Doc) -> [Goal] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Goal -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1)
                       ([Goal] -> [Doc]) -> [Goal] -> [Doc]
forall a b. (a -> b) -> a -> b
$ DelayedCt -> [Goal]
dctGoals DelayedCt
d )])))
    where
 

    bullets :: [Doc] -> [Doc]
bullets [Doc]
xs = [ Doc
"•" Doc -> Doc -> Doc
<+> Doc
x | Doc
x <- [Doc]
xs ]

    sig :: Doc
sig = case Maybe Name
name of
            Just Name
n -> Doc
"in the definition of" Doc -> Doc -> Doc
<+> Doc -> Doc
quotes (Name -> Doc
forall a. PP a => a -> Doc
pp Name
n) Doc -> Doc -> Doc
<.>
                      Doc
comma Doc -> Doc -> Doc
<+> Doc
"at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp (Name -> Range
nameLoc Name
n) Doc -> Doc -> Doc
<.> Doc
comma
            Maybe Name
Nothing -> Doc
"when checking the module's parameters,"

    name :: Maybe Name
name  = DelayedCt -> Maybe Name
dctSource DelayedCt
d
    vars :: [Doc]
vars = case [TParam]
otherTPs of
             [] -> []
             [TParam]
xs -> [Doc
"for any type" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [TParam]
xs)]
    asmps :: [Doc]
asmps = case DelayedCt -> [Prop]
dctAsmps DelayedCt
d of
              [] -> []
              [Prop]
xs -> [Doc -> Int -> Doc -> Doc
hang Doc
"assuming"
                       Int
2 ([Doc] -> Doc
vcat ([Doc] -> [Doc]
bullets ((Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1) [Prop]
xs)))]

    tvars :: Set TVar
tvars = ([Prop], [Goal]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs (DelayedCt -> [Prop]
dctAsmps DelayedCt
d, DelayedCt -> [Goal]
dctGoals DelayedCt
d)
    used :: [TParam]
used = (TParam -> Bool) -> [TParam] -> [TParam]
forall a. (a -> Bool) -> [a] -> [a]
filter ((TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set TVar
tvars) (TVar -> Bool) -> (TParam -> TVar) -> TParam -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound) (DelayedCt -> [TParam]
dctForall DelayedCt
d)
    isModP :: TParam -> Bool
isModP TParam
tp =
      case TParam -> TPFlavor
tpFlav TParam
tp of
        TPModParam {} -> Bool
True
        TPFlavor
_ -> Bool
False
    ([TParam]
mpTPs,[TParam]
otherTPs) = (TParam -> Bool) -> [TParam] -> ([TParam], [TParam])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition TParam -> Bool
isModP [TParam]
used
    explain :: Doc -> Doc
explain = NameMap -> Set TVar -> Doc -> Doc
addTVarsDescsAfterFVS NameMap
ns1 ([TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList ((TParam -> TVar) -> [TParam] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> TVar
TVBound [TParam]
mpTPs))
    
    mps :: NameMap
mps = [TParam] -> NameMap -> NameMap
computeModParamNames [TParam]
mpTPs NameMap
names
    ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames [TParam]
otherTPs NameMap
mps



-- | Add a suffix to a name to make a different label.
nameVariant :: Int -> String -> String
nameVariant :: Int -> ShowS
nameVariant Int
n FilePath
x = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then FilePath
x else FilePath
x FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
suff
  where
  useUnicode :: Bool
useUnicode = Bool
True

  suff :: FilePath
suff
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
10 Bool -> Bool -> Bool
&& Bool
useUnicode = [Int -> Char
forall a. Enum a => Int -> a
toEnum (Int
0x2080 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)]
    | Bool
otherwise = Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n

  

-- | Pick names for the type parameters that correspond to module parameters,
-- avoiding strings that already appear in the given name map.
-- Returns an extended name map.
computeModParamNames :: [TParam] -> NameMap -> NameMap
computeModParamNames :: [TParam] -> NameMap -> NameMap
computeModParamNames [TParam]
tps NameMap
names = [(Int, FilePath)] -> NameMap
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, FilePath)]
newNames NameMap -> NameMap -> NameMap
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` NameMap
names
  where
  newNames :: [(Int, FilePath)]
newNames = (Set FilePath, [(Int, FilePath)]) -> [(Int, FilePath)]
forall a b. (a, b) -> b
snd ((Set FilePath
 -> (Int, FilePath) -> (Set FilePath, (Int, FilePath)))
-> Set FilePath
-> [(Int, FilePath)]
-> (Set FilePath, [(Int, FilePath)])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL Set FilePath -> (Int, FilePath) -> (Set FilePath, (Int, FilePath))
forall {a}.
Set FilePath -> (a, FilePath) -> (Set FilePath, (a, FilePath))
pickName Set FilePath
used0 ((TParam -> Maybe (Int, FilePath)) -> [TParam] -> [(Int, FilePath)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TParam -> Maybe (Int, FilePath)
isModP [TParam]
tps))

  used0 :: Set FilePath
used0 = [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList (NameMap -> [FilePath]
forall a. IntMap a -> [a]
IntMap.elems NameMap
names)

  pickName :: Set FilePath -> (a, FilePath) -> (Set FilePath, (a, FilePath))
pickName Set FilePath
used (a
u,FilePath
i) =
    let ns :: [FilePath]
ns   = (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set FilePath
used))
              ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (Int -> FilePath) -> [Int] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> ShowS
`nameVariant` FilePath
i) [Int
0..]
        name :: FilePath
name = case [FilePath]
ns of
                 FilePath
x : [FilePath]
_ -> FilePath
x
                 []    -> FilePath -> [FilePath] -> FilePath
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"computeModParamNames" [FilePath
"Out of names!"]
    in (FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => a -> Set a -> Set a
Set.insert FilePath
name Set FilePath
used, (a
u,FilePath
name))

  isModP :: TParam -> Maybe (Int, FilePath)
isModP TParam
tp =
    case TParam -> TPFlavor
tpFlav TParam
tp of
      TPModParam Name
x -> (Int, FilePath) -> Maybe (Int, FilePath)
forall a. a -> Maybe a
Just (TParam -> Int
tpUnique TParam
tp, Doc -> FilePath
forall a. Show a => a -> FilePath
show (Ident -> Doc
forall a. PP a => a -> Doc
pp (Name -> Ident
nameIdent Name
x)))
      TPFlavor
_ -> Maybe (Int, FilePath)
forall a. Maybe a
Nothing