0 | module TTImp.Elab.Dot
 1 |
 2 | import Core.Env
 3 | import Core.Metadata
 4 | import Core.UnifyState
 5 |
 6 | import Idris.REPL.Opts
 7 | import Idris.Syntax
 8 |
 9 | import TTImp.Elab.Check
10 | import TTImp.TTImp
11 |
12 | %default covering
13 |
14 | export
15 | registerDot : {vars : _} ->
16 |               {auto c : Ref Ctxt Defs} ->
17 |               {auto u : Ref UST UState} ->
18 |               RigCount -> Env Term vars ->
19 |               FC -> DotReason ->
20 |               Term vars -> Glued vars ->
21 |               Core (Term vars, Glued vars)
22 | registerDot rig env fc reason wantedTm gexpty
23 |     = do nm <- genName "dotTm"
24 |          expty <- getTerm gexpty
25 |          metaval <- metaVar fc rig env nm expty
26 |          addDot fc env nm wantedTm reason metaval
27 |          let tm = case reason of
28 |                     UserDotted => Erased fc (Dotted metaval)
29 |                     _ => metaval
30 |          pure (tm, gexpty)
31 |
32 | export
33 | checkDot : {vars : _} ->
34 |            {auto c : Ref Ctxt Defs} ->
35 |            {auto m : Ref MD Metadata} ->
36 |            {auto u : Ref UST UState} ->
37 |            {auto e : Ref EST (EState vars)} ->
38 |            {auto s : Ref Syn SyntaxInfo} ->
39 |            {auto o : Ref ROpts REPLOpts} ->
40 |            RigCount -> ElabInfo ->
41 |            NestedNames vars -> Env Term vars ->
42 |            FC -> DotReason -> RawImp -> Maybe (Glued vars) ->
43 |            Core (Term vars, Glued vars)
44 | checkDot rig elabinfo nest env fc reason tm Nothing
45 |     = throw (GenericMsg fc ("Dot pattern not valid here (unknown type) "
46 |                             ++ show tm))
47 | checkDot rig elabinfo nest env fc reason tm (Just gexpty)
48 |     = case elabMode elabinfo of
49 |         InLHS _ =>
50 |           do (wantedTm, wantedTy) <- check rig
51 |                                               ({ elabMode := InExpr }
52 |                                                   elabinfo)
53 |                                               nest env
54 |                                               tm (Just gexpty)
55 |              registerDot rig env fc reason wantedTm gexpty
56 |         _ => throw (GenericMsg fc ("Dot pattern not valid here (Not LHS) "
57 |                                    ++ show tm))
58 |