Implement higher-order def parameters

spectec/doc/Language.md

@@ -228,12 +228,14 @@ arg ::=
   exp
   "syntax" typ
   "grammar" sym
+  "def" defid
 
 params ::= ("(" list(param ",") ")")?
 param ::=
   (varid ":") typ
   "syntax" synid
   "grammar" gramid ":" typ
+  "def" "$" defid params ":" typ
 
 def ::=
   "syntax" varid params hint*                               syntax declaration

spectec/src/backend-latex/render.ml

@@ -1268,6 +1268,7 @@ and render_arg env arg =
   | ExpA e -> render_exp env e
   | TypA t -> render_typ env t
   | GramA g -> render_sym env g
+  | DefA id -> render_defid env id
 
 and render_args env args =
   match List.map (render_arg env) args with
@@ -1279,6 +1280,7 @@ let render_param env p =
   | ExpP (id, t) -> if id.it = "_" then render_typ env t else render_varid env id
   | TypP id -> render_typid env id
   | GramP (id, _t) -> render_gramid env id
+  | DefP (id, _ps, _t) -> render_defid env id
 
 let _render_params env = function
   | [] -> ""

spectec/src/el/ast.ml

@@ -175,12 +175,14 @@ and param' =
   | ExpP of id * typ                         (* varid `:` typ *)
   | TypP of id                               (* `syntax` varid *)
   | GramP of id * typ                        (* `grammar` gramid `:` typ *)
+  | DefP of id * param list * typ            (* `def` `$` defid params `:` typ *)
 
 and arg = arg' ref phrase
 and arg' =
   | ExpA of exp                              (* exp *)
   | TypA of typ                              (* `syntax` typ *)
   | GramA of sym                             (* `grammar` sym *)
+  | DefA of id                               (* `def` defid *)
 
 and def = def' phrase
 and def' =

spectec/src/el/convert.ml

@@ -173,13 +173,15 @@ let exp_of_arg a =
   | ExpA e -> e
   | _ -> error a.at "malformed expression"
 
-let param_of_arg a =
+let rec param_of_arg a =
   (match !(a.it) with
   | ExpA e ->
     (match e.it with
     | TypE ({it = VarE (id, []); _}, t) -> ExpP (id, t)
     | VarE (id, args) ->
       ExpP (id, typ_of_exp (VarE (strip_var_suffix id, args) $ e.at))
+    | TypE ({it = CallE (id, as_); _}, t) ->
+      DefP (id, List.map param_of_arg as_, t)
     | _ -> ExpP ("_" $ e.at, typ_of_exp e)
     )
   | TypA {it = VarT (id, []); _} ->
@@ -188,12 +190,13 @@ let param_of_arg a =
     TypP id
   | GramA {it = AttrG ({it = VarE (id, []); _}, g); _} ->
     GramP (id, typ_of_exp (exp_of_sym g))
-  | _ -> error a.at "malformed grammar"
+  | _ -> error a.at "malformed parameter"
   ) $ a.at
 
 let arg_of_param p =
   (match p.it with
   | ExpP (id, _t) -> ExpA ((*TypE ( *)VarE (id, []) $ id.at(*, t) $ p.at*))
   | TypP id -> TypA (VarT (id, []) $ id.at)
   | GramP (id, _t) -> GramA (VarG (id, []) $ id.at)
+  | DefP (id, _params, _t) -> DefA id
   ) |> ref $ p.at

spectec/src/el/eq.ml

@@ -165,11 +165,14 @@ and eq_arg a1 a2 =
   | ExpA e1, ExpA e2 -> eq_exp e1 e2
   | TypA t1, TypA t2 -> eq_typ t1 t2
   | GramA g1, GramA g2 -> eq_sym g1 g2
+  | DefA id1, DefA id2 -> eq_id id1 id2
   | _, _ -> false
 
 and eq_param p1 p2 =
   match p1.it, p2.it with
   | ExpP (id1, t1), ExpP (id2, t2) -> eq_id id1 id2 && eq_typ t1 t2
   | TypP id1, TypP id2 -> eq_id id1 id2
   | GramP (id1, t1), GramP (id2, t2) -> eq_id id1 id2 && eq_typ t1 t2
+  | DefP (id1, ps1, t1), DefP (id2, ps2, t2) ->
+    eq_id id1 id2 && eq_list eq_param ps1 ps2 && eq_typ t1 t2
   | _, _ -> false

spectec/src/el/free.ml

@@ -73,6 +73,7 @@ let free_defid id = {empty with defid = Set.singleton id.it}
 let bound_typid id = if id.it = "_" then empty else free_typid id
 let bound_gramid id = if id.it = "_" then empty else free_gramid id
 let bound_varid id = if id.it = "_" then empty else free_varid id
+let bound_defid id = if id.it = "_" then empty else free_defid id
 
 
 (* Iterations *)
@@ -280,30 +281,35 @@ and free_arg a =
   | ExpA e -> free_exp e
   | TypA t -> free_typ t
   | GramA g -> free_sym g
+  | DefA id -> free_defid id
 
 and det_arg a =
   match !(a.it) with
   | ExpA e -> det_exp e
   | TypA t -> free_typ t  (* must be an id *)
   | GramA g -> free_sym g (* must be an id *)
+  | DefA id -> free_defid id
 
 and idx_arg a =
   match !(a.it) with
   | ExpA e -> idx_exp e
   | TypA _ -> empty
   | GramA _ -> empty
+  | DefA _ -> empty
 
 and free_param p =
   match p.it with
   | ExpP (_, t) -> free_typ t
   | TypP _ -> empty
   | GramP (_, t) -> free_typ t
+  | DefP (_, ps, t) -> free_params ps + free_typ t - bound_params ps
 
 and bound_param p =
   match p.it with
   | ExpP (id, _) -> bound_varid id
   | TypP id -> bound_typid id
   | GramP (id, _) -> bound_gramid id
+  | DefP (id, _, _) -> bound_defid id
 
 and free_args as_ = free_list free_arg as_
 and det_args as_ = free_list det_arg as_

spectec/src/el/iter.ml

@@ -202,12 +202,14 @@ and arg a =
   | ExpA e -> exp e
   | TypA t -> typ t
   | GramA g -> sym g
+  | DefA x -> defid x
 
 and param p =
   match p.it with
   | ExpP (x, t) -> varid x; typ t
   | TypP x -> typid x
   | GramP (x, t) -> gramid x; typ t
+  | DefP (x, ps, t) -> defid x; params ps; typ t
 
 and args as_ = list arg as_
 and params ps = list param ps
@@ -309,6 +311,7 @@ and clone_arg a =
   | ExpA e -> ExpA (clone_exp e)
   | TypA t -> TypA (clone_typ t)
   | GramA _ as a' -> a'
+  | DefA _ as a' -> a'
   ) |> ref $ a.at
 
 and clone_hint hint = {hint with hintexp = clone_exp hint.hintexp}

spectec/src/el/print.ml

@@ -247,18 +247,20 @@ and string_of_arg a =
   | ExpA e -> string_of_exp e
   | TypA t -> "syntax " ^ string_of_typ t
   | GramA g -> "grammar " ^ string_of_sym g
+  | DefA id -> "def " ^ string_of_defid id
 
 and string_of_args = function
   | [] -> ""
   | args -> "(" ^ concat ", " (List.map string_of_arg args) ^ ")"
 
-let string_of_param p =
+let rec string_of_param p =
   match p.it with
   | ExpP (id, t) -> (if id.it = "_" then "" else string_of_varid id ^ " : ") ^ string_of_typ t
   | TypP id -> "syntax " ^ string_of_typid id
   | GramP (id, t) -> "grammar " ^ string_of_gramid id ^ " : " ^ string_of_typ t
+  | DefP (id, ps, t) -> "def " ^ string_of_defid id ^ string_of_params ps ^ " : " ^ string_of_typ t
 
-let string_of_params = function
+and string_of_params = function
   | [] -> ""
   | ps -> "(" ^ concat ", " (List.map string_of_param ps) ^ ")"
 

spectec/src/el/subst.ml

@@ -10,6 +10,7 @@ type subst =
   { varid : exp Map.t;
     typid : typ Map.t;
     gramid : sym Map.t;
+    defid : id Map.t;
   }
 
 type t = subst
@@ -18,20 +19,24 @@ let empty =
   { varid = Map.empty;
     typid = Map.empty;
     gramid = Map.empty;
+    defid = Map.empty;
   }
 
 let mem_varid s id = Map.mem id.it s.varid
 let mem_typid s id = Map.mem id.it s.typid
 let mem_gramid s id = Map.mem id.it s.gramid
+let mem_defid s id = Map.mem id.it s.defid
 
 let add_varid s id e = if id.it = "_" then s else {s with varid = Map.add id.it e s.varid}
 let add_typid s id t = if id.it = "_" then s else {s with typid = Map.add id.it t s.typid}
 let add_gramid s id g = if id.it = "_" then s else {s with gramid = Map.add id.it g s.gramid}
