f90a2d5a by Ifaz Kabir

Adding kDOT

1 parent cf82f49c
......@@ -10,3 +10,7 @@ The extensions are based on the [simple](https://github.com/amaurremi/dot-calcul
If you want to understand the DOT safety proof, or are interested in creating your own extensions to DOT, you can read our [OOPSLA](https://plg.uwaterloo.ca/~olhotak/pubs/oopsla17.pdf) paper, and check out the corresponding [Coq](https://github.com/amaurremi/dot-calculus/tree/master/src/simple-proof) proof.
## Extensions
We currently provide the following extensions:
- [κDOT](https://git.uwaterloo.ca/ikabir/dot-public/tree/master/kDOT)
......
*.v.d
*.vo
*.vo.aux
*.glob
*.swp
*.aux
.depend
*~
*#
*.swo
*.cache
.DS_Store
*.iml
_CoqProject
*.bak
*.dot
*.dpd
Makefile.coq
Makefile.coq.conf
html/
all:
$(MAKE) -C src ide proofs doc
clean:
$(MAKE) -C src clean
Extensions for Dependent Object Types
-------------------------------------
The DOT (Dependent Object Types) calculus by [Amin et al. (2016)](http://infoscience.epfl.ch/record/215280/files/paper_1.pdf) aims to formalizes Scala, specifically, abstract type members and path-dependent types.
This repository contains an extension to DOT that aim to bridge the gap between DOT and Scala, and to experiment with new Scala features. The extension is based on the [simple](https://github.com/amaurremi/dot-calculus/tree/master/src/simple-proof) type-safety proof, which we started as a fork of the [original](https://github.com/samuelgruetter/dot-calculus) proof as presented by Amin et al. (2016).
If you want to understand the DOT safety proof, or are interested in creating your own extensions to DOT, you can read our [OOPSLA](https://plg.uwaterloo.ca/~olhotak/pubs/oopsla17.pdf) paper, and check out the corresponding [Coq](https://github.com/amaurremi/dot-calculus/tree/master/src/simple-proof) proof.
## Compiling the Proof
To compile the proof, we require `coq 8.7.2` and related tooling to be run in a unix-like environment. We also require `coq-tlc` library. We recommend installing both using `opam`.
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin add coq 8.7.2
opam install coq
opam install coq-tlc
Other requirements are:
* `make`
To compile the proof, clone the repository to a directory called `dot-calculus` and run
cd dot-calculus
make
`make` will do the following:
- compile the safety proof
- generate documentation.
/*.png
/*.html
/*.css
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="assets/resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="assets/resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="assets/resources/config.js"></script>
<script type="text/javascript" src="assets/resources/coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../README.html">README</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
var coqdocjs = coqdocjs || {};
coqdocjs.repl = {
"forall": "∀",
"exists": "∃",
"/\\": "∧",
"\\/": "∨",
"|->": "↦",
"->": "→",
"<-": "←",
"<->": "↔",
"=>": "⇒",
"<>": "≠",
"<=": "≤",
">=": "≥",
"mapsto": "↦",
"el": "∈",
"isin": "∈",
"top" : "⊤",
"bot" : "⊥",
"subG" : "≺:",
"nel": "∉",
"<<=": "⊆",
"|-": "⊢",
"/-": "⊢",
">>": "»",
"<<": "⊆",
"++": "⧺",
"===": "≡",
"=/=": "≢",
"=~=": "≅",
"==>": "⟹",
"G": "Γ",
"Gamma": "Γ",
"Sigma": "Σ",
"kappa": "κ",
"mu": "μ",
"nu": "ν",
"lambda": "λ",
"eta": "η",
"nat": "ℕ"
};
coqdocjs.subscr = {
"0" : "₀",
"1" : "₁",
"2" : "₂",
"3" : "₃",
"4" : "₄",
"5" : "₅",
"6" : "₆",
"7" : "₇",
"8" : "₈",
"9" : "₉"
};
coqdocjs.replInText = Object.keys(coqdocjs.repl);
@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
body{
font-family: 'Open Sans', sans-serif;
font-size: 14px;
color: #2D2D2D
}
a {
text-decoration: none;
border-radius: 3px;
padding-left: 3px;
padding-right: 3px;
margin-left: -3px;
margin-right: -3px;
color: inherit;
font-weight: bold;
}
.readme a {
text-decoration: underline;
font-weight: none;
}
#main .code a, #main .inlinecode a, #toc a {
font-weight: inherit;
}
a[href]:hover, [clickable]:hover{
background-color: rgba(0,0,0,0.1);
cursor: pointer;
}
h, h1, h2, h3, h4, h5 {
line-height: 1;
color: black;
text-rendering: optimizeLegibility;
font-weight: normal;
letter-spacing: 0.1em;
text-align: left;
}
div + br {
display: none;
}
div:empty{ display: none;}
#main h1 {
font-size: 2em;
}
#main h2 {
font-size: 1.667rem;
}
#main h3 {
font-size: 1.333em;
}
#main h4, #main h5, #main h6 {
font-size: 1em;
}
#toc h2 {
padding-bottom: 0;
}
#main .doc {
margin: 0;
text-align: justify;
}
.inlinecode, .code, #main pre {
font-family: monospace;
}
.code > br:first-child {
display: none;
}
.doc + .code{
margin-top:0.5em;
}
.block{
display: block;
margin-top: 5px;
margin-bottom: 5px;
padding: 10px;
text-align: center;
}
.block img{
margin: 15px;
}
table.infrule {
border: 0px;
margin-left: 50px;
margin-top: 10px;
margin-bottom: 10px;
}
td.infrule {
font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
text-align: center;
padding: 0;
line-height: 1;
}
tr.infrulemiddle hr {
margin: 1px 0 1px 0;
}
.infrulenamecol {
color: rgb(60%,60%,60%);
padding-left: 1em;
padding-bottom: 0.1em
}
.id[type="constructor"], .id[type="projection"], .id[type="method"],
.id[title="constructor"], .id[title="projection"], .id[title="method"] {
color: #A30E16;
}
.id[type="var"], .id[type="variable"],
.id[title="var"], .id[title="variable"] {
color: inherit;
}
.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
color: #A6650F;
}
.id[type="lemma"],
.id[title="lemma"]{
color: #188B0C;
}
.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
color : #2874AE;
}
.comment {
color: #808080;
}
/* TOC */
#toc h2{
letter-spacing: 0;
font-size: 1.333em;
}
/* Index */
#index {
margin: 0;
padding: 0;
width: 100%;
}
#index #frontispiece {
margin: 1em auto;
padding: 1em;
width: 60%;
}
.booktitle { font-size : 140% }
.authors { font-size : 90%;
line-height: 115%; }
.moreauthors { font-size : 60% }
#index #entrance {
text-align: center;
}
#index #entrance .spacer {
margin: 0 30px 0 30px;
}
ul.doclist {
margin-top: 0em;
margin-bottom: 0em;
}
#toc > * {
clear: both;
}
#toc > a {
display: block;
float: left;
margin-top: 1em;
}
#toc a h2{
display: inline;
}
/* replace unicode */
.id[repl] .hidden {
font-size: 0;
}
.inlinecode .hidden {
display: none;
}
.id[repl]:before{
content: attr(repl);
}
/* folding proofs */
@keyframes show-proof {
0% {
max-height: 1.2em;
opacity: 1;
}
99% {
max-height: 1000em;
}
100%{
}
}
@keyframes hide-proof {
from {
visibility: visible;
max-height: 10em;
opacity: 1;
}
to {
max-height: 1.2em;
}
}
.proof {
cursor: pointer;
}
.proof * {
cursor: pointer;
}
.proof {
overflow: hidden;
position: relative;
display: inline-block;
}
.proof[show="false"] {
max-height: 1.2em;
visibility: hidden;
opacity: 0;
}
.proof[show="false"][animate] {
animation-name: hide-proof;
animation-duration: 0.25s;
}
.proof[show=true] {
animation-name: show-proof;
animation-duration: 10s;
}
.proof[show="false"]:before {
position: absolute;
visibility: visible;
width: 100%;
height: 100%;
display: block;
opacity: 0;
content: "M";
}
.proof[show="false"]:hover:before {
content: "";
}
.proof[show="false"] + br + br {
display: none;
}
.proof[show="false"]:hover {
visibility: visible;
opacity: 0.5;
}
#toggle-proofs[proof-status="no-proofs"] {
display: none;
}
#toggle-proofs[proof-status="some-hidden"]:before {
content: "Show Proofs";
}
#toggle-proofs[proof-status="all-shown"]:before {
content: "Hide Proofs";
}
/* page layout */
html, body {
height: 100%;
margin:0;
padding:0;
}
body {
display: flex;
flex-direction: column
}
#content {
flex: 1;
overflow: auto;
display: flex;
flex-direction: column;
}
#content:focus {
outline: none; /* prevent glow in OS X */
}
#main {
display: block;
padding: 16px;
padding-top: 1em;
padding-bottom: 2em;
margin-left: auto;
margin-right: auto;
max-width: 60em;
flex: 1 0 auto;
}
.libtitle {
display: none;
}
/* header */
#header {
width:100%;
padding: 0;
margin: 0;
display: flex;
align-items: center;
background-color: rgb(21,57,105);
color: white;
font-weight: bold;
overflow: hidden;
}
.button {
cursor: pointer;
}
#header * {
text-decoration: none;
vertical-align: middle;
margin-left: 15px;
margin-right: 15px;
}
#header > .right, #header > .left {
display: flex;
flex: 1;
align-items: center;
}
#header > .left {
text-align: left;
}
#header > .right {
flex-direction: row-reverse;
}
#header a, #header .button {
color: white;
box-sizing: border-box;
}
#header a {
border-radius: 0;
padding: 0.2em;
}
#header .button {
background-color: rgb(63, 103, 156);
border-radius: 1em;
padding-left: 0.5em;
padding-right: 0.5em;
margin: 0.2em;
}
#header a:hover, #header .button:hover {
background-color: rgb(181, 213, 255);
color: black;
}
#header h1 { padding: 0;
margin: 0;}
/* footer */
#footer {
text-align: center;
opacity: 0.5;
font-size: 75%;
}
/* hyperlinks */
@keyframes highlight {
50%{
background-color: black;
}
}
:target * {
animation-name: highlight;
animation-duration: 1s;
}
a[name]:empty {
float: right;
}
/* Proviola */
div.code {
width: auto;
float: none;
}
div.goal {
position: fixed;
left: 75%;
width: 25%;
top: 3em;
}
div.doc {
background-color: #e0e5f8;
padding: 10px;
clear: both;
}
span.command:hover {
background-color: inherit;
}
var coqdocjs = coqdocjs || {};
(function(){
function replace(s){
var m;
if (m = s.match(/^(.+)'/)) {
return replace(m[1])+"'";
} else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
return replace(m[1])+m[2].replace(/\d/g, function(d){return coqdocjs.subscr[d]});
} else if (coqdocjs.repl.hasOwnProperty(s)){
return coqdocjs.repl[s]
} else {
return s;
}
}
function toArray(nl){
return Array.prototype.slice.call(nl);
}
function replInTextNodes() {
coqdocjs.replInText.forEach(function(toReplace){
toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){
toArray(elem.childNodes).forEach(function(node){
if (node.nodeType != Node.TEXT_NODE) return;
var fragments = node.textContent.split(toReplace);
node.textContent = fragments[fragments.length-1];
for (var k = 0; k < fragments.length - 1; ++k) {
node.parentNode.insertBefore(document.createTextNode(fragments[k]),node);
var replacement = document.createElement("span");
replacement.appendChild(document.createTextNode(toReplace));
replacement.setAttribute("class", "id");
replacement.setAttribute("type", "keyword");
node.parentNode.insertBefore(replacement, node);
}
});
});
});
}
function replNodes() {
toArray(document.getElementsByClassName("id")).forEach(function(node){
if (["var", "variable", "keyword", "notation", "definition", "inductive", "tactic"].indexOf(node.getAttribute("type"))>=0){
var text = node.textContent;
var replText = replace(text);
if(text != replText) {
node.setAttribute("repl", replText);
node.setAttribute("title", text);
var hidden = document.createElement("span");
hidden.setAttribute("class", "hidden");
while (node.firstChild) {
hidden.appendChild(node.firstChild);
}
node.appendChild(hidden);
}
}
});
}
function replNotIn() {
toArray(document.getElementsByClassName("id")).forEach(function(node){
if (node.getAttribute("type") == "notation" && node.textContent == "\\" && node.nextSibling.getAttribute("type") == "notation" && node.nextSibling.textContent == "notin"){
var next = node.nextSibling;
node.setAttribute("repl", "∉");
node.setAttribute("title", "\\notin");
var hidden = document.createElement("span");
hidden.setAttribute("class", "hidden");
while (node.firstChild) {
hidden.appendChild(node.firstChild);
}
hidden.appendChild(next);
node.appendChild(hidden);
}
});
coqdocjs.replInText.forEach(function(toReplace){
toArray(document.getElementsByClassName("inlinecode")).forEach(function(node){
var fc = node.firstChild;
if (fc && fc.textContent == "\\" && fc.nextSibling) {
var ns = fc.nextSibling;
if (ns.getAttribute("type") == "var" && ns.textContent == "notin") {
var child = ns.cloneNode(true);
child.setAttribute("repl", "∉");
child.setAttribute("title", "\\notin");
while (child.firstChild) {
child.removeChild(child.firstChild);
}
var hidden = document.createElement("span");
hidden.setAttribute("class", "hidden");
while (node.firstChild) {
hidden.appendChild(node.firstChild);
}
node.appendChild(child);
node.appendChild(hidden);
}
}
});
});
}
function isVernacStart(l, t){
t = t.trim();
for(var s of l){
if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){
return true;
}
}
return false;
}
function isProofStart(s){
return isVernacStart(["Proof"], s);
}
function isProofEnd(s){
return isVernacStart(["Qed", "Admitted", "Defined"], s);
}
function proofStatus(){
var proofs = toArray(document.getElementsByClassName("proof"));
if(proofs.length) {
for(var proof of proofs) {
if (proof.getAttribute("show") === "false") {
return "some-hidden";
}
}
return "all-shown";
}
else {
return "no-proofs";
}
}
function updateView(){
document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus());
}
function foldProofs() {
var hasCommands = true;
var nodes = document.getElementsByClassName("command");
if(nodes.length == 0) {
hasCommands = false;
console.log("no command tags found")
nodes = document.getElementsByClassName("id");
}
toArray(nodes).forEach(function(node){
if(isProofStart(node.textContent)) {
var proof = document.createElement("span");
proof.setAttribute("class", "proof");
node.parentNode.insertBefore(proof, node);
if(proof.previousSibling.nodeType === Node.TEXT_NODE)
proof.appendChild(proof.previousSibling);
while(node && !isProofEnd(node.textContent)) {
proof.appendChild(node);
node = proof.nextSibling;
}
if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed
if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed
proof.addEventListener("click", function(proof){return function(e){
if (e.target.parentNode.tagName.toLowerCase() === "a")
return;
proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true");
proof.setAttribute("animate", "");
updateView();
};}(proof));
proof.setAttribute("show", "false");
}
});
}
function toggleProofs(){
var someProofsHidden = proofStatus() === "some-hidden";
toArray(document.getElementsByClassName("proof")).forEach(function(proof){
proof.setAttribute("show", someProofsHidden);
proof.setAttribute("animate", "");
});
updateView();
}
function repairDom(){
// pull whitespace out of command
toArray(document.getElementsByClassName("command")).forEach(function(node){
while(node.firstChild && node.firstChild.textContent.trim() == ""){
console.log("try move");
node.parentNode.insertBefore(node.firstChild, node);
}
});
toArray(document.getElementsByClassName("id")).forEach(function(node){
node.setAttribute("type", node.getAttribute("title"));
});
toArray(document.getElementsByClassName("idref")).forEach(function(ref){
toArray(ref.childNodes).forEach(function(child){
if (["var", "variable"].indexOf(child.getAttribute("type")) > -1)
ref.removeAttribute("href");
});
});
}
function fixTitle(){
var url = "/" + window.location.pathname;
var modulename = "." + url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
modulename = modulename.substring(modulename.lastIndexOf('.')+1);
if (modulename === "toc") {modulename = "Table of Contents";}
else if (modulename === "indexpage") {modulename = "Index";}
else {modulename = modulename + ".v";};
document.title = modulename;
}
function postprocess(){
repairDom();
replInTextNodes()
replNodes();
replNotIn();
foldProofs();
document.getElementById("toggle-proofs").addEventListener("click", toggleProofs);
updateView();
}
fixTitle();
document.addEventListener('DOMContentLoaded', postprocess);
coqdocjs.toggleProofs = toggleProofs;