ericfinster · regular-citizen · May 24, 2023 · May 25, 2023 · May 29, 2023 · May 29, 2023
diff --git a/.gitignore b/.gitignore
@@ -23,4 +23,5 @@ lib/bs
 *.mliast
 .merlin
 _build/
-*.agdai
+result
+*.agdai
diff --git a/default.nix b/default.nix
@@ -0,0 +1,23 @@
+with import <nixpkgs> { };
+
+let
+  ocaml_inputs = [ dune_3 ocaml opam ] ++ (with ocamlPackages; [ fmt js_of_ocaml js_of_ocaml-ppx menhir sedlex ]);
+in
+stdenv.mkDerivation {
+  pname = "catt";
+  version = "0.2.0";
+  src = ./.;
+  buildInputs = ocaml_inputs;
+  buildPhase = ''
+    rm -rf result
+    dune build
+  '';
+  installPhase = ''
+    mkdir -p $out/bin
+    install -Dm755 _build/default/bin/catt.exe $out/bin
+    mkdir -p $out/web
+    install -Dm644 _build/default/web/index.html $out/web
+    install -Dm644 _build/default/web/*.js $out/web
+  '';
+}
+
diff --git a/lib/io.ml b/lib/io.ml
@@ -40,6 +40,25 @@ let rec parse lexbuf (checkpoint : 'a I.checkpoint) =
   | I.Rejected ->
     raise (Parse_error (None, "Invalid syntax (parser rejected the input)"))
 
+let parse_string s =
+  let lexbuf = Sedlexing.Utf8.from_string s in
+  let chkpt = Parser.Incremental.prog (fst (Sedlexing.lexing_positions lexbuf)) in
+    parse lexbuf chkpt
+
+let parse_stringify s =
+  try
+    let defs = parse_string s in
+    Printf.sprintf "Success: %d" (List.length defs)
+  with
+  | Parse_error (Some (line,pos), err) ->
+    Printf.sprintf "Parse error: %sLine: %d, Pos: %d@," err line pos
+  | Parse_error (None, err) ->
+    Printf.sprintf "Parse error: %s" err
+  | Lexer.Lexing_error (Some (line,pos), err) ->
+    Printf.sprintf "Lexing error: %s@,Line: %d, Pos: %d@," err line pos
+  | Lexer.Lexing_error (None, err) ->
+    Printf.sprintf "Lexing error: %s@," err
+
 let parse_file f =
   let fi = open_in f in
   let lexbuf = Sedlexing.Utf8.from_channel fi in

diff --git a/lib/typecheck.ml b/lib/typecheck.ml
@@ -534,7 +534,7 @@ let rec check_defs gma defs =
 let run_tc m =
   match m with
   | Ok _ ->
-    Fmt.pr "@[<v>----------------@,Success!@,@,@]"
+    Fmt.pr "@[<v>----------------@,Success!@,@,@]%!"
   | Error err ->
-     Fmt.pr "@,Typing error: @,@,%a@,@," pp_error err
+     Fmt.pr "@,Typing error: @,@,%a@,@,%!" pp_error err
 end
diff --git a/web/ace.js b/web/ace.js
diff --git a/web/cattweb.ml b/web/cattweb.ml
@@ -0,0 +1,42 @@
+(*****************************************************************************)
+(*                                                                           *)
+(*                                Web Main                                   *)
+(*                                                                           *)
+(*****************************************************************************)
+
+open Js_of_ocaml
+
+open Catt.Io
+open Catt.Reduction
+
+module W = Catt.Typecheck.Make(Weak)
+module SU = Catt.Typecheck.Make(StrictUnit.Rec)
+module SUA = Catt.Typecheck.Make(StrictUnitAssoc.Rec)
+
+let print_to_js s : unit =
+    let s = Js.string s in
+    Js.Unsafe.fun_call (Js.Unsafe.js_expr "printJS") [| Js.Unsafe.inject s |]
+
+let () = 
+    Sys_js.set_channel_flusher Stdlib.stdout print_to_js;
+    Js.export_all
+    (object%js
+      method parse s =
+          s |> Js.to_string |> parse_stringify |> Js.string
+      method typecheckweak s =
+          try
+              let defs = parse_string (Js.to_string s) in
+              W.run_tc (W.check_defs W.empty_ctx defs)
+          with _ -> Printf.printf "Failure\n%!"
+      method typechecksu s =
+          try
+              let defs = parse_string (Js.to_string s) in
+              SU.run_tc (SU.check_defs SU.empty_ctx defs)
+          with _ -> Printf.printf "Failure\n%!"
+      method typechecksua s =
+          try
+              let defs = parse_string (Js.to_string s) in
+              SUA.run_tc (SUA.check_defs SUA.empty_ctx defs)
+          with _ -> Printf.printf "Failure\n%!"
+    end)
+
diff --git a/web/dune b/web/dune
@@ -0,0 +1,7 @@
+
+(executable
+ (name cattweb)
+ (modes js)
+ (libraries catt)
+ (preprocess (pps js_of_ocaml-ppx)))
+
diff --git a/web/index.html b/web/index.html
@@ -0,0 +1,165 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+  <meta charset="UTF-8">
+  <meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1">
+  <title>Editor</title>
+  <style type="text/css" media="screen">
+    body {
+        overflow: hidden;
+    }
+
+    #editor {
+        margin: 0;
+        position: absolute;
+        top: 0;
+        bottom: 0;
+        left: 0;
+        right: 0;
+    }
+  </style>
+</head>
+<body>
+<script src="cattweb.bc.js" type="text/javascript" charset="utf-8"></script>
+<script src="ace.js" type="text/javascript" charset="utf-8"></script>
+<script src="theme-gruvbox.js" type="text/javascript" charset="utf-8"></script>
+<script type="text/javascript">
+	var buildDom = ace.require("ace/lib/dom").buildDom;
+	let options = {
+		theme: "ace/theme/gruvbox",
+		fontSize: "16px",
+		highlightActiveLine: true,
+		newLineMode: "unix",
+		minLines: 50,
+		maxLines: 50
+	};
+	var refs = {};
+	// 0 is fully strict
+	// 1 is strictly unital
+	// 2 is strictly unital and associative
+	var strictness = 0;
+
+    var editor = ace.edit();
+	editor.setOptions(options);
+
+	var output = ace.edit();
+	output.setOptions(options);
+	output.setOption("readOnly", true);
+	output.setOption("wrap", 80);
+
+	function printJS(s) {
+		output.insert(s);
+		output.gotoLine(output.session.getLength());
+	}
+
+	function updateToolbar() {
+		refs.saveButton.disabled = editor.session.getUndoManager().isClean();
+		refs.undoButton.disabled = !editor.session.getUndoManager().hasUndo();
+		refs.redoButton.disabled = !editor.session.getUndoManager().hasRedo();
+	}
+
+	function changeStrictnessMode() {
+		strictness = (strictness + 1) % 3;
+		let text = (strictness == 0 ?
+			"Mode: Weak" : (strictness == 1 ?
+			"Mode: SU" : "Mode: SUA"
+		));
+		document.getElementById("mode_button").innerText = text;
+	}
+
+	function run() {
+		// Clear output terminal
+		output.session.setValue("");
+		output.gotoLine(0);
+
+		var text = editor.getValue();
+		// OCaml code is invoked here
+		let tc_result = (strictness == 0 ?
+			typecheckweak(text) : (strictness == 1 ?
+				typechecksu(text) :	typechecksua(text)
+		));
+		console.log("Typecheck result", tc_result);
+		updateToolbar();
+	}
+
+	function save() {
+		localStorage.savedValue = editor.getValue();
+		editor.session.getUndoManager().markClean();
+		updateToolbar();
+	}
+
+	function undo() {
+		editor.undo();
+		updateToolbar();
+	}
+
+	function redo() {
+		editor.redo();
+		updateToolbar();
+	}
+
+	editor.on("input", updateToolbar);
+
+	editor.commands.addCommand({
+		name: 'run',
+		bindKey: {win: 'Ctrl-R', mac: 'Command-R'},
+		exec: function(editor) {run()},
+		readOnly: true
+	});
+	editor.commands.addCommand({
+		name: 'save',
+		bindKey: {win: 'Ctrl-S', mac: 'Command-S'},
+		exec: function(editor) {save()},
+		readOnly: true
+	});
+	editor.commands.addCommand({
+		name: 'undo',
+		bindKey: {win: 'Ctrl-Z', mac: 'Command-Z'},
+		exec: function(editor) {undo()},
+		readOnly: true
+	});
+	editor.commands.addCommand({
+		name: 'redo',
+		bindKey: {win: 'Ctrl-Shift-Z', mac: 'Command-Shift-Z'},
+		exec: function(editor) {redo()},
+		readOnly: true
+	});
+
+	buildDom([
+		"div", {}, ["div", {class: "toolbar"}, [
+			"button", {ref: "runButton", onclick: run}, "Run"
+		], [
+			"button", {ref: "saveButton", onclick: save}, "Save"
+		], [
+			"button", {ref: "undoButton", onclick: undo}, "Undo"
+		], [
+			"button", {ref: "redoButton", onclick: redo}, "Redo"
+		], [
+			"button", {ref: "modeButton", onclick: changeStrictnessMode, id: "mode_button"}, "Mode: Weak"
+		]
+	], [
+		"div", {id: "main", style: "display: flex; flex-direction: row; gap: 0.5rem"}, [
+			"div", {id: "main_editor", style: "flex-grow: 1"}, []
+		], [
+			"div", {id: "main_output", style: "flex-grow: 1"}, []
+	]]], document.body, refs);
+	document.getElementById("main_editor").appendChild(editor.container);
+	document.getElementById("main_output").appendChild(output.container);
+
+	let default_text = ["",
+		"coh id (x) : x => x",
+		"coh id1 (x(f)y) : f => f", "",
+		"coh comp (x(f)y(g)z) : x => z",
+		"coh comp2 (x(f(a)g(b)h)z) : f => h", "",
+		"coh assoc (x(f)y(g)z(h)w) : (comp f (comp g h)) => (comp (comp f g) h)",
+		"coh whiskr (x(f(a)g)y(h)z) : (comp f h) => (comp g h)", "",
+		"normalize (x(f(a)g)y(h)z(j)w)",
+		"  | (comp2 (whiskr a (comp h (comp (id z) j))) (assoc g h (comp (id z) j)))", ""
+	].join("\n");
+	editor.session.setValue(localStorage.savedValue || default_text);
+	output.session.setValue(
+		"Typechecker output is shown here!"
+	);
+</script>
+</body>
+</html>
diff --git a/web/theme-gruvbox.js b/web/theme-gruvbox.js
-Original file line number
+Diff line change
@@ Expand Up / @@ -23,4 +23,5 @@ lib/bs @@
     *.mliast
     .merlin
     _build/
-    *.agdai
+    result
+    *.agdai