{- |
Description :  Test file for Analysis_DFOL
-}

import DFOL.AS_DFOL
import DFOL.Analysis_DFOL
import DFOL.Sign
import Common.Id
import Data.Maybe
import Common.DocUtils
import qualified Common.Result as Result
import qualified Data.Map as Map
import qualified Data.Set as Set

mkTok :: String -> Token
mkTok s = Token s nullRange

natTok, matTok, plusTok, mTok, nTok, m1Tok :: NAME
natTok = mkTok "Nat"
matTok = mkTok "Mat"
plusTok = mkTok "plus"
mTok = mkTok "m"
m1Tok = mkTok "m0"
nTok = mkTok "n"
xTok = mkTok "x"
x1Tok = mkTok "x1"
x10Tok = mkTok "x10"

nat, mat, plus, m, n, m1 :: TERM

nat = Identifier natTok
mat = Identifier matTok
plus = Identifier plusTok
m = Identifier mTok
n = Identifier nTok
m1 = Identifier m1Tok

sig :: Sign
sig = Sign [([natTok], Sort),
            ([matTok], Func [Univ nat, Univ nat] Sort),
            ([plusTok], Pi [([mTok, m1Tok], Univ nat)] $ Func [Univ $ Appl mat [m, m1], Univ $ Appl mat [m, m1]] $ Univ $ Appl mat [m, m1])]

cont :: CONTEXT
cont = Context [([mTok, nTok], Univ nat)]

t0, t1, t2, t3, t4 :: TYPE
t0 = Pi [([mTok, nTok], Univ nat)] $ Func [Univ $ Appl mat [m, n], Univ $ Appl mat [m, n]] $ Univ $ Appl mat [m, n]
t1 = Pi [([mTok, m1Tok], Univ nat)] $ Func [Univ $ Appl mat [m, m1], Univ $ Appl mat [m, m1]] $ Univ $ Appl mat [m, m1]
t2 = Func [] $ typeRecForm t0
t3 = Func [Univ nat, Univ nat] Sort
t4 = Func [Univ nat] $ Func [Univ nat] $ Func [] Sort
t5 = Pi [([xTok], Sort)] $ Pi [([nTok], Sort)] $ Univ $ Appl mat [Identifier xTok, Identifier nTok]
t6 = Pi [([mTok], Sort)] $ Pi [([xTok], Sort)] $ Univ $ Appl mat [Identifier mTok, Identifier xTok]

t :: TYPE
t = let (Pi [([n1], t1)] s1) = t5
        (Pi [([n2], t2)] s2) = t6
        syms1 = Set.delete n1 $ getFreeVars s1
        syms2 = Set.delete n2 $ getFreeVars s2
        v = getNewName n1 $ Set.union syms1 syms2
        type1 = translate (Map.singleton n1 (Identifier v)) syms1 s1
        type2 = translate (Map.singleton n2 (Identifier v)) syms2 s2
        in type2

u :: NAME
u = let (Pi [([n1], t1)] s1) = t5
        (Pi [([n2], t2)] s2) = t6
        syms1 = Set.delete n1 $ getFreeVars s1
        syms2 = Set.delete n2 $ getFreeVars s2
        v = getNewName n1 $ Set.union syms1 syms2
        type1 = translate (Map.singleton n1 (Identifier v)) syms1 s1
        type2 = translate (Map.singleton n2 (Identifier v)) syms2 s2
        in v
