Merge pull request #1273 from edwinb/nfthreshold

Add heuristic for when to normalise metavars

Makefile

@@ -82,7 +82,7 @@ test-lib: contrib
 
 libs : prelude base contrib network test-lib
 
-testbin: test-lib install
+testbin: test-lib
 	@${MAKE} -C tests testbin IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 
 test: testbin

src/Core/Context.idr

@@ -2210,6 +2210,13 @@ setAutoImplicitLimit max
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->autoImplicitLimit = max } defs)
 
+export
+setNFThreshold : {auto c : Ref Ctxt Defs} ->
+                 Nat -> Core ()
+setNFThreshold max
+    = do defs <- get Ctxt
+         put Ctxt (record { options->elabDirectives->nfThreshold = max } defs)
+
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
                Core Bool

src/Core/Options.idr

@@ -126,6 +126,7 @@ record ElabDirectives where
   totality : TotalReq
   ambigLimit : Nat
   autoImplicitLimit : Nat
+  nfThreshold : Nat
   --
   -- produce traditional (prefix) record projections,
   -- in addition to postfix (dot) projections
@@ -201,7 +202,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 50 True
 
 export
 defaults : Options

src/Core/Unify.idr

@@ -7,6 +7,7 @@ import Core.Core
 import Core.Env
 import Core.GetType
 import Core.Normalise
+import Core.Options
 import Core.TT
 import public Core.UnifyState
 import Core.Value
@@ -626,6 +627,31 @@ isDefInvertible fc i
               | Nothing => throw (UndefinedName fc (Resolved i))
          pure (invertible gdef)
 
+tooBig : (counting : Bool) -> Nat -> List (Term vars) -> Term vars -> Bool
+tooBig _ Z _ _ = True
+tooBig c k stk (App _ f a)
+    = tooBig c k (a :: stk) f
+tooBig c (S k) stk (Bind _ _ _ sc)
+    = tooBig c (S k) [] sc || any (tooBig c k []) stk
+tooBig c (S k) stk (Meta _ _ _ as)
+    = any (tooBig c k []) as || any (tooBig c k []) stk
+tooBig c (S k) stk f
+    = if c || isFn f -- start counting, we're under a function
+         then tooBigArgs True k stk
+         else tooBigArgs c (S k) stk
+  where
+    isFn : Term vs -> Bool
+    isFn (Ref _ Func _) = True
+    isFn _ = False -- Don't count if it's not a function, because normalising
+                   -- won't help
+
+    tooBigArgs : Bool -> Nat -> List (Term vars) -> Bool
+    tooBigArgs c Z _ = True
+    tooBigArgs c k [] = False
+    tooBigArgs c (S k) (a :: as)
+       = tooBig c (if c then k else S k) [] a || tooBigArgs c k as
+tooBig _ _ _ _ = False
+
 mutual
   unifyIfEq : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
@@ -865,7 +891,12 @@ mutual
                          | _ => postponeS True swap loc mode "Delayed hole" env
                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
                                           tmnf
-                     tm <- quote empty env tmnf
+                     tmq <- quote empty env tmnf
+                     tm <- if tooBig False
+                                     defs.options.elabDirectives.nfThreshold
+                                     [] tmq
+                              then quote defs env tmnf
+                              else pure tmq
                      Just tm <- occursCheck loc env mode mname tm
                          | _ => postponeS True swap loc mode "Occurs check failed" env
                                           (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')
@@ -876,7 +907,7 @@ mutual
                                                 margs margs' locs submv
                                                 tm stm tmnf
                           Nothing =>
-                            do tm' <- normalise defs env tm
+                            do tm' <- quote defs env tmnf
                                case shrinkTerm tm' submv of
                                     Nothing => postponeS True swap loc mode "Can't shrink" env
                                                (NApp loc (NMeta mname mref margs) $ map (EmptyFC,) margs')

src/Idris/Desugar.idr

@@ -978,6 +978,7 @@ mutual
                pure [IPragma [] (\nest, env => setPrefixRecordProjections b)]
              AmbigDepth n => pure [IPragma [] (\nest, env => setAmbigLimit n)]
              AutoImplicitDepth n => pure [IPragma [] (\nest, env => setAutoImplicitLimit n)]
+             NFMetavarThreshold n => pure [IPragma [] (\nest, env => setNFThreshold n)]
              PairNames ty f s => pure [IPragma [] (\nest, env => setPair fc ty f s)]
              RewriteName eq rw => pure [IPragma [] (\nest, env => setRewrite fc eq rw)]
              PrimInteger n => pure [IPragma [] (\nest, env => setFromInteger n)]

src/Idris/Parser.idr

@@ -1058,6 +1058,10 @@ directive fname indents
          dpt <- intLit
          atEnd indents
          pure (AutoImplicitDepth (fromInteger dpt))
+  <|> do pragma "nf_metavar_threshold"
+         dpt <- intLit
+         atEnd indents
+         pure (NFMetavarThreshold (fromInteger dpt))
   <|> do pragma "pair"
          ty <- name
          f <- name

src/Idris/Syntax.idr

@@ -253,6 +253,7 @@ mutual
        DefaultTotality : TotalReq -> Directive
        PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
+       NFMetavarThreshold : Nat -> Directive
 
   public export
   data PField : Type where