Skip to content

Commit

Permalink
deploy: 8bd87d7
Browse files Browse the repository at this point in the history
  • Loading branch information
BraeWebb committed Apr 17, 2024
1 parent dd41cfe commit 1386489
Show file tree
Hide file tree
Showing 120 changed files with 7,370 additions and 5,461 deletions.
2 changes: 2 additions & 0 deletions .browser_info/index.json
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@
{"name": "Proofs",
"description": "Supporting proof theories and definitions"},
{"name": "Semantics", "description": "Semantics of the GraalVM IR"},
{"name": "SemanticsPaper",
"description": "Content for IR semantics description paper"},
{"name": "Snippets",
"description":
"Additional commands to enable the generation of LaTeX snippets of theories"},
Expand Down
2 changes: 1 addition & 1 deletion Canonicalizations/.browser_info/build_uuid
Original file line number Diff line number Diff line change
@@ -1 +1 @@
94b2d873-b4be-4e0a-9045-3603d668dae4
9410185a-1397-4e37-823e-e573c61b1bda
54 changes: 27 additions & 27 deletions Canonicalizations/AbsPhase.html

Large diffs are not rendered by default.

46 changes: 23 additions & 23 deletions Canonicalizations/AddPhase.html

Large diffs are not rendered by default.

44 changes: 22 additions & 22 deletions Canonicalizations/AndPhase.html

Large diffs are not rendered by default.

8 changes: 4 additions & 4 deletions Canonicalizations/BinaryNode.html
Original file line number Diff line number Diff line change
Expand Up @@ -12,23 +12,23 @@
<h1>Theory BinaryNode</h1>
</div>

<pre class="source"><span class="keyword1"><span class="command"><span>subsection</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span></span><span>BinaryNode Phase</span><span></span></span></span><span>
<pre class="source"><span class="keyword1"><span class="command"><span>subsection</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span>‹BinaryNode Phase›</span></span></span><span>

</span><span class="keyword1"><span class="command"><span>theory</span></span></span><span> </span><a href="BinaryNode.html"><span>BinaryNode</span></a><span>
</span><span class="keyword2"><span class="keyword"><span>imports</span></span></span><span>
</span><a href="Common.html"><span>Common</span></a><span>
</span><span class="keyword2"><span class="keyword"><span>begin</span></span></span><span>

</span><span class="keyword1"><span class="command"><span>phase</span></span></span><span> </span><span>BinaryNode</span><span>
</span><span class="keyword1"><span class="command"><span>phase</span></span></span><span> BinaryNode
</span><span class="keyword2"><span class="keyword"><span>terminating</span></span></span><span> </span><span class="quoted"><a class="entity_ref" href="../OptimizationDSL/Canonicalization.html#Canonicalization.size|const"><span>size</span></a></span><span>
</span><span class="keyword2"><span class="keyword"><span>begin</span></span></span><span>

</span><span class="keyword1"><span class="command"><span class="entity_def" id="BinaryNode.BinaryFoldConstant_code|const"><span>optimization</span></span></span></span><span> </span><span class="entity_def" id="BinaryNode.BinaryFoldConstant|fact"><span class="entity_def" id="BinaryNode.BinaryFoldConstant_code|fact"><span class="entity_def" id="BinaryNode.BinaryFoldConstant(2)|thm"><span class="entity_def" id="BinaryNode.BinaryFoldConstant(1)|thm"><span class="entity_def" id="BinaryNode.BinaryFoldConstant_code|thm"><span class="entity_def" id="BinaryNode.BinaryFoldConstant_code_raw|axiom"><span>BinaryFoldConstant</span></span></span></span></span></span></span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.IRExpr.BinaryExpr|const"><span>BinaryExpr</span></a><span> </span><span class="free"><span>op</span></span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><a class="entity_ref" href="../OptimizationDSL/Markup.html#Markup.ExtraNotation.ConstantNotation|const"><span>const</span></a></span><span> </span><span class="free"><span>v1</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><span>(</span></span><span class="keyword1"><a class="entity_ref" href="../OptimizationDSL/Markup.html#Markup.ExtraNotation.ConstantNotation|const"><span>const</span></a></span><span> </span><span class="free"><span>v2</span></span><span class="main"><span>)</span></span><span> </span><span class="main"><a class="entity_ref" href="../OptimizationDSL/Markup.html#Markup.Rewrite.Transform|const"><span></span></a></span><span> </span><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.IRExpr.ConstantExpr|const"><span>ConstantExpr</span></a><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.bin_eval|const"><span>bin_eval</span></a><span> </span><span class="free"><span>op</span></span><span> </span><span class="free"><span>v1</span></span><span> </span><span class="free"><span>v2</span></span><span class="main"><span>)</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>unfolding</span></span></span><span> </span><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.le_expr_def|fact"><span>le_expr_def</span></a><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html#HOL.rule|method"><span class="operator"><span>rule</span></span></a><span> </span><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.allI|fact"><span>allI</span></a><span> </span><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.impI|fact"><span>impI</span></a><span class="main"><span>)</span></span><span class="main"><span class="keyword3"><span>+</span></span></span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>premises</span></span></span><span> </span><span class="entity_def" id="offset_297..300">bin</span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> m p v</span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>premises</span></span></span><span> </span><span class="entity_def" id="offset_297..300">bin</span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> m p v
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/classical.ML.html#HOL.rule|method"><span class="operator"><span>rule</span></span></a><span> </span><a class="entity_ref" href="../Semantics/IRTreeEval.html#IRTreeEval.BinaryExprE|fact"><span>BinaryExprE</span></a><span class="main"><span class="main"><span>[</span></span></span><span class="operator"><span>OF</span></span><span> </span><a class="entity_ref" href="BinaryNode.html#offset_297..300"><span>bin</span></a><span class="main"><span class="main"><span>]</span></span></span><span class="main"><span>)</span></span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>premises</span></span></span><span> </span><span class="entity_def" id="offset_369..374">prems</span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> x y</span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>premises</span></span></span><span> </span><span class="entity_def" id="offset_369..374">prems</span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> x y
</span><span class="keyword1"><span class="command"><span>proof</span></span></span><span> </span><span class="operator"><span>-</span></span><span>
</span><span class="keyword1"><span class="command"><span>have</span></span></span><span> </span><span class="entity_def" id="offset_406..407">x</span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="skolem"><span>x</span></span><span> </span><span class="main"><a class="entity_ref" href="../../HOL/HOL/HOL.html#HOL.eq|const"><span>=</span></a></span><span> </span><span class="free"><span>v1</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span>using</span></span></span><span> </span><a class="entity_ref" href="BinaryNode.html#offset_369..374"><span>prems</span></a><span> </span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/clasimp.ML.html#HOL.auto|method"><span class="operator"><span>auto</span></span></a><span>
Expand Down
4 changes: 2 additions & 2 deletions Canonicalizations/Common.html
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
<h1>Theory Common</h1>
</div>

