edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-28 14:06:26 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into sourcedir

Browse Source
This commit is contained in:
Edwin Brady 2019-10-25 14:07:52 +01:00 committed by GitHub
commit 3b73bf2813
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
22 changed files with 236 additions and 102 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/Core/Binary.idr
View File

@ -62,12 +62,16 @@ record TTCFile extra where
extraData : extra
HasNames a => HasNames (List a) where
full c [] = pure []
full c (n :: ns) = pure $ !(full c n) :: !(full c ns)
full c ns = full_aux c [] ns
where full_aux : Context -> List a -> List a -> Core (List a)
full_aux c res [] = pure (reverse res)
full_aux c res (n :: ns) = full_aux c (!(full c n):: res) ns
resolved c [] = pure []
resolved c (n :: ns) = pure $ !(resolved c n) :: !(resolved c ns)
resolved c ns = resolved_aux c [] ns
where resolved_aux : Context -> List a -> List a -> Core (List a)
resolved_aux c res [] = pure (reverse res)
resolved_aux c res (n :: ns) = resolved_aux c (!(resolved c n) :: res) ns
HasNames (Int, FC, Name) where
full c (i, fc, n) = pure (i, fc, !(full c n))
resolved c (i, fc, n) = pure (i, fc, !(resolved c n))

78
src/Core/Context.idr
View File

@ -719,6 +719,8 @@ record Defs where
userHoles : NameMap ()
-- ^ Metavariables the user still has to fill in. In practice, that's
-- everything with a user accessible name and a definition of Hole
timings : StringMap Integer
-- ^ record of timings from logTimeRecord
-- Label for context references
export
@ -735,15 +737,17 @@ initDefs : Core Defs
initDefs
= do gam <- initCtxt
pure (MkDefs gam [] ["Main"] [] defaults empty 100
empty empty empty [] [] [] 5381 [] [] [] [] [] empty)
empty empty empty [] [] [] 5381 [] [] [] [] [] empty
empty)
-- Reset the context, except for the options
export
clearCtxt : {auto c : Ref Ctxt Defs} ->
Core ()
clearCtxt
= do defs <- get Ctxt
put Ctxt (record { options = options defs } !initDefs)
put Ctxt (record { options = options defs,
timings = timings defs } !initDefs)
export
addHash : {auto c : Ref Ctxt Defs} ->
@ -1879,6 +1883,32 @@ logC lvl cmsg
coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
else pure ()
export
logTimeOver : {auto c : Ref Ctxt Defs} ->
Integer -> Core String -> Core a -> Core a
logTimeOver nsecs str act
= do clock <- coreLift clockTime
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift clockTime
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
when (time > nsecs) $
assert_total $ -- We're not dividing by 0
do str' <- str
coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
pure res
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
export
logTimeWhen : {auto c : Ref Ctxt Defs} ->
Bool -> Lazy String -> Core a -> Core a
@ -1905,6 +1935,48 @@ logTimeWhen p str act
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
-- for ad-hoc profiling, record the time the action takes and add it
-- to the time for the given category
export
logTimeRecord : {auto c : Ref Ctxt Defs} ->
String -> Core a -> Core a
logTimeRecord key act
= do clock <- coreLift clockTime
let nano = 1000000000
let t = seconds clock * nano + nanoseconds clock
res <- act
clock <- coreLift clockTime
let t' = seconds clock * nano + nanoseconds clock
let time = t' - t
defs <- get Ctxt
let tot = case lookup key (timings defs) of
Nothing => 0
Just t => t
put Ctxt (record { timings $= insert key (tot + time) } defs)
pure res
export
showTimeRecord : {auto c : Ref Ctxt Defs} ->
Core ()
showTimeRecord
= do defs <- get Ctxt
traverse_ showTimeLog (toList (timings defs))
where
addZeros : List Char -> String
addZeros [] = "000"
addZeros [x] = "00" ++ cast x
addZeros [x,y] = "0" ++ cast x ++ cast y
addZeros str = pack str
showTimeLog : (String, Integer) -> Core ()
showTimeLog (key, time)
= do coreLift $ putStr (key ++ ": ")
let nano = 1000000000
assert_total $ -- We're not dividing by 0
coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
"s"
export
logTime : {auto c : Ref Ctxt Defs} ->
Lazy String -> Core a -> Core a

