diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 7bf3280..202bf18 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -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)) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index eab50ff..78bfa81 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -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 diff --git a/src/Core/TT.idr b/src/Core/TT.idr index a3de943..98c93ea 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -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) diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 62ef19d..a7792d0 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -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 diff --git a/src/Data/IOArray.idr b/src/Data/IOArray.idr index 96d5a28..271ad20 100644 --- a/src/Data/IOArray.idr +++ b/src/Data/IOArray.idr @@ -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" diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index 23ca505..5647ec6 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -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 diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 96a922c..7e7887b 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -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 diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 9a7e37a..8398e43 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -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') diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 05b59e4..aaf6237 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -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 diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index bec500c..fe84b99 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -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) diff --git a/src/TTImp/ProcessParams.idr b/src/TTImp/ProcessParams.idr index 718f15a..31834d5 100644 --- a/src/TTImp/ProcessParams.idr +++ b/src/TTImp/ProcessParams.idr @@ -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 diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 0199771..c4f0f06 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -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 diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index a995e0c..05e9c55 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -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) diff --git a/tests/Main.idr b/tests/Main.idr index f7b8122..09060dc 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -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", diff --git a/tests/idris2/basic029/Params.idr b/tests/idris2/basic029/Params.idr new file mode 100644 index 0000000..298dc6d --- /dev/null +++ b/tests/idris2/basic029/Params.idr @@ -0,0 +1,3 @@ +parameters (x : Nat, y : Nat) + add : Nat + add = x + y diff --git a/tests/idris2/basic029/expected b/tests/idris2/basic029/expected new file mode 100644 index 0000000..1cffd67 --- /dev/null +++ b/tests/idris2/basic029/expected @@ -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! diff --git a/tests/idris2/basic029/input b/tests/idris2/basic029/input new file mode 100644 index 0000000..33f73b1 --- /dev/null +++ b/tests/idris2/basic029/input @@ -0,0 +1,5 @@ +add 1 1 +add 0 0 +add 1 0 +add 0 1 +:q diff --git a/tests/idris2/basic029/run b/tests/idris2/basic029/run new file mode 100644 index 0000000..c2f0c30 --- /dev/null +++ b/tests/idris2/basic029/run @@ -0,0 +1,3 @@ +$1 --no-banner Params.idr < input + +rm -rf build diff --git a/tests/idris2/params001/expected b/tests/idris2/params001/expected new file mode 100644 index 0000000..96e9797 --- /dev/null +++ b/tests/idris2/params001/expected @@ -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 diff --git a/tests/idris2/params001/param.idr b/tests/idris2/params001/param.idr new file mode 100644 index 0000000..1c4f802 --- /dev/null +++ b/tests/idris2/params001/param.idr @@ -0,0 +1,8 @@ +parameters (n:Nat) + namespace X + export + foo : Bool + foo = True + + U : Bool + U = foo diff --git a/tests/idris2/params001/parambad.idr b/tests/idris2/params001/parambad.idr new file mode 100644 index 0000000..864bfb0 --- /dev/null +++ b/tests/idris2/params001/parambad.idr @@ -0,0 +1,7 @@ +parameters (n:Nat) + namespace X + foo : Bool + foo = True + + U : Bool + U = foo diff --git a/tests/idris2/params001/run b/tests/idris2/params001/run new file mode 100755 index 0000000..71c2b12 --- /dev/null +++ b/tests/idris2/params001/run @@ -0,0 +1,6 @@ +unset IDRIS2_PATH + +$1 --no-banner --check param.idr +$1 --no-banner --check parambad.idr + +rm -rf build