Informath2MathCore.hs

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

module Informath2MathCore where

import Semantics (SemDefs, appSemDefs, inSituResults)
import Informath
import GodementSemantics (godementExpand, godementSem)

data SEnv = SEnv {varlist :: [String]}

initSEnv :: SEnv
initSEnv = SEnv {varlist = []}

-- used when no Kind is given e.g. as quantifier domain
unspecifiedKind :: GKind
unspecifiedKind = GNounKind (LexNoun "object_Noun")

newVar :: SEnv -> (GIdent, SEnv)
newVar senv = (xi, senv{varlist = x : varlist senv}) where
  x = head [x | x <- ["_h" ++ show i | i <- [0..]], notElem x (varlist senv)]
  xi = GStrIdent (GString x)
  
semantics :: SemDefs -> GJmt -> [GJmt]
semantics defs =
  concatMap (inSituResults . addCoercions . addParenth . sem initSEnv . godementSem)
  . godementExpand . removeFonts . appSemDefs defs

addCoercions :: Tree a -> Tree a
addCoercions t = case t of
  GAxiomJmt label hypos prop -> GAxiomJmt label (addCoercions hypos) (proofProp prop)  
  GThmJmt label hypos prop proof -> GThmJmt label (addCoercions hypos) (proofProp prop) proof
  GAxiomExpJmt label hypos exp kind -> GAxiomExpJmt label (addCoercions hypos) exp (elemKind kind)

---- TODO: check where exactly coercions are needed
  
  --AxiomPropJmt : Label -> ListHypo -> Prop -> Jmt ;
  --DefPropJmt : Label -> ListHypo -> Prop -> Prop -> Jmt ;
  --SuchThatKind : Ident -> Kind -> Prop -> Kind ;
  --AxiomKindJmt : Label -> ListHypo -> Kind -> Kind -> Jmt ;
  --DefExpJmt : Label -> ListHypo -> Exp -> Kind -> Exp -> Jmt ;
  --DefKindJmt : Label -> ListHypo -> Kind -> Kind -> Jmt ;

  GPropHypo prop -> GPropHypo (proofProp prop)
  GVarsHypo idents kind -> GVarsHypo idents (elemKind kind)
  _ -> composOp addCoercions t
 where
   proofProp prop = case prop of
     GProofProp _ -> prop
     _ -> GProofProp prop
   elemKind kind = case kind of
     GElemKind _ -> kind      -- already coerced: semantics may be applied twice
     _ -> GElemKind kind

removeFonts :: Tree a -> Tree a
removeFonts t = case t of
  GTextbfTerm term -> removeFonts term
  _ -> composOp removeFonts t

addParenth :: Tree a -> Tree a
addParenth t = case t of
  GAndProp (GListProp props) -> foldl1 GCoreAndProp (map addParenth props)
  GOrProp (GListProp props) -> foldl1 GCoreOrProp (map addParenth props)
  GIfProp a b -> GCoreIfProp (addParenth a) (addParenth b)
  GIffProp a b -> GCoreIffProp (addParenth a) (addParenth b)
  -- a variable with a condition (FormulaArgKind) has it as the premiss of an
  -- implication (for all) or the first conjunct (there exists)
  GAllProp (GListArgKind argkinds) prop ->
    foldr (\ (var, exp, cond) y -> GCoreAllProp exp var (maybe y (\c -> GCoreIfProp c y) cond))
        (addParenth prop)
        (concatMap semArgkindCond argkinds)
  GExistProp (GListArgKind argkinds) prop ->
    foldr (\ (var, exp, cond) y -> GCoreExistProp exp var (maybe y (\c -> GCoreAndProp c y) cond))
        (addParenth prop)
        (concatMap semArgkindCond argkinds)
  _ -> composOp addParenth t

-- | The variables of an argkind with their kinds and conditions
semArgkindCond :: GArgKind -> [(GIdent, GKind, Maybe GProp)]
semArgkindCond argkind = case argkind of
  GFormulaArgKind kind f | Just x <- boundVar f -> [(x, kind, Just (GFormulaProp f))]
  _ -> [(x, k, Nothing) | (x, k) <- semArgkind argkind]

semArgkind :: GArgKind -> [(GIdent, GKind)]
semArgkind argkind = case argkind of
  GIdentArgKind kind ident -> [(ident, kind)]
  GIdentsArgKind kind (GListIdent idents) -> [(ident, kind) | ident <- idents]
  GIndexedDeclarationArgKind (GInt i) ->
     [((GStrIdent (GString ("UNRESOLVED_" ++ show i))),
       GExpKind (GTermExp (GIdentTerm (GStrIdent (GString "UNRESOLVED_KIND")))))]
  GKindArgKind kind -> [(GStrIdent (GString "KIND_"), kind)]
  GBareIdentsArgKind (GListIdent idents) -> [(ident, unspecifiedKind) | ident <- idents]
  --- these should have been resolved in sem
  _ -> error ("semArgKind failure")


semHypo :: GHypo -> [GHypo]
semHypo hypo = case hypo of
  GAdjKindHypo xs@(GListIdent xx) adj kind ->
    GVarsHypo xs kind : [GPropHypo (GAdjProp adj (GTermExp (GIdentTerm x))) | x <- xx]
  GSuchThatHypo xs prop kind ->
    [GVarsHypo xs kind, GPropHypo prop]
  _ -> [hypo]


sem :: SEnv -> Tree a -> Tree a
sem env t = case t of

  -- a structure defined by extension is a structure whose first clauses are
  -- its carrier and its parent
  GExtensionJmt label kind parent x (GListArgKind args) prop ->
    sem env (extensionStructure label kind parent x args [prop])
  GExtensionPropJmt label kind parent x prop ->
    sem env (extensionStructure label kind parent x [] [prop])
  GExtensionDataJmt label kind parent x (GListArgKind args) ->
    sem env (extensionStructure label kind parent x args [])
  GExtensionHyposJmt label (GListHypo hypos) kind parent x (GListArgKind args) prop ->
    case sem env (extensionStructure label kind parent x args [prop]) of
      GStructureJmt l (GListClause cs) k ->
        GStructureJmt l (GListClause (concatMap (paramClauses env) hypos ++ cs)) k
      j -> j

  GLetFormulaHypo formula -> case (sem env formula) of
    GElemFormula (GListTerm terms) term | length xs == length terms ->
      GVarsHypo (GListIdent xs) (GExpKind (GTermExp term))
        where xs = [x | GIdentTerm x <- terms]
    -- "let $x \\in A$" read as a comparison
    GEquationFormula (GBinaryEquation (LexCompar "element_Compar") (GIdentTerm x) term) ->
      GVarsHypo (GListIdent [x]) (GExpKind (GTermExp term))
    _ -> GPropHypo (sem env (GFormulaProp (sem env formula)))
  -- "let $x, y \\in A$", as MathCore2Informath generates it for variables of A
  GLetDeclarationHypo decl -> case (sem env decl) of
    GElemDeclaration (GListTerm terms) term | length xs == length terms ->
      GVarsHypo (GListIdent xs) (GExpKind (GTermExp term))
        where xs = [x | GIdentTerm x <- terms]
    d -> GLetDeclarationHypo d
  -- "let $x, y \\in A$ such that P", as MathCore2Informath generates it
  GLetFormulaSuchThatHypo formula prop -> case (sem env formula) of
    GElemFormula (GListTerm terms) term | length xs == length terms ->
      sem env (GSuchThatHypo (GListIdent xs) prop (GExpKind (GTermExp term)))
        where xs = [x | GIdentTerm x <- terms]
    GEquationFormula (GBinaryEquation (LexCompar "element_Compar") (GIdentTerm x) term) ->
      sem env (GSuchThatHypo (GListIdent [x]) prop (GExpKind (GTermExp term)))
    f -> GLetFormulaSuchThatHypo f (sem env prop)
{- ----
  GIfProp cond@(GFormulaProp (GElemFormula (GListTerm terms) (GSetTerm set))) prop ->
    case getJustVarsFromTerms env terms of
      Just xs -> sem env (GAllProp (GListArgKind [GIdentsArgKind (GSetKind set) (GListIdent xs)]) prop)
      _ ->  GIfProp (sem env cond) (sem env prop)
-}      

  GDefinedAdjJmt label hypos exp adj prop ->
    sem env (GDefPropJmt label hypos (GAdjProp adj exp) prop)

  GListHypo hypos -> GListHypo (concatMap (semHypo . sem env) hypos)

  -- "for all $x > 0$ in $A$", "there exists $x > 0$ in $A$ such that"
  GBoundedInAllProp f set prop | Just x <- boundVar f ->
    sem env (GCoreAllProp (GExpKind set) x (GIfProp (GFormulaProp f) prop))
  GBoundedInExistProp f set prop | Just x <- boundVar f ->
    sem env (GCoreExistProp (GExpKind set) x (GAndProp (GListProp [GFormulaProp f, prop])))
  -- "function from A to B" is the function kind of the sets A and B
  GFunExpKind a b ->
    sem env (GFunKind (GListArgKind [GKindArgKind (GExpKind a)]) (GExpKind b))
  GIfProp cond prop -> case getAndProps cond of
    Just props -> sem env (foldr (\a b -> GIfProp a b) prop props)
    _ -> GIfProp (sem env cond) (sem env prop)

  GOnlyIfProp cond prop -> sem env (GIfProp cond prop)
  GFormulaImpliesProp cond prop ->
    sem env (GIfProp (GFormulaProp cond) (GFormulaProp prop))

  GExistNoProp argkinds prop -> GCoreNotProp (sem env (GExistProp argkinds prop))

  GPostQuantProp prop exp -> case sem env exp of
    GEveryIdentKindQuant ident kind ->
      sem env (GCoreAllProp kind ident prop)
    GIndefIdentKindQuant ident kind ->
      sem env (GCoreExistProp kind ident prop)
    GSomeIdentsKindQuant idents kind ->
      sem env (GExistProp (GListArgKind [GIdentsArgKind kind idents]) prop)
    GAllIdentsKindQuant idents kind ->
      sem env (GAllProp (GListArgKind [GIdentsArgKind kind idents]) prop)
    GNoIdentsKindQuant idents kind ->
      sem env (GAllProp (GListArgKind [GIdentsArgKind kind idents]) (GCoreNotProp prop))
    _ -> t ----TODO some cases: error ("sem not yet: " ++ showExpr [] (gf t))

  GAllProp argkinds prop -> GAllProp (sem env argkinds) (sem env prop)

  ---- TODO: generalize aggregation and in situ resolution to all predication functions
  GAdjProp adj (GQuantExp (GAllIdentsKindQuant (GListIdent [x]) kind)) ->
    sem env (GAllProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
              (GAdjProp adj (GTermExp (GIdentTerm x))))
  GAdjProp adj (GQuantExp (GEveryIdentKindQuant x kind)) ->
    sem env (GAdjProp adj (GQuantExp (GAllIdentsKindQuant  (GListIdent [x]) kind)))
  GAdjProp adj (GQuantExp (GSomeIdentsKindQuant (GListIdent [x]) kind)) ->
    sem env (GExistProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
              (GAdjProp adj (GTermExp (GIdentTerm x))))
  GAdjProp adj (GQuantExp (GIndefIdentKindQuant x kind)) ->
    sem env (GAdjProp adj (GQuantExp (GSomeIdentsKindQuant  (GListIdent [x]) kind)))
  GAdjProp adj (GQuantExp (GNoIdentsKindQuant (GListIdent [x]) kind)) ->
    sem env (GAllProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
              (GNotAdjProp adj (GTermExp (GIdentTerm x))))

  GAdjProp adj (GQuantExp (GEveryKindQuant kind)) ->
    let (x, env') = newVar env
    in sem env'
      (GAllProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
        (GAdjProp adj (GTermExp (GIdentTerm x))))
  GAdjProp adj (GQuantExp (GAllKindQuant kind)) ->
    sem env (GAdjProp adj (GQuantExp (GEveryKindQuant kind)))
  GAdjProp adj (GQuantExp (GSomeKindQuant kind)) ->
    let (x, env') = newVar env
    in sem env'
      (GExistProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
        (GAdjProp adj (GTermExp (GIdentTerm x))))
  GAdjProp adj (GQuantExp (GIndefKindQuant kind)) ->
    sem env (GAdjProp adj (GQuantExp (GSomeKindQuant kind)))
  GAdjProp adj (GQuantExp (GNoKindQuant kind)) ->
    let (x, env') = newVar env
    in sem env'
      (GAllProp (GListArgKind [GIdentsArgKind kind (GListIdent [x])])
        (GNotAdjProp adj (GTermExp (GIdentTerm x))))

  GAdjProp adj exp -> case sem env adj of
    GAndAdj (GListAdj adjs)  ->
      let sx = sem env exp
      in GAndProp (GListProp [GAdjProp adj sx | adj <- adjs])
    GOrAdj (GListAdj adjs)  ->
      let sx = sem env exp
      in GOrProp (GListProp [GAdjProp adj sx | adj <- adjs])
    GAdj2Adj adj2 exp2 ->
      GAdj2Prop adj2 (sem env exp) (sem env exp2)
    GAdj3Adj adj3 exp2 exp3 ->
      GAdj3Prop adj3 (sem env exp) (sem env exp2) (sem env exp3)
    sa -> case sem env exp of
      (GAndExp (GListExp exps)) ->
        GAndProp (GListProp [GAdjProp sa exp | exp <- exps])
      (GOrExp (GListExp exps)) ->
        GOrProp (GListProp [GAdjProp sa exp | exp <- exps])
      sexp -> GAdjProp sa sexp

  GAdjCCollProp adj (GListExp [x, y]) -> GAdjCProp adj (sem env x) (sem env y)
  ---- TODO: AdjCColl properly implemented in Dedukti
  
  GAdjECollProp adj (GListExp xs) ->
    GAndProp (GListProp [GAdjEProp adj x y | (x, y) <- subsequentPairs (map (sem env) xs)])

  GBothAndProp a b -> GAndProp (GListProp [sem env a, sem env b])
  GBothAndAdj a b -> GAndAdj (GListAdj [sem env a, sem env b])
  GBothAndExp a b -> GAndExp (GListExp [sem env a, sem env b])

  GEitherOrProp a b -> GOrProp (GListProp [sem env a, sem env b])
  GEitherOrAdj a b -> GOrAdj (GListAdj [sem env a, sem env b])
  GEitherOrExp a b -> GOrExp (GListExp [sem env a, sem env b])

  GNotAdjProp adj exp -> GCoreNotProp (sem env (GAdjProp adj exp))
  GNotAdj2Prop adj x y -> GCoreNotProp (sem env (GAdj2Prop adj x y))
  GNotAdjCProp adj exps -> GCoreNotProp (sem env (GAdjCCollProp adj exps))
  GNotAdjEProp adj exps -> GCoreNotProp (sem env (GAdjECollProp adj exps))
  GNotNoun1Prop adj exp -> GCoreNotProp (sem env (GNoun1Prop adj exp))
  GNotNoun2Prop adj x y -> GCoreNotProp (sem env (GNoun2Prop adj x y))
  GNotNoun3Prop noun x y z -> GCoreNotProp (sem env (GNoun3Prop noun x y z))
  GNotVerbProp adj exp -> GCoreNotProp (sem env (GVerbProp adj exp))
  GNotVerb2Prop adj x y -> GCoreNotProp (sem env (GVerb2Prop adj x y))
  GNotAdvProp adv exp -> GCoreNotProp (sem env (GAdvProp adv exp))
  GNotAdv2Prop adv x y -> GCoreNotProp (sem env (GAdv2Prop adv x y))
  GNotAdvCProp adv exps -> GCoreNotProp (sem env (GAdvCCollProp adv exps))

  GPluralKindExp kind -> GKindExp kind

  GKindArgKind kind -> 
    let (var, nenv) = newVar env
    in GIdentsArgKind (sem nenv kind) (GListIdent [var])

  GDisplayFormulaProp formula -> sem env (GFormulaProp formula)
  
  GFormulaProp (GEquationFormula equation@(GChainEquation _ _ _)) -> case chainedEquations equation of
    triples -> GAndProp (GListProp
      [sem env (GFormulaProp (GEquationFormula (GBinaryEquation eqsign x y))) | (eqsign, x, y) <- triples])
  GFormulaProp (GElemFormula (GListTerm xs) y) -> case xs of
    [x] -> GNoun2Prop (LexNoun2 "element_Noun2")
              (sem env (GTermExp x)) (sem env (GTermExp y))
    _ -> GAndProp (GListProp [sem env (GFormulaProp (GElemFormula (GListTerm [x]) y)) | x <- xs])

{-
  GTermExp (GTSum3dots m m1 n) ->
    let
      [sm, sm1, sn] = map (sem env) [m, m1, n]
      (var, nenv) = newVar env
    in sem nenv (GTermExp (iqTest var m m1 n)) 
-}
  Gtimes_Term x y -> GOper2Term (LexOper2 "times_Oper2") (sem env x) (sem env y)
  GParenthTerm term -> sem env term

-- Naproche extensions
  GSupposePropHypo prop -> sem env (GPropHypo prop)
  GIffIffProp a b -> sem env (GIffProp a b)
  GWeHaveProp prop -> sem env prop
  GNoCommaAllProp argkinds prop -> sem env (GAllProp argkinds prop)
  GBareIdentsArgKind idents -> sem env (GIdentsArgKind unspecifiedKind idents) ---- TODO: get from env
  GDeclarationArgKind declaration -> case sem env declaration of
   ---- TODO: check that all are idents
    GElemDeclaration (GListTerm terms) term ->
      GIdentsArgKind (GExpKind (GTermExp term)) (GListIdent [x | GIdentTerm x <- terms])
    _ -> t ---- error "cannot use declaration as argkind yet"
  GNoCommaExistProp argkinds prop ->
    sem env (GExistProp argkinds prop)
  GNoArticleExistProp argkind prop ->
    sem env (GExistProp (GListArgKind [argkind]) prop)
  GWeDefineAdjJmt label hypos exp adj prop ->
    sem env (GDefPropJmt label hypos (GAdjProp adj exp) prop)
  _ -> composOp (sem env) t

{- ----
-- trying to guess the summation term from given examples
iqTest :: GIdent -> GTerm -> GTerm -> GTerm -> GTerm
iqTest i mterm m1term nterm = case findTerm mterm m1term nterm of
  Just term -> term
  _ -> foldl1 (GAppOperTerm (LexOper "plus_Oper")) [mterm, m1term, unknownTerm, nterm]
 where
   findTerm mterm m1term nterm = case refactorTerms mterm nterm of
     Just (m, n, f) -> return (GTSigma i m n (f (GIdentTerm i))) ---- verify with m1term
     _ -> Nothing
   refactorTerms :: GTerm -> GTerm -> Maybe (GTerm, GTerm, GTerm -> GTerm)
   refactorTerms mterm nterm = case (mterm, nterm) of
     (GAppOperTerm f1 x1 y1, GAppOperTerm f2 x2 y2) | f1 == f2 -> case () of  --- special case: one binop
       _ | x1 == x2 && y1 /= y2 -> return (y1, y2, \y -> GAppOperTerm f1 x1 y)
       _ | x1 /= x2 && y1 == y2 -> return (x1, x2, \x -> GAppOperTerm f1 x y1)
     _ -> Nothing
-}


chainedEquations :: GEquation -> [(GCompar, GTerm, GTerm)]
chainedEquations equation = case equation of
  GChainEquation eqsign term equ ->
    let triples@((_, x, _):_) = chainedEquations equ
    in (eqsign, term, x) : triples
  GBinaryEquation eqsign term1 term2 ->
    [(eqsign, term1, term2)]

{-
ifs2hypos :: [GHypo] -> GProp -> ([GHypo], GProp)
ifs2hypos hs prop = case prop of
  GIfProp p q -> 
-}


-- identify exp lists that are just variable lists, possibly bindings
getJustVars :: SEnv -> GExp -> Maybe [GIdent]
getJustVars env exp = case exp of
  GTermExp (GIdentTerm x) -> Just [x]
  GAndExp (GListExp exps) -> do
    xss <- mapM (getJustVars env) exps
    return (concat xss)
  _ -> Nothing

getJustVarsFromTerms :: SEnv -> [GTerm] -> Maybe [GIdent]
getJustVarsFromTerms env terms = case terms of
  GIdentTerm x : ts ->  do
    xs <- getJustVarsFromTerms env ts
    return (x : xs)
  [] -> return []
  _ -> Nothing

mkAndProp :: [GProp] -> GProp
mkAndProp props = case props of
  [prop] -> prop
  _ -> GAndProp (GListProp props)


getAndProps :: GProp -> Maybe [GProp]
getAndProps prop = case prop of
  GAndProp (GListProp props) -> Just props
  _ -> Nothing

--- also in DMC
gExps :: [GExp] -> GExps
gExps exps = case exps of
  [exp] -> GOneExps exp
  _ -> GManyExps (GListExp exps)


--- used in iqTest when guessing summation terms 
unknownTerm :: GTerm
unknownTerm = GIdentTerm (GStrIdent (GString "UNKNOWN"))

-- used for decomposing AdjE over a list
subsequentPairs :: [b] -> [(b, b)]
subsequentPairs xs = [(xs !! k, xs !! (k+1)) | k <- [0..(length xs - 2)] ]

-- | The structure that an extension judgement abbreviates: "a monoid is a
-- semigroup M with an element 1 of M such that P" has the clauses "M is a
-- set", "M is a semigroup", "1 is an element of M" and P.
-- | Parameters of a structure, back from "let R be a semiring".
paramClauses :: SEnv -> GHypo -> [GClause]
paramClauses env h = case h of
  GVarsHypo (GListIdent ys) (GNounKind n) | isStructureNoun n ->
    concat [[GVarClause y (GNounKind (LexNoun "set_Noun")),
             GPropClause (GProofProp (GNoun1Prop (GNounNoun1 n) (GTermExp (GIdentTerm y))))] | y <- ys]
  GVarsHypo (GListIdent ys) k -> [GVarClause y (sem env (GElemKind k)) | y <- ys]
  GPropHypo q -> [GPropClause (GProofProp (sem env q))]
  _ -> []
 where
  isStructureNoun n = case n of
    LexNoun "set_Noun" -> False
    _ -> True

extensionStructure :: GLabel -> GKind -> GKind -> GIdent -> [GArgKind] -> [GProp] -> GJmt
extensionStructure label kind parent x args props =
  GStructureJmt label (GListClause (
      [GVarClause x setKind, GPropClause (GProofProp (parentProp parent))]
      ++ [GVarClause y (GElemKind k) | (y, k) <- concatMap semArgkind args]
      ++ [GPropClause (GProofProp p) | p <- concatMap conjuncts props]))
    kind
 where
  setKind = GNounKind (LexNoun "set_Noun")
  parentProp k = case k of
    GNounKind n -> GNoun1Prop (GNounNoun1 n) (GTermExp (GIdentTerm x))
    _ -> GKindProp (GTermExp (GIdentTerm x)) k
  conjuncts p = case p of
    GAndProp (GListProp ps) -> ps
    _ -> [p]

-- | The variable of a bounded quantifier, the left side of its comparison
boundVar :: GFormula -> Maybe GIdent
boundVar f = case f of
  GEquationFormula (GBinaryEquation _ (GIdentTerm x) _) -> Just x
  _ -> Nothing