+let add_defid s id id' = if id.it = "_" then s else {s with defid = Map.add id.it id' s.defid}
 
 let union s1 s2 =
   { varid = Map.union (fun _ _e1 e2 -> Some e2) s1.varid s2.varid;
     typid = Map.union (fun _ _t1 t2 -> Some t2) s1.typid s2.typid;
     gramid = Map.union (fun _ _g1 g2 -> Some g2) s1.gramid s2.gramid;
+    defid = Map.union (fun _ _id1 id2 -> Some id2) s1.defid s2.defid;
   }
 
 
@@ -58,6 +63,11 @@ let subst_gramid s id =
   | Some {it = VarG (id', []); _} -> id'
   | Some _ -> raise (Invalid_argument "subst_gramid")
 
+let subst_defid s id =
+  match Map.find_opt id.it s.defid with
+  | None -> id
+  | Some id' -> id'
+
 
 (* Iterations *)
 
@@ -134,7 +144,7 @@ and subst_exp s e =
   | TupE es -> TupE (subst_list subst_exp s es)
   | InfixE (e1, atom, e2) -> InfixE (subst_exp s e1, atom, subst_exp s e2)
   | BrackE (l, e1, r) -> BrackE (l, subst_exp s e1, r)
-  | CallE (id, args) -> CallE (id, subst_list subst_arg s args)
+  | CallE (id, args) -> CallE (subst_defid s id, subst_list subst_arg s args)
   | IterE (e1, iter) -> IterE (subst_exp s e1, subst_iter s iter)
   | TypE (e1, t) -> TypE (subst_exp s e1, subst_typ s t)
   | ArithE e1 -> ArithE (subst_exp s e1)
@@ -210,11 +220,13 @@ and subst_arg s a =
   | ExpA e -> ExpA (subst_exp s e)
   | TypA t -> TypA (subst_typ s t)
   | GramA g -> GramA (subst_sym s g)
+  | DefA id -> DefA (subst_defid s id)
   ) $ a.at
 
 and subst_param s p =
   (match p.it with
   | ExpP (id, t) -> ExpP (id, subst_typ s t)
   | TypP id -> TypP id
   | GramP (id, t) -> GramP (id, subst_typ s t)
+  | DefP (id, ps, t) -> DefP (id, List.map (subst_param s) ps, subst_typ s t)
   ) $ p.at

spectec/src/el/subst.mli

@@ -6,6 +6,7 @@ type subst =
   { varid : exp Map.t;
     typid : typ Map.t;
     gramid : sym Map.t;
+    defid : id Map.t;
   }
 type t = subst
 
@@ -15,10 +16,12 @@ val union : subst -> subst -> subst (* right overrides *)
 val add_varid : subst -> id -> exp -> subst
 val add_typid : subst -> id -> typ -> subst
 val add_gramid : subst -> id -> sym -> subst
+val add_defid : subst -> id -> id -> subst
 
 val mem_varid : subst -> id -> bool
 val mem_typid : subst -> id -> bool
 val mem_gramid : subst -> id -> bool
+val mem_defid : subst -> id -> bool
 
 val subst_iter : subst -> iter -> iter
 val subst_typ : subst -> typ -> typ

spectec/src/frontend/dim.ml

@@ -233,8 +233,9 @@ and check_arg env ctx a =
   | ExpA e -> check_exp env ctx e
   | TypA t -> check_typ env ctx t
   | GramA g -> check_sym env ctx g
+  | DefA _id -> ()
 
-let check_param env ctx p =
+and check_param env ctx p =
   match p.it with
   | ExpP (id, t) ->
     check_varid env ctx id;
@@ -243,6 +244,9 @@ let check_param env ctx p =
   | GramP (id, t) ->
     check_gramid env ctx id;
     check_typ env ctx t
+  | DefP (_id, ps, t) ->
+    List.iter (check_param env ctx) ps;
+    check_typ env ctx t
 
 let check_def d : env =
   let env = ref Env.empty in
@@ -455,6 +459,7 @@ and annot_arg env a : Il.Ast.arg * occur =
       let e', occur1 = annot_exp env e in
       ExpA e', occur1
     | TypA t -> TypA t, Env.empty
+    | DefA id -> DefA id, Env.empty
   in {a with it}, occur
 
 and annot_prem env prem : Il.Ast.prem * occur =