Merge pull request #65 from Wasm-DSL/typed-splice

Support expression splices with type annotation

spectec/doc/Latex.md

@@ -28,7 +28,9 @@ splice ::=
   tag"{" desc "}"
 
 desc ::=
-  ":" exp                               expression splice
+  ":" exp                               untyped expression splice
+  "exp" typ ":" exp                     typed expression splice
+  "exp" relid ":" exp                   typed relation splice
   sort ":" group*                       definition splice
 
 group ::=
@@ -54,7 +56,7 @@ The `tag` can be configured differently for different file formats. Currently, t
 
 There are two forms of splices:
 
-1. _Expression splices_ (`tag{: exp }`). The body of this splice is an [expression](Language.md#expressions) in the DSL. The effect is to render this expression and insert it.
+1. _Expression splices_ (`tag{: exp }`). The body of this splice is an [expression](Language.md#expressions) in the DSL. The effect is to render this expression and insert it. Optionally, these slices may be prefixed with a type or a relation identifier, which is necessary if the expression contains custom notation that is supposed to be type-set with macros (the type information is needed to generate the right macro names for atoms).
 
 2. _Definition splices_ (`tag{sort: group* }`). This splice renders and inserts (a set of) [definitions](Language.md#definitions) from the DSL, identified by the _names_ in the `group`. The following `sort`s are recognised:
 

spectec/src/backend-latex/config.ml

@@ -1,10 +1,10 @@
 type config =
   {
-    (* Generate id's as macro calls `\id` instead of `\mathit{id}` *)
+    (* Generate ids as macro calls `\id` instead of `\mathit{id}` *)
     macros_for_ids : bool;
 
-    (* Generate vdash's as macro calls `\vdashRelid` instead of `\vdash` *)
-    macros_for_vdash : bool;
+    (* Generate atoms as macro calls, e.g., `\vdashRelid` instead of `\vdash` *)
+    macros_for_atoms : bool;
 
     (* Decorate grammars with l.h.s. description like "(instruction) instr ::= ..." *)
     include_grammar_desc : bool;
@@ -14,6 +14,6 @@ type t = config
 
 let default =
   { macros_for_ids = false;
-    macros_for_vdash = false;
+    macros_for_atoms = false;
     include_grammar_desc = false;
   }

spectec/src/backend-latex/render.ml

@@ -416,51 +416,55 @@ let render_rule_deco env pre id1 id2 post =
 (* Operators *)
 
 let render_atom env atom =
-  match atom.it with
-  | Atom id when id.[0] = '_' && id <> "_" -> ""
-  | Atom id ->
-    if id <> "_" && !(atom.note) = "" then
-      failwith (string_of_region atom.at ^
-        ": latex backend: render atom `" ^ id ^ "` without type id");
-    render_atomid env id !(atom.note)
-  | Infinity -> "\\infty"
-  | Bot -> "\\bot"
-  | Top -> "\\top"
-  | Dot -> "."
-  | Dot2 -> ".."
-  | Dot3 -> "\\dots"
-  | Semicolon -> ";"
-  | Backslash -> "\\setminus"
-  | In -> "\\in"
-  | Arrow -> "\\rightarrow"
-  | Arrow2 -> "\\Rightarrow"
-  | Colon -> ":"
-  | Sub -> "\\leq"
-  | Sup -> "\\geq"
-  | Assign -> ":="
-  | Equiv -> "\\equiv"
-  | Approx -> "\\approx"
-  | SqArrow -> "\\hookrightarrow"
-  | SqArrowStar -> "\\hookrightarrow^\\ast"
-  | Prec -> "\\prec"
-  | Succ -> "\\succ"
-  | Tilesturn -> "\\dashv"
-  | Turnstile ->
-    if env.config.macros_for_vdash then
-      "\\vdash" ^ env.current_rel
+  let macros = env.config.macros_for_atoms in
+  let tid =
+    if not macros then
+      ""
+    else if !(atom.note) <> "" then
+      !(atom.note)
     else
-      "\\vdash"
-  | Quest -> "{}^?"
-  | Plus -> "{}^+"
-  | Star -> "{}^\\ast"
-  | Comma -> ","
-  | Bar -> "\\mid"
-  | LParen -> "("
-  | RParen -> ")"
-  | LBrack -> "["
-  | RBrack -> "]"
-  | LBrace -> "\\{"
-  | RBrace -> "\\}"
+      error atom.at
+        ("cannot infer type of notation `" ^ El.Print.string_of_atom atom ^ "`")
+  in
+  let s =
+    match atom.it with
+    | Atom id when id.[0] = '_' && id <> "_" -> ""
+    | Atom id -> render_atomid env id tid
+    | Infinity -> "\\infty"
+    | Bot -> "\\bot"
+    | Top -> "\\top"
+    | Dot -> if macros then "\\dot" else "."
+    | Dot2 -> if macros then "\\dotdot" else ".."
+    | Dot3 -> "\\dots"
+    | Semicolon -> if macros then "\\semicolon" else ";"
+    | Backslash -> "\\setminus"
+    | In -> "\\in"
+    | Arrow -> "\\rightarrow"
+    | Arrow2 -> "\\Rightarrow"
+    | Colon -> if macros then "\\colon" else ":"
+    | Sub -> "\\leq"
+    | Sup -> "\\geq"
+    | Assign -> if macros then "\\assign" else ":="
+    | Equiv -> "\\equiv"
+    | Approx -> "\\approx"
+    | SqArrow -> "\\hookrightarrow"
+    | SqArrowStar -> "\\hookrightarrow^\\ast"
+    | Prec -> "\\prec"
+    | Succ -> "\\succ"
+    | Tilesturn -> "\\dashv"
+    | Turnstile -> "\\vdash"
+    | Quest -> if macros then "\\quest" else "{}^?"
+    | Plus -> if macros then "\\plus" else "{}^+"
+    | Star -> if macros then "\\ast" else "{}^\\ast"
+    | Comma -> if macros then "\\comma" else ","
+    | Bar -> "\\mid"
+    | LParen -> if macros then "\\lparen" else "("
+    | RParen -> if macros then "\\rparen" else ")"
+    | LBrack -> if macros then "\\lbrack" else "["
+    | RBrack -> if macros then "\\rbrack" else "]"
+    | LBrace -> if macros then "\\lbrace" else "\\{"
+    | RBrace -> if macros then "\\rbrace" else "\\}"
+  in s ^ tid
 
 let render_unop = function
   | NotOp -> "\\neg"

spectec/src/backend-splice/config.ml

@@ -22,8 +22,8 @@ type t = config
 
 let latex =
   { anchors = [
-      {token = "@@"; prefix = "$"; suffix = "$"; indent = ""};
-      {token = "@@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
+      {token = "@"; prefix = "$"; suffix = "$"; indent = ""};
+      {token = "@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
     ];
     latex = Backend_latex.Config.default;
     prose = Backend_prose.Config.default;

spectec/src/backend-splice/splice.ml

@@ -43,7 +43,8 @@ type relation_prose = {ralgos : (string * Backend_prose.Prose.def * use) list}
 type definition_prose = {falgo : Backend_prose.Prose.def; use : use}
 
 type env =
-  { config : Config.t;
+  { elab : Frontend.Elab.env;
+    config : Config.t;
     latex : Backend_latex.Render.env;
     prose : Backend_prose.Render.env;
     mutable syn : syntax Map.t;
@@ -105,11 +106,11 @@ let env_prose env prose =
   | Algo (Al.Ast.FuncA (id, _, _)) ->
     env.def_prose <- Map.add id {falgo = prose; use = ref 0} env.def_prose
 
-let env (config : config) pdsts odsts el pr : env =
+let env (config : config) pdsts odsts elab el pr : env =
   let latex = Backend_latex.Render.env config.latex el in
   let prose = Backend_prose.Render.env config.prose pdsts odsts latex el pr in
   let env =
-    { config; latex; prose;
+    { elab; config; latex; prose;
       syn = Map.empty;
       gram = Map.empty;
       rel = Map.empty;
@@ -235,15 +236,21 @@ let try_string src s : bool =
 let try_anchor_start src anchor : bool =
   try_string src (anchor ^ "{")
 
-let rec parse_anchor_end src j depth =
+let rec parse_to_colon src =
   if eos src then
-    error {src with i = j} "unclosed anchor"
+    error src "colon `:` expected"
+  else if get src <> ':' then
+    (adv src; parse_to_colon src)
+
+let rec parse_to_anchor_end i0 depth src =
+  if eos src then
+    error {src with i = i0} "unclosed anchor"
   else if get src = '{' then
-    (adv src; parse_anchor_end src j (depth + 1))
+    (adv src; parse_to_anchor_end i0 (depth + 1) src)
   else if get src <> '}' then
-    (adv src; parse_anchor_end src j depth)
+    (adv src; parse_to_anchor_end i0 depth src)
   else if depth > 0 then
-    (adv src; parse_anchor_end src j (depth - 1))
+    (adv src; parse_to_anchor_end i0 (depth - 1) src)
 
 let rec parse_id' src =
   if not (eos src) then
@@ -300,26 +307,63 @@ let try_def_anchor env src r sort space1 space2 find mode : bool =
   );
   b
 
+let run_parser find_end parser src =
+  let i = src.i in
+  find_end src;
+  let s = str src i in
+  adv src;
+  try parser s with Source.Error (at, msg) ->
+    (* Translate relative positions *)
+    let pos = pos {src with i} in
+    let shift {line; column; _} =
+      { file = src.file; line = line + pos.line - 1;
+        column = if line = 1 then column + pos.column - 1 else column} in
+    let at' = {left = shift at.left; right = shift at.right} in
+    raise (Source.Error (at', msg))
+
+let try_relid src : id option =
+  let i = src.i in
+  parse_space src;
+  let id = try parse_id src "relation" with Source.Error _ -> " " in
+  if id.[0] <> Char.lowercase_ascii id.[0] then
+    let pos = pos {src with i} in
+    let left = {file = src.file; line = pos.line; column = pos.column} in
+    let right = {left with column = left.column + String.length id} in
+    Some (id $ {left; right})
+  else
+    (advn src (i - src.i); None)
+
+let parse_typ src : typ =
+  run_parser parse_to_colon Frontend.Parse.parse_typ src
+
+let parse_exp src i0 : exp =
+  run_parser (parse_to_anchor_end i0 0) Frontend.Parse.parse_exp src
+
 let try_exp_anchor env src r : bool =
-  let b = try_string src ":" in
-  if b then (
-  	let j = src.i in
-    parse_anchor_end src (j - 4) 0;
-    let s = str src j in
-    adv src;
-    let exp =
-      try Frontend.Parse.parse_exp s with Source.Error (at, msg) ->
-        (* Translate relative positions *)
-        let pos = pos {src with i = j} in
-        let shift {line; column; _} =
-          { file = src.file; line = line + pos.line - 1;
-            column = if false(*line = 1*) then column + pos.column - 1 else column} in
-        let at' = {left = shift at.left; right = shift at.right} in
-        raise (Source.Error (at', msg))
+  let i0 = src.i - 2 in
+  if try_string src ":" then (
+    let exp = parse_exp src i0 in
+    r := Backend_latex.Render.render_exp env.latex exp;
+    true
+  )
+  else if try_string src "exp " then (
+    let elab =
+      match try_relid src with
+      | None ->
+        let typ = parse_typ src in
+        fun env exp -> Frontend.Elab.elab_exp env exp typ
+      | Some id ->
+        parse_space src;
+        if not (try_string src ":") then
+          error src "colon `:` expected";
+        fun env exp -> Frontend.Elab.elab_rel env exp id
     in
-    r := Backend_latex.Render.render_exp env.latex exp
-  );
-  b
+    let exp = parse_exp src i0 in
+    let _ = elab env.elab exp in
+    r := Backend_latex.Render.render_exp env.latex exp;
+    true
+  )
+  else false
 
 let try_prose_anchor env src r sort space1 space2 find mode : bool =
   let b = try_string src (sort ^ ":") in

spectec/src/backend-splice/splice.mli

@@ -1,6 +1,6 @@
 type env
 
-val env : Config.config -> string list -> string list -> El.Ast.script -> Backend_prose.Prose.prose -> env
+val env : Config.config -> string list -> string list -> Frontend.Elab.env -> El.Ast.script -> Backend_prose.Prose.prose -> env
 
 val splice_string : env -> string -> string -> string (* raise Source.Error *)
 val splice_file : ?dry:bool -> env -> string -> string -> unit (* raise Source.Error *)

spectec/src/exe-watsup/main.ml

@@ -160,7 +160,7 @@ let () =
     if !print_el then
       Printf.printf "%s\n%!" (El.Print.string_of_script el);
     log "Elaboration...";
-    let il = Frontend.Elab.elab el in
+    let il, elab_env = Frontend.Elab.elab el in
     if !print_elab_il || !print_all_il then
       Printf.printf "%s\n%!" (Il.Print.string_of_script il);
     log "IL Validation...";
@@ -245,7 +245,7 @@ let () =
       log "Prose Generation...";
       let prose = Backend_prose.Gen.gen_prose il al in
       log "Splicing...";
-      let env = Backend_splice.Splice.(env config !pdsts !odsts el prose) in
+      let env = Backend_splice.Splice.(env config !pdsts !odsts elab_env el prose) in
       List.iter2 (Backend_splice.Splice.splice_file ~dry:!dry env) !pdsts !odsts;
       if !warn_math then Backend_splice.Splice.warn_math env;
       if !warn_prose then Backend_splice.Splice.warn_prose env;

spectec/src/frontend/elab.ml

@@ -958,9 +958,12 @@ and elab_exp_notation' env tid e t : Il.exp list =
     if atom.it <> atom'.it then error_typ e.at "infix expression" t;
     let es1' = elab_exp_notation' env tid e1 t1 in
     let es2' = elab_exp_notation' env tid e2 t2 in
+    ignore (elab_atom atom tid);
     es1' @ es2'
   | BrackE (l, e1, r), BrackT (l', t1, r') ->
     if (l.it, r.it) <> (l'.it, r'.it) then error_typ e.at "bracket expression" t;
+    ignore (elab_atom l tid);
+    ignore (elab_atom r tid);
     elab_exp_notation' env tid e1 t1
 
   | SeqE [], SeqT [] ->
@@ -1661,11 +1664,20 @@ let recursify_defs ds' : Il.def list =
   ) sccs
 
 
-let elab ds : Il.script =
+let elab ds : Il.script * env =
   let env = new_env () in
   List.iter (infer_syndef env) ds;
   let ds' = List.concat_map (elab_def env) ds in
   let ds' = List.map (populate_def env) ds' in
   List.iter (infer_gramdef env) ds;
   List.iter (elab_gramdef env) ds;
-  recursify_defs ds'
+  recursify_defs ds', env
+
+let elab_exp env e t : Il.exp =
+  let _ = elab_typ env t in
+  elab_exp env e t
+
+let elab_rel env e id : Il.exp =
+  match (elab_prem env (RulePr (id, e) $ e.at)).it with
+  | Il.RulePr (_, _, e') -> e'
+  | _ -> assert false

spectec/src/frontend/elab.mli

@@ -1 +1,5 @@
-val elab : El.Ast.script -> Il.Ast.script (* raises Source.Error *)
+type env
+
+val elab : El.Ast.script -> Il.Ast.script * env (* raises Source.Error *)
+val elab_exp : env -> El.Ast.exp -> El.Ast.typ -> Il.Ast.exp (* raises Source.Error *)
+val elab_rel : env -> El.Ast.exp -> El.Ast.id -> Il.Ast.exp (* raises Source.Error *)

spectec/src/frontend/parse.ml

@@ -8,9 +8,13 @@ let with_lexbuf name lexbuf start =
   with Parser.Error ->
     raise (Source.Error (Lexer.region lexbuf, "unexpected token"))
 
+let parse_typ s =
+  let lexbuf = Lexing.from_string s in
+  with_lexbuf "(string)" lexbuf Parser.typ_eof
+
 let parse_exp s =
   let lexbuf = Lexing.from_string s in
-  with_lexbuf "(string)" lexbuf Parser.expression
+  with_lexbuf "(string)" lexbuf Parser.exp_eof
 
 let parse_script s =
   let lexbuf = Lexing.from_string s in

spectec/src/frontend/parse.mli

@@ -1,3 +1,4 @@
+val parse_typ : string -> El.Ast.typ (* raises Source.Error *)
 val parse_exp : string -> El.Ast.exp (* raises Source.Error *)
 val parse_script : string -> El.Ast.script (* raises Source.Error *)
 val parse_file : string -> El.Ast.script (* raises Source.Error *)

spectec/src/frontend/parser.mly

@@ -128,9 +128,10 @@ let is_post_exp e =
 %left PLUS MINUS COMPOSE
 %left STAR SLASH BACKSLASH
 
-%start script expression check_atom
+%start script typ_eof exp_eof check_atom
 %type<El.Ast.script> script
-%type<El.Ast.exp> expression
+%type<El.Ast.typ> typ_eof
+%type<El.Ast.exp> exp_eof
 %type<bool> check_atom
 
 %%
@@ -759,7 +760,10 @@ hint :
 script :
   | def* EOF { $1 }
 
-expression :
+typ_eof :
+  | typ EOF { $1 }
+
+exp_eof :
   | exp EOF { $1 }
 
 %%