content: {-# LANGUAGE OverloadedStrings #-}
  module Main(main) where
  
  import Prelude
  import Test.HUnit
  import CedilleTypes
  import CedilleLexer hiding (main)
  import CedilleParser hiding (main)
  import qualified CedilleCommentsLexer as C
  import Control.Arrow
  import Control.Monad
  import System.IO  
  import qualified System.Exit as Exit
  import Data.Text (Text, pack)
  
  test_comments_str = unlines [
      " aaaaaa            " -- 20 characters per row
    , " ddk 4adjf30  ,,   "
    , " {- comments       "
    , "    more           "
    , "               -}  "
    , " dadfdf            "
    , " aaaa -- comments  "
    , " fffffffffffffff   " ]
  
  test_lexer_comments = TestCase (assertEqual "test lexer comments "
                          (C.File (C.Entity (C.EntityComment "42" "98") (C.Entity (C.EntityComment "127" "140") C.EndEntity)))
                          (C.scanComments (pack test_comments_str)))
    
  
  removeLexerPositions :: Either a [Token] -> Either a [TokenClass]
  removeLexerPositions = right (map (\ (Token _ tc) -> tc))
  
  test_lexer_str = "αβγδ" -- greek letters
  
  test_lexer = TestCase (assertEqual "test lexer 0"
                          (Prelude.Right [TVar "αβγδ"])
                          (removeLexerPositions (scanner test_lexer_str)))
                          
  
  test_parser_str = unlines [
    "import ../hello/world . %comments",
    "import module . ",
    "%comments 2 ",
    "module αβγδ . "
    ]
  
  test_parser_module = TestCase (assertEqual "test parser 0"
                                 (Prelude.Right (File "0" ImportsStart "αβγδ" ParamsNil CmdsStart "34"))
                                 (runAlex test_parser_str $ cedilleParser))
  
  -- test_atype_hole_str = "  ●"
  -- test_atype_hole = TestCase (assertEqual "test atype Hole"
  --                        (Prelude.Right (TpHole (AlexPn 2 1 3)))
  --                        (runAlex test_atype_hole_str $ atypes))
  
  -- test_atype_qvar_str = " aaa "
  -- test_atype_qvar = TestCase (assertEqual "test atype Qvar"
  --                             (Prelude.Right (TpVar (AlexPn 1 1 2) "aaa"))
  --                             (runAlex test_atype_qvar_str $ atypes))
  
  -- test_atype_qvar2_str = " aaa.bbb.ccc "
  -- test_atype_qvar2 = TestCase (assertEqual "test atype Qvar Qualified"
  --                             (Prelude.Right (TpVar (AlexPn 1 1 2) "aaa.bbb.ccc"))
  --                             (runAlex test_atype_qvar2_str $ atypes))
  
  
  test_type_arrow_str = " cNat ➔ cNat "
  
  test_type_arrow = TestCase (assertEqual "test type Arrow"
                               (Prelude.Right (TpArrow (TpVar "2" "cNat") UnerasedArrow (TpVar "9" "cNat")))
                               (runAlex test_type_arrow_str $ types))
  
  test_parser_term_str = unlines [
    " Λ X . λ f . λ a . a  " ,
    ""                                             
    ]
  
  test_parser_term = TestCase (assertEqual "test parser term"
                                 (Prelude.Right (Lam "2" ErasedLambda "4" "X" NoClass (Lam "8" KeptLambda "10" "f" NoClass (Lam "14" KeptLambda "16" "a" NoClass (Var "20" "a")))))
                                 (runAlex test_parser_term_str $ term))
  
  test_parser_deftermtype_str = unlines [
      "cZ ◂ cNat = Λ X . λ f . λ α . α  " ,
  --    "cS ◂ X ➔ X = a "  ,
      ""
    ]
  
  test_parser_deftermtype = TestCase (assertEqual "test parser definition"
                                     (Prelude.Right (DefTerm "1" "cZ" (Type (TpVar "6" "cNat")) (Lam "13" ErasedLambda "15" "X" NoClass (Lam "19" KeptLambda "21" "f" NoClass (Lam "25" KeptLambda "27" "α" NoClass (Var "31" "α"))))))
                                  (runAlex test_parser_deftermtype_str $ deftermtype))
  
  test_parser_cmd_str = unlines [
  --  "import ChurchNat ." ,                         
  --  "cNat ◂ ★ = ∀ X : ★ . (X ➔ X) ➔ X ➔ X . " ,
  --  "cZ ◂ cNat = Λ X . λ f . λ a . a.1  . " ,
      "cS : X ➔ X  = λ n . Λ X . λ f . λ a . f (n · X f a) . "  ,
      " "
    ]
  
  test_parser_cmd = TestCase (assertEqual "test parser command"
                              (Prelude.Right (DefTermOrType (DefTerm "1" "cS" (Type (TpArrow (TpVar "6" "X") UnerasedArrow (TpVar "10" "X"))) (Lam "15" KeptLambda "17" "n" NoClass (Lam "21" ErasedLambda "23" "X" NoClass (Lam "27" KeptLambda "29" "f" NoClass (Lam "33" KeptLambda "35" "a" NoClass (App (Var "39" "f") NotErased (Parens "41" (App (App (AppTp (Var "42" "n") (TpVar "46" "X")) NotErased (Var "48" "f")) NotErased (Var "50" "a")) "52"))))))) "54"))
                                 (runAlex test_parser_cmd_str $ cmd))
  
  -- Problem shift-reduce confict in state 12 causes it is not correctly parsed
  
  test_parser_liftingtype_str = unlines [
   {-# SCC "" #-}    "     a ➔↑ ☆   "
    ]
  
  test_parser_liftingtype = TestCase (assertEqual "test parser lifting type"
                                      (Prelude.Right (LiftTpArrow (TpVar "6" "a") (LiftStar "11")))
                                      (runAlex test_parser_liftingtype_str $ liftingtype))
  
  test_parser_cnat_str = unlines [
    "{- Multi -   ",
    "    Lines    ",
    "    Comments ",
    "",
    "        -}",
    "module ChurchNat ."                         ,
    ""                                           ,
    "cNat ◂ ★ = ∀ X : ★ . (X ➔ X) ➔ X ➔ X . " ,
    ""                                           ,
    "cZ ◂ cNat = Λ X . λ f . λ a . a . "         ,
    ""                                           ,
    "cS : cNat ➔ cNat = λ n . Λ X . λ f . λ a . f (n · X f a) . ",
    "{- Multi -   ",
    "    Lines    ",
    "    Comments ",
    "",
    "        -}"
    ]
  
  test_parser_cnat = TestCase (assertEqual "test parser cnat module"
                                 (Prelude.Right
                                  (File "1" ImportsStart "ChurchNat" ParamsNil (CmdsNext (DefTermOrType (DefType "75" "cNat" (Star "82") (Abs "86" All "88" "X" (Tkk (Star "92")) (TpArrow (TpParens "96" (TpArrow (TpVar "97" "X") UnerasedArrow (TpVar "101" "X")) "103") UnerasedArrow (TpArrow (TpVar "106" "X") UnerasedArrow (TpVar "110" "X"))))) "113") (CmdsNext (DefTermOrType (DefTerm "116" "cZ" (Type (TpVar "121" "cNat")) (Lam "128" ErasedLambda "130" "X" NoClass (Lam "134" KeptLambda "136" "f" NoClass (Lam "140" KeptLambda "142" "a" NoClass (Var "146" "a"))))) "149") (CmdsNext (DefTermOrType (DefTerm "152" "cS" (Type (TpArrow (TpVar "157" "cNat") UnerasedArrow (TpVar "164" "cNat"))) (Lam "171" KeptLambda "173" "n" NoClass (Lam "177" ErasedLambda "179" "X" NoClass (Lam "183" KeptLambda "185" "f" NoClass (Lam "189" KeptLambda "191" "a" NoClass (App (Var "195" "f") NotErased (Parens "197" (App (App (AppTp (Var "198" "n") (TpVar "202" "X")) NotErased (Var "204" "f")) NotErased (Var "206" "a")) "208"))))))) "210") CmdsStart))) "266"))
                                 (runAlex test_parser_cnat_str $ cedilleParser))
  
  test_cnat = TestCase (do
                          cnt <- readFile "test/tests/cnat.ced"
                          (assertEqual "test file cnat.ced"
                            (Prelude.Right (File "1" ImportsStart "Cnat" ParamsNil (CmdsNext (DefTermOrType (DefType "16" "cNat" (Star "23") (Abs "27" All "29" "X" (Tkk (Star "33")) (TpArrow (TpParens "37" (TpArrow (TpVar "38" "X") UnerasedArrow (TpVar "42" "X")) "44") UnerasedArrow (TpArrow (TpVar "47" "X") UnerasedArrow (TpVar "51" "X"))))) "54") (CmdsNext (DefTermOrType (DefTerm "56" "cZ" (Type (TpVar "61" "cNat")) (Lam "68" ErasedLambda "70" "X" NoClass (Lam "74" KeptLambda "76" "f" NoClass (Lam "80" KeptLambda "82" "a" NoClass (Var "86" "a"))))) "89") (CmdsNext (DefTermOrType (DefTerm "91" "cS" (Type (TpArrow (TpVar "96" "cNat") UnerasedArrow (TpVar "103" "cNat"))) (Lam "110" KeptLambda "112" "n" NoClass (Lam "116" ErasedLambda "118" "X" NoClass (Lam "122" KeptLambda "124" "f" NoClass (Lam "128" KeptLambda "130" "a" NoClass (App (Var "134" "f") NotErased (Parens "136" (App (App (AppTp (Var "137" "n") (TpVar "141" "X")) NotErased (Var "143" "f")) NotErased (Var "145" "a")) "147"))))))) "149") CmdsStart))) "153"))                                       (runAlex cnt $ cedilleParser)))
  
  test_nat = TestCase (do
                          cnt <- readFile "test/tests/nat.ced"
                          (assertEqual "test file nat.ced"
                            (Prelude.Right (File "1" ImportsStart "Nat" ParamsNil (CmdsNext (ImportCmd (Import "15" "cnat" NoOptAs (ArgsNil "25") "27")) (CmdsNext (DefTermOrType (DefType "29" "cNatInductive" (KndTpArrow (TpVar "45" "cNat") (Star "52")) (TpLambda "56" "58" "x" (Tkt (TpVar "62" "cNat")) (Abs "69" All "71" "Q" (Tkk (KndTpArrow (TpVar "75" "cNat") (Star "82"))) (TpArrow (TpParens "86" (Abs "87" All "89" "x" (Tkt (TpVar "93" "cNat")) (TpArrow (TpAppt (TpVar "100" "Q") (Var "102" "x")) UnerasedArrow (TpAppt (TpVar "106" "Q") (Parens "108" (App (Var "109" "cS") NotErased (Var "112" "x")) "114")))) "115") UnerasedArrow (TpArrow (TpAppt (TpVar "118" "Q") (Var "120" "cZ")) UnerasedArrow (TpAppt (TpVar "125" "Q") (Var "127" "x"))))))) "129") (CmdsNext (DefTermOrType (DefType "131" "Nat" (Star "137") (Iota "141" "143" "x" (SomeType (TpVar "147" "cNat")) (TpAppt (TpVar "154" "cNatInductive") (Var "168" "x")))) "170") (CmdsNext (DefTermOrType (DefTerm "172" "Z" (Type (TpVar "176" "Nat")) (IotaPair "182" (Var "184" "cZ") (Lam "189" ErasedLambda "191" "X" NoClass (Lam "195" KeptLambda "197" "s" NoClass (Lam "201" KeptLambda "203" "z" NoClass (Var "207" "z")))) "210")) "212") (CmdsNext (DefTermOrType (DefTerm "213" "S" (Type (TpArrow (TpVar "217" "Nat") UnerasedArrow (TpVar "223" "Nat"))) (Lam "229" KeptLambda "231" "n" NoClass (IotaPair "235" (App (Var "237" "cS") NotErased (IotaProj (Var "240" "n") "1" "243")) (Lam "246" ErasedLambda "248" "P" NoClass (Lam "252" KeptLambda "254" "s" NoClass (Lam "258" KeptLambda "260" "z" NoClass (App (App (Var "264" "s") Erased (IotaProj (Var "267" "n") "1" "270")) NotErased (Parens "271" (App (App (AppTp (IotaProj (Var "272" "n") "2" "275") (TpVar "278" "P")) NotErased (Var "280" "s")) NotErased (Var "282" "z")) "284"))))) "286"))) "288") (CmdsNext (DefTermOrType (DefTerm "290" "NatRec" (Type (TpArrow (TpVar "299" "Nat") UnerasedArrow (TpVar "305" "cNat"))) (Lam "312" KeptLambda "314" "n" NoClass (IotaProj (Var "318" "n") "1" "321"))) "323") (CmdsNext (DefTermOrType (DefTerm "325" "add" (Type (TpArrow (TpVar "331" "Nat") UnerasedArrow (TpArrow (TpVar "337" "Nat") UnerasedArrow (TpVar "343" "Nat")))) (Lam "349" KeptLambda "351" "m" NoClass (Lam "355" KeptLambda "357" "n" NoClass (App (App (AppTp (App (Var "361" "NatRec") NotErased (Var "368" "m")) (TpVar "372" "Nat")) NotErased (Var "376" "S")) NotErased (Var "378" "n"))))) "381") (CmdsNext (DefTermOrType (DefTerm "383" "mult" (Type (TpArrow (TpVar "390" "Nat") UnerasedArrow (TpArrow (TpVar "396" "Nat") UnerasedArrow (TpVar "402" "Nat")))) (Lam "408" KeptLambda "410" "m" NoClass (Lam "414" KeptLambda "416" "n" NoClass (App (App (AppTp (App (Var "420" "NatRec") NotErased (Var "427" "m")) (TpVar "431" "Nat")) NotErased (Parens "435" (App (Var "436" "add") NotErased (Var "440" "n")) "442")) NotErased (Var "443" "Z"))))) "446") (CmdsNext (DefTermOrType (DefTerm "448" "exp" (Type (TpArrow (TpVar "454" "Nat") UnerasedArrow (TpArrow (TpVar "460" "Nat") UnerasedArrow (TpVar "466" "Nat")))) (Lam "472" KeptLambda "474" "m" NoClass (Lam "478" KeptLambda "480" "n" NoClass (App (App (AppTp (App (Var "484" "NatRec") NotErased (Var "491" "n")) (TpVar "495" "Nat")) NotErased (Parens "499" (App (Var "500" "mult") NotErased (Var "505" "m")) "507")) NotErased (Parens "508" (App (Var "509" "S") NotErased (Var "511" "Z")) "513"))))) "515") (CmdsNext (DefTermOrType (DefTerm "517" "NatInd" (Type (Abs "526" Pi "528" "x" (Tkt (TpVar "532" "Nat")) (Abs "538" All "540" "Q" (Tkk (KndTpArrow (TpVar "544" "Nat") (Star "550"))) (TpArrow (TpParens "554" (Abs "555" All "557" "x" (Tkt (TpVar "561" "Nat")) (TpArrow (TpAppt (TpVar "567" "Q") (Var "569" "x")) UnerasedArrow (TpAppt (TpVar "573" "Q") (Parens "575" (App (Var "576" "S") NotErased (Var "578" "x")) "580")))) "581") UnerasedArrow (TpArrow (TpAppt (TpVar "584" "Q") (Var "586" "Z")) UnerasedArrow (TpAppt (TpVar "590" "Q") (Var "592" "x"))))))) (Lam "598" KeptLambda "600" "x" NoClass (Lam "604" ErasedLambda "606" "Q" NoClass (Lam "610" KeptLambda "612" "s" NoClass (Lam "616" KeptLambda "618" "z" NoClass (App (AppTp (App (App (AppTp (App (Var "622" "a") NotErased (IotaProj (Var "628" "x") "2" "631")) (TpParens "634" (TpLambda "635" "637" "x" (Tkt (TpVar "641" "cNat")) (Abs "648" All "650" "X" (Tkk (Star "654")) (TpArrow (TpParens "658" (Abs "659" Pi "661" "x'" (Tkt (TpVar "666" "Nat")) (TpArrow (TpEq (Var "674" "x") (Var "678" "x'")) UnerasedArrow (TpArrow (TpAppt (TpVar "685" "Q") (Var "687" "x'")) UnerasedArrow (TpVar "692" "X")))) "694") UnerasedArrow (TpVar "697" "X")))) "699")) NotErased (Parens "705" (Lam "706" ErasedLambda "708" "x'" NoClass (Lam "713" KeptLambda "715" "ih" NoClass (Lam "720" ErasedLambda "722" "X" NoClass (Lam "726" KeptLambda "728" "c" NoClass (App (AppTp (Var "732" "ih") (TpVar "737" "X")) NotErased (Parens "739" (Lam "740" KeptLambda "742" "x''" NoClass (Lam "748" KeptLambda "750" "e" NoClass (Lam "754" KeptLambda "756" "u" NoClass (App (App (App (Var "760" "c") NotErased (Parens "762" (App (Var "763" "S") NotErased (Var "765" "x''")) "769")) NotErased (Parens "770" (Rho "771" RhoPlain (Var "773" "e") (Beta "777" NoTerm)) "779")) NotErased (Parens "780" (App (App (Var "781" "s") Erased (Var "784" "x''")) NotErased (Var "788" "u")) "790"))))) "791")))))) "792")) NotErased (Parens "798" (Lam "799" ErasedLambda "801" "X" NoClass (Lam "805" KeptLambda "807" "c" NoClass (App (App (App (Var "811" "c") NotErased (Var "813" "Z")) NotErased (Beta "815" NoTerm)) NotErased (Var "817" "z")))) "819")) (TpParens "822" (TpAppt (TpVar "823" "Q") (Var "825" "x")) "827")) NotErased (Parens "828" (Lam "829" KeptLambda "831" "x'" NoClass (Lam "836" KeptLambda "838" "e" NoClass (Lam "842" KeptLambda "844" "u" NoClass (Rho "848" RhoPlain (Var "850" "e") (Var "854" "u"))))) "856"))))))) "857") CmdsStart)))))))))) "861"))
                            (runAlex cnt $ cedilleParser)))
  
  test_clist = TestCase (do
                          cnt <- readFile "test/tests/clist.ced"
                          (assertEqual "test file clist.ced"
                            (Prelude.Right (File "1" ImportsStart "Clist" ParamsNil (CmdsNext (DefTermOrType (DefType "17" "cList" (KndArrow (Star "25") (Star "29")) (TpLambda "33" "35" "A" (Tkk (Star "39")) (Abs "43" All "45" "X" (Tkk (Star "49")) (TpArrow (TpParens "53" (TpArrow (TpVar "54" "A") UnerasedArrow (TpArrow (TpVar "58" "X") UnerasedArrow (TpVar "62" "X"))) "64") UnerasedArrow (TpArrow (TpVar "67" "X") UnerasedArrow (TpVar "71" "X")))))) "74") (CmdsNext (DefTermOrType (DefTerm "76" "cNil" (Type (Abs "83" All "85" "A" (Tkk (Star "89")) (TpApp (TpVar "93" "cList") (TpVar "101" "A")))) (Lam "105" ErasedLambda "107" "A" NoClass (Lam "111" ErasedLambda "113" "X" NoClass (Lam "117" KeptLambda "119" "c" NoClass (Lam "123" KeptLambda "125" "n" NoClass (Var "129" "n")))))) "132") (CmdsNext (DefTermOrType (DefTerm "134" "cCons" (Type (Abs "142" All "144" "A" (Tkk (Star "148")) (TpArrow (TpVar "152" "A") UnerasedArrow (TpArrow (TpApp (TpVar "156" "cList") (TpVar "164" "A")) UnerasedArrow (TpApp (TpVar "168" "cList") (TpVar "176" "A")))))) (Lam "180" ErasedLambda "182" "A" NoClass (Lam "186" KeptLambda "188" "h" NoClass (Lam "192" KeptLambda "194" "t" NoClass (Lam "198" ErasedLambda "200" "X" NoClass (Lam "204" KeptLambda "206" "c" NoClass (Lam "210" KeptLambda "212" "n" NoClass (App (App (Var "216" "c") NotErased (Var "218" "h")) NotErased (Parens "220" (App (App (AppTp (Var "221" "t") (TpVar "225" "X")) NotErased (Var "227" "c")) NotErased (Var "229" "n")) "231"))))))))) "233") CmdsStart))) "234"))                          
                            (runAlex cnt $ cedilleParser)))
  
  test_list = TestCase (do
                          cnt <- readFile "test/tests/list.ced"
                          (assertEqual "test file list.ced"
                            (Prelude.Right (File "1" ImportsStart "List" ParamsNil (CmdsNext (ImportCmd (Import "16" "clist" NoOptAs (ArgsNil "27") "29")) (CmdsNext (ImportCmd (Import "30" "nat" NoOptAs (ArgsNil "39") "41")) (CmdsNext (DefTermOrType (DefType "43" "cListParametric" (KndPi "61" "63" "A" (Tkk (Star "67")) (KndTpArrow (TpApp (TpVar "71" "cList") (TpVar "79" "A")) (Star "83"))) (TpLambda "89" "91" "A" (Tkk (Star "95")) (TpLambda "99" "101" "l" (Tkt (TpApp (TpVar "105" "cList") (TpVar "113" "A"))) (Abs "117" All "119" "X" (Tkk (Star "123")) (Abs "127" All "129" "Q" (Tkk (KndTpArrow (TpVar "133" "X") (Star "137"))) (Abs "141" All "143" "cons" (Tkt (TpArrow (TpVar "150" "A") UnerasedArrow (TpArrow (TpVar "154" "X") UnerasedArrow (TpVar "158" "X")))) (Abs "162" All "164" "nil" (Tkt (TpVar "170" "X")) (TpArrow (TpParens "179" (Abs "180" Pi "182" "h" (Tkt (TpVar "186" "A")) (Abs "190" All "192" "t" (Tkt (TpVar "196" "X")) (TpArrow (TpAppt (TpVar "200" "Q") (Var "202" "t")) UnerasedArrow (TpAppt (TpVar "206" "Q") (Parens "208" (App (App (Var "209" "cons") NotErased (Var "214" "h")) NotErased (Var "216" "t")) "218"))))) "219") UnerasedArrow (TpArrow (TpAppt (TpVar "222" "Q") (Var "224" "nil")) UnerasedArrow (TpAppt (TpVar "230" "Q") (Parens "232" (App (App (AppTp (Var "233" "l") (TpVar "237" "X")) NotErased (Var "239" "cons")) NotErased (Var "244" "nil")) "248"))))))))))) "250") (CmdsNext (DefTermOrType (DefType "252" "List" (KndArrow (Star "259") (Star "263")) (TpLambda "267" "269" "A" (Tkk (Star "273")) (Iota "277" "279" "x" (SomeType (TpApp (TpVar "283" "cList") (TpVar "291" "A"))) (Iota "295" "297" "_" (SomeType (TpEq (App (App (Var "303" "x") NotErased (Var "305" "cCons")) NotErased (Var "311" "cNil")) (Var "318" "x"))) (TpAppt (TpApp (TpVar "324" "cListParametric") (TpVar "342" "A")) (Var "344" "x")))))) "347") (CmdsNext (DefTermOrType (DefTerm "349" "Nil" (Type (Abs "355" All "357" "A" (Tkk (Star "361")) (TpApp (TpVar "365" "List") (TpVar "372" "A")))) (Lam "376" ErasedLambda "378" "A" NoClass (IotaPair "382" (AppTp (Var "384" "cNil") (TpVar "391" "A")) (IotaPair "395" (Beta "397" (SomeTerm (Var "399" "cNil") "404")) (Lam "407" ErasedLambda "409" "Q" NoClass (Lam "413" ErasedLambda "415" "Q" NoClass (Lam "419" ErasedLambda "421" "cons" NoClass (Lam "428" ErasedLambda "430" "nil" NoClass (Lam "436" KeptLambda "438" "c" NoClass (Lam "442" KeptLambda "444" "n" NoClass (Var "448" "n"))))))) "451") "453"))) "454") (CmdsNext (DefTermOrType (DefTerm "456" "Cons" (Type (Abs "463" All "465" "A" (Tkk (Star "469")) (TpArrow (TpVar "473" "A") UnerasedArrow (TpArrow (TpApp (TpVar "477" "List") (TpVar "484" "A")) UnerasedArrow (TpApp (TpVar "488" "List") (TpVar "495" "A")))))) (Lam "501" ErasedLambda "503" "A" NoClass (Lam "507" KeptLambda "509" "h" NoClass (Lam "513" KeptLambda "515" "t" NoClass (IotaPair "523" (App (App (AppTp (Var "525" "cCons") (TpVar "533" "A")) NotErased (Var "535" "h")) NotErased (IotaProj (Var "537" "t") "1" "540")) (IotaPair "547" (Epsilon "549" Both EpsHnf (Rho "551" RhoPlain (IotaProj (IotaProj (Var "553" "t") "2" "556") "1" "558") (Beta "561" (SomeTerm (App (App (Var "563" "cCons") NotErased (Var "569" "h")) NotErased (Var "571" "t")) "573")))) (Lam "582" ErasedLambda "584" "X" NoClass (Lam "588" ErasedLambda "590" "Q" NoClass (Lam "594" ErasedLambda "596" "cons" NoClass (Lam "603" ErasedLambda "605" "nil" NoClass (Lam "611" KeptLambda "613" "c" NoClass (Lam "617" KeptLambda "619" "n" NoClass (App (App (App (Var "623" "c") NotErased (Var "625" "h")) Erased (Parens "628" (App (App (AppTp (IotaProj (Var "629" "t") "1" "632") (TpVar "635" "X")) NotErased (Var "637" "cons")) NotErased (Var "642" "nil")) "646")) NotErased (Parens "647" (App (App (App (App (AppTp (AppTp (IotaProj (IotaProj (Var "648" "t") "2" "651") "2" "653") (TpVar "656" "X")) (TpVar "660" "Q")) Erased (Var "663" "cons")) Erased (Var "669" "nil")) NotErased (Var "673" "c")) NotErased (Var "675" "n")) "677")))))))) "679") "681"))))) "682") (CmdsNext (DefTermOrType (DefTerm "684" "ListRec" (Type (Abs "694" All "696" "A" (Tkk (Star "700")) (TpArrow (TpApp (TpVar "704" "List") (TpVar "711" "A")) UnerasedArrow (TpApp (TpVar "715" "cList") (TpVar "723" "A"))))) (Lam "727" ErasedLambda "729" "A" NoClass (Lam "733" KeptLambda "735" "l" NoClass (IotaProj (Var "739" "l") "1" "742")))) "744") (CmdsNext (DefTermOrType (DefTerm "746" "ListInd" (Type (Abs "756" All "758" "A" (Tkk (Star "762")) (Abs "766" Pi "768" "l" (Tkt (TpApp (TpVar "772" "List") (TpVar "779" "A"))) (Abs "793" All "795" "P" (Tkk (KndTpArrow (TpApp (TpVar "799" "List") (TpVar "806" "A")) (Star "810"))) (TpArrow (TpParens "824" (Abs "825" Pi "827" "h" (Tkt (TpVar "831" "A")) (Abs "835" All "837" "t" (Tkt (TpApp (TpVar "841" "List") (TpVar "848" "A"))) (TpArrow (TpAppt (TpVar "852" "P") (Var "854" "t")) UnerasedArrow (TpAppt (TpVar "858" "P") (Parens "860" (App (App (AppTp (Var "861" "Cons") (TpVar "868" "A")) NotErased (Var "870" "h")) NotErased (Var "872" "t")) "874"))))) "875") UnerasedArrow (TpArrow (TpAppt (TpVar "888" "P") (Parens "890" (AppTp (Var "891" "Nil") (TpVar "897" "A")) "899")) UnerasedArrow (TpAppt (TpVar "912" "P") (Var "914" "l")))))))) (Lam "918" ErasedLambda "920" "A" NoClass (Lam "924" KeptLambda "926" "l" NoClass (Lam "930" ErasedLambda "932" "P" NoClass (Lam "936" KeptLambda "938" "c" NoClass (Lam "942" KeptLambda "944" "n" NoClass (Rho "948" RhoPlain (Sigma "950" (IotaProj (IotaProj (Var "952" "l") "2" "955") "1" "957")) (Parens "960" (App (App (App (App (AppTp (AppTp (IotaProj (IotaProj (Var "961" "l") "2" "964") "2" "966") (TpParens "969" (TpApp (TpVar "970" "List") (TpVar "977" "A")) "979")) (TpVar "982" "P")) Erased (Parens "985" (AppTp (Var "986" "Cons") (TpVar "993" "A")) "995")) Erased (Parens "997" (AppTp (Var "998" "Nil") (TpVar "1004" "A")) "1006")) NotErased (Var "1007" "c")) NotErased (Var "1009" "n")) "1011")))))))) "1013") (CmdsNext (DefTermOrType (DefTerm "1015" "append" (Type (Abs "1024" All "1026" "A" (Tkk (Star "1030")) (TpArrow (TpApp (TpVar "1034" "List") (TpVar "1041" "A")) UnerasedArrow (TpArrow (TpApp (TpVar "1045" "List") (TpVar "1052" "A")) UnerasedArrow (TpApp (TpVar "1056" "List") (TpVar "1063" "A")))))) (Lam "1069" ErasedLambda "1071" "A" NoClass (Lam "1075" KeptLambda "1077" "l1" NoClass (Lam "1082" KeptLambda "1084" "l2" NoClass (App (App (AppTp (App (AppTp (Var "1093" "ListRec") (TpVar "1103" "A")) NotErased (Var "1105" "l1")) (TpParens "1110" (TpApp (TpVar "1111" "List") (TpVar "1118" "A")) "1120")) NotErased (Parens "1127" (AppTp (Var "1128" "Cons") (TpVar "1135" "A")) "1137")) NotErased (Var "1144" "l2")))))) "1148") (CmdsNext (DefTermOrType (DefTerm "1150" "length" (Type (Abs "1159" All "1161" "A" (Tkk (Star "1165")) (TpArrow (TpApp (TpVar "1169" "List") (TpVar "1176" "A")) UnerasedArrow (TpVar "1180" "Nat")))) (Lam "1187" ErasedLambda "1189" "A" NoClass (Lam "1193" KeptLambda "1195" "l" NoClass (App (App (AppTp (App (AppTp (Var "1202" "ListRec") (TpVar "1212" "A")) NotErased (Var "1214" "l")) (TpVar "1218" "Nat")) NotErased (Parens "1227" (Lam "1228" KeptLambda "1230" "_" NoClass (Var "1234" "S")) "1236")) NotErased (Var "1237" "Z"))))) "1240") (CmdsNext (DefTermOrType (DefTerm "1242" "map" (Type (Abs "1248" All "1250" "A" (Tkk (Star "1254")) (Abs "1258" All "1260" "B" (Tkk (Star "1264")) (TpArrow (TpParens "1268" (TpArrow (TpVar "1269" "A") UnerasedArrow (TpVar "1273" "B")) "1275") UnerasedArrow (TpArrow (TpApp (TpVar "1278" "List") (TpVar "1285" "A")) UnerasedArrow (TpApp (TpVar "1289" "List") (TpVar "1296" "B"))))))) (Lam "1302" ErasedLambda "1304" "A" NoClass (Lam "1308" ErasedLambda "1310" "B" NoClass (Lam "1314" KeptLambda "1316" "f" NoClass (Lam "1320" KeptLambda "1322" "l" NoClass (App (App (AppTp (App (AppTp (Var "1326" "ListRec") (TpVar "1336" "A")) NotErased (Var "1338" "l")) (TpParens "1342" (TpApp (TpVar "1343" "List") (TpVar "1350" "B")) "1352")) NotErased (Parens "1353" (Lam "1354" KeptLambda "1356" "a" NoClass (Lam "1360" KeptLambda "1362" "bl" NoClass (App (App (AppTp (Var "1367" "Cons") (TpVar "1374" "B")) NotErased (Parens "1376" (App (Var "1377" "f") NotErased (Var "1379" "a")) "1381")) NotErased (Var "1382" "bl")))) "1385")) NotErased (Parens "1386" (AppTp (Var "1387" "Nil") (TpVar "1393" "B")) "1395"))))))) "1397") (CmdsNext (DefTermOrType (DefTerm "1399" "foldr" (Type (Abs "1407" All "1409" "A" (Tkk (Star "1413")) (Abs "1417" All "1419" "B" (Tkk (Star "1423")) (TpArrow (TpParens "1427" (TpArrow (TpVar "1428" "A") UnerasedArrow (TpArrow (TpVar "1432" "B") UnerasedArrow (TpVar "1436" "B"))) "1438") UnerasedArrow (TpArrow (TpVar "1441" "B") UnerasedArrow (TpArrow (TpApp (TpVar "1445" "List") (TpVar "1452" "A")) UnerasedArrow (TpVar "1456" "B"))))))) (Lam "1462" ErasedLambda "1464" "A" NoClass (Lam "1468" ErasedLambda "1470" "B" NoClass (Lam "1474" KeptLambda "1476" "f" NoClass (Lam "1480" KeptLambda "1482" "i" NoClass (Lam "1486" KeptLambda "1488" "l" NoClass (App (App (AppTp (App (AppTp (Var "1492" "ListRec") (TpVar "1502" "A")) NotErased (Var "1504" "l")) (TpVar "1508" "B")) NotErased (Var "1510" "f")) NotErased (Var "1512" "i")))))))) "1515") CmdsStart)))))))))))) "1516"))
                            (runAlex cnt $ cedilleParser)))
  
  -- test liftingtype conflict resolution
  test_lifttypes = TestCase (do
                          cnt <- readFile "test/tests/descn.ced"
                          (assertEqual "test file descn.ced"
                            (Prelude.Right (File "1" ImportsStart "descn" ParamsNil (CmdsNext (ImportCmd (Import "16" "or" NoOptAs (ArgsNil "24") "26")) (CmdsNext (ImportCmd (Import "27" "and" NoOptAs (ArgsNil "36") "38")) (CmdsNext (ImportCmd (Import "39" "true" NoOptAs (ArgsNil "49") "51")) (CmdsNext (ImportCmd (Import "52" "nat" NoOptAs (ArgsNil "61") "63")) (CmdsNext (DefTermOrType (DefType "65" "Fin" (KndTpArrow (TpVar "71" "Nat") (Star "77")) (TpLambda "81" "83" "x" (Tkt (TpVar "87" "Nat")) (TpVar "93" "Nat"))) "98") (CmdsNext (DefTermOrType (DefType "153" "Desc" (KndTpArrow (TpVar "160" "Nat") (Star "166")) (TpLambda "170" "172" "n" (Tkt (TpVar "176" "Nat")) (Abs "199" All "201" "X" (Tkk (Star "205")) (TpArrow (TpParens "232" (TpArrow (TpVar "233" "X") UnerasedArrow (TpArrow (TpVar "237" "X") UnerasedArrow (TpVar "241" "X"))) "243") UnerasedArrow (TpArrow (TpParens "274" (TpArrow (TpVar "275" "X") UnerasedArrow (TpArrow (TpVar "279" "X") UnerasedArrow (TpVar "283" "X"))) "285") UnerasedArrow (TpArrow (TpVar "320" "X") UnerasedArrow (TpArrow (TpParens "353" (TpArrow (TpAppt (TpVar "354" "Fin") (Var "358" "n")) UnerasedArrow (TpVar "362" "X")) "364") UnerasedArrow (TpArrow (TpVar "407" "X") UnerasedArrow (TpVar "452" "X"))))))))) "455") (CmdsNext (DefTermOrType (DefType "457" "interp" (KndPi "466" "468" "n" (Tkt (TpVar "472" "Nat")) (KndTpArrow (TpAppt (TpVar "478" "Desc") (Var "483" "n")) (KndArrow (KndParens "487" (KndTpArrow (TpAppt (TpVar "488" "Fin") (Var "492" "n")) (Star "496")) "498") (KndArrow (Star "501") (Star "505"))))) (TpLambda "511" "513" "n" (Tkt (TpVar "517" "Nat")) (TpLambda "523" "525" "d" (Tkt (TpAppt (TpVar "529" "Desc") (Var "534" "n"))) (TpLambda "538" "540" "A" (Tkk (KndParens "544" (KndTpArrow (TpAppt (TpVar "545" "Fin") (Var "549" "n")) (Star "553")) "555")) (TpLambda "560" "562" "X" (Tkk (Star "566")) (TpApp (TpApp (TpApp (TpApp (TpApp (TpParens "570" (Lft "571" "573" "Z" (AppTp (Var "577" "d") (TpVar "581" "Z")) (LiftParens "585" (LiftArrow (LiftParens "586" (LiftArrow (LiftStar "587") (LiftArrow (LiftStar "592") (LiftStar "597"))) "599") (LiftArrow (LiftParens "603" (LiftArrow (LiftStar "604") (LiftArrow (LiftStar "609") (LiftStar "614"))) "616") (LiftArrow (LiftStar "620") (LiftArrow (LiftParens "625" (LiftTpArrow (TpAppt (TpVar "626" "Fin") (Var "630" "n")) (LiftStar "635")) "637") (LiftArrow (LiftStar "641") (LiftStar "646")))))) "648")) "649") (TpVar "667" "Or")) (TpVar "687" "And")) (TpVar "708" "True")) (TpVar "730" "A")) (TpVar "749" "X"))))))) "751") CmdsStart))))))) "753"))
                            (runAlex cnt $ cedilleParser)))
  
  
  test_lifttypes2 = TestCase (do
                          cnt <- readFile "test/tests/sysf-norm.ced"
                          (assertEqual "test file sysf-norm.ced"
                           (Prelude.Right (File "1" ImportsStart "sysf" ParamsNil (CmdsNext (ImportCmd (Import "15" "bool" NoOptAs (ArgsNil "25") "27")) (CmdsNext (ImportCmd (Import "28" "sysf" NoOptAs (ArgsNil "38") "40")) (CmdsNext (ImportCmd (Import "41" "red" NoOptAs (ArgsNil "50") "52")) (CmdsNext (ImportCmd (Import "53" "norm" NoOptAs (ArgsNil "63") "65")) (CmdsNext (DefTermOrType (DefType "68" "Candidat" (KndArrow (KndParens "79" (KndTpArrow (TpVar "80" "trm") (Star "86")) "88") (Star "91")) (TpLambda "97" "99" "R" (Tkk (KndTpArrow (TpVar "103" "trm") (Star "109"))) (Abs "115" Pi "117" "t" (Tkt (TpVar "121" "trm")) (TpArrow (TpAppt (TpVar "127" "R") (Var "129" "t")) UnerasedArrow (TpApp (TpApp (TpVar "138" "And") (TpParens "144" (TpAppt (TpVar "145" "Normalizing") (Var "157" "t")) "159")) (TpParens "170" (Abs "171" Pi "173" "t'" (Tkt (TpVar "178" "trm")) (TpArrow (TpAppt (TpAppt (TpVar "184" "red") (Var "188" "t'")) (Var "191" "t")) UnerasedArrow (TpAppt (TpVar "195" "R") (Var "197" "t'")))) "200")))))) "202") (CmdsNext (DefTermOrType (DefType "205" "ninterp" (KndArrow (KndParens "215" (KndTpArrow (TpVar "216" "Nat") (KndTpArrow (TpVar "222" "trm") (Star "228"))) "230") (KndTpArrow (TpVar "233" "tp") (KndParens "238" (KndTpArrow (TpVar "239" "trm") (Star "245")) "247"))) (TpLambda "252" "254" "R" (Tkk (KndTpArrow (TpVar "258" "Nat") (KndTpArrow (TpVar "264" "trm") (Star "270")))) (TpLambda "274" "276" "T" (Tkt (TpVar "280" "tp")) (TpApp (TpApp (TpApp (Lft "289" "291" "X" (AppTp (Var "295" "T") (TpParens "299" (TpLambda "300" "302" "_" (Tkt (TpVar "306" "tp")) (TpArrow (TpVar "311" "trm") UnerasedArrow (TpVar "317" "X"))) "319")) (LiftParens "333" (LiftArrow (LiftParens "334" (LiftTpArrow (TpVar "335" "tp") (LiftTpArrow (TpVar "341" "tp") (LiftArrow (LiftParens "347" (LiftTpArrow (TpVar "348" "trm") (LiftStar "355")) "357") (LiftArrow (LiftParens "361" (LiftTpArrow (TpVar "362" "trm") (LiftStar "369")) "371") (LiftParens "375" (LiftTpArrow (TpVar "376" "trm") (LiftStar "383")) "385"))))) "386") (LiftArrow (LiftParens "390" (LiftTpArrow (TpVar "391" "Nat") (LiftTpArrow (TpVar "398" "tp") (LiftArrow (LiftParens "404" (LiftArrow (LiftParens "405" (LiftTpArrow (TpVar "406" "trm") (LiftStar "413")) "415") (LiftParens "419" (LiftTpArrow (TpVar "420" "trm") (LiftStar "427")) "429")) "430") (LiftParens "434" (LiftTpArrow (TpVar "435" "trm") (LiftStar "442")) "444")))) "445") (LiftArrow (LiftParens "449" (LiftTpArrow (TpVar "450" "Nat") (LiftParens "457" (LiftTpArrow (TpVar "458" "trm") (LiftStar "465")) "467")) "468") (LiftParens "472" (LiftTpArrow (TpVar "473" "trm") (LiftStar "480")) "482")))) "483")) (TpParens "498" (TpLambda "499" "501" "_" (Tkt (TpVar "505" "tp")) (TpLambda "510" "512" "_" (Tkt (TpVar "516" "tp")) (TpLambda "521" "523" "S1" (Tkk (KndParens "528" (KndTpArrow (TpVar "529" "trm") (Star "535")) "537")) (TpLambda "540" "542" "S2" (Tkk (KndParens "547" (KndTpArrow (TpVar "548" "trm") (Star "554")) "556")) (TpLambda "559" "561" "t" (Tkt (TpVar "565" "trm")) (TpApp (TpApp (TpVar "579" "And") (TpParens "585" (TpAppt (TpVar "586" "Normalizing") (Var "598" "t")) "600")) (TpParens "603" (Abs "604" Pi "606" "t'" (Tkt (TpVar "611" "trm")) (TpArrow (TpAppt (TpVar "617" "S1") (Var "620" "t'")) UnerasedArrow (TpAppt (TpVar "625" "S2") (Parens "628" (App (App (Var "629" "app") NotErased (Var "633" "t")) NotErased (Var "635" "t'")) "638")))) "639"))))))) "640")) (TpParens "648" (TpLambda "649" "651" "_" (Tkt (TpVar "655" "Nat")) (TpLambda "661" "663" "_" (Tkt (TpVar "667" "tp")) (TpLambda "672" "674" "S" (Tkk (KndArrow (KndParens "678" (KndTpArrow (TpVar "679" "trm") (Star "685")) "687") (KndParens "690" (KndTpArrow (TpVar "691" "trm") (Star "697")) "699"))) (TpLambda "702" "704" "t" (Tkt (TpVar "708" "trm")) (Abs "723" All "725" "R" (Tkk (KndTpArrow (TpVar "729" "trm") (Star "735"))) (TpArrow (TpApp (TpVar "739" "Candidat") (TpVar "750" "R")) UnerasedArrow (TpAppt (TpApp (TpVar "754" "S") (TpVar "758" "R")) (Var "760" "t")))))))) "762")) (TpVar "770" "R"))))) "773") (CmdsNext (DefTermOrType (DefType "775" "All-normalizing" (KndTpArrow (TpVar "793" "trm") (Star "799")) (TpLambda "805" "807" "t" (Tkt (TpVar "811" "trm")) (TpAppt (TpVar "817" "Normalizing") (Var "829" "t")))) "832") (CmdsNext (DefTermOrType (DefTerm "834" "all-normalizing-red-lem" (Type (TpApp (TpVar "860" "Candidat") (TpVar "871" "All-normalizing"))) (Lam "891" KeptLambda "893" "t" NoClass (Lam "897" KeptLambda "899" "pf" NoClass (App (App (AppTp (AppTp (Var "908" "mkpair") (TpParens "923" (TpAppt (TpVar "924" "Normalizing") (Var "936" "t")) "938")) (TpParens "947" (Abs "948" Pi "950" "t'" (Tkt (TpVar "955" "trm")) (TpParens "961" (TpArrow (TpParens "962" (TpAppt (TpAppt (TpVar "963" "red") (Var "967" "t'")) (Var "970" "t")) "972") UnerasedArrow (TpParens "975" (TpAppt (TpVar "976" "Normalizing") (Var "988" "t'")) "991")) "992")) "993")) NotErased (Var "1000" "pf")) NotErased (Parens "1009" (Lam "1010" KeptLambda "1012" "t'" NoClass (Lam "1017" KeptLambda "1019" "r" NoClass (Parens "1023" (App (App (App (App (Var "1024" "norm-lem") NotErased (Var "1033" "t")) NotErased (Var "1035" "t'")) NotErased (Var "1038" "pf")) NotErased (Parens "1041" (App (App (App (AppTp (AppTp (Var "1042" "rtc-step") (TpVar "1053" "trm")) (TpVar "1059" "red")) NotErased (Var "1063" "t'")) NotErased (Var "1066" "t")) NotErased (Var "1068" "r")) "1070")) "1071"))) "1072"))))) "1074") (CmdsNext (DefTermOrType (DefTerm "1077" "reducibility-lem" (Type (Abs "1096" Pi "1098" "T" (Tkt (TpVar "1102" "tp")) (Abs "1107" All "1109" "R" (Tkk (KndParens "1113" (KndTpArrow (TpVar "1114" "Nat") (KndTpArrow (TpVar "1120" "trm") (Star "1126"))) "1128")) (TpArrow (TpParens "1131" (Abs "1132" Pi "1134" "i" (Tkt (TpVar "1138" "Nat")) (TpApp (TpVar "1144" "Candidat") (TpParens "1155" (TpAppt (TpVar "1156" "R") (Var "1158" "i")) "1160"))) "1161") UnerasedArrow (TpApp (TpVar "1164" "Candidat") (TpParens "1175" (TpAppt (TpApp (TpVar "1176" "ninterp") (TpVar "1186" "R")) (Var "1188" "T")) "1190")))))) (Lam "1196" KeptLambda "1198" "T" NoClass (Theta "1203" Abstract (Var "1205" "T") (LtermsCons NotErased (Parens "1228" (Lam "1229" KeptLambda "1231" "T1" NoClass (Lam "1236" KeptLambda "1238" "T2" NoClass (Lam "1243" KeptLambda "1245" "_" NoClass (Lam "1249" KeptLambda "1251" "ih2" NoClass (Lam "1257" ErasedLambda "1259" "R" NoClass (Lam "1263" KeptLambda "1265" "cr" NoClass (Lam "1270" KeptLambda "1272" "t" NoClass (Lam "1276" KeptLambda "1278" "u" NoClass (Theta "1290" Abstract (Var "1292" "u") (LtermsCons NotErased (Parens "1304" (Lam "1305" KeptLambda "1307" "a" NoClass (Lam "1311" KeptLambda "1313" "b" NoClass (App (App (AppTp (AppTp (Var "1329" "mkpair") (TpParens "1345" (TpAppt (TpVar "1346" "Normalizing") (Var "1358" "t")) "1360")) (TpParens "1370" (Abs "1371" Pi "1373" "t'" (Tkt (TpVar "1378" "trm")) (TpParens "1384" (TpArrow (TpParens "1385" (TpAppt (TpAppt (TpVar "1386" "red") (Var "1390" "t'")) (Var "1393" "t")) "1395") UnerasedArrow (TpParens "1398" (TpAppt (TpAppt (TpApp (TpVar "1399" "ninterp") (TpVar "1409" "R")) (Parens "1411" (App (App (Var "1412" "arrow") NotErased (Var "1418" "T1")) NotErased (Var "1421" "T2")) "1424")) (Var "1425" "t'")) "1428")) "1429")) "1430")) NotErased (Var "1438" "a")) NotErased (Parens "1447" (Lam "1448" KeptLambda "1450" "t'" NoClass (Lam "1455" KeptLambda "1457" "r" NoClass (App (App (AppTp (AppTp (Var "1470" "mkpair") (TpParens "1489" (TpAppt (TpVar "1490" "Normalizing") (Var "1502" "t'")) "1505")) (TpParens "1518" (Abs "1519" Pi "1521" "t''" (Tkt (TpVar "1527" "trm")) (TpArrow (TpParens "1533" (TpAppt (TpAppt (TpApp (TpVar "1534" "ninterp") (TpVar "1544" "R")) (Var "1546" "T1")) (Var "1549" "t''")) "1553") UnerasedArrow (TpParens "1556" (TpAppt (TpAppt (TpApp (TpVar "1557" "ninterp") (TpVar "1567" "R")) (Var "1569" "T2")) (Parens "1572" (App (App (Var "1573" "app") NotErased (Var "1577" "t'")) NotErased (Var "1580" "t''")) "1584")) "1585"))) "1586")) NotErased (Parens "1597" (App (App (App (App (Var "1598" "norm-lem") NotErased (Var "1607" "t")) NotErased (Var "1609" "t'")) NotErased (Var "1612" "a")) NotErased (Parens "1614" (App (App (App (AppTp (AppTp (Var "1615" "rtc-step") (TpVar "1626" "trm")) (TpVar "1632" "red")) NotErased (Var "1636" "t'")) NotErased (Var "1639" "t")) NotErased (Var "1641" "r")) "1643")) "1644")) NotErased (Parens "1655" (Lam "1656" KeptLambda "1658" "t''" NoClass (Lam "1664" KeptLambda "1666" "pf" NoClass (App (App (App (AppTp (AppTp (Var "1671" "snd") (TpParens "1677" (TpAppt (TpVar "1678" "Normalizing") (Parens "1690" (App (App (Var "1691" "app") NotErased (Var "1695" "t")) NotErased (Var "1697" "t''")) "1701")) "1702")) (TpParens "1735" (Abs "1736" Pi "1738" "t'" (Tkt (TpVar "1743" "trm")) (TpParens "1749" (TpArrow (TpParens "1750" (TpAppt (TpAppt (TpVar "1751" "red") (Var "1755" "t'")) (Parens "1758" (App (App (Var "1759" "app") NotErased (Var "1763" "t")) NotErased (Var "1765" "t''")) "1769")) "1770") UnerasedArrow (TpParens "1773" (TpAppt (TpAppt (TpApp (TpVar "1774" "ninterp") (TpVar "1784" "R")) (Var "1786" "T2")) (Var "1789" "t'")) "1792")) "1793")) "1794")) NotErased (Parens "1804" (App (App (App (AppTp (Var "1805" "ih2") (TpVar "1811" "R")) NotErased (Var "1813" "cr")) NotErased (Parens "1816" (App (App (Var "1817" "app") NotErased (Var "1821" "t")) NotErased (Var "1823" "t''")) "1827")) NotErased (Parens "1828" (App (App (Var "1829" "b") NotErased (Var "1831" "t''")) NotErased (Var "1835" "pf")) "1838")) "1839")) NotErased (Parens "1840" (App (App (Var "1841" "app") NotErased (Var "1845" "t'")) NotErased (Var "1848" "t''")) "1852")) NotErased (Parens "1853" (App (App (App (App (Var "1854" "red-app1") NotErased (Var "1863" "t'")) NotErased (Var "1866" "t")) NotErased (Var "1868" "t''")) NotErased (Var "1872" "r")) "1874")))) "1875")))) "1887")))) "1888") (LtermsNil "1887"))))))))))) "1889") (LtermsCons NotErased (Parens "1907" (Lam "1908" KeptLambda "1910" "i" NoClass (Lam "1914" KeptLambda "1916" "T'" NoClass (Lam "1921" KeptLambda "1923" "ih" NoClass (Lam "1928" ErasedLambda "1930" "R" NoClass (Lam "1934" KeptLambda "1936" "cr" NoClass (Lam "1941" KeptLambda "1943" "t" NoClass (Lam "1947" KeptLambda "1949" "pf" NoClass (App (App (AppTp (AppTp (Var "1962" "mkpair") (TpParens "1979" (TpAppt (TpVar "1980" "Normalizing") (Var "1992" "t")) "1994")) (TpParens "2005" (Abs "2006" Pi "2008" "t'" (Tkt (TpVar "2013" "trm")) (TpArrow (TpParens "2019" (TpAppt (TpAppt (TpVar "2020" "red") (Var "2024" "t'")) (Var "2027" "t")) "2029") UnerasedArrow (TpParens "2032" (TpAppt (TpAppt (TpApp (TpVar "2033" "ninterp") (TpVar "2043" "R")) (Parens "2045" (App (App (Var "2046" "forall") NotErased (Var "2053" "i")) NotErased (Var "2055" "T'")) "2058")) (Var "2059" "t'")) "2062"))) "2063")) NotErased (Parens "2072" (App (AppTp (AppTp (Var "2073" "fst") (TpParens "2089" (TpAppt (TpVar "2090" "Normalizing") (Var "2102" "t")) "2104")) (TpParens "2110" (Abs "2111" Pi "2113" "t'" (Tkt (TpVar "2118" "trm")) (TpParens "2124" (TpArrow (TpParens "2125" (TpAppt (TpAppt (TpVar "2126" "red") (Var "2130" "t'")) (Var "2133" "t")) "2135") UnerasedArrow (TpParens "2138" (TpAppt (TpAppt (TpApp (TpVar "2139" "ninterp") (TpParens "2149" (TpLambda "2150" "2152" "x" (Tkt (TpVar "2156" "Nat")) (TpParens "2162" (TpApp (TpApp (TpParens "2163" (Lft "2164" "2166" "X" (Parens "2170" (AppTp (App (App (Var "2171" "eqnat") NotErased (Var "2177" "x")) NotErased (Var "2179" "i")) (TpParens "2183" (TpLambda "2184" "2186" "_" (Tkt (TpVar "2190" "Bool")) (TpParens "2197" (TpArrow (TpVar "2198" "trm") UnerasedArrow (TpVar "2204" "X")) "2206")) "2207")) "2208") (LiftParens "2211" (LiftArrow (LiftParens "2212" (LiftTpArrow (TpVar "2213" "trm") (LiftStar "2220")) "2222") (LiftArrow (LiftParens "2226" (LiftTpArrow (TpVar "2227" "trm") (LiftStar "2234")) "2236") (LiftTpArrow (TpVar "2240" "trm") (LiftStar "2247")))) "2249")) "2250") (TpVar "2253" "All-normalizing")) (TpParens "2271" (TpAppt (TpVar "2272" "R") (Var "2274" "x")) "2276")) "2277")) "2278")) (Var "2279" "T'")) (Var "2282" "t'")) "2285")) "2286")) "2287")) NotErased (Parens "2298" (App (App (App (AppTp (App (Var "2299" "ih") NotErased (Parens "2302" (Lam "2303" ErasedLambda "2305" "R" NoClass (Lam "2309" KeptLambda "2311" "cr" NoClass (App (Var "2316" "cr") NotErased (Var "2319" "i")))) "2321")) (TpParens "2327" (TpLambda "2328" "2330" "x" (Tkt (TpVar "2334" "Nat")) (TpApp (TpApp (Lft "2340" "2342" "X" (AppTp (Parens "2346" (App (App (Var "2347" "eqnat") NotErased (Var "2353" "x")) NotErased (Var "2355" "i")) "2357") (TpParens "2360" (TpLambda "2361" "2363" "_" (Tkt (TpVar "2367" "Bool")) (TpArrow (TpVar "2374" "trm") UnerasedArrow (TpVar "2380" "X"))) "2382")) (LiftParens "2385" (LiftArrow (LiftParens "2386" (LiftTpArrow (TpVar "2387" "trm") (LiftStar "2394")) "2396") (LiftArrow (LiftParens "2400" (LiftTpArrow (TpVar "2401" "trm") (LiftStar "2408")) "2410") (LiftParens "2414" (LiftTpArrow (TpVar "2415" "trm") (LiftStar "2422")) "2424"))) "2425")) (TpVar "2488" "All-normalizing")) (TpParens "2506" (TpAppt (TpVar "2507" "R") (Var "2509" "x")) "2511"))) "2512")) NotErased (Parens "2518" (Lam "2519" KeptLambda "2521" "x" NoClass (Theta "2525" AbstractEq (Parens "2528" (App (App (Var "2529" "eqnat") NotErased (Var "2535" "x")) NotErased (Var "2537" "i")) "2539") (LtermsCons NotErased (Parens "2540" (Lam "2541" KeptLambda "2543" "u" NoClass (Lam "2547" KeptLambda "2549" "t" NoClass (Lam "2553" KeptLambda "2555" "pf2" NoClass (App (App (Var "2561" "all-normalizing-red-lem") NotErased (Var "2585" "t")) NotErased (Var "2587" "pf2"))))) "2591") (LtermsCons NotErased (Parens "2592" (Lam "2593" KeptLambda "2595" "u" NoClass (App (Var "2599" "cr") NotErased (Var "2602" "i"))) "2604") (LtermsNil "2603"))))) "2605")) NotErased (Var "2632" "t")) NotErased (Parens "2639" (App (AppTp (Var "2640" "pf") (TpVar "2645" "All-normalizing")) NotErased (Var "2661" "all-normalizing-red-lem")) "2685")) "2686")) "2687")) NotErased (Hole "2691"))))))))) "2702") (LtermsCons NotErased (Parens "2727" (Lam "2728" KeptLambda "2730" "i" NoClass (Lam "2734" ErasedLambda "2736" "R" NoClass (Lam "2740" KeptLambda "2742" "cr" NoClass (App (Var "2747" "cr") NotErased (Var "2750" "i"))))) "2752") (LtermsNil "2752"))))))) "2754") CmdsStart))))))))) "3019"))                          
                           (runAlex cnt $ cedilleParser)))
  
  tests = TestList [
      TestLabel "test comments lexer"        test_lexer_comments
    , TestLabel "test lexer"                 test_lexer
    
    --, TestLabel "test atype hole" test_atype_hole 
    --, TestLabel "test atype qvar" test_atype_qvar 
    --, TestLabel "test atype qvar qualified" test_atype_qvar2
    
    , TestLabel "test parser term"           test_parser_term 
    , TestLabel "test parser term defintion" test_parser_deftermtype 
    , TestLabel "test type arrow"            test_type_arrow 
    , TestLabel "test parser command"        test_parser_cmd 
    , TestLabel "test parser cnat module"    test_parser_cnat
    , TestLabel "test cnat.ced"              test_cnat
    , TestLabel "test nat.ced"               test_nat
    , TestLabel "test clist.ced"             test_clist
    , TestLabel "test list.ced"              test_list
  
    -- shift/reduce conflict in lifting types problematic test 
    , TestLabel "test lifting type"          test_parser_liftingtype
    , TestLabel "test descn.ced"             test_lifttypes
    , TestLabel "test sysf-norm.ced"         test_lifttypes2  
  
    ]
  
  main = do
    count  <- Test.HUnit.runTestTT tests
    if Test.HUnit.failures count > 0    
      then Exit.exitFailure
      else return ()
  
  
  