Render inverse functions in prose, without ^(-1)

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' =

spectec/src/al/print.ml

@@ -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
@@ -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) ->

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)

spectec/src/il2al/translate.ml

@@ -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 *)
@@ -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 *)