wip

src/Elaboration.hs-boot

@@ -1,12 +1,8 @@
 module Elaboration where
 
-import Protolude
-
-import Data.HashSet (HashSet)
-import Prettyprinter (Doc)
-
 import qualified Core.Domain as Domain
 import qualified Core.Syntax as Syntax
+import Data.HashSet (HashSet)
 import Elaboration.Context (Context)
 import Literal (Literal)
 import qualified Meta
@@ -15,26 +11,24 @@ import Name (Name)
 import qualified Name
 import Plicity
 import qualified Postponement
+import Prettyprinter (Doc)
+import Protolude
 import qualified Surface.Syntax as Surface
 
 check
   :: Context v
   -> Surface.Term
   -> Domain.Type
   -> M (Syntax.Term v)
-
 inferLiteral :: Literal -> Domain.Type
-
 evaluate
   :: Context v
   -> Syntax.Term v
   -> M Domain.Value
-
 readback
   :: Context v
   -> Domain.Value
   -> M (Syntax.Term v)
-
 getExpectedTypeName
   :: Context v
   -> Domain.Type
@@ -50,7 +44,6 @@ resolveConstructor
   -> HashSet Name.Qualified
   -> M (Maybe (Either Meta.Index Name.Qualified))
   -> M (Either Meta.Index ResolvedConstructor)
-
 inferenceFailed
   :: Context v
   -> M (Syntax.Term v, Domain.Type)
@@ -65,9 +58,7 @@ insertMetas
   -> InsertUntil
   -> Domain.Type
   -> M ([(Plicity, Domain.Value)], Domain.Type)
-
 prettyValue :: Context v -> Domain.Value -> M (Doc ann)
-
 postpone
   :: Context v
   -> Domain.Type

src/Elaboration/Context.hs

@@ -680,14 +680,21 @@ forceNeutral context head_ spine
             pure Nothing
       _ -> pure Nothing
 
-isStuck :: Domain.Value -> Bool
-isStuck headApp = case headApp of
-  Domain.AnyNeutral _ (Domain.Apps _) -> False
-  Domain.Con {} -> False
-  Domain.Lit {} -> False
-  Domain.Pi {} -> False
-  Domain.Fun {} -> False
-  _ -> True
+unstuck :: Context v -> Domain.Value -> M (Maybe Domain.Value)
+unstuck context headApp = do
+  headApp' <- forceHeadGlue context headApp
+  case headApp' of
+    Domain.AnyNeutral _ (Domain.Apps _) -> pure $ Just headApp'
+    Domain.Glued _ (Domain.Apps _) _ -> pure $ Just headApp'
+    Domain.Glued _ _ value -> unstuck context value
+    Domain.Con {} -> pure $ Just headApp'
+    Domain.Lit {} -> pure $ Just headApp'
+    Domain.Pi {} -> pure $ Just headApp'
+    Domain.Fun {} -> pure $ Just headApp'
+    _ -> do
+      -- putText "unstuck.stuck:"
+      -- dumpValue context headApp'
+      pure Nothing
 
 -- | Evaluate the head of a value further, if (now) possible due to meta
 -- solutions or new value bindings. Also evaluates through glued values.
@@ -699,11 +706,12 @@ forceHead context value =
   case value of
     Domain.Neutral head_ spine -> neutral head_ spine
     Domain.Stuck head_ args headApp spine -> do
-      headApp' <- forceHead context headApp
-      if isStuck headApp'
-        then neutral head_ $ Domain.Apps args <> spine
-        else do
-          value' <- Evaluation.applySpine headApp' spine
+      maybeUnstuck <- unstuck context headApp
+      case maybeUnstuck of
+        Nothing ->
+          neutral head_ $ Domain.Apps args <> spine
+        Just unstuckValue -> do
+          value' <- Evaluation.applySpine unstuckValue spine
           forceHead context value'
     Domain.Glued _ _ value' ->
       forceHead context value'
@@ -732,12 +740,14 @@ forceHeadGlue context value =
   case value of
     Domain.Neutral head_ spine -> neutral head_ spine
     Domain.Stuck head_ args headApp spine -> do
-      headApp' <- forceHead context headApp
-      if isStuck headApp'
-        then neutral head_ $ Domain.Apps args <> spine
-        else do
-          value' <- Evaluation.applySpine headApp' spine
-          forceHeadGlue context value'
+      let spine' = Domain.Apps args <> spine
+      maybeUnstuck <- unstuck context headApp
+      case maybeUnstuck of
+        Nothing ->
+          neutral head_ spine'
+        Just unstuckValue -> do
+          lazyValue <- lazy $ Evaluation.applySpine unstuckValue spine
+          pure $ Domain.Glued head_ spine' $ Domain.Lazy lazyValue
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHeadGlue context value'

src/Elaboration/Unification.hs-boot

@@ -1,8 +1,8 @@
 module Elaboration.Unification where
 
-import  Elaboration.Context.Type
+import qualified Core.Domain as Domain
+import Elaboration.Context.Type
 import Monad
 import Protolude
-import qualified Core.Domain as Domain
 
 equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool

tests/singles/type-checking/array-append.vix

@@ -17,23 +17,23 @@ append_vector : forall m n A. Vector m A -> Vector n A -> Vector (add m n) A
 append_vector Nil ys = ys
 append_vector (Cons x xs) ys = Cons x (append_vector xs ys)
 
-data Array A where
-  Array : forall n. Vector n A -> Array A
-
-append_array : forall A. Array A -> Array A -> Array A
-append_array (Array xs) (Array ys) = Array (append_vector xs ys)
-
-filter_length : forall A n. (A -> Bool) -> Vector n A -> Nat
-filter_length p Nil = Z
-filter_length p (Cons x xs) = case p x of
-  False -> filter_length p xs
-  True -> S (filter_length p xs)
-
-filter_vector : forall A n. (p : A -> Bool)(xs : Vector n A) -> Vector (filter_length p xs) A
-filter_vector p Nil = Nil
-filter_vector p (Cons x xs) = case p x of
-  False -> filter_vector p xs
-  True -> Cons x (filter_vector p xs)
-
-filter_array : forall A. (A -> Bool) -> Array A -> Array A
-filter_array p (Array xs) = Array (filter_vector p xs)
+-- data Array A where
+--   Array : forall n. Vector n A -> Array A
+
+-- append_array : forall A. Array A -> Array A -> Array A
+-- append_array (Array xs) (Array ys) = Array (append_vector xs ys)
+
+-- filter_length : forall A n. (A -> Bool) -> Vector n A -> Nat
+-- filter_length p Nil = Z
+-- filter_length p (Cons x xs) = case p x of
+--   False -> filter_length p xs
+--   True -> S (filter_length p xs)
+
+-- filter_vector : forall A n. (p : A -> Bool)(xs : Vector n A) -> Vector (filter_length p xs) A
+-- filter_vector p Nil = Nil
+-- filter_vector p (Cons x xs) = case p x of
+--   False -> filter_vector p xs
+--   True -> Cons x (filter_vector p xs)
+
+-- filter_array : forall A. (A -> Bool) -> Array A -> Array A
+-- filter_array p (Array xs) = Array (filter_vector p xs)