Changes between Version 42 and Version 43 of Holes


Ignore:
Timestamp:
Aug 5, 2012 9:59:29 PM (3 years ago)
Author:
vilhelm_s
Comment:

How should holes interact with with GHC API?

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v42 v43  
    393393    In the definition of `main': main = _?x >>= return 
    394394}}} 
     395 
     396= API access to Holes = 
     397 
     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 
     403http://www.haskell.org/haskellwiki/Haskell_mode_for_Emacs#ghc-mod ghc-mod] can display 
     404the holes information and let the user move between them. 
     405 
     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: 
     408 
     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. 
     412 
     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. 
     416 
     4172. Treat them like top-level bindings, and have a set of methods for querying 
     418them that way. 
     419 
     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. 
     424 
     425What is the best way to do this?