[isabelle] Failing to handle a fairly large dataype



Dear Isabelle Community,

I and a graduate student of mine, Liyi Li, have been working on formalizing the K specification language of Grigore Rosu in Isabelle. One of the very first datatypes we have, giving the bulk of the syntax definition for K chokes Isabelle on my machine (MacBook Pro 2.8 GHz Core i7 with 16 GB DDR3 memory). The error message I get is


Welcome to Isabelle/HOL (Isabelle2016-1: December 2016)
Run out of store - interrupting threads

Run out of store - interrupting threads

Failed to recover - exiting

message_output terminated
standard_error terminated
standard_output terminated
process terminated
command_input terminated
process_manager terminated
Return code: 1


The code that is causing the choke is:


datatype ('upVar, 'var, 'svar, 'metaVar) kLabel
     = KLabel 'svar
     | KLabelFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
                 "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
     | IdKLabel 'metaVar
and ('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite
              = KLabelTerm "('upVar, 'var, 'svar, 'metaVar) kLabel"
              | KLabelRewrite "('upVar, 'var, 'svar, 'metaVar) kLabel"
                              "('upVar, 'var, 'svar, 'metaVar) kLabel"
and ('upVar, 'var, 'svar, 'metaVar) kItem =
KItem "('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite" "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
                                              'upVar
                                      | Constant "'var theConstant" 'upVar
                                      | IdKItem "'metaVar" 'upVar
                                      |  HOLE 'upVar
and ('upVar, 'var, 'svar, 'metaVar) kItemWithRewrite
             = KItemTerm "('upVar, 'var, 'svar, 'metaVar) kItem"
             | KItemRewrite "('upVar, 'var, 'svar, 'metaVar) kItem"
                            "('upVar, 'var, 'svar, 'metaVar) kItem"
and ('upVar, 'var, 'svar, 'metaVar) kList =
KListCon "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite" "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
                                 | UnitKList
| KListItem "('upVar, 'var, 'svar, 'metaVar) bigKWithBag"
                                 | IdKList "'metaVar"
and ('upVar, 'var, 'svar, 'metaVar) kListWithRewrite
             = KListTerm "('upVar, 'var, 'svar, 'metaVar) kList"
             | KListRewrite "('upVar, 'var, 'svar, 'metaVar) kList"
                            "('upVar, 'var, 'svar, 'metaVar) kList"
and ('upVar, 'var, 'svar, 'metaVar) bigK = TheK "('upVar, 'var, 'svar, 'metaVar) kWithRewrite" | TheList "('upVar, 'var, 'svar, 'metaVar) theListRewrite" | TheSet "('upVar, 'var, 'svar, 'metaVar) theSetRewrite" | TheMap "('upVar, 'var, 'svar, 'metaVar) theMapRewrite" and ('upVar, 'var, 'svar, 'metaVar) bigKWithBag = TheBigK "('upVar, 'var, 'svar, 'metaVar) bigK" | TheBigBag "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite" | TheLabel "('upVar, 'var, 'svar, 'metaVar) kLabelWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) k
         = Tilda "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
                 "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
| UnitK | IdK 'metaVar | SingleK "('upVar, 'var, 'svar, 'metaVar) kItemWithRewrite"
           | KFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
                  "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) kWithRewrite = KTerm "('upVar, 'var, 'svar, 'metaVar) k" | KRewrite "('upVar, 'var, 'svar, 'metaVar) k" "('upVar, 'var, 'svar, 'metaVar) k"

and ('upVar, 'var, 'svar, 'metaVar) theList = ListCon "('upVar, 'var, 'svar, 'metaVar) theListRewrite" "('upVar, 'var, 'svar, 'metaVar) theListRewrite"
                                    | UnitList
                                    | IdList 'metaVar
| ListItem "('upVar, 'var, 'svar, 'metaVar) kWithRewrite" | ListFun "('upVar, 'var, 'svar, 'metaVar) kLabel" "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theListRewrite =
       TheListTerm "('upVar, 'var, 'svar, 'metaVar) theList"
     | TheListRewrite "('upVar, 'var, 'svar, 'metaVar) theList"
                      "('upVar, 'var, 'svar, 'metaVar) theList"
and ('upVar, 'var, 'svar, 'metaVar) theSet = SetCon "('upVar, 'var, 'svar, 'metaVar) theSetRewrite" "('upVar, 'var, 'svar, 'metaVar) theSetRewrite"
                                    | UnitSet
                                    | IdSet 'metaVar
| SetItem "('upVar, 'var, 'svar, 'metaVar) kWithRewrite" | SetFun "('upVar, 'var, 'svar, 'metaVar) kLabel" "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theSetRewrite =
       TheSetTerm "('upVar, 'var, 'svar, 'metaVar) theSet"
     | TheSetRewrite "('upVar, 'var, 'svar, 'metaVar) theSet"
                     "('upVar, 'var, 'svar, 'metaVar) theSet"
and ('upVar, 'var, 'svar, 'metaVar) theMap
  = MapCon "('upVar, 'var, 'svar, 'metaVar) theMapRewrite"
           "('upVar, 'var, 'svar, 'metaVar) theMapRewrite"
         | UnitMap
         | IdMap 'metaVar
         | MapItem "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
                   "('upVar, 'var, 'svar, 'metaVar) kWithRewrite"
         | MapFun "('upVar, 'var, 'svar, 'metaVar) kLabel"
                  "('upVar, 'var, 'svar, 'metaVar) kListWithRewrite"
and ('upVar, 'var, 'svar, 'metaVar) theMapRewrite =
       TheMapTerm "('upVar, 'var, 'svar, 'metaVar) theMap"
| TheMapRewrite "('upVar, 'var, 'svar, 'metaVar) theMap" "('upVar, 'var, 'svar, 'metaVar) theMap"
and ('upVar, 'var, 'svar, 'metaVar) bag
            = BagCon "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite"
                     "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite"
             | UnitBag
             | IdBag 'metaVar
| Xml 'var "feature list" "('upVar, 'var, 'svar, 'metaVar) bagWithRewrite" | SingleCell 'var "feature list" "('upVar, 'var, 'svar, 'metaVar) bigK"
and ('upVar, 'var, 'svar, 'metaVar) bagWithRewrite =
       BagTerm "('upVar, 'var, 'svar, 'metaVar) bag"
| BagRewrite "('upVar, 'var, 'svar, 'metaVar) bag" "('upVar, 'var, 'svar, 'metaVar) bag"

It takes something like three to four hours on my student's computer (Windows machine with the same amount of memory), but it does complete. Is there some way to tweak Isabelle or this definition to make it more likely to go through?

---Elsa





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.