mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 22:57:45 +02:00
Code now compiles on windows as well. (Doesn't run well yet)
This commit is contained in:
parent
fbcba8c580
commit
2e901070d9
2 changed files with 22 additions and 20 deletions
|
@ -22,8 +22,8 @@ executable NominalAngluin
|
||||||
build-depends:
|
build-depends:
|
||||||
base >=4.8 && <4.9,
|
base >=4.8 && <4.9,
|
||||||
containers,
|
containers,
|
||||||
|
haskeline,
|
||||||
mtl,
|
mtl,
|
||||||
NLambda,
|
NLambda
|
||||||
readline
|
|
||||||
hs-source-dirs: src
|
hs-source-dirs: src
|
||||||
default-language: Haskell2010
|
default-language: Haskell2010
|
||||||
|
|
|
@ -18,7 +18,7 @@ import qualified Prelude
|
||||||
import Control.Monad.Identity (Identity(..))
|
import Control.Monad.Identity (Identity(..))
|
||||||
|
|
||||||
-- Used in the IO teacher
|
-- Used in the IO teacher
|
||||||
import System.Console.Readline
|
import System.Console.Haskeline
|
||||||
import System.IO.Unsafe (unsafePerformIO)
|
import System.IO.Unsafe (unsafePerformIO)
|
||||||
import Text.Read (readMaybe)
|
import Text.Read (readMaybe)
|
||||||
|
|
||||||
|
@ -102,34 +102,25 @@ instance Teacher TeacherWithIO Atom where
|
||||||
Prelude.putStrLn "# You may use the following atoms:"
|
Prelude.putStrLn "# You may use the following atoms:"
|
||||||
Prelude.putStr "# "
|
Prelude.putStr "# "
|
||||||
Prelude.print $ zip supp [0..]
|
Prelude.print $ zip supp [0..]
|
||||||
answer <- fix (\m -> do
|
answer <- runInputT defaultSettings loop
|
||||||
x <- readline "> "
|
return $ interpret supp answer
|
||||||
|
where
|
||||||
|
loop = do
|
||||||
|
x <- getInputLine "> "
|
||||||
case x of
|
case x of
|
||||||
Nothing -> error "Quit"
|
Nothing -> error "Quit"
|
||||||
Just str -> do
|
Just str -> do
|
||||||
case readMaybe str :: Maybe Form of
|
case readMaybe str :: Maybe Form of
|
||||||
Nothing -> do
|
Nothing -> do
|
||||||
Prelude.putStrLn $ "Unable to parse " ++ str ++ " :: Form"
|
outputStrLn $ "Unable to parse " ++ str ++ " :: Form"
|
||||||
m
|
loop
|
||||||
Just f -> return f
|
Just f -> return f
|
||||||
)
|
|
||||||
return $ interpret supp answer
|
|
||||||
equivalent _ hypothesis = unsafePerformIO $ do
|
equivalent _ hypothesis = unsafePerformIO $ do
|
||||||
Prelude.putStrLn "\n# Is the following automaton correct?"
|
Prelude.putStrLn "\n# Is the following automaton correct?"
|
||||||
Prelude.putStr "# "
|
Prelude.putStr "# "
|
||||||
Prelude.print hypothesis
|
Prelude.print hypothesis
|
||||||
Prelude.putStrLn "# Nothing for Yes, Just [...] for a counter example"
|
Prelude.putStrLn "# Nothing for Yes, Just [...] for a counter example"
|
||||||
answer <- fix (\m -> do
|
answer <- runInputT defaultSettings loop
|
||||||
x <- readline "> "
|
|
||||||
case x of
|
|
||||||
Nothing -> error "Quit"
|
|
||||||
Just str -> do
|
|
||||||
case readMaybe str :: Maybe (Maybe [Prelude.String]) of
|
|
||||||
Nothing -> do
|
|
||||||
Prelude.putStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]"
|
|
||||||
m
|
|
||||||
Just f -> return f
|
|
||||||
)
|
|
||||||
case answer of
|
case answer of
|
||||||
Nothing -> return Nothing
|
Nothing -> return Nothing
|
||||||
Just input -> do
|
Just input -> do
|
||||||
|
@ -142,6 +133,17 @@ instance Teacher TeacherWithIO Atom where
|
||||||
let rels s = and [op i j (s !! i) (s !! j) | i <- [0..n - 1], j <- [0..n - 1], i < j]
|
let rels s = and [op i j (s !! i) (s !! j) | i <- [0..n - 1], j <- [0..n - 1], i < j]
|
||||||
let fseq = filter rels sequence
|
let fseq = filter rels sequence
|
||||||
return $ Just fseq
|
return $ Just fseq
|
||||||
|
where
|
||||||
|
loop = do
|
||||||
|
x <- getInputLine "> "
|
||||||
|
case x of
|
||||||
|
Nothing -> error "Quit"
|
||||||
|
Just str -> do
|
||||||
|
case readMaybe str :: Maybe (Maybe [Prelude.String]) of
|
||||||
|
Nothing -> do
|
||||||
|
outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]"
|
||||||
|
loop
|
||||||
|
Just f -> return f
|
||||||
alphabet _ = atoms
|
alphabet _ = atoms
|
||||||
|
|
||||||
-- Data structure for reading formulas (with the derived Read instance)
|
-- Data structure for reading formulas (with the derived Read instance)
|
||||||
|
|
Loading…
Add table
Reference in a new issue