content: {- |
  Module      :  ./HasCASL/ParseTerm.hs
  Description :  parser for HasCASL kinds, types, terms, patterns and equations
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  parser for HasCASL kinds, types, terms, patterns and equations
  -}
  
  module HasCASL.ParseTerm where
  
  import Common.AnnoState
  import Common.Id
  import Common.Keywords
  import Common.Lexer
  import Common.Parsec
  import Common.Token
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.HToken
  
  import Text.ParserCombinators.Parsec
  
  import Data.List ((\\))
  import qualified Data.Set as Set
  
  -- * key sign tokens
  
  -- | a colon not followed by a question mark
  colT :: AParser st Token
  colT = asKey colonS
  
  -- * parser for bracketed lists
  
  -- | a generic bracket parser
  bracketParser :: AParser st a -> AParser st Token -> AParser st Token
                -> AParser st Token -> ([a] -> Range -> b) -> AParser st b
  bracketParser parser op cl sep k = do
      o <- op
      (ts, ps) <- option ([], []) $ separatedBy parser sep
      c <- cl
      return $ k ts $ toRange o ps c
  
  -- | parser for square brackets
  mkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b
  mkBrackets p = bracketParser p oBracketT cBracketT anComma
  
  -- | parser for braces
  mkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b
  mkBraces p = bracketParser p oBraceT cBraceT anComma
  
  -- * kinds
  
  -- | parse a simple class name or the type universe as kind
  parseClassId :: AParser st Kind
  parseClassId = fmap ClassKind classId
  
  -- | do 'parseClassId' or a kind in parenthessis
  parseSimpleKind :: AParser st Kind
  parseSimpleKind = parseClassId <|> (oParenT >> kind << cParenT)
  
  -- | do 'parseSimpleKind' and check for an optional 'Variance'
  parseExtKind :: AParser st (Variance, Kind)
  parseExtKind = pair variance parseSimpleKind
  
  -- | parse a (right associative) function kind for a given argument kind
  arrowKind :: (Variance, Kind) -> AParser st Kind
  arrowKind (v, k) = do
      a <- asKey funS
      k2 <- kind
      return $ FunKind v k k2 $ tokPos a
  
  -- | parse a function kind but reject an extended kind
  kind :: AParser st Kind
  kind = do
      k1@(v, k) <- parseExtKind
      arrowKind k1 <|> case v of
          NonVar -> return k
          _ -> unexpected "variance of kind"
  
  -- | parse a function kind but accept an extended kind
  extKind :: AParser st (Variance, Kind)
  extKind = do
      k1 <- parseExtKind
      do k <- arrowKind k1
         return (NonVar, k)
        <|> return k1
  
  -- * type variables
  
  variance :: AParser st Variance
  variance = let l = [CoVar, ContraVar] in
      choice (map ( \ v -> asKey (show v) >> return v) l) <|> return NonVar
  
  -- a (simple) type variable with a 'Variance'
  extVar :: AParser st Id -> AParser st (Id, Variance)
  extVar vp = pair vp variance
  
  -- several 'extVar' with a 'Kind'
  typeVars :: AParser st [TypeArg]
  typeVars = do
      (ts, ps) <- extVar typeVar `separatedBy` anComma
      typeKind False ts ps
  
  allIsNonVar :: [(Id, Variance)] -> Bool
  allIsNonVar = all ( \ (_, v) -> case v of
      NonVar -> True
      _ -> False)
  
  -- 'parseType' a 'Downset' starting with 'lessT' (True means require kind)
  typeKind :: Bool -> [(Id, Variance)] -> [Token]
           -> AParser st [TypeArg]
  typeKind b vs ps = do
      c <- colT
      if allIsNonVar vs then do
          (v, k) <- extKind
          return $ makeTypeArgs vs ps v (VarKind k) $ tokPos c
        else do
          k <- kind
          return $ makeTypeArgs vs ps NonVar (VarKind k) $ tokPos c
    <|> do
      l <- lessT
      t <- parseType
      return $ makeTypeArgs vs ps NonVar (Downset t) $ tokPos l
    <|> if b then unexpected "missing kind" else
            return (makeTypeArgs vs ps NonVar MissingKind nullRange)
  
  -- | add the 'Kind' to all 'extVar' and yield a 'TypeArg'
  makeTypeArgs :: [(Id, Variance)] -> [Token]
               -> Variance -> VarKind -> Range -> [TypeArg]
  makeTypeArgs ts ps vv vk qs =
      zipWith (mergeVariance Comma vv vk) (init ts)
                  (map tokPos ps)
                  ++ [mergeVariance Other vv vk (last ts) qs]
                  where
      mergeVariance c v k (t, NonVar) q = TypeArg t v k rStar 0 c q
      mergeVariance c _ k (t, v) q = TypeArg t v k rStar 0 c q
  
  -- | a single 'TypeArg' (parsed by 'typeVars')
  singleTypeArg :: AParser st TypeArg
  singleTypeArg = do
      as <- typeVars
      case as of
        [a] -> return a
        _ -> unexpected "list of type arguments"
  
  -- | a 'singleTypeArg' put in parentheses
  parenTypeArg :: AParser st (TypeArg, [Token])
  parenTypeArg = do
      o <- oParenT
      a <- singleTypeArg
      p <- cParenT
      return (a, [o, p])
  
  -- | a 'singleTypeArg' possibly put in parentheses
  typeArg :: AParser st (TypeArg, [Token])
  typeArg = do
      a <- singleTypeArg
      return (a, [])
    <|> parenTypeArg
  
  -- | a 'singleTypeArg' put in parentheses as 'TypePattern'
  typePatternArg :: AParser st TypePattern
  typePatternArg = do
      (a, ps) <- parenTypeArg
      return $ TypePatternArg a $ catRange ps
  
  -- * parse special identifier tokens
  
  type TokenMode = [String]
  
  {- | parse a 'Token' of an 'Id' (to be declared)
  but exclude the signs in 'TokenMode' -}
  aToken :: TokenMode -> AParser st Token
  aToken b = pToken $ scanQuotedChar <|> scanDigit <|> scanHCWords <|> placeS
      <|> reserved b scanHCSigns
  
  -- | just 'aToken' only excluding basic HasCASL keywords
  idToken :: AParser st Token
  idToken = aToken [] <|> pToken scanDotWords
  
  -- * type patterns
  
  {- 'TypePatternToken's within 'BracketTypePattern's
  may recusively be 'idToken's.
  Parenthesis are only legal for a 'typePatternArg'. -}
  primTypePatternOrId :: AParser st TypePattern
  primTypePatternOrId = fmap TypePatternToken idToken
      <|> mkBraces typePatternOrId (BracketTypePattern Braces)
      <|> mkBrackets typePatternOrId (BracketTypePattern Squares)
      <|> typePatternArg
  
  -- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
  mixTypePattern :: AParser st TypePattern -> AParser st TypePattern
  mixTypePattern p = do
      ts <- many1 p
      return $ case ts of
         [hd] -> hd
         _ -> MixfixTypePattern ts
  
  -- several 'primTypePatternOrId's possibly yielding a 'MixfixTypePattern'
  typePatternOrId :: AParser st TypePattern
  typePatternOrId = mixTypePattern primTypePatternOrId
  
  {- | those (top-level) 'Token's (less than 'idToken')
  that may appear in 'TypePattern's as 'TypePatternToken'. -}
  typePatternToken :: AParser st TypePattern
  typePatternToken = fmap TypePatternToken $ pToken $ scanHCWords <|> placeS
      <|> reserved hascasl_reserved_tops scanHCSigns
  
  {- | a 'typePatternToken' or something in braces (a 'typePattern'),
  in square brackets (a 'typePatternOrId' covering compound lists)
  or parenthesis ('typePatternArg') -}
  primTypePattern :: AParser st TypePattern
  primTypePattern = typePatternToken
      <|> mkBrackets typePatternOrId (BracketTypePattern Squares)
      <|> mkBraces typePattern (BracketTypePattern Braces)
      <|> typePatternArg
  
  -- several 'primTypePatter's possibly yielding a 'MixfixTypePattern'
  typePattern :: AParser st TypePattern
  typePattern = mixTypePattern primTypePattern
  
  {- * types
  a parsed type may also be interpreted as a kind (by the mixfix analysis) -}
  
  -- | type tokens with some symbols removed
  typeToken :: AParser st Type
  typeToken = fmap TypeToken $ pToken $ scanHCWords <|> placeS <|>
      reserved (hascasl_reserved_tops ++ hascasl_type_ops)
      scanHCSigns
  
  {- | 'TypeToken's within 'BracketType's may recusively be
  'idToken's. Parenthesis may group a mixfix type
  or may be interpreted as a kind later on in a GEN-VAR-DECL. -}
  primTypeOrId :: AParser st Type
  primTypeOrId = fmap TypeToken idToken
      <|> mkBrackets typeOrId (BracketType Squares)
      <|> mkBraces typeOrId (BracketType Braces)
      <|> bracketParser typeOrId oParenT cParenT anComma (BracketType Parens)
  
  mkMixfixType :: AParser st Type -> AParser st Type
  mkMixfixType p = do
      ts <- many1 p
      return $ case ts of
                [hd] -> hd
                _ -> MixfixType ts
  
  mkKindedMixType :: AParser st Type -> AParser st Type
  mkKindedMixType p = do
      t <- mkMixfixType p
      kindAnno t <|> return t
  
  {- | several 'primTypeOrId's possibly yielding a 'MixfixType'
  and possibly followed by a 'kindAnno'. -}
  typeOrId :: AParser st Type
  typeOrId = mkKindedMixType primTypeOrId
  
  -- | a 'Kind' annotation starting with 'colT'.
  kindAnno :: Type -> AParser st Type
  kindAnno t = do
      c <- colT
      k <- kind
      return $ KindedType t (Set.singleton k) $ tokPos c
  
  -- | a typeToken' or a 'BracketType'. Square brackets may contain 'typeOrId'.
  primType :: AParser st Type
  primType = typeToken
      <|> mkBrackets typeOrId (BracketType Squares)
      <|> mkBraces parseType (BracketType Braces)
      <|> bracketParser parseType oParenT cParenT anComma (BracketType Parens)
  
  -- | a 'primType' possibly preceded by 'quMarkT'
  lazyType :: AParser st Type
  lazyType = fmap mkLazyType (quMarkT >> mkMixfixType primType) <|> primType
  
  -- | several 'lazyType's (as 'MixfixType') possibly followed by 'kindAnno'
  mixType :: AParser st Type
  mixType = mkKindedMixType lazyType
  
  -- | 'mixType' possibly interspersed with 'crossT'
  prodType :: AParser st Type
  prodType = do
      (ts, ps) <- mixType `separatedBy` crossT
      return $ mkProductTypeWithRange ts $ catRange ps
  
  -- | a (right associativ) function type
  parseType :: AParser st Type
  parseType = do
      t1 <- prodType
      do a <- arrowT <?> show funS
         t2 <- parseType
         return $ mkTypeAppl
             (TypeName a (toRaw $ funKindWithRange $ posOfId a) 0) [t1, t2]
        <|> return t1
  
  -- | parse one of the four possible 'Arrow's
  arrowT :: AParser st Id
  arrowT = let l = [FunArr, PFunArr, ContFunArr, PContFunArr] in
      choice $ map ( \ a -> do
             t <- asKey $ show a
             return $ mkId [placeTok, t, placeTok]) l
  
  -- | parse a 'TypeScheme' using 'forallT', 'typeVars', 'dotT' and 'parseType'
  typeScheme :: PolyId -> AParser st TypeScheme
  typeScheme (PolyId _ tys ps) = if null tys then do
      f <- forallT
      (ts, cs) <- typeVars `separatedBy` anSemi
      d <- dotT
      t <- parseType
      return $ TypeScheme (concat ts) t $ toRange f cs d
    <|> fmap simpleTypeScheme parseType
    else do
      t <- parseType
      return $ TypeScheme tys t ps
  
  -- * varDecls and genVarDecls
  
  -- | comma separated 'var' with 'varDeclType'
  varDecls :: AParser st [VarDecl]
  varDecls = do
     (vs, ps) <- var `separatedBy` anComma
     varDeclType vs ps
  
  -- | a type ('parseType') following a colon
  varDeclType :: [Id] -> [Token] -> AParser st [VarDecl]
  varDeclType vs ps = do
      c <- colonST
      t <- parseType
      return $ makeVarDecls vs ps t $ tokPos c
  
  -- | attach the 'Type' to every 'Var'
  makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl]
  makeVarDecls vs ps t q = zipWith ( \ v -> VarDecl v t Comma . tokPos)
      (init vs) ps ++ [VarDecl (last vs) t Other q]
  
  {- | either like 'varDecls' or declared type variables.
  A 'GenVarDecl' may later become a 'GenTypeVarDecl'. -}
  genVarDecls :: AParser st [GenVarDecl]
  genVarDecls = fmap (map ( \ g -> case g of
      GenTypeVarDecl (TypeArg i v MissingKind _ n s ps) ->
          GenTypeVarDecl (TypeArg i v (VarKind universe)
                                                rStar n s ps)
      _ -> g)) $ do
      (vs, ps) <- extVar var `separatedBy` anComma
      let other = fmap (map GenTypeVarDecl) (typeKind True vs ps)
      if allIsNonVar vs then fmap (map GenVarDecl)
          (varDeclType (map fst vs) ps) <|> other
        else other
  
  -- * patterns
  
  {- | different legal 'TermToken's possibly excluding 'funS' or
  'equalS' for case or let patterns resp. -}
  tokenPattern :: TokenMode -> AParser st Term
  tokenPattern b = fmap TermToken (aToken b <|> pToken (string "_"))
  -- a single underscore serves as wildcard pattern
  
  -- | 'tokenPattern' or 'BracketTerm'
  primPattern :: TokenMode -> AParser st Term
  primPattern b = tokenPattern b
      <|> mkBrackets pattern (BracketTerm Squares)
      <|> mkBraces pattern (BracketTerm Braces)
      <|> bracketParser (pattern <|> varTerm <|> qualOpName)
            oParenT cParenT anComma (BracketTerm Parens)
  
  mkMixfixTerm :: [Term] -> Term
  mkMixfixTerm ts = case ts of
      [hd] -> hd
      _ -> MixfixTerm ts
  
  -- | several 'typedPattern'
  mixPattern :: TokenMode -> AParser st Term
  mixPattern = fmap mkMixfixTerm . many1 . asPattern
  
  -- | a possibly typed ('parseType') pattern
  typedPattern :: TokenMode -> AParser st Term
  typedPattern b = do
      t <- primPattern b
      do c <- colT
         ty <- parseType
         return $ MixfixTerm [t, MixTypeTerm OfType ty $ tokPos c]
        <|> return t
  
  -- | top-level pattern (possibly 'AsPattern')
  asPattern :: TokenMode -> AParser st Term
  asPattern b = do
      v <- typedPattern b
      case v of
        TermToken tt -> if isPlace tt then return v else do
            c <- asKey asP
            t <- typedPattern b
            return $ AsPattern (VarDecl (mkId [tt]) (MixfixType [])
                                Other $ tokPos c) t $ tokPos c
          <|> return v
        _ -> return v
  
  -- | an unrestricted 'asPattern'
  pattern :: AParser st Term
  pattern = mixPattern []
  
  myChoice :: [(AParser st Token, a)] -> AParser st (a, Token)
  myChoice = choice . map ( \ (p, a) -> do
     t <- p
     return (a, t))
  
  -- | a 'Total' or 'Partial' lambda dot
  lamDot :: AParser st (Partiality, Token)
  lamDot = myChoice [ (choice $ map (asKey . (++ exMark)) [dotS, cDot], Total)
                    , (dotT, Partial)]
  
  -- | patterns between 'lamS' and 'lamDot'
  lamPattern :: AParser st [Term]
  lamPattern =
      (lookAhead lamDot >> return []) <|> typedPattern [] <:> lamPattern
  
  -- * terms
  
  {- | 'Token's that may occur in 'Term's including literals
     'scanFloat', 'scanString' but excluding 'ifS', 'whenS' and 'elseS'
     to allow a quantifier after 'whenS'. In case-terms also 'barS' will
     be excluded on the top-level. -}
  
  tToken :: TokenMode -> AParser st Token
  tToken b = pToken (scanFloat
      <|> scanString
      <|> scanQuotedChar <|> scanDotWords
      <|> reserved [ifS, whenS, elseS] scanHCWords
      <|> reserved b scanHCSigns
      <|> placeS <?> "id/literal")
  
  -- | 'tToken' as 'Term' plus 'exEqual' and 'equalS'
  termToken :: TokenMode -> AParser st Term
  termToken b = fmap TermToken (asKey exEqual <|> asKey equalS <|> tToken b)
  
  -- | 'termToken' plus 'BracketTerm's
  primTerm :: TokenMode -> AParser st Term
  primTerm b = termToken b
      <|> mkBraces term (BracketTerm Braces)
      <|> mkBrackets term (BracketTerm Squares)
      <|> bracketParser termInParens oParenT cParenT anComma (BracketTerm Parens)
  
  -- | how the keyword 'inS' should be treated
  data InMode = NoIn   -- ^ next 'inS' belongs to 'letS'
              | WithIn -- ^ 'inS' is the element test
  
  -- | all 'Term's that start with a unique keyword
  baseTerm :: (InMode, TokenMode) -> AParser st Term
  baseTerm b = ifTerm b
      <|> whenTerm b
      <|> exTerm b
      <|> lambdaTerm b
      <|> caseTerm b
      <|> letTerm b
  
  -- | 'whenS' possibly followed by an 'elseS'
  whenTerm :: (InMode, TokenMode) -> AParser st Term
  whenTerm b = do
      i <- asKey whenS
      c <- mixTerm b
      let l1 = [TermToken i, c]
      do t <- asKey elseS
         e <- mixTerm b
         return $ MixfixTerm $ l1 ++ [TermToken t, e]
        <|> return (MixfixTerm l1)
  
  {- | 'ifS' possibly followed by 'thenS' and 'elseS'
  yielding a 'MixfixTerm' -}
  ifTerm :: (InMode, TokenMode) -> AParser st Term
  ifTerm b = do
      i <- asKey ifS
      c <- mixTerm b
      let l1 = [TermToken i, c]
      do t <- asKey thenS
         e <- mixTerm b
         let l2 = l1 ++ [TermToken t, e]
         do s <- asKey elseS
            f <- mixTerm b
            return $ MixfixTerm $ l2 ++ [TermToken s, f]
           <|> return (MixfixTerm l2)
        <|> return (MixfixTerm l1)
  
  -- | unrestricted terms including qualified names
  termInParens :: AParser st Term
  termInParens = term <|> varTerm <|> qualOpName <|> qualPredName
  
  -- | a qualified 'var'
  varTerm :: AParser st Term
  varTerm = do
      v <- asKey varS
      i <- var
      c <- colonST
      t <- parseType
      return $ QualVar $ VarDecl i t Other $ toRange v [] c
  
  -- | 'opS' or 'functS'
  opBrand :: AParser st (Token, OpBrand)
  opBrand = pair (asKey opS) (return Op)
      <|> pair (asKey functS) (return Fun)
  
  parsePolyId :: AParser st PolyId
  parsePolyId = do
      l <- try ite <|> start hcKeys
      if isPlace (last l)
        then return $ PolyId (Id l [] nullRange) [] nullRange else do
          (cs, ps) <- option ([], nullRange) (try $ comps hcKeys)
          (tys, qs) <- option ([], nullRange) $
                  bracketParser typeVars oBracketT cBracketT semiT (,)
          u <- many placeT
          return $ PolyId (Id (l ++ u) cs ps) (concat tys) qs
  
  -- | a qualified operation (with 'opBrand')
  qualOpName :: AParser st Term
  qualOpName = do
      (v, b) <- opBrand
      i <- parsePolyId
      c <- colonST
      t <- typeScheme i
      return $ QualOp b i t [] Infer $ toRange v [] c
  
  -- | a qualified predicate
  qualPredName :: AParser st Term
  qualPredName = do
      v <- asKey predS
      i <- parsePolyId
      c <- colT
      t <- typeScheme i
      let p = toRange v [] c
      return $ QualOp Pred i (predTypeScheme p t) [] Infer p
  
  {- | a qualifier expecting a further 'Type'.
  'inS' is rejected for 'NoIn' -}
  typeQual :: InMode -> AParser st (TypeQual, Token)
  typeQual m = myChoice $ (colT, OfType) : (asT, AsType) : case m of
      NoIn -> []
      WithIn -> [(asKey inS, InType)]
  
  -- | a qualifier plus a subsequent type as mixfix term component
  qualAndType :: InMode -> AParser st Term
  qualAndType i = do
    (q, p) <- typeQual i
    ty <- parseType
    return $ MixTypeTerm q ty $ tokPos p
  
  -- | a possibly type qualified ('typeQual') 'primTerm' or a 'baseTerm'
  typedTerm :: (InMode, TokenMode) -> AParser st Term
  typedTerm (i, b) = do
      t <- primTerm b
      tys <- many $ qualAndType i
      return $ if null tys then t else MixfixTerm $ t : tys
    <|> baseTerm (i, b)
  
  -- | several 'typedTerm's yielding a 'MixfixTerm'
  mixTerm :: (InMode, TokenMode) -> AParser st Term
  mixTerm = fmap mkMixfixTerm . many1 . typedTerm
  
  -- | keywords that start a new item
  hasCaslStartKeywords :: [String]
  hasCaslStartKeywords =
      dotS : cDot : (hascasl_reserved_words \\ [existsS, letS, caseS])
  
  -- | a 'mixTerm' followed by 'whereS' and equations separated by 'optSemi'
  whereTerm :: (InMode, TokenMode) -> AParser st Term
  whereTerm b = do
      t <- mixTerm b
      do p <- asKey whereS
         (es, ps, _ans) <- itemAux hasCaslStartKeywords $
           patternTermPair [equalS] b equalS
           -- ignore collected annotations
         return $ LetTerm Where es t $ catRange $ p : ps
        <|> return t
  
  -- | a 'whereTerm' called with ('WithIn', [])
  term :: AParser st Term
  term = whereTerm (WithIn, [])
  
  -- | a 'Universal', 'Unique' or 'Existential' 'QuantifiedTerm'
  exQuant :: AParser st (Token, Quantifier)
  exQuant = choice $ map (\ (v, s) -> pair (asKey s) $ return v)
    [ (Universal, forallS)
    , (Unique, existsS ++ exMark)
    , (Existential, existsS) ]
  
  -- | a (possibly unique) existential 'QuantifiedTerm'
  exTerm :: (InMode, TokenMode) -> AParser st Term
  exTerm b = do
      (p, q) <- exQuant
      (vs, ps) <- varDecls `separatedBy` anSemi
      d <- dotT
      f <- mixTerm b
      return $ QuantifiedTerm q (map GenVarDecl $ concat vs) f $ toRange p ps d
  
  lamDecls :: AParser st [Term]
  lamDecls = try ((do
      (vs, _) <- separatedBy varDecls anSemi
      lookAhead lamDot
      return $ case concat vs of
        [VarDecl (Id [t] [] _) ty _ ps] ->
            -- this may be a constant constructor
            [MixfixTerm [TermToken t, MixTypeTerm OfType ty ps]]
        vss -> map QualVar vss) <?> "VAR-DECL") <|> lamPattern
  
  -- | a 'LambdaTerm'
  lambdaTerm :: (InMode, TokenMode) -> AParser st Term
  lambdaTerm b = do
      l <- asKey lamS
      pl <- lamDecls
      (k, d) <- lamDot
      t <- mixTerm b
      return $ LambdaTerm (if null pl then [BracketTerm Parens [] nullRange]
                           else pl) k t $ toRange l [] d
  
  -- | a 'CaseTerm' with 'funS' excluded in 'patternTermPair'
  caseTerm :: (InMode, TokenMode) -> AParser st Term
  caseTerm (i, _) = do
      c <- asKey caseS
      t <- term
      o <- asKey ofS
      (ts, ps) <- patternTermPair [funS] (i, [barS]) funS `separatedBy` barT
      return $ CaseTerm t ts $ catRange $ c : o : ps
  
  {- | a 'LetTerm' with 'equalS' excluded in 'patternTermPair'
  (called with 'NoIn') -}
  letTerm :: (InMode, TokenMode) -> AParser st Term
  letTerm b = do
      l <- asKey letS
      (es, ps) <- patternTermPair [equalS] (NoIn, []) equalS `separatedBy` anSemi
      i <- asKey inS
      t <- mixTerm b
      return $ LetTerm Let es t $ toRange l ps i
  
  -- | a customizable pattern equation
  patternTermPair :: TokenMode -> (InMode, TokenMode) -> String
                  -> AParser st ProgEq
  patternTermPair b1 b2 sep = do
      p <- mixPattern b1
      s <- asKey sep
      t <- mixTerm b2
      return $ ProgEq p t $ tokPos s
  