idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 00:55:00 +03:00
Code Issues Projects Releases Wiki Activity

[ debug ] better eval logging

Browse Source
This commit is contained in:
Guillaume Allais 2022-06-09 12:39:47 +01:00 committed by G. Allais
parent 268a3520f3
commit 128099fd47
4 changed files with 105 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

52
src/Core/Normalise/Eval.idr
View File

@ -12,6 +12,7 @@ import Core.Value
import Data.List
import Data.Maybe
import Data.Nat
import Data.String
import Data.Vect
%default covering
@ -271,8 +272,8 @@ parameters (defs : Defs, topopts : EvalOpts)
-- pure $ "Found bound variable: " ++ show fn'
pure def
evalRef env meta fc nt@Func n stk def
= do -- logC "eval.ref.func" 50 $ do n' <- toFullNames n
-- pure $ "Found function: " ++ show n'
= do -- logC "eval.ref" 50 $ do n' <- toFullNames n
-- pure $ "Found function: " ++ show n'
Just res <- lookupCtxtExact n (gamma defs)
| Nothing => pure def
let redok1 = evalAll topopts
@ -286,14 +287,18 @@ parameters (defs : Defs, topopts : EvalOpts)
-- when evaluating something recursive, so this is a
-- good place to check
unless redok2 $ logC "eval.stuck" 5 $ do n' <- toFullNames n
pure $ "Stuck function: " ++ show n'
pure $ "Stuck function: \{show n'}"
if redok
then do
Just opts' <- updateLimit nt n topopts
| Nothing => do log "eval.stuck" 10 $ "Function " ++ show n ++ " past reduction limit"
| Nothing => do log "eval.stuck" 10 $ "Function \{show n} past reduction limit"
pure def -- name is past reduction limit
evalDef env opts' meta fc
nf <- evalDef env opts' meta fc
(multiplicity res) (definition res) (flags res) stk def
-- logC "eval.ref" 50 $ do n' <- toFullNames n
-- nf <- toFullNames nf
-- pure "Reduced \{show n'} to \{show nf}"
pure nf
else pure def
getCaseBound : List (Closure free) ->
@ -387,8 +392,10 @@ parameters (defs : Defs, topopts : EvalOpts)
= do Result val <- tryAlt env loc opts fc stk val x
| NoMatch => findAlt env loc opts fc stk val xs
| GotStuck => do
logC "eval.casetree.stuck" 5 $
pure $ "Got stuck matching " ++ show val ++ " against " ++ show !(toFullNames x)
logC "eval.casetree.stuck" 5 $ do
val <- toFullNames val
x <- toFullNames x
pure $ "Got stuck matching \{show val} against \{show x}"
pure GotStuck
pure (Result val)
@ -401,7 +408,9 @@ parameters (defs : Defs, topopts : EvalOpts)
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
-- we have not defined quote yet (it depends on eval itself) so we show the NF
-- i.e. only the top-level constructor.
log "eval.casetree" 5 $ "Evaluated " ++ show name ++ " to " ++ show xval
logC "eval.casetree" 5 $ do
xval <- toFullNames xval
pure "Evaluated \{show name} to \{show xval}"
let loc' = updateLocal opts env idx (varExtend x) loc xval
findAlt env loc' opts fc stk xval alts
evalTree env loc opts fc stk (STerm _ tm)
@ -483,17 +492,36 @@ parameters (defs : Defs, topopts : EvalOpts)
|| (meta && holesOnly opts)
|| (tcInline opts && elem TCInline flags)
then case argsFromStack args stk of
Nothing => pure def
Nothing => do logC "eval.def.underapplied" 50 $ do
def <- toFullNames def
pure "Cannot reduce under-applied \{show def}"
pure def
Just (locs', stk') =>
do Result res <- evalTree env locs' opts fc stk' tree
| _ => pure def
| _ => do logC "eval.def.stuck" 50 $ do
def <- toFullNames def
pure "evalTree failed on \{show def}"
pure def
pure res
else pure def
else do -- logC "eval.def.stuck" 50 $ do
-- def <- toFullNames def
-- pure $ unlines [ "Refusing to reduce \{show def}:"
-- , " holesOnly : \{show $ holesOnly opts}"
-- , " argHolesOnly: \{show $ argHolesOnly opts}"
-- , " tcInline : \{show $ tcInline opts}"
-- , " meta : \{show meta}"
-- , " rigd : \{show rigd}"
-- ]
pure def
evalDef env opts meta fc rigd (Builtin op) flags stk def
= evalOp (getOp op) stk def
-- All other cases, use the default value, which is already applied to
-- the stack
evalDef env opts _ _ _ _ _ stk def = pure def
evalDef env opts meta fc rigd def flags stk orig = do
logC "eval.def.stuck" 50 $ do
orig <- toFullNames orig
pure "Cannot reduce def \{show orig}: it is a \{show def}"
pure orig
-- Make sure implicit argument order is right... 'vars' is used so we'll
-- write it explicitly, but it does appear after the parameters in 'eval'!

3
src/Core/Options/Log.idr
View File

