|
| 1 | +module Interaction where |
| 2 | + |
| 3 | +import Prelude hiding (lookup) |
| 4 | +import Generator (generateTerm, generateNamelessTerm) |
| 5 | +import Parser (parseTerm) |
| 6 | +import Stack (emptyStack) |
| 7 | +import Substitution.Named (substitute) |
| 8 | +import Transformer (toNameless, toNamed) |
| 9 | +import Data.Map (empty, lookup) |
| 10 | +import Substitution.Nameless (substituteNameless) |
| 11 | + |
| 12 | +data TermType = Nameless | Named deriving (Show, Eq) |
| 13 | + |
| 14 | +parseTermType :: String -> TermType |
| 15 | +parseTermType "named" = Named |
| 16 | +parseTermType "Named" = Named |
| 17 | +parseTermType "nameless" = Nameless |
| 18 | +parseTermType "Nameless" = Nameless |
| 19 | +parseTermType _ = error "Invalid term type" |
| 20 | + |
| 21 | +getOutputTermType :: IO TermType |
| 22 | +getOutputTermType = putStr "Please enter the type of the output terms (named, nameless): " >> parseTermType <$> getLine |
| 23 | + |
| 24 | +getSubstitutionType :: IO TermType |
| 25 | +getSubstitutionType = putStr "Please enter the type of the substitution to be used (named, nameless): " >> parseTermType <$> getLine |
| 26 | + |
| 27 | +doSubstituteNamed :: String -> String -> String -> String |
| 28 | +doSubstituteNamed term var substituteTerm = generateTerm $ substitute (parseTerm term emptyStack) (head var) (parseTerm substituteTerm emptyStack) |
| 29 | + |
| 30 | +doSubstituteNameless :: String -> String -> String -> TermType -> String |
| 31 | +doSubstituteNameless term var substituteTerm outputTermType = |
| 32 | + let (namelessTerm, context) = toNameless (parseTerm term emptyStack) empty |
| 33 | + substituteVariable = head var `lookup` context |
| 34 | + in case substituteVariable of |
| 35 | + Nothing -> term |
| 36 | + Just index -> |
| 37 | + let (substituteNamelessTerm, updatedContext) = toNameless (parseTerm substituteTerm emptyStack) context |
| 38 | + result = substituteNameless namelessTerm index substituteNamelessTerm |
| 39 | + in if outputTermType == Named |
| 40 | + then generateTerm $ toNamed result updatedContext |
| 41 | + else generateNamelessTerm result |
0 commit comments