From 663e1b8f69995b0be77ba53492b5c15249fe5116 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 7 Dec 2019 18:54:02 +0000 Subject: [PATCH] Add uniqueSearch data type option This changes the behaviour of 'auto' implicits so that by default they return the first result, rather than checking for unique results. This is consistent with Idris 1. However, we still want to check for uniqueness somtimes (for example, with interface search, which should reject overlapping results) so the 'uniqueSearch' option means that any auto implicit search for the type should check uniqueness of results. Fixes #169 --- libs/base/Language/Reflection/TTImp.idr | 1 + src/Compiler/Common.idr | 2 +- src/Compiler/CompileExpr.idr | 2 +- src/Core/AutoSearch.idr | 7 ++++- src/Core/Binary.idr | 2 +- src/Core/Context.idr | 40 ++++++++++++++++--------- src/Core/Coverage.idr | 4 +-- src/Core/Reflect.idr | 2 +- src/Core/TTC.idr | 7 +++-- src/Core/Termination.idr | 6 ++-- src/Idris/Elab/Interface.idr | 4 +-- src/Idris/Parser.idr | 2 ++ src/TTImp/Elab/Ambiguity.idr | 2 +- src/TTImp/Elab/App.idr | 4 +-- src/TTImp/Elab/Record.idr | 2 +- src/TTImp/Interactive/CaseSplit.idr | 2 +- src/TTImp/Interactive/ExprSearch.idr | 2 +- src/TTImp/Parser.idr | 2 ++ src/TTImp/ProcessData.idr | 8 +++-- src/TTImp/Reflect.idr | 3 ++ src/TTImp/TTImp.idr | 4 +++ tests/Main.idr | 2 +- tests/idris2/perf003/Auto.idr | 18 +++++++++++ tests/idris2/perf003/expected | 1 + tests/idris2/perf003/run | 3 ++ 25 files changed, 93 insertions(+), 39 deletions(-) create mode 100644 tests/idris2/perf003/Auto.idr create mode 100644 tests/idris2/perf003/expected create mode 100755 tests/idris2/perf003/run diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 0256515..0eac986 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -102,6 +102,7 @@ mutual data DataOpt : Type where SearchBy : List Name -> DataOpt -- determining arguments NoHints : DataOpt -- Don't generate search hints for constructors + UniqueSearch : DataOpt public export data Data : Type where diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 8f349b9..0f0e47f 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -61,7 +61,7 @@ mkNameTags : Defs -> NameTags -> Int -> List Name -> Core NameTags mkNameTags defs tags t [] = pure tags mkNameTags defs tags t (n :: ns) = case !(lookupDefExact n (gamma defs)) of - Just (TCon _ _ _ _ _ _) + Just (TCon _ _ _ _ _ _ _) => mkNameTags defs (insert n t tags) (t + 1) ns _ => mkNameTags defs tags t ns diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 9196b86..50457c3 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -359,7 +359,7 @@ toCDef tags n ty (Builtin {arity} op) getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest) toCDef tags n _ (DCon tag arity) = pure $ MkCon (fromMaybe tag $ lookup n tags) arity -toCDef tags n _ (TCon tag arity _ _ _ _) +toCDef tags n _ (TCon tag arity _ _ _ _ _) = pure $ MkCon (fromMaybe tag $ lookup n tags) arity -- We do want to be able to compile these, but also report an error at run time -- (and, TODO: warn at compile time) diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index a5e7d57..597a116 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -113,6 +113,11 @@ anyOne : {vars : _} -> List (Core (Term vars)) -> Core (Term vars) anyOne fc env top [] = throw (CantSolveGoal fc [] top) +anyOne fc env top [elab] + = catch elab + (\err => case err of + CantSolveGoal _ _ _ => throw err + _ => throw (CantSolveGoal fc [] top)) anyOne fc env top (elab :: elabs) = tryUnify elab (anyOne fc env top elabs) @@ -335,7 +340,7 @@ searchName fc rigc defaults trying depth def top env target (n, ndef) let namety : NameType = case definition ndef of DCon tag arity => DataCon tag arity - TCon tag arity _ _ _ _ => TyCon tag arity + TCon tag arity _ _ _ _ _ => TyCon tag arity _ => Func nty <- nf defs env (embed ty) logNF 10 ("Searching Name " ++ show n) env nty diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 08b18b5..d1b4824 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -27,7 +27,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 12 +ttcVersion = 13 export checkTTCVersion : Int -> Int -> Core () diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 0d76623..7653009 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -43,6 +43,8 @@ data Def : Type where TCon : (tag : Int) -> (arity : Nat) -> (parampos : List Nat) -> -- parameters (detpos : List Nat) -> -- determining arguments + (uniqueAuto : Bool) -> -- should 'auto' implicits check + -- for uniqueness (mutwith : List Name) -> (datacons : List Name) -> Def @@ -68,7 +70,7 @@ Show Def where show (PMDef _ args ct rt pats) = show args ++ "; " ++ show ct show (DCon t a) = "DataCon " ++ show t ++ " " ++ show a - show (TCon t a ps ds ms cons) + show (TCon t a ps ds u ms cons) = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ " constructors: " ++ show cons ++ " mutual with: " ++ show ms @@ -577,9 +579,9 @@ HasNames Def where fullNamesPat (_ ** (env, lhs, rhs)) = pure $ (_ ** (!(full gam env), !(full gam lhs), !(full gam rhs))) - full gam (TCon t a ps ds ms cs) - = pure $ TCon t a ps ds !(traverse (full gam) ms) - !(traverse (full gam) cs) + full gam (TCon t a ps ds u ms cs) + = pure $ TCon t a ps ds u !(traverse (full gam) ms) + !(traverse (full gam) cs) full gam (BySearch c d def) = pure $ BySearch c d !(full gam def) full gam (Guess tm b cs) @@ -595,9 +597,9 @@ HasNames Def where resolvedNamesPat (_ ** (env, lhs, rhs)) = pure $ (_ ** (!(resolved gam env), !(resolved gam lhs), !(resolved gam rhs))) - resolved gam (TCon t a ps ds ms cs) - = pure $ TCon t a ps ds !(traverse (resolved gam) ms) - !(traverse (resolved gam) cs) + resolved gam (TCon t a ps ds u ms cs) + = pure $ TCon t a ps ds u !(traverse (resolved gam) ms) + !(traverse (resolved gam) cs) resolved gam (BySearch c d def) = pure $ BySearch c d !(resolved gam def) resolved gam (Guess tm b cs) @@ -1201,7 +1203,7 @@ getSearchData : {auto c : Ref Ctxt Defs} -> Core SearchData getSearchData fc defaults target = do defs <- get Ctxt - Just (TCon _ _ _ dets _ _) <- lookupDefExact target (gamma defs) + Just (TCon _ _ _ dets u _ _) <- lookupDefExact target (gamma defs) | _ => throw (UndefinedName fc target) let hs = case lookup !(toFullNames target) (typeHints defs) of Just hs => hs @@ -1218,7 +1220,7 @@ getSearchData fc defaults target pure (MkSearchData dets (filter (isCons . snd) [(False, opens), (False, autos), - (False, tyhs), + (not u, tyhs), (True, chasers)])) where isDefault : (Name, Bool) -> Bool @@ -1234,9 +1236,9 @@ setMutWith fc tn tns = do defs <- get Ctxt Just g <- lookupCtxtExact tn (gamma defs) | _ => throw (UndefinedName fc tn) - let TCon t a ps dets _ cons = definition g + let TCon t a ps dets u _ cons = definition g | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setMutWith]")) - updateDef tn (const (Just (TCon t a ps dets tns cons))) + updateDef tn (const (Just (TCon t a ps dets u tns cons))) export addMutData : {auto c : Ref Ctxt Defs} -> @@ -1259,10 +1261,10 @@ setDetermining fc tyn args = do defs <- get Ctxt Just g <- lookupCtxtExact tyn (gamma defs) | _ => throw (UndefinedName fc tyn) - let TCon t a ps _ cons ms = definition g + let TCon t a ps _ u cons ms = definition g | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]")) apos <- getPos 0 args (type g) - updateDef tyn (const (Just (TCon t a ps apos cons ms))) + updateDef tyn (const (Just (TCon t a ps apos u cons ms))) where -- Type isn't normalised, but the argument names refer to those given -- explicitly in the type, so there's no need. @@ -1276,6 +1278,16 @@ setDetermining fc tyn args getPos _ ns ty = throw (GenericMsg fc ("Unknown determining arguments: " ++ showSep ", " (map show ns))) +export +setUniqueSearch : {auto c : Ref Ctxt Defs} -> + FC -> Name -> Bool -> Core () +setUniqueSearch fc tyn u + = do defs <- get Ctxt + Just g <- lookupCtxtExact tyn (gamma defs) + | _ => throw (UndefinedName fc tyn) + let TCon t a ps ds _ cons ms = definition g + | _ => throw (GenericMsg fc (show (fullname g) ++ " is not a type constructor [setDetermining]")) + updateDef tyn (const (Just (TCon t a ps ds u cons ms))) export addHintFor : {auto c : Ref Ctxt Defs} -> @@ -1509,7 +1521,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons) (TCon tag arity (paramPos (Resolved tidx) (map type datacons)) (allDet arity) - [] (map name datacons)) + False [] (map name datacons)) (idx, gam') <- addCtxt tyn tydef (gamma defs) gam'' <- addDataConstructors 0 datacons gam' put Ctxt (record { gamma = gam'' } defs) diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index 22d21ca..515c54a 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -51,7 +51,7 @@ export isEmpty : Defs -> NF vars -> Core Bool isEmpty defs (NTCon fc n t a args) = case !(lookupDefExact n (gamma defs)) of - Just (TCon _ _ _ _ _ cons) + Just (TCon _ _ _ _ _ _ cons) => allM (conflict defs (NTCon fc n t a args)) cons _ => pure False isEmpty defs _ = pure False @@ -66,7 +66,7 @@ freeEnv fc (n :: ns) = PVar RigW Explicit (Erased fc) :: freeEnv fc ns getCons : Defs -> NF vars -> Core (List (NF [], Name, Int, Nat)) getCons defs (NTCon _ tn _ _ _) = case !(lookupDefExact tn (gamma defs)) of - Just (TCon _ _ _ _ _ cons) => + Just (TCon _ _ _ _ _ _ cons) => do cs' <- traverse addTy cons pure (mapMaybe id cs') _ => pure [] diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr index cd6f59e..3abbc99 100644 --- a/src/Core/Reflect.idr +++ b/src/Core/Reflect.idr @@ -21,7 +21,7 @@ getCon : FC -> Defs -> Name -> Core (Term vars) getCon fc defs n = case !(lookupDefExact n (gamma defs)) of Just (DCon t a) => resolved (gamma defs) (Ref fc (DataCon t a) n) - Just (TCon t a _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n) + Just (TCon t a _ _ _ _ _) => resolved (gamma defs) (Ref fc (TyCon t a) n) Just _ => resolved (gamma defs) (Ref fc Func n) _ => throw (UndefinedName fc n) diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 234cb90..e2a8aa0 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -743,9 +743,9 @@ TTC Def where toBuf b (Builtin a) = throw (InternalError "Trying to serialise a Builtin") toBuf b (DCon t arity) = do tag 4; toBuf b t; toBuf b arity - toBuf b (TCon t arity parampos detpos ms datacons) + toBuf b (TCon t arity parampos detpos u ms datacons) = do tag 5; toBuf b t; toBuf b arity; toBuf b parampos - toBuf b detpos; toBuf b ms; toBuf b datacons + toBuf b detpos; toBuf b u; toBuf b ms; toBuf b datacons toBuf b (Hole locs p) = do tag 6; toBuf b locs; toBuf b p toBuf b (BySearch c depth def) @@ -772,8 +772,9 @@ TTC Def where pure (DCon t a) 5 => do t <- fromBuf b; a <- fromBuf b ps <- fromBuf b; dets <- fromBuf b; + u <- fromBuf b ms <- fromBuf b; cs <- fromBuf b - pure (TCon t a ps dets ms cs) + pure (TCon t a ps dets u ms cs) 6 => do l <- fromBuf b p <- fromBuf b pure (Hole l p) diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index d0a12df..234512e 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -492,7 +492,7 @@ posArg : Defs -> List Name -> NF [] -> Core Terminating posArg defs tyns (NTCon _ tc _ _ args) = let testargs : List (Closure []) = case !(lookupDefExact tc (gamma defs)) of - Just (TCon _ _ params _ _ _) => + Just (TCon _ _ params _ _ _ _) => dropParams 0 params args _ => args in if !(anyM (nameIn defs tyns) @@ -548,7 +548,7 @@ calcPositive : {auto c : Ref Ctxt Defs} -> calcPositive loc n = do defs <- get Ctxt case !(lookupDefTyExact n (gamma defs)) of - Just (TCon _ _ _ _ tns dcons, ty) => + Just (TCon _ _ _ _ _ tns dcons, ty) => case !(totRefsIn defs ty) of IsTerminating => do t <- checkData defs (n :: tns) dcons @@ -588,7 +588,7 @@ checkTotal loc n_in case isTerminating tot of Unchecked => case !(lookupDefExact n (gamma defs)) of - Just (TCon _ _ _ _ _ _) + Just (TCon _ _ _ _ _ _ _) => checkPositive loc n _ => checkTerminating loc n t => pure t diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 3df2955..962881e 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -36,8 +36,8 @@ mkIfaceData : {auto c : Ref Ctxt Defs} -> List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl mkIfaceData {vars} fc vis env constraints n conName ps dets meths = let opts = if isNil dets - then [NoHints] - else [NoHints, SearchBy dets] + then [NoHints, UniqueSearch] + else [NoHints, UniqueSearch, SearchBy dets] retty = apply (IVar fc n) (map (IVar fc) (map fst ps)) conty = mkTy Implicit (map jname ps) $ mkTy Explicit (map bhere constraints ++ map bname meths) retty diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 28afb59..2ad65a0 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -836,6 +836,8 @@ dataOpt : Rule DataOpt dataOpt = do exactIdent "noHints" pure NoHints + <|> do exactIdent "uniqueSearch" + pure UniqueSearch <|> do exactIdent "search" ns <- some name pure (SearchBy ns) diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 5223e2c..0c461ae 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -78,7 +78,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp wrapDot : Bool -> EState vars -> ElabMode -> Name -> List RawImp -> Def -> RawImp -> RawImp wrapDot _ _ _ _ _ (DCon _ _) tm = tm - wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _) tm = tm + wrapDot _ _ _ _ _ (TCon _ _ _ _ _ _ _) tm = tm -- Leave primitive applications alone, because they'll be inlined -- before compiling the case tree wrapDot prim est (InLHS _) n' [arg] _ tm diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 3d9b412..95bdfce 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -56,7 +56,7 @@ getNameType rigc env fc x let nt = case definition def of PMDef _ _ _ _ _ => Func DCon t a => DataCon t a - TCon t a _ _ _ _ => TyCon t a + TCon t a _ _ _ _ _ => TyCon t a _ => Func pure (Ref fc nt (Resolved i), gnf env (embed (type def))) where @@ -90,7 +90,7 @@ getVarType rigc nest env fc x let nt = case definition ndef of PMDef _ _ _ _ _ => Func DCon t a => DataCon t a - TCon t a _ _ _ _ => TyCon t a + TCon t a _ _ _ _ _ => TyCon t a _ => Func tm = tmf fc nt tyenv = useVars (getArgs tm) diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index d4c44a2..596ac55 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -37,7 +37,7 @@ toRHS loc (Constr con args) findConName : Defs -> Name -> Core (Maybe Name) findConName defs tyn = case !(lookupDefExact tyn (gamma defs)) of - Just (TCon _ _ _ _ _ [con]) => pure (Just con) + Just (TCon _ _ _ _ _ _ [con]) => pure (Just con) _ => pure Nothing findFields : Defs -> Name -> Core (Maybe (List (String, Maybe Name))) diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index 45aaac0..608e593 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -92,7 +92,7 @@ findCons n lhs Nothing => pure (SplitFail (CantSplitThis n ("Can't find type of " ++ show n ++ " in LHS"))) Just tyn => - do Just (TCon _ _ _ _ _ cons) <- + do Just (TCon _ _ _ _ _ _ cons) <- lookupDefExact tyn (gamma defs) | res => pure (SplitFail (CantSplitThis n diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 685cb7f..21ae8fd 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -114,7 +114,7 @@ searchName fc rigc opts env target topty defining (n, ndef) let namety : NameType = case definition ndef of DCon tag arity => DataCon tag arity - TCon tag arity _ _ _ _ => TyCon tag arity + TCon tag arity _ _ _ _ _ => TyCon tag arity _ => Func log 5 $ "Trying " ++ show (fullname ndef) nty <- nf defs env (embed ty) diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index fdeaa34..3fe1e93 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -524,6 +524,8 @@ dataOpt : Rule DataOpt dataOpt = do exactIdent "noHints" pure NoHints + <|> do exactIdent "uniqueSearch" + pure UniqueSearch <|> do exactIdent "search" ns <- some name pure (SearchBy ns) diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 77a1522..08ee751 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -23,6 +23,8 @@ processDataOpt fc n NoHints = pure () processDataOpt fc ndef (SearchBy dets) = setDetermining fc ndef dets +processDataOpt fc ndef UniqueSearch + = setUniqueSearch fc ndef True checkRetType : {auto c : Ref Ctxt Defs} -> Env Term vars -> NF vars -> @@ -121,7 +123,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw) -- Add the type constructor as a placeholder tidx <- addDef n (newDef fc n Rig1 vars fullty vis - (TCon 0 arity [] [] [] [])) + (TCon 0 arity [] [] False [] [])) addMutData (Resolved tidx) defs <- get Ctxt traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs) @@ -158,7 +160,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra Nothing => pure [] Just ndef => case definition ndef of - TCon _ _ _ _ mw _ => + TCon _ _ _ _ _ mw _ => do ok <- convert defs [] fullty (type ndef) if ok then pure mw else do logTermNF 1 "Previous" [] (type ndef) @@ -174,7 +176,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra -- Add the type constructor as a placeholder while checking -- data constructors tidx <- addDef n (newDef fc n Rig1 vars fullty vis - (TCon 0 arity [] [] [] [])) + (TCon 0 arity [] [] False [] [])) case vis of Private => pure () _ => do addHash n diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index 0c5fd4c..bf9c078 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -252,6 +252,8 @@ mutual pure (SearchBy x') reify defs (NDCon _ (NS _ (UN "NoHints")) _ _ _) = pure NoHints + reify defs (NDCon _ (NS _ (UN "UniqueSearch")) _ _ _) + = pure UniqueSearch reify defs val = cantReify val "DataOpt" export @@ -549,6 +551,7 @@ mutual = do x' <- reflect fc defs env x appCon fc defs (reflectionttimp "SearchBy") [x'] reflect fc defs env NoHints = getCon fc defs (reflectionttimp "NoHints") + reflect fc defs env UniqueSearch = getCon fc defs (reflectionttimp "UniqueSearch") export Reflect ImpData where diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 67a9e05..1d4539c 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -221,11 +221,13 @@ mutual data DataOpt : Type where SearchBy : List Name -> DataOpt -- determining arguments NoHints : DataOpt -- Don't generate search hints for constructors + UniqueSearch : DataOpt -- auto implicit search must check result is unique export Eq DataOpt where (==) (SearchBy xs) (SearchBy ys) = xs == ys (==) NoHints NoHints = True + (==) UniqueSearch UniqueSearch = True (==) _ _ = False public export @@ -794,12 +796,14 @@ mutual toBuf b (SearchBy ns) = do tag 0; toBuf b ns toBuf b NoHints = tag 1 + toBuf b UniqueSearch = tag 2 fromBuf b = case !getTag of 0 => do ns <- fromBuf b pure (SearchBy ns) 1 => pure NoHints + 2 => pure UniqueSearch _ => corrupt "DataOpt" export diff --git a/tests/Main.idr b/tests/Main.idr index 5c415be..00890f6 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -44,7 +44,7 @@ idrisTests "linear001", "linear002", "linear003", "linear004", "linear005", "linear006", "linear007", "params001", - "perf001", "perf002", + "perf001", "perf002", "perf003", "perror001", "perror002", "perror003", "perror004", "perror005", "perror006", "pkg001", diff --git a/tests/idris2/perf003/Auto.idr b/tests/idris2/perf003/Auto.idr new file mode 100644 index 0000000..bc61cc2 --- /dev/null +++ b/tests/idris2/perf003/Auto.idr @@ -0,0 +1,18 @@ +public export +data Phase = Gas | Liquid | Solid + +public export +data ChangePhase : Phase -> Phase -> Type where + Sequence : ChangePhase a b -> ChangePhase b c -> ChangePhase a c + Condense : ChangePhase Gas Liquid + Freeze : ChangePhase Liquid Solid + Melt : ChangePhase Solid Liquid + Vaporize : ChangePhase Liquid Gas + Sublimate : ChangePhase Solid Gas + +public export +inferred : { auto transition : ChangePhase l r } -> ChangePhase l r +inferred { transition } = transition + +test : ChangePhase Gas Solid +test = inferred diff --git a/tests/idris2/perf003/expected b/tests/idris2/perf003/expected new file mode 100644 index 0000000..31cf9a2 --- /dev/null +++ b/tests/idris2/perf003/expected @@ -0,0 +1 @@ +1/1: Building Auto (Auto.idr) diff --git a/tests/idris2/perf003/run b/tests/idris2/perf003/run new file mode 100755 index 0000000..3318fdd --- /dev/null +++ b/tests/idris2/perf003/run @@ -0,0 +1,3 @@ +$1 --check Auto.idr + +rm -rf build