wip

src/Core/Evaluation.hs

@@ -16,6 +16,7 @@ import qualified Core.Domain.Telescope as Domain.Telescope
 import qualified Core.Syntax as Syntax
 import Data.OrderedHashMap (OrderedHashMap)
 import qualified Data.OrderedHashMap as OrderedHashMap
+import qualified Data.Sequence as Seq
 import Data.Some (Some)
 import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
@@ -28,6 +29,7 @@ import Plicity
 import Protolude hiding (IntMap, Seq, evaluate, force, head, try)
 import Query (Query)
 import qualified Query
+import qualified Query.Mapped as Mapped
 import Rock
 import Telescope (Telescope)
 import qualified Telescope
@@ -61,15 +63,19 @@ evaluate env term =
           Domain.var var
         Just value
           | Index.Succ index > Environment.glueableBefore env ->
-              Domain.Glued (Domain.Var var) mempty value
+              Domain.Stuck (Domain.Var var) mempty value mempty
           | otherwise ->
               value
     Syntax.Global name -> do
       result <- try $ fetch $ Query.ElaboratedDefinition name
       case result of
         Right (Syntax.ConstantDefinition term', _) -> do
+          recursive <- fetch $ Query.TransitiveDependencies name $ Mapped.Query name
           value <- lazyEvaluate Environment.empty term'
-          pure $ Domain.Glued (Domain.Global name) mempty value
+          pure
+            if isJust recursive
+              then Domain.Stuck (Domain.Global name) mempty value mempty
+              else Domain.Glued (Domain.Global name) mempty value
         Left (Cyclic (_ :: Some Query)) ->
           pure $ Domain.global name
         _ ->
@@ -207,6 +213,9 @@ apply fun plicity arg =
           panic "Core.Evaluation: plicity mismatch"
     Domain.Neutral hd spine ->
       pure $ Domain.Neutral hd $ spine Domain.:> Domain.App plicity arg
+    Domain.Stuck hd args headApp Domain.Empty -> do
+      headApp' <- apply headApp plicity arg
+      pure $ Domain.Stuck hd (args Seq.:|> (plicity, arg)) headApp' Domain.Empty
     Domain.Stuck hd args value spine ->
       pure $ Domain.Stuck hd args value $ spine Domain.:> Domain.App plicity arg
     Domain.Glued hd spine value -> do

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

@@ -647,7 +647,7 @@ forceNeutral context head_ spine
     chooseDefaultBranch =
       case spine of
         (Domain.Spine _ (_ Seq.:<| _))
-          | Just spineInequalities <- HashMap.lookup head_ context.notEqual -> do
+          | Just spineInequalities <- HashMap.lookup head_ context.notEqual ->
               findMatchingDefaultBranch spineInequalities
         _ -> metaSolution
 
@@ -684,6 +684,22 @@ forceNeutral context head_ spine
             pure Nothing
       _ -> pure Nothing
 
+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.
 forceHead
@@ -692,23 +708,31 @@ forceHead
   -> M Domain.Value
 forceHead context value =
   case value of
-    Domain.Neutral head_ spine -> do
-      maybeEqValue <- forceNeutral context head_ spine
-      case maybeEqValue of
-        Just meqValue -> do
-          value'' <- meqValue
-          forceHead context value''
+    Domain.Neutral head_ spine -> neutral head_ spine
+    Domain.Stuck head_ args headApp spine -> do
+      maybeUnstuck <- unstuck context headApp
+      case maybeUnstuck of
         Nothing ->
-          pure value
-    Domain.Stuck head_ args value' spine ->
-      undefined -- TODO
+          neutral head_ $ Domain.Apps args <> spine
+        Just unstuckValue -> do
+          value' <- Evaluation.applySpine unstuckValue spine
+          forceHead context value'
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHead context value'
     _ ->
       pure value
+  where
+    neutral head_ spine = do
+      maybeEqValue <- forceNeutral context head_ spine
+      case maybeEqValue of
+        Just meqValue -> do
+          value' <- meqValue
+          forceHead context value'
+        Nothing ->
+          pure value
 
 -- | Evaluate the head of a value further, if (now) possible due to meta
 -- solutions or new value bindings, returning glued values.
@@ -718,21 +742,30 @@ forceHeadGlue
   -> M Domain.Value
 forceHeadGlue context value =
   case value of
-    Domain.Neutral head_ spine -> do
+    Domain.Neutral head_ spine -> neutral head_ spine
+    Domain.Stuck head_ args headApp spine -> do
+      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'
+    _ ->
+      pure value
+  where
+    neutral head_ spine = do
       maybeEqValue <- forceNeutral context head_ spine
       case maybeEqValue of
         Just meqValue -> do
           lazyValue <- lazy meqValue
           pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
         Nothing ->
           pure value
-    Domain.Stuck head_ args value' spine ->
-      undefined -- TODO
-    Domain.Lazy lazyValue -> do
-      value' <- force lazyValue
-      forceHeadGlue context value'
-    _ ->
-      pure value
 
 instantiateType
   :: Context v

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)