----------------------------------------------------------------------
-- |
-- Module      : Grammar
-- Maintainer  : AR
-- Stability   : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/04/21 16:22:20 $ 
-- > CVS $Author: bringert $
-- > CVS $Revision: 1.8 $
--
-- GF source abstract syntax used internally in compilation.
--
-- AR 23\/1\/2000 -- 30\/5\/2001 -- 4\/5\/2003
-----------------------------------------------------------------------------

module GF.Grammar.Grammar (
        -- ** Grammar modules
        Grammar, ModuleName, Module, ModuleInfo(..),
        SourceGrammar, SourceModInfo, SourceModule,
        ModuleType(..),
        emptyGrammar, mGrammar, modules, prependModule, moduleMap,

        MInclude (..), OpenSpec(..),
        extends, isInherited, inheritAll,
        openedModule, allDepsModule, partOfGrammar, depPathModule,
        allExtends, allExtendsPlus, --searchPathModule,
        
        lookupModule,
        isModAbs, isModRes, isModCnc,
        sameMType, isCompilableModule, isCompleteModule,
        allAbstracts, greatestAbstract, allResources,
        greatestResource, allConcretes, allConcreteModules,
        abstractOfConcrete,

        ModuleStatus(..),

        -- ** Judgements
        Info(..),
        -- ** Terms
        Term(..),
        Type,
        Cat,
        Fun,
        QIdent,
        BindType(..),
        Patt(..),
        TInfo(..),
        Label(..),
        MetaId,
        Hypo,
        Context,
        Equation,
        Labelling,
        Assign,
        Case,
        LocalDef,
        Param,
        Altern,
        Substitution,
        varLabel, tupleLabel, linLabel, theLinLabel,
        ident2label, label2ident,
        -- ** Source locations
        Location(..), L(..), unLoc, noLoc, ppLocation, ppL,

        -- ** PMCFG        
        PMCFG(..), Production(..), FId, FunId, SeqId, LIndex, Sequence
        ) where

import GF.Infra.Ident
import GF.Infra.Option ---
import GF.Infra.Location

import GF.Data.Operations

import PGF.Internal (FId, FunId, SeqId, LIndex, Sequence, BindType(..))

import Data.Array.IArray(Array)
import Data.Array.Unboxed(UArray)
import qualified Data.Map as Map
import GF.Text.Pretty


-- | A grammar is a self-contained collection of grammar modules
data Grammar = MGrammar { 
    Grammar -> Map ModuleName ModuleInfo
moduleMap :: Map.Map ModuleName ModuleInfo,
    Grammar -> [Module]
modules :: [Module]
  }

-- | Modules
type Module = (ModuleName, ModuleInfo)

data ModuleInfo = ModInfo {
    ModuleInfo -> ModuleType
mtype   :: ModuleType,
    ModuleInfo -> ModuleStatus
mstatus :: ModuleStatus,
    ModuleInfo -> Options
mflags  :: Options,
    ModuleInfo -> [(ModuleName, MInclude)]
mextend :: [(ModuleName,MInclude)],
    ModuleInfo
-> Maybe (ModuleName, MInclude, [(ModuleName, ModuleName)])
mwith   :: Maybe (ModuleName,MInclude,[(ModuleName,ModuleName)]),
    ModuleInfo -> [OpenSpec]
mopens  :: [OpenSpec],
    ModuleInfo -> [ModuleName]
mexdeps :: [ModuleName],
    ModuleInfo -> FilePath
msrc    :: FilePath,
    ModuleInfo -> Maybe (Array SeqId Sequence)
mseqs   :: Maybe (Array SeqId Sequence),
    ModuleInfo -> Map Ident Info
jments  :: Map.Map Ident Info
  }

type SourceGrammar = Grammar
type SourceModule = Module
type SourceModInfo = ModuleInfo

instance HasSourcePath ModuleInfo where sourcePath :: ModuleInfo -> FilePath
sourcePath = ModuleInfo -> FilePath
msrc

-- | encoding the type of the module
data ModuleType = 
    MTAbstract 
  | MTResource
  | MTConcrete ModuleName
  | MTInterface
  | MTInstance (ModuleName,MInclude)
  deriving (ModuleType -> ModuleType -> Bool
(ModuleType -> ModuleType -> Bool)
-> (ModuleType -> ModuleType -> Bool) -> Eq ModuleType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleType -> ModuleType -> Bool
$c/= :: ModuleType -> ModuleType -> Bool
== :: ModuleType -> ModuleType -> Bool
$c== :: ModuleType -> ModuleType -> Bool
Eq,SeqId -> ModuleType -> ShowS
[ModuleType] -> ShowS
ModuleType -> FilePath
(SeqId -> ModuleType -> ShowS)
-> (ModuleType -> FilePath)
-> ([ModuleType] -> ShowS)
-> Show ModuleType
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [ModuleType] -> ShowS
$cshowList :: [ModuleType] -> ShowS
show :: ModuleType -> FilePath
$cshow :: ModuleType -> FilePath
showsPrec :: SeqId -> ModuleType -> ShowS
$cshowsPrec :: SeqId -> ModuleType -> ShowS
Show)

data MInclude = MIAll | MIOnly [Ident] | MIExcept [Ident]
  deriving (MInclude -> MInclude -> Bool
(MInclude -> MInclude -> Bool)
-> (MInclude -> MInclude -> Bool) -> Eq MInclude
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MInclude -> MInclude -> Bool
$c/= :: MInclude -> MInclude -> Bool
== :: MInclude -> MInclude -> Bool
$c== :: MInclude -> MInclude -> Bool
Eq,SeqId -> MInclude -> ShowS
[MInclude] -> ShowS
MInclude -> FilePath
(SeqId -> MInclude -> ShowS)
-> (MInclude -> FilePath) -> ([MInclude] -> ShowS) -> Show MInclude
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [MInclude] -> ShowS
$cshowList :: [MInclude] -> ShowS
show :: MInclude -> FilePath
$cshow :: MInclude -> FilePath
showsPrec :: SeqId -> MInclude -> ShowS
$cshowsPrec :: SeqId -> MInclude -> ShowS
Show)

