git.iko.soy/Idris-dev
on master help sign in
Clean up inference in Pruviloj
210db7dDavid Raymond Christiansen
libs/pruviloj/Pruviloj/Core.idr+27−9
compare with master
unifiedsplit
@@ -3,13 +3,8 @@
3||| eventual Prelude inclusion.
3||| eventual Prelude inclusion.
4module Pruviloj.Core
4module Pruviloj.Core
5
5
6−
7−import Language.Reflection.Elab
8import Language.Reflection.Utils
6import Language.Reflection.Utils
9
7
10−data Infer : Type where
11− MkInfer : (a : Type) -> a -> Infer
12−
13||| Run something for effects, throwing away the return value
8||| Run something for effects, throwing away the return value
14ignore : Functor f => f a -> f ()
9ignore : Functor f => f a -> f ()
15ignore x = map (const ()) x
10ignore x = map (const ()) x
@@ -85,11 +80,11 @@ intros = do g <- snd <$> getGoal
85
80
86||| Run a tactic inside of a particular hole, if it still exists. If
81||| Run a tactic inside of a particular hole, if it still exists. If
87||| it has been solved, do nothing.
82||| it has been solved, do nothing.
88−inHole : TTName -> Elab () -> Elab ()
83+inHole : TTName -> Elab a -> Elab (Maybe a)
89inHole h todo =
84inHole h todo =
90− when (h `elem` !getHoles) $
85+ if (h `elem` !getHoles)
91− do focus h
86+ then do focus h; Just <$> todo
92− todo
87+ else return Nothing
93
88
94||| Restrict a polymorphic type to () for contexts where it doesn't
89||| Restrict a polymorphic type to () for contexts where it doesn't
95||| matter. This is nice for sticking `debug` in a context where
90||| matter. This is nice for sticking `debug` in a context where
@@ -142,3 +137,26 @@ bindPat = do compute
142 case g of
137 case g of
143 Bind n (PVTy _) _ => patbind n
138 Bind n (PVTy _) _ => patbind n
144 _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
139 _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
140+
141+||| The underlying implementation type for the inferType operator.
142+data Infer : Type where
143+ MkInfer : (a : Type) -> a -> Infer
144+
145+||| Run a tactic script in a context where the type of the resulting
146+||| expression must be solvable via unification. Return the term and
147+||| its type.
148+|||
149+||| @ tac a tactic script that will be run with focus on the hole
150+||| whose type is to be inferred.
151+total
152+inferType : (tac : Elab ()) -> Elab (TT, TT)
153+inferType tac =
154+ case fst !(runElab `(Infer) (startInfer *> tac)) of
155+ `(MkInfer ~ty ~tm) => return (tm, ty)
156+ _ => fail [TextPart "Not infer"]
157+ where
158+ startInfer : Elab ()
159+ startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]
160+ | err => fail [TextPart "Type inference failure"]
161+ solve
162+ focus tmH
libs/pruviloj/Pruviloj/Internals.idr+5−9
@@ -77,10 +77,6 @@ enumerate xs = enumerate' xs 0
77 enumerate' [] _ = []
77 enumerate' [] _ = []
78 enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
78 enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
79
79
80−getSigmaArgs : Raw -> Elab (Raw, Raw)
81−getSigmaArgs `(MkSigma {a=~_} {P=~_} ~rhsTy ~lhs) = return (rhsTy, lhs)
82−getSigmaArgs arg = fail [TextPart "Not a sigma constructor"]
83−
84bindPats : List (TTName, Binder Raw) -> Raw -> Raw
80bindPats : List (TTName, Binder Raw) -> Raw -> Raw
85bindPats [] res = res
81bindPats [] res = res
86bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
82bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
@@ -109,19 +105,19 @@ partial
109elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
105elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
110elabPatternClause lhs rhs =
106elabPatternClause lhs rhs =
111 do -- Elaborate the LHS in a context where its type will be solved via unification
107 do -- Elaborate the LHS in a context where its type will be solved via unification
112− (pat, _) <- runElab `(Sigma Type id) $
108+ (pat, _) <- runElab `(Infer) $
113 do th <- newHole "finalTy" `(Type)
109 do th <- newHole "finalTy" `(Type)
114 patH <- newHole "pattern" (Var th)
110 patH <- newHole "pattern" (Var th)
115− fill `(MkSigma ~(Var th) ~(Var patH) : Sigma Type id)
111+ fill `(MkInfer ~(Var th) ~(Var patH))
116 solve
112 solve
117 focus patH
113 focus patH
118 lhs
114 lhs
119 -- Convert all remaining holes to pattern variables
115 -- Convert all remaining holes to pattern variables
120 traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
116 traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
121− let (pvars, sigma) = extractBinders !(forgetTypes pat)
117+ (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forgetTypes pat)
122− (rhsTy, lhsTm) <- getSigmaArgs sigma
118+ | fail [TextPart "Couldn't infer type of left-hand pattern"]
123 rhsTm <- runElab (bindPatTys pvars rhsTy) $
119 rhsTm <- runElab (bindPatTys pvars rhsTy) $
124− do -- Introduce all the pattern variables from the LHS
120+ do -- Introduce all the pattern variables from the LHS
125 repeatUntilFail bindPat <|> return ()
121 repeatUntilFail bindPat <|> return ()
126 rhs
122 rhs
127 realRhs <- forgetTypes (fst rhsTm)
123 realRhs <- forgetTypes (fst rhsTm)