Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

more typecheck listeners #1362

Merged
merged 1 commit into from
Dec 9, 2024

Conversation

digama0
Copy link
Contributor

@digama0 digama0 commented Dec 7, 2024

Continuation of #1346. Adds typecheck listeners for

  • pretype elaboration, i.e. “:type” and Type foo = ...
  • Definition elaboration
  • Datatype elaboration
    • This also has a parse listener because simple datatypes skip the typechecker

@digama0 digama0 force-pushed the typecheck_listener branch from 20701d0 to 83fe3be Compare December 7, 2024 05:28
@mn200
Copy link
Member

mn200 commented Dec 9, 2024

I think the codebase should make it easy for multiple listeners to coincide in the one "slot". Could perhaps have

signature listener = 
sig
 
   type 'a t
   val add_listener : 'a t -> (string * ('a -> unit)) -> unit
   val remove_listener : 'a t -> string -> unit
   val current_listeners : 'a t -> (string * ('a -> unit)) list
end

which would be implemented with a ref to a list of listener functions (of type 'a -> unit)
You might then use with

signature foo = sig
  ...
  val event_listener : eventtype listener.t

end

We avoid exposing the implementation as refs, and stop people from foolishly dumping over existing entries.

@mn200
Copy link
Member

mn200 commented Dec 9, 2024

Happy to merge as is for the moment anyway.

@mn200 mn200 merged commit 46ee6e9 into HOL-Theorem-Prover:develop Dec 9, 2024
4 checks passed
mn200 added a commit that referenced this pull request Dec 9, 2024
Thanks to discussion with Mario Carneiro on github pull request #1362
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants