isaplib

[Lucas Dixon]

Hello, just wondering, if quantomatic is still using the git isaplib repo? I see the last version to be made to work with Isabelle is 2013, I am going to update this for Isabelle 2015 I think. But I wanted to make sure I'm not duplicating work. 

cheers,

lucas

[Aleks Kissinger]

Wow, an unexpected development!

Quantomatic is in fact not running on isaplib anymore. It is designed
to run natively in Isabelle 2014 (for the "stable" and "integration"
branches) and work-in-progress for running in 2015 ("isabelle2015"
branch). The top-level file is "quanto.thy".

Thus there is now a much smaller library which is factored out of
isabelle and lives in the "core/lib" directory. Its most important
bits are the name/maps functors and the JSON stream parser. To build
standalone, it keeps a copy of isabelle's "Pure" directory also in
core. It uses a fairly stupid sed script to turn the top-level
theories into plain ML files (essentially turning every "ML_file"
statement into "use").

So, to summarise, yes, you'd probably be duplicating some effort, and
might be better off to start with "core/lib" from quanto's
"isabelle2015" branch. However, the JSON stream parser is currently
broken and I haven't had time to fix it yet.

> --
> You received this message because you are subscribed to the Google Groups
> "Quantomatic" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to quantomatic...@googlegroups.com.
> To post to this group, send email to quant...@googlegroups.com.
> Visit this group at http://groups.google.com/group/quantomatic.
> For more options, visit https://groups.google.com/d/optout.

[Lucas Dixon]

Thanks! (somewhat belatedly!) 

I actually had no difficulty building isaplib on Isabelle 2015: 

see: https://github.com/iislucas/isaplib/tree/iislucas-isabelle-2015 

I found I could simply remove all the Isabelle code, and make a theory that loaded the relevant files: 

https://github.com/iislucas/isaplib/blob/iislucas-isabelle-2015/isabelle/isaplib/isaplib.thy 

Working on Isabelle 2015 does seem like a much better editing experience. I do miss some of the things I'd hacked, but my old editing environment never really had much love. Does Isabelle's jEdit mode have the ability to select some code and have the editor tell you the type? 

One thing I noticed is that the maps/ directory looks very similar to things still in the names/ directory. There seem to be binary relations, injective relations, injective endos, mappings, and name-tables, for instance. It looks like your newer versions of these are somewhat simpler and cleaner - although I see a bit less about renaming within a structure, maybe you do that by relation-composition? I'm curious about the differences, and pleased to see the simpler interfaces. 

cheers,

lucas

[Aleks Kissinger]

​The new Isabelle2015 environment is quite nice to work in. I assume there are ways you can get to all those poly/ML IDE hooks e.g. to pull the type of some text, but I'm not sure how to do it. The most handy things I find are CTRL+clicking to jump to defs (which of course mainstream languages have had since the 90s in their IDEs) and making a little ML {* *} scratch area in quanto.thy for testing stuff out and getting instant feedback.

Quanto is still using names and NSet, but all the old renamer structures etc have been superceded by the new maps.

​ I didn't ever get around to taking out the old maps, as they were a bit entangled with names and namesets.​

All renaming is done via composition

​, but there are also some helper functions in the map structures designed particularly for renaming​

.

​ For example, extend_fresh extends the domain of a map by sending anything not yet in the domain to something fresh w.r.t. the codomain. Here's an example of renaming in action:

fun rename_bang_graph (vsub,esub,bsub) g = let
  val vrnm  = VSub.extend_fresh (get_vertices g) vsub
  val vrnmi = VSub.inverse_of vrnm
  val ernm  = ESub.extend_fresh (get_edges g) esub
  val ernmi = ESub.inverse_of ernm
  val brnm  = BSub.extend_fresh (get_bboxes g) bsub
  val brnmi = BSub.inverse_of brnm
in
  (
    (vrnm,ernm,brnm),
    g |> update_vdata    (fn m => VTab.compose (m,vrnmi))
      |> update_edata    (fn m => ETab.compose (m,ernmi))
      |> update_source   (fn m => EVFn.compose3 (vrnm,m,ernmi))
      |> update_target   (fn m => EVFn.compose3 (vrnm,m,ernmi))
      |> update_bboxes   (BSub.img_of_set brnm)
      |> update_bbox_rel (fn m => BVRel.compose3 (vrnm, m, brnmi))
      |> update_bbox_child_rel (fn m => BBRel.compose3 (brnm, m, brnmi))
      |> update_v_anno   (fn m => VTab.compose (m,vrnmi))
      |> update_e_anno   (fn m => ETab.compose (m,ernmi))
      |> update_bb_anno  (fn m => BTab.compose (m,brnmi))
  )
end

[Lucas Dixon]

Cool, thanks!

We should make a cleanup issue to remove the old structure... (Done)

I remember there were some odd edge cases that took a while to get right (interactions of avoids sets and domain/codomian or similar).   At one point I thought that the name management work we did was worth a paper because it is actually quite involved and no one else seemed to have done it.