From 4e023604b4378fa23eb295a0a63d9fc151137064 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 8 Apr 2023 16:52:38 +0200 Subject: [PATCH 1/6] Il-to-Il Totalization pass, adding TheE constructor --- spectec/src/dune | 1 + spectec/src/frontend/multiplicity.ml | 3 + spectec/src/il/ast.ml | 1 + spectec/src/il/eq.ml | 6 +- spectec/src/il/free.ml | 1 + spectec/src/il/print.ml | 1 + spectec/src/il/validation.ml | 3 + spectec/src/middlend/dune | 5 + spectec/src/middlend/totalize.ml | 145 +++++++++++++++++++++++++++ spectec/src/middlend/totalize.mli | 1 + 10 files changed, 166 insertions(+), 1 deletion(-) create mode 100644 spectec/src/middlend/dune create mode 100644 spectec/src/middlend/totalize.ml create mode 100644 spectec/src/middlend/totalize.mli diff --git a/spectec/src/dune b/spectec/src/dune index 0eb3c22f77..ea13545166 100644 --- 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 index 7733ad03b2..e9e716b0ef 100644 --- 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 index 05c29aaea2..2730a0cd9f 100644 --- 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 index 90c097b306..59411a5d33 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml @@ -12,6 +12,10 @@ let eq_opt eq_x xo1 xo2 = 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 *) @@ -32,7 +36,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 diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index c1137c6bb0..be4d50a623 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -84,6 +84,7 @@ and free_exp e = free_list free_exp [e1; e2] | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3] | OptE eo -> free_opt free_exp eo + | TheE e -> free_exp e | TupE es | ListE es -> free_list free_exp es | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> union (free_list free_exp [e1; e2]) (free_path p) diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index a705ee69b7..fb15188429 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -148,6 +148,7 @@ and string_of_exp e = | CallE (id, e) -> "$" ^ id.it ^ string_of_exp_args e | IterE (e1, iter) -> string_of_exp e1 ^ string_of_iterexp iter | OptE eo -> "?(" ^ string_of_exps "" (Option.to_list eo) ^ ")" + | TheE e -> "THE(" ^ string_of_exp e ^ ")" | 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 index 821f99ef05..dcd77e8e90 100644 --- 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 e -> as_iter_typ Opt "option" env Check (infer_exp env e) e.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 e -> + valid_exp env e (IterT (t, Opt) $ e.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 new file mode 100644 index 0000000000..4a0111ab9f --- /dev/null +++ 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 new file mode 100644 index 0000000000..f291c0173f --- /dev/null +++ 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 new file mode 100644 index 0000000000..542bbf8052 --- /dev/null +++ b/spectec/src/middlend/totalize.mli @@ -0,0 +1 @@ +val transform : Il.Ast.script -> Il.Ast.script From c781588886c4e8c683dafb36e11735351f9021b7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 8 Apr 2023 19:25:20 +0200 Subject: [PATCH 2/6] Update print.ml --- spectec/src/il/print.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index fb15188429..fbc9886c37 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -148,7 +148,7 @@ and string_of_exp e = | CallE (id, e) -> "$" ^ id.it ^ string_of_exp_args e | IterE (e1, iter) -> string_of_exp e1 ^ string_of_iterexp iter | OptE eo -> "?(" ^ string_of_exps "" (Option.to_list eo) ^ ")" - | TheE e -> "THE(" ^ string_of_exp e ^ ")" + | TheE e -> "!(" ^ string_of_exp e ^ ")" | ListE es -> "[" ^ string_of_exps " " es ^ "]" | CatE (e1, e2) -> string_of_exp e1 ^ " :: " ^ string_of_exp e2 | CaseE (atom, e1, t) -> From bd66146d1228d417f54c06a67868fe5ce6ec80da Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 8 Apr 2023 19:27:06 +0200 Subject: [PATCH 3/6] Update eq.ml --- spectec/src/il/eq.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml index 59411a5d33..8e10ac8877 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml @@ -12,11 +12,13 @@ let eq_opt eq_x xo1 xo2 = 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 = @@ -91,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 From 8e7040dce063fc5486fa8e57853437fd8e98cee4 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 8 Apr 2023 19:27:50 +0200 Subject: [PATCH 4/6] Update free.ml --- spectec/src/il/free.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml index be4d50a623..7d2128735e 100644 --- a/spectec/src/il/free.ml +++ b/spectec/src/il/free.ml @@ -77,14 +77,13 @@ 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) -> free_list free_exp [e1; e2] | SliceE (e1, e2, e3) -> free_list free_exp [e1; e2; e3] | OptE eo -> free_opt free_exp eo - | TheE e -> free_exp e | TupE es | ListE es -> free_list free_exp es | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> union (free_list free_exp [e1; e2]) (free_path p) From 0609ce6270413257b6d52bbbcfb7b25335724f9b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 8 Apr 2023 19:28:34 +0200 Subject: [PATCH 5/6] Update print.ml --- spectec/src/il/print.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml index fbc9886c37..a76d8ca95e 100644 --- a/spectec/src/il/print.ml +++ b/spectec/src/il/print.ml @@ -145,10 +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 e -> "!(" ^ string_of_exp e ^ ")" + | 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) -> From 0aa846628eb21bc5c915e5ad08993a914f52a9a8 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 8 Apr 2023 19:29:44 +0200 Subject: [PATCH 6/6] Update validation.ml --- spectec/src/il/validation.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/spectec/src/il/validation.ml b/spectec/src/il/validation.ml index dcd77e8e90..fcdd4c52c6 100644 --- a/spectec/src/il/validation.ml +++ b/spectec/src/il/validation.ml @@ -317,7 +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 e -> as_iter_typ Opt "option" env Check (infer_exp env e) e.at + | 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" @@ -413,8 +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 e -> - valid_exp env e (IterT (t, Opt) $ e.at) + | 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