More post-Idris2-boot cleanups

This commit is contained in:
Kamil Shakirov 2020-08-17 13:16:22 +06:00
parent e985f719f7
commit 68bd8bba52
3 changed files with 15 additions and 26 deletions

View File

@ -44,9 +44,8 @@ Make sure that:
### 2: Installing without an existing Idris 2
If you _don't_ have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot) installed, you can build from pre-built
Chez Scheme source, as long as you have Chez Scheme installed (or,
alternatively, Racket). To do this, enter one of the following:
You can build from pre-built Chez Scheme source, as long as you have Chez Scheme
installed (or, alternatively, Racket). To do this, enter one of the following:
- `make bootstrap SCHEME=chez`
- `make bootstrap-racket`
@ -65,20 +64,14 @@ If all is well, to install, type:
- `make install`
### (Alternative 2: Installing with an existing Idris 2)
### 3: Installing with an existing Idris 2
If you have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot)
installed:
- `make all IDRIS2_BOOT=idris2boot`
- `make install IDRIS2_BOOT=idris2boot`
If you have an earlier version of this Idris 2 installer
If you have an earlier version of this Idris 2 installed
- `make all`
- `make install`
### 3: (Optional) Self-hosting step
### 4: (Optional) Self-hosting step
As a final step, you can rebuild from the newly installed Idris 2 to verify
that everything has worked correctly. Assuming that `idris2` is in your
@ -87,12 +80,12 @@ that everything has worked correctly. Assuming that `idris2` is in your
- `make clean` -- to make sure you're building everything with the new version
- `make all && make install`
### 4: Running tests
### 5: Running tests
After `make all`, type `make test` to check everything works. This uses the
executable in `./build/exec`.
### 5: (Optional) Installing the Idris 2 API
### 6: (Optional) Installing the Idris 2 API
You'll only need this if you're developing support tools, such as an external
code generator. To do so, once everything is successfully installed, type:

View File

@ -35,7 +35,6 @@ import Data.List
-- Data for building recursive calls - the function name, and the structure
-- of the LHS. Only recursive calls with a different structure are okay.
public export -- to keep Idris2-boot happy!
record RecData where
constructor MkRecData
{vars : List Name}
@ -592,7 +591,7 @@ makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
-- Go right to left on variable split, to get the variable we just
-- added first.
-- There must be at least one case split.
((helper :: _), nextdef) <-
((helper :: _), nextdef) <-
searchN 1 $ gendef (record { getRecData = False,
inUnwrap = True,
depth = depth',
@ -601,14 +600,14 @@ makeHelper fc rig opts env letty targetty (Result (locapp, ds) next)
helpern 0 ty
| _ => do log 10 "No results"
noResult
let helperdef = IDef fc helpern (snd helper)
log 10 $ "Def: " ++ show helperdef
pure (Result (def, helperdef :: ds) -- plus helper
(do next' <- next
makeHelper fc rig opts env letty targetty next'))
where
-- convert a metavar application (as created by 'metaVar') to a normal
-- convert a metavar application (as created by 'metaVar') to a normal
-- application (as required by a case block)
toApp : forall vars . Term vars -> Term vars
toApp (Meta fc n i args) = apply fc (Ref fc Func (Resolved i)) args
@ -645,8 +644,8 @@ tryIntermediateWith fc rig opts env ((p, pty) :: rest) ty topty
-- something we can pattern match on (so, NTCon) then apply it,
-- let bind the result, and try to generate a definition for
-- the scope of the let binding
do True <- matchable defs
!(sc defs (toClosure defaultOpts env
do True <- matchable defs
!(sc defs (toClosure defaultOpts env
(Erased fc False)))
| False => noResult
intnty <- genVarName "cty"
@ -680,7 +679,7 @@ tryIntermediateRec : {vars : _} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
FC -> RigCount -> SearchOpts ->
Env Term vars ->
Env Term vars ->
Term vars -> ClosedTerm ->
Maybe RecData -> Core (Search (Term vars, ExprDefs))
tryIntermediateRec fc rig opts env ty topty Nothing = noResult
@ -754,7 +753,7 @@ searchType fc rig opts env topty _ ty
case recData opts of
Nothing => []
Just rd => [tryRecursive fc rig opts env ty topty rd]
let tryIntRec =
let tryIntRec =
if doneSplit opts
then [tryIntermediateRec fc rig opts env ty topty (recData opts)]
else []

View File

@ -245,10 +245,7 @@ runTest opts testPath
| Left err => do print err
pure False
let result = normalize out == normalize exp
-- The issue #116 that made this necessary is fixed, but
-- please resist putting 'result' here until it's also
-- fixed in Idris2-boot!
if normalize out == normalize exp
if result
then putStrLn "success"
else do
putStrLn "FAILURE"