diff --git a/Src/Main.hs b/Src/Main.hs deleted file mode 100644 index ecf3703..0000000 --- a/Src/Main.hs +++ /dev/null @@ -1,6 +0,0 @@ -module Ask.Src.Main where - -import Ask.Src.ChkRaw - -main :: IO () -main = interact filth diff --git a/ask.cabal b/ask.cabal new file mode 100644 index 0000000..92c8e88 --- /dev/null +++ b/ask.cabal @@ -0,0 +1,143 @@ +cabal-version: 3.0 +-- The cabal-version field refers to the version of the .cabal specification, +-- and can be different from the cabal-install (the tool) version and the +-- Cabal (the library) version you are using. As such, the Cabal (the library) +-- version used must be equal or greater than the version stated in this field. +-- Starting from the specification version 2.2, the cabal-version field must be +-- the first thing in the cabal file. + +-- Initial package description 'ask' generated by +-- 'cabal init'. For further documentation, see: +-- http://haskell.org/cabal/users-guide/ +-- +-- The name of the package. +name: ask + +-- The package version. +-- See the Haskell package versioning policy (PVP) for standards +-- guiding when and how versions should be incremented. +-- https://pvp.haskell.org +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 + +tested-with: GHC ==9.8.2 || ==9.6.4 || ==9.4.8 || ==9.2.8 + +-- A short (one-line) description of the package. +-- synopsis: + +-- A longer description of the package. +-- description: + +-- The license under which the package is released. +license: NONE + +-- The package author(s). +author: Conor Mc Bride + +-- An email address to which users can send suggestions, bug reports, and patches. +maintainer: conor.mcbride@strath.ac.uk + +-- A copyright notice. +-- copyright: +category: Language +build-type: Simple + +-- Extra source files to be distributed with the package, such as examples, or a tutorial module. +-- extra-source-files: + +common warnings + ghc-options: -Wall + +library + -- Import common warning flags. + import: warnings + + -- Modules exported by the library. + exposed-modules: Language.Ask.Bwd + , Language.Ask.ChkRaw + , Language.Ask.Context + , Language.Ask.Glueing + , Language.Ask.HalfZip + , Language.Ask.HardwiredRules + , Language.Ask.Hide + , Language.Ask.Lexing + , Language.Ask.OddEven + , Language.Ask.Parsing + , Language.Ask.Printing + , Language.Ask.Progging + , Language.Ask.Proving + , Language.Ask.RawAsk + , Language.Ask.Thin + , Language.Ask.Tm + , Language.Ask.Typing + + + -- Modules included in this library but not exported. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + + -- Other library packages from which modules are imported. + build-depends: base >=4.16 && <=4.21 + , mtl >=2.2 && <2.4 + , containers >= 0.6 && <0.7 + + -- Directories containing source files. + hs-source-dirs: lib + + -- Base language which the package is written in. + default-language: Haskell2010 + +executable ask + -- Import common warning flags. + import: warnings + + -- .hs or .lhs file containing the Main module. + main-is: Main.hs + + -- Modules included in this executable, other than Main. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + + -- Other library packages from which modules are imported. + build-depends: + base ^>=4.19.1.0, + ask + + -- Directories containing source files. + hs-source-dirs: src + + -- Base language which the package is written in. + default-language: Haskell2010 + +test-suite ask-test + -- Import common warning flags. + import: warnings + + -- Base language which the package is written in. + default-language: Haskell2010 + + -- Modules included in this executable, other than Main. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + + -- The interface type and version of the test suite. + type: exitcode-stdio-1.0 + + -- Directories containing source files. + hs-source-dirs: test + + -- The entrypoint to the test suite. + main-is: Main.hs + + -- Test dependencies. + build-depends: + base ^>=4.19.1.0, + ask diff --git a/Src/Bwd.hs b/lib/Language/Ask/Bwd.hs similarity index 93% rename from Src/Bwd.hs rename to lib/Language/Ask/Bwd.hs index a00f113..409b767 100644 --- a/Src/Bwd.hs +++ b/lib/Language/Ask/Bwd.hs @@ -1,6 +1,6 @@ {-# LANGUAGE DeriveTraversable #-} -module Ask.Src.Bwd where +module Language.Ask.Bwd where infixl 3 :<, <>< diff --git a/Src/ChkRaw.hs b/lib/Language/Ask/ChkRaw.hs similarity index 98% rename from Src/ChkRaw.hs rename to lib/Language/Ask/ChkRaw.hs index 7452387..0e6258a 100644 --- a/Src/ChkRaw.hs +++ b/lib/Language/Ask/ChkRaw.hs @@ -1,6 +1,6 @@ {-# LANGUAGE TupleSections, LambdaCase, PatternSynonyms #-} -module Ask.Src.ChkRaw where +module Language.Ask.ChkRaw where import Data.List hiding ((\\)) import Data.Char @@ -13,20 +13,20 @@ import Data.Foldable import Debug.Trace -import Ask.Src.Hide -import Ask.Src.Thin -import Ask.Src.Bwd -import Ask.Src.OddEven -import Ask.Src.Lexing -import Ask.Src.RawAsk -import Ask.Src.Tm -import Ask.Src.Glueing -import Ask.Src.Context -import Ask.Src.Typing -import Ask.Src.Proving -import Ask.Src.Printing -import Ask.Src.HardwiredRules -import Ask.Src.Progging +import Language.Ask.Hide +import Language.Ask.Thin +import Language.Ask.Bwd +import Language.Ask.OddEven +import Language.Ask.Lexing +import Language.Ask.RawAsk +import Language.Ask.Tm +import Language.Ask.Glueing +import Language.Ask.Context +import Language.Ask.Typing +import Language.Ask.Proving +import Language.Ask.Printing +import Language.Ask.HardwiredRules +import Language.Ask.Progging tracy = const id diff --git a/Src/Context.hs b/lib/Language/Ask/Context.hs similarity index 97% rename from Src/Context.hs rename to lib/Language/Ask/Context.hs index 658fb20..dc53ac1 100644 --- a/Src/Context.hs +++ b/lib/Language/Ask/Context.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.Context ---------- +---------- Context ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -11,7 +11,7 @@ , LambdaCase #-} -module Ask.Src.Context where +module Language.Ask.Context where import Control.Monad import qualified Control.Monad.Fail as Fail @@ -19,11 +19,11 @@ import qualified Data.Map as M import Control.Applicative import Control.Arrow ((***)) -import Ask.Src.Bwd -import Ask.Src.Hide -import Ask.Src.Tm -import Ask.Src.Lexing -import Ask.Src.RawAsk +import Language.Ask.Bwd +import Language.Ask.Hide +import Language.Ask.Tm +import Language.Ask.Lexing +import Language.Ask.RawAsk ------------------------------------------------------------------------------ @@ -336,5 +336,3 @@ data Proglem = Proglem , leftAppl :: [(Tm, Tm)] -- ditto for application arguments , rightTy :: Tm -- return type } deriving Show - - diff --git a/Src/Glueing.hs b/lib/Language/Ask/Glueing.hs similarity index 86% rename from Src/Glueing.hs rename to lib/Language/Ask/Glueing.hs index fdc0c19..b934228 100644 --- a/Src/Glueing.hs +++ b/lib/Language/Ask/Glueing.hs @@ -1,7 +1,7 @@ -module Ask.Src.Glueing where +module Language.Ask.Glueing where -import Ask.Src.Tm -import Ask.Src.RawAsk +import Language.Ask.Tm +import Language.Ask.RawAsk data TmR = My Tm diff --git a/Src/HalfZip.hs b/lib/Language/Ask/HalfZip.hs similarity index 91% rename from Src/HalfZip.hs rename to lib/Language/Ask/HalfZip.hs index 4348311..adedbad 100644 --- a/Src/HalfZip.hs +++ b/lib/Language/Ask/HalfZip.hs @@ -1,4 +1,4 @@ -module Ask.Src.HalfZip where +module Language.Ask.HalfZip where class HalfZippable f where halfZipWith :: (x -> y -> Maybe z) -> f x -> f y -> Maybe (f z) diff --git a/Src/HardwiredRules.hs b/lib/Language/Ask/HardwiredRules.hs similarity index 94% rename from Src/HardwiredRules.hs rename to lib/Language/Ask/HardwiredRules.hs index ae3c22b..8fe0ba5 100644 --- a/Src/HardwiredRules.hs +++ b/lib/Language/Ask/HardwiredRules.hs @@ -1,11 +1,11 @@ -module Ask.Src.HardwiredRules where +module Language.Ask.HardwiredRules where import qualified Data.Map as M -import Ask.Src.Bwd -import Ask.Src.Tm -import Ask.Src.RawAsk -import Ask.Src.Context +import Language.Ask.Bwd +import Language.Ask.Tm +import Language.Ask.RawAsk +import Language.Ask.Context myFixities :: FixityTable myFixities = M.fromList diff --git a/Src/Hide.hs b/lib/Language/Ask/Hide.hs similarity index 85% rename from Src/Hide.hs rename to lib/Language/Ask/Hide.hs index a52598b..aa30326 100644 --- a/Src/Hide.hs +++ b/lib/Language/Ask/Hide.hs @@ -1,4 +1,4 @@ -module Ask.Src.Hide where +module Language.Ask.Hide where newtype Hide x = Hide {peek :: x} diff --git a/Src/Lexing.hs b/lib/Language/Ask/Lexing.hs similarity index 99% rename from Src/Lexing.hs rename to lib/Language/Ask/Lexing.hs index bdae3ca..157a4ba 100644 --- a/Src/Lexing.hs +++ b/lib/Language/Ask/Lexing.hs @@ -1,13 +1,13 @@ {-# LANGUAGE EmptyDataDeriving, DeriveFunctor #-} -module Ask.Src.Lexing where +module Language.Ask.Lexing where import Data.Char import Data.List import Data.Bifunctor -import Ask.Src.Bwd -import Ask.Src.OddEven +import Language.Ask.Bwd +import Language.Ask.OddEven lexAll :: String -> Bloc Line lexAll = lexPhase1 . lexPhase0 diff --git a/Src/OddEven.hs b/lib/Language/Ask/OddEven.hs similarity index 97% rename from Src/OddEven.hs rename to lib/Language/Ask/OddEven.hs index 21201ea..bfe849b 100644 --- a/Src/OddEven.hs +++ b/lib/Language/Ask/OddEven.hs @@ -1,4 +1,4 @@ -module Ask.Src.OddEven where +module Language.Ask.OddEven where import Data.Bifunctor import Data.Bifoldable diff --git a/Src/Parsing.hs b/lib/Language/Ask/Parsing.hs similarity index 96% rename from Src/Parsing.hs rename to lib/Language/Ask/Parsing.hs index 27c4a2d..44adde0 100644 --- a/Src/Parsing.hs +++ b/lib/Language/Ask/Parsing.hs @@ -4,14 +4,14 @@ , LambdaCase #-} -module Ask.Src.Parsing where +module Language.Ask.Parsing where import Control.Monad import Control.Applicative import Data.List -import Ask.Src.OddEven -import Ask.Src.Lexing +import Language.Ask.OddEven +import Language.Ask.Lexing newtype ParTok e x = ParTok {parTok :: e -- some sort of read-only environment, never mind what diff --git a/Src/Printing.hs b/lib/Language/Ask/Printing.hs similarity index 96% rename from Src/Printing.hs rename to lib/Language/Ask/Printing.hs index 066bd56..cb590e2 100644 --- a/Src/Printing.hs +++ b/lib/Language/Ask/Printing.hs @@ -1,18 +1,18 @@ {-# LANGUAGE LambdaCase #-} -module Ask.Src.Printing where +module Language.Ask.Printing where import Data.Char import Data.List -import Ask.Src.Hide -import Ask.Src.Bwd -import Ask.Src.Lexing -import Ask.Src.RawAsk -import Ask.Src.Tm -import Ask.Src.Glueing -import Ask.Src.Context -import Ask.Src.Typing +import Language.Ask.Hide +import Language.Ask.Bwd +import Language.Ask.Lexing +import Language.Ask.RawAsk +import Language.Ask.Tm +import Language.Ask.Glueing +import Language.Ask.Context +import Language.Ask.Typing data Spot = AllOK | RadSpot | Infix (Int, Either Assocy Assocy) | Fun | Arg deriving (Show, Eq) data Wot = Rad | Inf (Int, Assocy) | App deriving (Show, Eq) diff --git a/Src/Progging.hs b/lib/Language/Ask/Progging.hs similarity index 95% rename from Src/Progging.hs rename to lib/Language/Ask/Progging.hs index ec7e71b..566f0bc 100644 --- a/Src/Progging.hs +++ b/lib/Language/Ask/Progging.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.Progging ---------- +---------- Progging ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -8,7 +8,7 @@ LambdaCase #-} -module Ask.Src.Progging where +module Language.Ask.Progging where import Data.Char import Data.List hiding ((\\)) @@ -19,14 +19,14 @@ import Control.Arrow ((***)) import Debug.Trace -import Ask.Src.Bwd -import Ask.Src.Hide -import Ask.Src.HalfZip -import Ask.Src.Tm -import Ask.Src.Context -import Ask.Src.Typing -import Ask.Src.Lexing -import Ask.Src.RawAsk +import Language.Ask.Bwd +import Language.Ask.Hide +import Language.Ask.HalfZip +import Language.Ask.Tm +import Language.Ask.Context +import Language.Ask.Typing +import Language.Ask.Lexing +import Language.Ask.RawAsk trade = const id @@ -53,7 +53,7 @@ proglify f (u, s) = go B0 B0 s where x <- fresh "" let xp = (x, Hide a) go (de :< Bind xp (User "")) (iz :< (TE (TP xp), a)) (s // TP xp) - + ------------------------------------------------------------------------------ -- get names from user @@ -163,7 +163,7 @@ inductively p@(Proglem de f u li ls la ty) xs = do Bind (yn, Hide ty) k -> do let yp = (yn, Hide (rfold e4p sb ty)) return ((yn, TP yp) : sb, ga :< Bind yp k) - z -> return (sb, ga :< z) + z -> return (sb, ga :< z) (sb, de) <- mark de return $ Proglem de f u (rfold e4p sb li) @@ -258,4 +258,4 @@ bigg xs z sb (Bind (nom, Hide ty) k : de) g = case k of push $ Bind xp (User x) bigg xs z ((nom, TP xp) : sb) de g _ -> gripe $ NotADataType ty -bigg xs z sb (_ : de) g = bigg xs z sb de g \ No newline at end of file +bigg xs z sb (_ : de) g = bigg xs z sb de g diff --git a/Src/Proving.hs b/lib/Language/Ask/Proving.hs similarity index 94% rename from Src/Proving.hs rename to lib/Language/Ask/Proving.hs index b5ebce8..7da4468 100644 --- a/Src/Proving.hs +++ b/lib/Language/Ask/Proving.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.Proving ---------- +---------- Proving ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -8,20 +8,20 @@ LambdaCase #-} -module Ask.Src.Proving where +module Language.Ask.Proving where import Data.Foldable import Data.Traversable -import Ask.Src.Thin -import Ask.Src.Hide -import Ask.Src.Bwd -import Ask.Src.Lexing -import Ask.Src.RawAsk -import Ask.Src.Tm -import Ask.Src.Glueing -import Ask.Src.Context -import Ask.Src.Typing +import Language.Ask.Thin +import Language.Ask.Hide +import Language.Ask.Bwd +import Language.Ask.Lexing +import Language.Ask.RawAsk +import Language.Ask.Tm +import Language.Ask.Glueing +import Language.Ask.Context +import Language.Ask.Typing import Debug.Trace @@ -40,7 +40,7 @@ by goal a@(_, (t, _, r) :$$ ss) | elem t [Uid, Sym] = do where backchain :: CxE -> AM [(Tel, [Subgoal])] -- list of successes backchain (ByRule _ ((gop, (h, tel)) :<= prems)) - | h == r = + | h == r = cope (do m <- maAM (gop, goal) return [(stan m tel, stan m prems)]) @@ -167,7 +167,7 @@ given goal = do (\ gr -> trice "OOPS" $ gripe gr) return doorStep - True <- trice "BINGO" $ return True + True <- trice "BINGO" $ return True return b ) (\ gr -> go ga) return @@ -252,4 +252,4 @@ under (TE lhs) (TE rhs) (_, (_, _, h) :$$ []) = () <$ go lhs rhs where so ((x, b) : m) ss bs ds so _ _ _ _ = gripe FAIL mo _ _ _ _ _ = gripe FAIL -under _ _ f = gripe FAIL \ No newline at end of file +under _ _ f = gripe FAIL diff --git a/Src/RawAsk.hs b/lib/Language/Ask/RawAsk.hs similarity index 97% rename from Src/RawAsk.hs rename to lib/Language/Ask/RawAsk.hs index 8c7ed6a..d738e93 100644 --- a/Src/RawAsk.hs +++ b/lib/Language/Ask/RawAsk.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.RawAsk ---------- +---------- RawAsk ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -11,12 +11,12 @@ , LambdaCase #-} -module Ask.Src.RawAsk where +module Language.Ask.RawAsk where -import Ask.Src.OddEven -import Ask.Src.Lexing -import Ask.Src.Parsing -import Ask.Src.Tm +import Language.Ask.OddEven +import Language.Ask.Lexing +import Language.Ask.Parsing +import Language.Ask.Tm import qualified Data.Map as M import Control.Applicative @@ -38,7 +38,7 @@ data RawDecl | RawTest Appl (Maybe Appl) | RawProof (Make () Appl) deriving Show - + data RawIntro = RawIntro { introPats :: [Appl] diff --git a/Src/Thin.hs b/lib/Language/Ask/Thin.hs similarity index 97% rename from Src/Thin.hs rename to lib/Language/Ask/Thin.hs index e6eb610..fbff041 100644 --- a/Src/Thin.hs +++ b/lib/Language/Ask/Thin.hs @@ -1,4 +1,4 @@ -module Ask.Src.Thin where +module Language.Ask.Thin where import Data.Bits diff --git a/Src/Tm.hs b/lib/Language/Ask/Tm.hs similarity index 97% rename from Src/Tm.hs rename to lib/Language/Ask/Tm.hs index 8638723..47ae88f 100644 --- a/Src/Tm.hs +++ b/lib/Language/Ask/Tm.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.Tm ---------- +---------- Tm ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -12,7 +12,7 @@ , PatternSynonyms #-} -module Ask.Src.Tm where +module Language.Ask.Tm where import Data.Bits import Data.List hiding ((\\)) @@ -21,10 +21,10 @@ import Control.Arrow ((***)) import Data.Monoid import Control.Monad.Writer -import Ask.Src.Bwd -import Ask.Src.Thin -import Ask.Src.HalfZip -import Ask.Src.Hide +import Language.Ask.Bwd +import Language.Ask.Thin +import Language.Ask.HalfZip +import Language.Ask.Hide ------------------------------------------------------------------------------ @@ -127,7 +127,7 @@ instance Thin s => Thin (Chk s) where thicken th (TC c ts) = TC c <$> thicken th ts thicken th (TB t) = TB <$> thicken th t thicken th (TE s) = TE <$> thicken th s - + instance Thin Syn where TV i <^> th = TV (i <^> th) (t ::: _T) <^> th = (t <^> th) ::: (_T <^> th) @@ -230,7 +230,7 @@ instance Stan Syn where [TV i | i <- [u ..]] sbst u es (t ::: _T) = sbst u es t ::: sbst u es _T sbst u es (e :$ s) = sbst u es e :$ sbst u es s - sbst u es (TF f is as) = TF f (sbst u es is) (sbst u es as) + sbst u es (TF f is as) = TF f (sbst u es is) (sbst u es as) sbst u es e = e abst x i (TP (y, _)) | x == y = TV i <$ tell (Any True) abst x i (t ::: _T) = (:::) <$> abst x i t <*> abst x i _T @@ -302,7 +302,7 @@ instance Stan t => Stan (Hide t) where stan ms (Hide t) = Hide (stan ms t) sbst u es (Hide t) = Hide (sbst u es t) abst x i (Hide t) = Hide <$> abst x i t - + ------------------------------------------------------------------------------ -- Metavariable dependency testing and topological insertion diff --git a/Src/Typing.hs b/lib/Language/Ask/Typing.hs similarity index 98% rename from Src/Typing.hs rename to lib/Language/Ask/Typing.hs index 5962e99..441804b 100644 --- a/Src/Typing.hs +++ b/lib/Language/Ask/Typing.hs @@ -1,6 +1,6 @@ ------------------------------------------------------------------------------ ---------- ---------- ----------- Ask.Src.Typing ---------- +---------- Typing ---------- ---------- ---------- ------------------------------------------------------------------------------ @@ -11,7 +11,7 @@ , TypeSynonymInstances , FlexibleInstances #-} -module Ask.Src.Typing where +module Language.Ask.Typing where --import Data.List import Control.Applicative @@ -23,15 +23,15 @@ import Data.List hiding ((\\)) import Debug.Trace -import Ask.Src.Bwd -import Ask.Src.Thin -import Ask.Src.Hide -import Ask.Src.HalfZip -import Ask.Src.Lexing -import Ask.Src.RawAsk -import Ask.Src.Tm -import Ask.Src.Glueing -import Ask.Src.Context +import Language.Ask.Bwd +import Language.Ask.Thin +import Language.Ask.Hide +import Language.Ask.HalfZip +import Language.Ask.Lexing +import Language.Ask.RawAsk +import Language.Ask.Tm +import Language.Ask.Glueing +import Language.Ask.Context track = const id @@ -328,7 +328,7 @@ elabTm m ty (ls, l@(_, _, y) :$$ ras) = do fst <$> elabVec m y tel ras _ -> gripe FAIL where - + shitSort :: [((String, Tm), Appl)] -> AM [((String, Tm), Appl)] shitSort [] = return [] diff --git a/Src/Makefile b/lib/Makefile similarity index 100% rename from Src/Makefile rename to lib/Makefile diff --git a/Src/Test.html b/lib/Test.html similarity index 100% rename from Src/Test.html rename to lib/Test.html diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..7a3f61b --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,6 @@ +module Main where + +import Language.Ask.ChkRaw + +main :: IO () +main = interact filth diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 index 0000000..3e2059e --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,4 @@ +module Main (main) where + +main :: IO () +main = putStrLn "Test suite not yet implemented."