diff --git a/CHANGELOG.md b/CHANGELOG.md index 6cfcb3eb2..236908d08 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -44,10 +44,6 @@ * `getChar` is now supported on Node.js and `putChar` is supported on both JavaScript backends. * Integer-indexed arrays are now supported. -#### Optimizations - -* Unit types can now be erased by the optimiser in data types. - ### Compiler changes * If `IAlternative` expression with `FirstSuccess` rule fails to typecheck, diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index d9fc0a056..46e74a7fd 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -29,7 +29,7 @@ import public Libraries.Utils.Binary ||| version number if you're changing the version more than once in the same day. export ttcVersion : Int -ttcVersion = 20230705 * 100 + 0 +ttcVersion = 20230331 * 100 + 0 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr index cf7b57b2b..b07c92098 100644 --- a/src/TTImp/Elab/Utils.idr +++ b/src/TTImp/Elab/Utils.idr @@ -1,7 +1,6 @@ module TTImp.Elab.Utils import Core.Case.CaseTree -import Core.CompileExpr import Core.Context import Core.Core import Core.Env @@ -33,23 +32,6 @@ detagSafe defs (NTCon _ n _ _ args) = elem i ns || notErased (i + 1) ns rest detagSafe defs _ = pure False -||| Check if the name at the head of a given Term is a unit type. -||| This does not evaluate the term, so can return false negatives, -||| if the unit type is not in the Term directly. -export -isUnitType : - {auto _ : Ref Ctxt Defs} -> - Term vs -> - Core Bool -isUnitType (Ref fc (TyCon {}) n) = do - defs <- get Ctxt - Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n $ gamma defs - | _ => pure False - hasFlag (virtualiseFC fc) con (ConType UNIT) -isUnitType (App _ f _) = isUnitType f -isUnitType (Bind fc x (Let {}) rhs) = isUnitType rhs -isUnitType _ = pure False - findErasedFrom : {auto c : Ref Ctxt Defs} -> Defs -> Nat -> NF [] -> Core (List Nat, List Nat) findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf) @@ -60,9 +42,9 @@ findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf) (erest, dtrest) <- findErasedFrom defs (1 + pos) sc let dt' = if !(detagSafe defs !(evalClosure defs aty)) then (pos :: dtrest) else dtrest - if isErased c || !(isUnitType !(quote defs [] aty)) - then pure (pos :: erest, dt') - else pure (erest, dt') + pure $ if isErased c + then (pos :: erest, dt') + else (erest, dt') findErasedFrom defs pos tm = pure ([], []) -- Find the argument positions in the given type which are guaranteed to be diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index afb176e7e..f4d11791e 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -210,25 +210,25 @@ getDetags fc tys getRelevantArg : {auto c : Ref Ctxt Defs} -> Defs -> Nat -> Maybe Nat -> Bool -> NF [] -> Core (Maybe (Bool, Nat)) -getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc) = - if isErased rig || !(isUnitType !(quote defs [] val)) - then getRelevantArg defs (1 + i) rel world - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) - else case !(evalClosure defs val) of - -- %World is never inspected, so might as well be deleted from data types, - -- although it needs care when compiling to ensure that the function that - -- returns the IO/%World type isn't erased - (NPrimVal _ $ PrT WorldType) => - getRelevantArg defs (1 + i) rel False - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) - _ => - -- if we haven't found a relevant argument yet, make - -- a note of this one and keep going. Otherwise, we - -- have more than one, so give up. - maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) - getRelevantArg defs (1 + i) (Just i) False sc') - (const (pure Nothing)) - rel +getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc) + = branchZero (getRelevantArg defs (1 + i) rel world + !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))) + (case !(evalClosure defs val) of + -- %World is never inspected, so might as well be deleted from data types, + -- although it needs care when compiling to ensure that the function that + -- returns the IO/%World type isn't erased + (NPrimVal _ $ PrT WorldType) => + getRelevantArg defs (1 + i) rel False + !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + _ => + -- if we haven't found a relevant argument yet, make + -- a note of this one and keep going. Otherwise, we + -- have more than one, so give up. + maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + getRelevantArg defs (1 + i) (Just i) False sc') + (const (pure Nothing)) + rel) + rig getRelevantArg defs i rel world tm = pure ((world,) <$> rel) @@ -247,29 +247,25 @@ findNewtype [con] _ => Nothing findNewtype _ = pure () -hasArgs : {auto _ : Ref Ctxt Defs} -> Nat -> Term vs -> Core Bool -hasArgs (S k) (Bind _ _ (Pi _ c _ ty) sc) - = if isErased c || !(isUnitType ty) - then hasArgs (S k) sc - else hasArgs k sc -hasArgs (S k) _ = pure False -hasArgs Z (Bind _ _ (Pi _ c _ ty) sc) - = if isErased c || !(isUnitType ty) - then hasArgs Z sc - else pure False -hasArgs Z _ = pure True +hasArgs : Nat -> Term vs -> Bool +hasArgs (S k) (Bind _ _ (Pi _ c _ _) sc) + = if isErased c + then hasArgs (S k) sc + else hasArgs k sc +hasArgs (S k) _ = False +hasArgs Z (Bind _ _ (Pi _ c _ _) sc) + = if isErased c + then hasArgs Z sc + else False +hasArgs Z _ = True -- get the first non-erased argument -firstArg : - Ref Ctxt Defs => - {vs : _} -> - Term vs -> - Core (Maybe (Exists Term)) +firstArg : Term vs -> Maybe (Exists Term) firstArg (Bind _ _ (Pi _ c _ val) sc) - = if isErased c || !(isUnitType val) + = if isErased c then firstArg sc - else pure $ Just $ Evidence _ val -firstArg tm = pure Nothing + else Just $ Evidence _ val +firstArg tm = Nothing typeCon : Term vs -> Maybe Name typeCon (Ref _ (TyCon _ _) n) = Just n @@ -277,12 +273,12 @@ typeCon (App _ fn _) = typeCon fn typeCon _ = Nothing shaped : {auto c : Ref Ctxt Defs} -> - (forall vs. Term vs -> Core Bool) -> + (forall vs . Term vs -> Bool) -> List Constructor -> Core (Maybe Name) shaped as [] = pure Nothing shaped as (c :: cs) = do defs <- get Ctxt - if !(as !(normalise defs [] (type c))) + if as !(normalise defs [] (type c)) then pure (Just (name c)) else shaped as cs @@ -335,7 +331,7 @@ calcEnum fc cs isNullary : Constructor -> Core Bool isNullary c = do defs <- get Ctxt - hasArgs 0 !(normalise defs [] (type c)) + pure $ hasArgs 0 !(normalise defs [] (type c)) calcRecord : {auto c : Ref Ctxt Defs} -> FC -> List Constructor -> Core Bool @@ -356,7 +352,7 @@ calcNaty fc tyCon cs@[_, _] | Nothing => pure False let Just succCon = find (\con => name con == succ) cs | Nothing => pure False - Just (Evidence _ succArgTy) <- firstArg (type succCon) + let Just (Evidence _ succArgTy) = firstArg (type succCon) | Nothing => pure False let Just succArgCon = typeCon succArgTy | Nothing => pure False