Wasm-DSL · nomeata · Apr 8, 2023 · Apr 8, 2023 · Apr 8, 2023 · Apr 8, 2023
diff --git a/spectec/src/dune b/spectec/src/dune
@@ -6,6 +6,7 @@
     (re_export el)
     (re_export il)
     (re_export frontend)
+    (re_export middlend)
     (re_export backend_latex)
     (re_export backend_prose)
   )

diff --git a/spectec/src/frontend/multiplicity.ml b/spectec/src/frontend/multiplicity.ml
@@ -228,6 +228,9 @@ and annot_exp env e : Il.Ast.exp * occur =
   | OptE (Some e1) ->
     let e1', occur1 = annot_exp env e1 in
     OptE (Some e1') $ e.at, occur1
+  | TheE e1 ->
+    let e1', occur1 = annot_exp env e1 in
+    TheE e1' $ e.at, occur1
   | ListE es ->
     let es', occurs = List.split (List.map (annot_exp env) es) in
     ListE es' $ e.at, List.fold_left union Env.empty occurs

diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
@@ -111,6 +111,7 @@ and exp' =
   | CallE of id * exp            (* defid exp? *)
   | IterE of exp * iterexp       (* exp iter *)
   | OptE of exp option           (* exp? : typ? *)
+  | TheE of exp                  (* THE exp *)
   | ListE of exp list            (* [exp ... exp] *)
   | CatE of exp * exp            (* exp :: exp *)
   | CaseE of atom * exp * typ    (* atom exp : typ *)

diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml
@@ -13,6 +13,12 @@ let eq_list eq_x xs1 xs2 =
   List.length xs1 = List.length xs2 && List.for_all2 eq_x xs1 xs2
 
 
+(* Ids *)
+
+let eq_id i1 i2 =
+  i1.it = i2.it
+
+
 (* Iteration *)
 
 let rec eq_iter iter1 iter2 =
@@ -32,7 +38,7 @@ and eq_typ t1 t2 =
   *)
   t1.it = t2.it ||
   match t1.it, t2.it with
-  | VarT id1, VarT id2 -> id1.it = id2.it
+  | VarT id1, VarT id2 -> eq_id id1 id2
   | TupT ts1, TupT ts2 -> eq_list eq_typ ts1 ts2
   | IterT (t11, iter1), IterT (t21, iter2) ->
     eq_typ t11 t21 && eq_iter iter1 iter2
@@ -87,4 +93,4 @@ and eq_path p1 p2 =
   | _, _ -> false
 
 and eq_iterexp (iter1, ids1) (iter2, ids2) =
-  eq_iter iter1 iter2 && eq_list (fun id1 id2 -> id1.it = id2.it) ids1 ids2
+  eq_iter iter1 iter2 && eq_list eq_id ids1 ids2
diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml
@@ -77,7 +77,7 @@ and free_exp e =
   match e.it with
   | VarE id -> free_varid id
   | BoolE _ | NatE _ | TextE _ -> empty
-  | UnE (_, e1) | LenE e1 | MixE (_, e1) | SubE (e1, _, _) ->
+  | UnE (_, e1) | LenE e1 | TheE e1 | MixE (_, e1) | SubE (e1, _, _) ->
     free_exp e1
   | BinE (_, e1, e2) | CmpE (_, e1, e2)
   | IdxE (e1, e2) | CompE (e1, e2) | CatE (e1, e2) ->

diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
@@ -145,9 +145,10 @@ and string_of_exp e =
   | LenE e1 -> "|" ^ string_of_exp e1 ^ "|"
   | TupE es -> "(" ^ string_of_exps ", " es ^ ")"
   | MixE (op, e1) -> string_of_mixop op ^ string_of_exp_args e1
-  | CallE (id, e) -> "$" ^ id.it ^ string_of_exp_args e
+  | CallE (id, e1) -> "$" ^ id.it ^ string_of_exp_args e1
   | IterE (e1, iter) -> string_of_exp e1 ^ string_of_iterexp iter
   | OptE eo -> "?(" ^ string_of_exps "" (Option.to_list eo) ^ ")"
