diff --git a/INSTALL.md b/INSTALL.md index bf3a975e6..78f4311e7 100644 --- a/INSTALL.md +++ b/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` diff --git a/config.mk b/config.mk index 21f98250c..9c7148730 100644 --- a/config.mk +++ b/config.mk @@ -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 diff --git a/docs/source/tutorial/packages.rst b/docs/source/tutorial/packages.rst index 49ec0f022..267fc95c8 100644 --- a/docs/source/tutorial/packages.rst +++ b/docs/source/tutorial/packages.rst @@ -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. diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index c55ffb3db..432a11fd8 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -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 diff --git a/idris2.ipkg b/idris2.ipkg index 5019cb948..588f7e0a7 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -17,8 +17,6 @@ modules = Compiler.Scheme.Common, Compiler.VMCode, - Control.Delayed, - Core.AutoSearch, Core.Binary, Core.CaseBuilder, diff --git a/idris2api.ipkg b/idris2api.ipkg index d274c4a0d..ae03ac332 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -17,8 +17,6 @@ modules = Compiler.Scheme.Common, Compiler.VMCode, - Control.Delayed, - Core.AutoSearch, Core.Binary, Core.CaseBuilder, diff --git a/libs/base/Data/Fuel.idr b/libs/base/Data/Fuel.idr new file mode 100644 index 000000000..71d20e246 --- /dev/null +++ b/libs/base/Data/Fuel.idr @@ -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 diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index bc7f5e960..e6c464d90 100644 --- a/libs/prelude/Builtin.idr +++ b/libs/prelude/Builtin.idr @@ -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 diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index a06176fc1..adc2c8dee 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -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 diff --git a/src/Control/Delayed.idr b/src/Control/Delayed.idr deleted file mode 100644 index 0219a82cc..000000000 --- a/src/Control/Delayed.idr +++ /dev/null @@ -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 diff --git a/src/Core/CaseTree.idr b/src/Core/CaseTree.idr index 6fed505d4..4cabfd2c3 100644 --- a/src/Core/CaseTree.idr +++ b/src/Core/CaseTree.idr @@ -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 diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 9c87ab800..7a562b319 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -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 diff --git a/src/Core/Context.idr b/src/Core/Context.idr index cbe37bf13..2af606c95 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -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) -> diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 38837f209..7f0504609 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -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 diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 01a374f9c..8812c61d3 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -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 diff --git a/src/Core/TT.idr b/src/Core/TT.idr index f31c4727e..44edd98f4 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -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 diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index 4239ed50d..fb66a86b7 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 7d612ebeb..eeb0fae54 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -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)] diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index d8b69e006..ee1a9ac1a 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -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 = "" show ExprArg = "" + show DeclsArg = "" show NumberArg = "" show OptionArg = "