
  0 | module TTImp.Elab.Hole
  1 | 
  2 | import Core.Context.Log
  3 | import Core.Env
  4 | import Core.Metadata
  5 | import Core.Normalise
  6 | import Core.Unify
  7 | import Core.Value
  8 | 
  9 | import TTImp.Elab.Check
 10 | import TTImp.TTImp
 11 | 
 12 | %default covering
 13 | 
 14 | -- If the hole type is itself a hole, mark it as to be solved without
 15 | -- generalising multiplicities so that we get as precise as possible a type
 16 | -- for the hole
 17 | mkPrecise : {auto c : Ref Ctxt Defs} ->
 18 |             NF vars -> Core ()
 19 | mkPrecise (NApp _ (NMeta n i _) _)
 20 |     = updateDef (Resolved i)
 21 |                 (\case
 22 |                     Hole i p => Just (Hole i ({ precisetype := True} p))
 23 |                     d => Nothing)
 24 | mkPrecise _ = pure ()
 25 | 
 26 | export
 27 | checkHole : {vars : _} ->
 28 |             {auto c : Ref Ctxt Defs} ->
 29 |             {auto m : Ref MD Metadata} ->
 30 |             {auto u : Ref UST UState} ->
 31 |             {auto e : Ref EST (EState vars)} ->
 32 |             RigCount -> ElabInfo ->
 33 |             NestedNames vars -> Env Term vars ->
 34 |             FC -> UserName -> Maybe (Glued vars) ->
 35 |             Core (Term vars, Glued vars)
 36 | checkHole rig elabinfo nest env fc n_in (Just gexpty)
 37 |     = do nm <- inCurrentNS (UN n_in)
 38 |          defs <- get Ctxt
 39 |          Nothing <- lookupCtxtExact nm (gamma defs)
 40 |              | _ => do log "elab.hole" 1 $ show nm ++ " already defined"
 41 |                        throw (AlreadyDefined fc nm)
 42 |          expty <- getTerm gexpty
 43 |          -- Turn lets into lambda before making the hole so that they
 44 |          -- get abstracted over in the hole (it's fine here, unlike other
 45 |          -- holes, because we're not trying to unify it so it's okay if
 46 |          -- applying the metavariable isn't a pattern form)
 47 |          let env' = letToLam env
 48 |          (idx, metaval) <- metaVarI fc rig env' nm expty
 49 |          mkPrecise !(getNF gexpty)
 50 |          -- Record the LHS for this hole in the metadata
 51 |          withCurrentLHS (Resolved idx)
 52 |          addNameLoc fc nm
 53 |          addUserHole False nm
 54 |          saveHole nm
 55 |          pure (metaval, gexpty)
 56 | checkHole rig elabinfo nest env fc n_in exp
 57 |     = do nmty <- genName ("type_of_" ++ show n_in)
 58 |          let env' = letToLam env
 59 |          u <- uniVar fc
 60 |          ty <- metaVar fc erased env' nmty (TType fc u)
 61 |          nm <- inCurrentNS (UN n_in)
 62 |          defs <- get Ctxt
 63 |          mkPrecise !(nf defs env' ty)
 64 | 
 65 |          Nothing <- lookupCtxtExact nm (gamma defs)
 66 |              | _ => do log "elab.hole" 1 $ show nm ++ " already defined"
 67 |                        throw (AlreadyDefined fc nm)
 68 |          (idx, metaval) <- metaVarI fc rig env' nm ty
 69 |          withCurrentLHS (Resolved idx)
 70 |          addNameLoc fc nm
 71 |          addUserHole False nm
 72 |          saveHole nm
 73 |          pure (metaval, gnf env ty)
 74 |