Initial program from translator #99

Closed
xrchz opened this Issue Feb 3, 2016 · 9 comments

Projects

None yet

3 participants

@myreen myreen added a commit that referenced this issue Aug 4, 2016
@myreen myreen Produce entire basis program with translation and CF
Every binding has either a translator certificate or a CF
verified theorem.

This practically completes #99, but I won't close it
until the old basis program has been deleted and all
its uses have been replaced by this basis program.

Note that currently the basis program has no I/O. This
will be added soon.
0e51b09
@myreen myreen assigned myreen and xrchz and unassigned myreen Aug 4, 2016
@myreen
Contributor
myreen commented Aug 4, 2016

@xrchz could you replace the old basis program with this one?

@xrchz xrchz added a commit that referenced this issue Aug 5, 2016
@xrchz xrchz Attempt to remove initialProgram, in favour of basisProgram
- semantics/initialProgram becomes semantics/primTypes, which still
  defines the primitive types program.
- initSemEnv becomes primSemEnv, and the part for evaluating out the
  basis_program is deleted
- cf_initialProgram and ml_prog_demo deleted (they both relied heavily
  on the defunct basis_program, and are therefore replaced by
  basisProgram)
- somewhat orthogonal change:
    initialProgram$top_state -> semantics$state

Problem:
- cf_example and cf_tutorial no longer work. I have moved them to
  characteristic/examples in order that they can depend on basisProgram,
  but it seems like basisProgram does not provied CF-suitable specs for
  its translated functions.

This is progress on #99
bf9c99e
@xrchz
Member
xrchz commented Aug 5, 2016

@myreen I have attempted to remove the old basis program. The biggest users were in fact the cf and translator examples/demos/tutorials. I have not been able to update the cf examples to use the new basis program: could you take a look at that? See commit message above.

@Armael Armael self-assigned this Aug 5, 2016
@Armael Armael added a commit that referenced this issue Aug 5, 2016
@Armael Armael Make CF able to use specs produced by the translator
This makes progress on #134 and #99, however some unfolding (e.g. for
"plus") still needs to happen somewhere so that
characteristic/examples/* can be run again without modifications.
1a96d39
@Armael
Member
Armael commented Aug 5, 2016

I made some progress in 1a96d39 . CF is now able to use theorems produced by the translator, turning them into cf specs using cfAppLib.app_of_Arrow_rule. However, that is not enough for characteristic/examples/* to be run again without modifying them.

For example, the theorem for plus produced by the translator is:

> basisProgramTheory.plus_v_thm;
val it =
   |- (INT --> INT --> INT) plus plus_v:
   thm

The cf spec that is produced is then:

> cfAppLib.app_of_Arrow_rule basisProgramTheory.plus_v_thm;
val it =
   |- INT x0 v0 ∧ INT x1 v1 ⇒
   app p plus_v [v0; v1] emp (λv. &INT (plus x0 x1) v):
   thm

Previously the (hand-written) specification was directly using + without the plus wrapper, so that's why the examples don't work as they are now.

As it is, this generated spec is also annoying to use: plus is just a wrapper over + so I think we don't really want the user to rewrite with basisProgramTheory.plus_def every time they certify a program that uses + (same with -, etc.).
However, in general, I guess we don't want to unfold the definition of the translated function in the cf-generated spec (especially for recursive functions..).

So some unfolding has to happen, but I don't know exactly where...

@xrchz
Member
xrchz commented Aug 5, 2016

Nice work! I think in general there should not be any unfolding, because usually we have a proper definition being translated. Those basis library wrapper functions are a special case: they are just there to wrap the abstract syntax primitives. I think the CF specs for the translated basis functions should be saved in basisProgramTheory after manually unfolding plus_def etc. for the ones that are simple wrappers.

@Armael
Member
Armael commented Aug 5, 2016

Yes, sounds like a good solution. This should work nicely as cf tactics search first for a proper cf spec, before looking for a theorem from the translator.

@myreen
Contributor
myreen commented Aug 6, 2016

Indeed, nice work!

As Ramana says, the wrappers are a silly side effect of the way the basis program is generated. I suggest that I update the way the translation works in basisProgramScript so that these wrapper functions are removed immediately after each translation in basisProgramScript.

@myreen myreen self-assigned this Aug 6, 2016
@myreen
Contributor
myreen commented Aug 6, 2016

Commit b88d525 removes the wrappers mentioned above.

@myreen myreen removed their assignment Aug 6, 2016
@Armael
Member
Armael commented Aug 6, 2016

And commit 51a161b makes characteristic/examples/* compile again (with only very minor modifications).

@Armael Armael removed their assignment Aug 6, 2016
@xrchz xrchz closed this Aug 6, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment