From 959a4ba4b1d6c31b11e7a88bc226b85ed2f9287d Mon Sep 17 00:00:00 2001 From: Gregory Croisdale Date: Tue, 16 Jul 2024 17:08:36 -0400 Subject: [PATCH 1/5] added initial SexpConversion function --- src/haz3lcore/zipper/Touched.re | 4 +++- src/haz3lweb/SexpConversion.re | 40 ++++++++++++++++++++++++++++++++ src/haz3lweb/Update.re | 12 ++++++++++ src/haz3lweb/UpdateAction.re | 1 + src/haz3lweb/util/JsUtil.re | 3 +-- src/haz3lweb/util/WeakMap.re | 6 ++--- src/haz3lweb/view/LangDoc.re | 1 + src/haz3lweb/view/ScratchMode.re | 12 +++++++++- src/lwtutil/Lwt_timed.re | 8 +++++-- src/pretty/Box.rei | 4 +++- src/pretty/MeasuredLayout.rei | 4 +++- src/util/Monads.re | 2 +- src/util/StateMonad.re | 4 +++- src/util/StateMonad.rei | 4 +++- 14 files changed, 90 insertions(+), 15 deletions(-) create mode 100644 src/haz3lweb/SexpConversion.re diff --git a/src/haz3lcore/zipper/Touched.re b/src/haz3lcore/zipper/Touched.re index 70644f9c2b..2a428deb28 100644 --- a/src/haz3lcore/zipper/Touched.re +++ b/src/haz3lcore/zipper/Touched.re @@ -1,7 +1,9 @@ include Id.Map; type t = Id.Map.t(Time.t); -module type S = {let touched: t;}; +module type S = { + let touched: t; +}; let update = (t: Time.t, es: list(Effect.t), td: t) => es diff --git a/src/haz3lweb/SexpConversion.re b/src/haz3lweb/SexpConversion.re new file mode 100644 index 0000000000..489ae5d859 --- /dev/null +++ b/src/haz3lweb/SexpConversion.re @@ -0,0 +1,40 @@ +open Haz3lcore; +open Sexplib; + +let rec go: Term.UExp.t => Sexp.t = + term => { + switch (term.term) { + // | Invalid(string) + // | EmptyHole + // | MultiHole(list(Any.t)) + | 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)) + // | Constructor(string) + // | Fun(UPat.t, t) + // | Tuple(list(t)) + // | Var(Var.t) + // | Let(UPat.t, t, t) + // | TyAlias(UTPat.t, UTyp.t, t) + // | Ap(t, t) + // | If(t, t, t) + // | Seq(t, t) + // | Test(t) + // | Parens(t) // ( + // | Cons(t, t) + // | ListConcat(t, t) + // | UnOp(op_un, t) + // | BinOp(op_bin, t, t) + // | Match(t, list((UPat.t, t))) + | _ => + print_endline(Term.UExp.show(term)); + Atom("Not implemented"); + }; + }; + +// likely need UPat, UType, UTPat to Sexp + +// ? for empty hole \ No newline at end of file diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 804682c202..355052b578 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,17 @@ 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); + + print_endline("PrintSexp: " ++ 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/util/JsUtil.re b/src/haz3lweb/util/JsUtil.re index 7a3852ff1e..acd2b609e1 100644 --- a/src/haz3lweb/util/JsUtil.re +++ b/src/haz3lweb/util/JsUtil.re @@ -11,8 +11,7 @@ let get_elem_by_id = id => { }; let date_now = () => { - %js - new Js.date_now; + [%js new Js.date_now]; }; let timestamp = () => date_now()##valueOf; diff --git a/src/haz3lweb/util/WeakMap.re b/src/haz3lweb/util/WeakMap.re index edf5fda68d..a3ab0951a9 100644 --- a/src/haz3lweb/util/WeakMap.re +++ b/src/haz3lweb/util/WeakMap.re @@ -16,8 +16,7 @@ module JsMap = { let mk: 'k 'v. unit => t('k, 'v) = () => { let c = Js.Unsafe.global##._Map; - %js - new c; + [%js new c]; }; }; @@ -27,8 +26,7 @@ module JsWeakMap = { let mk: 'k 'v. unit => t('k, 'v) = () => { let c = Js.Unsafe.global##._WeakMap; - %js - new c; + [%js new c]; }; }; 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]; }; diff --git a/src/lwtutil/Lwt_timed.re b/src/lwtutil/Lwt_timed.re index 5eeca72433..e17b77e5f8 100644 --- a/src/lwtutil/Lwt_timed.re +++ b/src/lwtutil/Lwt_timed.re @@ -1,8 +1,12 @@ open Lwt.Infix; -module type TIMER = {let delay: (unit => unit, int) => unit;}; +module type TIMER = { + let delay: (unit => unit, int) => unit; +}; -module type S = {let wrap: (int, Lwt.t('a)) => Lwt.t(option('a));}; +module type S = { + let wrap: (int, Lwt.t('a)) => Lwt.t(option('a)); +}; exception TimedOut; module Make = (T: TIMER) => { diff --git a/src/pretty/Box.rei b/src/pretty/Box.rei index f19613be50..67bb197242 100644 --- a/src/pretty/Box.rei +++ b/src/pretty/Box.rei @@ -29,4 +29,6 @@ type t('annot) = | VBox(list(t('annot))) | Annot('annot, t('annot)); -module Make: (MemoTbl.S) => {let mk: Layout.t('annot) => t('annot);}; +module Make: (MemoTbl.S) => { + let mk: Layout.t('annot) => t('annot); + }; diff --git a/src/pretty/MeasuredLayout.rei b/src/pretty/MeasuredLayout.rei index 8ebc6dbf74..428cbb85e6 100644 --- a/src/pretty/MeasuredLayout.rei +++ b/src/pretty/MeasuredLayout.rei @@ -97,4 +97,6 @@ let pos_fold: let next_position: (~indent: int, MeasuredPosition.t, t(_)) => MeasuredPosition.t; -module Make: (MemoTbl.S) => {let mk: Layout.t('annot) => t('annot);}; +module Make: (MemoTbl.S) => { + let mk: Layout.t('annot) => t('annot); + }; diff --git a/src/util/Monads.re b/src/util/Monads.re index 394f695a0e..dea4a3f872 100644 --- a/src/util/Monads.re +++ b/src/util/Monads.re @@ -74,4 +74,4 @@ module Make_Monad_Z = (M: MONAD_ZIP) => { }; module Make_Monad_B = (M: MONAD_BASIC) => - Make_Monad_Z((Make_Zip((Make_Functor(M))))); + Make_Monad_Z(Make_Zip(Make_Functor(M))); diff --git a/src/util/StateMonad.re b/src/util/StateMonad.re index b86fb19fe9..3209f9c1cd 100644 --- a/src/util/StateMonad.re +++ b/src/util/StateMonad.re @@ -1,4 +1,6 @@ -module type STATE = {type t;}; +module type STATE = { + type t; +}; module type S = { type state; diff --git a/src/util/StateMonad.rei b/src/util/StateMonad.rei index 96eed96261..42a668f00e 100644 --- a/src/util/StateMonad.rei +++ b/src/util/StateMonad.rei @@ -5,7 +5,9 @@ /** State type module specification. */ -module type STATE = {type t;}; +module type STATE = { + type t; +}; /** Output of the functor [Make]. From c12ac5f75ef018f687a9a16bc9764852562ad395 Mon Sep 17 00:00:00 2001 From: Gregory Croisdale Date: Thu, 18 Jul 2024 01:24:57 -0400 Subject: [PATCH 2/5] added helper funcs, several matches --- src/haz3lweb/SexpConversion.re | 102 ++++++++++++++++++++++++++------- 1 file changed, 82 insertions(+), 20 deletions(-) diff --git a/src/haz3lweb/SexpConversion.re b/src/haz3lweb/SexpConversion.re index 489ae5d859..fda3b74bde 100644 --- a/src/haz3lweb/SexpConversion.re +++ b/src/haz3lweb/SexpConversion.re @@ -4,7 +4,7 @@ open Sexplib; let rec go: Term.UExp.t => Sexp.t = term => { switch (term.term) { - // | Invalid(string) + | Invalid(string) => Atom("Invalid: " ++ string) // | EmptyHole // | MultiHole(list(Any.t)) | Triv => List([]) @@ -13,28 +13,90 @@ let rec go: Term.UExp.t => Sexp.t = | Float(float) => Atom(string_of_float(float)) | String(string) => Atom(string) | ListLit(list) => List([Sexp.Atom("list")] @ List.map(go, list)) - // | Constructor(string) - // | Fun(UPat.t, t) - // | Tuple(list(t)) - // | Var(Var.t) - // | Let(UPat.t, t, t) - // | TyAlias(UTPat.t, UTyp.t, t) - // | Ap(t, t) - // | If(t, t, t) - // | Seq(t, t) - // | Test(t) - // | Parens(t) // ( - // | Cons(t, t) - // | ListConcat(t, t) - // | UnOp(op_un, t) - // | BinOp(op_bin, t, t) - // | Match(t, list((UPat.t, t))) + | 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("tyAlias"), 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("listConcat"), go(list1), go(list2)]) + // TODO: how to access TermBase.re un_op_to_string? + | UnOp(_op_un, a) => List([Atom("op_un"), go(a)]) + // | BinOp(op_bin, a, b) => List([Atom("op_bin"), go(a), go(b)]) + // | Match(exp, [pat, cases]) => + // List([Atom("match"), go(exp), List([goUPat(pat), go(cases)])]) | _ => print_endline(Term.UExp.show(term)); - Atom("Not implemented"); + Atom("Not implemented"); /* ? for empty hol*/ }; - }; + } // likely need UPat, UType, UTPat to Sexp +// (EmptyHole|Wild|Triv|MultiHole _|Int _|Float _|Bool _|String _|ListLit _| Cons (_, _)|Parens _|Ap (_, _)|TypeAnn (_, _))ocamllsp +and goUPat: Term.UPat.t => Sexp.t = + pat => { + switch (pat.term) { + | EmptyHole => Atom("EmptyHole") + | Wild => Atom("Wild") + | Triv => Atom("Triv") + | MultiHole(_) => Atom("MultiHole") + | Int(_) => Atom("Int") + | Float(_) => Atom("Float") + | Bool(_) => Atom("Bool") + | String(_) => Atom("String") + | ListLit(_) => Atom("ListPat") + | Cons(_, _) => Atom("Cons") + | Parens(_) => Atom("Parens") + | Ap(_, _) => Atom("Ap") + | TypeAnn(_, _) => Atom("TypeAnn") + | Invalid(string) => Atom("Invalid: " ++ string) + | Var(string) => Atom(string) + | Constructor(string) => Atom(string) + | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(goUPat, list)) + }; + } + +and goUTPat: Term.UTPat.t => Sexp.t = + pat => { + switch (pat.term) { + | EmptyHole => Atom("EmptyHole") + | MultiHole(_) => Atom("MultiHole") + | Invalid(string) => Atom("Invalid: " ++ string) + | Var(string) => Atom(string) + }; + } -// ? for empty hole \ No newline at end of file +and goTyp: Term.UTyp.t => Sexp.t = + typ => { + switch (typ.term) { + | EmptyHole => Atom("EmptyHole") + // | Wild => Atom("Wild") + // | Triv => Atom("Triv") + | MultiHole(_) => Atom("MultiHole") + | Int => Atom("Int") + | Float => Atom("Float") + | Bool => Atom("Bool") + | String => Atom("String") + | List(_) => Atom("List") + | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(goTyp, list)) + // | Fun(_, _) => Atom("Fun") + | Var(string) => Atom(string) + | Constructor(string) => Atom(string) + // | TypeApp(_, _) => Atom("TypeApp") + // | TypeAnn(_, _) => Atom("TypeAnn") + | Invalid(string) => Atom("Invalid: " ++ string) + | Sum(_list) => Atom("list") //List([Sexp.Atom("sum")] @ List.map(goTyp, list)) + | Arrow(_, _) => Atom("Arrow") + | Parens(_) => Atom("Parens") + | Ap(_, _) => Atom("Ap") + }; + }; From aa78e0216593505a889c07cd49da3430e66ba45f Mon Sep 17 00:00:00 2001 From: Gregory Croisdale Date: Thu, 18 Jul 2024 18:31:58 -0400 Subject: [PATCH 3/5] added all cases for base UExp, began reversal function --- src/haz3lcore/statics/TermBase.re | 2 + src/haz3lweb/SexpConversion.re | 93 ++++++++++++++++++++----------- src/haz3lweb/Update.re | 2 + 3 files changed, 65 insertions(+), 32 deletions(-) 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 index fda3b74bde..464ce9decc 100644 --- a/src/haz3lweb/SexpConversion.re +++ b/src/haz3lweb/SexpConversion.re @@ -4,15 +4,16 @@ open Sexplib; let rec go: Term.UExp.t => Sexp.t = term => { switch (term.term) { - | Invalid(string) => Atom("Invalid: " ++ string) - // | EmptyHole - // | MultiHole(list(Any.t)) + | 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) + | 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)) @@ -20,51 +21,53 @@ let rec go: Term.UExp.t => Sexp.t = | Let(pat, exp1, exp2) => List([Atom("let"), List([go(exp1), go(exp2)]), goUPat(pat)]) | TyAlias(pat, typ, exp) => - List([Atom("tyAlias"), goUTPat(pat), goTyp(typ), go(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("listConcat"), go(list1), go(list2)]) - // TODO: how to access TermBase.re un_op_to_string? - | UnOp(_op_un, a) => List([Atom("op_un"), go(a)]) - // | BinOp(op_bin, a, b) => List([Atom("op_bin"), go(a), go(b)]) - // | Match(exp, [pat, cases]) => - // List([Atom("match"), go(exp), List([goUPat(pat), go(cases)])]) - | _ => - print_endline(Term.UExp.show(term)); - Atom("Not implemented"); /* ? for empty hol*/ + | 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))]) }; } -// likely need UPat, UType, UTPat to Sexp -// (EmptyHole|Wild|Triv|MultiHole _|Int _|Float _|Bool _|String _|ListLit _| Cons (_, _)|Parens _|Ap (_, _)|TypeAnn (_, _))ocamllsp +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("EmptyHole") - | Wild => Atom("Wild") - | Triv => Atom("Triv") - | MultiHole(_) => Atom("MultiHole") - | Int(_) => Atom("Int") - | Float(_) => Atom("Float") - | Bool(_) => Atom("Bool") - | String(_) => Atom("String") - | ListLit(_) => Atom("ListPat") - | Cons(_, _) => Atom("Cons") - | Parens(_) => Atom("Parens") - | Ap(_, _) => Atom("Ap") - | TypeAnn(_, _) => Atom("TypeAnn") - | Invalid(string) => Atom("Invalid: " ++ string) - | Var(string) => Atom(string) + | 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)]) + // | _ => Atom("Not implemented") }; } +// Only for type declarations! and goUTPat: Term.UTPat.t => Sexp.t = pat => { switch (pat.term) { @@ -100,3 +103,29 @@ and goTyp: Term.UTyp.t => Sexp.t = | Ap(_, _) => Atom("Ap") }; }; + +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(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 355052b578..f2fa2093b8 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -321,8 +321,10 @@ let rec apply = 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) => From ec9fd77b15a8116990b464eafd4c99ce27be6a72 Mon Sep 17 00:00:00 2001 From: Gregory Croisdale Date: Fri, 19 Jul 2024 00:09:44 -0400 Subject: [PATCH 4/5] filled all utyp cases, more sexp_of_uexp --- src/haz3lweb/SexpConversion.re | 46 ++++++++++++++++++++++++++-------- 1 file changed, 35 insertions(+), 11 deletions(-) diff --git a/src/haz3lweb/SexpConversion.re b/src/haz3lweb/SexpConversion.re index 464ce9decc..548cec740d 100644 --- a/src/haz3lweb/SexpConversion.re +++ b/src/haz3lweb/SexpConversion.re @@ -63,7 +63,6 @@ and goUPat: Term.UPat.t => Sexp.t = | Tuple(list) => List([Sexp.Atom("tuple")] @ List.map(goUPat, list)) | Wild => Atom("_") | TypeAnn(pat, typ) => List([goUPat(pat), goTyp(typ)]) - // | _ => Atom("Not implemented") }; } @@ -71,9 +70,9 @@ and goUPat: Term.UPat.t => Sexp.t = and goUTPat: Term.UTPat.t => Sexp.t = pat => { switch (pat.term) { - | EmptyHole => Atom("EmptyHole") - | MultiHole(_) => Atom("MultiHole") - | Invalid(string) => Atom("Invalid: " ++ string) + | EmptyHole => Atom("?") + | MultiHole(_) => Atom("Not implemented") + | Invalid(string) => Atom(string) | Var(string) => Atom(string) }; } @@ -82,21 +81,17 @@ and goTyp: Term.UTyp.t => Sexp.t = typ => { switch (typ.term) { | EmptyHole => Atom("EmptyHole") - // | Wild => Atom("Wild") - // | Triv => Atom("Triv") | MultiHole(_) => Atom("MultiHole") | Int => Atom("Int") | Float => Atom("Float") | Bool => Atom("Bool") | String => Atom("String") - | List(_) => Atom("List") + | 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)) - // | Fun(_, _) => Atom("Fun") | Var(string) => Atom(string) | Constructor(string) => Atom(string) - // | TypeApp(_, _) => Atom("TypeApp") - // | TypeAnn(_, _) => Atom("TypeAnn") - | Invalid(string) => Atom("Invalid: " ++ string) + | Invalid(string) => Atom(string) | Sum(_list) => Atom("list") //List([Sexp.Atom("sum")] @ List.map(goTyp, list)) | Arrow(_, _) => Atom("Arrow") | Parens(_) => Atom("Parens") @@ -104,6 +99,7 @@ and goTyp: Term.UTyp.t => Sexp.t = }; }; +// Inverse of go let rec sexp_of_uexp: Sexplib.Sexp.t => string = sexp => { switch (sexp) { @@ -116,6 +112,34 @@ let rec sexp_of_uexp: Sexplib.Sexp.t => string = ++ "\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)) ++ ")" }; From bbf23cc061f9241f84b30b9089f72ba3e47a603c Mon Sep 17 00:00:00 2001 From: Gregory Croisdale Date: Wed, 24 Jul 2024 22:44:24 -0400 Subject: [PATCH 5/5] updated deps (for hopeful gh actions build?) --- src/haz3lcore/zipper/Touched.re | 4 +--- src/haz3lweb/util/JsUtil.re | 3 ++- src/haz3lweb/util/WeakMap.re | 6 ++++-- src/lwtutil/Lwt_timed.re | 8 ++------ src/pretty/Box.rei | 4 +--- src/pretty/MeasuredLayout.rei | 4 +--- src/util/Monads.re | 2 +- src/util/StateMonad.re | 4 +--- src/util/StateMonad.rei | 4 +--- 9 files changed, 14 insertions(+), 25 deletions(-) diff --git a/src/haz3lcore/zipper/Touched.re b/src/haz3lcore/zipper/Touched.re index 2a428deb28..70644f9c2b 100644 --- a/src/haz3lcore/zipper/Touched.re +++ b/src/haz3lcore/zipper/Touched.re @@ -1,9 +1,7 @@ include Id.Map; type t = Id.Map.t(Time.t); -module type S = { - let touched: t; -}; +module type S = {let touched: t;}; let update = (t: Time.t, es: list(Effect.t), td: t) => es diff --git a/src/haz3lweb/util/JsUtil.re b/src/haz3lweb/util/JsUtil.re index acd2b609e1..7a3852ff1e 100644 --- a/src/haz3lweb/util/JsUtil.re +++ b/src/haz3lweb/util/JsUtil.re @@ -11,7 +11,8 @@ let get_elem_by_id = id => { }; let date_now = () => { - [%js new Js.date_now]; + %js + new Js.date_now; }; let timestamp = () => date_now()##valueOf; diff --git a/src/haz3lweb/util/WeakMap.re b/src/haz3lweb/util/WeakMap.re index a3ab0951a9..edf5fda68d 100644 --- a/src/haz3lweb/util/WeakMap.re +++ b/src/haz3lweb/util/WeakMap.re @@ -16,7 +16,8 @@ module JsMap = { let mk: 'k 'v. unit => t('k, 'v) = () => { let c = Js.Unsafe.global##._Map; - [%js new c]; + %js + new c; }; }; @@ -26,7 +27,8 @@ module JsWeakMap = { let mk: 'k 'v. unit => t('k, 'v) = () => { let c = Js.Unsafe.global##._WeakMap; - [%js new c]; + %js + new c; }; }; diff --git a/src/lwtutil/Lwt_timed.re b/src/lwtutil/Lwt_timed.re index e17b77e5f8..5eeca72433 100644 --- a/src/lwtutil/Lwt_timed.re +++ b/src/lwtutil/Lwt_timed.re @@ -1,12 +1,8 @@ open Lwt.Infix; -module type TIMER = { - let delay: (unit => unit, int) => unit; -}; +module type TIMER = {let delay: (unit => unit, int) => unit;}; -module type S = { - let wrap: (int, Lwt.t('a)) => Lwt.t(option('a)); -}; +module type S = {let wrap: (int, Lwt.t('a)) => Lwt.t(option('a));}; exception TimedOut; module Make = (T: TIMER) => { diff --git a/src/pretty/Box.rei b/src/pretty/Box.rei index 67bb197242..f19613be50 100644 --- a/src/pretty/Box.rei +++ b/src/pretty/Box.rei @@ -29,6 +29,4 @@ type t('annot) = | VBox(list(t('annot))) | Annot('annot, t('annot)); -module Make: (MemoTbl.S) => { - let mk: Layout.t('annot) => t('annot); - }; +module Make: (MemoTbl.S) => {let mk: Layout.t('annot) => t('annot);}; diff --git a/src/pretty/MeasuredLayout.rei b/src/pretty/MeasuredLayout.rei index 428cbb85e6..8ebc6dbf74 100644 --- a/src/pretty/MeasuredLayout.rei +++ b/src/pretty/MeasuredLayout.rei @@ -97,6 +97,4 @@ let pos_fold: let next_position: (~indent: int, MeasuredPosition.t, t(_)) => MeasuredPosition.t; -module Make: (MemoTbl.S) => { - let mk: Layout.t('annot) => t('annot); - }; +module Make: (MemoTbl.S) => {let mk: Layout.t('annot) => t('annot);}; diff --git a/src/util/Monads.re b/src/util/Monads.re index dea4a3f872..394f695a0e 100644 --- a/src/util/Monads.re +++ b/src/util/Monads.re @@ -74,4 +74,4 @@ module Make_Monad_Z = (M: MONAD_ZIP) => { }; module Make_Monad_B = (M: MONAD_BASIC) => - Make_Monad_Z(Make_Zip(Make_Functor(M))); + Make_Monad_Z((Make_Zip((Make_Functor(M))))); diff --git a/src/util/StateMonad.re b/src/util/StateMonad.re index 3209f9c1cd..b86fb19fe9 100644 --- a/src/util/StateMonad.re +++ b/src/util/StateMonad.re @@ -1,6 +1,4 @@ -module type STATE = { - type t; -}; +module type STATE = {type t;}; module type S = { type state; diff --git a/src/util/StateMonad.rei b/src/util/StateMonad.rei index 42a668f00e..96eed96261 100644 --- a/src/util/StateMonad.rei +++ b/src/util/StateMonad.rei @@ -5,9 +5,7 @@ /** State type module specification. */ -module type STATE = { - type t; -}; +module type STATE = {type t;}; /** Output of the functor [Make].