@ -115,7 +115,10 @@ knownTopics = [
("elab.with", Nothing),
("eval.casetree", Nothing),
("eval.casetree.stuck", Nothing),
("eval.def.underapplied", Just "Evaluating definitions (unavailable by default, edit Core.Normalise.Eval & recompile)"),
("eval.def.stuck", Just "Evaluating definitions (unavailable by default, edit Core.Normalise.Eval & recompile)"),
("eval.eta", Nothing),
("eval.ref", Just "Evaluating refs (unavailable by default, edit Core.Normalise.Eval & recompile)"),
("eval.stuck", Nothing),
("ide-mode.completion", Just "Autocompletion requests"),
("ide-mode.hole", Just "Displaying hole contexts"),

22
src/Core/TT.idr
View File

@ -28,6 +28,8 @@ data NameType : Type where
DataCon : (tag : Int) -> (arity : Nat) -> NameType
TyCon : (tag : Int) -> (arity : Nat) -> NameType
%name NameType nt
export
covering
Show NameType where
@ -49,6 +51,8 @@ record KindedName where
fullName : Name -- fully qualified name
rawName : Name
%name KindedName kn
export
defaultKindedName : Name -> KindedName
defaultKindedName nm = MkKindedName Nothing nm nm
@ -83,6 +87,8 @@ data PrimType
| DoubleType
| WorldType
%name PrimType pty
public export
data Constant
= I Int
@ -101,6 +107,8 @@ data Constant
| PrT PrimType
| WorldVal
%name Constant cst
export
isConstantType : Name -> Maybe PrimType
isConstantType (UN (Basic n)) = case n of
@ -304,6 +312,8 @@ primTypeTag Int64Type = 16
public export
data Precision = P Int | Unlimited
%name Precision prec
export
Eq Precision where
(P m) == (P n) = m == n
@ -389,6 +399,8 @@ data PrimFn : Nat -> Type where
BelieveMe : PrimFn 3
Crash : PrimFn 2
%name PrimFn f
export
Show (PrimFn arity) where
show (Add ty) = "+" ++ show ty
@ -477,6 +489,8 @@ prettyOp op@Crash [v1,v2] = annotate (Fun $ UN $ Basic $ show op) "crash" <++> v
public export
data PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t
%name PiInfo pinfo
namespace PiInfo
export
@ -535,6 +549,8 @@ data Binder : Type -> Type where
-- the type of pattern bound variables
PVTy : FC -> RigCount -> (ty : type) -> Binder type
%name Binder bd
export
isLet : Binder t -> Bool
isLet (Let _ _ _ _) = True
@ -659,6 +675,8 @@ data IsVar : Name -> Nat -> List Name -> Type where
First : IsVar n Z (n :: ns)
Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
%name IsVar idx
export
dropLater : IsVar nm (S idx) (v :: vs) -> IsVar nm idx vs
dropLater (Later p) = p
@ -814,11 +832,15 @@ namespace CList
public export
data LazyReason = LInf | LLazy | LUnknown
%name LazyReason lz
-- For as patterns matching linear arguments, select which side is
-- consumed
public export
data UseSide = UseLeft | UseRight
%name UseSide side
public export
data Term : List Name -> Type where
Local : FC -> (isLet : Maybe Bool) ->

40
src/Core/Value.idr
View File

@ -78,6 +78,7 @@ mutual
NRef : NameType -> Name -> NHead vars
NMeta : Name -> Int -> List (Closure vars) -> NHead vars
-- Values themselves. 'Closure' is an unevaluated thunk, which means
-- we can wait until necessary to reduce constructor arguments
public export
@ -100,6 +101,11 @@ mutual
NErased : FC -> (imp : Bool) -> NF vars
NType : FC -> Name -> NF vars
%name LocalEnv lenv
%name Closure cl
%name NHead hd
%name NF nf
export
ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars
-- Part of the machinery for matching on types - I believe this won't affect
@ -133,6 +139,40 @@ export
Show (Closure free) where
show _ = "[closure]"
export
HasNames (NHead free) where
full defs (NRef nt n) = NRef nt <$> full defs n
full defs hd = pure hd
resolved defs (NRef nt n) = NRef nt <$> resolved defs n
resolved defs hd = pure hd
export
HasNames (NF free) where
full defs (NBind fc x bd f) = pure $ NBind fc x bd f
full defs (NApp fc hd xs) = pure $ NApp fc !(full defs hd) xs
full defs (NDCon fc n tag arity xs) = pure $ NDCon fc !(full defs n) tag arity xs
full defs (NTCon fc n tag arity xs) = pure $ NTCon fc !(full defs n) tag arity xs
full defs (NAs fc side nf nf1) = pure $ NAs fc side !(full defs nf) !(full defs nf1)
full defs (NDelayed fc lz nf) = pure $ NDelayed fc lz !(full defs nf)
full defs (NDelay fc lz cl cl1) = pure $ NDelay fc lz cl cl1
full defs (NForce fc lz nf xs) = pure $ NForce fc lz !(full defs nf) xs
full defs (NPrimVal fc cst) = pure $ NPrimVal fc cst
full defs (NErased fc imp) = pure $ NErased fc imp
full defs (NType fc n) = pure $ NType fc !(full defs n)
resolved defs (NBind fc x bd f) = pure $ NBind fc x bd f
resolved defs (NApp fc hd xs) = pure $ NApp fc !(resolved defs hd) xs
resolved defs (NDCon fc n tag arity xs) = pure $ NDCon fc !(resolved defs n) tag arity xs
resolved defs (NTCon fc n tag arity xs) = pure $ NTCon fc !(resolved defs n) tag arity xs
resolved defs (NAs fc side nf nf1) = pure $ NAs fc side !(resolved defs nf) !(resolved defs nf1)
resolved defs (NDelayed fc lz nf) = pure $ NDelayed fc lz !(resolved defs nf)
resolved defs (NDelay fc lz cl cl1) = pure $ NDelay fc lz cl cl1
resolved defs (NForce fc lz nf xs) = pure $ NForce fc lz !(resolved defs nf) xs
resolved defs (NPrimVal fc cst) = pure $ NPrimVal fc cst
resolved defs (NErased fc imp) = pure $ NErased fc imp
resolved defs (NType fc n) = pure $ NType fc !(resolved defs n)
export
covering
{free : _} -> Show (NF free) where