BuildConstantTable.hs

{-# LANGUAGE GADTs, KindSignatures, DataKinds, Rank2Types #-}
{-# LANGUAGE LambdaCase #-}

module BuildConstantTable where

import Dedukti.AbsDedukti
import Dedukti.PrintDedukti
import Dedukti.ErrM

import CommonConcepts (lookupConstant, mainCats, symbolicCats, gfCatMap)
import DeduktiTheoryAPI
import DeduktiOperations
import Lexing (lextex)
import Semantics (SemDefs, NLGDefs, readSemDef)

import PGF

import Utils (split, splitOutside)

import qualified Data.Map as M
import qualified Data.Set as S
import Data.List (partition, sort, groupBy, intersperse, mapAccumL, nub, dropWhileEnd)
import Data.Char (isDigit, isAlpha, isSpace)

type GFTree = PGF.Tree
type Fun = GFTree
type FunProfile = (Fun, Profile)
type Cat = CId
type Formalism = String

showGFTree :: GFTree -> String
showGFTree = showExpr []

showFunProfile :: FunProfile -> String
showFunProfile (f, p) = showGFTree f ++ " " ++ showProfile p

-- OK to fail, because it should stop compilation
parseFunProfile :: PGF -> Language -> Maybe Int -> String -> FunProfile
parseFunProfile pgf lang mdrop s = case tryParseFunProfile pgf lang mdrop s of
  Ok fp -> fp
  Bad s -> error s

-- used for parsing line by line
tryParseFunProfile :: PGF -> Language -> Maybe Int -> String -> Err FunProfile
tryParseFunProfile pgf lang mdrop s = case s of
  '"':cs -> case parseExample pgf lang (init cs) of
    [] -> Bad $ "cannot parse example: " ++ s
    tp@(t, p):_ -> case (mdrop, p) of   ---- TODO: if many parses?
      (Nothing, _) -> return tp
      (Just k, NoProfile) -> return (t, DropProfile k)
      (Just k, DropProfile n) | k == n -> return (t, DropProfile k)
      (Just k, _) -> Bad $ "conflicting profile information in " ++ s ++ ": Drop " ++ show k ++ " vs. " ++ showProfile p
  -- a tree with its argument profile, as printed by printSymbolTable: f x [1,3]
  _ | Just (t, is) <- treeWithProfile s, mdrop == Nothing -> return (readGFTree t, PermProfile is)
  _ -> return (readGFTree s, maybe NoProfile DropProfile mdrop)
 where
  -- "f x [1,3]" -> Just ("f x", [1,3]); "c []" -> Just ("c", [])
  treeWithProfile str =
    let t = dropWhileEnd isSpace str
        (revProf, revBody) = break (== '[') (reverse (init t))
        prof = reverse revProf
        body = dropWhileEnd isSpace (reverse (drop 1 revBody))
    in if not (null t) && last t == ']' && not (null revBody) && not (null body)
          && all (\c -> isDigit c || c == ',') prof
       then Just (body, if null prof then [] else map read (split ',' prof))
       else Nothing


-- no separate drop table assumed here; could be done by preproc in general
tryParseConstantTableEntry :: PGF -> Language -> String -> Err (QIdent, ConstantTableEntry)
tryParseConstantTableEntry pgf lang s = do
  let qid:gids = splitEntry s
  let (latexs, gfids) = partition ((=='$') . head) gids
  let macros = [macroName qid i | (_, i) <-  zip latexs [0..]]
  annots <- mapM (tryParseFunProfile pgf lang Nothing) (gfids ++ macros) -- Nothing as no separate drop table
  let entry = mkConstantTableEntry pgf annots
  return (QIdent qid, entry)

parseExample :: PGF -> Language -> String -> [FunProfile]
parseExample pgf lang =
    map extract . parse pgf lang (maybe undefined id (readType "Example")) . lexex
  where
   extract t = case unApp t of
     Just (_, ex:args) -> case getProfile args of
       Just p -> (ex, p)
       _ -> (ex, NoProfile)
     _ -> error $ "cannot get example from: " ++ showGFTree t

   lexex s = case s of
     c:' ':cs -> c : ' ' :lextex cs  -- don't uncap first letter
     c:_ | isAlpha c -> case lextex s of  -- don't uncap first letter, but lex the
       _:ws -> c : ws                    -- whole first word (French l'action)
       ws -> ws
     _ -> lextex s

   getProfile args = do
     let iargs = [i | Just (f, [x]) <- map unApp args, showCId f == "IntArgument", Just i <- [unInt x]]
     if length iargs == length args
       then return (PermProfile iargs)
       else Nothing


readGFTree :: String -> GFTree
readGFTree s = case s of
  '\\':_ -> mkApp (mkCId s) []
  _ -> maybe (error ("cannot parse as GFTree: " ++ s)) id (readExpr s)

------

data SymbolTable = SymbolTable {
  constantTable :: ConstantTable,
  backConstantTable :: BackConstantTable,
  conversionTable :: ConversionTable,
  dropTable :: DropTable,
  showTable :: ShowTable,
  macroTable :: MacroTable,
  semanticsTable :: SemDefs,
  nlgTable :: NLGDefs,
  builtinSet :: S.Set QIdent,
  excludedConstants :: S.Set QIdent,
  implicitTypes :: [String],  -- #IMPLICIT: types of variables left implicit, as Dedukti text
  -- #HIDE c i j ...: the arguments of c not shown in readings (the implicit
  -- arguments of Lean), counted from 1; the entries of c count the others
  hideTable :: M.Map QIdent [Int],
  -- #COERCION c k: c is read as its k'th argument (counted before #HIDE)
  coercionTable :: M.Map QIdent Int
  }

-- conversion from Dk to GF, with synonyms and category information
type ConstantTable = M.Map QIdent ConstantTableEntry

-- conversion from Dk to other formalisms
type ConversionTable = M.Map Formalism (M.Map QIdent QIdent)

-- conversions in Dk that drop a number of initial arguments
--- redundant with profiles, except for proofs
type DropTable = M.Map QIdent Int

-- which arguments of a proof-building constant are shown in a proof text:
-- the rule's premisses, rather than the propositions and objects it is also
-- applied to.  #DROP k is the special case "all but the first k".
type ShowTable = M.Map QIdent Profile

-- definitions of macros to be converted to \newcommand in LaTeX
type MacroTable = M.Map String (Int, String)

data ConstantTableEntry = ConstantTableEntry {
  primary   :: (FunProfile, Type),
  symbolics :: [(FunProfile, Type)],
  synonyms  :: [(FunProfile, Type)]
  }

allGFFuns :: ConstantTable -> QIdent -> [(FunProfile, Type)]
allGFFuns table qident = maybe [] merge $ M.lookup qident table where
  merge entry = primary entry : symbolics entry ++ synonyms entry

-- shown in the form that can be parsed as a constant table
showConstantTable :: ConstantTable -> String
showConstantTable = unlines . map prEntry . M.toList where
  prEntry :: (QIdent, ConstantTableEntry) -> String
  prEntry (QIdent q, entry) =
    unwords $ [q, ":"] ++
    intersperse "|" (map (showFunProfile . fst) (primary entry : synonyms entry ++ symbolics entry))

-- shown in a longer format; not currently used
showConstantTableLong :: ConstantTable -> String
showConstantTableLong = concat . map prEntry . M.toList where
  prEntry :: (QIdent, ConstantTableEntry) -> String
  prEntry (QIdent q, entry) =
    unlines $ [
      q ++ ":"
      ] ++
      map ("  " ++) [
        "primary: " ++ prTyping (primary entry),
        "symbolics: " ++ unwords (map prTyping (symbolics entry)),
        "synonyms: " ++ unwords (map prTyping (synonyms entry))
      ]
  prTyping (funprof, typ) = showFunProfile funprof ++ " : " ++ showType [] typ ++ " ;"


-- maps GF idents to original "Dk" idents; the Profile is the original one, to be applied backwards
type BackConstantTable = M.Map Fun [(QIdent, Profile)] 

type BuiltinSet = S.Set QIdent -- built-in constants not expected in ConstantTable

buildBackConstantTable :: ConstantTable -> BackConstantTable
buildBackConstantTable table = M.fromListWith (++) [
  (fun, [(qid, profile)]) | 
    (qid, entry) <- M.toList table,
    (fun, profile) <- map fst (primary entry : symbolics entry ++ synonyms entry)
  ]

---- TODO: make this accessible from RunInformath
printBackTable ::  BackConstantTable -> String
printBackTable = unlines . map prEntry . M.toList where
  prEntry :: (Fun, [(QIdent, Profile)]) -> String
  prEntry (f, qids) = showGFTree f ++ ": " ++ unwords [g ++ showProfile prof | (QIdent g, prof) <- qids]

-- | Drop Dedukti comments (; ... ;), which can span lines and nest, keeping
-- the lines themselves, so that a comment is not read as an entry.
stripDkComments :: [String] -> [String]
stripDkComments = lines . strip (0 :: Int) . unlines
  where
    strip d s = case s of
      '(':';':r -> strip (d+1) r
      ';':')':r | d > 0 -> strip (d-1) r
      '\n':r -> '\n' : strip d r
      c:r | d == 0 -> c : strip d r
      _:r -> strip d r
      [] -> []

buildSymbolTable :: PGF -> Language -> [String] -> SymbolTable
buildSymbolTable pgf lang ls = SymbolTable {
  constantTable = constantTable,
  backConstantTable = backConstantTable,
  conversionTable = conversionTable,
  dropTable = dropTable,
  showTable = showTable,
  macroTable = macroTable,
  semanticsTable = semanticsTable,
  nlgTable = nlgTable,
  builtinSet = builtinSet,
  implicitTypes = implicitTypes,
  hideTable = M.fromList [(QIdent c, map read ns) | "#HIDE":c:ns <- entrylines],
  coercionTable = M.fromList [(QIdent c, read k) | ["#COERCION", c, k] <- entrylines],
  excludedConstants = S.fromList [QIdent c | line <- filter isExclude (entrylines), c <- tail line]
  }
 where
    entrylines = filter (not . null) (map words (stripDkComments ls))
    constantlines = filter isConstantEntry entrylines
    conversionlines = filter isConversion entrylines
    droplines = filter isDrop entrylines
    showlines = filter isShow entrylines
    macrolines = filter isMacro entrylines
    builtinlines = filter isBuiltin entrylines
    implicitlines = filter isImplicit entrylines
    semanticslines = filter isSemantics entrylines
    nlglines = filter isNLG entrylines
    -- every latex form of every constant line, numbered once for the whole
    -- table, so that constantTable and macroTable give the same macro the same
    -- name; see macroName
    numberedlines = snd (mapAccumL numberLine 0 (map (splitEntry . unwords) constantlines))
      where
        numberLine n entry = case entry of
          qid:gids -> let latexs = [gid | gid@('$':_) <- gids]
                      in (n + length latexs,
                          (entry, [macroName qid i | i <- [n .. n + length latexs - 1]]))
          _ -> (n, (entry, []))
    constantTable = M.fromList [
        (QIdent qid, mkConstantTableEntry pgf
           (map (parseFunProfile pgf lang (ifDrop (QIdent qid))) gfids ++
            [macroProfile (ifDrop (QIdent qid)) latex macro | (latex, macro) <- zip latexs macros])) |
                     (qid:gids@(_:_), macros) <- numberedlines,
           let gfids = [gid | gid <- gids, head gid /= '$'],
           let latexs = [gid | gid@('$':_) <- gids]
           ]
    conversionTable = M.fromList [
        (form, M.fromList [(QIdent d, QIdent f) | _:d:f:_ <- fids]) |
       fids@((form:_):_) <- groupBy (\x y -> head x == head y) (sort (map tail conversionlines))]
    backConstantTable = buildBackConstantTable constantTable
    dropTable = M.fromList [(QIdent c, read n) | _:c:n:_ <- droplines]
    showTable = M.fromList (
        [(QIdent c, DropProfile (read n)) | _:c:n:_ <- droplines] ++
        [(QIdent c, prof) | _:c:rest <- showlines, Just prof <- [readProfile (concat rest)]])
    ifDrop qid = M.lookup qid dropTable --- copy dropTable entry to profile
    macroTable = M.fromList (
        [(c, (read n, d)) | _:rest <- macrolines, let [c, n, d] = splitNewcommand (unwords rest)] ++
        [mkMacro name gid |
          (_:gids, names) <- numberedlines,
          (gid, name) <- zip [gid | gid@('$':_) <- gids] names])
    builtinSet = S.fromList [QIdent c | _:cs <- builtinlines, c <- cs]
    implicitTypes = [normalizeType (unwords ws) | _:ws <- implicitlines]
    semanticsTable = M.fromList [readSemDef (unwords ws) | _:ws <- semanticslines]
    nlgTable = M.fromListWith (++) [(c, [f]) | _:ws <- nlglines, let (c, f) = readSemDef (unwords ws)]
    
    isConstantEntry line = head (head line) /= '#'
    isConversion line = head line == "#CONV"
    isDrop line = head line == "#DROP"
    isShow line = head line == "#SHOW"
    isMacro line = head line == "#MACRO"
    isBuiltin line = head line == "#BUILTIN"
    isImplicit line = head line == "#IMPLICIT"
    isSemantics line = head line == "#SEMANTICS"
    isNLG line = head line == "#NLG"
    isExclude line = head line == "#EXCLUDE"

-- | A type as written in #IMPLICIT or printed from Dedukti, for comparison:
-- without parentheses and with single spaces
normalizeType :: String -> String
normalizeType = unwords . words . map (\c -> if c == '(' || c == ')' then ' ' else c)

splitEntry :: [Char] -> [String]
splitEntry s = case splitOutside '$'  '|' s of
  fg : ws -> split ':' fg ++ ws
  _ -> []

-- works on \newcommand{\foo}[n]{def}, also \renewcommand and with no [n]
splitNewcommand :: String -> [String]
splitNewcommand s = case break (=='{') s of
  (_, _:rest) -> case break (=='}') rest of
    (macro, _:mrest) -> macro : case mrest of
      '[':nrest -> case break (==']') nrest of
        (n@(_:_), _:drest) | all isDigit n -> n : [init (tail drest)]
      _ -> "0" : [init (tail mrest)]
    _ -> error ("expected valid newcommand, found: " ++ s)
  _ -> error ("expected valid newcommand, found: " ++ s)


-- | The macro of an inline LaTeX form such as $#4 \\circ #5$ takes only the
-- arguments the form uses, renumbered from #1 in increasing order, so that
-- the macro of a constant with many arguments (the implicit types of type
-- theory, say) stays within the four that the grammar can apply a macro to,
-- and so that arguments the form leaves out are not printed after it.  The
-- constant gets the matching profile, see macroProfile.
mkMacro :: String -> String -> (String, (Int, String))
mkMacro name s = (name, (length used, renumberLatexArgs used body))
 where
   body = init (tail s)
   used = latexArgs body

-- | The distinct arguments #k of a LaTeX form, in increasing order.
latexArgs :: String -> [Int]
latexArgs = S.toList . S.fromList . go
 where
   go s = case s of
     '#':c:cs | isDigit c -> read [c] : go cs --- only one-digit arguments
     _:cs -> go cs
     _ -> []

-- | #k becomes #i where k is the i'th of the used arguments.
renumberLatexArgs :: [Int] -> String -> String
renumberLatexArgs used s = case s of
  '#':c:cs | isDigit c -> '#' : show (position (read [c])) ++ renumberLatexArgs used cs
  c:cs -> c : renumberLatexArgs used cs
  [] -> []
 where
   position k = length (takeWhile (/= k) used) + 1

-- | The profile of a constant shown by the macro of an inline LaTeX form:
-- the arguments that the form uses, none if it uses none, unless a #DROP
-- line already says which arguments to show.
macroProfile :: Maybe Int -> String -> String -> FunProfile
macroProfile mdrop latex macro = case mdrop of
  Just k -> (readGFTree macro, DropProfile k)
  Nothing -> (readGFTree macro, PermProfile used)
 where
   used = latexArgs (init (tail latex))

-- | The LaTeX name of the i'th macro of the whole symbol table.  A LaTeX
-- control sequence can only hold letters, so the constant's own name cannot
-- make the macro unique: digits and underscores would have to be dropped, and
-- card0, card1, card2 would all become \cardMACRo, the last \newcommand
-- silently winning.  The alphabetic part of the name is therefore only a
-- readable stem, and uniqueness comes from the index, spelled in letters:
-- MACRoA, MACRoB, ..., MACRoZ, MACRoAA, MACRoAB, ...  The index is global to
-- the symbol table, so no two macros can collide whatever the constants are
-- called.
macroName :: String -> Int -> String
macroName c i = "\\" ++ filter isAlpha c ++ "MACRo" ++ letterIndex i

-- | 0 -> "A", 25 -> "Z", 26 -> "AA", 27 -> "AB", ... (bijective base 26)
letterIndex :: Int -> String
letterIndex i = go i ""
 where
   go n acc = case divMod n 26 of
     (0, r) -> toEnum (fromEnum 'A' + r) : acc
     (q, r) -> go (q - 1) (toEnum (fromEnum 'A' + r) : acc)

mkConstantTableEntry :: PGF -> [FunProfile] -> ConstantTableEntry
mkConstantTableEntry _ [] = error "constant table entry cannot be empty"
mkConstantTableEntry pgf (funp@(fun, _) : funps) = ConstantTableEntry {
  primary = (funp, funtype pgf fun),
  symbolics = [(f, typ) | (f, typ) <- symbs],
  synonyms = [(f, typ) | (f, typ) <- syns]
  }
 where
 
   funtype _ = inferFunType pgf

   -- the symbolic forms are the $...$ ones, the first form included; the
   -- verbal ones are the "..." ones and GF functions, the primary among them
   symbs = [fpt | fpt <- (funp, funtype pgf fun) : allfuns, isSymbolic (snd fpt)]
   syns = [fpt | fpt <- allfuns, not (isSymbolic (snd fpt))]
   allfuns = [(fp, funtype pgf f) | fp@(f,_) <- funps]
   isSymbolic typ = case unType typ of
     (_, cat, _) -> S.member (showCId cat) symbolicCats


-- PGF: inferExpr :: PGF -> Expr -> Either TcError (Expr, Type)

inferFunType :: PGF -> Fun -> Type
inferFunType pgf fun = case inferExpr pgf fun of
  Right (_, typ) -> typ
  _ -> case showGFTree fun of
     '\'':'\\':_ -> mkType [] (mkCId "MACRO") []
     _ -> error ("when building symbol table entry: cannot infer type of " ++ showGFTree fun)


type DkType = ([Dedukti.AbsDedukti.Hypo], Exp)

mismatchingTypes :: MacroTable -> DkType -> Type -> Fun -> Maybe ((String, Int), ([String], Int))
mismatchingTypes mt dktyp gftyp fun = arityMismatch dktyp (unType gftyp) where

  arityMismatch (dkhypos, typ) (gfhypos, cid, _) =
    let (dka, gfa) = (dkArity (binderCat cid) dkhypos typ, (gfCats cid, gfArity gfhypos cid)) in
    if not (compatible dka gfa)
    then Just (dka, gfa)
    else Nothing
    
  compatible (dkcat, dar) (gfcats, gar) = dar == gar && elem dkcat gfcats
  
  gfArity gfhypos cid = case showCId cid of
    "MACRO" -> maybe 0 fst (M.lookup (tail (filter (/='\'') (showGFTree fun))) mt)
    c | S.member c mainCats -> length gfhypos
    c -> case M.lookup c gfCatMap of
      Just (_, args) -> length args
      _ -> length gfhypos
      
  gfCats cid = case showCId cid of
    "MACRO" -> S.toList mainCats --- uncertain; any may work
    c -> case M.lookup c gfCatMap of
       Just ("Exp", _) -> ["Exp", "Kind", "ProofExp", "Proof"]
       Just ("Kind", _) -> ["Exp", "Kind", "Prop"]
       Just ("Proof", _) -> ["Exp", "Kind", "ProofExp", "Proof"]
       Just ("Prop", _) -> ["Exp", "Kind", "Prop"]
       Just (val, _) -> [val]
       _ -> ["UNKNOWN-GF"] ---
       
  -- a function argument is one argument, except for a binder, which shows
  -- its bound variables as arguments of their own (Ident)
  binderCat cid = case M.lookup (showCId cid) gfCatMap of
    Just (_, args) -> elem "Ident" args
    _ -> False

  dkArity binder dkhypos typ =
    (valCat typ, sum (map (if binder then hypoArity else const 1) dkhypos))
  valCat typ = case fst (splitApp typ) of
    EIdent f | f == identProp -> "Prop"
    EIdent f | elem f [identSet, identType] -> "Kind"
    EIdent f | f == identElem -> "Exp"
    EIdent f | f == identProof -> "Proof"
    _ -> "Prop" --- UNKNOWN-DK" --- default, but not accurate

  hypoArity hypo = maybe 1 ((+1) . length . fst . splitType) (hypo2type hypo) -- for HOAS
    
symbolTableErrors :: Module -> PGF -> SymbolTable -> [String]
symbolTableErrors dk _ st =
  let mt = macroTable st
      ct = constantTable st
      bset = builtinSet st 
      funs = deduktiFunctions dk
      missing = [fun | (fun, _) <- funs, M.notMember fun ct, S.notMember fun bset]
      -- each form once (the first LaTeX form is also a symbolic one)
      forms = [(dkfun, dktyp, form) | (dkfun, dktyp) <- funs, form <- nub (allGFFuns ct dkfun)]
      -- a form shows #i that the constant does not have
      outOfRange = [(dkfun, gffun, i, length (fst dktyp)) |
            (dkfun, dktyp, ((gffun, prof), _)) <- forms,
            i <- profileIndices prof, i > length (fst dktyp)]
      -- each form is checked against the arguments its profile shows,
      -- which include the #DROP of the constant
      mismatches = [((dkfun, gffun), (e, f)) |
            (dkfun, dktyp, ((gffun, prof), gftyp)) <- forms,
            all (<= length (fst dktyp)) (profileIndices prof),
            Just (e, f) <- [mismatchingTypes mt (shownHypos prof dktyp) gftyp gffun]]
  in 
    ["MISSING IN TABLE: " ++ printTree fun | fun <- missing] ++
    [unwords ["ARGUMENT OUT OF RANGE:", printTree dkfun, showGFTree gffun,
              "shows #" ++ show i ++ ", but the constant has", show n, "arguments"] |
                      (dkfun, gffun, i, n) <- outOfRange] ++
    [unwords ["MISMATCHING TYPES:", printTree dkfun,
              show e, "<>", showGFTree gffun, show f] |
                      ((dkfun, gffun), (e, f)) <- mismatches]

-- the argument positions a profile shows, as #i
profileIndices :: Profile -> [Int]
profileIndices prof = case prof of
  PermProfile is -> is
  _ -> []

-- the hypotheses of a constant that a profile shows as arguments
shownHypos :: Profile -> DkType -> DkType
shownHypos prof (hypos, typ) = case prof of
  NoProfile -> (hypos, typ)
  DropProfile k -> (drop k hypos, typ)
  PermProfile is -> ([hypos !! (i-1) | i <- is, i <= length hypos], typ)
  HoasProfile _ -> (hypos, typ)

deduktiFunctions :: Module -> [(QIdent, DkType)]
deduktiFunctions (MJmts jmts) = concatMap getFun jmts where
  getFun :: Jmt -> [(QIdent, DkType)]
  getFun jmt = case jmt of
    JStatic fun typ -> return (fun, splitType typ)
    JDef fun (MTExp typ) _ -> return (fun, splitType typ)
    JInj fun (MTExp typ) _ -> return (fun, splitType typ)
    JThm fun (MTExp typ) _ -> return (fun, splitType typ)
    _ -> []
    

valCat :: Type -> Cat
valCat t = case unType t of (_, c, _) -> c

argCats :: Type -> [Cat]
argCats t = case unType t of (hs, _, _) -> [valCat h | (_, _, h) <- hs]

-- deciding the kind of a new constant introduced in a judgement
guessGFCat :: QIdent -> Exp -> String
guessGFCat (QIdent c) typ =
  let
    (_, val) = splitType typ
  in case lookupConstant c of
    Just (cat, _) -> cat
    _ -> case splitApp val of
      (EIdent (QIdent f), _) -> case takeWhile (/='#') f of
        k | QIdent k == identProp -> "Prop"
        k | elem (QIdent k) [identSet, identType] -> "Kind"
        k | QIdent k == identElem -> "Exp"
        k | QIdent k == identProof -> "Label"
        _ -> "Label" 

macroCommands :: MacroTable -> [String]
macroCommands t = [concat ["\\newcommand{", c, "}", arity n, "{", d, "}"] | (c, (n, d)) <- M.assocs t]
  where
    arity n = if n==0 then "" else "[" ++ show n ++ "]"