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?