{-# LANGUAGE ScopedTypeVariables #-}

module Parser where

import Text.ParserCombinators.Parsec

import Text.ParserCombinators.Parsec.Expr

import Logic

import Grothendieck

import Structured

import Data.Dynamic

import Data.Maybe

hetParse :: LogicGraph -> String -> SPEC

hetParse (logics@((_, defaultLogic) : _), translations) input =

case runParser spec defaultLogic "" input of

Left err -> error ("parse error at " ++ show err)

Right x -> x

where

spec :: CharParser AnyLogic SPEC

spec = buildExpressionParser table basic

<?> "SPEC"

basic = do { G_logic id <- getState;

b <- parse_basic_spec id;

return (Basic_spec (G_basic_spec id b))}

table = [[Prefix (do {string "logic"; spaces;

name <- many1 alphaNum;

setState

(fromMaybe (error ("logic " ++ name ++ " unknown"))

(lookup name logics));

spaces; return id } )],

[Postfix (do

string "with"; spaces;

do string "logic"; spaces

name <- many1 alphaNum

G_logic (id :: src) <- getState

case lookup name translations of

Nothing -> error ("translation " ++ name ++ " unknown")

Just (G_LTR tr) ->

case coerce (source tr) :: Maybe src of

Nothing -> error "translation type mismatch"

Just _ -> do

setState (G_logic (target tr))

return (\ sp -> Inter_Translation sp (G_LTR tr))

<|> do G_logic id <- getState

sy <- parse_symbol_mapping id

spaces

return (\ sp -> Intra_Translation sp (G_symbol_mapping_list id sy))

)],

[Infix (do {string "then"; spaces; return Extension}) AssocLeft]

]