module Helium.StaticAnalysis.Directives.TS_Parser where
import Helium.Syntax.UHA_Syntax
import Helium.Syntax.UHA_Utils (nameFromString)
import qualified Helium.Syntax.UHA_Pretty as PP
import Helium.StaticAnalysis.Directives.TS_Syntax
import Helium.Parser.Lexer (Token, Lexeme)
import Helium.Parser.ParseLibrary hiding (satisfy)
import Helium.Parser.Parser (exp0, type_, atype)
import qualified Helium.Parser.ResolveOperators as ResolveOperators
import Text.ParserCombinators.Parsec
import Data.List (intersperse, intercalate)
import Helium.Parser.OperatorTable
import Helium.Utils.Utils (internalError)
parseTypingStrategies :: OperatorTable -> String -> [Token] -> Either ParseError TypingStrategies
parseTypingStrategies operatorTable filename toks =
runHParser (many parseTypingStrategy) filename toks True
where
parseTypingStrategy :: HParser TypingStrategy
parseTypingStrategy =
do lexSIBLINGS
names <- commas1 (var <|> varop <|> con <|> conop <|> special)
lexSEMI
return (TypingStrategy_Siblings names)
<|>
do typerule <- parseTypeRule
constraints <- many parseConstraint
lexSEMI
return (TypingStrategy_TypingStrategy typerule constraints)
parseTypeRule :: HParser TypeRule
parseTypeRule =
do judgements <- many1 parseJudgement
lexSEMI
let (premises, conclusion) = (init judgements, last judgements)
return (TypeRule_TypeRule (map judgementToSimpleJudgement premises) conclusion)
parseJudgement :: HParser Judgement
parseJudgement =
do expression <- exp0
lexCOLCOL
exprType <- type_
lexSEMI
let resolvedExpression = ResolveOperators.expression operatorTable expression
return (Judgement_Judgement resolvedExpression exprType)
parseConstraint :: HParser UserStatement
parseConstraint =
do
lexPHASE
phase <- fmap read lexInt
return (UserStatement_Phase (fromInteger phase))
<|>
do
lexCONSTRAINTS
theName <- varid
return (UserStatement_MetaVariableConstraints theName)
<|>
parseUserConstraint
parseUserConstraint :: HParser UserStatement
parseUserConstraint = try pPredicate <|> pEquality
where
pPredicate =
do
predClass <- con
predType <- atype
lexCOL
msgLines <- many1 lexString
let message = concat (intersperse "\n" msgLines)
return (UserStatement_Pred predClass predType message)
pEquality =
do
leftType <- type_
lexASGASG
rightType <- type_
lexCOL
msgLines <- many1 lexString
let message = intercalate "\n" msgLines
return (UserStatement_Equal leftType rightType message)
special :: GenParser (SourcePos,Lexeme) SourcePos Name
special = do lexCOL ; return (nameFromString ":")
<|> do lexASGASG ; return (nameFromString "==")
judgementToSimpleJudgement :: Judgement -> SimpleJudgement
judgementToSimpleJudgement judgement =
case judgement of
Judgement_Judgement (Expression_Variable _ theName) tp
-> SimpleJudgement_SimpleJudgement theName tp
Judgement_Judgement expression _
-> internalError "TS_Parser.hs" "judgementToSimpleJudgement"
("the following expression should have been a meta-variable: "++showExpression expression)
showExpression :: Expression -> String
showExpression e = show $ PP.text_Syn_Expression $ PP.wrap_Expression (PP.sem_Expression e) PP.Inh_Expression