Changes between Version 42 and Version 43 of Holes

Aug 5, 2012 9:59:29 PM (3 years ago)

How should holes interact with with GHC API?


  • Holes

    v42 v43  
    393393    In the definition of `main': main = _?x >>= return
     396= API access to Holes =
     398Another open question is how to
     399programmatically get information back from GHC. It seems that so far we are
     400just thinking about printing a warning message from the compiler. But in order
     401to write something like Agda-mode, I guess we ultimately want to expose this in
     402the GHC API, so programs like [ghc-mod
     403 ghc-mod] can display
     404the holes information and let the user move between them.
     406This seems tricky since it doesn't fit completely with the way the GHC API is
     407currently set up. I think there are two options:
     4091. Treat them like warning messages are currently handled, and extend the
     410"listener" callback which gets called during compilation to have messages about
     411holes as well as warnings in general.
     413However, this is not very uniform: the list of holes in a module is
     414more similar to the list of top-level bindings in the modules, so the API for
     415querying them should be similar.
     4172. Treat them like top-level bindings, and have a set of methods for querying
     418them that way.
     420Currently, GHC is set up so that each time you compile a module a .hi is
     421generated, and all the API methods for querying for module information looks at
     422the .hi file. So this alternative entails modifying the .hi file format to also
     423have a section about holes.
     425What is the best way to do this?