Minor syntax refactoring in EL

spectec/src/backend-latex/render.ml

@@ -179,7 +179,7 @@ let rec expand_iter args iter =
 
 and expand_exp args e =
   (match e.it with
-  | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ | EpsE -> e.it
+  | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE -> e.it
   | VarE (id, args') -> VarE (id, List.map (expand_arg args) args')
   | UnE (op, e) -> UnE (op, expand_exp args e)
   | BinE (e1, op, e2) ->
@@ -496,9 +496,9 @@ and render_typ env t =
     "\\begin{array}[t]{@{}l@{}l@{}}\n" ^
     concat_map_nl ",\\; " "\\\\\n  " (render_typfield env) tfs ^ " \\;\\}" ^
     "\\end{array}"
-  | CaseT (dots1, ids, tcases, dots2) ->
+  | CaseT (dots1, ts, tcases, dots2) ->
     altern_map_nl " ~|~ " " \\\\ &&|&\n" Fun.id
-      (render_dots dots1 @ map_nl_list (render_synid env) ids @
+      (render_dots dots1 @ map_nl_list (render_typ env) ts @
         map_nl_list (render_typcase env) tcases @ render_dots dots2)
   | RangeT tes ->
     altern_map_nl " ~|~ " "\\\\ &&|&\n" (render_typenum env) tes
@@ -532,14 +532,14 @@ and render_exp env e =
   | VarE (id, args) ->
     render_apply render_varid render_exp env env.show_syn id args
   | BoolE b -> render_atom env (Atom (string_of_bool b))
-  | NatE n -> string_of_int n
-  | HexE n ->
+  | NatE (DecOp, n) -> string_of_int n
+  | NatE (HexOp, n) ->
     let fmt : (_, _, _) format =
       if n < 0x100 then "%02X" else
       if n < 0x10000 then "%04X" else
       "%X"
     in "\\mathtt{0x" ^ Printf.sprintf fmt n ^ "}"
-  | CharE n ->
+  | NatE (CharOp, n) ->
     let fmt : (_, _, _) format =
       if n < 0x100 then "%02X" else
       if n < 0x10000 then "%04X" else
@@ -678,14 +678,14 @@ and render_sym env g =
   match g.it with
   | VarG (id, args) ->
     render_apply render_gramid render_exp_as_sym env env.show_gram id args
-  | NatG n -> string_of_int n
-  | HexG n ->
+  | NatG (DecOp, n) -> string_of_int n
+  | NatG (HexOp, n) ->
     let fmt : (_, _, _) format =
       if n < 0x100 then "%02X" else
       if n < 0x10000 then "%04X" else
       "%X"
     in "\\mathtt{0x" ^ Printf.sprintf fmt n ^ "}"
-  | CharG n ->
+  | NatG (CharOp, n) ->
     let fmt : (_, _, _) format =
       if n < 0x100 then "%02X" else
       if n < 0x10000 then "%04X" else
@@ -838,9 +838,9 @@ let render_reddef env d =
 
 let render_funcdef env d =
   match d.it with
-  | DefD (id1, e1, e2, prems) ->
-    render_exp env (CallE (id1, e1) $ d.at) ^ " &=& " ^
-      render_exp env e2 ^ render_conditions env "&&&" prems
+  | DefD (id1, args, e, prems) ->
+    render_exp env (CallE (id1, args) $ d.at) ^ " &=& " ^
+      render_exp env e ^ render_conditions env "&&&" prems
   | _ -> failwith "render_funcdef"
 
 let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function

spectec/src/el/ast.ml

@@ -81,7 +81,7 @@ and typ' =
   | IterT of typ * iter          (* typ iter *)
   (* The forms below are only allowed in type definitions *)
   | StrT of typfield nl_list     (* `{` list(typfield,`,`') `}` *)
-  | CaseT of dots * id nl_list * typcase nl_list * dots (* `|` list(`...`|varid|typcase, `|`) *)
+  | CaseT of dots * typ nl_list * typcase nl_list * dots (* `|` list(`...`|typ|typcase, `|`) *)
   | RangeT of typenum nl_list    (* exp `|` `...` `|` exp *)
   | AtomT of atom                (* atom *)
   | SeqT of typ list             (* `eps` / typ typ *)
@@ -95,6 +95,11 @@ and typenum = exp * exp option                  (* exp (`|` exp (`|` `...` `|` e
 
 (* Expressions *)
 
+and natop =
+  | DecOp   (* n *)
+  | HexOp   (* 0xhex *)
+  | CharOp  (* U+hex *)
+
 and unop =
   | NotOp   (* `~` *)
   | PlusOp  (* `+` *)
@@ -124,9 +129,7 @@ and exp' =
   | VarE of id * arg list        (* varid *)
   | AtomE of atom                (* atom *)
   | BoolE of bool                (* bool *)
-  | NatE of nat                  (* nat *)
-  | HexE of nat                  (* 0xhex *)
-  | CharE of nat                 (* 0uhex *)
+  | NatE of natop * nat          (* nat *)
   | TextE of text                (* text *)
   | UnE of unop * exp            (* unop exp *)
   | BinE of exp * binop * exp    (* exp binop exp *)
@@ -168,9 +171,7 @@ and path' =
 and sym = sym' phrase
 and sym' =
   | VarG of id * arg list                    (* gramid (`(` arg,* `)`)? *)
-  | NatG of int                              (* nat *)
-  | HexG of int                              (* 0xhex *)
-  | CharG of int                             (* U+hex *)
+  | NatG of natop * int                      (* nat *)
   | TextG of string                          (* `"`text`"` *)
   | EpsG                                     (* `eps` *)
   | SeqG of sym nl_list                      (* sym sym *)
@@ -211,7 +212,7 @@ and def' =
   | RuleD of id * id * exp * premise nl_list       (* `rule` relid ruleid? `:` exp (`--` premise)* *)
   | VarD of id * typ * hint list                   (* `var` varid `:` typ *)
   | DecD of id * param list * typ * hint list      (* `def` `$` defid params `:` typ hint* *)
-  | DefD of id * arg list * exp * premise nl_list  (* `def` `$` defid exp? `=` exp (`--` premise)* *)
+  | DefD of id * arg list * exp * premise nl_list  (* `def` `$` defid args `=` exp (`--` premise)* *)
   | SepD                                           (* separator *)
   | HintD of hintdef
 

spectec/src/el/convert.ml

@@ -4,9 +4,18 @@ open Ast
 
 
 let filter_nl xs = List.filter_map (function Nl -> None | Elem x -> Some x) xs
+let find_nl_list f xs = List.find_opt f (filter_nl xs)
 let iter_nl_list f xs = List.iter f (filter_nl xs)
 let map_filter_nl_list f xs = List.map f (filter_nl xs)
 let map_nl_list f xs = List.map (function Nl -> Nl | Elem x -> Elem (f x)) xs
+let concat_map_nl_list f xs = List.concat_map (function Nl -> [Nl] | Elem x -> f x) xs
+
+
+let strip_var_suffix id =
+  match String.index_opt id.it '_', String.index_opt id.it '\'' with
+  | None, None -> id
+  | None, Some n | Some n, None -> String.sub id.it 0 n $ id.at
+  | Some n1, Some n2 -> String.sub id.it 0 (min n1 n2) $ id.at
 
 
 let arg_of_exp e =
@@ -58,7 +67,7 @@ let rec exp_of_typ t =
   | SeqT ts -> SeqE (List.map exp_of_typ ts)
   | InfixT (t1, atom, t2) -> InfixE (exp_of_typ t1, atom, exp_of_typ t2)
   | BrackT (l, t1, r) -> BrackE (l, exp_of_typ t1, r)
-  | _ -> Source.error t.at "syntax" "malformed expression"
+  | CaseT _ | RangeT _ -> Source.error t.at "syntax" "malformed expression"
   ) $ t.at
 
 and expfield_of_typfield (atom, (t, _prems), _) =
@@ -68,9 +77,7 @@ and expfield_of_typfield (atom, (t, _prems), _) =
 let rec sym_of_exp e =
   (match e.it with
   | VarE (id, args) -> VarG (id, args)
-  | NatE n -> NatG n
-  | HexE n -> HexG n
-  | CharE c -> CharG c
+  | NatE (op, n) -> NatG (op, n)
   | TextE s -> TextG s
   | EpsE -> EpsG
   | SeqE es -> SeqG (List.map (fun e -> Elem (sym_of_exp e)) es)
@@ -84,9 +91,7 @@ let rec sym_of_exp e =
 let rec exp_of_sym g =
   (match g.it with
   | VarG (id, args) -> VarE (id, args)
-  | NatG n -> NatE n
-  | HexG n -> HexE n
-  | CharG n -> CharE n
+  | NatG (op, n) -> NatE (op, n)
   | TextG t -> TextE t
   | EpsG -> EpsE
   | SeqG gs -> SeqE (map_filter_nl_list exp_of_sym gs)
@@ -112,3 +117,10 @@ let param_of_arg a =
     GramP (id, typ_of_exp (exp_of_sym g))
   | _ -> Source.error a.at "syntax" "malformed grammar"
   ) $ a.at
+
+let arg_of_param p =
+  (match p.it with
+  | ExpP (id, _t) -> ExpA (VarE (id, []) $ id.at)
+  | SynP id -> SynA (VarT (id, []) $ id.at)
+  | GramP (id, _t) -> GramA (VarG (id, []) $ id.at)
+  ) |> ref $ p.at

spectec/src/el/convert.mli

@@ -1,8 +1,10 @@
 open Ast
 
 val filter_nl : 'a nl_list -> 'a list
+val find_nl_list : ('a -> bool) -> 'a nl_list -> 'a option
 val iter_nl_list : ('a -> unit) -> 'a nl_list -> unit
 val map_nl_list : ('a -> 'b) -> 'a nl_list -> 'b nl_list
+val concat_map_nl_list : ('a -> 'b nl_list) -> 'a nl_list -> 'b nl_list
 val map_filter_nl_list : ('a -> 'b) -> 'a nl_list -> 'b list
 
 val typ_of_exp : exp -> typ (* raises Source.Error *)
@@ -12,3 +14,6 @@ val exp_of_sym : sym -> exp (* raises Source.Error *)
 val arg_of_exp : exp -> arg (* raises Source.Error *)
 val exp_of_arg : arg -> exp (* raises Source.Error *)
 val param_of_arg : arg -> param (* raises Source.Error *)
+val arg_of_param : param -> arg (* raises Source.Error *)
+
+val strip_var_suffix : id -> id

spectec/src/el/eq.ml

@@ -44,8 +44,8 @@ and eq_typ t1 t2 =
   | IterT (t11, iter1), IterT (t21, iter2) ->
     eq_typ t11 t21 && eq_iter iter1 iter2
   | StrT tfs1, StrT tfs2 -> eq_nl_list eq_typfield tfs1 tfs2
-  | CaseT (dots11, ids1, tcs1, dots12), CaseT (dots21, ids2, tcs2, dots22) ->
-    dots11 = dots21 && eq_nl_list (=) ids1 ids2 &&
+  | CaseT (dots11, ts1, tcs1, dots12), CaseT (dots21, ts2, tcs2, dots22) ->
+    dots11 = dots21 && eq_nl_list eq_typ ts1 ts2 &&
     eq_nl_list eq_typcase tcs1 tcs2 && dots12 = dots22
   | RangeT tes1, RangeT tes2 -> eq_nl_list eq_typenum tes1 tes2
   | SeqT ts1, SeqT ts2 -> eq_list eq_typ ts1 ts2

spectec/src/el/free.ml

@@ -80,8 +80,8 @@ and free_typ t =
   | TupT ts -> free_list free_typ ts
   | IterT (t1, iter) -> union (free_typ t1) (free_iter iter)
   | StrT tfs -> free_nl_list free_typfield tfs
-  | CaseT (_, ids, tcs, _) ->
-    union (free_nl_list free_synid ids) (free_nl_list free_typcase tcs)
+  | CaseT (_, ts, tcs, _) ->
+    union (free_nl_list free_typ ts) (free_nl_list free_typcase tcs)
   | RangeT tes -> free_nl_list free_typenum tes
   | AtomT _ -> empty
   | SeqT ts -> free_list free_typ ts
@@ -101,7 +101,7 @@ and free_typenum (e, eo) =
 and free_exp e =
   match e.it with
   | VarE (id, args) -> union (free_varid id) (free_list free_arg args)
-  | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ | EpsE | HoleE _ ->
+  | AtomE _ | BoolE _ | NatE _ | TextE _ | EpsE | HoleE _ ->
     empty
   | UnE (_, e1) | DotE (e1, _) | LenE e1
   | ParenE (e1, _) | BrackE (_, e1, _) -> free_exp e1
@@ -133,7 +133,7 @@ and free_path p =
 and bound_exp e =
   match e.it with
   | CmpE (e1, EqOp, e2) -> union (pat_exp e1) (pat_exp e2)
-  | VarE _ | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _
+  | VarE _ | AtomE _ | BoolE _ | NatE _ | TextE _
   | SizeE _ | EpsE | HoleE _ -> empty
   | UnE (_, e1) | DotE (e1, _) | LenE e1
   | ParenE (e1, _) | BrackE (_, e1, _) -> bound_exp e1
@@ -229,7 +229,7 @@ and bound_prem prem =
 and free_sym g =
   match g.it with
   | VarG (id, args) -> union (free_gramid id) (free_list free_arg args)
-  | NatG _ | HexG _ | CharG _ | TextG _ | EpsG -> empty
+  | NatG _ | TextG _ | EpsG -> empty
   | SeqG gs | AltG gs -> free_nl_list free_sym gs
   | RangeG (g1, g2) -> union (free_sym g1) (free_sym g2)
   | ParenG g1 -> free_sym g1
@@ -267,24 +267,27 @@ let bound_param p =
   | SynP id -> bound_synid id
   | GramP (id, _) -> bound_gramid id
 
+let free_args args = free_list free_arg args
+let free_params ps = free_list free_param ps
+let bound_args args = free_list pat_arg args
 let bound_params ps = free_list bound_param ps
 
 let free_def d =
   match d.it with
   | SynD (_id1, _id2, ps, t, _hints) ->
-    union (free_list free_param ps) (diff (free_typ t) (bound_params ps))
+    union (free_params ps) (diff (free_typ t) (bound_params ps))
   | GramD (_id1, _id2, ps, t, gram, _hints) ->
     union
-      (free_list free_param ps)
+      (free_params ps)
       (diff (union (free_typ t) (free_gram gram)) (bound_params ps))
   | VarD _ | SepD -> empty
   | RelD (_id, t, _hints) -> free_typ t
   | RuleD (id1, _id2, e, prems) ->
     union (free_relid id1) (union (free_exp e) (free_nl_list free_prem prems))
   | DecD (_id, ps, t, _hints) ->
-    union (free_list free_param ps) (diff (free_typ t) (bound_params ps))
+    union (free_params ps) (diff (free_typ t) (bound_params ps))
   | DefD (id, args, e, prems) ->
     union
-      (union (free_defid id) (free_list free_arg args))
-      (union (free_exp e) (free_nl_list free_prem prems))
+      (union (free_defid id) (free_args args))
+      (diff (union (free_exp e) (free_nl_list free_prem prems)) (bound_args args))
   | HintD _ -> empty

spectec/src/el/print.ml

@@ -109,9 +109,9 @@ and string_of_typ t =
   | IterT (t1, iter) -> string_of_typ t1 ^ string_of_iter iter
   | StrT tfs ->
     "{" ^ concat ", " (map_filter_nl_list string_of_typfield tfs) ^ "}"
-  | CaseT (dots1, ids, tcases, dots2) ->
+  | CaseT (dots1, ts, tcases, dots2) ->
     "\n  | " ^ concat "\n  | "
-      (strings_of_dots dots1 @ map_filter_nl_list it ids @
+      (strings_of_dots dots1 @ map_filter_nl_list string_of_typ ts @
         map_filter_nl_list string_of_typcase tcases @ strings_of_dots dots2)
   | RangeT tes -> concat " | " (map_filter_nl_list string_of_typenum tes)
   | AtomT atom -> string_of_atom atom
@@ -146,9 +146,9 @@ and string_of_exp e =
   | VarE (id, args) -> id.it ^ string_of_args args
   | AtomE atom -> string_of_atom atom
   | BoolE b -> string_of_bool b
-  | NatE n -> string_of_int n
-  | HexE n -> Printf.sprintf "0x%X" n
-  | CharE n -> Printf.sprintf "U+%X" n
+  | NatE (DecOp, n) -> string_of_int n
+  | NatE (HexOp, n) -> Printf.sprintf "0x%X" n
+  | NatE (CharOp, n) -> Printf.sprintf "U+%X" n
   | TextE t -> "\"" ^ String.escaped t ^ "\""
   | UnE (op, e2) -> string_of_unop op ^ " " ^ string_of_exp e2
   | BinE (e1, op, e2) ->
@@ -222,9 +222,9 @@ and string_of_prem prem =
 and string_of_sym g =
   match g.it with
   | VarG (id, args) -> id.it ^ string_of_args args
-  | NatG n -> string_of_int n
-  | HexG n -> Printf.sprintf "0x%X" n
-  | CharG n -> Printf.sprintf "U+%X" n
+  | NatG (DecOp, n) -> string_of_int n
+  | NatG (HexOp, n) -> Printf.sprintf "0x%X" n
+  | NatG (CharOp, n) -> Printf.sprintf "U+%X" n
   | TextG t -> "\"" ^ String.escaped t ^ "\""
   | EpsG -> "eps"
   | SeqG gs -> "{" ^ concat " " (map_filter_nl_list string_of_sym gs) ^ "}"

spectec/src/el/subst.ml

@@ -33,12 +33,6 @@ let subst_varid s id =
   | Some {it = VarE (id', []); _} -> id'
   | Some _ -> raise (Invalid_argument "subst_varid")
 
-let subst_synid s id =
-  match Map.find_opt id.it s.synid with
-  | None -> id
-  | Some {it = VarT (id', []); _} -> id'
-  | Some _ -> raise (Invalid_argument "subst_synid")
-
 let subst_gramid s id =
   match Map.find_opt id.it s.gramid with
   | None -> id
@@ -69,8 +63,8 @@ and subst_typ s t =
   | TupT ts -> TupT (subst_list subst_typ s ts)
   | IterT (t1, iter) -> IterT (subst_typ s t1, subst_iter s iter)
   | StrT tfs -> StrT (subst_nl_list subst_typfield s tfs)
-  | CaseT (dots1, ids, tcs, dots2) ->
-    CaseT (dots1, subst_nl_list subst_synid s ids,
+  | CaseT (dots1, ts, tcs, dots2) ->
+    CaseT (dots1, subst_nl_list subst_typ s ts,
       subst_nl_list subst_typcase s tcs, dots2)
   | RangeT tes -> RangeT (subst_nl_list subst_typenum s tes)
   | SeqT ts -> SeqT (subst_list subst_typ s ts)
@@ -96,7 +90,7 @@ and subst_exp s e =
     | Some e' ->
       assert (args = []); e'  (* We do not support higher-order substitutions yet *)
     ).it
-  | AtomE _ | BoolE _ | NatE _ | HexE _ | CharE _ | TextE _ -> e.it
+  | AtomE _ | BoolE _ | NatE _ | TextE _ -> e.it
   | UnE (op, e1) -> UnE (op, subst_exp s e1)
   | BinE (e1, op, e2) -> BinE (subst_exp s e1, op, subst_exp s e2)
   | CmpE (e1, op, e2) -> CmpE (subst_exp s e1, op, subst_exp s e2)
@@ -156,7 +150,7 @@ and subst_sym s g =
     | Some g' ->
       assert (args = []); g' (* We do not support higher-order substitutions yet *)
     ).it
-  | NatG _ | HexG _ | CharG _ | TextG _ -> g.it
+  | NatG _ | TextG _ -> g.it
   | EpsG -> EpsG
   | SeqG gs -> SeqG (subst_nl_list subst_sym s gs)
   | AltG gs -> AltG (subst_nl_list subst_sym s gs)

spectec/src/el/subst.mli

@@ -18,5 +18,6 @@ val subst_typ : subst -> typ -> typ
 val subst_exp : subst -> exp -> exp
 val subst_path : subst -> path -> path
 val subst_prem : subst -> premise -> premise
+val subst_sym : subst -> sym -> sym
 val subst_arg : subst -> arg -> arg
 val subst_param : subst -> param -> param