extends :: ModuleInfo -> [ModuleName]
extends :: ModuleInfo -> [ModuleName]
extends = ((ModuleName, MInclude) -> ModuleName)
-> [(ModuleName, MInclude)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, MInclude) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, MInclude)] -> [ModuleName])
-> (ModuleInfo -> [(ModuleName, MInclude)])
-> ModuleInfo
-> [ModuleName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> [(ModuleName, MInclude)]
mextend

isInherited :: MInclude -> Ident -> Bool
isInherited :: MInclude -> Ident -> Bool
isInherited MInclude
c Ident
i = case MInclude
c of
  MInclude
MIAll -> Bool
True
  MIOnly [Ident]
is -> Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Ident
i [Ident]
is
  MIExcept [Ident]
is -> Ident -> [Ident] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Ident
i [Ident]
is

inheritAll :: ModuleName -> (ModuleName,MInclude)
inheritAll :: ModuleName -> (ModuleName, MInclude)
inheritAll ModuleName
i = (ModuleName
i,MInclude
MIAll)

data OpenSpec = 
   OSimple ModuleName
 | OQualif ModuleName ModuleName
  deriving (OpenSpec -> OpenSpec -> Bool
(OpenSpec -> OpenSpec -> Bool)
-> (OpenSpec -> OpenSpec -> Bool) -> Eq OpenSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OpenSpec -> OpenSpec -> Bool
$c/= :: OpenSpec -> OpenSpec -> Bool
== :: OpenSpec -> OpenSpec -> Bool
$c== :: OpenSpec -> OpenSpec -> Bool
Eq,SeqId -> OpenSpec -> ShowS
[OpenSpec] -> ShowS
OpenSpec -> FilePath
(SeqId -> OpenSpec -> ShowS)
-> (OpenSpec -> FilePath) -> ([OpenSpec] -> ShowS) -> Show OpenSpec
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [OpenSpec] -> ShowS
$cshowList :: [OpenSpec] -> ShowS
show :: OpenSpec -> FilePath
$cshow :: OpenSpec -> FilePath
showsPrec :: SeqId -> OpenSpec -> ShowS
$cshowsPrec :: SeqId -> OpenSpec -> ShowS
Show)

data ModuleStatus = 
   MSComplete 
 | MSIncomplete 
  deriving (ModuleStatus -> ModuleStatus -> Bool
(ModuleStatus -> ModuleStatus -> Bool)
-> (ModuleStatus -> ModuleStatus -> Bool) -> Eq ModuleStatus
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleStatus -> ModuleStatus -> Bool
$c/= :: ModuleStatus -> ModuleStatus -> Bool
== :: ModuleStatus -> ModuleStatus -> Bool
$c== :: ModuleStatus -> ModuleStatus -> Bool
Eq,Eq ModuleStatus
Eq ModuleStatus
-> (ModuleStatus -> ModuleStatus -> Ordering)
-> (ModuleStatus -> ModuleStatus -> Bool)
-> (ModuleStatus -> ModuleStatus -> Bool)
-> (ModuleStatus -> ModuleStatus -> Bool)
-> (ModuleStatus -> ModuleStatus -> Bool)
-> (ModuleStatus -> ModuleStatus -> ModuleStatus)
-> (ModuleStatus -> ModuleStatus -> ModuleStatus)
-> Ord ModuleStatus
ModuleStatus -> ModuleStatus -> Bool
ModuleStatus -> ModuleStatus -> Ordering
ModuleStatus -> ModuleStatus -> ModuleStatus
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ModuleStatus -> ModuleStatus -> ModuleStatus
$cmin :: ModuleStatus -> ModuleStatus -> ModuleStatus
max :: ModuleStatus -> ModuleStatus -> ModuleStatus
$cmax :: ModuleStatus -> ModuleStatus -> ModuleStatus
>= :: ModuleStatus -> ModuleStatus -> Bool
$c>= :: ModuleStatus -> ModuleStatus -> Bool
> :: ModuleStatus -> ModuleStatus -> Bool
$c> :: ModuleStatus -> ModuleStatus -> Bool
<= :: ModuleStatus -> ModuleStatus -> Bool
$c<= :: ModuleStatus -> ModuleStatus -> Bool
< :: ModuleStatus -> ModuleStatus -> Bool
$c< :: ModuleStatus -> ModuleStatus -> Bool
compare :: ModuleStatus -> ModuleStatus -> Ordering
$ccompare :: ModuleStatus -> ModuleStatus -> Ordering
$cp1Ord :: Eq ModuleStatus
Ord,SeqId -> ModuleStatus -> ShowS
[ModuleStatus] -> ShowS
ModuleStatus -> FilePath
(SeqId -> ModuleStatus -> ShowS)
-> (ModuleStatus -> FilePath)
-> ([ModuleStatus] -> ShowS)
-> Show ModuleStatus
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [ModuleStatus] -> ShowS
$cshowList :: [ModuleStatus] -> ShowS
show :: ModuleStatus -> FilePath
$cshow :: ModuleStatus -> FilePath
showsPrec :: SeqId -> ModuleStatus -> ShowS
$cshowsPrec :: SeqId -> ModuleStatus -> ShowS
Show)

openedModule :: OpenSpec -> ModuleName
openedModule :: OpenSpec -> ModuleName
openedModule OpenSpec
o = case OpenSpec
o of
  OSimple ModuleName
m -> ModuleName
m
  OQualif ModuleName
_ ModuleName
m -> ModuleName
m

-- | initial dependency list
depPathModule :: ModuleInfo -> [OpenSpec]
depPathModule :: ModuleInfo -> [OpenSpec]
depPathModule ModuleInfo
m = ModuleInfo -> [OpenSpec]
fors ModuleInfo
m [OpenSpec] -> [OpenSpec] -> [OpenSpec]
forall a. [a] -> [a] -> [a]
++ ModuleInfo -> [OpenSpec]
exts ModuleInfo
m [OpenSpec] -> [OpenSpec] -> [OpenSpec]
forall a. [a] -> [a] -> [a]
++ ModuleInfo -> [OpenSpec]
mopens ModuleInfo
m
  where
    fors :: ModuleInfo -> [OpenSpec]
fors ModuleInfo
m = 
      case ModuleInfo -> ModuleType
mtype ModuleInfo
m of
        MTConcrete ModuleName
i   -> [ModuleName -> OpenSpec
OSimple ModuleName
i]
        MTInstance (ModuleName
i,MInclude
_)   -> [ModuleName -> OpenSpec
OSimple ModuleName
i]
        ModuleType
_              -> []
    exts :: ModuleInfo -> [OpenSpec]
exts ModuleInfo
m = (ModuleName -> OpenSpec) -> [ModuleName] -> [OpenSpec]
forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> OpenSpec
OSimple (ModuleInfo -> [ModuleName]
extends ModuleInfo
m)

-- | all dependencies
allDepsModule :: Grammar -> ModuleInfo -> [OpenSpec]
allDepsModule :: Grammar -> ModuleInfo -> [OpenSpec]
allDepsModule Grammar
gr ModuleInfo
m = ([OpenSpec] -> [OpenSpec]) -> [OpenSpec] -> [OpenSpec]
forall a. Eq a => ([a] -> [a]) -> [a] -> [a]
iterFix [OpenSpec] -> [OpenSpec]
add [OpenSpec]
os0 where
  os0 :: [OpenSpec]
os0 = ModuleInfo -> [OpenSpec]
depPathModule ModuleInfo
m
  add :: [OpenSpec] -> [OpenSpec]
add [OpenSpec]
os = [OpenSpec
m | OpenSpec
o <- [OpenSpec]
os, Just ModuleInfo
n <- [ModuleName -> [Module] -> Maybe ModuleInfo
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (OpenSpec -> ModuleName
openedModule OpenSpec
o) [Module]
mods], 
                OpenSpec
m <- ModuleInfo -> [OpenSpec]
depPathModule ModuleInfo
n]
  mods :: [Module]
mods = Grammar -> [Module]
modules Grammar
gr

-- | select just those modules that a given one depends on, including itself
partOfGrammar :: Grammar -> Module -> Grammar
partOfGrammar :: Grammar -> Module -> Grammar
partOfGrammar Grammar
gr (ModuleName
i,ModuleInfo
m) = [Module] -> Grammar
mGrammar [Module
mo | mo :: Module
mo@(ModuleName
j,ModuleInfo
_) <- [Module]
mods, ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ModuleName
j [ModuleName]
modsFor]
  where
    mods :: [Module]
mods = Grammar -> [Module]
modules Grammar
gr
    modsFor :: [ModuleName]
modsFor = (ModuleName
iModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
:) ([ModuleName] -> [ModuleName]) -> [ModuleName] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ (OpenSpec -> ModuleName) -> [OpenSpec] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map OpenSpec -> ModuleName
openedModule ([OpenSpec] -> [ModuleName]) -> [OpenSpec] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Grammar -> ModuleInfo -> [OpenSpec]
allDepsModule Grammar
gr ModuleInfo
m

-- | all modules that a module extends, directly or indirectly, with restricts
allExtends :: Grammar -> ModuleName -> [Module]
allExtends :: Grammar -> ModuleName -> [Module]
allExtends Grammar
gr ModuleName
m =
  case Grammar -> ModuleName -> Err ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
gr ModuleName
m of
    Ok ModuleInfo
mi -> (ModuleName
m,ModuleInfo
mi) Module -> [Module] -> [Module]
forall a. a -> [a] -> [a]
: ((ModuleName, MInclude) -> [Module])
-> [(ModuleName, MInclude)] -> [Module]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Grammar -> ModuleName -> [Module]
allExtends Grammar
gr (ModuleName -> [Module])
-> ((ModuleName, MInclude) -> ModuleName)
-> (ModuleName, MInclude)
-> [Module]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, MInclude) -> ModuleName
forall a b. (a, b) -> a
fst) (ModuleInfo -> [(ModuleName, MInclude)]
mextend ModuleInfo
mi)
    Err ModuleInfo
