Using Latex backend for rendering AL expressions

spectec/src/backend-interpreter/manual.ml

@@ -95,10 +95,10 @@ let call_ref =
               (accE (fi, dotP ("MODULE", "module")))
           ));
           letI (ff, frameE (Some m, f));
-          enterI (ff, listE ([caseE (("FRAME_", ""), [])]),
+          enterI (ff, listE ([caseE (("FRAME_", "admininstr"), [])]),
             [
             letI (ll, labelE (m, listE []));
-            enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (("LABEL_", ""), [])])), []);
+            enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (("LABEL_", "admininstr"), [])])), []);
             ]
           );
         ], []);
@@ -211,7 +211,7 @@ let return_instrs_of_instantiate config =
   [
     enterI (
       frameE (Some (numE 0L), frame),
-      listE ([ caseE (("FRAME_", ""), []) ]), rhs
+      listE ([ caseE (("FRAME_", "admininstr"), []) ]), rhs
     );
     returnI (Some (tupE [ store; varE "mm" ]))
   ]
@@ -221,7 +221,7 @@ let return_instrs_of_invoke config =
     letI (varE "k", lenE (iterE (varE "t_2", ["t_2"], List)));
     enterI (
       frameE (Some (varE "k"), frame),
-      listE ([caseE (("FRAME_", ""), [])]), rhs
+      listE ([caseE (("FRAME_", "admininstr"), [])]), rhs
     );
     popI (iterE (varE "val", ["val"], ListN (varE "k", None)));
     returnI (Some (iterE (varE "val", ["val"], ListN (varE "k", None))))

spectec/src/backend-latex/render.mli

@@ -11,12 +11,6 @@ val with_syntax_decoration : bool -> env -> env
 val with_rule_decoration : bool -> env -> env
 
 
-(* Utilities *)
-
-(* TODO: this should not be public *)
-val expand_exp : arg list -> int ref -> exp -> exp
-
-
 (* Generators *)
 
 val render_atom : env -> atom -> string

spectec/src/backend-prose/dune

@@ -8,6 +8,5 @@
     gen
     render
     macro
-    hint
     symbol)
 )

spectec/src/backend-prose/gen.mli

@@ -0,0 +1,2 @@
+val gen_string : Il.Ast.script -> Al.Ast.algorithm list -> string
+val gen_prose : Il.Ast.script -> Al.Ast.algorithm list -> Prose.prose

spectec/src/backend-prose/macro.ml

@@ -31,6 +31,10 @@ type env =
     sections: string Map.t ref;
   }
 
+(* Environment Lookup *)
+
+let find_section env s = Map.mem s !(env.sections)
+
 (* Macro Generation *)
 
 let macro_template = {|
@@ -84,10 +88,10 @@ let gen_macro_kwd env syntax kwd =
   gen_macro_rule ~note:syntax env header font kwd
 
 let gen_macro_kwds env kwds =
-  Map.fold
+  Symbol.Map.fold
     (fun syntax variants skwd ->
       let terminals, _ = variants in
-      let svariants = Set.fold
+      let svariants = Symbol.Set.fold
         (fun kwd svariants ->
           let svariant = gen_macro_kwd env syntax kwd in
           svariants ^ svariant ^ "\n")
@@ -106,15 +110,17 @@ let gen_macro_func env fname =
   gen_macro_rule env header font fname
 
 let gen_macro_funcs env funcs =
-  Set.fold
+  Symbol.Set.fold
     (fun fname sfunc ->
       let sword = gen_macro_func env fname in
       sfunc ^ sword ^ "\n")
     funcs ""
 
 let gen_macro' env (symbol: Symbol.env)  =
-  let skwd = gen_macro_kwds env !(symbol.kwds) in
-  let sfunc = gen_macro_funcs env !(symbol.funcs) in
+  let kwds = Symbol.kwds symbol in
+  let skwd = gen_macro_kwds env kwds in
+  let funcs = Symbol.funcs symbol in
+  let sfunc = gen_macro_funcs env funcs in
   macro_template
   ^ ".. syntax\n.. ------\n\n"
   ^ skwd
@@ -168,9 +174,8 @@ let env inputs outputs =
   let sections = if check_rst outputs then parse_section inputs outputs else Map.empty in
   { sections = ref sections; }
 
-(* Environment Lookup *)
 
-let find_section env s = Map.mem s !(env.sections)
+(* Macro generation *)
 
 let macro_kwd env kwd =
   let variant, syntax = kwd in

spectec/src/backend-prose/macro.mli

@@ -0,0 +1,19 @@
+open Al.Ast
+
+(* Environment *)
+
+type env
+
+val env : string list -> string list -> env
+
+
+(* Lookups *)
+
+val find_section : env -> string -> bool
+
+
+(* Macro Generation *)
+
+val macro_kwd : env -> kwd -> string * string
+val macro_func : env -> id -> string * string
+val gen_macro : env -> Symbol.env -> unit

spectec/src/backend-prose/print.ml

@@ -3,6 +3,7 @@ open Prose
 open Printf
 
 (* Helpers *)
+
 let string_of_opt prefix stringifier suffix = function
   | None -> ""
   | Some x -> prefix ^ stringifier x ^ suffix
@@ -81,30 +82,3 @@ let string_of_def = function
 | Algo algo -> string_of_algorithm algo
 
 let string_of_prose prose = List.map string_of_def prose |> String.concat "\n"
-
-(* Structured string *)
-
-let string_of_structured_instr = function
-  | LetI _ -> "LetI(...)"
-  | CmpI _ -> "CmpI(...)"
-  | MustValidI (e1, e2, eo) ->
-      "MustValidI ("
-      ^ structured_string_of_expr e1
-      ^ ", "
-      ^ structured_string_of_expr e2
-      ^ ", "
-      ^ "(" ^ string_of_opt "" structured_string_of_expr "" eo ^ ")"
-      ^ ")"
-  | MustMatchI (e1, e2) ->
-      "MustMatchI ("
-      ^ structured_string_of_expr e1
-      ^ ", "
-      ^ structured_string_of_expr e2
-      ^ ")"
-  | IsValidI e_opt ->
-      "IsValidI" ^ string_of_opt " (" structured_string_of_expr ")" e_opt
-  | IfI _ -> "IfI(...)"
-  | ForallI _ -> "ForallI(...)"
-  | EquivI _ -> "EquivI ..."
-  | YetI s -> "YetI (" ^ s ^ ")"
-

spectec/src/backend-prose/print.mli

@@ -0,0 +1,5 @@
+open Prose
+
+val string_of_instr : instr -> string
+val string_of_def : def -> string
+val string_of_prose : prose -> string