content: %-------------------------------=  --------------------------------------------
  \subsection{Directives}
  %-------------------------------=  --------------------------------------------
  
  %if codeOnly || showModuleHeader
  
  > module Directives             (  Formats, parseFormat, Equation, Substs, Subst, parseSubst, Toggles, eval, define, value, nrargs  )
  > where
  >
  > import Control.Applicative
  > import Data.Char              (  isDigit  )
  > import Data.List
  > import Parser
  > import TeXCommands
  > import HsLexer
  > import FiniteMap              (  FiniteMap, (!)  )
  > import qualified FiniteMap as FM
  > import Auxiliaries
  > import Document
  > import Value
  
  %endif
  
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  \subsubsection{@%format@ directives}
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  
  > type Formats                  =  FiniteMap Char Equation
  > type Equation                 =  (Bool, [Bool], [String], [Token])
  
  ks, 20.07.03: The |Equation| type contains the following information:
  does the definition have surrounding parentheses, do the arguments
  have surrounding parentheses, what are the names of the arguments,
  and the tokens to replace the macro with.
  
  ks, 06.09.03: Adding the |nrargs| function that yields the number of
  arguments a formatting directive expects.
  
  > nrargs                        :: Equation -> Int
  > nrargs (_,_,args,_)           =  length args
  
  \NB Die Substution wird nicht als Funktion |[[Token]] -> [Token]|
  repr"asentiert, da math |Pos Token| verlangt.
  
  >
  > parseFormat                   :: Lang -> String -> Either Exc (String, Equation)
  > parseFormat lang s            =  parse lang (equation lang) (convert s)
  
  Format directives. \NB @%format ( = "(\;"@ is legal.
  
  > equation                      :: Lang -> Parser Token (String, Equation)
  > equation lang                 =   do (opt, (f, opts, args)) <- optParen lhs
  >                                      _ <- varsym lang "="
  >                                      r <- many item
  >                                      eof
  >                                      return (f, (opt, opts, args, r))
  >                               <|> do f <- item
  >                                      _ <- varsym lang "="
  >                                      r <- many item
  >                                      eof
  >                                      return (string f, (False, [], [], r))
  >                               -- no RHS, try implicit formatting rules
  >                               <|> do f <- satisfy isVarid <|> satisfy isConid
  >                                      eof
  >                                      return (string f, (False, [], [], tex f))
  
  \Todo{@%format `div1`@ funktioniert nicht.}
  
  >     where
  >     agda                      =  lang == Agda
  >     tex (Varid s) | agda      =  operator s
  >     tex (Conid s) | agda      =  operator s
  >     tex (Varid s)             =  subscript Varid s
  >     tex (Conid s)             =  subscript Conid s
  >     tex (Qual [] s)           =  tex s
  >     tex (Qual (m:ms) s)       =  Conid m : tex (Qual ms s)
  >      -- ks, 03.09.2003: was "tex (Qual m s) = Conid m : tex s";
  >      -- seems strange though ...
  >     tex _                     =  impossible "equation.tex"
  >     subscript f s
  >       | null t && not (null w) && (null v || head w == '_')
  >                               =  underscore f s
  >       | otherwise             =  [f (reverse w)
  >                                  , TeX False
  >                                        (Text ((if   not (null v)
  >                                                then "_{" ++ reverse v ++ "}"
  >                                                else ""
  >                                               ) ++ reverse t))
  >                                  ]
  >         where s'              =  reverse s
  >               (t, u)          =  span (== '\'') s'
  >               (v, w)          =  span isDigit u
  
  >     operator s                =  let parts = splitOn (=='_') s
  >                                      start = "_" `isPrefixOf` s
  >                                      end   = "_" `isSuffixOf` s
  >                                  in  (if start then [Varid "_"] else []) ++
  >                                      Data.List.intersperse (Varid "_") (map Varid parts) ++
  >                                      (if end   then [Varid "_"] else [])
  
  ks, 02.02.2004: I have added implicit formatting via |underscore|.
  The above condition should guarantee that it is (almost) only used in
  cases where previously implicit formatting did not do anything useful.
  The function |underscore| typesets an identifier such as
  |a_b_c| as $a_{b_{c}}$. TODO: Instead of hard-coded subscripting a
  substitution directive should be invoked here.
  
  >     underscore f s
  >                               =  [f t]
  >                                  ++ if null u then []
  >                                               else [TeX False (Text "_{")]
  >                                                    ++
  >                                                    proc_u
  >                                                    ++
  >                                                    [TeX False (Text "}")]
  >         where (t, u)          =  break (== '_') s
  >               tok_u           =  tokenize lang (tail u)
  >               proc_u          =  case tok_u of
  >                                    Left  _  -> [f (tail u)] -- should not happen
  >                                    Right t' -> t'
  
  > lhs                           :: Parser Token (String, [Bool], [String])
  > lhs                           =  do f <- varid <|> conid
  >                                     as <- many (optParen varid)
  >                                     let (opts, args) = unzip as
  >                                     return (f, opts, args)
  
  > optParen                      :: Parser Token a -> Parser Token (Bool, a)
  > optParen p                    =   do _ <- open'; a <- p; _ <- close'; return (True, a)
  >                               <|> do a <- p ; return (False, a)
  >
  > item                          :: Parser Token Token
  > item                          =  satisfy (const True)
  
  > convert                       :: String -> String
  > convert []                    =  []
  > convert ('"' : '"' : s)       =  '"' : convert s
  > convert ('"' : s)             =  '{' : '-' : '"' : convert' s
  > convert (c : s)               =  c : convert s
  >
  > convert'                      :: String -> String
  > convert' []                   =  []
  > convert' ('"' : '"' : s)      =  '"' : convert' s
  > convert' ('"' : s)            =  '"' : '-' : '}' : convert s
  > convert' (c : s)              =  c : convert' s
  
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  \subsubsection{@%subst@ directives}
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  
  > type Substs                   =  FiniteMap Char Subst
  > type Subst                    =  [Doc] -> Doc
  
  > parseSubst                    :: Lang -> String -> Either Exc (String, Subst)
  > parseSubst lang s             =  parse lang (substitution lang) (convert s)
  >
  > substitution                  :: Lang -> Parser Token (String, Subst)
  > substitution lang             =  do s <- varid
  >                                     args <- many varid
  >                                     _ <- varsym lang "="
  >                                     rhs <- many (satisfy isVarid <|> satisfy isTeX)
  >                                     return (s, subst args rhs)
  >   where
  >   subst :: [String] -> [Token] -> Subst
  >   subst args rhs ds           =  catenate (map sub rhs)
  >       where sub (TeX _ d)     =  d
  >             sub (Varid x)     =  FM.fromList (zip args ds) ! x
  >             sub _             =  impossible "substitution.subst.sub"
  > -- TODO: The above lookup can fail badly if unknown variables are used on the rhs of a subst.
  
  \Todo{unbound variables behandeln.}
  ks, 24.10.2008: A bit messy: For Agda, we explicitly exclude "=" from the set
  of varids accepted on the lhs of a directive, because according to the Agda
  lexer, "=" is both a varid and a varsym. This shouldn't matter for Haskell,
  because "=" will never occur in a Varid constructor.
  
  > varid                         :: Parser Token String
  > varid                         =  do x <- satisfy (\ x -> isVarid x && x /= Varid "="); return (string x)
  
  > conid                         :: Parser Token String
  > conid                         =  do x <- satisfy isConid; return (string x)
  
  > varsym                        :: Lang -> String -> Parser Token Token
  > varsym Agda s                 =  satisfy (\ x -> x == Varsym s || x == Varid s) -- Agda has no symbol/id distinction
  > varsym Haskell s              =  satisfy (== (Varsym s))
  >
  > isTeX                         :: Token -> Bool
  > isTeX (TeX _ _)               =  True
  > isTeX _                       =  False
  
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  \subsubsection{Conditional directives}
  % - - - - - - - - - - - - - - - = - - - - - - - - - - - - - - - - - - - - - - -
  
  > type Toggles                  =  FiniteMap Char Value
  
  Auswertung Boole'scher Ausdr"ucke.
  
  > eval                          :: Lang -> Toggles -> String -> Either Exc Value
  > eval lang togs                =  parse lang (expression lang togs)
  >
  > expression                    :: Lang -> Toggles -> Parser Token Value
  > expression lang togs          =  expr
  >   where
  >   expr                        =  do e1 <- appl
  >                                     e2 <- optional (do op <- varsym' lang; e <- expr; return (op, e))
  >                                     return (maybe e1 (\(op, e2') -> sys2 op e1 e2') e2)
  >   appl                        =  do f <- optional not'
  >                                     e <- atom
  >                                     return (maybe e (\_ -> onBool1 not e) f)
  >   atom                        =   do x <- satisfy isVarid; return (value togs (string x))
  >                               <|> do _ <- true'; return (Bool True)
  >                               <|> do _ <- false'; return (Bool False)
  >                               <|> do s <- satisfy isString; return (Str (read (string s)))
  >                               <|> do s <- satisfy isNumeral; return (Int (read (string s)))
  >                               <|> do _ <- open'; e <- expr; _ <- close'; return e
  >
  > sys2                          :: String -> Binary Value
  > sys2 "&&"                     =  onBool2 (&&)
  > sys2 "||"                     =  onBool2 (||)
  > sys2 "=="                     =  onMatching (==) (==) (==)
  > sys2 "/="                     =  onMatching (/=) (/=) (/=)
  > sys2 "<"                      =  onMatching (<) (<) (<)
  > sys2 "<="                     =  onMatching (<=) (<=) (<=)
  > sys2 ">="                     =  onMatching (>=) (>=) (>=)
  > sys2 ">"                      =  onMatching (>) (>) (>)
  > sys2 "++"                     =  onStr2 (++)
  > sys2 "+"                      =  onInt2 (+)
  > sys2 "-"                      =  onInt2 (-)
  > sys2 "*"                      =  onInt2 (*)
  > sys2 "/"                      =  onInt2 div
  > sys2 _                        =  \_ _ -> Undef
  
  Definierende Gleichungen.
  
  > define                        :: Lang -> Toggles -> String -> Either Exc (String, Value)
  > define lang togs              =  parse lang (definition lang togs)
  >
  > definition                    :: Lang -> Toggles -> Parser Token (String, Value)
  > definition lang togs          =  do x <- satisfy isVarid
  >                                     _ <- equal' lang
  >                                     b <- expression lang togs
  >                                     return (string x, b)
  
  Primitive Parser.
  
  > not',  true', false', open', close'
  >                               :: Parser Token Token
  > equal'                        :: Lang -> Parser Token Token
  > equal' lang                   =  varsym lang "="
  > not'                          =  satisfy (== (Varid "not"))
  > true'                         =  satisfy (== (Conid "True"))
  > false'                        =  satisfy (== (Conid "False"))
  > open'                         =  satisfy (== (Special '('))
  > close'                        =  satisfy (== (Special ')'))
  
  > varsym'                       :: Lang -> Parser Token String
  > varsym' lang                  =  do x <- satisfy (isVarsym lang); return (string x)
  
  > isVarsym                      :: Lang -> Token -> Bool
  > isVarsym _ (Varsym _)         =  True
  > isVarsym Agda (Varid _)       =  True  -- for Agda
  > isVarsym _ _                  =  False
  
  > isString                      :: Token -> Bool
  > isString (String _)           =  True
  > isString _                    =  False
  
  > isNumeral                     :: Token -> Bool
  > isNumeral (Numeral _)         =  True
  > isNumeral _                   =  False
  
  Hilfsfunktionen.
  
  > parse                         :: Lang -> Parser Token a -> String -> Either Exc a
  > parse lang p str'             =  do ts <- tokenize lang str'
  >                                     let ts' = map (\t -> case t of TeX _ x -> TeX False x; _ -> t) .
  >                                               filter (\t -> catCode t /= White || isTeX t) $ ts
  >                                     maybe (Left msg) Right (run p ts')
  >     where msg                 =  ("syntax error in directive", str')
  
  Hack: |isTeX t| f"ur |parseSubst|.
  
  > value                         :: Toggles -> String -> Value
  > value togs x                  =  case FM.lookup x togs of
  >     Nothing                   -> Undef
  >     Just b                    -> b
  