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

add a command-line shell for LangDef queries #121

Merged
merged 4 commits into from
Mar 8, 2025

Conversation

zerbina
Copy link
Collaborator

@zerbina zerbina commented Mar 6, 2025

Summary

Add a simple command-line shell to query LangDefs with and execute
their functions and relations. The source language is currently
hardcoded as the language to query.

Details

The shell is intended to aid with language development, by providing a
convenient way to test relations and functions with various input.

For ease of implementation, commands are provided as S-expressions.
Result values are also rendered as S-expressions. Constructors for
built-in meta-language terms (e.g., true, false, tuples, etc.) are
prefixed with a colon to distinguish them from user-defined type
constructors.

In addition, to showing the result of a function/relation application,
the shell also shows the interpreter-generated trace of which
relations.

Additional Changes

  • move the line-buffered stream and S-expression parsing implementations
    from the repl to the new sexpstreams module (queryshell also
    needs both)
  • parse colon-prefixed symbols as S-expression symbols in the parse
    iterator, instead of reporting an error
  • collect the used rules in traces generated by the interpreter

zerbina added 4 commits March 6, 2025 15:41
A preparation for the query shell, which also needs the S-expression
stream parsing.
This allows for symbols starting with the `:` character, which is
needed for the query shell.
@zerbina zerbina added the enhancement New feature or request label Mar 6, 2025
@zerbina
Copy link
Collaborator Author

zerbina commented Mar 6, 2025

A showcase of how the output looks like:

> (default C) (set c)
Got: (:rec (symbols (:map)) (ret (VoidTy)))
> (apply types $c (Call (Ident "+") (Call (Ident "+") (IntVal 1) (IntVal 2)) (IntVal 4)))
- types (:rec (symbols (:map)) (ret (VoidTy))) (Call (Ident "+") (Call (Ident "+") (IntVal 1) (IntVal 2)) (IntVal 4)) (IntTy) | S-builtin-plus
  - mtypes (:rec (symbols (:map)) (ret (VoidTy))) (Call (Ident "+") (IntVal 1) (IntVal 2)) (IntTy) | 
    - types (:rec (symbols (:map)) (ret (VoidTy))) (Call (Ident "+") (IntVal 1) (IntVal 2)) (IntTy) | S-builtin-plus
      - mtypes (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 1) (IntTy) | 
        - types (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 1) (IntTy) | S-int
      - mtypes (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 2) (IntTy) | 
        - types (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 2) (IntTy) | S-int
  - mtypes (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 4) (IntTy) | 
    - types (:rec (symbols (:map)) (ret (VoidTy))) (IntVal 4) (IntTy) | S-int
Got: (IntTy)

It's a bit noisy due to the S-expression-based rendering of record/tuple/set/map values.

Possible future improvements:

  • a rendering mode where record/tuple/set/map/values are formatted the same way they're written in the macro DSL (e.g., records as {symbols: {}, ...})
  • tracking the lineage of values and omitting identical ones from the trace
  • user-provided custom formatting for relations (e.g., so that types a b c shows as a |- b : c)

@saem saem merged commit 02ba891 into nim-works:main Mar 8, 2025
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants