Skip to content

Commit

Permalink
Merge pull request #109 from Wasm-DSL/render-inverse
Browse files Browse the repository at this point in the history 
Render inverse functions in prose, without ^(-1)
  • Loading branch information
@jaehyun1ee
jaehyun1ee authored Jul 19, 2024
2 parents 4a13994 + d606b95 commit 3ff8100
Show file tree
Hide file tree
Showing 4 changed files with 140 additions and 97 deletions.
80 changes: 40 additions & 40 deletions spectec/src/al/ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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' =
Expand Down
4 changes: 3 additions & 1 deletion spectec/src/al/print.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,9 +145,10 @@ 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)
|> List.map string_of_int
|> List.fold_left (^) ""
|> sprintf "%s_%s" id
Expand Down Expand Up @@ -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) ->
Expand Down
144 changes: 92 additions & 52 deletions spectec/src/backend-prose/render.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
9 changes: 5 additions & 4 deletions spectec/src/il2al/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,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 ~note:lhs.note in
let indices = List.init (List.length args) (fun i -> Some i) in
let new_rhs = invCallE (f, indices, rhs2args rhs) ~at:lhs.at ~note:lhs.note in
handle_special_lhs new_lhs new_rhs free_ids

(* Some arguments are free *)
Expand All @@ -551,10 +552,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 *)
Expand Down

0 comments on commit 3ff8100

Please sign in to comment.