renamed html->docs

.gitignore

@@ -1,6 +1,5 @@
 *~
 *.s
-/html
 obsolete
 obsolete/*
 dist.tgz

README.in.md

@@ -0,0 +1,15 @@
+# Isabelle-LLVM Parallel
+
+Note: this distribution has been copied and adapted from the original Isabelle-LLVM framework.
+
+Isabelle-LLVM Parallel is a verification framework for Isabelle/HOL that targets LLVM as backend.
+It adds parallel execution to the original [Isabelle LLVM](http://www21.in.tum.de/~lammich/isabelle_llvm/).
+
+For build instructions and starting points to browse the theories, see [HTML:(index.html)].
+
+# Regression Test
+
+The regression test can be run using `make` in the [regression](regression) directory. The following commands must be available.
+- [Valgrind](https://valgrind.org/) as `valgrind` 
+- clang as `clang`
+- Intel's [intruction set emulator](https://www.intel.com/content/www/us/en/developer/articles/tool/software-development-emulator.html) as `sde`

README.md

@@ -5,7 +5,7 @@ Note: this distribution has been copied and adapted from the original Isabelle-L
 Isabelle-LLVM Parallel is a verification framework for Isabelle/HOL that targets LLVM as backend.
 It adds parallel execution to the original [Isabelle LLVM](http://www21.in.tum.de/~lammich/isabelle_llvm/).
 
-For build instructions and starting points to browse the theories, see [html/index.html].
+For build instructions and starting points to browse the theories, see [HTML:(index.html)].
 
 # Regression Test
 

docs/LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2018, Peter Lammich
+
+All rights reserved.
+
+All files of Isabelle LLVM are released under the following license.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+Redistributions of source code must retain the above copyright notice,
+this list of conditions and the following disclaimer.  Redistributions
+in binary form must reproduce the above copyright notice, this list of
+conditions and the following disclaimer in the documentation and/or
+other materials provided with the distribution.  Neither the name of
+the GRAT tool chain nor the names of its contributors may be
+used to endorse or promote products derived from this software without
+specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

docs/browser_info/.browser_info/index.json

@@ -0,0 +1,18 @@
+{"kind": "root",
+ "items":
+   [{"name": "HOL",
+     "description":
+       "\n    Higher-Order Logic.\n\n    Isabelle/HOL is a version of classical higher-order logic resembling\n    that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).\n  "},
+    {"name": "FOL",
+     "description":
+       "\n    First-Order Logic with some variations: single-sorted vs. many-sorted\n    (polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs.\n    set-theory (ZF).\n  "},
+    {"name": "Pure",
+     "description":
+       "\n    The Pure logical framework.\n\n    Isabelle/Pure is a version of intuitionistic higher-order logic that\n    expresses rules for Natural Deduction declaratively.\n  "},
+    {"name": "Misc",
+     "description":
+       "\n    Miscellaneous object-logics, tools, and experiments.\n  "},
+    {"name": "Doc", "description": "\n    Sources of Documentation.\n  "},
+    {"name": "Unsorted",
+     "description": "\n    Sessions without 'chapter' declaration.\n  "},
+    {"name": "AFP", "description": "\n    Archive of Formal Proofs\n  "}]}

docs/browser_info/AFP/.browser_info/index.json

@@ -0,0 +1,5 @@
+{"kind": "chapter",
+ "items":
+   [{"name": "Automatic_Refinement", "description": ""},
+    {"name": "Go", "description": "A Go frontend for the code generator."},
+    {"name": "Refine_Monadic", "description": ""}]}

docs/browser_info/AFP/Automatic_Refinement/.browser_info/build_uuid

@@ -0,0 +1 @@
+184c71b2-f19f-4065-b7f7-2f58e521c1be

docs/browser_info/AFP/Automatic_Refinement/AFP/Automatic_Refinement/Lib/Cond_Rewr_Conv.ML.html

@@ -0,0 +1,48 @@
+<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"/><link rel="stylesheet" type="text/css" href="isabelle.css"/>
+<title>File ‹Cond_Rewr_Conv.ML›</title>
+</head>
+
+
+<body>
+<div class="head">
+<h1>File ‹Cond_Rewr_Conv.ML›</h1>
+</div>
+
+<pre class="source"><span class="keyword1"><span class="keyword"><span>signature</span></span></span><span> </span><span class="entity"><span>COND_REWR_CONV</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword2"><span class="keyword"><span>sig</span></span></span><span>
+  </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> cond_rewr_conv</span><span class="main"><span>:</span></span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>Proof.context</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>tactic</span><span class="main"><span>)</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>thm</span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span class="entity"><span>Proof.context</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>conv</span><span>
+  </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> cond_rewrs_conv</span><span class="main"><span>:</span></span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>Proof.context</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>tactic</span><span class="main"><span>)</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>thm</span><span> </span><span>list</span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span class="entity"><span>Proof.context</span></span><span> </span><span class="main"><span>-&gt;</span></span><span> </span><span>conv</span><span>
+</span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span>
+
+</span><span class="keyword1"><span class="keyword"><span>structure</span></span></span><span> </span><span class="entity"><span>Cond_Rewr_Conv</span></span><span> </span><span class="main"><span>:</span></span><span class="entity"><span>COND_REWR_CONV</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword2"><span class="keyword"><span>struct</span></span></span><span>
+  </span><span class="keyword3"><span class="keyword"><span>open</span></span></span><span> </span><span>Refine_Util</span><span>
+  </span><span class="comment1"><span>(* Conditional rewrite rule. tac used to discharge conditions *)</span></span><span>
+  </span><span class="keyword1"><span class="keyword"><span>fun</span></span></span><span> </span><span class="entity"><span>cond_rewr_conv_aux</span></span><span> </span><span class="entity"><span>tac</span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="entity"><span>ctxt</span></span><span> </span><span class="entity"><span>ct</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="keyword2"><span class="keyword"><span>let</span></span></span><span>
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>lhs</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span>|&gt;</span><span> </span><span>Thm.concl_of</span><span> </span><span>|&gt;</span><span> </span><span>Logic.dest_equals</span><span> </span><span>|&gt;</span><span> </span><span class="main"><span>#</span></span><span class="inner_numeral"><span>1</span></span><span> </span><span>|&gt;</span><span> </span><span>Thm.cterm_of</span><span> </span><span class="entity"><span>ctxt</span></span><span>
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>inst</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>Thm.match</span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>lhs</span></span><span class="main"><span>,</span></span><span class="entity"><span>ct</span></span><span class="main"><span>)</span></span><span> 
+      </span><span class="keyword3"><span class="keyword"><span>handle</span></span></span><span> </span><span>Pattern.MATCH</span><span> </span><span class="main"><span>=&gt;</span></span><span> </span><span class="keyword3"><span class="keyword"><span>raise</span></span></span><span> </span><span>CTERM</span><span> </span><span class="main"><span>(</span></span><span class="inner_quoted"><span>"dis_rewr_conv: MATCH"</span></span><span class="main"><span>,</span></span><span class="main"><span>[</span></span><span class="entity"><span>lhs</span></span><span class="main"><span>,</span></span><span class="entity"><span>ct</span></span><span class="main"><span>]</span></span><span class="main"><span>)</span></span><span>
+
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>thm'</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>Thm.instantiate</span><span> </span><span class="entity"><span>inst</span></span><span> </span><span class="entity"><span>thm</span></span><span>
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>dprems</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>Thm.prems_of</span><span> </span><span class="entity"><span>thm'</span></span><span> 
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>dthms</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span>map</span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><span class="keyword"><span>fn</span></span></span><span> </span><span class="entity"><span>t</span></span><span> </span><span class="main"><span>=&gt;</span></span><span> 
+      </span><span class="main"><span>(</span></span><span>Goal.prove</span><span> </span><span class="entity"><span>ctxt</span></span><span> </span><span class="main"><span>[</span></span><span class="main"><span>]</span></span><span> </span><span class="main"><span>[</span></span><span class="main"><span>]</span></span><span> </span><span class="entity"><span>t</span></span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>tac</span></span><span> </span><span>o</span><span> </span><span class="main"><span>#</span></span><span>context</span><span class="main"><span>)</span></span><span class="main"><span>)</span></span><span> </span><span class="keyword3"><span class="keyword"><span>handle</span></span></span><span> </span><span>ERROR</span><span> </span><span class="entity"><span>s</span></span><span> 
+        </span><span class="main"><span>=&gt;</span></span><span> </span><span class="keyword3"><span class="keyword"><span>raise</span></span></span><span> </span><span>TERM</span><span> </span><span class="main"><span>(</span></span><span class="inner_quoted"><span>"dis_rew_conv: "</span></span><span>^</span><span> </span><span class="entity"><span>s</span></span><span class="main"><span>,</span></span><span class="main"><span>[</span></span><span class="entity"><span>t</span></span><span class="main"><span>]</span></span><span class="main"><span>)</span></span><span class="main"><span>)</span></span><span> </span><span class="entity"><span>dprems</span></span><span>
+    </span><span class="keyword1"><span class="keyword"><span>val</span></span></span><span> </span><span class="entity"><span>res</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>thm'</span></span><span> </span><span>OF</span><span> </span><span class="entity"><span>dthms</span></span><span>
+  </span><span class="keyword2"><span class="keyword"><span>in</span></span></span><span> </span><span class="entity"><span>res</span></span><span> </span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span class="main"><span>;</span></span><span>
+
+  </span><span class="keyword1"><span class="keyword"><span>fun</span></span></span><span> </span><span class="entity"><span>cond_rewr_conv</span></span><span> </span><span class="entity"><span>tac</span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="entity"><span>ctxt</span></span><span> </span><span class="main"><span>=</span></span><span> </span><span class="entity"><span>fix_conv</span></span><span> </span><span class="entity"><span>ctxt</span></span><span> </span><span class="main"><span>(</span></span><span class="entity"><span>cond_rewr_conv_aux</span></span><span> </span><span class="entity"><span>tac</span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="entity"><span>ctxt</span></span><span class="main"><span>)</span></span><span>
+
+  </span><span class="comment1"><span>(*fun first_conv [] ct = Conv.no_conv ct
+    | first_conv (cv::cvs) ct = (cv else_conv first_conv cvs) ct*)</span></span><span>
+
+  </span><span class="keyword1"><span class="keyword"><span>fun</span></span></span><span> </span><span class="entity"><span>cond_rewrs_conv</span></span><span> </span><span class="entity"><span>tac</span></span><span> </span><span class="entity"><span>thms</span></span><span> </span><span class="entity"><span>ctxt</span></span><span> </span><span class="main"><span>=</span></span><span> 
+    </span><span>Conv.first_conv</span><span> </span><span class="main"><span>(</span></span><span>map</span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><span class="keyword"><span>fn</span></span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="main"><span>=&gt;</span></span><span> </span><span class="entity"><span>cond_rewr_conv</span></span><span> </span><span class="entity"><span>tac</span></span><span> </span><span class="entity"><span>thm</span></span><span> </span><span class="entity"><span>ctxt</span></span><span class="main"><span>)</span></span><span> </span><span class="entity"><span>thms</span></span><span class="main"><span>)</span></span><span> 
+
+</span><span class="keyword2"><span class="keyword"><span>end</span></span></span><span>
+</span></pre>
+</body>
+
+</html>