_     -> []

-- | the same as 'allExtends' plus that an instance extends its interface
allExtendsPlus :: Grammar -> ModuleName -> [ModuleName]
allExtendsPlus :: Grammar -> ModuleName -> [ModuleName]
allExtendsPlus Grammar
gr ModuleName
i =
  case Grammar -> ModuleName -> Err ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
gr ModuleName
i of
    Ok ModuleInfo
m -> ModuleName
i ModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
: (ModuleName -> [ModuleName]) -> [ModuleName] -> [ModuleName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Grammar -> ModuleName -> [ModuleName]
allExtendsPlus Grammar
gr) (ModuleInfo -> [ModuleName]
exts ModuleInfo
m)
    Err ModuleInfo
_    -> []
  where
    exts :: ModuleInfo -> [ModuleName]
exts ModuleInfo
m = ModuleInfo -> [ModuleName]
extends ModuleInfo
m [ModuleName] -> [ModuleName] -> [ModuleName]
forall a. [a] -> [a] -> [a]
++ [ModuleName
j | MTInstance (ModuleName
j,MInclude
_) <- [ModuleInfo -> ModuleType
mtype ModuleInfo
m]]

-- -- | initial search path: the nonqualified dependencies
-- searchPathModule :: ModuleInfo -> [ModuleName]
-- searchPathModule m = [i | OSimple i <- depPathModule m]