<pre class="source"><span class="keyword1"><span class="command"><span>section</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span></span><span>Canonicalization Optimizations</span><span></span></span></span><span>
<pre class="source"><span class="keyword1"><span class="command"><span>section</span></span></span><span> </span><span class="quoted"><span class="plain_text"><span>‹Canonicalization Optimizations›</span></span></span><span>

</span><span class="keyword1"><span class="command"><span>theory</span></span></span><span> </span><a href="Common.html"><span>Common</span></a><span>
</span><span class="keyword2"><span class="keyword"><span>imports</span></span></span><span>
Expand All @@ -22,7 +22,7 @@ <h1>Theory Common</h1>

</span><span class="keyword1"><span class="command"><span>lemma</span></span></span><span> </span><span class="entity_def" id="Common.size_pos|fact"><span class="entity_def" id="Common.size_pos|thm"><span>size_pos</span></span></span><span class="main"><span>[</span></span><a class="entity_ref" href="../OptimizationDSL/Canonicalization.html#Canonicalization.size_simps|attribute"><span class="operator"><span>size_simps</span></span></a><span class="main"><span>]</span></span><span class="main"><span>:</span></span><span> </span><span class="quoted"><span class="quoted"><span>"</span><span class="main"><a class="entity_ref" href="../../HOL/HOL/Groups.html#Groups.zero_class.zero|const"><span>0</span></a></span><span> </span><span class="main"><a class="entity_ref" href="../../HOL/HOL/Orderings.html#Orderings.ord_class.less|const"><span>&lt;</span></a></span><span> </span><a class="entity_ref" href="../OptimizationDSL/Canonicalization.html#Canonicalization.size|const"><span>size</span></a><span> </span><span class="free"><span>y</span></span><span>"</span></span></span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Tools/induction.ML.html#HOL.induction|method"><span class="operator"><span>induction</span></span></a><span> </span><span class="quoted"><span class="free"><span>y</span></span></span><span class="main"><span class="keyword3"><span>;</span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Provers/clasimp.ML.html#HOL.auto|method"><span class="operator"><span>auto</span></span></a><span class="main"><span class="keyword3"><span>?</span></span></span><span class="main"><span>)</span></span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> op</span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>subgoal</span></span></span></span></span><span> </span><span class="keyword2"><span class="keyword"><span>for</span></span></span><span> op
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>apply</span></span></span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/Tools/induct.ML.html#HOL.cases|method"><span class="operator"><span>cases</span></span></a><span> </span><span class="quoted"><span class="skolem"><span>op</span></span></span><span class="main"><span>)</span></span><span>
</span><span class="keyword1"><span class="command"><span>by</span></span></span><span> </span><span class="main"><span>(</span></span><a class="entity_ref" href="../../HOL/HOL/ISABELLE_HOME/src/HOL/Tools/SMT/smt_systems.ML.html#SMT.smt|method"><span class="operator"><span>smt</span></span></a><span> </span><span class="main"><span class="main"><span>(</span></span></span><span>z3</span><span class="main"><span class="main"><span>)</span></span></span><span> </span><a class="entity_ref" href="../../HOL/HOL/Nat.html#Nat.gr0I|fact"><span>gr0I</span></a><span> </span><a class="entity_ref" href="../../HOL/HOL/Rings.html#Rings.zero_neq_one_class.one_neq_zero|fact"><span>one_neq_zero</span></a><span> </span><a class="entity_ref" href="../../HOL/HOL/NthRoot.html#NthRoot.pos2|fact"><span>pos2</span></a><span> </span><a class="entity_ref" href="../OptimizationDSL/Canonicalization.html#Canonicalization.size.elims|fact"><span>size.elims</span></a><span> </span><a class="entity_ref" href="../../HOL/HOL/Nat.html#Nat.trans_less_add2|fact"><span>trans_less_add2</span></a><span class="main"><span>)</span></span><span class="main"><span class="keyword3"><span>+</span></span></span><span>
</span><span class="keyword1"><span class="command"><span class="improper"><span class="command"><span>done</span></span></span></span></span><span>
Expand Down
Loading

0 comments on commit 1386489

Please sign in to comment.