diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 5c3a1d8aee..b74d9dacda 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -147,6 +147,8 @@ and UExp: { let int_op_to_string: op_bin_int => string; let float_op_to_string: op_bin_float => string; let string_op_to_string: op_bin_string => string; + let bin_op_to_string: op_bin => string; + let un_op_to_string: op_un => string; } = { [@deriving (show({with_path: false}), sexp, yojson)] type op_un_bool = diff --git a/src/haz3lweb/SexpConversion.re b/src/haz3lweb/SexpConversion.re new file mode 100644 index 0000000000..548cec740d --- /dev/null +++ b/src/haz3lweb/SexpConversion.re @@ -0,0 +1,155 @@ +open Haz3lcore; +open Sexplib; + +let rec go: Term.UExp.t => Sexp.t = + term => { + switch (term.term) { + | Invalid(string) => Atom(string) + | EmptyHole => Atom("?") + | MultiHole(_) => Atom("Not implemented") + | Triv => List([]) + | Bool(bool) => Atom(string_of_bool(bool)) + | Int(int) => Atom(string_of_int(int)) + | Float(float) => Atom(string_of_float(float)) + | String(string) => Atom("\"" ++ string ++ "\"") + | ListLit(list) => List([Sexp.Atom("list")] @ List.map(go, list)) + | Parens(exp) => go(exp) + | Constructor(string) => Atom(string) + | Fun(pat, exp) => List([Atom("fun"), goUPat(pat), go(exp)]) + | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(go, list)) + | Var(t) => Atom(t) + | Let(pat, exp1, exp2) => + List([Atom("let"), List([go(exp1), go(exp2)]), goUPat(pat)]) + | TyAlias(pat, typ, exp) => + List([Atom("type"), goUTPat(pat), goTyp(typ), go(exp)]) + | Ap(func, arg) => List([go(func), go(arg)]) + | If(cond, thenBranch, elseBranch) => + List([Atom("if"), go(cond), go(thenBranch), go(elseBranch)]) + | Seq(exp1, exp2) => List([Atom("seq"), go(exp1), go(exp2)]) + | Test(t) => List([Atom("test"), go(t)]) + | Cons(head, tail) => List([Atom("cons"), go(head), go(tail)]) + | ListConcat(list1, list2) => List([Atom("@"), go(list1), go(list2)]) + | UnOp(op_un, a) => + List([Atom(TermBase.UExp.un_op_to_string(op_un)), go(a)]) + | BinOp(op_bin, a, b) => + List([Atom(TermBase.UExp.bin_op_to_string(op_bin)), go(a), go(b)]) + | Match(exp, cases) => + List([Atom("case"), go(exp), List(List.map(goRule, cases))]) + }; + } + +and goRule: ((Term.UPat.t, Term.UExp.t)) => Sexp.t = { + ((pat, exp)) => List([goUPat(pat), go(exp)]); +} + +and goUPat: Term.UPat.t => Sexp.t = + pat => { + switch (pat.term) { + | EmptyHole => Atom("?") + | Triv => List([]) + | MultiHole(_) => Atom("Not implemented") + | Int(x) => Atom(string_of_int(x)) + | Float(x) => Atom(string_of_float(x)) + | Bool(x) => Atom(string_of_bool(x)) + | String(x) => Atom("\"" ++ x ++ "\"") + | ListLit(list) => List([Sexp.Atom("list")] @ List.map(goUPat, list)) + | Cons(head, tail) => + List([Sexp.Atom("cons"), goUPat(head), goUPat(tail)]) + | Parens(pat) => goUPat(pat) + | Ap(pat1, pat2) => List([goUPat(pat1), goUPat(pat2)]) + | Invalid(string) => Atom(string) + | Var(t) => Atom(t) + | Constructor(string) => Atom(string) + | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(goUPat, list)) + | Wild => Atom("_") + | TypeAnn(pat, typ) => List([goUPat(pat), goTyp(typ)]) + }; + } + +// Only for type declarations! +and goUTPat: Term.UTPat.t => Sexp.t = + pat => { + switch (pat.term) { + | EmptyHole => Atom("?") + | MultiHole(_) => Atom("Not implemented") + | Invalid(string) => Atom(string) + | Var(string) => Atom(string) + }; + } + +and goTyp: Term.UTyp.t => Sexp.t = + typ => { + switch (typ.term) { + | EmptyHole => Atom("EmptyHole") + | MultiHole(_) => Atom("MultiHole") + | Int => Atom("Int") + | Float => Atom("Float") + | Bool => Atom("Bool") + | String => Atom("String") + | List(t) => List([Sexp.Atom("list"), goTyp(t)]) + //Atom("[" ++ Sexp.to_string_mach(goTyp(t)) ++ "]") + | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(goTyp, list)) + | Var(string) => Atom(string) + | Constructor(string) => Atom(string) + | Invalid(string) => Atom(string) + | Sum(_list) => Atom("list") //List([Sexp.Atom("sum")] @ List.map(goTyp, list)) + | Arrow(_, _) => Atom("Arrow") + | Parens(_) => Atom("Parens") + | Ap(_, _) => Atom("Ap") + }; + }; + +// Inverse of go +let rec sexp_of_uexp: Sexplib.Sexp.t => string = + sexp => { + switch (sexp) { + | Atom(string) => string + | List([Atom("fun"), pat, exp]) => + "fun " ++ sexp_of_uexp(pat) ++ " -> " ++ sexp_of_uexp(exp) + | List([Atom("case"), exp, List(cases)]) => + "case " + ++ sexp_of_uexp(exp) + ++ "\n" + ++ String.concat("\n", List.map(rule_to_string, cases)) + ++ "\nend" + | List([Atom("let"), List([exp1, exp2]), pat]) => + "let " + ++ sexp_of_uexp(pat) + ++ " = " + ++ sexp_of_uexp(exp1) + ++ " in " + ++ sexp_of_uexp(exp2) + | List([Atom("type"), pat, typ, exp]) => + "type " + ++ sexp_of_uexp(pat) + ++ " = " + ++ sexp_of_uexp(typ) + ++ " in " + ++ sexp_of_uexp(exp) + | List([Atom("if"), cond, thenBranch, elseBranch]) => + "if " + ++ sexp_of_uexp(cond) + ++ " then " + ++ sexp_of_uexp(thenBranch) + ++ " else " + ++ sexp_of_uexp(elseBranch) + | List([Atom("seq"), exp1, exp2]) => + sexp_of_uexp(exp1) ++ "; " ++ sexp_of_uexp(exp2) + | List([Atom("test"), t]) => "test " ++ sexp_of_uexp(t) + | List([Atom("cons"), head, tail]) => + sexp_of_uexp(head) ++ " :: " ++ sexp_of_uexp(tail) + | List([Atom("@"), list1, list2]) => + sexp_of_uexp(list1) ++ " @ " ++ sexp_of_uexp(list2) + | List(list) => + "(" ++ String.concat(" ", List.map(sexp_of_uexp, list)) ++ ")" + }; + } + +and rule_to_string: Sexplib.Sexp.t => string = + sexp => { + switch (sexp) { + | List([pat, exp]) => + " | " ++ sexp_of_uexp(pat) ++ " => " ++ sexp_of_uexp(exp) + | _ => failwith("expected rule") + }; + }; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 804682c202..f2fa2093b8 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -172,6 +172,7 @@ let reevaluate_post_update = (settings: Settings.t) => | DebugAction(_) | DoTheThing | StoreKey(_) + | PrintSexp | ExportPersistentData => false | MUVSyntax(_) | Benchmark(_) @@ -312,6 +313,19 @@ let rec apply = : Result.t(Model.t) => { let m: Result.t(Model.t) = switch (update) { + | PrintSexp => + let editor = model.editors |> Editors.get_editor; + // let str = Printer.to_string_selection(editor); + let zipper = Editor.get_z(editor); + let sel = zipper.selection.content; + let term = MakeTerm.go(sel) |> fst; + let sexp = SexpConversion.go(term); + let str = Sexplib.Sexp.to_string_hum(sexp); + let alt_str = SexpConversion.sexp_of_uexp(sexp); + + print_endline("PrintSexp: " ++ str); + print_endline("PrintSexp (alt): " ++ alt_str); + Ok(model); | Reset => Ok(Model.reset(model)) | Set(s_action) => let model = update_settings(s_action, model); diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index e4d75479ea..d1a50268a5 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -62,6 +62,7 @@ type benchmark_action = [@deriving (show({with_path: false}), sexp, yojson)] type t = /* meta */ + | PrintSexp | Reset | Set(settings_action) | SetMeta(set_meta) diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index c42a0a1643..4fd708998c 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2927,6 +2927,7 @@ let view = explanation, ), section(~section_clss="examples", ~title="Examples", example), + section(~section_clss="sexp-test", ~title="sexp test", example), ], ), ], diff --git a/src/haz3lweb/view/ScratchMode.re b/src/haz3lweb/view/ScratchMode.re index 2bcc7626c4..f32ce7130d 100644 --- a/src/haz3lweb/view/ScratchMode.re +++ b/src/haz3lweb/view/ScratchMode.re @@ -89,6 +89,10 @@ let download_slide_state = state => { JsUtil.download_json("hazel-scratchpad", json_data); }; +let get_sexp = _state => { + print_endline("get_sexp"); +}; + let toolbar_buttons = (~inject, state: ScratchSlide.state) => { let export_button = Widgets.button( @@ -99,6 +103,12 @@ let toolbar_buttons = (~inject, state: ScratchSlide.state) => { }, ~tooltip="Export Scratchpad", ); + let debug_button = + Widgets.button( + Icons.eye, + _ => {inject(UpdateAction.PrintSexp)}, + ~tooltip="Debug", + ); let import_button = Widgets.file_select_button( "import-scratchpad", @@ -128,5 +138,5 @@ let toolbar_buttons = (~inject, state: ScratchSlide.state) => { }, ~tooltip="Reset Scratchpad", ); - [export_button, import_button] @ [reset_button]; + [export_button, import_button, debug_button] @ [reset_button]; };