content: {- |
  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"
  