diff --git a/spectec/src/middlend/dune b/spectec/src/middlend/dune index 6564b4b657..3c262ad049 100644 --- a/spectec/src/middlend/dune +++ b/spectec/src/middlend/dune @@ -1,5 +1,5 @@ (library (name middlend) (libraries util il) - (modules sub totalize unthe sideconditions) + (modules traverse sub totalize unthe sideconditions) ) diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml index ceda4ad2e2..e76cf3ab30 100644 --- a/spectec/src/middlend/sub.ml +++ b/spectec/src/middlend/sub.ml @@ -79,92 +79,14 @@ let var_of_typ typ = match typ.it with (* Step 1 and 4: Collect SubE occurrences, and replace with function *) (* The main transformation case *) -let rec t_exp env exp = - let exp' = t_exp2 env exp in - match exp'.it with +let transform_exp env exp = + match exp.it with | SubE (e, sub_ty, sup_ty) -> let sub = var_of_typ sub_ty in let sup = var_of_typ sup_ty in env.pairs <- S.add (sub, sup) env.pairs; - { exp' with it = CallE (injection_name sub sup, e)} - | _ -> exp' - -(* Traversal boilerplate *) - -and t_exp2 env x = { x with it = t_exp' env x.it } - -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 (e, a) -> DotE (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) -> CaseE (a, t_exp env e) - | 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) - | SliceP (path, e1, e2) -> SliceP (t_path env path, t_exp env e1, t_exp env e2) - | 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 t_clauses env = List.map (t_clause env) - -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) -> - DecD (id, typ1, typ2, t_clauses env clauses) - | RelD (id, mixop, typ, rules) -> - RelD (id, mixop, typ, List.map (t_rule env) rules) - | def -> def - -and t_def env (def : def) = { def with it = t_def' env def.it } + { exp with it = CallE (injection_name sub sup, e)} + | _ -> exp (* Step 2 and 3: Traverse definitions, collect type information, insert as soon as possible *) @@ -218,7 +140,7 @@ let insert_injections env (def : def) : def list = let transform (defs : script) = let env = new_env () in - let defs' = List.map (t_def env) defs in + let defs' = Traverse.reader ~exp:transform_exp env defs in let defs'' = List.concat_map (insert_injections env) defs' in S.iter (fun (sub, sup) -> error sub.at ("left-over subtype coercion " ^ sub.it ^ " <: " ^ sup.it)) env.pairs; defs'' diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml index 7f3c9ed9e7..aca7b94f89 100644 --- a/spectec/src/middlend/totalize.ml +++ b/spectec/src/middlend/totalize.ml @@ -42,101 +42,26 @@ let register_partial (env : env) (id :id) = (* Transformation *) (* The main transformation case *) -let rec t_exp env exp = - let exp' = t_exp2 env exp in - match exp'.it with +let totalize_exp env e = + match e.it with | CallE (f, _) when is_partial env f -> - {exp' with it = TheE {exp' with note = IterT (exp'.note, Opt) $ exp'.at}} - | _ -> 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 (e, a) -> DotE (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) -> CaseE (a, t_exp env e) - | 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) - | SliceP (path, e1, e2) -> SliceP (t_path env path, t_exp env e1, t_exp env e2) - | 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 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) -> - let clauses' = List.map (t_clause env) clauses in - if is_partial env id - then + {e with it = TheE {e with note = IterT (e.note, Opt) $ e.at}} + | _ -> e + +let totalize_def env d = + match d.it with + | DecD (id, typ1, typ2, clauses) when is_partial env id -> let typ2' = IterT (typ2, Opt) $ no_region in - let clauses'' = List.map (fun clause -> match clause.it with + 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 % typ2', prems) } - ) clauses' in + ) clauses in let x = "x" $ no_region in let catch_all = DefD ([(x, typ1, [])], VarE x $$ no_region % typ1, OptE None $$ no_region % typ2', []) $ no_region in - DecD (id, typ1, typ2', clauses'' @ [ catch_all ]) - else - DecD (id, typ1, typ2, clauses') - | RelD (id, mixop, typ, rules) -> - RelD (id, mixop, typ, List.map (t_rule env) rules) - | (SynD _ | HintD _) as def -> def - -and t_def env x = { x with it = t_def' env x.it } - + {d with it = DecD (id, typ1, typ2', clauses' @ [ catch_all ])} + | _ -> d let is_partial_hint hint = hint.hintid.it = "partial" @@ -149,5 +74,4 @@ let register_hints env def = let transform (defs : script) = let env = new_env () in List.iter (register_hints env) defs; - List.map (t_def env) defs - + Traverse.reader ~exp:totalize_exp ~def:totalize_def env defs diff --git a/spectec/src/middlend/traverse.ml b/spectec/src/middlend/traverse.ml new file mode 100644 index 0000000000..d424a5e282 --- /dev/null +++ b/spectec/src/middlend/traverse.ml @@ -0,0 +1,320 @@ +open Util +open Il.Ast +open Source + +let traverse_phrase traverse p trv acc = + let it, acc' = traverse p.it trv acc in + ({ p with it }, acc') + +let traverse2 tx1 tx2 trv acc = + let x1', acc' = tx1 trv acc in + let x2', acc'' = tx2 trv acc' in + ((x1', x2'), acc'') + +let traverse3 tx1 tx2 tx3 trv acc = + let x1', acc' = tx1 trv acc in + let x2', acc'' = tx2 trv acc' in + let x3', acc''' = tx3 trv acc'' in + ((x1', x2', x3'), acc''') + +let traverse4 tx1 tx2 tx3 tx4 trv acc = + let x1', acc' = tx1 trv acc in + let x2', acc'' = tx2 trv acc' in + let x3', acc''' = tx3 trv acc'' in + let x4', acc'''' = tx4 trv acc''' in + ((x1', x2', x3', x4'), acc'''') + +let rec traverse_list f ds trv acc = + match ds with + | [] -> ([], acc) + | d :: ds -> + let d', acc' = f d trv acc in + let ds', acc'' = traverse_list f ds trv acc' in + (d' :: ds', acc'') + +let traverse_option f eo trv acc = + match eo with + | None -> (None, acc) + | Some e -> + let e', acc' = f e trv acc in + (Some e', acc') + +let rec traverse_fieldlist f es trv acc = + match es with + | [] -> ([], acc) + | (x, e) :: es -> + let e', acc' = f e trv acc in + let es', acc'' = traverse_fieldlist f es trv acc' in + ((x, e') :: es', acc'') + +type ('acc, 't) fold_map = 't -> 'acc -> 't * 'acc + +type 'acc t = { + exp : ('acc, exp) fold_map; + rule : ('acc, rule) fold_map; + def : ('acc, def) fold_map; +} + +let rec traverse_exp e trv acc = + let e', acc' = traverse_phrase traverse_exp' e trv acc in + trv.exp e' acc' + +and traverse_exp' exp' trv acc = + match exp' with + | VarE x -> (VarE x, acc) + | BoolE b -> (BoolE b, acc) + | NatE n -> (NatE n, acc) + | TextE tx -> (TextE tx, acc) + | UnE (op, e) -> + let e', acc' = traverse_exp e trv acc in + (UnE (op, e'), acc') + | BinE (op, e1, e2) -> + let (e1', e2'), acc' = + traverse2 (traverse_exp e1) (traverse_exp e2) trv acc + in + (BinE (op, e1', e2'), acc') + | CmpE (op, e1, e2) -> + let (e1', e2'), acc' = + traverse2 (traverse_exp e1) (traverse_exp e2) trv acc + in + (CmpE (op, e1', e2'), acc') + | IdxE (e1, e2) -> + let (e1', e2'), acc' = + traverse2 (traverse_exp e1) (traverse_exp e2) trv acc + in + (IdxE (e1', e2'), acc') + | SliceE (e1, e2, e3) -> + let (e1', e2', e3'), acc' = + traverse3 (traverse_exp e1) (traverse_exp e2) (traverse_exp e3) trv acc + in + (SliceE (e1', e2', e3'), acc') + | UpdE (e1, p, e2) -> + let (e1', p', e2'), acc' = + traverse3 (traverse_exp e1) (traverse_path p) (traverse_exp e2) trv acc + in + (UpdE (e1', p', e2'), acc') + | ExtE (e1, p, e2) -> + let (e1', p', e2'), acc' = + traverse3 (traverse_exp e1) (traverse_path p) (traverse_exp e2) trv acc + in + (ExtE (e1', p', e2'), acc') + | StrE es -> + let es', acc' = traverse_fieldlist traverse_exp es trv acc in + (StrE es', acc') + | DotE (e, x) -> + let e', acc' = traverse_exp e trv acc in + (DotE (e', x), acc') + | CompE (e1, e2) -> + let (e1', e2'), acc' = + traverse2 (traverse_exp e1) (traverse_exp e2) trv acc + in + (CompE (e1', e2'), acc') + | LenE e -> + let e', acc' = traverse_exp e trv acc in + (LenE e', acc') + | TupE es -> + let es', acc' = traverse_list traverse_exp es trv acc in + (TupE es', acc') + | MixE (op, e) -> + let e', acc' = traverse_exp e trv acc in + (MixE (op, e'), acc') + | CallE (x, e) -> + let e', acc' = traverse_exp e trv acc in + (CallE (x, e'), acc') + | IterE (e, ie) -> + let (e', ie'), acc' = + traverse2 (traverse_exp e) (traverse_iterexp ie) trv acc + in + (IterE (e', ie'), acc') + | OptE eo -> + let eo', acc' = traverse_option traverse_exp eo trv acc in + (OptE eo', acc') + | TheE e -> + let e', acc' = traverse_exp e trv acc in + (TheE e', acc') + | ListE es -> + let es', acc' = traverse_list traverse_exp es trv acc in + (ListE es', acc') + | CatE (e1, e2) -> + let (e1', e2'), acc' = + traverse2 (traverse_exp e1) (traverse_exp e2) trv acc + in + (CatE (e1', e2'), acc') + | CaseE (x, e) -> + let e', acc' = traverse_exp e trv acc in + (CaseE (x, e'), acc') + | SubE (e, t1, t2) -> + let e', acc' = traverse_exp e trv acc in + (SubE (e', t1, t2), acc') + +and traverse_iterexp (ie, vs) trv acc = + let ie', acc' = traverse_iter ie trv acc in + ((ie', vs), acc') + +and traverse_iter ie trv acc = + match ie with + | Opt -> (Opt, acc) + | List -> (List, acc) + | List1 -> (List1, acc) + | ListN e -> + let e', acc' = traverse_exp e trv acc in + (ListN e', acc') + +and traverse_path p trv acc = + let p', acc' = traverse_path' p.it trv acc in + ({ p with it = p' }, acc') + +and traverse_path' p trv acc = + match p with + | RootP -> (RootP, acc) + | IdxP (p, e) -> + let (p', e'), acc' = + traverse2 (traverse_path p) (traverse_exp e) trv acc + in + (IdxP (p', e'), acc') + | SliceP (p, e1, e2) -> + let (p', e1', e2'), acc' = + traverse3 (traverse_path p) (traverse_exp e1) (traverse_exp e2) trv acc + in + (SliceP (p', e1', e2'), acc') + | DotP (p, a) -> + let p', acc' = traverse_path p trv acc in + (DotP (p', a), acc') + +let traverse_bind (x, t, iters) trv acc = + let iters', acc' = traverse_list traverse_iter iters trv acc in + ((x, t, iters'), acc') + +let traverse_binds bs trv acc = + let bs', acc' = traverse_list traverse_bind bs trv acc in + (bs', acc') + +let rec traverse_def d trv acc = + let d', acc' = traverse_phrase traverse_def' d trv acc in + trv.def d' acc' + +and traverse_def' def' trv acc = + match def' with + | SynD (x, t) -> (SynD (x, t), acc) + | RelD (x, op, t, rs) -> + let rs', acc' = traverse_list traverse_rule rs trv acc in + (RelD (x, op, t, rs'), acc') + | DecD (x, t1, t2, cs) -> + let cs', acc' = traverse_list traverse_clause cs trv acc in + (DecD (x, t1, t2, cs'), acc') + | RecD ds -> + let ds', acc' = traverse_list traverse_def ds trv acc in + (RecD ds', acc') + | HintD hd -> (HintD hd, acc) + +and traverse_rule r trv acc = + let r', acc' = traverse_phrase traverse_rule' r trv acc in + trv.rule r' acc' + +and traverse_rule' r trv acc = + match r with + | RuleD (x, bs, op, e, ps) -> + let (bs', e', ps'), acc' = + traverse3 (traverse_binds bs) (traverse_exp e) + (traverse_list traverse_premise ps) + trv acc + in + (RuleD (x, bs', op, e', ps'), acc') + +and traverse_clause c trv acc = traverse_phrase traverse_clause' c trv acc + +and traverse_clause' c trv acc = + match c with + | DefD (bs, e1, e2, ps) -> + let (bs', e1', e2', ps'), acc' = + traverse4 (traverse_binds bs) (traverse_exp e1) (traverse_exp e2) + (traverse_list traverse_premise ps) + trv acc + in + (DefD (bs', e1', e2', ps'), acc') + +and traverse_premise p trv acc = traverse_phrase traverse_premise' p trv acc + +and traverse_premise' p trv acc = + match p with + | RulePr (x, op, e) -> + let e', acc' = traverse_exp e trv acc in + (RulePr (x, op, e'), acc') + | IfPr e -> + let e', acc' = traverse_exp e trv acc in + (IfPr e', acc') + | ElsePr -> (ElsePr, acc) + | IterPr (p, ie) -> + let (p', ie'), acc' = + traverse2 (traverse_premise p) (traverse_iterexp ie) trv acc + in + (IterPr (p', ie'), acc') + +let traverse_script s trv acc = + let s', acc' = traverse_list traverse_def s trv acc in + (s', acc') + +let id_fold x acc = (x, acc) + +let fold_map ?exp ?rule ?def (s : script) acc = + let arg_to_fold_map f = Option.value f ~default:id_fold in + let trv = + { + exp = arg_to_fold_map exp; + rule = arg_to_fold_map rule; + def = arg_to_fold_map def; + } + in + let s', acc' = traverse_script s trv acc in + (s', acc') + +type 't map = 't -> 't + +let map ?exp ?rule ?def (s : script) = + let arg_to_map = function + | None -> fun x () -> (x, ()) + | Some f -> fun x () -> (f x, ()) + in + let trv = + { + exp = arg_to_map exp; + rule = arg_to_map rule; + def = arg_to_map def; + } + in + let s', () = traverse_script s trv () in + s' + +type ('acc, 't) fold = 't -> 'acc -> 'acc + +let fold ?exp ?rule ?def (s : script) acc = + let arg_to_fold = function + | None -> fun x acc -> (x, acc) + | Some f -> fun x acc -> (x, f x acc) + in + let trv = + { + exp = arg_to_fold exp; + rule = arg_to_fold rule; + def = arg_to_fold def; + } + in + let _, acc' = traverse_script s trv acc in + acc' + +type ('env, 't) reader = 'env -> 't -> 't + +let reader ?exp ?rule ?def env (s : script) = + let arg_to_reader = function + | None -> fun x env -> (x, env) + | Some f -> fun x env -> (f env x, env) + in + let trv = + { + exp = arg_to_reader exp; + rule = arg_to_reader rule; + def = arg_to_reader def; + } + in + let s', _ = traverse_script s trv env in + s' diff --git a/spectec/src/middlend/traverse.mli b/spectec/src/middlend/traverse.mli new file mode 100644 index 0000000000..1dcc891dc6 --- /dev/null +++ b/spectec/src/middlend/traverse.mli @@ -0,0 +1,31 @@ +type ('acc, 't) fold_map = 't -> 'acc -> 't * 'acc + +val fold_map : + ?exp:('acc, Il.Ast.exp) fold_map -> + ?rule:('acc, Il.Ast.rule) fold_map -> + ?def:('acc, Il.Ast.def) fold_map -> + ('acc, Il.Ast.script) fold_map + +type 't map = 't -> 't + +val map : + ?exp:Il.Ast.exp map -> + ?rule:Il.Ast.rule map -> + ?def:Il.Ast.def map -> + Il.Ast.script map + +type ('acc, 't) fold = 't -> 'acc -> 'acc + +val fold : + ?exp:('acc, Il.Ast.exp) fold -> + ?rule:('acc, Il.Ast.rule) fold -> + ?def:('acc, Il.Ast.def) fold -> + ('acc, Il.Ast.script) fold + +type ('env, 't) reader = 'env -> 't -> 't + +val reader : + ?exp:('env, Il.Ast.exp) reader -> + ?rule:('env, Il.Ast.rule) reader -> + ?def:('env, Il.Ast.def) reader -> + ('env, Il.Ast.script) reader