{- |

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