This commit is contained in:
crumbtoo
2024-03-17 09:25:29 -06:00
parent de058abc40
commit 6aae979a58
9 changed files with 2233 additions and 1 deletions

Submodule visualisers/hmvis deleted from 8371c86933

8
visualisers/hmvis/.gitignore vendored Normal file
View File

@@ -0,0 +1,8 @@
/public/js
/node_modules
/target
/.shadow-cljs
/*.iml
/.nrepl-port
/.idea

1947
visualisers/hmvis/package-lock.json generated Normal file

File diff suppressed because it is too large Load Diff

View File

@@ -0,0 +1,10 @@
{
"devDependencies": {
"shadow-cljs": "^2.26.2"
},
"dependencies": {
"ace-builds": "^1.32.7",
"react": "16.13.0",
"react-dom": "16.13.0"
}
}

View File

@@ -0,0 +1,53 @@
body {
font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, Oxygen, Ubuntu, Cantarell, 'Open Sans', 'Helvetica Neue', sans-serif;
color: green;
overflow: hidden;
}
#editor {
margin: 0;
position: absolute;
top: 0;
bottom: 0;
left: 0;
right: 0;
}
#type-check {
position: fixed;
top: 0;
left: 50%;
z-index: 2;
transform: translateX(-50%);
}
.split {
height: 100%;
width: 50%;
position: fixed;
z-index: 1;
top: 0;
overflow-x: hidden;
padding-top: 20px;
}
.left {
left: 0;
}
.right {
right: 0;
}
.annotation-wrapper
{ display: inline-block
}
.annotation-wrapper .annotation
{ display: hidden
}
.annotation-wrapper.hovering .annotation
{ display: sticky
}

View File

@@ -0,0 +1,29 @@
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="stylesheet" href="/css/main.css">
<title>Hindley-Milner</title>
<style type="text/css" media="screen">
</style>
</head>
<body>
<button id="type-check">type-check</button>
<div class="split left">
<pre id="editor">id = \x -&gt x
twice f x = f (f x)
</pre>
</div>
<div class="split right" id="output">
</div>
<script src="/js/node_modules/ace-builds/src-min-noconflict/ace.js"></script>
<script src="/js/node_modules/ace-builds/src-min-noconflict/theme-solarized_light.js"></script>
<script src="/js/main.js"></script>
</body>
</html>

View File

@@ -0,0 +1,27 @@
;; shadow-cljs configuration
{:source-paths
["src/"]
:dependencies
[[cider/cider-nrepl "0.24.0"]
[nilenso/wscljs "0.2.0"]
[org.clojure/core.match "1.1.0"]
[binaryage/oops "0.7.2"]
[reagent "0.10.0"]
[cljsjs/react "17.0.2-0"]
[cljsjs/react-dom "17.0.2-0"]
[cljsx "1.0.0"]]
:dev-http
{8020 "public"}
:builds
{:app
{:target :browser
:output-dir "public/js"
:asset-path "/js"
:modules
{:main ; becomes public/js/main.js
{:init-fn main/init}}}}}

View File

@@ -0,0 +1,90 @@
(ns hmvis.annotated
(:require [cljs.core.match :refer-macros [match]]
; [cljsx.core :refer [jsx> react> defcomponent]]
; [react :as react]
; [react-dom :as react-dom]
[reagent.core :as r]
[reagent.dom :as rdom]
[clojure.pprint :refer [cl-format]]))
(defonce tc-input (r/atom nil))
(defonce current-annotation-text (r/atom nil))
(def app-prec 10)
(def app-prec1 11)
(defn hsep [& as]
(let [f (fn [a b] (str a " " b))]
(reduce f as)))
; (defn maybe-parens [c s]
; (if c
; (react> (<> "(" s ")"))
; s))
(defn formatln [fs & rest]
(apply cl-format true (str fs "~%") rest))
(defn Typed [t & children]
(formatln "type: ~S" t)
[:div {:class "annotation-wrapper"
:onMouseEnter #(do (println "doge")
(reset! current-annotation-text "doge"))
:onMouseLeave #(reset! current-annotation-text nil)}
children])
(defn Annotation []
[:p (or @current-annotation-text "<nil>")])
(declare Expr)
(defn LambdaExpr [binds body]
[:<>
[:code
(hsep "λ" (apply hsep binds) "-> ")]
[Expr 0 body]])
(defn VarExpr [var-id]
[:code var-id])
(defn AppExpr [f x]
[:<> [Expr app-prec f]
" "
[Expr app-prec1 x]])
(defn Expr [p {e :e t :type}]
(match e
{:InL {:tag "LamF" :contents [bs body & _]}}
[LambdaExpr bs body]
{:InL {:tag "VarF" :contents var-id}}
[VarExpr var-id]
{:InL {:tag "AppF" :contents [f x]}}
[AppExpr f x]
:else [:code "<expr>"]))
(defn render-decl [{name :name body :body}]
[:code {:key name :display "block"}
(str name " = ") [Expr 0 body] #_ (render-expr body)
[:br]])
(defn Thing []
[:h1 @current-annotation-text])
(defn type-checker []
[:div
[Thing]
#_ [:button {:on-click #(reset! current-annotation-text "doge")}]])
; (defcomponent TypeChecker props
; (react>
; (<div>
; (<Thing>)
; (<button :onClick #(do (reset! current-annotation-text "doge")
; (formatln "thing: ~S" @current-annotation-text)) >)
; #_ (map render-decl (or @tc-input [])))))
(defn init []
(rdom/render [type-checker]
(js/document.querySelector "#type-check")))

View File

@@ -0,0 +1,69 @@
(ns main
(:require [clojure.spec.alpha :as s]
[wscljs.client :as ws]
[wscljs.format :as fmt]
[cljs.core.match :refer-macros [match]]
[hmvis.annotated :as annotated]
[reagent.dom :as rdom]))
(def *editor
(doto (js/ace.edit "editor")
(.setTheme "ace/theme/solarized_light")
(.setKeyboardHandler "ace/keyboard/vim")
(.setOption "mode" "ace/mode/haskell")))
(def *output (.querySelector js/document "#output"))
(defn display-errors [es]
(doseq [{{e :contents} :diagnostic} es]
(let [fmte (map #(str " • " % "\n") e)]
(js/console.warn (apply str "message from rlpc:\n" fmte)))))
(defn with-success [f ma]
(match ma
{:errors es :result nil} (display-errors es)
{:errors es :result a} (do (display-errors es)
(f a))))
(defn on-message [e]
(let [r (js->clj (js/JSON.parse (.-data e)) :keywordize-keys true)]
(match r
{:tag "Annotated" :contents c}
(with-success #(reset! annotated/tc-input %) c)
:else
(js/console.warn "unrecognisable response from rlp"))))
(def *socket (ws/create "ws://127.0.0.1:9002"
{:on-message on-message
:on-open #(println "socket opened")
:on-close #(println "socket closed")
:on-error #(println "error: " %)}))
(defn send [msg]
(ws/send *socket msg fmt/json))
(defn init-type-check-button []
(let [b (.querySelector js/document "#type-check")]
(.addEventListener b "click"
#(send {:command "annotate"
:source (.getValue *editor)}))))
;; start is called by init and after code reloading finishes
(defn ^:dev/after-load start []
; (rdom/render [type-checker] (js/document.getElementById "output"))
(annotated/init)
(js/console.log "start"))
(defn init []
(init-type-check-button)
;; init is called ONCE when the page loads
;; this is called in the index.html and must be exported
;; so it is available even in :advanced release builds
(js/console.log "init")
(start))
;; this is called before any code is reloaded
(defn ^:dev/before-load stop []
(ws/close *socket)
(js/console.log "stop"))