prependModule :: Grammar -> Module -> Grammar
prependModule :: Grammar -> Module -> Grammar
prependModule (MGrammar Map ModuleName ModuleInfo
mm [Module]
ms) im :: Module
im@(ModuleName
i,ModuleInfo
m) = Map ModuleName ModuleInfo -> [Module] -> Grammar
MGrammar (ModuleName
-> ModuleInfo
-> Map ModuleName ModuleInfo
-> Map ModuleName ModuleInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ModuleName
i ModuleInfo
m Map ModuleName ModuleInfo
mm) (Module
imModule -> [Module] -> [Module]
forall a. a -> [a] -> [a]
:[Module]
ms)

emptyGrammar :: Grammar
emptyGrammar = [Module] -> Grammar
mGrammar []

mGrammar :: [Module] -> Grammar
mGrammar :: [Module] -> Grammar
mGrammar [Module]
ms = Map ModuleName ModuleInfo -> [Module] -> Grammar
MGrammar ([Module] -> Map ModuleName ModuleInfo
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [Module]
ms) [Module]
ms


-- | we store the module type with the identifier

abstractOfConcrete :: ErrorMonad m => Grammar -> ModuleName -> m ModuleName
abstractOfConcrete :: Grammar -> ModuleName -> m ModuleName
abstractOfConcrete Grammar
gr ModuleName
c = do
  ModuleInfo
n <- Grammar -> ModuleName -> m ModuleInfo
forall (m :: * -> *).
ErrorMonad m =>
Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
gr ModuleName
c
  case ModuleInfo -> ModuleType
mtype ModuleInfo
n of
    MTConcrete ModuleName
a -> ModuleName -> m ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleName
a
    ModuleType
_ -> FilePath -> m ModuleName
forall (m :: * -> *) a. ErrorMonad m => FilePath -> m a
raise (FilePath -> m ModuleName) -> FilePath -> m ModuleName
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
forall a. Pretty a => a -> FilePath
render (FilePath
"expected concrete" FilePath -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
c)

lookupModule :: ErrorMonad m => Grammar -> ModuleName -> m ModuleInfo
lookupModule :: Grammar -> ModuleName -> m ModuleInfo
lookupModule Grammar
gr ModuleName
m = case ModuleName -> Map ModuleName ModuleInfo -> Maybe ModuleInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
m (Grammar -> Map ModuleName ModuleInfo
moduleMap Grammar
gr) of
  Just ModuleInfo
i  -> ModuleInfo -> m ModuleInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
i
  Maybe ModuleInfo
Nothing -> FilePath -> m ModuleInfo
forall (m :: * -> *) a. ErrorMonad m => FilePath -> m a
raise (FilePath -> m ModuleInfo) -> FilePath -> m ModuleInfo
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
forall a. Pretty a => a -> FilePath
render (FilePath
"unknown module" FilePath -> ModuleName -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> ModuleName
m Doc -> FilePath -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> FilePath
"among" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [ModuleName] -> Doc
forall a. Pretty a => [a] -> Doc
hsep ((Module -> ModuleName) -> [Module] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map Module -> ModuleName
forall a b. (a, b) -> a
fst (Grammar -> [Module]
modules Grammar
gr)))

isModAbs :: ModuleInfo -> Bool
isModAbs :: ModuleInfo -> Bool
isModAbs ModuleInfo
m =
  case ModuleInfo -> ModuleType
mtype ModuleInfo
m of
    ModuleType
MTAbstract -> Bool
True
    ModuleType
_          -> Bool
False

isModRes :: ModuleInfo -> Bool
isModRes :: ModuleInfo -> Bool
isModRes ModuleInfo
m =
  case ModuleInfo -> ModuleType
mtype ModuleInfo
m of
    ModuleType
MTResource   -> Bool
True
    ModuleType
MTInterface  -> Bool
True ---
    MTInstance (ModuleName, MInclude)
_ -> Bool
True
    ModuleType
_            -> Bool
False

isModCnc :: ModuleInfo -> Bool
isModCnc :: ModuleInfo -> Bool
isModCnc ModuleInfo
m =
  case ModuleInfo -> ModuleType
mtype ModuleInfo
m of
    MTConcrete ModuleName
_ -> Bool
True
    ModuleType
_            -> Bool
False

sameMType :: ModuleType -> ModuleType -> Bool
sameMType :: ModuleType -> ModuleType -> Bool
sameMType ModuleType
m ModuleType
n =
  case (ModuleType
n,ModuleType
m) of
    (MTConcrete ModuleName
_, MTConcrete ModuleName
_) -> Bool
True

    (MTInstance (ModuleName, MInclude)
_, MTInstance (ModuleName, MInclude)
_) -> Bool
True
    (MTInstance (ModuleName, MInclude)
_, ModuleType
MTResource)   -> Bool
True
    (MTInstance (ModuleName, MInclude)
_, MTConcrete ModuleName
_) -> Bool
True

    (ModuleType
MTInterface,  MTInstance (ModuleName, MInclude)
_) -> Bool
True
    (ModuleType
MTInterface,  ModuleType
MTResource)   -> Bool
True    -- for reuse
    (ModuleType
MTInterface,  ModuleType
MTAbstract)   -> Bool
True    -- for reuse
    (ModuleType
MTInterface,  MTConcrete ModuleName
_) -> Bool
True    -- for reuse

    (ModuleType
MTResource,   MTInstance (ModuleName, MInclude)
_) -> Bool
True
    (ModuleType
MTResource,   MTConcrete ModuleName
_) -> Bool
True    -- for reuse

    (ModuleType, ModuleType)
_                            -> ModuleType
m ModuleType -> ModuleType -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleType
n

