From 677acf0d841285395758361f74bf904c8853f40b Mon Sep 17 00:00:00 2001 From: Zoe Stafford <36511192+Z-snails@users.noreply.github.com> Date: Wed, 5 Jul 2023 19:51:34 +0100 Subject: [PATCH] Treat unit types as erased in constructors (#3002) * Treat unit types as erased in constructors * Cleanup + dump ttc version * Update CHANGELOG.md --- CHANGELOG.md | 4 ++ src/Core/Binary.idr | 2 +- src/TTImp/Elab/Utils.idr | 24 ++++++++++-- src/TTImp/ProcessData.idr | 80 ++++++++++++++++++++------------------- 4 files changed, 68 insertions(+), 42 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 236908d08..6cfcb3eb2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -44,6 +44,10 @@ * `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 46e74a7fd..d9fc0a056 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 = 20230331 * 100 + 0 +ttcVersion = 20230705 * 100 + 0 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr index b07c92098..cf7b57b2b 100644 --- a/src/TTImp/Elab/Utils.idr +++ b/src/TTImp/Elab/Utils.idr @@ -1,6 +1,7 @@ module TTImp.Elab.Utils import Core.Case.CaseTree +import Core.CompileExpr import Core.Context import Core.Core import Core.Env @@ -32,6 +33,23 @@ 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) @@ -42,9 +60,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 - pure $ if isErased c - then (pos :: erest, dt') - else (erest, dt') + if isErased c || !(isUnitType !(quote defs [] aty)) + then pure (pos :: erest, dt') + else pure (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 f4d11791e..afb176e7e 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) - = 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 (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 tm = pure ((world,) <$> rel) @@ -247,25 +247,29 @@ findNewtype [con] _ => Nothing findNewtype _ = pure () -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 +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 -- get the first non-erased argument -firstArg : Term vs -> Maybe (Exists Term) +firstArg : + Ref Ctxt Defs => + {vs : _} -> + Term vs -> + Core (Maybe (Exists Term)) firstArg (Bind _ _ (Pi _ c _ val) sc) - = if isErased c + = if isErased c || !(isUnitType val) then firstArg sc - else Just $ Evidence _ val -firstArg tm = Nothing + else pure $ Just $ Evidence _ val +firstArg tm = pure Nothing typeCon : Term vs -> Maybe Name typeCon (Ref _ (TyCon _ _) n) = Just n @@ -273,12 +277,12 @@ typeCon (App _ fn _) = typeCon fn typeCon _ = Nothing shaped : {auto c : Ref Ctxt Defs} -> - (forall vs . Term vs -> Bool) -> + (forall vs. Term vs -> Core 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 @@ -331,7 +335,7 @@ calcEnum fc cs isNullary : Constructor -> Core Bool isNullary c = do defs <- get Ctxt - pure $ hasArgs 0 !(normalise defs [] (type c)) + hasArgs 0 !(normalise defs [] (type c)) calcRecord : {auto c : Ref Ctxt Defs} -> FC -> List Constructor -> Core Bool @@ -352,7 +356,7 @@ calcNaty fc tyCon cs@[_, _] | Nothing => pure False let Just succCon = find (\con => name con == succ) cs | Nothing => pure False - let Just (Evidence _ succArgTy) = firstArg (type succCon) + Just (Evidence _ succArgTy) <- firstArg (type succCon) | Nothing => pure False let Just succArgCon = typeCon succArgTy | Nothing => pure False