Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
@ollef
ollef committed Jan 10, 2024
1 parent d201d10 commit fdac233
Show file tree
Hide file tree
Showing 2 changed files with 57 additions and 59 deletions.
89 changes: 44 additions & 45 deletions src/Elaboration/Context.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,6 @@ data Context (v :: Data.Kind.Type) = Context
, indices :: Index.Map v Var
, surfaceNames :: HashMap Name.Surface (Domain.Value, Domain.Type)
, varNames :: EnumMap Var Name
, values :: EnumMap Var Domain.Value
, types :: EnumMap Var Domain.Type
, boundVars :: IntSeq Var
, metas :: !(IORef (Meta.State M))
Expand Down Expand Up @@ -115,7 +114,6 @@ empty definitionKind definitionName = do
, surfaceNames = mempty
, varNames = mempty
, indices = Index.Map.Empty
, values = mempty
, types = mempty
, boundVars = mempty
, metas = ms
Expand All @@ -134,7 +132,6 @@ emptyFrom context =
, surfaceNames = mempty
, varNames = mempty
, indices = Index.Map.Empty
, values = mempty
, types = mempty
, boundVars = mempty
, metas = context.metas
Expand Down Expand Up @@ -220,7 +217,10 @@ extendSurfaceDef context surfaceName@(Name.Surface nameText) value type_ = do
{ surfaceNames = HashMap.insert surfaceName (Domain.var var, type_) context.surfaceNames
, varNames = EnumMap.insert var (Name nameText) context.varNames
, indices = context.indices Index.Map.:> var
, values = EnumMap.insert var value context.values
, equations =
context.equations
{ equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
}
, types = EnumMap.insert var type_ context.types
}
, var
Expand All @@ -244,7 +244,10 @@ extendDef context name value type_ = do
( context
{ varNames = EnumMap.insert var name context.varNames
, indices = context.indices Index.Map.:> var
, values = EnumMap.insert var value context.values
, equations =
context.equations
{ equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
}
, types = EnumMap.insert var type_ context.types
}
, var
Expand Down Expand Up @@ -272,21 +275,26 @@ extendBefore context beforeVar binding type_ = do
)

defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
defineWellOrdered context var value =
defineWellOrdered context head spine value =
context
{ values = EnumMap.insert var value context.values
, boundVars = IntSeq.delete var context.boundVars
{ equations =
context.equations
{ equal = HashMap.insertWith (<>) head [(spine, value)] context.equations.equal
}
, boundVars = case (head, spine) of
(Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
_ -> context.boundVars
}

skip :: Context v -> M (Context (Succ v))
skip context = do
(context', _) <- extendDef context "skip" Builtin.Type Builtin.Type
pure context'

define :: Context v -> Var -> Domain.Value -> M (Context v)
define context var value = do
deps <- evalStateT (dependencies context value) mempty
let context' = defineWellOrdered context var value
define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
define context head spine value = do
deps <- evalStateT (freeVars context value) mempty
let context' = defineWellOrdered context head spine value
(pre, post) =
Tsil.partition (`EnumSet.member` deps) $
IntSeq.toTsil context'.boundVars
Expand All @@ -297,51 +305,51 @@ define context var value = do
}

-- TODO: Move
dependencies
freeVars
:: Context v
-> Domain.Value
-> StateT (EnumMap Var (EnumSet Var)) M (EnumSet Var)
dependencies context value = do
freeVars context value = do
value' <- lift $ forceHeadGlue context value
case value' of
Domain.Neutral hd spine -> do
hdVars <- headVars hd
elimVars <- Domain.mapM eliminationDependencies spine
elimVars <- Domain.mapM eliminationVars spine
pure $ hdVars <> fold elimVars
Domain.Con _ args ->
fold <$> mapM (dependencies context . snd) args
fold <$> mapM (freeVars context . snd) args
Domain.Lit _ ->
pure mempty
Domain.Glued (Domain.Global _) spine _ ->
fold <$> Domain.mapM eliminationDependencies spine
fold <$> Domain.mapM eliminationVars spine
Domain.Glued _ _ value'' ->
dependencies context value''
freeVars context value''
Domain.Lazy lazyValue -> do
value'' <- lift $ force lazyValue
dependencies context value''
freeVars context value''
Domain.Lam bindings type' _ closure ->
abstractionDependencies (Bindings.toName bindings) type' closure
abstractionVars (Bindings.toName bindings) type' closure
Domain.Pi binding type' _ closure ->
abstractionDependencies (Binding.toName binding) type' closure
abstractionVars (Binding.toName binding) type' closure
Domain.Fun domain _ target -> do
domainVars <- dependencies context domain
targetVars <- dependencies context target
domainVars <- freeVars context domain
targetVars <- freeVars context target
pure $ domainVars <> targetVars
where
eliminationDependencies elimination =
eliminationVars elimination =
case elimination of
Domain.App _plicity arg ->
dependencies context arg
freeVars context arg
Domain.Case (Domain.Branches env branches defaultBranch) -> do
defaultBranchVars <- mapM (dependencies context <=< lift . Evaluation.evaluate env) defaultBranch
defaultBranchVars <- mapM (freeVars context <=< lift . Evaluation.evaluate env) defaultBranch
brVars <- branchVars context env branches
pure $ fold defaultBranchVars <> brVars

abstractionDependencies name type' closure = do
typeVars <- dependencies context type'
abstractionVars name type' closure = do
typeVars <- freeVars context type'
(context', var) <- lift $ extend context name type'
body <- lift $ Evaluation.evaluateClosure closure $ Domain.var var
bodyVars <- dependencies context' body
bodyVars <- freeVars context' body
pure $ typeVars <> EnumSet.delete var bodyVars

headVars hd =
Expand All @@ -351,7 +359,7 @@ dependencies context value = do
cache <- get
typeDeps <- case EnumMap.lookup v cache of
Nothing -> do
typeDeps <- dependencies context $ lookupVarType v context
typeDeps <- freeVars context $ lookupVarType v context
modify $ EnumMap.insert v typeDeps
pure typeDeps
Just typeDeps ->
Expand All @@ -378,7 +386,7 @@ dependencies context value = do
Syntax.LiteralBranches literalBranches ->
forM (toList literalBranches) \(_, branch) -> do
branch' <- lift $ Evaluation.evaluate env branch
dependencies context' branch'
freeVars context' branch'

telescopeVars
:: Context v
Expand All @@ -389,10 +397,10 @@ dependencies context value = do
case tele of
Telescope.Empty body -> do
body' <- lift $ Evaluation.evaluate env body
dependencies context' body'
freeVars context' body'
Telescope.Extend binding domain _ tele' -> do
domain' <- lift $ Evaluation.evaluate env domain
domainVars <- dependencies context' domain'
domainVars <- freeVars context' domain'
(context'', var) <- lift $ extend context' (Bindings.toName binding) domain'
let env' =
Environment.extendVar env var
Expand Down Expand Up @@ -427,10 +435,6 @@ lookupVarType :: Var -> Context v -> Domain.Type
lookupVarType var context =
EnumMap.findWithDefault (panic $ "Context.lookupVarType " <> show var) var context.types

lookupVarValue :: Var -> Context v -> Maybe Domain.Type
lookupVarValue var context =
EnumMap.lookup var context.values

-------------------------------------------------------------------------------
-- Prettyable terms

Expand Down Expand Up @@ -492,12 +496,7 @@ newMetaReturningIndex context type_ = do
piBoundVars :: Context v -> Domain.Type -> M (Syntax.Type Void, Int)
piBoundVars context type_ = do
let arity = IntSeq.length context.boundVars
piType <-
varPis
context
Environment.empty {Environment.values = context.values}
((Explicit,) <$> toList context.boundVars)
type_
piType <- varPis context Environment.empty ((Explicit,) <$> toList context.boundVars) type_
pure (piType, arity)

varPis
Expand Down Expand Up @@ -600,7 +599,7 @@ forceHead context value =
Meta.EagerUnsolved {} ->
pure value
Domain.Neutral head spine
| Just spineValues <- HashMap.lookup head context.equalities.equal -> do
| Just spineValues <- HashMap.lookup head context.equations.equal -> do
let go [] = pure value
go ((eqSpine, eqValue) : rest)
| Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
Expand Down Expand Up @@ -639,7 +638,7 @@ forceHeadGlue context value =
Meta.EagerUnsolved {} ->
pure value
Domain.Neutral head spine
| Just spineValues <- HashMap.lookup head context.equalities.equal -> do
| Just spineValues <- HashMap.lookup head context.equations.equal -> do
let go [] = pure value
go ((eqSpine, eqValue) : rest)
| Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
Expand Down
27 changes: 13 additions & 14 deletions src/Elaboration/Matching.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -603,7 +603,7 @@ expandAnnotations context matches =
pure ()
pure $ Match value forcedValue plicity (unresolvedPattern pat) type_ : matches'
_ ->
fail "couldn't create instantitation for prefix"
fail "couldn't create instantiation for prefix"

matchInstantiation :: Match -> Maybe PatternInstantiation
matchInstantiation match =
Expand All @@ -615,7 +615,7 @@ matchInstantiation match =
Match _ _ _ (Pattern _ (Forced _)) _ ->
pure mempty
_ ->
fail "No match instantitation"
fail "No match instantiation"

solved :: [Match] -> Maybe PatternInstantiation
solved =
Expand Down Expand Up @@ -665,18 +665,17 @@ splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine
_ -> do
typeType <- fetch $ Query.ElaboratedType typeName
typeType' <- Evaluation.evaluate Environment.empty typeType
let
contextWithoutScrutineeVar =
case scrutineeHead of
Domain.Var scrutineeVar ->
-- Ensure the metas don't depend on the scrutineeVar, because that
-- is guaranteed to lead to circularity when solving scrutineeVar
-- later.
outerContext
{ Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
}
-- TODO: is this correct?
_ -> outerContext
let contextWithoutScrutineeVar =
case scrutineeHead of
Domain.Var scrutineeVar ->
-- Ensure the metas don't depend on the scrutineeVar, because that
-- is guaranteed to lead to circularity when solving scrutineeVar
-- later.
outerContext
{ Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
}
-- TODO: is this correct?
_ -> outerContext
(metas, _) <- Elaboration.insertMetas contextWithoutScrutineeVar Elaboration.UntilTheEnd typeType'
f <- Unification.tryUnify outerContext (Domain.Neutral (Domain.Global typeName) $ Domain.Apps $ fromList metas) outerType
result <- goParams (Context.spanned span outerContext) metas mempty tele'
Expand Down

0 comments on commit fdac233

Please sign in to comment.