-- | don't generate code for interfaces and for incomplete modules
isCompilableModule :: ModuleInfo -> Bool
isCompilableModule :: ModuleInfo -> Bool
isCompilableModule ModuleInfo
m =
  case ModuleInfo -> ModuleType
mtype ModuleInfo
m of
    ModuleType
MTInterface -> Bool
False
    ModuleType
_           -> ModuleInfo -> ModuleStatus
mstatus ModuleInfo
m ModuleStatus -> ModuleStatus -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleStatus
MSComplete

-- | interface and "incomplete M" are not complete
isCompleteModule :: ModuleInfo -> Bool
isCompleteModule :: ModuleInfo -> Bool
isCompleteModule ModuleInfo
m = ModuleInfo -> ModuleStatus
mstatus ModuleInfo
m ModuleStatus -> ModuleStatus -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleStatus
MSComplete Bool -> Bool -> Bool
&& ModuleInfo -> ModuleType
mtype ModuleInfo
m ModuleType -> ModuleType -> Bool
forall a. Eq a => a -> a -> Bool
/= ModuleType
MTInterface


-- | all abstract modules sorted from least to most dependent
allAbstracts :: Grammar -> [ModuleName]
allAbstracts :: Grammar -> [ModuleName]
allAbstracts Grammar
gr = 
 case [(ModuleName, [ModuleName])] -> Either [ModuleName] [[ModuleName]]
forall a. Ord a => [(a, [a])] -> Either [a] [[a]]
topoTest [(ModuleName
i,ModuleInfo -> [ModuleName]
extends ModuleInfo
m) | (ModuleName
i,ModuleInfo
m) <- Grammar -> [Module]
modules Grammar
gr, ModuleInfo -> ModuleType
mtype ModuleInfo
m ModuleType -> ModuleType -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleType
MTAbstract] of
   Left  [ModuleName]
is     -> [ModuleName]
is
   Right [[ModuleName]]
