0 | module TTImp.Elab.As
 1 |
 2 | import Core.Env
 3 | import Core.Metadata
 4 | import Core.Unify
 5 |
 6 | import Idris.REPL.Opts
 7 | import Idris.Syntax
 8 |
 9 | import TTImp.Elab.Check
10 | import TTImp.Elab.ImplicitBind
11 | import TTImp.TTImp
12 |
13 | %default covering
14 |
15 | export
16 | checkAs : {vars : _} ->
17 |           {auto c : Ref Ctxt Defs} ->
18 |           {auto m : Ref MD Metadata} ->
19 |           {auto u : Ref UST UState} ->
20 |           {auto e : Ref EST (EState vars)} ->
21 |           {auto s : Ref Syn SyntaxInfo} ->
22 |           {auto o : Ref ROpts REPLOpts} ->
23 |           RigCount -> ElabInfo ->
24 |           NestedNames vars -> Env Term vars ->
25 |           FC -> (nameFC : FC) -> UseSide -> Name -> RawImp -> Maybe (Glued vars) ->
26 |           Core (Term vars, Glued vars)
27 | checkAs rig elabinfo nest env fc nameFC side n_in pat topexp
28 |     = do let elabmode = elabMode elabinfo
29 |          let InLHS _ = elabmode
30 |              | _ => do log "elab.as" 2 $ "Bad @-pattern " ++ show pat
31 |                        throw (GenericMsg fc "@-patterns only allowed in pattern clauses")
32 |          est <- get EST
33 |          let n = PV n_in (defining est)
34 |          noteLHSPatVar elabmode n_in
35 |          notePatVar n
36 |          case lookup n (boundNames est) of
37 |               Nothing =>
38 |                  do (pattm, patty) <- check rigPat elabinfo nest env pat topexp
39 |                     (tm, exp, bty) <- mkPatternHole nameFC rig n env
40 |                                             (implicitMode elabinfo)
41 |                                             topexp
42 |                     log "elab.as" 5 $ "Added as pattern name " ++ show (n, (rigAs, tm, exp, bty))
43 |                     defs <- get Ctxt
44 |                     update EST { boundNames $= ((n, AsBinding rigAs Explicit tm exp pattm) :: ),
45 |                                  toBind $= ((n, AsBinding rigAs Explicit tm bty pattm) ::) }
46 |                     (ntm, nty) <- checkExp rig elabinfo env nameFC tm (gnf env exp)
47 |                                            (Just patty)
48 |
49 |                     -- Add the name type to the metadata
50 |                     log "metadata.names" 7 $ "checkAs is adding ↓"
51 |                     addNameType nameFC n_in env !(getTerm nty)
52 |
53 |                     pure (As fc side ntm pattm, patty)
54 |               Just bty => throw (NonLinearPattern fc n_in)
55 |   where
56 |     -- Only one side can be usable if it's linear! Normally we'd assume this
57 |     -- to be the new variable (UseRight), but in generated case blocks it's
58 |     -- better if it's the pattern (UseLeft)
59 |     rigPat' : UseSide -> RigCount
60 |     rigPat' UseLeft = if isLinear rig then linear else rig
61 |     rigPat' UseRight = if isLinear rig then erased else rig
62 |
63 |     rigPat : RigCount
64 |     rigPat = rigPat' side
65 |
66 |     rigAs' : UseSide -> RigCount
67 |     rigAs' UseLeft = if isLinear rig then erased else rig
68 |     rigAs' UseRight = if isLinear rig then linear else rig
69 |
70 |     rigAs : RigCount
71 |     rigAs = rigAs' side
72 |