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.

Sign up for GitHub

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

Jump to bottom

Compile one argument identity function #10

Merged
merged 27 commits into from
Dec 18, 2023
Merged

Compile one argument identity function #10

merged 27 commits into from
Dec 18, 2023

Conversation

lemastero
Copy link
Owner

@lemastero lemastero commented Dec 15, 2023 •
edited
Loading

Chanes

Handle (non-polymorphic) identity function

  • get result type for function
  • get argument type
  • get argument name

This is simplified version - real solution with multiple arguments should lookup names using deBruijn indices defined in Clause.

I have choose to aggressively throw errors for every missed case - to easier find them.

lemastero added 19 commits December 14, 2023 11:45
test existing code creating moduleHeader
0a6d976
module header is proper Rust comment
c933d1b
fix non-compiling Test.agda example - add test.Test module
8cb8de2
handle module name and brackets
c396f62
handle function name, brackets around body, raw body
ba9da5e
handle data type definition as enum - name, brackets and raw clauses
a361e29
update examples Hello and Test with new handling of functions and dat…
bdb2893 
…a types
simplify Hello.agda enum + function on enum
67c2931
extract functions for hande functions, handle data type, handle module
98afd79
handle enums
08fb589
use bracket, rename handleX to compileX
7e79c28
use bracket, rename handleX to compileX - fix unit tests
8e651fb
use bracket, rename handleX to compileX - fix unit tests 2
b372353
extract PrettyPrintingUtils and ToRustCompiler; common types between …
5136c29 
…ToRustCompiler and Backed are in CommonTypes
add typeSeparator and argList for pretty printing
86fbc17
compile singe argument function - argument name, its argument, functi…
bf114fd 
…on result type and single variable result body
compile singe argument function - add return
61ee734
compile singe argument function - update Hello example
0069f23
compile singe argument function - add comments for further improvements
0c04760
@lemastero lemastero mentioned this pull request Dec 16, 2023
Open
2 tasks
Base automatically changed from produce-rust to master December 17, 2023 23:58
lemastero and others added 7 commits December 18, 2023 02:23
merge from master
e4de243
fix function return types (broke during rebase)
aa6d090
change to lowercase names
fad17ff
remove empty lines
6079bf5
fix use module name instead of first directory
4db314b
@lemastero
RustExpr to separate pretty printing from traverse Agda internals (#18)
2f56f9a 
* add RustExpr to separate pretty printing and creating expression from Agda internals

* rename after refactor to RustExpr

* rename after refactor to RustExpr - fix

* swap unless to when
@lemastero
Revert "RustExpr to separate pretty printing from traverse Agda inter…
5853726 
…nals (#18)" (#19)

This reverts commit 2f56f9a.
@lemastero lemastero merged commit 2e60ae8 into master Dec 18, 2023
1 check passed
@lemastero lemastero deleted the one-arg-id branch December 18, 2023 15:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@lemastero