cycles -> FilePath -> [ModuleName]
forall a. HasCallStack => FilePath -> a
error (FilePath -> [ModuleName]) -> FilePath -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath
forall a. Pretty a => a -> FilePath
render (FilePath
"Cyclic abstract modules:" FilePath -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
vcat (([ModuleName] -> Doc) -> [[ModuleName]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [ModuleName] -> Doc
forall a. Pretty a => [a] -> Doc
hsep [[ModuleName]]
cycles))

-- | the last abstract in dependency order (head of list)
greatestAbstract :: Grammar -> Maybe ModuleName
greatestAbstract :: Grammar -> Maybe ModuleName
greatestAbstract Grammar
gr =
  case Grammar -> [ModuleName]
allAbstracts Grammar
gr of
    [] -> Maybe ModuleName
forall a. Maybe a
Nothing
    [ModuleName]
as -> ModuleName -> Maybe ModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return (ModuleName -> Maybe ModuleName) -> ModuleName -> Maybe ModuleName
forall a b. (a -> b) -> a -> b
$ [ModuleName] -> ModuleName
forall a. [a] -> a
last [ModuleName]
as

-- | all resource modules
allResources :: Grammar -> [ModuleName]
allResources :: Grammar -> [ModuleName]
allResources Grammar
gr = [ModuleName
i | (ModuleName
i,ModuleInfo
m) <- Grammar -> [Module]
modules Grammar
gr, ModuleInfo -> Bool
isModRes ModuleInfo
m Bool -> Bool -> Bool
|| ModuleInfo -> Bool
isModCnc ModuleInfo
m]

-- | the greatest resource in dependency order
greatestResource :: Grammar -> Maybe ModuleName
greatestResource :: Grammar -> Maybe ModuleName
greatestResource Grammar
gr =
  case Grammar -> [ModuleName]
allResources Grammar
gr of
    [] -> Maybe ModuleName
forall a. Maybe a
Nothing
    ModuleName
mo:[ModuleName]
_ -> ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just ModuleName
mo ---- why not last as in Abstract? works though AR 24/5/2008

-- | all concretes for a given abstract
allConcretes :: Grammar -> ModuleName -> [ModuleName]
allConcretes :: Grammar -> ModuleName -> [ModuleName]
allConcretes Grammar
gr ModuleName
a =
  [ModuleName
i | (ModuleName
i, ModuleInfo
m) <- Grammar -> [Module]
modules Grammar
gr, ModuleInfo -> ModuleType
mtype ModuleInfo
m ModuleType -> ModuleType -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName -> ModuleType
MTConcrete ModuleName
a, ModuleInfo -> Bool
isCompleteModule ModuleInfo
m]

-- | all concrete modules for any abstract
allConcreteModules :: Grammar -> [ModuleName]
allConcreteModules :: Grammar -> [ModuleName]
allConcreteModules Grammar
gr =
  [ModuleName
i | (ModuleName
i, ModuleInfo
m) <- Grammar -> [Module]
modules Grammar
gr, MTConcrete ModuleName
_ <- [ModuleInfo -> ModuleType
mtype ModuleInfo
m], ModuleInfo -> Bool
isCompleteModule ModuleInfo
m]


data Production = Production {-# UNPACK #-} !FId
                             {-# UNPACK #-} !FunId
                             [[FId]]
                  deriving (Production -> Production -> Bool
(Production -> Production -> Bool)
-> (Production -> Production -> Bool) -> Eq Production
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Production -> Production -> Bool
$c/= :: Production -> Production -> Bool
== :: Production -> Production -> Bool
$c== :: Production -> Production -> Bool
Eq,Eq Production
Eq Production
-> (Production -> Production -> Ordering)
-> (Production -> Production -> Bool)
-> (Production -> Production -> Bool)
-> (Production -> Production -> Bool)
-> (Production -> Production -> Bool)
-> (Production -> Production -> Production)
-> (Production -> Production -> Production)
-> Ord Production
Production -> Production -> Bool
Production -> Production -> Ordering
Production -> Production -> Production
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Production -> Production -> Production
$cmin :: Production -> Production -> Production
max :: Production -> Production -> Production
$cmax :: Production -> Production -> Production
>= :: Production -> Production -> Bool
$c>= :: Production -> Production -> Bool
> :: Production -> Production -> Bool
$c> :: Production -> Production -> Bool
<= :: Production -> Production -> Bool
$c<= :: Production -> Production -> Bool
< :: Production -> Production -> Bool
$c< :: Production -> Production -> Bool
compare :: Production -> Production -> Ordering
$ccompare :: Production -> Production -> Ordering
$cp1Ord :: Eq Production
Ord,SeqId -> Production -> ShowS
[Production] -> ShowS
Production -> FilePath
(SeqId -> Production -> ShowS)
-> (Production -> FilePath)
-> ([Production] -> ShowS)
-> Show Production
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Production] -> ShowS
$cshowList :: [Production] -> ShowS
show :: Production -> FilePath
$cshow :: Production -> FilePath
showsPrec :: SeqId -> Production -> ShowS
$cshowsPrec :: SeqId -> Production -> ShowS
Show)

data PMCFG = PMCFG [Production]
                   (Array FunId (UArray LIndex SeqId)) 
             deriving (PMCFG -> PMCFG -> Bool
(PMCFG -> PMCFG -> Bool) -> (PMCFG -> PMCFG -> Bool) -> Eq PMCFG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PMCFG -> PMCFG -> Bool
$c/= :: PMCFG -> PMCFG -> Bool
== :: PMCFG -> PMCFG -> Bool
$c== :: PMCFG -> PMCFG -> Bool
Eq,SeqId -> PMCFG -> ShowS
[PMCFG] -> ShowS
PMCFG -> FilePath
(SeqId -> PMCFG -> ShowS)
-> (PMCFG -> FilePath) -> ([PMCFG] -> ShowS) -> Show PMCFG
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [PMCFG] -> ShowS
$cshowList :: [PMCFG] -> ShowS
show :: PMCFG -> FilePath
$cshow :: PMCFG -> FilePath
showsPrec :: SeqId -> PMCFG -> ShowS
$cshowsPrec :: SeqId -> PMCFG -> ShowS
Show)

-- | the constructors are judgements in 
--
--   - abstract syntax (/ABS/)
-- 
--   - resource (/RES/)
--
--   - concrete syntax (/CNC/)
--
-- and indirection to module (/INDIR/)
data Info =
-- judgements in abstract syntax
   AbsCat   (Maybe (L Context))                                            -- ^ (/ABS/) context of a category
 | AbsFun   (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) (Maybe Bool) -- ^ (/ABS/) type, arrity and definition of a function

-- judgements in resource
 | ResParam (Maybe (L [Param])) (Maybe [Term])   -- ^ (/RES/) the second parameter is list of all possible values
 | ResValue (L Type)                             -- ^ (/RES/) to mark parameter constructors for lookup
 | ResOper  (Maybe (L Type)) (Maybe (L Term))    -- ^ (/RES/)

 | ResOverload [ModuleName] [(L Type,L Term)]         -- ^ (/RES/) idents: modules inherited

-- judgements in concrete syntax
 | CncCat  (Maybe (L Type))             (Maybe (L Term)) (Maybe (L Term)) (Maybe (L Term)) (Maybe PMCFG) -- ^ (/CNC/) lindef ini'zed, 
 | CncFun  (Maybe (Ident,Context,Type)) (Maybe (L Term))                  (Maybe (L Term)) (Maybe PMCFG) -- ^ (/CNC/) type info added at 'TC'

-- indirection to module Ident
 | AnyInd Bool ModuleName                        -- ^ (/INDIR/) the 'Bool' says if canonical
  deriving SeqId -> Info -> ShowS
[Info] -> ShowS
Info -> FilePath
(SeqId -> Info -> ShowS)
-> (Info -> FilePath) -> ([Info] -> ShowS) -> Show Info
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Info] -> ShowS
$cshowList :: [Info] -> ShowS
show :: Info -> FilePath
$cshow :: Info -> FilePath
showsPrec :: SeqId -> Info -> ShowS
$cshowsPrec :: SeqId -> Info -> ShowS
Show

type Type = Term
type Cat  = QIdent
type Fun  = QIdent

type QIdent = (ModuleName,Ident)

data Term =
   Vr Ident                      -- ^ variable
 | Cn Ident                      -- ^ constant
 | Con Ident                     -- ^ constructor
 | Sort Ident                    -- ^ basic type
 | EInt Int                      -- ^ integer literal
 | EFloat Double                 -- ^ floating point literal
 | K String                      -- ^ string literal or token: @\"foo\"@
 | Empty                         -- ^ the empty string @[]@

 | App Term Term                 -- ^ application: @f a@
 | Abs BindType Ident Term       -- ^ abstraction: @\x -> b@
 | Meta {-# UNPACK #-} !MetaId   -- ^ metavariable: @?i@ (only parsable: ? = ?0)
 | ImplArg Term                  -- ^ placeholder for implicit argument @{t}@
 | Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@
 | Typed Term Term               -- ^ type-annotated term
--
-- /below this, the constructors are only for concrete syntax/
 | Example Term String           -- ^ example-based term: @in M.C "foo"
 | RecType [Labelling]           -- ^ record type: @{ p : A ; ...}@
 | R [Assign]                    -- ^ record:      @{ p = a ; ...}@
 | P Term Label                  -- ^ projection:  @r.p@
 | ExtR Term Term                -- ^ extension:   @R ** {x : A}@ (both types and terms)
 
 | Table Term Term               -- ^ table type:  @P => A@
 | T TInfo [Case]                -- ^ table:       @table {p => c ; ...}@
 | V Type [Term]                 -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
 | S Term Term                   -- ^ selection:   @t ! p@

 | Let LocalDef Term             -- ^ local definition: @let {t : T = a} in b@

 | Q  QIdent                     -- ^ qualified constant from a package
 | QC QIdent                     -- ^ qualified constructor from a package

 | C Term Term                   -- ^ concatenation: @s ++ t@
 | Glue Term Term                -- ^ agglutination: @s + t@

 | EPatt Patt                    -- ^ pattern (in macro definition): # p
 | EPattType Term                -- ^ pattern type: pattern T

 | ELincat Ident Term            -- ^ boxed linearization type of Ident
 | ELin Ident Term               -- ^ boxed linearization of type Ident

 | AdHocOverload [Term]          -- ^ ad hoc overloading generated in Rename

 | FV [Term]                     -- ^ alternatives in free variation: @variants { s ; ... }@

 | Alts Term [(Term, Term)]      -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
 | Strs [Term]                   -- ^ conditioning prefix strings: @strs {s ; ...}@
 | Error String                  -- ^ error values returned by Predef.error
  deriving (SeqId -> Term -> ShowS
[Term] -> ShowS
Term -> FilePath
(SeqId -> Term -> ShowS)
-> (Term -> FilePath) -> ([Term] -> ShowS) -> Show Term
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> FilePath
$cshow :: Term -> FilePath
showsPrec :: SeqId -> Term -> ShowS
$cshowsPrec :: SeqId -> Term -> ShowS
Show, Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord)

-- | Patterns
data Patt =
   PC Ident [Patt]        -- ^ constructor pattern: @C p1 ... pn@    @C@ 
 | PP QIdent [Patt]       -- ^ package constructor pattern: @P.C p1 ... pn@    @P.C@ 
 | PV Ident               -- ^ variable pattern: @x@
 | PW                     -- ^ wild card pattern: @_@
 | PR [(Label,Patt)]      -- ^ record pattern: @{r = p ; ...}@  -- only concrete
 | PString String         -- ^ string literal pattern: @\"foo\"@  -- only abstract
 | PInt    Int            -- ^ integer literal pattern: @12@    -- only abstract
 | PFloat Double          -- ^ float literal pattern: @1.2@    -- only abstract
 | PT Type Patt           -- ^ type-annotated pattern

 | PAs Ident Patt         -- ^ as-pattern: x@p
 
 | PImplArg Patt          -- ^ placeholder for pattern for implicit argument @{p}@
 | PTilde   Term          -- ^ inaccessible pattern

 -- regular expression patterns
 | PNeg Patt              -- ^ negated pattern: -p
 | PAlt Patt Patt         -- ^ disjunctive pattern: p1 | p2
 | PSeq Patt Patt         -- ^ sequence of token parts: p + q
 | PMSeq MPatt MPatt      -- ^ sequence of token parts: p + q
 | PRep Patt              -- ^ repetition of token part: p*
 | PChar                  -- ^ string of length one: ?
 | PChars [Char]          -- ^ character list: ["aeiou"]
 | PMacro Ident           -- #p
 | PM QIdent              -- #m.p
  deriving (SeqId -> Patt -> ShowS
[Patt] -> ShowS
Patt -> FilePath
(SeqId -> Patt -> ShowS)
-> (Patt -> FilePath) -> ([Patt] -> ShowS) -> Show Patt
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Patt] -> ShowS
$cshowList :: [Patt] -> ShowS
show :: Patt -> FilePath
$cshow :: Patt -> FilePath
showsPrec :: SeqId -> Patt -> ShowS
$cshowsPrec :: SeqId -> Patt -> ShowS
Show, Patt -> Patt -> Bool
(Patt -> Patt -> Bool) -> (Patt -> Patt -> Bool) -> Eq Patt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Patt -> Patt -> Bool
$c/= :: Patt -> Patt -> Bool
== :: Patt -> Patt -> Bool
$c== :: Patt -> Patt -> Bool
Eq, Eq Patt
Eq Patt
-> (Patt -> Patt -> Ordering)
-> (Patt -> Patt -> Bool)
-> (Patt -> Patt -> Bool)
-> (Patt -> Patt -> Bool)
-> (Patt -> Patt -> Bool)
-> (Patt -> Patt -> Patt)
-> (Patt -> Patt -> Patt)
-> Ord Patt
Patt -> Patt -> Bool
Patt -> Patt -> Ordering
Patt -> Patt -> Patt
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Patt -> Patt -> Patt
$cmin :: Patt -> Patt -> Patt
max :: Patt -> Patt -> Patt
$cmax :: Patt -> Patt -> Patt
>= :: Patt -> Patt -> Bool
$c>= :: Patt -> Patt -> Bool
> :: Patt -> Patt -> Bool
$c> :: Patt -> Patt -> Bool
<= :: Patt -> Patt -> Bool
$c<= :: Patt -> Patt -> Bool
< :: Patt -> Patt -> Bool
$c< :: Patt -> Patt -> Bool
compare :: Patt -> Patt -> Ordering
$ccompare :: Patt -> Patt -> Ordering
$cp1Ord :: Eq Patt
Ord)

-- | Measured pattern (paired with the min & max matching length)
type MPatt = ((Int,Int),Patt)

-- | to guide computation and type checking of tables
data TInfo = 
   TRaw         -- ^ received from parser; can be anything
 | TTyped Type  -- ^ type annontated, but can be anything
 | TComp Type   -- ^ expanded
 | TWild Type   -- ^ just one wild card pattern, no need to expand 
  deriving (SeqId -> TInfo -> ShowS
[TInfo] -> ShowS
TInfo -> FilePath
(SeqId -> TInfo -> ShowS)
-> (TInfo -> FilePath) -> ([TInfo] -> ShowS) -> Show TInfo
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [TInfo] -> ShowS
$cshowList :: [TInfo] -> ShowS
show :: TInfo -> FilePath
$cshow :: TInfo -> FilePath
showsPrec :: SeqId -> TInfo -> ShowS
$cshowsPrec :: SeqId -> TInfo -> ShowS
Show, TInfo -> TInfo -> Bool
(TInfo -> TInfo -> Bool) -> (TInfo -> TInfo -> Bool) -> Eq TInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TInfo -> TInfo -> Bool
$c/= :: TInfo -> TInfo -> Bool
== :: TInfo -> TInfo -> Bool
$c== :: TInfo -> TInfo -> Bool
Eq, Eq TInfo
Eq TInfo
-> (TInfo -> TInfo -> Ordering)
-> (TInfo -> TInfo -> Bool)
-> (TInfo -> TInfo -> Bool)
-> (TInfo -> TInfo -> Bool)
-> (TInfo -> TInfo -> Bool)
-> (TInfo -> TInfo -> TInfo)
-> (TInfo -> TInfo -> TInfo)
-> Ord TInfo
TInfo -> TInfo -> Bool
TInfo -> TInfo -> Ordering
TInfo -> TInfo -> TInfo
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TInfo -> TInfo -> TInfo
$cmin :: TInfo -> TInfo -> TInfo
max :: TInfo -> TInfo -> TInfo
$cmax :: TInfo -> TInfo -> TInfo
>= :: TInfo -> TInfo -> Bool
$c>= :: TInfo -> TInfo -> Bool
> :: TInfo -> TInfo -> Bool
$c> :: TInfo -> TInfo -> Bool
<= :: TInfo -> TInfo -> Bool
$c<= :: TInfo -> TInfo -> Bool
< :: TInfo -> TInfo -> Bool
$c< :: TInfo -> TInfo -> Bool
compare :: TInfo -> TInfo -> Ordering
$ccompare :: TInfo -> TInfo -> Ordering
$cp1Ord :: Eq TInfo
Ord)

-- | record label
data Label = 
    LIdent RawIdent
  | LVar Int
   deriving (SeqId -> Label -> ShowS
[Label] -> ShowS
Label -> FilePath
(SeqId -> Label -> ShowS)
-> (Label -> FilePath) -> ([Label] -> ShowS) -> Show Label
forall a.
(SeqId -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [Label] -> ShowS
$cshowList :: [Label] -> ShowS
show :: Label -> FilePath
$cshow :: Label -> FilePath
showsPrec :: SeqId -> Label -> ShowS
$cshowsPrec :: SeqId -> Label -> ShowS
Show, Label -> Label -> Bool
(Label -> Label -> Bool) -> (Label -> Label -> Bool) -> Eq Label
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c== :: Label -> Label -> Bool
Eq, Eq Label
Eq Label
-> (Label -> Label -> Ordering)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Label)
-> (Label -> Label -> Label)
-> Ord Label
Label -> Label -> Bool
Label -> Label -> Ordering
Label -> Label -> Label
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Label -> Label -> Label
$cmin :: Label -> Label -> Label
max :: Label -> Label -> Label
$cmax :: Label -> Label -> Label
>= :: Label -> Label -> Bool
$c>= :: Label -> Label -> Bool
> :: Label -> Label -> Bool
$c> :: Label -> Label -> Bool
<= :: Label -> Label -> Bool
$c<= :: Label -> Label -> Bool
< :: Label -> Label -> Bool
$c< :: Label -> Label -> Bool
compare :: Label -> Label -> Ordering
$ccompare :: Label -> Label -> Ordering
$cp1Ord :: Eq Label
Ord)

type MetaId = Int

type Hypo     = (BindType,Ident,Term)   -- (x:A)  (_:A)  A  ({x}:A)
type Context  = [Hypo]                  -- (x:A)(y:B)   (x,y:A)   (_,_:A)
type Equation = ([Patt],Term) 

type Labelling = (Label, Type) 
type Assign = (Label, (Maybe Type, Term)) 
type Case = (Patt, Term) 
--type Cases = ([Patt], Term) 
type LocalDef = (Ident, (Maybe Type, Term))

type Param = (Ident, Context) 
type Altern = (Term, [(Term, Term)])

type Substitution =  [(Ident, Term)]

varLabel :: Int -> Label
varLabel :: SeqId -> Label
varLabel = SeqId -> Label
LVar

tupleLabel, linLabel :: Int -> Label
tupleLabel :: SeqId -> Label
tupleLabel SeqId
i = RawIdent -> Label
LIdent (RawIdent -> Label) -> RawIdent -> Label
forall a b. (a -> b) -> a -> b
$! FilePath -> RawIdent
rawIdentS (Char
'p'Char -> ShowS
forall a. a -> [a] -> [a]
:SeqId -> FilePath
forall a. Show a => a -> FilePath
show SeqId
i)
linLabel :: SeqId -> Label
linLabel   SeqId
i = RawIdent -> Label
LIdent (RawIdent -> Label) -> RawIdent -> Label
forall a b. (a -> b) -> a -> b
$! FilePath -> RawIdent
rawIdentS (Char
's'Char -> ShowS
forall a. a -> [a] -> [a]
:SeqId -> FilePath
forall a. Show a => a -> FilePath
show SeqId
i)

theLinLabel :: Label
theLinLabel :: Label
theLinLabel = RawIdent -> Label
LIdent (FilePath -> RawIdent
rawIdentS FilePath
"s")

ident2label :: Ident -> Label
ident2label :: Ident -> Label
ident2label Ident
c = RawIdent -> Label
LIdent (Ident -> RawIdent
ident2raw Ident
c)

label2ident :: Label -> Ident
label2ident :: Label -> Ident
label2ident (LIdent RawIdent
s) = RawIdent -> Ident
identC RawIdent
s
label2ident (LVar SeqId
i)   = FilePath -> Ident
identS (Char
'$'Char -> ShowS
forall a. a -> [a] -> [a]
:SeqId -> FilePath
forall a. Show a => a -> FilePath
show SeqId
i)