Skip to content
This repository has been archived by the owner on Sep 7, 2023. It is now read-only.

(feat) stringify to "ergo" syntax #364

Merged
merged 3 commits into from
Aug 3, 2018
Merged

(feat) stringify to "ergo" syntax #364

merged 3 commits into from
Aug 3, 2018

Conversation

kach
Copy link
Contributor

@kach kach commented Aug 3, 2018 

ergo$ define concept Bear {name: String, age: Integer}

ergo$ define constant pooh = Bear {name: "Winnie", age: 4}

ergo$ return pooh;
Response. ~org.accordproject.ergotop.Bear {name: "Winnie", age: 4}
  :  {emit: Unit[], response: ~org.accordproject.ergotop.Bear, state: Unit}?

@kach kach requested a review from jeromesimeon August 3, 2018 16:19
@kach
Copy link
Contributor Author

kach commented Aug 3, 2018

@jeromesimeon

@kach kach mentioned this pull request Aug 3, 2018
Closed
jeromesimeon
jeromesimeon suggested changes Aug 3, 2018
View reviewed changes
mechanization/Common/Utils/EData.v
Fixpoint string_of_data (d : ergo_data) : string :=
let jsonify := ErgoData.data_to_json_string fmt_dq in
let string_of_rec : list (string * ergo_data) -> string :=
fun rec =>
Copy link
Member

Choose a reason for hiding this comment

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

Might want to try String.concat !

Lemma concat_test : String.concat ", " ("a"::"b"::"c"::nil) = "a, b, c".
Proof.
  reflexivity.
Qed.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

okay, okay 72886c3

mechanization/Common/Utils/EData.v Outdated
arr ""%string)
++ "]"%string
| dleft s => "some("%string ++ (string_of_data s) ++ ")"%string
| dright _ => "none"
Copy link
Member

Choose a reason for hiding this comment

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

If so maybe fix ErgoLexer.mll (nil -> none) as well?

Copy link
Member

Choose a reason for hiding this comment

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

See #321

Copy link
Contributor Author

Choose a reason for hiding this comment

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

No, nil is currently unit. #321 needs to be fixed properly on its own.

@kach
Copy link
Contributor Author

kach commented Aug 3, 2018

@jeromesimeon travis is being wonky again, can we just disable that particular test?

@kach
(chore) shhhh
e2abd22 
Signed-off-by: kach <[email protected]>
@kach kach merged commit 0edacfe into master Aug 3, 2018
@kach kach deleted the kc-feat-print branch August 3, 2018 17:05
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jeromesimeon jeromesimeon jeromesimeon requested 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
@kach @jeromesimeon