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

Num from to string #401

Merged
merged 4 commits into from
Jan 19, 2018
Merged

Num from to string #401

merged 4 commits into from
Jan 19, 2018

Conversation

agomezl
Copy link
Contributor

@agomezl agomezl commented Dec 5, 2017

Resolves: #342

@agomezl agomezl requested a review from xrchz December 5, 2017 12:58
agomezl
agomezl commented Dec 5, 2017
View reviewed changes
characteristic/cfNormaliseScript.sml
@@ -158,7 +158,7 @@ val dest_opapp_size = Q.prove(

val get_name_aux_def = tDefine "get_name_aux" `
get_name_aux n vs =
let v = "t" ++ num_to_dec_string n in
let v = "t" ++ num_toString n in
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is just a comment

xrchz
xrchz approved these changes Dec 6, 2017
View reviewed changes
Copy link
Member

@xrchz xrchz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking good at a quick glance.

@xrchz
Copy link
Member

xrchz commented Dec 6, 2017

In case you didn't see, this failed the regression test.

agomezl
agomezl commented Dec 7, 2017
View reviewed changes
compiler/backend/displayLangScript.sml
@@ -20,7 +20,7 @@ val sExp_size_def = fetch "-" "sExp_size_def";

(* display_to_json *)
val num_to_json_def = Define`
num_to_json n = String (explode (toString (&n)))`;
num_to_json n = String (explode (toString n))`;
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Damn you type-inference!!

@xrchz
Copy link
Member

xrchz commented Dec 11, 2017

I'm closing this while it's failing the regression test. Re-open when fixed.

@xrchz xrchz closed this Dec 11, 2017
@agomezl
Copy link
Contributor Author

agomezl commented Dec 21, 2017

I think we are safe now (Sorry, took me a while to realize I hadn't push my changes)

@agomezl agomezl reopened this Dec 21, 2017
@agomezl
Copy link
Contributor Author

agomezl commented Dec 21, 2017

@xrchz I'm not sure if the build system will re-run this

@xrchz
Copy link
Member

xrchz commented Dec 22, 2017

As you can see, it has run and failed.

@xrchz
Copy link
Member

xrchz commented Dec 22, 2017

(Reopen when the above failure is fixed.)

@xrchz xrchz closed this Dec 22, 2017
@xrchz
Copy link
Member

xrchz commented Dec 29, 2017

Does this replace #379 btw?

@xrchz
Copy link
Member

xrchz commented Jan 4, 2018

@agomezl are you still working on this?

@agomezl
Copy link
Contributor Author

agomezl commented Jan 4, 2018

@xrchz yes, this PR does replace #379, I opened a new one since there is a current issue with github that does not allow to reopen PRs if the original reference is no longer an ancestor of the branch used in the PR (Basically no force pushes)

I have now found a work around for that, sorry for the duplication.

@agomezl
Copy link
Contributor Author

agomezl commented Jan 4, 2018

I updated and rebased my branch, and was able to reproduce the error, I'm currently trying to figure where this comes from:

error in load wordfreqCompileScript : 
HOL_ERR {message = "not terminated by EMPTYSTRING"
                  , origin_function = "dest_string_lit"
                  , origin_structure = "Literal"}

since I didn't change anything inside tutorial/. My best guess is some error with the overloading of toString between mlintTheory and mlnumTheory

@agomezl
Add Num.fromString and Num.toString
972c2f1 
  Issue: CakeML#342
@agomezl
Add custom v_thm for num_to_dec_string
982c01e 
  Issue: CakeML#342
@agomezl
Refactor mlnum$toString and mlnum$fromString use
b7d0350 
  * Replace several instances of `mlint$toString (&(n:num))`
    for more concise `mlnum$toString (n:num)`

  * Other minor fixes to various theories

  Issue: CakeML#342
@agomezl
Update diffTheory to use mlnumTheory
1784c16 
  Solves CakeML#342
@agomezl
Copy link
Contributor Author

agomezl commented Jan 18, 2018

After quite some fiddling, I thing I finally solved this issue.

@agomezl agomezl reopened this Jan 18, 2018
agomezl
agomezl commented Jan 18, 2018
View reviewed changes
basis/pure/basisComputeLib.sml
mlnumTheory.toString_def,
mlnumTheory.num_toString_def,
mlnumTheory.fromString_def,
mlnumTheory.fromString_unsafe_def
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The lack of these definitions was the main culprit of the whole "not terminated by EMPTYSTRING" issue

@xrchz xrchz merged commit f8dd05a into CakeML:master Jan 19, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@xrchz xrchz xrchz approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@agomezl @xrchz