From e4edbfb97b94788c35c660ed1e61b8a698872580 Mon Sep 17 00:00:00 2001 From: Olle Fredriksson Date: Wed, 20 Mar 2024 07:37:53 +0100 Subject: [PATCH] wip --- src/Elaboration.hs-boot | 15 ++---- src/Elaboration/Context.hs | 48 ++++++++++++-------- src/Elaboration/Unification.hs-boot | 4 +- tests/singles/type-checking/array-append.vix | 40 ++++++++-------- 4 files changed, 54 insertions(+), 53 deletions(-) diff --git a/src/Elaboration.hs-boot b/src/Elaboration.hs-boot index 6ec12f22..d22af172 100644 --- a/src/Elaboration.hs-boot +++ b/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,6 +11,8 @@ import Name (Name) import qualified Name import Plicity import qualified Postponement +import Prettyprinter (Doc) +import Protolude import qualified Surface.Syntax as Surface check @@ -22,19 +20,15 @@ check -> 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 diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs index dcbba856..17c55c4f 100644 --- a/src/Elaboration/Context.hs +++ b/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' diff --git a/src/Elaboration/Unification.hs-boot b/src/Elaboration/Unification.hs-boot index e8996f61..21961dd7 100644 --- a/src/Elaboration/Unification.hs-boot +++ b/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 diff --git a/tests/singles/type-checking/array-append.vix b/tests/singles/type-checking/array-append.vix index 76b48bab..ed1ed36b 100644 --- a/tests/singles/type-checking/array-append.vix +++ b/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)