@@ -35,10 +35,10 @@ toplevel = EInfo [] emptyContext id Nothing
36-- Also find deferred names in the term and their types
36-- Also find deferred names in the term and their types
38−build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
38+build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
39 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
39 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
40−build ist info pattern fn tm
40+build ist info pattern opts fn tm
41− = do elab ist info pattern False fn tm
41+ = do elab ist info pattern opts fn tm
42 ivs <- get_instances
42 ivs <- get_instances
43 hs <- get_holes
43 hs <- get_holes
44 ptm <- get_term
44 ptm <- get_term
@@ -75,10 +75,10 @@ build ist info pattern fn tm
75-- (Separate, so we don't go overboard resolving things that we don't
75-- (Separate, so we don't go overboard resolving things that we don't
76-- know about yet on the LHS of a pattern def)
76-- know about yet on the LHS of a pattern def)
78−buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
78+buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
79 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
79 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
80−buildTC ist info pattern tcgen fn tm
80+buildTC ist info pattern opts fn tm
81− = do elab ist info pattern tcgen fn tm
81+ = do elab ist info pattern opts fn tm
82 probs <- get_probs
82 probs <- get_probs
83 tm <- get_term
83 tm <- get_term
84 case probs of
84 case probs of
@@ -94,19 +94,22 @@ buildTC ist info pattern tcgen fn tm
94-- Returns the set of declarations we need to add to complete the definition
94-- Returns the set of declarations we need to add to complete the definition
95-- (most likely case blocks to elaborate)
95-- (most likely case blocks to elaborate)
97−elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
97+elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
99−elab ist info pattern tcgen fn tm
99+elab ist info pattern opts fn tm
100 = do let loglvl = opt_logLevel (idris_options ist)
100 = do let loglvl = opt_logLevel (idris_options ist)
101 when (loglvl > 5) $ unifyLog True
101 when (loglvl > 5) $ unifyLog True
102 compute -- expand type synonyms, etc
102 compute -- expand type synonyms, etc
103− elabE (False, False) tm -- (in argument, guarded)
103+ elabE (False, False, False) tm -- (in argument, guarded, in type)
104 end_unify
104 end_unify
105 when pattern -- convert remaining holes to pattern vars
105 when pattern -- convert remaining holes to pattern vars
106 (do update_term orderPats
106 (do update_term orderPats
107 tm <- get_term
107 tm <- get_term
110+ tcgen = Dictionary `elem` opts
111+ reflect = Reflection `elem` opts
110 isph arg = case getTm arg of
113 isph arg = case getTm arg of
111 Placeholder -> (True, priority arg)
114 Placeholder -> (True, priority arg)
112 _ -> (False, priority arg)
115 _ -> (False, priority arg)
@@ -125,6 +128,7 @@ elab ist info pattern tcgen fn tm
125 (h: hs) -> do patvar h; mkPat
128 (h: hs) -> do patvar h; mkPat
126 [] -> return ()
129 [] -> return ()
131+ elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
128 elabE ina t = {- do g <- goal
132 elabE ina t = {- do g <- goal
129 tm <- get_term
133 tm <- get_term
130 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
134 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
@@ -144,9 +148,18 @@ elab ist info pattern tcgen fn tm
145 local f = do e <- get_env
149 local f = do e <- get_env
146 return (f `elem` map fst e)
150 return (f `elem` map fst e)
152+ constType (AType _) = True
153+ constType StrType = True
154+ constType PtrType = True
155+ constType VoidType = True
148 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
158 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
149 elab' ina PType = do apply RType []; solve
159 elab' ina PType = do apply RType []; solve
160+ elab' (_,_,inty) (PConstant c)
161+ | constType c && pattern && not reflect && not inty
162+ = lift $ tfail (Msg "Typecase is not allowed")
150 elab' ina (PConstant c) = do apply (RConstant c) []; solve
163 elab' ina (PConstant c) = do apply (RConstant c) []; solve
151 elab' ina (PQuote r) = do fill r; solve
164 elab' ina (PQuote r) = do fill r; solve
152 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
165 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
@@ -168,13 +181,13 @@ elab ist info pattern tcgen fn tm
168 [pimp (MN 0 "a") Placeholder True,
181 [pimp (MN 0 "a") Placeholder True,
169 pimp (MN 0 "b") Placeholder False,
182 pimp (MN 0 "b") Placeholder False,
170 pexp l, pexp r])
183 pexp l, pexp r])
171− elab' ina@(_, a) (PPair fc l r)
184+ elab' ina@(_, a, inty) (PPair fc l r)
172 = do hnf_compute
185 = do hnf_compute
173 g <- goal
186 g <- goal
174 case g of
187 case g of
175− TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)
188+ TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
176− [pexp l,pexp r])
189+ [pexp l,pexp r])
177− _ -> elabE (True, a) (PApp fc (PRef fc pairCon)
190+ _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
178 [pimp (MN 0 "A") Placeholder True,
191 [pimp (MN 0 "A") Placeholder True,
179 pimp (MN 0 "B") Placeholder True,
192 pimp (MN 0 "B") Placeholder True,
180 pexp l, pexp r])
193 pexp l, pexp r])
@@ -222,7 +235,10 @@ elab ist info pattern tcgen fn tm
222 trySeq' deferr (x : xs)
235 trySeq' deferr (x : xs)
223 = try' (elab' ina x) (trySeq' deferr xs) True
236 = try' (elab' ina x) (trySeq' deferr xs) True
224 elab' ina (PPatvar fc n) | pattern = patvar n
237 elab' ina (PPatvar fc n) | pattern = patvar n
238+ elab' (_, _, inty) (PRef fc f)
239+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
240+ = lift $ tfail (Msg "Typecase is not allowed")
225− elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
241+ elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
226 = do ctxt <- get_context
242 = do ctxt <- get_context
227 let defined = case lookupTy n ctxt of
243 let defined = case lookupTy n ctxt of
228 [] -> False
244 [] -> False
@@ -239,7 +255,7 @@ elab ist info pattern tcgen fn tm
239 _ -> True
255 _ -> True
240 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
256 elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
241 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
257 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
242− elab' ina@(_, a) (PLam n Placeholder sc)
258+ elab' ina@(_, a, inty) (PLam n Placeholder sc)
243 = do -- n' <- unique_hole n
259 = do -- n' <- unique_hole n
244 -- let sc' = mapPT (repN n n') sc
260 -- let sc' = mapPT (repN n n') sc
245 ptm <- get_term
261 ptm <- get_term
@@ -247,10 +263,10 @@ elab ist info pattern tcgen fn tm
247 checkPiGoal n
263 checkPiGoal n
248 attack; intro (Just n);
264 attack; intro (Just n);
249 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
265 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
250− elabE (True, a) sc; solve
266+ elabE (True, a, inty) sc; solve
251 where repN n n' (PRef fc x) | x == n' = PRef fc n'
267 where repN n n' (PRef fc x) | x == n' = PRef fc n'
252 repN _ _ t = t
268 repN _ _ t = t
253− elab' ina@(_, a) (PLam n ty sc)
269+ elab' ina@(_, a, inty) (PLam n ty sc)
254 = do hsin <- get_holes
270 = do hsin <- get_holes
255 ptmin <- get_term
271 ptmin <- get_term
256 tyn <- unique_hole (MN 0 "lamty")
272 tyn <- unique_hole (MN 0 "lamty")
@@ -265,12 +281,12 @@ elab ist info pattern tcgen fn tm
265 introTy (Var tyn) (Just n)
281 introTy (Var tyn) (Just n)
266 -- end_unify
282 -- end_unify
267 focus tyn
283 focus tyn
268− elabE (True, a) ty
284+ elabE (True, a, True) ty
269− elabE (True, a) sc
285+ elabE (True, a, inty) sc
271− elab' ina@(_,a) (PPi _ n Placeholder sc)
287+ elab' ina@(_, a, _) (PPi _ n Placeholder sc)
272− = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve
288+ = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve
273− elab' ina@(_,a) (PPi _ n ty sc)
289+ elab' ina@(_, a, _) (PPi _ n ty sc)
274 = do attack; tyn <- unique_hole (MN 0 "ty")
290 = do attack; tyn <- unique_hole (MN 0 "ty")
275 claim tyn RType
291 claim tyn RType
276 n' <- case n of
292 n' <- case n of
@@ -278,10 +294,10 @@ elab ist info pattern tcgen fn tm
278 _ -> return n
294 _ -> return n
279 forall n' (Var tyn)
295 forall n' (Var tyn)
280 focus tyn
296 focus tyn
281− elabE (True, a) ty
297+ elabE (True, a, True) ty
282− elabE (True, a) sc
298+ elabE (True, a, True) sc
284− elab' ina@(_,a) (PLet n ty val sc)
300+ elab' ina@(_, a, inty) (PLet n ty val sc)
285 = do attack;
301 = do attack;
286 tyn <- unique_hole (MN 0 "letty")
302 tyn <- unique_hole (MN 0 "letty")
287 claim tyn RType
303 claim tyn RType
@@ -293,17 +309,17 @@ elab ist info pattern tcgen fn tm
293 Placeholder -> return ()
309 Placeholder -> return ()
294 _ -> do focus tyn
310 _ -> do focus tyn
295 explicit tyn
311 explicit tyn
296− elabE (True, a) ty
312+ elabE (True, a, True) ty
297 focus valn
313 focus valn
298− elabE (True, a) val
314+ elabE (True, a, True) val
299 env <- get_env
315 env <- get_env
300− elabE (True, a) sc
316+ elabE (True, a, inty) sc
301 -- HACK: If the name leaks into its type, it may leak out of
317 -- HACK: If the name leaks into its type, it may leak out of
302 -- scope outside, so substitute in the outer scope.
318 -- scope outside, so substitute in the outer scope.
303 expandLet n (case lookup n env of
319 expandLet n (case lookup n env of
304 Just (Let t v) -> v)
320 Just (Let t v) -> v)
306− elab' ina@(_,a) (PGoal fc r n sc) = do
322+ elab' ina@(_, a, inty) (PGoal fc r n sc) = do
307 rty <- goal
323 rty <- goal
309 tyn <- unique_hole (MN 0 "letty")
325 tyn <- unique_hole (MN 0 "letty")
@@ -312,10 +328,10 @@ elab ist info pattern tcgen fn tm
312 claim valn (Var tyn)
328 claim valn (Var tyn)
313 letbind n (Var tyn) (Var valn)
329 letbind n (Var tyn) (Var valn)
314 focus valn
330 focus valn
315− elabE (True, a) (PApp fc r [pexp (delab ist rty)])
331+ elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
316 env <- get_env
332 env <- get_env
317 computeLet n
333 computeLet n
318− elabE (True, a) sc
334+ elabE (True, a, inty) sc
320-- elab' ina (PLet n Placeholder
336-- elab' ina (PLet n Placeholder
321-- (PApp fc r [pexp (delab ist rty)]) sc)
337-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -365,14 +381,17 @@ elab ist info pattern tcgen fn tm
365 Just xs@(_:_) -> NS n xs
381 Just xs@(_:_) -> NS n xs
368− elab' (ina, g) (PMatchApp fc fn)
384+ elab' ina (PMatchApp fc fn)
369 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
385 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
370 [(n, args)] -> return (n, map (const True) args)
386 [(n, args)] -> return (n, map (const True) args)
371 _ -> lift $ tfail (NoSuchVariable fn)
387 _ -> lift $ tfail (NoSuchVariable fn)
372 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
388 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
390+ elab' (_, _, inty) (PApp fc (PRef _ f) args')
391+ | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
392+ = lift $ tfail (Msg "Typecase is not allowed")
374 -- if f is local, just do a simple_app
393 -- if f is local, just do a simple_app
375− elab' (ina, g) tm@(PApp fc (PRef _ f) args')
394+ elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args')
376 = do let args = {- case lookupCtxt f (inblock info) of
395 = do let args = {- case lookupCtxt f (inblock info) of
377 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
396 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
378 _ -> -} args'
397 _ -> -} args'
@@ -380,8 +399,8 @@ elab ist info pattern tcgen fn tm
380 env <- get_env
399 env <- get_env
381 if (f `elem` map fst env && length args' == 1)
400 if (f `elem` map fst env && length args' == 1)
382 then -- simple app, as below
401 then -- simple app, as below
383− do simple_app (elabE (ina, g) (PRef fc f))
402+ do simple_app (elabE (ina, g, inty) (PRef fc f))
384− (elabE (True, g) (getTm (head args')))
403+ (elabE (True, g, inty) (getTm (head args')))
385 (show tm)
404 (show tm)
@@ -405,7 +424,7 @@ elab ist info pattern tcgen fn tm
405 sortBy (\(_,x) (_,y) ->
424 sortBy (\(_,x) (_,y) ->
406 compare (priority x) (priority y))
425 compare (priority x) (priority y))
407 (zip ns args)
426 (zip ns args)
408− elabArgs (ina || not isinf, guarded)
427+ elabArgs (ina || not isinf, guarded, inty)
409 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
428 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)
410 mkSpecialised ist fc f (map getTm args') tm
429 mkSpecialised ist fc f (map getTm args') tm
@@ -436,9 +455,9 @@ elab ist info pattern tcgen fn tm
436 setInjective (PApp _ (PRef _ n) _) = setinj n
455 setInjective (PApp _ (PRef _ n) _) = setinj n
437 setInjective _ = return ()
456 setInjective _ = return ()
439− elab' ina@(_, a) tm@(PApp fc f [arg])
458+ elab' ina@(_, a, inty) tm@(PApp fc f [arg])
440 = erun fc $
459 = erun fc $
441− do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
460+ do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
442 (show tm)
461 (show tm)
444 elab' ina Placeholder = do (h : hs) <- get_holes
463 elab' ina Placeholder = do (h : hs) <- get_holes
@@ -487,7 +506,7 @@ elab ist info pattern tcgen fn tm
487 elab' ina sc
506 elab' ina sc
488 elab' ina (PRef fc letn)
507 elab' ina (PRef fc letn)
490− elab' ina@(_, a) c@(PCase fc scr opts)
509+ elab' ina@(_, a, inty) c@(PCase fc scr opts)
491 = do attack
510 = do attack
492 tyn <- unique_hole (MN 0 "scty")
511 tyn <- unique_hole (MN 0 "scty")
493 claim tyn RType
512 claim tyn RType
@@ -496,7 +515,7 @@ elab ist info pattern tcgen fn tm
496 claim valn (Var tyn)
515 claim valn (Var tyn)
497 letbind scvn (Var tyn) (Var valn)
516 letbind scvn (Var tyn) (Var valn)
498 focus valn
517 focus valn
499− elabE (True, a) scr
518+ elabE (True, a, inty) scr
500 args <- get_env
519 args <- get_env
501 cname <- unique_hole' True (mkCaseName fn)
520 cname <- unique_hole' True (mkCaseName fn)
502 let cname' = mkN cname
521 let cname' = mkN cname
@@ -679,9 +698,9 @@ findInstances ist t
679 | otherwise = []
698 | otherwise = []
681trivial' ist
700trivial' ist
682− = trivial (elab ist toplevel False False (MN 0 "tac")) ist
701+ = trivial (elab ist toplevel False [] (MN 0 "tac")) ist
683proofSearch' ist top n hints
702proofSearch' ist top n hints
684− = proofSearch (elab ist toplevel False False (MN 0 "tac")) top n hints ist
703+ = proofSearch (elab ist toplevel False [] (MN 0 "tac")) top n hints ist
687resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
706resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
@@ -810,7 +829,7 @@ runTac autoSolve ist tac
811 bname (Bind n _ _) = Just n
830 bname (Bind n _ _) = Just n
812 bname _ = Nothing
831 bname _ = Nothing
813− runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
832+ runT (Exact tm) = do elab ist toplevel False [] (MN 0 "tac") tm
814 when autoSolve solveAll
833 when autoSolve solveAll
815 runT (MatchRefine fn)
834 runT (MatchRefine fn)
816 = do fnimps <-
835 = do fnimps <-
@@ -857,7 +876,7 @@ runTac autoSolve ist tac
857 letn <- unique_hole (MN 0 "equiv_val")
876 letn <- unique_hole (MN 0 "equiv_val")
858 letbind letn (Var tyn) (Var valn)
877 letbind letn (Var tyn) (Var valn)
859 focus tyn
878 focus tyn
860− elab ist toplevel False False (MN 0 "tac") tm
879+ elab ist toplevel False [] (MN 0 "tac") tm
861 focus valn
880 focus valn
862 when autoSolve solveAll
881 when autoSolve solveAll
863 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
882 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
@@ -870,7 +889,7 @@ runTac autoSolve ist tac
870 letn <- unique_hole (MN 0 "rewrite_rule")
889 letn <- unique_hole (MN 0 "rewrite_rule")
871 letbind letn (Var tyn) (Var valn)
890 letbind letn (Var tyn) (Var valn)
872 focus valn
891 focus valn
873− elab ist toplevel False False (MN 0 "tac") tm
892+ elab ist toplevel False [] (MN 0 "tac") tm
874 rewrite (Var letn)
893 rewrite (Var letn)
875 when autoSolve solveAll
894 when autoSolve solveAll
876 runT (Induction nm)
895 runT (Induction nm)
@@ -885,7 +904,7 @@ runTac autoSolve ist tac
885 letn <- unique_hole n
904 letn <- unique_hole n
886 letbind letn (Var tyn) (Var valn)
905 letbind letn (Var tyn) (Var valn)
887 focus valn
906 focus valn
888− elab ist toplevel False False (MN 0 "tac") tm
907+ elab ist toplevel False [] (MN 0 "tac") tm
889 when autoSolve solveAll
908 when autoSolve solveAll
890 runT (LetTacTy n ty tm)
909 runT (LetTacTy n ty tm)
891 = do attack
910 = do attack
@@ -896,9 +915,9 @@ runTac autoSolve ist tac
896 letn <- unique_hole n
915 letn <- unique_hole n
897 letbind letn (Var tyn) (Var valn)
916 letbind letn (Var tyn) (Var valn)
898 focus tyn
917 focus tyn
899− elab ist toplevel False False (MN 0 "tac") ty
918+ elab ist toplevel False [] (MN 0 "tac") ty
900 focus valn
919 focus valn
901− elab ist toplevel False False (MN 0 "tac") tm
920+ elab ist toplevel False [] (MN 0 "tac") tm
902 when autoSolve solveAll
921 when autoSolve solveAll
903 runT Compute = compute
922 runT Compute = compute
904 runT Trivial = do trivial' ist; when autoSolve solveAll
923 runT Trivial = do trivial' ist; when autoSolve solveAll
@@ -916,7 +935,7 @@ runTac autoSolve ist tac
916 scriptvar <- unique_hole (MN 0 "scriptvar" )
935 scriptvar <- unique_hole (MN 0 "scriptvar" )
917 letbind scriptvar scriptTy (Var script)
936 letbind scriptvar scriptTy (Var script)
918 focus script
937 focus script
919− elab ist toplevel False False (MN 0 "tac") tm
938+ elab ist toplevel False [] (MN 0 "tac") tm
920 (script', _) <- get_type_val (Var scriptvar)
939 (script', _) <- get_type_val (Var scriptvar)
921 -- now that we have the script apply
940 -- now that we have the script apply
922 -- it to the reflected goal and context
941 -- it to the reflected goal and context
@@ -949,7 +968,7 @@ runTac autoSolve ist tac
949 letbind scriptvar scriptTy (Var script)
968 letbind scriptvar scriptTy (Var script)
950 focus script
969 focus script
951 ptm <- get_term
970 ptm <- get_term
952− elab ist toplevel False False (MN 0 "tac")
971+ elab ist toplevel False [] (MN 0 "tac")
953 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
972 (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
954 (script', _) <- get_type_val (Var scriptvar)
973 (script', _) <- get_type_val (Var scriptvar)
955 -- now that we have the script apply
974 -- now that we have the script apply
@@ -977,7 +996,7 @@ runTac autoSolve ist tac
977 letn <- unique_hole (MN 0 "letvar")
996 letn <- unique_hole (MN 0 "letvar")
978 letbind letn (Var tyn) (Var valn)
997 letbind letn (Var tyn) (Var valn)
979 focus valn
998 focus valn
980− elab ist toplevel False False (MN 0 "tac") v
999+ elab ist toplevel False [] (MN 0 "tac") v
981 (value, _) <- get_type_val (Var letn)
1000 (value, _) <- get_type_val (Var letn)
982 ctxt <- get_context
1001 ctxt <- get_context
983 env <- get_env
1002 env <- get_env
@@ -991,7 +1010,7 @@ runTac autoSolve ist tac
991 letn <- unique_hole (MN 0 "letvar")
1010 letn <- unique_hole (MN 0 "letvar")
992 letbind letn (Var tyn) (Var valn)
1011 letbind letn (Var tyn) (Var valn)
993 focus valn
1012 focus valn
994− elab ist toplevel False False (MN 0 "tac") v
1013+ elab ist toplevel False [] (MN 0 "tac") v
995 (value, _) <- get_type_val (Var letn)
1014 (value, _) <- get_type_val (Var letn)
996 ctxt <- get_context
1015 ctxt <- get_context
997 env <- get_env
1016 env <- get_env