summaryrefslogtreecommitdiff
path: root/src/Inky/Term/Desugar.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Inky/Term/Desugar.idr')
-rw-r--r--src/Inky/Term/Desugar.idr110
1 files changed, 15 insertions, 95 deletions
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 50676ce..1ce0e41 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -80,89 +80,6 @@ desugarMapCaseNames [<] [<] i [<] f = Refl
desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
cong (:< l) $ desugarMapCaseNames as fresh i prfs f
--- -- Well Formed
-
--- desugarMapChecks :
--- (0 meta : m) =>
--- (a : Ty (tyCtx :< arg ++ bound)) -> (len : LengthOf bound) ->
--- (0 prf : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveIn` a) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- Synths tyEnv tmEnv t (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) a) ->
--- SynthsOnly t ->
--- Checks tyEnv tmEnv
--- (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) a)
--- (desugarMap {m} a (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prf f t)
--- desugarMapTupleChecks :
--- (0 meta : m) =>
--- (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
--- (0 fresh' : AllFresh (as <>< bs).names) ->
--- (0 fresh : AllFresh as.names) ->
--- (len : LengthOf bound) ->
--- (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- Synths tyEnv tmEnv t
--- (sub (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) (TProd (MkRow (as <>< bs) fresh'))) ->
--- SynthsOnly t ->
--- AllChecks tyEnv tmEnv
--- (subAll (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) as)
--- (desugarMapTuple {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f t).context
--- desugarMapCaseBranches :
--- (0 meta : m) =>
--- (as : Context (Ty (tyCtx :< arg ++ bound))) -> (len' : LengthOf bs) ->
--- (0 fresh' : AllFresh (as <>< bs).names) ->
--- (0 fresh : AllFresh as.names) ->
--- (len : LengthOf bound) ->
--- (0 prfs : index (dropAll len) (toVar {sx = tyCtx :< arg} Here) `StrictlyPositiveInAll` as) ->
--- {env1 : All (const $ Thinned Ty [<]) tyCtx} ->
--- {env2 : All (const $ Thinned Ty [<]) bound} ->
--- {b, c : Ty [<]} ->
--- Synths tyEnv tmEnv f (TArrow b c) ->
--- AllBranches tyEnv tmEnv
--- (subAll (((:<) {x = arg} env1 (b `Over` Id)) ++ env2) as)
--- (sub (((:<) {x = arg} env1 (c `Over` Id)) ++ env2) (TSum (MkRow (as <>< bs) fresh')))
--- (desugarMapCase {m} as fresh (index (dropAll len) (toVar {sx = tyCtx :< arg} Here)) prfs f).context
-
--- desugarMapChecks (TVar j) len TVar fun arg argSynOnly
--- with (index (dropAll len) (toVar Here) `decEq` j)
--- desugarMapChecks (TVar _) len TVar fun arg argSynOnly | True `Because` Refl =
--- EmbedC App (AppS fun [EmbedC argSynOnly arg $ alphaSym $ alphaRefl b _ $ ?b]) ?c
--- _ | False `Because` neq =
--- EmbedC argSynOnly arg $ alphaSym $ alphaRefl _ _ ?a
--- desugarMapChecks (TArrow a b) len (TArrow prf) fun arg argSynOnly =
--- EmbedC argSynOnly arg $ ?dmc_2
--- desugarMapChecks (TProd (MkRow as fresh)) len (TProd prfs) fun arg argSynOnly =
--- TupC (desugarMapTupleChecks as Z fresh fresh len prfs fun arg argSynOnly)
--- desugarMapChecks (TSum (MkRow as fresh)) len (TSum prfs) fun arg argSynOnly =
--- CaseC arg (desugarMapCaseBranches as Z fresh fresh len prfs fun)
--- desugarMapChecks (TFix x a) len (TFix prf) fun arg' argSynOnly =
--- let
--- x =
--- -- FoldC arg' (RollC $
--- desugarMapChecks
--- { m
--- , meta
--- , tyCtx
--- , arg
--- , bound = bound :< x
--- , env1
--- , env2 = env2 :< ?dmc_90
--- , b
--- , c
--- , tyEnv
--- , tmEnv = tmEnv :< (?dmc_92 `Over` Id)
--- , f = thin (Drop Id) f
--- , t = Var meta ((%%) "_eta" {pos = Here})
--- }
--- a (S len) prf ?x ?y ?z
--- -- Need assoc. of subst
--- in FoldC arg' (RollC ?dmc_99)
-
-- Desugar Terms ---------------------------------------------------------------
desugarSynths :
@@ -225,8 +142,8 @@ desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
(Abs meta
(["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
(TArrow (TArrow (TArrow b c)
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
desugarChecks (VarC prf1 prf2) = desugarSynths prf1
@@ -277,11 +194,11 @@ maybeDesugarList :
maybeDesugarAll :
(len : LengthOf tyCtx) =>
(ts : Context (Term Sugar m tyCtx tmCtx)) ->
- Maybe (All (const $ Term NoSugar m tyCtx tmCtx) ts.names)
+ Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
maybeDesugarBranches :
(len : LengthOf tyCtx) =>
(ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
- Maybe (All (const $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
+ Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
maybeDesugar (Annot meta t a) = do
t <- maybeDesugar t
@@ -302,8 +219,8 @@ maybeDesugar (App meta e ts) = do
ts <- maybeDesugarList ts
pure (App meta e ts)
maybeDesugar (Tup meta (MkRow ts fresh)) = do
- ts' <- maybeDesugarAll ts
- pure (Tup meta (fromAll (MkRow ts fresh) ts'))
+ ts <- maybeDesugarAll ts
+ pure (Tup meta (fromAll ts fresh))
maybeDesugar (Prj meta e l) = do
e <- maybeDesugar e
pure (Prj meta e l)
@@ -312,8 +229,8 @@ maybeDesugar (Inj meta l t) = do
pure (Inj meta l t)
maybeDesugar (Case meta e (MkRow ts fresh)) = do
e <- maybeDesugar e
- ts' <- maybeDesugarBranches ts
- pure (Case meta e (fromAll (MkRow ts fresh) ts'))
+ ts <- maybeDesugarBranches ts
+ pure (Case meta e (fromAll ts fresh))
maybeDesugar (Roll meta t) = do
t <- maybeDesugar t
pure (Roll meta t)
@@ -333,17 +250,20 @@ maybeDesugar (Map meta (x ** a) b c) =
(Abs meta
(["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
(TArrow (TArrow (TArrow b c)
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (b `Over` Id)) a))
- (sub (tabulate len ((`Over` Id) . TVar . toVar) :< (c `Over` Id)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a))
+ (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a))
maybeDesugarList [] = pure []
maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = [| maybeDesugarAll ts :< maybeDesugar t |]
+maybeDesugarAll (ts :< (l :- t)) = do
+ ts <- maybeDesugarAll ts
+ t <- maybeDesugar t
+ pure (ts :< (l :- t))
maybeDesugarBranches [<] = pure [<]
maybeDesugarBranches (ts :< (l :- (x ** t))) = do
ts <- maybeDesugarBranches ts
t <- maybeDesugar t
- pure (ts :< (x ** t))
+ pure (ts :< (l :- (x ** t)))
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:42:19 +0000