Unify anchors

spectec/src/backend-splice/config.ml

@@ -1,8 +1,8 @@
 type anchor =
   {
     token : string;   (* anchor token *)
-    prefix : string;  (* prefix generated for splice *)
-    suffix : string;  (* suffix generated for splice *)
+    prefix : string;  (* prefix generated for math splice *)
+    suffix : string;  (* suffix generated for math splice *)
     indent : string;  (* inserted after generated newlines *)
   }
 
@@ -20,24 +20,18 @@ type config =
 
 type t = config
 
-let default =
-  { anchors = [ {token = "%"; prefix = ""; suffix = ""; indent = ""} ];
-    latex = Backend_latex.Config.default;
-    prose = Backend_prose.Config.default;
-  }
-
 let latex =
-  { anchors = default.anchors @ [
-      {token = "@@"; prefix = "$"; suffix ="$"; indent = ""};
+  { anchors = [
+      {token = "@@"; prefix = "$"; suffix = "$"; indent = ""};
       {token = "@@@"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
     ];
     latex = Backend_latex.Config.default;
     prose = Backend_prose.Config.default;
   }
 
 let sphinx =
-  { anchors = default.anchors @ [
-      {token = "$"; prefix = ":math:`"; suffix ="`"; indent = ""};
+  { anchors = [
+      {token = "$"; prefix = ":math:`"; suffix = "`"; indent = ""};
       {token = "$$"; prefix = ".. math::\n   "; suffix = ""; indent = "   "};
     ];
     latex = Backend_latex.Config.default;

spectec/src/backend-splice/splice.ml

@@ -24,10 +24,9 @@ let rec pos' src j (line, column) : Source.pos =
       (if src.s.[j] = '\n' then line + 1, 1 else line, column + 1)
 
 let pos src = pos' src 0 (1, 1)
+let region src = let pos = pos src in {left = pos; right = pos}
 
-let error src msg =
-  let pos = pos src in
-  Source.error {left = pos; right = pos} "splice replacement" msg
+let error src msg = Source.error (region src) "splicing" msg
 
 
 (* Environment *)
@@ -40,9 +39,8 @@ type syntax = {sdef : El.Ast.def; sfragments : (string * El.Ast.def * use) list}
 type grammar = {gdef : El.Ast.def; gfragments : (string * El.Ast.def * use) list}
 type relation = {rdef : El.Ast.def; rules : (string * El.Ast.def * use) list}
 type definition = {fdef : El.Ast.def; clauses : El.Ast.def list; use : use}
-type validation_prose = {vprose : Backend_prose.Prose.def; use : use}
-type execution_prose = {eprose : Backend_prose.Prose.def; use : use}
-type definition_prose = {fprose : Backend_prose.Prose.def; use : use}
+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;
@@ -52,8 +50,7 @@ type env =
     mutable gram : grammar Map.t;
     mutable rel : relation Map.t;
     mutable def : definition Map.t;
-    mutable valid_prose : validation_prose Map.t;
-    mutable exec_prose : execution_prose Map.t;
+    mutable rel_prose : relation_prose Map.t;
     mutable def_prose : definition_prose Map.t;
   }
 
@@ -86,14 +83,27 @@ let env_def env def =
   | VarD _ | SepD | HintD _ ->
     ()
 
+let valid_id = "valid"
+let exec_id = "exec"
+
+let normalize_id id =
+  let id' =
+    if id = "" || id.[String.length id - 1] <> '_' then id else
+    String.sub id 0 (String.length id - 1)
+  in String.lowercase_ascii id'
+
 let env_prose env prose =
   match prose with
   | Pred ((id, _), _, _) ->
-    env.valid_prose <- Map.add id {vprose = prose; use = ref 0} env.valid_prose
+    let relation = Map.find valid_id env.rel_prose in
+    let ralgos = (normalize_id id, prose, ref 0) :: relation.ralgos in
+    env.rel_prose <- Map.add valid_id {ralgos} env.rel_prose
   | Algo (Al.Ast.RuleA ((id, _), _, _)) ->
-    env.exec_prose <- Map.add id {eprose = prose; use = ref 0} env.exec_prose
+    let relation = Map.find exec_id env.rel_prose in
+    let ralgos = (normalize_id id, prose, ref 0) :: relation.ralgos in
+    env.rel_prose <- Map.add exec_id {ralgos} env.rel_prose
   | Algo (Al.Ast.FuncA (id, _, _)) ->
-    env.def_prose <- Map.add id {fprose = prose; use = ref 0} env.def_prose
+    env.def_prose <- Map.add id {falgo = prose; use = ref 0} env.def_prose
 
 let env (config : config) pdsts odsts el pr : env =
   let latex = Backend_latex.Render.env config.latex el in
@@ -104,8 +114,7 @@ let env (config : config) pdsts odsts el pr : env =
       gram = Map.empty;
       rel = Map.empty;
       def = Map.empty;
-      valid_prose = Map.empty;
-      exec_prose = Map.empty;
+      rel_prose = Map.(add valid_id {ralgos = []} (add exec_id {ralgos = []} empty));
       def_prose = Map.empty;
     }
   in
@@ -120,7 +129,7 @@ let warn_use use space id1 id2 =
     let msg = if !use = 0 then "never spliced" else "spliced more than once" in
     prerr_endline ("warning: " ^ space ^ " `" ^ id ^ "` was " ^ msg)
 
-let warn env =
+let warn_math env =
   Map.iter (fun id1 {sfragments; _} ->
     List.iter (fun (id2, _, use) -> warn_use use "syntax" id1 id2) sfragments
   ) env.syn;
@@ -130,16 +139,15 @@ let warn env =
   Map.iter (fun id1 {rules; _} ->
   	List.iter (fun (id2, _, use) -> warn_use use "rule" id1 id2) rules
   ) env.rel;
-  Map.iter (fun id1 ({use; _}: definition) ->
+  Map.iter (fun id1 ({use; _} : definition) ->
     warn_use use "definition" id1 ""
-  ) env.def;
-  Map.iter (fun id1 ({use; _}: validation_prose) ->
-    warn_use use "validation prose" id1 ""
-  ) env.valid_prose;
-  Map.iter (fun id1 ({use; _}: execution_prose) ->
-    warn_use use "execution prose" id1 ""
-  ) env.exec_prose;
-  Map.iter (fun id1 ({use; _}: definition_prose) ->
+  ) env.def
+
+let warn_prose env =
+  Map.iter (fun id1 {ralgos} ->
+    List.iter (fun (id2, _, use) -> warn_use use "rule prose" id1 id2) ralgos
+  ) env.rel_prose;
+  Map.iter (fun id1 ({use; _} : definition_prose) ->
     warn_use use "definition prose" id1 ""
   ) env.def_prose
 
@@ -158,6 +166,16 @@ let find_entries space src id1 id2 entries =
     error src ("unknown " ^ space ^ " identifier `" ^ id1 ^ "/" ^ id2 ^ "`");
   List.map (fun (_, def, use) -> incr use; def) defs
 
+let find_entry space src id1 id2 entries =
+  match find_entries space src id1 id2 entries with
+  | [def] -> def
+  | defs ->
+    Printf.eprintf "warning: %s `%s/%s` has multiple definitions\n%!" space id1 id2;
+    List.hd defs
+(* TODO: this should be an error
+    error src ("duplicate " ^ space ^ " identifier `" ^ id1 ^ "/" ^ id2 ^ "`")
+*)
+
 let find_syntax env src id1 id2 =
   match Map.find_opt id1 env.syn with
   | None -> error src ("unknown syntax identifier `" ^ id1 ^ "`")
@@ -179,7 +197,7 @@ let find_rule env src id1 id2 =
   | None -> error src ("unknown relation identifier `" ^ id1 ^ "`")
   | Some relation -> find_entries "rule" src id1 id2 relation.rules
 
-let find_func env src id1 id2 =
+let find_def env src id1 id2 =
   find_nosub "definition" src id1 id2;
   match Map.find_opt id1 env.def with
   | None -> error src ("unknown definition identifier `" ^ id1 ^ "`")
@@ -188,20 +206,16 @@ let find_func env src id1 id2 =
       error src ("definition `" ^ id1 ^ "` has no clauses");
     incr definition.use; definition.clauses
 
-let find_vrule_prose env src id =
-  match Map.find_opt id env.valid_prose with
-  | None -> error src ("unknown validation identifier `" ^ id ^ "`")
-  | Some prose -> incr prose.use; prose.vprose
-
-let find_rrule_prose env src id =
-  match Map.find_opt id env.exec_prose with
-  | None -> error src ("unknown execution identifier `" ^ id ^ "`")
-  | Some prose -> incr prose.use; prose.eprose
+let find_rule_prose env src id1 id2 =
+  match Map.find_opt id1 env.rel_prose with
+  | None -> error src ("unknown prose relation identifier `" ^ id1 ^ "`")
+  | Some relation -> find_entry "prose rule" src id1 id2 relation.ralgos
 
-let find_def_prose env src id =
-  match Map.find_opt id env.def_prose with
-  | None -> error src ("unknown definition identifier `" ^ id ^ "`")
-  | Some prose -> incr prose.use; prose.fprose
+let find_def_prose env src id1 id2 =
+  find_nosub "definition" src id1 id2;
+  match Map.find_opt id1 env.def_prose with
+  | None -> error src ("unknown prose definition identifier `" ^ id1 ^ "`")
+  | Some definition -> incr definition.use; definition.falgo
 
 
 (* Parsing *)
@@ -245,7 +259,7 @@ let parse_id src space : string =
     error {src with i = j} ("expected " ^ space ^ " identifier or `}`");
   str src j
 
-let parse_id_id env src space1 space2 find : El.Ast.def list =
+let parse_id_id env src space1 space2 find =
   let j = src.i in
   let id1 = parse_id src space1 in
   let id2 =
@@ -273,12 +287,9 @@ let rec parse_group_list env src space1 space2 find : El.Ast.def list list =
 type mode = Decorated | Undecorated | Ignored
 
 let try_def_anchor env src r sort space1 space2 find mode : bool =
-  let b = try_string src sort in
+  let b = try_string src (sort ^ ":") in
   if b then
-  ( parse_space src;
-    if not (try_string src ":") then
-      error src "colon `:` expected";
-    let groups = parse_group_list env src space1 space2 find in
+  ( let groups = parse_group_list env src space1 space2 find in
     let defs = List.tl (List.concat_map ((@) [SepD $ no_region]) groups) in
     if mode <> Ignored then
       let env' = env.latex
@@ -310,18 +321,16 @@ let try_exp_anchor env src r : bool =
   );
   b
 
-let try_prose_anchor env src r sort find : bool =
-  let b = try_string src sort in
+let try_prose_anchor env src r sort space1 space2 find mode : bool =
+  let b = try_string src (sort ^ ":") in
   if b then (
     parse_space src;
-    if not (try_string src ":") then
-      error src "colon `:` expected";
+    let algo = parse_id_id env src space1 space2 find in
     parse_space src;
-    let id = parse_id src "prose name" in
     if not (try_string src "}") then
       error src "closing bracket `}` expected";
-    let prose = find env src id in
-    r := Backend_prose.Render.render_def env.prose prose
+    if mode <> Ignored then
+      r := Backend_prose.Render.render_def env.prose algo
   );
   b
 
@@ -331,37 +340,36 @@ let try_prose_anchor env src r sort find : bool =
 let splice_anchor env src anchor buf =
   parse_space src;
   let r = ref "" in
+  let prose = ref false in
   ignore (
     try_exp_anchor env src r ||
-    try_def_anchor env src r "syntax-ignore" "syntax" "fragment" find_syntax Ignored ||
-    try_def_anchor env src r "grammar-ignore" "grammar" "fragment" find_grammar Ignored ||
-    try_def_anchor env src r "relation-ignore" "relation" "" find_relation Ignored ||
-    try_def_anchor env src r "rule-ignore" "relation" "rule" find_rule Ignored ||
-    try_def_anchor env src r "definition-ignore" "definition" "" find_func Ignored ||
-    try_def_anchor env src r "syntax+" "syntax" "fragment" find_syntax Decorated ||
     try_def_anchor env src r "syntax" "syntax" "fragment" find_syntax Undecorated ||
+    try_def_anchor env src r "syntax+" "syntax" "fragment" find_syntax Decorated ||
     try_def_anchor env src r "grammar" "grammar" "fragment" find_grammar Undecorated ||
     try_def_anchor env src r "relation" "relation" "" find_relation Undecorated ||
-    try_def_anchor env src r "rule+" "relation" "rule" find_rule Decorated ||
     try_def_anchor env src r "rule" "relation" "rule" find_rule Undecorated ||
-    try_def_anchor env src r "definition" "definition" "" find_func Undecorated ||
-    (* TODO: make anchors consistent:
-     * - change anchors to `rule-prose` (for both pred and algo) and `def-prose`
-     * - add anchors `rule-prose-ignore` and `rule-def-ignore`
-     *)
-    try_prose_anchor env src r "prose-pred" find_vrule_prose ||
-    try_prose_anchor env src r "prose-algo" find_rrule_prose ||
-    try_prose_anchor env src r "prose-func" find_def_prose ||
-    error src "unknown definition sort";
+    try_def_anchor env src r "rule+" "relation" "rule" find_rule Decorated ||
+    try_def_anchor env src r "definition" "definition" "" find_def Undecorated ||
+    try_def_anchor env src r "syntax-ignore" "syntax" "fragment" find_syntax Ignored ||
+    try_def_anchor env src r "grammar-ignore" "grammar" "fragment" find_grammar Ignored ||
+    try_def_anchor env src r "relation-ignore" "relation" "" find_relation Ignored ||
+    try_def_anchor env src r "rule-ignore" "relation" "rule" find_rule Ignored ||
+    try_def_anchor env src r "definition-ignore" "definition" "" find_def Ignored ||
+    (prose := true; false) ||
+    try_prose_anchor env src r "rule-prose" "prose relation" "rule" find_rule_prose Undecorated ||
+    try_prose_anchor env src r "definition-prose" "prose definition" "" find_def_prose Undecorated ||
+    try_prose_anchor env src r "rule-prose-ignore" "prose relation" "rule" find_rule_prose Ignored ||
+    try_prose_anchor env src r "definition-prose-ignore" "prose definition" "" find_def_prose Ignored ||
+    error src "unknown anchor sort";
   );
   if !r <> "" then
   ( let s =
-      if anchor.indent = "" then !r else
+      if !prose || anchor.indent = "" then !r else
       Str.(global_replace (regexp "\n") ("\n" ^ anchor.indent) !r)
     in
-    Buffer.add_string buf anchor.prefix;
+    if not !prose then Buffer.add_string buf anchor.prefix;
     Buffer.add_string buf s;
-    Buffer.add_string buf anchor.suffix;
+    if not !prose then Buffer.add_string buf anchor.suffix;
   )
 
 let rec try_anchors env src buf = function

spectec/src/backend-splice/splice.mli

@@ -5,4 +5,5 @@ val env : Config.config -> string list -> string list -> El.Ast.script -> Backen
 val splice_string : env -> string -> string -> string (* raise Source.Error *)
 val splice_file : ?dry:bool -> env -> string -> string -> unit (* raise Source.Error *)
 
-val warn : env -> unit
+val warn_math : env -> unit
+val warn_prose : env -> unit

spectec/src/exe-watsup/main.ml

@@ -38,10 +38,11 @@ type file_kind =
   | Output
 
 let target = ref Latex
-let log = ref false      (* log execution steps *)
-let in_place = ref false (* splice patch files in place *)
-let dry = ref false      (* dry run for patching *)
-let warn = ref false     (* warn about unused or reused splices *)
+let log = ref false        (* log execution steps *)
+let in_place = ref false   (* splice patch files in place *)
+let dry = ref false        (* dry run for patching *)
+let warn_math = ref false  (* warn about unused or reused math splices *)
+let warn_prose = ref false (* warn about unused or reused prose splices *)
 
 let file_kind = ref Spec
 let srcs = ref []    (* spec src file arguments *)
@@ -112,7 +113,12 @@ let argspec = Arg.align
   "-d", Arg.Set dry, " Dry run (when -p) ";
   "-o", Arg.Unit (fun () -> file_kind := Output), " Output files";
   "-l", Arg.Set log, " Log execution steps";
-  "-w", Arg.Set warn, " Warn about unused or multiply used splices";
+  "-w", Arg.Unit (fun () -> warn_math := true; warn_prose := true),
+    " Warn about unused or multiply used splices";
+  "--warn-math", Arg.Set warn_math,
+    " Warn about unused or multiply used math splices";
+  "--warn-prose", Arg.Set warn_prose,
+    " Warn about unused or multiply used prose splices";
 
   "--check", Arg.Unit (fun () -> target := Check), " Check only";
   "--latex", Arg.Unit (fun () -> target := Latex),
@@ -180,6 +186,7 @@ let () =
         )
       ) il all_passes
     in
+    last_pass := "";
 
     if !print_final_il && not !print_all_il then
       Printf.printf "%s\n%!" (Il.Print.string_of_script il);
@@ -240,7 +247,8 @@ let () =
       log "Splicing...";
       let env = Backend_splice.Splice.(env config !pdsts !odsts el prose) in
       List.iter2 (Backend_splice.Splice.splice_file ~dry:!dry env) !pdsts !odsts;
-      if !warn then Backend_splice.Splice.warn env;
+      if !warn_math then Backend_splice.Splice.warn_math env;
+      if !warn_prose then Backend_splice.Splice.warn_prose env;
 
     | Interpreter args ->
       log "Initializing interpreter...";
@@ -252,7 +260,7 @@ let () =
   with
   | Source.Error (at, msg) ->
     let pass = if !last_pass = "" then "" else "(pass " ^ !last_pass ^ ") " in
-    prerr_endline (Source.string_of_region at ^ ": " ^ pass ^ msg);
+    Source.print_error at (pass ^ msg);
     exit 1
   | exn ->
     flush_all ();

spectec/src/util/source.ml

@@ -50,3 +50,6 @@ let note {note; _} = note
 exception Error of region * string
 
 let error at category msg = raise (Error (at, category ^ " error: " ^ msg))
+
+let print_error at msg = prerr_endline (string_of_region at ^ ": " ^ msg)
+let print_warn at msg = prerr_endline (string_of_region at ^ ": warning: " ^ msg)

spectec/src/util/source.mli

@@ -31,3 +31,6 @@ val note : ('a, 'b) note_phrase -> 'b
 exception Error of region * string
 
 val error : region -> string -> string -> 'a
+
+val print_error : region -> string -> unit
+val print_warn : region -> string -> unit