@@ -1589,8 +1589,6 @@ case_ ind autoSolve ist fn tm = do
15891589 else casetac (forget val)
15901590 when autoSolve solveAll
15911591
1592−tacN :: String -> Name
1593−tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]
15941592
15951593runTactical :: FC -> Env -> Term -> ElabD ()
15961594runTactical fc env tm = do tm' <- eval tm
@@ -2018,780 +2016,6 @@ runTac autoSolve ist perhapsFC fn tac
20182016 runReflected t = do t' <- reify ist t
20192017 runTac autoSolve ist perhapsFC fn t'
20202018
2021−-- | Prefix a name with the "Language.Reflection" namespace
2022−reflm :: String -> Name
2023−reflm n = sNS (sUN n) ["Reflection", "Language"]
2024−
2025−
2026−-- | Reify tactics from their reflected representation
2027−reify :: IState -> Term -> ElabD PTactic
2028−reify _ (P _ n _) | n == reflm "Intros" = return Intros
2029−reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
2030−reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
2031−reify _ (P _ n _) | n == reflm "Solve" = return Solve
2032−reify _ (P _ n _) | n == reflm "Compute" = return Compute
2033−reify _ (P _ n _) | n == reflm "Skip" = return Skip
2034−reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
2035−reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
2036−reify ist t@(App _ _)
2037− | (P _ f _, args) <- unApply t = reifyApp ist f args
2038−reify _ t = fail ("Unknown tactic " ++ show t)
2039−
2040−reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
2041−reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
2042−reifyApp _ t [Constant (I i)]
2043− | t == reflm "Search" = return (ProofSearch True True i Nothing [])
2044−reifyApp _ t [x]
2045− | t == reflm "Refine" = do n <- reifyTTName x
2046− return $ Refine n []
2047−reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
2048− goal <- reifyTT ty
2049− return $ Claim n' (delab ist goal)
2050−reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
2051−reifyApp ist t [Constant (Str n), x]
2052− | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
2053−reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
2054−reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
2055−reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
2056−reifyApp ist t [t']
2057− | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
2058−reifyApp ist t [t']
2059− | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
2060−reifyApp ist t [t']
2061− | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
2062−reifyApp _ t [t']
2063− | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
2064−reifyApp ist t [t']
2065− | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
2066−reifyApp ist t [x]
2067− | t == reflm "Focus" = liftM Focus (reifyTTName x)
2068−reifyApp ist t [t']
2069− | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
2070−reifyApp ist t [n, t']
2071− | t == reflm "LetTac" = do n' <- reifyTTName n
2072− t'' <- reifyTT t'
2073− return $ LetTac n' (delab ist t')
2074−reifyApp ist t [n, tt', t']
2075− | t == reflm "LetTacTy" = do n' <- reifyTTName n
2076− tt'' <- reifyTT tt'
2077− t'' <- reifyTT t'
2078− return $ LetTacTy n' (delab ist tt'') (delab ist t'')
2079−reifyApp ist t [errs]
2080− | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
2081−reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
2082−
2083−reifyReportParts :: Term -> ElabD [ErrorReportPart]
2084−reifyReportParts errs =
2085− case unList errs of
2086− Nothing -> fail "Failed to reify errors"
2087− Just errs' ->
2088− let parts = mapM reifyReportPart errs' in
2089− case parts of
2090− Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
2091− Right errs'' ->
2092− return errs''
2093−
2094−-- | Reify terms from their reflected representation
2095−reifyTT :: Term -> ElabD Term
2096−reifyTT t@(App _ _)
2097− | (P _ f _, args) <- unApply t = reifyTTApp f args
2098−reifyTT t@(P _ n _)
2099− | n == reflm "Erased" = return $ Erased
2100−reifyTT t@(P _ n _)
2101− | n == reflm "Impossible" = return $ Impossible
2102−reifyTT t = fail ("Unknown reflection term: " ++ show t)
2103−
2104−reifyTTApp :: Name -> [Term] -> ElabD Term
2105−reifyTTApp t [nt, n, x]
2106− | t == reflm "P" = do nt' <- reifyTTNameType nt
2107− n' <- reifyTTName n
2108− x' <- reifyTT x
2109− return $ P nt' n' x'
2110−reifyTTApp t [Constant (I i)]
2111− | t == reflm "V" = return $ V i
2112−reifyTTApp t [n, b, x]
2113− | t == reflm "Bind" = do n' <- reifyTTName n
2114− b' <- reifyTTBinder reifyTT (reflm "TT") b
2115− x' <- reifyTT x
2116− return $ Bind n' b' x'
2117−reifyTTApp t [f, x]
2118− | t == reflm "App" = do f' <- reifyTT f
2119− x' <- reifyTT x
2120− return $ App f' x'
2121−reifyTTApp t [c]
2122− | t == reflm "TConst" = liftM Constant (reifyTTConst c)
2123−reifyTTApp t [t', Constant (I i)]
2124− | t == reflm "Proj" = do t'' <- reifyTT t'
2125− return $ Proj t'' i
2126−reifyTTApp t [tt]
2127− | t == reflm "TType" = liftM TType (reifyTTUExp tt)
2128−reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
2129−
2130−-- | Reify raw terms from their reflected representation
2131−reifyRaw :: Term -> ElabD Raw
2132−reifyRaw t@(App _ _)
2133− | (P _ f _, args) <- unApply t = reifyRawApp f args
2134−reifyRaw t@(P _ n _)
2135− | n == reflm "RType" = return $ RType
2136−reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)
2137−
2138−reifyRawApp :: Name -> [Term] -> ElabD Raw
2139−reifyRawApp t [n]
2140− | t == reflm "Var" = liftM Var (reifyTTName n)
2141−reifyRawApp t [n, b, x]
2142− | t == reflm "RBind" = do n' <- reifyTTName n
2143− b' <- reifyTTBinder reifyRaw (reflm "Raw") b
2144− x' <- reifyRaw x
2145− return $ RBind n' b' x'
2146−reifyRawApp t [f, x]
2147− | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
2148−reifyRawApp t [t']
2149− | t == reflm "RForce" = liftM RForce (reifyRaw t')
2150−reifyRawApp t [c]
2151− | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
2152−reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ show (t, args))
2153−
2154−reifyTTName :: Term -> ElabD Name
2155−reifyTTName t
2156− | (P _ f _, args) <- unApply t = reifyTTNameApp f args
2157−reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
2158−
2159−reifyTTNameApp :: Name -> [Term] -> ElabD Name
2160−reifyTTNameApp t [Constant (Str n)]
2161− | t == reflm "UN" = return $ sUN n
2162−reifyTTNameApp t [n, ns]
2163− | t == reflm "NS" = do n' <- reifyTTName n
2164− ns' <- reifyTTNamespace ns
2165− return $ sNS n' ns'
2166−reifyTTNameApp t [Constant (I i), Constant (Str n)]
2167− | t == reflm "MN" = return $ sMN i n
2168−reifyTTNameApp t []
2169− | t == reflm "NErased" = return NErased
2170−reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
2171−
2172−reifyTTNamespace :: Term -> ElabD [String]
2173−reifyTTNamespace t@(App _ _)
2174− = case unApply t of
2175− (P _ f _, [Constant StrType])
2176− | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
2177− (P _ f _, [Constant StrType, Constant (Str n), ns])
2178− | f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
2179− _ -> fail ("Unknown reflection namespace arg: " ++ show t)
2180−reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
2181−
2182−reifyTTNameType :: Term -> ElabD NameType
2183−reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
2184−reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
2185−reifyTTNameType t@(App _ _)
2186− = case unApply t of
2187− (P _ f _, [Constant (I tag), Constant (I num)])
2188− | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!
2189− | f == reflm "TCon" -> return $ TCon tag num
2190− _ -> fail ("Unknown reflection name type: " ++ show t)
2191−reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
2192−
2193−reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
2194−reifyTTBinder reificator binderType t@(App _ _)
2195− = case unApply t of
2196− (P _ f _, bt:args) | forget bt == Var binderType
2197− -> reifyTTBinderApp reificator f args
2198− _ -> fail ("Mismatching binder reflection: " ++ show t)
2199−reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
2200−
2201−reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
2202−reifyTTBinderApp reif f [t]
2203− | f == reflm "Lam" = liftM Lam (reif t)
2204−reifyTTBinderApp reif f [t, k]
2205− | f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
2206−reifyTTBinderApp reif f [x, y]
2207− | f == reflm "Let" = liftM2 Let (reif x) (reif y)
2208−reifyTTBinderApp reif f [x, y]
2209− | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
2210−reifyTTBinderApp reif f [t]
2211− | f == reflm "Hole" = liftM Hole (reif t)
2212−reifyTTBinderApp reif f [t]
2213− | f == reflm "GHole" = liftM (GHole 0) (reif t)
2214−reifyTTBinderApp reif f [x, y]
2215− | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
2216−reifyTTBinderApp reif f [t]
2217− | f == reflm "PVar" = liftM PVar (reif t)
2218−reifyTTBinderApp reif f [t]
2219− | f == reflm "PVTy" = liftM PVTy (reif t)
2220−reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
2221−
2222−reifyTTConst :: Term -> ElabD Const
2223−reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
2224−reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
2225−reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
2226−reifyTTConst t@(App _ _)
2227− | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
2228−reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
2229−
2230−reifyTTConstApp :: Name -> Term -> ElabD Const
2231−reifyTTConstApp f aty
2232− | f == reflm "AType" = fmap AType (reifyArithTy aty)
2233−reifyTTConstApp f (Constant c@(I _))
2234− | f == reflm "I" = return $ c
2235−reifyTTConstApp f (Constant c@(BI _))
2236− | f == reflm "BI" = return $ c
2237−reifyTTConstApp f (Constant c@(Fl _))
2238− | f == reflm "Fl" = return $ c
2239−reifyTTConstApp f (Constant c@(I _))
2240− | f == reflm "Ch" = return $ c
2241−reifyTTConstApp f (Constant c@(Str _))
2242− | f == reflm "Str" = return $ c
2243−reifyTTConstApp f (Constant c@(B8 _))
2244− | f == reflm "B8" = return $ c
2245−reifyTTConstApp f (Constant c@(B16 _))
2246− | f == reflm "B16" = return $ c
2247−reifyTTConstApp f (Constant c@(B32 _))
2248− | f == reflm "B32" = return $ c
2249−reifyTTConstApp f (Constant c@(B64 _))
2250− | f == reflm "B64" = return $ c
2251−reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
2252−
2253−reifyArithTy :: Term -> ElabD ArithTy
2254−reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
2255−reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
2256−reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
2257−
2258−reifyNativeTy :: Term -> ElabD NativeTy
2259−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2260−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2261−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2262−reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
2263−reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
2264−
2265−reifyIntTy :: Term -> ElabD IntTy
2266−reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
2267−reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
2268−reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
2269−reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
2270−reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"
2271−
2272−reifyTTUExp :: Term -> ElabD UExp
2273−reifyTTUExp t@(App _ _)
2274− = case unApply t of
2275− (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
2276− (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
2277− _ -> fail ("Unknown reflection type universe expression: " ++ show t)
2278−reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
2279−
2280−-- | Create a reflected call to a named function/constructor
2281−reflCall :: String -> [Raw] -> Raw
2282−reflCall funName args
2283− = raw_apply (Var (reflm funName)) args
2284−
2285−-- | Lift a term into its Language.Reflection.TT representation
2286−reflect :: Term -> Raw
2287−reflect = reflectTTQuote []
2288−
2289−-- | Lift a term into its Language.Reflection.Raw representation
2290−reflectRaw :: Raw -> Raw
2291−reflectRaw = reflectRawQuote []
2292−
2293−claimTT :: Name -> ElabD Name
2294−claimTT n = do n' <- getNameFrom n
2295− claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
2296− return n'
2297−
2298−-- | Convert a reflected term to a more suitable form for pattern-matching.
2299−-- In particular, the less-interesting bits are elaborated to _ patterns. This
2300−-- happens to NameTypes, universe levels, names that are bound but not used,
2301−-- and the type annotation field of the P constructor.
2302−reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
2303−reflectTTQuotePattern unq (P _ n _)
2304− | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
2305− do fill (Var n) ; solve
2306− | otherwise =
2307− do tyannot <- claimTT (sMN 0 "pTyAnnot")
2308− movelast tyannot -- use a _ pattern here
2309− nt <- getNameFrom (sMN 0 "nt")
2310− claim nt (Var (reflm "NameType"))
2311− movelast nt -- use a _ pattern here
2312− n' <- getNameFrom (sMN 0 "n")
2313− claim n' (Var (reflm "TTName"))
2314− fill $ reflCall "P" [Var nt, Var n', Var tyannot]
2315− solve
2316− focus n'; reflectNameQuotePattern n
2317−reflectTTQuotePattern unq (V n)
2318− = do fill $ reflCall "V" [RConstant (I n)]
2319− solve
2320−reflectTTQuotePattern unq (Bind n b x)
2321− = do x' <- claimTT (sMN 0 "sc")
2322− movelast x'
2323− b' <- getNameFrom (sMN 0 "binder")
2324− claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
2325− (Var (sNS (sUN "TT") ["Reflection", "Language"])))
2326− if n `elem` freeNames x
2327− then do fill $ reflCall "Bind"
2328− [reflectName n,
2329− Var b',
2330− Var x']
2331− solve
2332− else do any <- getNameFrom (sMN 0 "anyName")
2333− claim any (Var (reflm "TTName"))
2334− movelast any
2335− fill $ reflCall "Bind"
2336− [Var any,
2337− Var b',
2338− Var x']
2339− solve
2340− focus x'; reflectTTQuotePattern unq x
2341− focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b
2342−reflectTTQuotePattern unq (App f x)
2343− = do f' <- claimTT (sMN 0 "f"); movelast f'
2344− x' <- claimTT (sMN 0 "x"); movelast x'
2345− fill $ reflCall "App" [Var f', Var x']
2346− solve
2347− focus f'; reflectTTQuotePattern unq f
2348− focus x'; reflectTTQuotePattern unq x
2349−reflectTTQuotePattern unq (Constant c)
2350− = do fill $ reflCall "TConst" [reflectConstant c]
2351− solve
2352−reflectTTQuotePattern unq (Proj t i)
2353− = do t' <- claimTT (sMN 0 "t"); movelast t'
2354− fill $ reflCall "Proj" [Var t', RConstant (I i)]
2355− solve
2356− focus t'; reflectTTQuotePattern unq t
2357−reflectTTQuotePattern unq (Erased)
2358− = do erased <- claimTT (sMN 0 "erased")
2359− movelast erased
2360− fill $ (Var erased)
2361− solve
2362−reflectTTQuotePattern unq (Impossible)
2363− = do fill $ Var (reflm "Impossible")
2364− solve
2365−reflectTTQuotePattern unq (TType exp)
2366− = do ue <- getNameFrom (sMN 0 "uexp")
2367− claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
2368− movelast ue
2369− fill $ reflCall "TType" [Var ue]
2370− solve
2371−reflectTTQuotePattern unq (UType u)
2372− = do uH <- getNameFrom (sMN 0 "someUniv")
2373− claim uH (Var (reflm "Universe"))
2374− movelast uH
2375− fill $ reflCall "UType" [Var uH]
2376− solve
2377− focus uH
2378− fill (Var (reflm (case u of
2379− NullType -> "NullType"
2380− UniqueType -> "UniqueType"
2381− AllTypes -> "AllTypes")))
2382− solve
2383−
2384−reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
2385−reflectRawQuotePattern unq (Var n)
2386− -- the unquoted names already have types, just use them
2387− | n `elem` unq = do fill (Var n); solve
2388− | otherwise = do fill (reflCall "Var" [reflectName n]); solve
2389−reflectRawQuotePattern unq (RBind n b sc) =
2390− do scH <- getNameFrom (sMN 0 "sc")
2391− claim scH (Var (reflm "Raw"))
2392− movelast scH
2393− bH <- getNameFrom (sMN 0 "binder")
2394− claim bH (RApp (Var (reflm "Binder"))
2395− (Var (reflm "Raw")))
2396− if n `elem` freeNamesR sc
2397− then do fill $ reflCall "RBind" [reflectName n,
2398− Var bH,
2399− Var scH]
2400− solve
2401− else do any <- getNameFrom (sMN 0 "anyName")
2402− claim any (Var (reflm "TTName"))
2403− movelast any
2404− fill $ reflCall "RBind" [Var any, Var bH, Var scH]
2405− solve
2406− focus scH; reflectRawQuotePattern unq sc
2407− focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b
2408− where freeNamesR (Var n) = [n]
2409− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,
2410− freeNamesR body \\ [n],
2411− freeNamesR t]
2412− freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
2413− (freeNamesR body \\ [n])
2414− freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
2415− freeNamesR RType = []
2416− freeNamesR (RUType _) = []
2417− freeNamesR (RForce r) = freeNamesR r
2418− freeNamesR (RConstant _) = []
2419−reflectRawQuotePattern unq (RApp f x) =
2420− do fH <- getNameFrom (sMN 0 "f")
2421− claim fH (Var (reflm "Raw"))
2422− movelast fH
2423− xH <- getNameFrom (sMN 0 "x")
2424− claim xH (Var (reflm "Raw"))
2425− movelast xH
2426− fill $ reflCall "RApp" [Var fH, Var xH]
2427− solve
2428− focus fH; reflectRawQuotePattern unq f
2429− focus xH; reflectRawQuotePattern unq x
2430−reflectRawQuotePattern unq RType =
2431− do fill (Var (reflm "RType"))
2432− solve
2433−reflectRawQuotePattern unq (RUType univ) =
2434− do uH <- getNameFrom (sMN 0 "universe")
2435− claim uH (Var (reflm "Universe"))
2436− movelast uH
2437− fill $ reflCall "RUType" [Var uH]
2438− solve
2439− focus uH; fill (reflectUniverse univ); solve
2440−reflectRawQuotePattern unq (RForce r) =
2441− do rH <- getNameFrom (sMN 0 "raw")
2442− claim rH (Var (reflm "Raw"))
2443− movelast rH
2444− fill $ reflCall "RForce" [Var rH]
2445− solve
2446− focus rH; reflectRawQuotePattern unq r
2447−reflectRawQuotePattern unq (RConstant c) =
2448− do cH <- getNameFrom (sMN 0 "const")
2449− claim cH (Var (reflm "Constant"))
2450− movelast cH
2451− fill (reflCall "RConstant" [Var cH]); solve
2452− focus cH
2453− fill (reflectConstant c); solve
2454−
2455−reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()
2456−reflectBinderQuotePattern q unq (Lam t)
2457− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2458− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
2459− solve
2460− focus t'; q unq t
2461−reflectBinderQuotePattern q unq (Pi _ t k)
2462− = do t' <- claimTT (sMN 0 "ty") ; movelast t'
2463− k' <- claimTT (sMN 0 "k"); movelast k';
2464− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
2465− solve
2466− focus t'; q unq t
2467−reflectBinderQuotePattern q unq (Let x y)
2468− = do x' <- claimTT (sMN 0 "ty"); movelast x';
2469− y' <- claimTT (sMN 0 "v"); movelast y';
2470− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
2471− solve
2472− focus x'; q unq x
2473− focus y'; q unq y
2474−reflectBinderQuotePattern q unq (NLet x y)
2475− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2476− y' <- claimTT (sMN 0 "v"); movelast y'
2477− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
2478− solve
2479− focus x'; q unq x
2480− focus y'; q unq y
2481−reflectBinderQuotePattern q unq (Hole t)
2482− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2483− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
2484− solve
2485− focus t'; q unq t
2486−reflectBinderQuotePattern q unq (GHole _ t)
2487− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2488− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
2489− solve
2490− focus t'; q unq t
2491−reflectBinderQuotePattern q unq (Guess x y)
2492− = do x' <- claimTT (sMN 0 "ty"); movelast x'
2493− y' <- claimTT (sMN 0 "v"); movelast y'
2494− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
2495− solve
2496− focus x'; q unq x
2497− focus y'; q unq y
2498−reflectBinderQuotePattern q unq (PVar t)
2499− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2500− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
2501− solve
2502− focus t'; q unq t
2503−reflectBinderQuotePattern q unq (PVTy t)
2504− = do t' <- claimTT (sMN 0 "ty"); movelast t'
2505− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
2506− solve
2507− focus t'; q unq t
2508−
2509−reflectUniverse :: Universe -> Raw
2510−reflectUniverse u =
2511− (Var (reflm (case u of
2512− NullType -> "NullType"
2513− UniqueType -> "UniqueType"
2514− AllTypes -> "AllTypes")))
2515−
2516−-- | Create a reflected TT term, but leave refs to the provided name intact
2517−reflectTTQuote :: [Name] -> Term -> Raw
2518−reflectTTQuote unq (P nt n t)
2519− | n `elem` unq = Var n
2520− | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
2521−reflectTTQuote unq (V n)
2522− = reflCall "V" [RConstant (I n)]
2523−reflectTTQuote unq (Bind n b x)
2524− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
2525−reflectTTQuote unq (App f x)
2526− = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
2527−reflectTTQuote unq (Constant c)
2528− = reflCall "TConst" [reflectConstant c]
2529−reflectTTQuote unq (Proj t i)
2530− = reflCall "Proj" [reflectTTQuote unq t, RConstant (I i)]
2531−reflectTTQuote unq (Erased) = Var (reflm "Erased")
2532−reflectTTQuote unq (Impossible) = Var (reflm "Impossible")
2533−reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
2534−reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
2535−
2536−reflectRawQuote :: [Name] -> Raw -> Raw
2537−reflectRawQuote unq (Var n)
2538− | n `elem` unq = Var n
2539− | otherwise = reflCall "Var" [reflectName n]
2540−reflectRawQuote unq (RBind n b r) =
2541− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
2542−reflectRawQuote unq (RApp f x) =
2543− reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
2544−reflectRawQuote unq RType = Var (reflm "RType")
2545−reflectRawQuote unq (RUType u) =
2546− reflCall "RUType" [reflectUniverse u]
2547−reflectRawQuote unq (RForce r) = reflCall "RForce" [reflectRawQuote unq r]
2548−reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]
2549−
2550−reflectNameType :: NameType -> Raw
2551−reflectNameType (Bound) = Var (reflm "Bound")
2552−reflectNameType (Ref) = Var (reflm "Ref")
2553−reflectNameType (DCon x y _)
2554− = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!
2555−reflectNameType (TCon x y)
2556− = reflCall "TCon" [RConstant (I x), RConstant (I y)]
2557−
2558−reflectName :: Name -> Raw
2559−reflectName (UN s)
2560− = reflCall "UN" [RConstant (Str (str s))]
2561−reflectName (NS n ns)
2562− = reflCall "NS" [ reflectName n
2563− , foldr (\ n s ->
2564− raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
2565− [ RConstant StrType, RConstant (Str n), s ])
2566− ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
2567− [ RConstant StrType ])
2568− (map str ns)
2569− ]
2570−reflectName (MN i n)
2571− = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
2572−reflectName (NErased) = Var (reflm "NErased")
2573−reflectName n = Var (reflm "NErased") -- special name, not yet implemented
2574−
2575−-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
2576−-- MNs corresponding to will care about the string but not the number. All
2577−-- others become _.
2578−reflectNameQuotePattern :: Name -> ElabD ()
2579−reflectNameQuotePattern n@(UN s)
2580− = do fill $ reflectName n
2581− solve
2582−reflectNameQuotePattern n@(NS _ _)
2583− = do fill $ reflectName n
2584− solve
2585−reflectNameQuotePattern (MN _ n)
2586− = do i <- getNameFrom (sMN 0 "mnCounter")
2587− claim i (RConstant (AType (ATInt ITNative)))
2588− movelast i
2589− fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
2590− solve
2591−reflectNameQuotePattern _ -- for all other names, match any
2592− = do nameHole <- getNameFrom (sMN 0 "name")
2593− claim nameHole (Var (reflm "TTName"))
2594− movelast nameHole
2595− fill (Var nameHole)
2596− solve
2597−
2598−reflectBinder :: Binder Term -> Raw
2599−reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
2600−
2601−reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
2602−reflectBinderQuote q ty unq (Lam t)
2603− = reflCall "Lam" [Var ty, q unq t]
2604−reflectBinderQuote q ty unq (Pi _ t k)
2605− = reflCall "Pi" [Var ty, q unq t, q unq k]
2606−reflectBinderQuote q ty unq (Let x y)
2607− = reflCall "Let" [Var ty, q unq x, q unq y]
2608−reflectBinderQuote q ty unq (NLet x y)
2609− = reflCall "NLet" [Var ty, q unq x, q unq y]
2610−reflectBinderQuote q ty unq (Hole t)
2611− = reflCall "Hole" [Var ty, q unq t]
2612−reflectBinderQuote q ty unq (GHole _ t)
2613− = reflCall "GHole" [Var ty, q unq t]
2614−reflectBinderQuote q ty unq (Guess x y)
2615− = reflCall "Guess" [Var ty, q unq x, q unq y]
2616−reflectBinderQuote q ty unq (PVar t)
2617− = reflCall "PVar" [Var ty, q unq t]
2618−reflectBinderQuote q ty unq (PVTy t)
2619− = reflCall "PVTy" [Var ty, q unq t]
2620−
2621−mkList :: Raw -> [Raw] -> Raw
2622−mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
2623−mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
2624− x)
2625− (mkList ty xs)
2626−
2627−reflectConstant :: Const -> Raw
2628−reflectConstant c@(I _) = reflCall "I" [RConstant c]
2629−reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
2630−reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
2631−reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
2632−reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
2633−reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
2634−reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
2635−reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
2636−reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
2637−reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
2638−reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
2639−reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
2640−reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
2641−reflectConstant StrType = Var (reflm "StrType")
2642−reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
2643−reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
2644−reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
2645−reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
2646−reflectConstant VoidType = Var (reflm "VoidType")
2647−reflectConstant Forgot = Var (reflm "Forgot")
2648−reflectConstant WorldType = Var (reflm "WorldType")
2649−reflectConstant TheWorld = Var (reflm "TheWorld")
2650−
2651−reflectUExp :: UExp -> Raw
2652−reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
2653−reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
2654−
2655−-- | Reflect the environment of a proof into a List (TTName, Binder TT)
2656−reflectEnv :: Env -> Raw
2657−reflectEnv = foldr consToEnvList emptyEnvList
2658− where
2659− consToEnvList :: (Name, Binder Term) -> Raw -> Raw
2660− consToEnvList (n, b) l
2661− = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
2662− [ envTupleType
2663− , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
2664− , (RApp (Var $ reflm "Binder")
2665− (Var $ reflm "TT"))
2666− , reflectName n
2667− , reflectBinder b
2668− ]
2669− , l
2670− ]
2671−
2672− emptyEnvList :: Raw
2673− emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
2674− [envTupleType]
2675−
2676−-- | Reflect an error into the internal datatype of Idris -- TODO
2677−rawBool :: Bool -> Raw
2678−rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
2679−rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
2680−
2681−rawNil :: Raw -> Raw
2682−rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
2683−
2684−rawCons :: Raw -> Raw -> Raw -> Raw
2685−rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
2686−
2687−rawList :: Raw -> [Raw] -> Raw
2688−rawList ty = foldr (rawCons ty) (rawNil ty)
2689−
2690−rawPairTy :: Raw -> Raw -> Raw
2691−rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
2692−
2693−rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
2694−rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
2695−
2696−reflectCtxt :: [(Name, Type)] -> Raw
2697−reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
2698− (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
2699− (reflectName n, reflect t)))
2700− ctxt)
2701−
2702−reflectErr :: Err -> Raw
2703−reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
2704−reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
2705−reflectErr (CantUnify b (t1,_) (t2,_) e ctxt i) =
2706− raw_apply (Var $ reflErrName "CantUnify")
2707− [ rawBool b
2708− , reflect t1
2709− , reflect t2
2710− , reflectErr e
2711− , reflectCtxt ctxt
2712− , RConstant (I i)]
2713−reflectErr (InfiniteUnify n tm ctxt) =
2714− raw_apply (Var $ reflErrName "InfiniteUnify")
2715− [ reflectName n
2716− , reflect tm
2717− , reflectCtxt ctxt
2718− ]
2719−reflectErr (CantConvert t t' ctxt) =
2720− raw_apply (Var $ reflErrName "CantConvert")
2721− [ reflect t
2722− , reflect t'
2723− , reflectCtxt ctxt
2724− ]
2725−reflectErr (CantSolveGoal t ctxt) =
2726− raw_apply (Var $ reflErrName "CantSolveGoal")
2727− [ reflect t
2728− , reflectCtxt ctxt
2729− ]
2730−reflectErr (UnifyScope n n' t ctxt) =
2731− raw_apply (Var $ reflErrName "UnifyScope")
2732− [ reflectName n
2733− , reflectName n'
2734− , reflect t
2735− , reflectCtxt ctxt
2736− ]
2737−reflectErr (CantInferType str) =
2738− raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
2739−reflectErr (NonFunctionType t t') =
2740− raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
2741−reflectErr (NotEquality t t') =
2742− raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
2743−reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
2744−reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
2745−reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
2746−reflectErr (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
2747−reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
2748−reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
2749−reflectErr (NotInjective t1 t2 t3) =
2750− raw_apply (Var $ reflErrName "NotInjective")
2751− [ reflect t1
2752− , reflect t2
2753− , reflect t3
2754− ]
2755−reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
2756−reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
2757−reflectErr (CantResolveAlts ss) =
2758− raw_apply (Var $ reflErrName "CantResolveAlts")
2759− [rawList (Var $ reflm "TTName") (map reflectName ss)]
2760−reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
2761−reflectErr (NoEliminator str t)
2762− = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),
2763− reflect t]
2764−reflectErr UniverseError = Var $ reflErrName "UniverseError"
2765−reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
2766−reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
2767−reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
2768−reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
2769−reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
2770−reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
2771−reflectErr (ProviderError str) =
2772− raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
2773−reflectErr (LoadingFailed str err) =
2774− raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2775−reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2776−
2777−-- | Reflect a file context
2778−reflectFC :: FC -> Raw
2779−reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2780− [ RConstant (Str (fc_fname fc))
2781− , raw_apply (Var pairCon) $
2782− [intTy, intTy] ++
2783− map (RConstant . I)
2784− [ fst (fc_start fc)
2785− , snd (fc_start fc)
2786− ]
2787− , raw_apply (Var pairCon) $
2788− [intTy, intTy] ++
2789− map (RConstant . I)
2790− [ fst (fc_end fc)
2791− , snd (fc_end fc)
2792− ]
2793− ]
2794− where intTy = RConstant (AType (ATInt ITNative))
27952019
27962020elaboratingArgErr :: [(Name, Name)] -> Err -> Err
27972021elaboratingArgErr [] err = err
@@ -2863,88 +2087,4 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
28632087 [] -> e
28642088 parts -> ReflectionError errorparts e
28652089
2866−fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
2867−fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)
2868− | just == txt "Just" = Just tm
2869−fromTTMaybe x = Nothing
2870−
2871−reflErrName :: String -> Name
2872−reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
2873−
2874−-- | Attempt to reify a report part from TT to the internal
2875−-- representation. Not in Idris or ElabD monads because it should be usable
2876−-- from either.
2877−reifyReportPart :: Term -> Either Err ErrorReportPart
2878−reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
2879− Right (TextPart msg)
2880−reifyReportPart (App (P (DCon _ _ _) n _) ttn)
2881− | n == reflm "NamePart" =
2882− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of
2883− Error e -> Left . InternalMsg $
2884− "could not reify name term " ++
2885− show ttn ++
2886− " when reflecting an error:" ++ show e
2887− OK (n', _)-> Right $ NamePart n'
2888−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2889− | n == reflm "TermPart" =
2890− case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of
2891− Error e -> Left . InternalMsg $
2892− "could not reify reflected term " ++
2893− show tm ++
2894− " when reflecting an error:" ++ show e
2895− OK (tm', _) -> Right $ TermPart tm'
2896−reifyReportPart (App (P (DCon _ _ _) n _) tm)
2897− | n == reflm "SubReport" =
2898− case unList tm of
2899− Just xs -> do subParts <- mapM reifyReportPart xs
2900− Right (SubReport subParts)
2901− Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
2902−reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
2903−
2904−reifyTyDecl :: Term -> ElabD RTyDecl
2905−reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)
2906− | n == tacN "Declare" =
2907− do tyN' <- reifyTTName tyN
2908− args' <- case unList args of
2909− Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
2910− Just xs -> mapM reifyRArg xs
2911− ret' <- reifyRaw ret
2912− return $ RDeclare tyN' args' ret'
2913− where reifyRArg :: Term -> ElabD RArg
2914− reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)
2915− | n == tacN "Explicit" = liftM2 RExplicit
2916− (reifyTTName argN)
2917− (reifyRaw argTy)
2918− | n == tacN "Implicit" = liftM2 RImplicit
2919− (reifyTTName argN)
2920− (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint
2921− (reifyTTName argN)
2922− (reifyRaw argTy)
2923− reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."
2924−reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
2925−
2926−reifyFunDefn :: Term -> ElabD RFunDefn
2927−reifyFunDefn (App (App (P _ n _) fnN) clauses)
2928− | n == tacN "DefineFun" =
2929− do fnN' <- reifyTTName fnN
2930− clauses' <- case unList clauses of
2931− Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
2932− Just cs -> mapM reifyC cs
2933− return $ RDefineFun fnN' clauses'
2934− where reifyC :: Term -> ElabD RFunClause
2935− reifyC (App (App (P (DCon _ _ _) n _) lhs) rhs)
2936− | n == tacN "MkFunClause" = liftM2 RMkFunClause
2937− (reifyRaw lhs)
2938− (reifyRaw rhs)
2939− reifyC (App (P (DCon _ _ _) n _) lhs)
2940− | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
2941− reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
2942−reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
2943−
2944−envTupleType :: Raw
2945−envTupleType
2946− = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
2947− , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
2948− ]
2949−
29502090solveAll = try (do solve; solveAll) (return ())