mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-01 16:12:26 +03:00
Merge branch 'master' into nats
This commit is contained in:
Edwin Brady
GitHub
commit
4cc4099ace
14
INSTALL.md
14
INSTALL.md
@ -1,12 +1,12 @@
|
||||
Installing
|
||||
==========
|
||||
|
||||
The easiest way to install is via the existing generated Scheme code. The
|
||||
requirements are:
|
||||
The easiest way to install is via the existing generated Scheme code.
|
||||
The requirements are:
|
||||
|
||||
* A Scheme compiler; either Chez Scheme (default), or Racket
|
||||
* `bash`, with `realpath`. On Linux, you probably already have this. On
|
||||
a Mac, you can install this with `brew install coreutils`.
|
||||
* A Scheme compiler; either Chez Scheme (default), or Racket.
|
||||
* `bash`, with `realpath`. On Linux, you probably already have this.
|
||||
On a Mac, you can install this with `brew install coreutils`.
|
||||
|
||||
On Windows, it has been reported that installing via `MSYS2` works
|
||||
(https://www.msys2.org/). On Windows older than Windows 8, you may need to
|
||||
@ -16,6 +16,8 @@ On Raspberry Pi, you can bootstrap via Racket.
|
||||
|
||||
By default, code generation is via Chez Scheme. You can use Racket instead,
|
||||
by setting the environment variable `IDRIS2_CG=racket` before running `make`.
|
||||
If you install Chez Scheme from source files, building it locally,
|
||||
make sure you run `./configure --threads` to build multithreading support in.
|
||||
|
||||
1: Set the PREFIX
|
||||
-----------------
|
||||
@ -59,7 +61,7 @@ If all is well, to install, type:
|
||||
----------------------------------------------------
|
||||
|
||||
If you have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot)
|
||||
installed:
|
||||
installed:
|
||||
|
||||
* `make all IDRIS2_BOOT=idris2boot`
|
||||
* `make install IDRIS2_BOOT=idris2boot`
|
||||
|
||||
@ -2,8 +2,6 @@
|
||||
|
||||
PREFIX ?= $(HOME)/.idris2
|
||||
|
||||
CC ?= clang
|
||||
|
||||
# For Windows targets. Set to 1 to support Windows 7.
|
||||
OLD_WIN ?= 0
|
||||
|
||||
@ -34,9 +32,9 @@ else ifneq (, $(findstring bsd, $(MACHINE)))
|
||||
SHLIB_SUFFIX := .so
|
||||
CFLAGS += -fPIC
|
||||
else
|
||||
OS := linux
|
||||
SHLIB_SUFFIX := .so
|
||||
CFLAGS += -fPIC
|
||||
OS := linux
|
||||
SHLIB_SUFFIX := .so
|
||||
CFLAGS += -fPIC
|
||||
endif
|
||||
|
||||
export OS
|
||||
|
||||
@ -82,6 +82,6 @@ a simple recipe for this trivial case:
|
||||
|
||||
package myProject
|
||||
|
||||
pkgs = pruviloj, lightyear
|
||||
depends = pruviloj, lightyear
|
||||
|
||||
- In Atom, use the File menu to Open Folder myProject.
|
||||
|
||||
@ -461,6 +461,34 @@ directory ``build/ttc``, in the root of the source tree, with the directory
|
||||
structure following the directory structure of the source. Executables are
|
||||
placed in ``build/exec``.
|
||||
|
||||
Packages
|
||||
--------
|
||||
|
||||
Dependencies on other packages are now indicated with the ``depends`` field,
|
||||
the ``pkgs`` field is no longer recognized. Also, fields with URLS or other
|
||||
string data (other than module or package names), must be enclosed in double
|
||||
quotes.
|
||||
For example:
|
||||
|
||||
::
|
||||
|
||||
package lightyear
|
||||
|
||||
sourceloc = "git://git@github.com:ziman/lightyear.git"
|
||||
bugtracker = "http://www.github.com/ziman/lightyear/issues"
|
||||
|
||||
depends = effects
|
||||
|
||||
modules = Lightyear
|
||||
, Lightyear.Position
|
||||
, Lightyear.Core
|
||||
, Lightyear.Combinators
|
||||
, Lightyear.StringFile
|
||||
, Lightyear.Strings
|
||||
, Lightyear.Char
|
||||
, Lightyear.Testing
|
||||
|
||||
|
||||
.. _sect-new-features:
|
||||
|
||||
New features
|
||||
|
||||
@ -17,8 +17,6 @@ modules =
|
||||
Compiler.Scheme.Common,
|
||||
Compiler.VMCode,
|
||||
|
||||
Control.Delayed,
|
||||
|
||||
Core.AutoSearch,
|
||||
Core.Binary,
|
||||
Core.CaseBuilder,
|
||||
|
||||
@ -17,8 +17,6 @@ modules =
|
||||
Compiler.Scheme.Common,
|
||||
Compiler.VMCode,
|
||||
|
||||
Control.Delayed,
|
||||
|
||||
Core.AutoSearch,
|
||||
Core.Binary,
|
||||
Core.CaseBuilder,
|
||||
|
||||
20
libs/base/Data/Fuel.idr
Normal file
20
libs/base/Data/Fuel.idr
Normal file
@ -0,0 +1,20 @@
|
||||
module Data.Fuel
|
||||
|
||||
%default total
|
||||
|
||||
||| Fuel for running total operations potentially indefinitely.
|
||||
public export
|
||||
data Fuel = Dry | More (Lazy Fuel)
|
||||
|
||||
||| Provide `n` units of fuel.
|
||||
export
|
||||
limit : Nat -> Fuel
|
||||
limit Z = Dry
|
||||
limit (S n) = More (limit n)
|
||||
|
||||
||| Provide fuel indefinitely.
|
||||
||| This function is fundamentally partial.
|
||||
partial
|
||||
export
|
||||
forever : Fuel
|
||||
forever = More forever
|
||||
@ -6,22 +6,35 @@ module Builtin
|
||||
|
||||
||| Assert to the totality checker that the given expression will always
|
||||
||| terminate.
|
||||
|||
|
||||
||| The multiplicity of its argument is 1, so `assert_total` won't affect how
|
||||
||| many times variables are used. If you're not writing a linear function,
|
||||
||| this doesn't make a difference.
|
||||
|||
|
||||
||| Note: assert_total can reduce at compile time, if required for unification,
|
||||
||| which might mean that it's no longer guarded a subexpression. Therefore,
|
||||
||| it is best to use it around the smallest possible subexpression.
|
||||
%inline
|
||||
public export
|
||||
assert_total : {0 a : _} -> a -> a
|
||||
assert_total : (1 _ : a) -> a
|
||||
assert_total x = x
|
||||
|
||||
||| Assert to the totality checker that y is always structurally smaller than x
|
||||
||| (which is typically a pattern argument, and *must* be in normal form for
|
||||
||| this to work).
|
||||
|||
|
||||
||| The multiplicity of x is 0, so in a linear function, you can pass values to
|
||||
||| x even if they have already been used.
|
||||
||| The multiplicity of y is 1, so `assert_smaller` won't affect how many times
|
||||
||| its y argument is used.
|
||||
||| If you're not writing a linear function, the multiplicities don't make a
|
||||
||| difference.
|
||||
|||
|
||||
||| @ x the larger value (typically a pattern argument)
|
||||
||| @ y the smaller value (typically an argument to a recursive call)
|
||||
%inline
|
||||
public export
|
||||
assert_smaller : {0 a, b : _} -> (x : a) -> (y : b) -> b
|
||||
assert_smaller : (0 x : a) -> (1 y : b) -> b
|
||||
assert_smaller x y = y
|
||||
|
||||
-- Unit type and pairs
|
||||
|
||||
@ -370,9 +370,9 @@ mutual
|
||||
-- let env : SubstCEnv args (MN "eff" 0 :: vars)
|
||||
-- = mkSubst 0 (CLocal fc First) pos args in
|
||||
-- do sc' <- toCExpTree n sc
|
||||
-- let scope = thin {outer=args}
|
||||
-- {inner=vars}
|
||||
-- (MN "eff" 0) sc'
|
||||
-- let scope = insertNames {outer=args}
|
||||
-- {inner=vars}
|
||||
-- [MN "eff" 0] sc'
|
||||
-- pure $ Just (CLet fc (MN "eff" 0) False scr
|
||||
-- (substs env scope))
|
||||
_ => pure Nothing -- there's a normal match to do
|
||||
|
||||
@ -1,16 +0,0 @@
|
||||
||| Utilities functions for contitionally delaying values.
|
||||
module Control.Delayed
|
||||
|
||||
%default total
|
||||
|
||||
||| Type-level function for a conditionally infinite type.
|
||||
public export
|
||||
inf : Bool -> Type -> Type
|
||||
inf False t = t
|
||||
inf True t = Inf t
|
||||
|
||||
||| Type-level function for a conditionally lazy type.
|
||||
public export
|
||||
lazy : Bool -> Type -> Type
|
||||
lazy False t = t
|
||||
lazy True t = Lazy t
|
||||
@ -142,16 +142,6 @@ mutual
|
||||
insertCaseAltNames ns (DefaultCase ct)
|
||||
= DefaultCase (insertCaseNames ns ct)
|
||||
|
||||
export
|
||||
thinTree : {outer, inner : _} ->
|
||||
(n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner)
|
||||
thinTree n (Case idx prf scTy alts)
|
||||
= let MkNVar prf' = insertNVar {n} _ prf in
|
||||
Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
|
||||
thinTree n (STerm i tm) = STerm i (thin n tm)
|
||||
thinTree n (Unmatched msg) = Unmatched msg
|
||||
thinTree n Impossible = Impossible
|
||||
|
||||
export
|
||||
Weaken CaseTree where
|
||||
weakenNs ns t = insertCaseNames {outer = []} ns t
|
||||
|
||||
@ -324,53 +324,6 @@ Show NamedDef where
|
||||
show args ++ " -> " ++ show ret
|
||||
show (MkNmError exp) = "Error: " ++ show exp
|
||||
|
||||
mutual
|
||||
export
|
||||
thin : {outer : _} ->
|
||||
(n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)
|
||||
thin n (CLocal fc prf)
|
||||
= let MkNVar var' = insertNVar {n} _ prf in
|
||||
CLocal fc var'
|
||||
thin _ (CRef fc x) = CRef fc x
|
||||
thin {outer} {inner} n (CLam fc x sc)
|
||||
= let sc' = thin {outer = x :: outer} {inner} n sc in
|
||||
CLam fc x sc'
|
||||
thin {outer} {inner} n (CLet fc x inl val sc)
|
||||
= let sc' = thin {outer = x :: outer} {inner} n sc in
|
||||
CLet fc x inl (thin n val) sc'
|
||||
thin n (CApp fc x xs)
|
||||
= CApp fc (thin n x) (assert_total (map (thin n) xs))
|
||||
thin n (CCon fc x tag xs)
|
||||
= CCon fc x tag (assert_total (map (thin n) xs))
|
||||
thin n (COp fc x xs)
|
||||
= COp fc x (assert_total (map (thin n) xs))
|
||||
thin n (CExtPrim fc p xs)
|
||||
= CExtPrim fc p (assert_total (map (thin n) xs))
|
||||
thin n (CForce fc x) = CForce fc (thin n x)
|
||||
thin n (CDelay fc x) = CDelay fc (thin n x)
|
||||
thin n (CConCase fc sc xs def)
|
||||
= CConCase fc (thin n sc) (assert_total (map (thinConAlt n) xs))
|
||||
(assert_total (map (thin n) def))
|
||||
thin n (CConstCase fc sc xs def)
|
||||
= CConstCase fc (thin n sc) (assert_total (map (thinConstAlt n) xs))
|
||||
(assert_total (map (thin n) def))
|
||||
thin _ (CPrimVal fc x) = CPrimVal fc x
|
||||
thin _ (CErased fc) = CErased fc
|
||||
thin _ (CCrash fc x) = CCrash fc x
|
||||
|
||||
thinConAlt : {outer : _} ->
|
||||
(n : Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ n :: inner)
|
||||
thinConAlt {outer} {inner} n (MkConAlt x tag args sc)
|
||||
= let sc' : CExp ((args ++ outer) ++ inner)
|
||||
= rewrite sym (appendAssociative args outer inner) in sc in
|
||||
MkConAlt x tag args
|
||||
(rewrite appendAssociative args outer (n :: inner) in
|
||||
thin n sc')
|
||||
|
||||
thinConstAlt : {outer : _} ->
|
||||
(n : Name) -> CConstAlt (outer ++ inner) -> CConstAlt (outer ++ n :: inner)
|
||||
thinConstAlt n (MkConstAlt x sc) = MkConstAlt x (thin n sc)
|
||||
|
||||
mutual
|
||||
export
|
||||
insertNames : {outer, inner : _} ->
|
||||
@ -501,7 +454,6 @@ mutual
|
||||
|
||||
export
|
||||
Weaken CExp where
|
||||
weaken = thin {outer = []} _
|
||||
weakenNs ns tm = insertNames {outer = []} ns tm
|
||||
|
||||
-- Substitute some explicit terms for names in a term, and remove those
|
||||
|
||||
@ -2016,6 +2016,13 @@ setAmbigLimit max
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->elabDirectives->ambigLimit = max } defs)
|
||||
|
||||
export
|
||||
setAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
|
||||
Nat -> Core ()
|
||||
setAutoImplicitLimit max
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { options->elabDirectives->autoImplicitLimit = max } defs)
|
||||
|
||||
export
|
||||
isLazyActive : {auto c : Ref Ctxt Defs} ->
|
||||
Core Bool
|
||||
@ -2049,6 +2056,13 @@ getAmbigLimit
|
||||
= do defs <- get Ctxt
|
||||
pure (ambigLimit (elabDirectives (options defs)))
|
||||
|
||||
export
|
||||
getAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
|
||||
Core Nat
|
||||
getAutoImplicitLimit
|
||||
= do defs <- get Ctxt
|
||||
pure (autoImplicitLimit (elabDirectives (options defs)))
|
||||
|
||||
export
|
||||
setPair : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
|
||||
|
||||
@ -113,9 +113,10 @@ mkdirAll dir = if parse dir == emptyPath
|
||||
else do exist <- dirExists dir
|
||||
if exist
|
||||
then pure (Right ())
|
||||
else do case parent dir of
|
||||
else do Right () <- case parent dir of
|
||||
Just parent => mkdirAll parent
|
||||
Nothing => pure (Right ())
|
||||
| err => pure err
|
||||
createDir dir
|
||||
|
||||
-- Given a namespace (i.e. a module name), make the build directory for the
|
||||
|
||||
@ -101,6 +101,7 @@ record ElabDirectives where
|
||||
totality : TotalReq
|
||||
ambigLimit : Nat
|
||||
undottedRecordProjections : Bool
|
||||
autoImplicitLimit : Nat
|
||||
|
||||
public export
|
||||
record Session where
|
||||
@ -150,7 +151,7 @@ defaultSession = MkSessionOpts False False False Chez 0 False False
|
||||
|
||||
export
|
||||
defaultElab : ElabDirectives
|
||||
defaultElab = MkElabDirectives True True CoveringOnly 3 True
|
||||
defaultElab = MkElabDirectives True True CoveringOnly 3 True 50
|
||||
|
||||
export
|
||||
defaults : Options
|
||||
|
||||
@ -711,42 +711,6 @@ insertNVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
|
||||
= let MkNVar prf = insertNVarNames {ns} i x in
|
||||
MkNVar (Later prf)
|
||||
|
||||
export
|
||||
thin : {outer, inner : _} ->
|
||||
(n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
|
||||
thin n (Local fc r idx prf)
|
||||
= let MkNVar var' = insertNVar {n} idx prf in
|
||||
Local fc r _ var'
|
||||
thin n (Ref fc nt name) = Ref fc nt name
|
||||
thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
|
||||
thin {outer} {inner} n (Bind fc x b scope)
|
||||
= let sc' = thin {outer = x :: outer} {inner} n scope in
|
||||
Bind fc x (thinBinder n b) sc'
|
||||
where
|
||||
thinPi : (n : Name) -> PiInfo (Term (outer ++ inner)) ->
|
||||
PiInfo (Term (outer ++ n :: inner))
|
||||
thinPi n Explicit = Explicit
|
||||
thinPi n Implicit = Implicit
|
||||
thinPi n AutoImplicit = AutoImplicit
|
||||
thinPi n (DefImplicit t) = DefImplicit (thin n t)
|
||||
|
||||
thinBinder : (n : Name) -> Binder (Term (outer ++ inner)) ->
|
||||
Binder (Term (outer ++ n :: inner))
|
||||
thinBinder n (Lam c p ty) = Lam c (thinPi n p) (thin n ty)
|
||||
thinBinder n (Let c val ty) = Let c (thin n val) (thin n ty)
|
||||
thinBinder n (Pi c p ty) = Pi c (thinPi n p) (thin n ty)
|
||||
thinBinder n (PVar c p ty) = PVar c (thinPi n p) (thin n ty)
|
||||
thinBinder n (PLet c val ty) = PLet c (thin n val) (thin n ty)
|
||||
thinBinder n (PVTy c ty) = PVTy c (thin n ty)
|
||||
thin n (App fc fn arg) = App fc (thin n fn) (thin n arg)
|
||||
thin n (As fc s nm tm) = As fc s (thin n nm) (thin n tm)
|
||||
thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)
|
||||
thin n (TDelay fc r ty tm) = TDelay fc r (thin n ty) (thin n tm)
|
||||
thin n (TForce fc r tm) = TForce fc r (thin n tm)
|
||||
thin n (PrimVal fc c) = PrimVal fc c
|
||||
thin n (Erased fc i) = Erased fc i
|
||||
thin n (TType fc) = TType fc
|
||||
|
||||
export
|
||||
insertNames : {outer, inner : _} ->
|
||||
(ns : List Name) -> Term (outer ++ inner) ->
|
||||
@ -774,7 +738,6 @@ insertNames ns (TType fc) = TType fc
|
||||
|
||||
export
|
||||
Weaken Term where
|
||||
weaken tm = thin {outer = []} _ tm
|
||||
weakenNs ns tm = insertNames {outer = []} ns tm
|
||||
|
||||
export
|
||||
|
||||
@ -157,6 +157,9 @@ mutual
|
||||
= findSC defs env g pats tm
|
||||
findSC defs env g pats tm
|
||||
= do let (fn, args) = getFnArgs tm
|
||||
-- if it's a 'case' or 'if' just go straight into the arguments
|
||||
Nothing <- handleCase fn args
|
||||
| Just res => pure res
|
||||
fn' <- conIfGuarded fn -- pretend it's a data constructor if
|
||||
-- it has the AllGuarded flag
|
||||
case (g, fn', args) of
|
||||
@ -186,6 +189,14 @@ mutual
|
||||
do scs <- traverse (findSC defs env Unguarded pats) args
|
||||
pure (concat scs)
|
||||
where
|
||||
handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall))
|
||||
handleCase (Ref fc nt n) args
|
||||
= do n' <- toFullNames n
|
||||
if caseFn n'
|
||||
then Just <$> findSCcall defs env g pats fc n 4 args
|
||||
else pure Nothing
|
||||
handleCase _ _ = pure Nothing
|
||||
|
||||
conIfGuarded : Term vars -> Core (Term vars)
|
||||
conIfGuarded (Ref fc Func n)
|
||||
= do defs <- get Ctxt
|
||||
|
||||
@ -392,10 +392,14 @@ mutual
|
||||
expandDo side ps topfc (DoExp fc tm :: rest)
|
||||
= do tm' <- desugar side ps tm
|
||||
rest' <- expandDo side ps topfc rest
|
||||
-- A free standing 'case' block must return ()
|
||||
let ty = case tm' of
|
||||
ICase _ _ _ _ => IVar fc (UN "Unit")
|
||||
_ => Implicit fc False
|
||||
gam <- get Ctxt
|
||||
pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm')
|
||||
(ILam fc top Explicit Nothing
|
||||
(Implicit fc False) rest')
|
||||
ty rest')
|
||||
expandDo side ps topfc (DoBind fc n tm :: rest)
|
||||
= do tm' <- desugar side ps tm
|
||||
rest' <- expandDo side ps topfc rest
|
||||
@ -810,6 +814,7 @@ mutual
|
||||
UndottedRecordProjections b => do
|
||||
pure [IPragma (\nest, env => setUndottedRecordProjections b)]
|
||||
AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
|
||||
AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
|
||||
PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]
|
||||
RewriteName eq rw => pure [IPragma (\nest, env => setRewrite fc eq rw)]
|
||||
PrimInteger n => pure [IPragma (\nest, env => setFromInteger n)]
|
||||
|
||||
@ -1096,6 +1096,10 @@ directive fname indents
|
||||
lvl <- intLit
|
||||
atEnd indents
|
||||
pure (AmbigDepth (fromInteger lvl))
|
||||
<|> do pragma "auto_implicit_depth"
|
||||
dpt <- intLit
|
||||
atEnd indents
|
||||
pure (AutoImplicitDepth (fromInteger dpt))
|
||||
<|> do pragma "pair"
|
||||
ty <- name
|
||||
f <- name
|
||||
@ -1707,6 +1711,9 @@ data CmdArg : Type where
|
||||
||| The command takes an expression.
|
||||
ExprArg : CmdArg
|
||||
|
||||
||| The command takes a list of declarations
|
||||
DeclsArg : CmdArg
|
||||
|
||||
||| The command takes a number.
|
||||
NumberArg : CmdArg
|
||||
|
||||
@ -1721,6 +1728,7 @@ Show CmdArg where
|
||||
show NoArg = ""
|
||||
show NameArg = "<name>"
|
||||
show ExprArg = "<expr>"
|
||||
show DeclsArg = "<decls>"
|
||||
show NumberArg = "<number>"
|
||||
show OptionArg = "<option>"
|
||||
show FileArg = "<filename>"
|
||||
@ -1785,6 +1793,18 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
|
||||
tm <- expr pdef "(interactive)" init
|
||||
pure (command tm)
|
||||
|
||||
declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
|
||||
declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
|
||||
where
|
||||
names : List String
|
||||
names = extractNames parseCmd
|
||||
parse : Rule REPLCmd
|
||||
parse = do
|
||||
symbol ":"
|
||||
runParseCmd parseCmd
|
||||
tm <- topDecl "(interactive)" init
|
||||
pure (command tm)
|
||||
|
||||
optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
|
||||
optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
|
||||
where
|
||||
@ -1845,6 +1865,7 @@ parserCommandsForHelp =
|
||||
, noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
|
||||
, noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
|
||||
, noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
|
||||
, declsArgCmd (ParseKeywordCmd "let") NewDefn "Define a new value"
|
||||
]
|
||||
|
||||
export
|
||||
|
||||
@ -424,6 +424,7 @@ data REPLResult : Type where
|
||||
OptionsSet : List REPLOpt -> REPLResult
|
||||
LogLevelSet : Nat -> REPLResult
|
||||
VersionIs : Version -> REPLResult
|
||||
DefDeclared : REPLResult
|
||||
Exited : REPLResult
|
||||
Edited : EditResult -> REPLResult
|
||||
|
||||
@ -443,6 +444,20 @@ execExp ctm
|
||||
pure $ Executed ctm
|
||||
|
||||
|
||||
execDecls : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto s : Ref Syn SyntaxInfo} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
List PDecl -> Core REPLResult
|
||||
execDecls decls = do
|
||||
traverse_ execDecl decls
|
||||
pure DefDeclared
|
||||
where
|
||||
execDecl : PDecl -> Core ()
|
||||
execDecl decl = do
|
||||
i <- desugarDecl [] decl
|
||||
traverse_ (processDecl [] (MkNested []) []) i
|
||||
|
||||
export
|
||||
compileExp : {auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
@ -492,6 +507,7 @@ process : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
REPLCmd -> Core REPLResult
|
||||
process (NewDefn decls) = execDecls decls
|
||||
process (Eval itm)
|
||||
= do opts <- get ROpts
|
||||
case evalMode opts of
|
||||
|
||||
@ -168,6 +168,7 @@ mutual
|
||||
Extension : LangExt -> Directive
|
||||
DefaultTotality : TotalReq -> Directive
|
||||
UndottedRecordProjections : Bool -> Directive
|
||||
AutoImplicitDepth : Nat -> Directive
|
||||
|
||||
public export
|
||||
data PField : Type where
|
||||
@ -304,6 +305,7 @@ data EditCmd : Type where
|
||||
|
||||
public export
|
||||
data REPLCmd : Type where
|
||||
NewDefn : List PDecl -> REPLCmd
|
||||
Eval : PTerm -> REPLCmd
|
||||
Check : PTerm -> REPLCmd
|
||||
PrintDef : Name -> REPLCmd
|
||||
|
||||
@ -195,7 +195,8 @@ mutual
|
||||
-- so we might as well calculate the whole thing now
|
||||
metaty <- quote defs env aty
|
||||
est <- get EST
|
||||
metaval <- searchVar fc argRig 50 (Resolved (defining est))
|
||||
lim <- getAutoImplicitLimit
|
||||
metaval <- searchVar fc argRig lim (Resolved (defining est))
|
||||
env nm metaty
|
||||
let fntm = App fc tm metaval
|
||||
fnty <- sc defs (toClosure defaultOpts env metaval)
|
||||
|
||||
@ -125,11 +125,11 @@ mutual
|
||||
Show RawImp where
|
||||
show (IVar fc n) = show n
|
||||
show (IPi fc c p n arg ret)
|
||||
= "(%pi " ++ show c ++ " " ++ show p ++
|
||||
" " ++ show n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
|
||||
= "(%pi " ++ show c ++ " " ++ show p ++ " " ++
|
||||
showPrec App n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
|
||||
show (ILam fc c p n arg sc)
|
||||
= "(%lam " ++ show c ++ " " ++ show p ++
|
||||
" " ++ show n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
|
||||
= "(%lam " ++ show c ++ " " ++ show p ++ " " ++
|
||||
showPrec App n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
|
||||
show (ILet fc c n ty val sc)
|
||||
= "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
|
||||
" " ++ show val ++ " " ++ show sc ++ ")"
|
||||
|
||||
@ -64,7 +64,7 @@ idrisTests
|
||||
"interface009", "interface010", "interface011", "interface012",
|
||||
"interface013", "interface014", "interface015",
|
||||
-- Miscellaneous REPL
|
||||
"interpreter001",
|
||||
"interpreter001", "interpreter002",
|
||||
-- Implicit laziness, lazy evaluation
|
||||
"lazy001",
|
||||
-- QTT and linearity related
|
||||
@ -222,6 +222,9 @@ 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
|
||||
then putStrLn "success"
|
||||
else do
|
||||
|
||||
@ -2,13 +2,13 @@
|
||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:263}_[] ?{_:264}_[])")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:260}_[] ?{_:261}_[])")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
|
||||
@ -2,13 +2,13 @@
|
||||
000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
|
||||
0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:263}_[] ?{_:264}_[])")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
|
||||
0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:260}_[] ?{_:261}_[])")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
|
||||
0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
|
||||
0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
|
||||
0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
|
||||
|
||||
@ -1,3 +1,3 @@
|
||||
1/1: Building casetot (casetot.idr)
|
||||
casetot.idr:12:1--13:1:main is not covering:
|
||||
Calls non covering function Main.case block in 2079(290)
|
||||
Calls non covering function Main.case block in 2079(287)
|
||||
|
||||
3
tests/idris2/interpreter002/expected
Normal file
3
tests/idris2/interpreter002/expected
Normal file
@ -0,0 +1,3 @@
|
||||
Main> Main> Main> "Privet, mir!"
|
||||
Main>
|
||||
Bye for now!
|
||||
3
tests/idris2/interpreter002/input
Normal file
3
tests/idris2/interpreter002/input
Normal file
@ -0,0 +1,3 @@
|
||||
:let i : String
|
||||
:let i = "Privet, mir!"
|
||||
i
|
||||
3
tests/idris2/interpreter002/run
Executable file
3
tests/idris2/interpreter002/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --no-banner --no-prelude < input
|
||||
|
||||
rm -rf build
|
||||
@ -1,8 +1,8 @@
|
||||
1/1: Building refprims (refprims.idr)
|
||||
LOG 0: Name: Prelude.List.++
|
||||
LOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
|
||||
LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just _) (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
|
||||
LOG 0: Name: Prelude.Strings.++
|
||||
LOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))
|
||||
LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
|
||||
LOG 0: Resolved name: Prelude.Nat
|
||||
LOG 0: Constructors: [Prelude.Z, Prelude.S]
|
||||
refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
|
||||
@ -12,4 +12,4 @@ Error during reflection: Still not trying
|
||||
refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
|
||||
Error during reflection: Undefined name
|
||||
refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
|
||||
Error during reflection: failed after generating Main.{plus:6081}
|
||||
Error during reflection: failed after generating Main.{plus:5838}
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
Processing as TTC
|
||||
Read TTC
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,5 +1,5 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
|
||||
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
|
||||
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y))))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,8 +1,8 @@
|
||||
Processing as TTImp
|
||||
QTT.yaff:14:1--16:1:When elaborating right hand side of Main.dupbad:
|
||||
QTT.yaff:14:13--16:1:There are 2 uses of linear name x
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
|
||||
Yaffle> Main.baz1 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
|
||||
Yaffle> Main.baz2 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
|
||||
Yaffle> Main.foo : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
|
||||
Yaffle> Main.bar : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
|
||||
Yaffle> Main.baz1 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
|
||||
Yaffle> Main.baz2 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 11) 10))
|
||||
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
|
||||
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
|
||||
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
|
||||
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
|
||||
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 10) 94))
|
||||
Yaffle> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user