From ad64b124850fbcad7503b51cdb26428fbf4d13cf Mon Sep 17 00:00:00 2001 From: jaehyun1ee <99jaehyunlee@kaist.ac.kr> Date: Wed, 17 Jul 2024 17:25:44 +0900 Subject: [PATCH 1/2] Render inverse functions in prose, without ^(-1) --- spectec/src/al/ast.ml | 80 ++++++++-------- spectec/src/al/print.ml | 2 + spectec/src/backend-prose/render.ml | 144 ++++++++++++++++++---------- spectec/src/il2al/translate.ml | 9 +- 4 files changed, 139 insertions(+), 96 deletions(-) diff --git a/spectec/src/al/ast.ml b/spectec/src/al/ast.ml index 3a3cb9a59e..b79f77de36 100644 --- a/spectec/src/al/ast.ml +++ b/spectec/src/al/ast.ml @@ -75,49 +75,49 @@ type iter = and expr = (expr', Il.Ast.typ) note_phrase and expr' = - | VarE of id (* varid *) - | NumE of Z.t (* number *) - | BoolE of bool (* boolean *) - | UnE of unop * expr (* unop expr *) - | BinE of binop * expr * expr (* expr binop expr *) - | AccE of expr * path (* expr `[` path `]` *) - | UpdE of expr * path list * expr (* expr `[` path* `]` `:=` expr *) - | ExtE of expr * path list * expr * extend_dir (* expr `[` path* `]` `:+` expr *) - | StrE of (atom, expr) record (* `{` (atom `->` expr)* `}` *) - | CatE of expr * expr (* expr `++` expr *) - | MemE of expr * expr (* expr `<-` expr *) - | LenE of expr (* `|` expr `|` *) - | TupE of expr list (* `(` (expr `,`)* `)` *) - | CaseE of atom * expr list (* atom `(` expr* `)` -- MixE/CaseE *) - | CallE of id * expr list (* id `(` expr* `)` *) - | InvCallE of id * int list * expr list (* id`_`int*`^-1(` expr* `)` *) - | IterE of expr * id list * iter (* expr (`{` id* `}`)* *) - | OptE of expr option (* expr? *) - | ListE of expr list (* `[` expr* `]` *) - | InfixE of expr * atom * expr (* "expr infix expr" *) (* TODO: Remove InfixE using hint *) - | ArityE of expr (* "the arity of expr" *) - | FrameE of expr option * expr (* "the activation of expr (with arity expr)?" *) - | LabelE of expr * expr (* "the label whose arity is expr and whose continuation is expr" *) - | GetCurStateE (* "the current state" *) - | GetCurFrameE (* "the current frame" *) - | GetCurLabelE (* "the current lbael" *) - | GetCurContextE (* "the current context" *) - | ContE of expr (* "the continuation of expr" *) + | VarE of id (* varid *) + | NumE of Z.t (* number *) + | BoolE of bool (* boolean *) + | UnE of unop * expr (* unop expr *) + | BinE of binop * expr * expr (* expr binop expr *) + | AccE of expr * path (* expr `[` path `]` *) + | UpdE of expr * path list * expr (* expr `[` path* `]` `:=` expr *) + | ExtE of expr * path list * expr * extend_dir (* expr `[` path* `]` `:+` expr *) + | StrE of (atom, expr) record (* `{` (atom `->` expr)* `}` *) + | CatE of expr * expr (* expr `++` expr *) + | MemE of expr * expr (* expr `<-` expr *) + | LenE of expr (* `|` expr `|` *) + | TupE of expr list (* `(` (expr `,`)* `)` *) + | CaseE of atom * expr list (* atom `(` expr* `)` -- MixE/CaseE *) + | CallE of id * expr list (* id `(` expr* `)` *) + | InvCallE of id * int option list * expr list (* id`_`int*`^-1(` expr* `)` *) + | IterE of expr * id list * iter (* expr (`{` id* `}`)* *) + | OptE of expr option (* expr? *) + | ListE of expr list (* `[` expr* `]` *) + | InfixE of expr * atom * expr (* "expr infix expr" *) (* TODO: Remove InfixE using hint *) + | ArityE of expr (* "the arity of expr" *) + | FrameE of expr option * expr (* "the activation of expr (with arity expr)?" *) + | LabelE of expr * expr (* "the label whose arity is expr and whose continuation is expr" *) + | GetCurStateE (* "the current state" *) + | GetCurFrameE (* "the current frame" *) + | GetCurLabelE (* "the current lbael" *) + | GetCurContextE (* "the current context" *) + | ContE of expr (* "the continuation of expr" *) (* Conditions *) - | IsCaseOfE of expr * atom (* expr is of the case kwd *) - | IsValidE of expr (* expr is valid *) - | ContextKindE of atom * expr (* TODO: desugar using IsCaseOf? *) - | IsDefinedE of expr (* expr is defined *) - | MatchE of expr * expr (* expr matches expr *) - | HasTypeE of expr * ty (* the type of expr is ty *) - | TopFrameE (* "a frame is now on the top of the stack" *) - | TopLabelE (* "a label is now on the top of the stack" *) + | IsCaseOfE of expr * atom (* expr is of the case kwd *) + | IsValidE of expr (* expr is valid *) + | ContextKindE of atom * expr (* TODO: desugar using IsCaseOf? *) + | IsDefinedE of expr (* expr is defined *) + | MatchE of expr * expr (* expr matches expr *) + | HasTypeE of expr * ty (* the type of expr is ty *) + | TopFrameE (* "a frame is now on the top of the stack" *) + | TopLabelE (* "a label is now on the top of the stack" *) (* Conditions used in assertions *) - | TopValueE of expr option (* "a value (of type expr)? is now on the top of the stack" *) - | TopValuesE of expr (* "at least expr number of values on the top of the stack" *) + | TopValueE of expr option (* "a value (of type expr)? is now on the top of the stack" *) + | TopValuesE of expr (* "at least expr number of values on the top of the stack" *) (* Administrative Instructions *) - | SubE of id * ty (* varid, with specific type *) - | YetE of string (* for future not yet implemented feature *) + | SubE of id * ty (* varid, with specific type *) + | YetE of string (* for future not yet implemented feature *) and path = path' phrase and path' = diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml index 05f00fe4d9..72ed37e687 100644 --- a/spectec/src/al/print.ml +++ b/spectec/src/al/print.ml @@ -148,6 +148,7 @@ and string_of_expr expr = if List.length nl = 0 then id else nl + |> List.filter_map (fun x -> x) |> List.map string_of_int |> List.fold_left (^) "" |> sprintf "%s_%s" id @@ -433,6 +434,7 @@ and structured_string_of_expr expr = | TupE el -> "TupE (" ^ structured_string_of_exprs el ^ ")" | CallE (id, el) -> "CallE (" ^ id ^ ", [ " ^ structured_string_of_exprs el ^ " ])" | InvCallE (id, nl, el) -> + let nl = List.filter_map (fun x -> x) nl in sprintf "InvCallE (%s, [%s], [%s])" id (string_of_list string_of_int "" nl) (structured_string_of_exprs el) | CatE (e1, e2) -> diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml index 7846ccc886..b6b43b987e 100644 --- a/spectec/src/backend-prose/render.ml +++ b/spectec/src/backend-prose/render.ml @@ -27,6 +27,65 @@ let env inputs outputs render_latex el prose : env = let env = { prose; render_latex; symbol; macro; } in env +(* Helpers *) + +let indent = " " + +let rec repeat str num = + if num = 0 then "" + else if Int.rem num 2 = 0 then repeat (str ^ str) (num / 2) + else str ^ repeat (str ^ str) (num / 2) + +let math = ":math:" + +let render_math s = + if (String.length s > 0) then math ^ sprintf "`%s`" s + else s + +let render_opt prefix stringifier suffix = function + | None -> "" + | Some x -> prefix ^ stringifier x ^ suffix + +let render_order index depth = + index := !index + 1; + + let num_idx = if !index = 1 then string_of_int !index else "#" in + let alp_idx = if !index = 1 then Char.escaped (Char.chr (96 + !index)) else "#" in + + match depth mod 4 with + | 0 -> num_idx ^ "." + | 1 -> alp_idx ^ "." + | 2 -> num_idx ^ ")" + | 3 -> alp_idx ^ ")" + | _ -> assert false + +(* Translation from Al inverse call exp to Al binary exp *) + +let al_invcalle_to_al_bine e id nl el = + let efree = (match e.it with Al.Ast.TupE el -> el | _ -> [ e ]) in + let ebound, erhs = + let nbound = List.length nl - List.length efree in + Util.Lib.List.split nbound el + in + let eargs, _, _ = + List.fold_left + (fun (eargs, efree, ebound) n -> + match n with + | Some _ -> (match efree with + | e :: efree -> eargs @ [ e ], efree, ebound + | _ -> assert false) + | None -> (match ebound with + | e :: ebound -> eargs @ [ e ], efree, ebound + | _ -> assert false)) + ([], efree, ebound) nl + in + let elhs = Al.Al_util.callE (id, eargs) in + let erhs = (match erhs with + | [ e ] -> e + | _ -> Al.Al_util.tupE erhs) + in + elhs, erhs + (* Translation from Al exp to El exp *) let (let*) = Option.bind @@ -105,26 +164,6 @@ and al_to_el_expr expr = elel in Some (El.Ast.CallE (elid, elel)) - | Al.Ast.InvCallE (id, nl, el) -> - let ($~) at it = it $ at in - let elid = - if List.length nl = 0 then - (id^"^-1") $ no_region - else - nl - |> List.map string_of_int - |> List.fold_left (^) "" - |> sprintf "%s_%s^-1" id - |> ($~) no_region - in - let* elel = al_to_el_exprs el in - let elel = List.map - (fun ele -> - let elarg = El.Ast.ExpA ele in - (ref elarg) $ no_region) - elel - in - Some (El.Ast.CallE (elid, elel)) | Al.Ast.CatE (e1, e2) -> let* ele1 = al_to_el_expr e1 in let* ele2 = al_to_el_expr e2 in @@ -213,38 +252,6 @@ and al_to_el_record record = Some (expfield @ [ elelem ])) record (Some []) -(* Helpers *) - -let indent = " " - -let rec repeat str num = - if num = 0 then "" - else if Int.rem num 2 = 0 then repeat (str ^ str) (num / 2) - else str ^ repeat (str ^ str) (num / 2) - -let math = ":math:" - -let render_math s = - if (String.length s > 0) then math ^ sprintf "`%s`" s - else s - -let render_opt prefix stringifier suffix = function - | None -> "" - | Some x -> prefix ^ stringifier x ^ suffix - -let render_order index depth = - index := !index + 1; - - let num_idx = if !index = 1 then string_of_int !index else "#" in - let alp_idx = if !index = 1 then Char.escaped (Char.chr (96 + !index)) else "#" in - - match depth mod 4 with - | 0 -> num_idx ^ "." - | 1 -> alp_idx ^ "." - | 2 -> num_idx ^ ")" - | 3 -> alp_idx ^ ")" - | _ -> assert false - (* Operators *) let render_prose_cmpop = function @@ -346,6 +353,23 @@ and render_expr' env expr = (match dir with | Al.Ast.Front -> sprintf "%s with %s prepended by %s" se1 sps se2 | Al.Ast.Back -> sprintf "%s with %s appended by %s" se1 sps se2) + | Al.Ast.InvCallE (id, nl, el) -> + let e = + if id = "lsizenn" || id = "lsizenn1" || id = "lsizenn2" then Al.Al_util.varE "N" + else if List.length nl = 1 then Al.Al_util.varE "fresh" + else + let el = + nl + |> List.filter_map (Option.map (fun x -> Al.Al_util.varE ("fresh_" ^ (string_of_int x)))) + in + Al.Al_util.tupE el + in + let elhs, erhs = al_invcalle_to_al_bine e id nl el in + sprintf "%s for which %s %s %s" + (render_expr env e) + (render_expr env elhs) + (render_math "=") + (render_expr env erhs) | Al.Ast.IterE (e, ids, iter) when al_to_el_expr e = None -> let se = render_expr env e in let ids = Al.Al_util.tupE (List.map Al.Al_util.varE ids) in @@ -554,6 +578,22 @@ let rec render_al_instr env algoname index depth instr = | Al.Ast.PopAllI e -> sprintf "%s Pop all values %s from the top of the stack." (render_order index depth) (render_expr env e) + | Al.Ast.LetI (e, { it = Al.Ast.IterE ({ it = Al.Ast.InvCallE (id, nl, el); _ }, ids, iter); _ }) -> + let elhs, erhs = al_invcalle_to_al_bine e id nl el in + let ebin = Al.Al_util.binE (Al.Ast.EqOp, elhs, erhs) in + let eiter = Al.Al_util.iterE (ebin, ids, iter) in + sprintf "%s Let %s be the result for which %s." + (render_order index depth) + (render_expr env e) + (render_expr env eiter) + | Al.Ast.LetI (e, { it = Al.Ast.InvCallE (id, nl, el); _ }) -> + let elhs, erhs = al_invcalle_to_al_bine e id nl el in + sprintf "%s Let %s be the result for which %s %s %s." + (render_order index depth) + (render_expr env e) + (render_expr env elhs) + (render_math "=") + (render_expr env erhs) | Al.Ast.LetI (n, e) -> sprintf "%s Let %s be %s." (render_order index depth) (render_expr env n) (render_expr env e) diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 72580ab910..6b69b636cd 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -537,7 +537,8 @@ and handle_inverse_function lhs rhs free_ids = (* All arguments are free *) if List.for_all contains_free args then let new_lhs = args2lhs args in - let new_rhs = invCallE (f, [], rhs2args rhs) ~at:lhs.at in + let indices = List.init (List.length args) (fun i -> Some i) in + let new_rhs = invCallE (f, indices, rhs2args rhs) ~at:lhs.at in handle_special_lhs new_lhs new_rhs free_ids (* Some arguments are free *) @@ -552,10 +553,10 @@ and handle_inverse_function lhs rhs free_ids = |> List.split in let bound_args = List.filter_map (fun x -> x) bound_args in - let free_args, indices = + let indices = List.map (Option.map snd) free_args_with_index in + let free_args = free_args_with_index - |> List.filter_map (fun x -> x) - |> List.split + |> List.filter_map (Option.map fst) in (* Free argument become new lhs & InvCallE become new rhs *) From d606b958cda7e6fe2bef0fcac4628dba9832afda Mon Sep 17 00:00:00 2001 From: jaehyun1ee <99jaehyunlee@kaist.ac.kr> Date: Fri, 19 Jul 2024 17:48:19 +0900 Subject: [PATCH 2/2] Hotfix Al printer for InvCallE --- spectec/src/al/print.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/src/al/print.ml b/spectec/src/al/print.ml index bbaea95e6b..e2488a5287 100644 --- a/spectec/src/al/print.ml +++ b/spectec/src/al/print.ml @@ -145,7 +145,7 @@ and string_of_expr expr = | CallE (id, el) -> sprintf "$%s(%s)" id (string_of_exprs ", " el) | InvCallE (id, nl, el) -> let id' = - if List.length nl = 0 then id + if List.for_all Option.is_some nl then id else nl |> List.filter_map (fun x -> x)