+  | TheE e1 -> "!(" ^ string_of_exp e1 ^ ")"
   | ListE es -> "[" ^ string_of_exps " " es ^ "]"
   | CatE (e1, e2) -> string_of_exp e1 ^ " :: " ^ string_of_exp e2
   | CaseE (atom, e1, t) ->

diff --git a/spectec/src/il/validation.ml b/spectec/src/il/validation.ml
@@ -317,6 +317,7 @@ and infer_exp env e : typ =
     let iter' = match fst iter with ListN _ -> List | iter' -> iter' in
     IterT (infer_exp env e1, iter') $ e.at
   | OptE _ -> error e.at "cannot infer type of option"
+  | TheE e1 -> as_iter_typ Opt "option" env Check (infer_exp env e1) e1.at
   | ListE _ -> error e.at "cannot infer type of list"
   | CatE _ -> error e.at "cannot infer type of concatenation"
   | CaseE _ -> error e.at "cannot infer type of case constructor"
@@ -412,6 +413,8 @@ and valid_exp env e t =
   | OptE eo ->
     let t1 = as_iter_typ Opt "option" env Check t e.at in
     Option.iter (fun e1 -> valid_exp env e1 t1) eo
+  | TheE e1 ->
+    valid_exp env e1 (IterT (t, Opt) $ e1.at)
   | ListE es ->
     let t1 = as_iter_typ List "list" env Check t e.at in
     List.iter (fun eI -> valid_exp env eI t1) es

diff --git a/spectec/src/middlend/dune b/spectec/src/middlend/dune
@@ -0,0 +1,5 @@
+(library
+  (name middlend)
+  (libraries util il)
+  (modules totalize)
+)
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
@@ -0,0 +1,145 @@
+(*
+This transformation totalizes partial functions.
+
+Partial functions are recognized by the partial flag hint (for now, inference
+would be possible).
+
+The declarations are changed:
+
+ * the return type is wrapped in the option type `?`
+ * all clauses rhs' are wrapped in the option type injection `?(…)`
+ * a catch-all clause is added returning `null`
+
+All calls to such functions are wrapped in option projection `THE e`.
+
+*)
+
+open Util
+open Source
+open Il.Ast
+
+(* Errors *)
+
+let _error at msg = Source.error at "totalize" msg
+
+(* Environment *)
+
+module S = Set.Make(String)
+
+type env =
+  { mutable total_funs : S.t;
+  }
+
+let new_env () : env =
+  { total_funs = S.empty;
+  }
+
+let is_partial (env : env) (id : id) = S.mem id.it env.total_funs
+
+let register (env : env) (id :id) =
+  env.total_funs <- S.add id.it env.total_funs
+
+(* Transformation *)
+
+(* The main transformation case *)
+let rec t_exp env exp =
+  let exp' = t_exp2 env exp in
+  match exp'.it with
+  | CallE (f, _) when is_partial env f ->
+    TheE exp' $ no_region
+  | _ -> exp'
+
+and t_exp2 env x = { x with it = t_exp' env x.it }
+
+(* Expr traversal *)
+and t_exp' env = function
+  | (VarE _ | BoolE _ | NatE _ | TextE _) as e -> e
+  | UnE (unop, exp) -> UnE (unop, t_exp env exp)
+  | BinE (binop, exp1, exp2) -> BinE (binop, t_exp env exp1, t_exp env exp2)
+  | CmpE (cmpop, exp1, exp2) -> CmpE (cmpop, t_exp env exp1, t_exp env exp2)
+  | IdxE (exp1, exp2) -> IdxE (t_exp env exp1, t_exp env exp2)
+  | SliceE (exp1, exp2, exp3) -> SliceE (t_exp env exp1, t_exp env exp2, t_exp env exp3)
+  | UpdE (exp1, path, exp2) -> UpdE (t_exp env exp1, t_path env path, t_exp env exp2)
+  | ExtE (exp1, path, exp2) -> ExtE (t_exp env exp1, t_path env path, t_exp env exp2)
+  | StrE fields -> StrE (List.map (fun (a, e) -> a, t_exp env e) fields)
+  | DotE (t, e, a) -> DotE (t, t_exp env e, a)
+  | CompE (exp1, exp2) -> CompE (t_exp env exp1, t_exp env exp2)
+  | LenE exp -> LenE exp
+  | TupE es -> TupE (List.map (t_exp env) es)
+  | MixE (mixop, exp) -> MixE (mixop, t_exp env exp)
+  | CallE (a, exp) -> CallE (a, t_exp env exp)
+  | IterE (e, iterexp) -> IterE (t_exp env e, t_iterexp env iterexp)
+  | OptE None -> OptE None
+  | OptE (Some exp) -> OptE (Some exp)
+  | TheE exp -> TheE exp
+  | ListE es -> ListE (List.map (t_exp env) es)
+  | CatE (exp1, exp2) -> CatE (t_exp env exp1, t_exp env exp2)
+  | CaseE (a, e, t) -> CaseE (a, t_exp env e, t)
+  | SubE (e, t1, t2) -> SubE (e, t1, t2)
+
+and t_iter env = function
+  | ListN e -> ListN (t_exp env e)
+  | i -> i
+
+and t_iterexp env (iter, vs) = (t_iter env iter, vs)
+
+and t_path' env = function
+  | RootP -> RootP
+  | IdxP (path, e) -> IdxP (t_path env path, t_exp env e)
+  | DotP (path, a) -> DotP (t_path env path, a)
+
+and t_path env x = { x with it = t_path' env x.it }
+
+let rec t_prem' env = function
+  | RulePr (id, mixop, exp) -> RulePr (id, mixop, t_exp env exp)
+  | IfPr e -> IfPr (t_exp env e)
+  | ElsePr -> ElsePr
+  | IterPr (prem, iterexp) -> IterPr (t_prem env prem, t_iterexp env iterexp)
+
+and t_prem env x = { x with it = t_prem' env x.it }
+
+let t_prems env = List.map (t_prem env)
+
+let t_clause' env = function
+ | DefD (binds, lhs, rhs, prems) ->
+  DefD (binds, t_exp env lhs, t_exp env rhs, t_prems env prems)
+
+let t_clause env (clause : clause) = { clause with it = t_clause' env clause.it }
+
+let is_partial_hint hint = hint.hintid.it = "partial"
+
+let t_rule' env = function
+  | RuleD (id, binds, mixop, exp, prems) ->
+    RuleD (id, binds, mixop, t_exp env exp, t_prems env prems)
+
+let t_rule env x = { x with it = t_rule' env x.it }
+
+let rec t_def' env = function
+  | RecD defs -> RecD (List.map (t_def env) defs)
+  | DecD (id, typ1, typ2, clauses, hints) ->
+    let clauses' = List.map (t_clause env) clauses in
+    if List.exists is_partial_hint hints
+    then
+      let typ2' = IterT (typ2, Opt) $ no_region in
+      let clauses'' = List.map (fun clause -> match clause.it with
+        DefD (binds, lhs, rhs, prems) ->
+          { clause with it = DefD (binds, lhs, OptE (Some rhs) $ no_region, prems) }
+        ) clauses' in
+      let x = "x" $ no_region in
+      let catch_all = DefD ([(x, typ1, [])], VarE x $ no_region, OptE None $ no_region, []) $ no_region in
+      let hints' = List.filter (fun hint -> not (is_partial_hint hint)) hints in
+      register env id;
+      DecD (id, typ1, typ2', clauses'' @ [ catch_all ], hints')
+    else
+      DecD (id, typ1, typ2, clauses', hints)
+  | RelD (id, mixop, typ, rules, hints) ->
+    RelD (id, mixop, typ, List.map (t_rule env) rules, hints)
+  | def -> def
+
+and t_def env x = { x with it = t_def' env x.it }
+
+
+let transform (defs : script) =
+  let env = new_env () in
+  List.map (t_def env) defs
+
diff --git a/spectec/src/middlend/totalize.mli b/spectec/src/middlend/totalize.mli
@@ -0,0 +1 @@
+val transform : Il.Ast.script -> Il.Ast.script