Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

General Il traversal #22

Draft
wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

General Il traversal #22

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
808cca4
Add general fold over expressions
matijapretnar May 15, 2023
e4c9970
Fold over iterexps and paths
matijapretnar May 16, 2023
1143352
Parametrize over acc type and pass in exp type and location
matijapretnar May 16, 2023
f5f4717
Expand traverse to definitions
matijapretnar May 16, 2023
4e74276
No need to provide values for all subcases
matijapretnar May 16, 2023
cc132ef
Adapt some of Joachim's shortcuts
matijapretnar May 16, 2023
9a60391
Merge everything in a single module
matijapretnar May 16, 2023
41efe1c
Use a record instead of a module
matijapretnar May 16, 2023
cb939e0
Add an interface
matijapretnar May 16, 2023
d7bf5ab
Move to middleend folder
matijapretnar May 16, 2023
a831e39
Add shortcut functions
matijapretnar May 16, 2023
8fa0efa
Add a case for rules
matijapretnar May 16, 2023
f58728d
Make Joachim happy/sad
matijapretnar May 16, 2023
7565e19
Remove unused hooks
matijapretnar May 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion spectec/src/middlend/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(library
(name middlend)
(libraries util il)
(modules sub totalize unthe sideconditions)
(modules traverse sub totalize unthe sideconditions)
)
88 changes: 5 additions & 83 deletions spectec/src/middlend/sub.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)

Expand Down Expand Up @@ -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''
Expand Down
102 changes: 13 additions & 89 deletions spectec/src/middlend/totalize.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand All @@ -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
Loading