11
src/Core/TT.idr
View File

@ -611,7 +611,16 @@ 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 (assert_total (map (thin n) b)) sc'
Bind fc x (thinBinder n b) sc'
where
thinBinder : (n : Name) -> Binder (Term (outer ++ inner)) ->
Binder (Term (outer ++ n :: inner))
thinBinder n (Lam c p ty) = Lam c 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 p (thin n ty)
thinBinder n (PVar c p ty) = PVar c 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 nm tm) = As fc (thin n nm) (thin n tm)
thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)

45
src/Core/Unify.idr
View File

@ -713,31 +713,31 @@ mutual
else postponeS True loc "Postponing constraint"
env (NApp fc hd args) tm
doUnifyBothApps : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
FC -> NHead vars -> List (Closure vars) ->
FC -> NHead vars -> List (Closure vars) ->
Core UnifyResult
doUnifyBothApps mode loc env xfc (NLocal xr x xp) [] yfc (NLocal yr y yp) []
unifyBothApps : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
FC -> NHead vars -> List (Closure vars) ->
FC -> NHead vars -> List (Closure vars) ->
Core UnifyResult
unifyBothApps mode loc env xfc (NLocal xr x xp) [] yfc (NLocal yr y yp) []
= if x == y
then pure success
else convertError loc env (NApp xfc (NLocal xr x xp) [])
(NApp yfc (NLocal yr y yp) [])
-- Locally bound things, in a term (not LHS). Since we have to unify
-- for *all* possible values, we can safely unify the arguments.
doUnifyBothApps InTerm loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
unifyBothApps InTerm loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
= if x == y
then unifyArgs InTerm loc env xargs yargs
else postpone loc "Postponing local app"
env (NApp xfc (NLocal xr x xp) xargs)
(NApp yfc (NLocal yr y yp) yargs)
doUnifyBothApps _ loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
unifyBothApps _ loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
= unifyIfEq True loc env (NApp xfc (NLocal xr x xp) xargs)
(NApp yfc (NLocal yr y yp) yargs)
-- If they're both holes, solve the one with the bigger context
doUnifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
= do invx <- isDefInvertible xi
if xi == yi && (invx || mode == InSearch)
-- Invertible, (from auto implicit search)
@ -764,17 +764,17 @@ mutual
NApp _ (NLocal _ _ _) _ => pure $ S !(localsIn cs)
_ => localsIn cs
doUnifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc fy yargs'
unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc fy yargs'
= unifyApp False mode loc env xfc (NMeta xn xi xargs) xargs'
(NApp yfc fy yargs')
doUnifyBothApps mode loc env xfc fx xargs' yfc (NMeta yn yi yargs) yargs'
unifyBothApps mode loc env xfc fx xargs' yfc (NMeta yn yi yargs) yargs'
= unifyApp True mode loc env xfc (NMeta yn yi yargs) yargs'
(NApp xfc fx xargs')
doUnifyBothApps InSearch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
unifyBothApps InSearch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
= if hdx == hdy
then unifyArgs InSearch loc env xargs yargs
else unifyApp False InSearch loc env xfc fx xargs (NApp yfc fy yargs)
doUnifyBothApps InMatch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
unifyBothApps InMatch loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
= if hdx == hdy
then do logC 5 (do defs <- get Ctxt
xs <- traverse (quote defs env) xargs
@ -782,22 +782,9 @@ mutual
pure ("Matching args " ++ show xs ++ " " ++ show ys))
unifyArgs InMatch loc env xargs yargs
else unifyApp False InMatch loc env xfc fx xargs (NApp yfc fy yargs)
doUnifyBothApps mode loc env xfc fx ax yfc fy ay
unifyBothApps mode loc env xfc fx ax yfc fy ay
= unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
unifyBothApps : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{vars : _} ->
UnifyMode -> FC -> Env Term vars ->
FC -> NHead vars -> List (Closure vars) ->
FC -> NHead vars -> List (Closure vars) ->
Core UnifyResult
unifyBothApps mode loc env xfc hx ax yfc hy ay
= do defs <- get Ctxt
if !(convert defs env (NApp xfc hx ax) (NApp yfc hy ay))
then pure success
else doUnifyBothApps mode loc env xfc hx ax yfc hy ay
-- Comparing multiplicities when converting pi binders
subRig : RigCount -> RigCount -> Bool
subRig Rig1 RigW = True -- we can pass a linear function if a general one is expected

2
src/Data/IOArray.idr
View File

@ -39,7 +39,7 @@ unsafeWriteArray (MkIORawArray p) i val
||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can
||| be implemented on top of this, either with a run time or compile time
||| check.
export
export %inline
unsafeReadArray : IORawArray elem -> Int -> IO elem
unsafeReadArray (MkIORawArray p) i
= do MkRaw val <- foreign FFI_C "idris_arrayGet"

1
src/Idris/Main.idr
View File

@ -169,6 +169,7 @@ stMain opts
when (not $ nobanner session) $
iputStrLn banner
repl {c} {u} {m}
showTimeRecord
else
-- exit with an error code if there was an error, otherwise
-- just exit

9
src/Idris/Parser.idr
View File

@ -994,10 +994,11 @@ paramDecls fname indents
keyword "parameters"
commit
symbol "("
ps <- some (do x <- unqualifiedName
symbol ":"
ty <- typeExpr pdef fname indents
pure (UN x, ty))
ps <- sepBy (symbol ",")
(do x <- unqualifiedName
symbol ":"
ty <- typeExpr pdef fname indents
pure (UN x, ty))
symbol ")"
ds <- assert_total (nonEmptyBlock (topDecl fname))
end <- location

75
src/TTImp/Elab/Ambiguity.idr
View File

@ -317,42 +317,47 @@ checkAlternative rig elabinfo nest env fc (UniqueDefault def) alts mexpected
checkImp rig elabinfo nest env t (Just exp')))
alts')
checkAlternative rig elabinfo nest env fc uniq alts mexpected
= do expected <- maybe (do nm <- genName "altTy"
ty <- metaVar fc Rig0 env nm (TType fc)
pure (gnf env ty))
pure mexpected
let solvemode = case elabMode elabinfo of
InLHS c => InLHS
_ => InTerm
delayOnFailure fc rig env expected ambiguous $
\delayed =>
do solveConstraints solvemode Normal
defs <- get Ctxt
exp <- getTerm expected
= do alts' <- maybe (pure [])
(\exp => pruneByType env !(getNF exp) alts) mexpected
case alts' of
[alt] => checkImp rig elabinfo nest env alt mexpected
_ =>
do expected <- maybe (do nm <- genName "altTy"
ty <- metaVar fc Rig0 env nm (TType fc)
pure (gnf env ty))
pure mexpected
let solvemode = case elabMode elabinfo of
InLHS c => InLHS
_ => InTerm
delayOnFailure fc rig env expected ambiguous $
\delayed =>
do solveConstraints solvemode Normal
defs <- get Ctxt
exp <- getTerm expected
-- We can't just use the old NF on the second attempt,
-- because we might know more now, so recalculate it
let exp' = if delayed
then gnf env exp
else expected
-- We can't just use the old NF on the second attempt,
-- because we might know more now, so recalculate it
let exp' = if delayed
then gnf env exp
else expected
alts' <- pruneByType env !(getNF exp') alts
alts' <- pruneByType env !(getNF exp') alts
logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++
" at " ++ show fc ++
"\nTarget type ") env exp'
let tryall = case uniq of
FirstSuccess => anyOne fc
_ => exactlyOne fc env
tryall (map (\t =>
(getName t,
do res <- checkImp rig elabinfo nest env t (Just exp')
-- Do it twice for interface resolution;
-- first pass gets the determining argument
-- (maybe rethink this, there should be a better
-- way that allows one pass)
solveConstraints solvemode Normal
solveConstraints solvemode Normal
log 10 $ show (getName t) ++ " success"
pure res)) alts')
logGlueNF 5 ("Ambiguous elaboration " ++ show alts' ++
" at " ++ show fc ++
"\nTarget type ") env exp'
let tryall = case uniq of
FirstSuccess => anyOne fc
_ => exactlyOne fc env
tryall (map (\t =>
(getName t,
do res <- checkImp rig elabinfo nest env t (Just exp')
-- Do it twice for interface resolution;
-- first pass gets the determining argument
-- (maybe rethink this, there should be a better
-- way that allows one pass)
solveConstraints solvemode Normal
solveConstraints solvemode Normal
log 10 $ show (getName t) ++ " success"
pure res)) alts')

25
src/TTImp/Elab/App.idr
View File

@ -15,6 +15,16 @@ import TTImp.TTImp
%default covering
checkVisibleNS : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Visibility -> Core ()
checkVisibleNS fc (NS ns x) vis
= if !(isVisible ns)
then if visibleInAny (!getNS :: !getNestedNS) (NS ns x) vis
then pure ()
else throw $ InvisibleName fc (NS ns x) Nothing
else throw $ InvisibleName fc (NS ns x) (Just ns)
checkVisibleNS _ _ _ = pure ()
-- Get the type of a variable, assuming we haven't found it in the nested
-- names. Look in the Env first, then the global context.
getNameType : {vars : _} ->
@ -41,7 +51,7 @@ getNameType rigc env fc x
[(pname, i, def)] <- lookupCtxtName x (gamma defs)
| [] => throw (UndefinedName fc x)
| ns => throw (AmbiguousName fc (map fst ns))
checkVisibleNS !(getFullName pname) (visibility def)
checkVisibleNS fc !(getFullName pname) (visibility def)
rigSafe (multiplicity def) rigc
let nt = case definition def of
PMDef _ _ _ _ _ => Func
@ -60,16 +70,6 @@ getNameType rigc env fc x
rigSafe Rig0 Rig1 = throw (LinearMisuse fc !(getFullName x) Rig0 Rig1)
rigSafe _ _ = pure ()
checkVisibleNS : Name -> Visibility -> Core ()
checkVisibleNS (NS ns x) vis
= if !(isVisible ns)
then if visibleInAny (!getNS :: !getNestedNS) (NS ns x) vis
then pure ()
else throw $ InvisibleName fc (NS ns x) Nothing
else throw $ InvisibleName fc (NS ns x) (Just ns)
checkVisibleNS _ _ = pure ()
-- Get the type of a variable, looking it up in the nested names first.
getVarType : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -95,7 +95,8 @@ getVarType rigc nest env fc x
tm = tmf fc nt
tyenv = useVars (getArgs tm)
(embed (type ndef)) in
do logTerm 10 ("Type of " ++ show n') tyenv
do checkVisibleNS fc (fullname ndef) (visibility ndef)
logTerm 10 ("Type of " ++ show n') tyenv
logTerm 10 ("Expands to") tm
pure (tm, gnf env tyenv)
where

2
src/TTImp/Elab/Local.idr
View File

@ -26,7 +26,7 @@ checkLocal : {vars : _} ->
(expTy : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
= do let defNames = definedInBlock nestdecls
= do let defNames = definedInBlock [] nestdecls
est <- get EST
let f = defining est
names' <- traverse (applyEnv f)

3
src/TTImp/ProcessParams.idr
View File

@ -44,7 +44,8 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
-- Treat the names in the block as 'nested names' so that we expand
-- the applications as we need to
defNames <- traverse inCurrentNS (definedInBlock ds)
defs <- get Ctxt
let defNames = definedInBlock (currentNS defs) ds
names' <- traverse (applyEnv env') defNames
let nestBlock = record { names $= (names' ++) } nest'
traverse (processDecl [] nestBlock env') ds

28
src/TTImp/TTImp.idr
View File

@ -459,19 +459,29 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
setAs is tm = pure tm
export
definedInBlock : List ImpDecl -> List Name
definedInBlock = concatMap defName
definedInBlock : List String -> -- namespace to resolve names
List ImpDecl -> List Name
definedInBlock ns = concatMap (defName ns)
where
getName : ImpTy -> Name
getName (MkImpTy _ n _) = n
defName : ImpDecl -> List Name
defName (IClaim _ _ _ _ ty) = [getName ty]
defName (IData _ _ (MkImpData _ n _ _ cons)) = n :: map getName cons
defName (IData _ _ (MkImpLater _ n _)) = [n]
defName (IParameters _ _ pds) = concatMap defName pds
defName (IRecord _ _ (MkImpRecord _ n _ _ _)) = [n]
defName _ = []
expandNS : List String -> Name -> Name
expandNS [] n = n
expandNS ns (UN n) = NS ns (UN n)
expandNS ns n@(MN _ _) = NS ns n
expandNS ns n@(DN _ _) = NS ns n
expandNS ns n = n
defName : List String -> ImpDecl -> List Name
defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)]
defName ns (IData _ _ (MkImpData _ n _ _ cons))
= expandNS ns n :: map (expandNS ns) (map getName cons)
defName ns (IData _ _ (MkImpLater _ n _)) = [expandNS ns n]
defName ns (IParameters _ _ pds) = concatMap (defName ns) pds
defName ns (INamespace _ _ n nds) = concatMap (defName (n ++ ns)) nds
defName ns (IRecord _ _ (MkImpRecord _ n _ _ _)) = [n]
defName _ _ = []
export
getFC : RawImp -> FC

2
src/TTImp/Utils.idr
View File

@ -86,7 +86,7 @@ mutual
= ICase fc (substNames bound ps y) (substNames bound ps ty)
(map (substNamesClause bound ps) xs)
substNames bound ps (ILocal fc xs y)
= let bound' = definedInBlock xs ++ bound in
= let bound' = definedInBlock [] xs ++ bound in
ILocal fc (map (substNamesDecl bound ps) xs)
(substNames bound' ps y)
substNames bound ps (IApp fc fn arg)

3
tests/Main.idr
View File

@ -28,7 +28,7 @@ idrisTests
"basic011", "basic012", "basic013", "basic014", "basic015",
"basic016", "basic017", "basic018", "basic019", "basic020",
"basic021", "basic022", "basic023", "basic024", "basic025",
"basic026", "basic027", "basic028",
"basic026", "basic027", "basic028", "basic029",
"coverage001", "coverage002", "coverage003", "coverage004",
"error001", "error002", "error003", "error004", "error005",
"error006", "error007", "error008", "error009", "error010",
@ -43,6 +43,7 @@ idrisTests
"lazy001",
"linear001", "linear002", "linear003", "linear004", "linear005",
"linear006", "linear007",
"params001",
"perf001", "perf002",
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006",

3
tests/idris2/basic029/Params.idr Normal file
View File

@ -0,0 +1,3 @@
parameters (x : Nat, y : Nat)
add : Nat
add = x + y

6
tests/idris2/basic029/expected Normal file
View File

@ -0,0 +1,6 @@
1/1: Building Params (Params.idr)
Main> S (S Z)
Main> Z
Main> S Z
Main> S Z
Main> Bye for now!

5
tests/idris2/basic029/input Normal file
View File

@ -0,0 +1,5 @@
add 1 1
add 0 0
add 1 0
add 0 1
:q

3
tests/idris2/basic029/run Normal file
View File

@ -0,0 +1,3 @@
$1 --no-banner Params.idr < input
rm -rf build

4
tests/idris2/params001/expected Normal file
View File

@ -0,0 +1,4 @@
1/1: Building param (param.idr)
1/1: Building parambad (parambad.idr)
parambad.idr:7:7--8:1:While processing right hand side of Main.U at parambad.idr:7:3--8:1:
Name Main.X.foo is private

8
tests/idris2/params001/param.idr Normal file
View File

@ -0,0 +1,8 @@
parameters (n:Nat)
namespace X
export
foo : Bool
foo = True
U : Bool
U = foo

7
tests/idris2/params001/parambad.idr Normal file
View File

@ -0,0 +1,7 @@
parameters (n:Nat)
namespace X
foo : Bool
foo = True
U : Bool
U = foo

6
tests/idris2/params001/run Executable file
View File

@ -0,0 +1,6 @@
unset IDRIS2_PATH
$1 --no-banner --check param.idr
$1 --no-banner --check parambad.idr
rm -rf build