remove dead files, update bootstrap
This commit is contained in:
File diff suppressed because one or more lines are too long
@@ -1,47 +0,0 @@
|
|||||||
module Main
|
|
||||||
|
|
||||||
import Lib.Types
|
|
||||||
import Lib.ProcessDecl
|
|
||||||
import Lib.TopContext
|
|
||||||
import Lib.Syntax
|
|
||||||
|
|
||||||
{-
|
|
||||||
|
|
||||||
Expect these to throw. (need failing blocks or a white box test here)
|
|
||||||
After we get pack/lsp issues sorted with this directory
|
|
||||||
|
|
||||||
foo : Maybe (Int × Int) -> Int
|
|
||||||
foo 1 = ?
|
|
||||||
foo _ = ?
|
|
||||||
|
|
||||||
foo : Maybe (Int × Int) -> Int
|
|
||||||
foo (1,1) = ?
|
|
||||||
foo _ = ?
|
|
||||||
|
|
||||||
-}
|
|
||||||
|
|
||||||
testCase : M ()
|
|
||||||
testCase = do
|
|
||||||
-- need to get some defs in here
|
|
||||||
top <- get
|
|
||||||
let ctx = mkCtx top.metaCtx
|
|
||||||
let e = emptyFC
|
|
||||||
-- maybe easier to parse out this data.
|
|
||||||
processDecl (Data e "Foo" (RU e) [])
|
|
||||||
|
|
||||||
tree <- buildTree ctx (MkProb [] (VU emptyFC))
|
|
||||||
--ty <- check (mkCtx top.metaCtx) tm (VU fc)
|
|
||||||
pure ()
|
|
||||||
|
|
||||||
|
|
||||||
main : IO ()
|
|
||||||
main = do
|
|
||||||
-- TODO move the tests elsewhere
|
|
||||||
-- We'll need a new top, start an M, maybe push a few things in there
|
|
||||||
-- run buildTree and see what we get back
|
|
||||||
ctx <- empty
|
|
||||||
Right _ <- runEitherT $ runStateT ctx $ testCase
|
|
||||||
| Left (E fc msg) => putStrLn "Error: \{msg}"
|
|
||||||
putStrLn "done"
|
|
||||||
pure ()
|
|
||||||
-- A telescope is a list of binders, right? I've been leaving things as pi types to be explicit
|
|
||||||
@@ -1,47 +0,0 @@
|
|||||||
package newt-test
|
|
||||||
version = 0.1.0
|
|
||||||
authors = "Steve Dunham"
|
|
||||||
-- maintainers =
|
|
||||||
-- license =
|
|
||||||
-- brief =
|
|
||||||
-- readme =
|
|
||||||
-- homepage =
|
|
||||||
-- sourceloc =
|
|
||||||
-- bugtracker =
|
|
||||||
|
|
||||||
-- the Idris2 version required (e.g. langversion >= 0.5.1)
|
|
||||||
-- langversion
|
|
||||||
|
|
||||||
-- packages to add to search path
|
|
||||||
depends = newt
|
|
||||||
|
|
||||||
-- modules to install
|
|
||||||
-- modules =
|
|
||||||
|
|
||||||
-- main file (i.e. file to load at REPL)
|
|
||||||
main = Main
|
|
||||||
|
|
||||||
-- name of executable
|
|
||||||
executable = "newt-test"
|
|
||||||
-- opts =
|
|
||||||
sourcedir = "src"
|
|
||||||
-- builddir =
|
|
||||||
-- outputdir =
|
|
||||||
|
|
||||||
-- script to run before building
|
|
||||||
-- prebuild =
|
|
||||||
|
|
||||||
-- script to run after building
|
|
||||||
-- postbuild =
|
|
||||||
|
|
||||||
-- script to run after building, before installing
|
|
||||||
-- preinstall =
|
|
||||||
|
|
||||||
-- script to run after installing
|
|
||||||
-- postinstall =
|
|
||||||
|
|
||||||
-- script to run before cleaning
|
|
||||||
-- preclean =
|
|
||||||
|
|
||||||
-- script to run after cleaning
|
|
||||||
-- postclean =
|
|
||||||
Reference in New Issue
Block a user