module DFOL.Parse_AS_DFOL
(
basicSpec
, symbItems
, symbMapItems
)
where
import qualified Common.Lexer as Lexer
import Common.Parsec
import Common.Token (criticalKeywords)
import qualified Common.Keywords as Keywords
import qualified Common.AnnoState as AnnoState
import Common.GlobalAnnotations (PrefixMap)
import DFOL.AS_DFOL
import Text.ParserCombinators.Parsec
dfolKeys :: [String]
dfolKeys = [Keywords.trueS,
Keywords.falseS,
Keywords.notS,
Keywords.forallS,
Keywords.existsS,
"Univ",
"Sort",
"Form",
"Pi"] ++ criticalKeywords
basicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
basicSpec _ = fmap Basic_spec (AnnoState.trailingAnnosParser basicItemP)
<|>
(Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))
basicItemP :: AnnoState.AParser st BASIC_ITEM
basicItemP = do AnnoState.dotT
f <- formulaP
return $ Axiom_item f
<|>
do ns <- namesP
AnnoState.asKey "::"
t <- typeP
return $ Decl_item (ns, t)
typeP :: AnnoState.AParser st TYPE
typeP = do AnnoState.asKey "Pi"
vs <- varsP
t <- typeP
return $ Pi vs t
<|>
do t <- type1P
(do AnnoState.asKey Keywords.funS
(ts, _) <- type1P `Lexer.separatedBy`
AnnoState.asKey Keywords.funS
let xs = t : ts
return $ Func (init xs) (last xs))
<|>
return t
type1P :: AnnoState.AParser st TYPE
type1P = do AnnoState.asKey "Sort"
return Sort
<|>
do AnnoState.asKey "Form"
return Form
<|>
do AnnoState.asKey "Univ"
Lexer.oParenT
t <- termP
Lexer.cParenT
return $ Univ t
<|>
do t <- termP
return $ Univ t
<|>
do Lexer.oParenT
t <- typeP
Lexer.cParenT
return t
termP :: AnnoState.AParser st TERM
termP = do f <- nameP
do Lexer.oParenT
(as, _) <- termP `Lexer.separatedBy` AnnoState.anComma
Lexer.cParenT
return $ Appl (Identifier f) as
<|> return (Identifier f)
nameP :: AnnoState.AParser st NAME
nameP = Lexer.pToken $ reserved dfolKeys Lexer.scanAnyWords
namesP :: AnnoState.AParser st [NAME]
namesP = fmap fst $ nameP `Lexer.separatedBy` AnnoState.anComma
varP :: AnnoState.AParser st ([NAME], TYPE)
varP = do ns <- namesP
AnnoState.asKey Keywords.colonS
t <- typeP
return (ns, t)
varsP :: AnnoState.AParser st [([NAME], TYPE)]
varsP = do (vs, _) <- varP `Lexer.separatedBy` AnnoState.asKey ";"
AnnoState.dotT
return vs
formulaP :: AnnoState.AParser st FORMULA
formulaP = forallP
<|>
existsP
<|>
formula1P
formula1P :: AnnoState.AParser st FORMULA
formula1P = do f <- formula2P
(do AnnoState.asKey Keywords.equivS
g <- formula2P
return $ Equivalence f g)
<|>
do AnnoState.asKey Keywords.implS
g <- formula2P
return $ Implication f g
<|> return f
formula2P :: AnnoState.AParser st FORMULA
formula2P = do f <- formula3P
(do AnnoState.asKey Keywords.lAnd
(fs, _) <- formula3P `Lexer.separatedBy`
AnnoState.asKey Keywords.lAnd
return $ Conjunction (f : fs))
<|>
do AnnoState.asKey Keywords.lOr
(fs, _) <- formula3P `Lexer.separatedBy`
AnnoState.asKey Keywords.lOr
return $ Disjunction (f : fs)
<|> return f
formula3P :: AnnoState.AParser st FORMULA
formula3P = parenFormulaP
<|>
negP
<|>
formula4P
<|>
trueP
<|>
falseP
formula4P :: AnnoState.AParser st FORMULA
formula4P = do x <- termP
(do AnnoState.asKey "=="
y <- termP
return $ Equality x y)
<|>
return (Pred x)
parenFormulaP :: AnnoState.AParser st FORMULA
parenFormulaP = do Lexer.oParenT
f <- formulaP
Lexer.cParenT
return f
forallP :: AnnoState.AParser st FORMULA
forallP = do AnnoState.asKey Keywords.forallS
vs <- varsP
f <- formulaP
return $ Forall vs f
existsP :: AnnoState.AParser st FORMULA
existsP = do AnnoState.asKey Keywords.existsS
vs <- varsP
f <- formulaP
return $ Exists vs f
negP :: AnnoState.AParser st FORMULA
negP = do AnnoState.asKey Keywords.negS <|> AnnoState.asKey Keywords.notS
f <- formula3P
return $ Negation f
trueP :: AnnoState.AParser st FORMULA
trueP = do AnnoState.asKey Keywords.trueS
return T
falseP :: AnnoState.AParser st FORMULA
falseP = do AnnoState.asKey Keywords.falseS
return F
symbItems :: AnnoState.AParser st SYMB_ITEMS
symbItems = fmap Symb_items namesP
symbMapItems :: AnnoState.AParser st SYMB_MAP_ITEMS
symbMapItems = do (xs, _) <- symbOrMap `Lexer.separatedBy` AnnoState.anComma
return $ Symb_map_items xs
symbOrMap :: AnnoState.AParser st SYMB_OR_MAP
symbOrMap = do s <- nameP
(do AnnoState.asKey Keywords.mapsTo
t <- nameP
return $ Symb_map s t)
<|>
return (Symb s)