{- |

Description : Test file for Parse_AS_DFOL

-}

import DFOL.AS_DFOL

import DFOL.Parse_AS_DFOL

import Text.ParserCombinators.Parsec

import Common.AnnoState

import Common.Doc

import Common.DocUtils

matrices :: String

matrices = "Nat :: Sort " ++

"Mat :: Nat -> Nat -> Sort " ++

"plus :: Pi m, n : Nat. Mat(m, n) -> Mat(m, n) -> Mat(m, n) " ++

"mult :: Pi p, q, r : Nat. Mat(p, q) -> Mat(q, r) -> Mat(p, r) " ++

".forall m, n : Nat; A, B : Mat(m, n). plus(m, n, A, B) == plus(m, n, B, A) %(plus_commut)% " ++

".forall m, n : Nat; A, B, C : Mat(m, n). plus(m, n, plus(m, n, A, B), C) == plus(m, n, A, plus(m, n, B, C)) %(plus_assoc)% " {- ++

".forall p, q, r, s : Nat; A : Mat(p, q); B : Mat(q, r); C : Mat(r, s). mult(p, r, s, mult(p, q, r, A, B), C) == mult(p, q, s, A, mult(q, r, s, B, C)) %(mult_commut)%" -}

run :: Either ParseError BASIC_SPEC

run = runParser basicSpec (AnnoState [] ()) "" matrices

result :: Pretty a => Either ParseError a -> Doc

result (Right x) = pretty x

result (Left _) = text "Error"