Skip to content

Commit

Permalink
Add more general walker
Browse files Browse the repository at this point in the history
  • Loading branch information
@ShinWonho
ShinWonho committed Jul 22, 2024
1 parent 3ff8100 commit 5300391
Show file tree
Hide file tree
Showing 2 changed files with 211 additions and 1 deletion.
192 changes: 192 additions & 0 deletions spectec/src/al/walk.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,198 @@ open Ast
open Util
open Source


(* Unit walker *)

type unit_walker = {
walk_algo: unit_walker -> algorithm -> unit;
walk_instr: unit_walker -> instr -> unit;
walk_expr: unit_walker -> expr -> unit;
walk_path: unit_walker -> path -> unit;
walk_iter: unit_walker -> iter -> unit;
}

let rec walk_iter (walker: unit_walker) (iter: iter) : unit =
match iter with
| Opt | List | List1 -> ()
| ListN (e, _) -> walker.walk_expr walker e

and walk_path (walker: unit_walker) (path: path) : unit =
match path.it with
| IdxP e -> walker.walk_expr walker e
| SliceP (e1, e2) -> walker.walk_expr walker e1; walker.walk_expr walker e2
| DotP _ -> ()

and walk_expr (walker: unit_walker) (expr: expr) : unit =
match expr.it with
| VarE _ | SubE _ | NumE _ | BoolE _ | GetCurStateE | GetCurLabelE
| GetCurContextE | GetCurFrameE | YetE _ | TopLabelE | TopFrameE
| TopValueE None -> ()

| UnE (_, e) | LenE e | ArityE e | ContE e | ContextKindE (_, e)
| IsDefinedE e | IsCaseOfE (e, _) | HasTypeE (e, _) | IsValidE e
| TopValueE (Some e) | TopValuesE e -> walker.walk_expr walker e

| BinE (_, e1, e2) | CatE (e1, e2) | MemE (e1, e2)
| InfixE (e1, _, e2) | LabelE (e1, e2) | MatchE (e1, e2) ->
walker.walk_expr walker e1; walker.walk_expr walker e2
| FrameE (e_opt, e) ->
Option.iter (walker.walk_expr walker) e_opt; walker.walk_expr walker e
| CallE (_, el) | InvCallE (_, _, el) | TupE el | ListE el | CaseE (_, el) ->
List.iter (walker.walk_expr walker) el
| StrE r -> List.iter (fun (_, e) -> walker.walk_expr walker !e) r
| AccE (e, p) -> walker.walk_expr walker e; walk_path walker p
| ExtE (e1, ps, e2, _) | UpdE (e1, ps, e2) ->
walker.walk_expr walker e1; List.iter (walk_path walker) ps;
walker.walk_expr walker e2
| OptE e_opt -> Option.iter (walker.walk_expr walker) e_opt
| IterE (e, _, i) -> walker.walk_expr walker e; walk_iter walker i

let rec walk_instr (walker: unit_walker) (instr: instr) : unit =
match instr.it with
| IfI (e, il1, il2) ->
walker.walk_expr walker e;
List.iter (walk_instr walker) il1; List.iter (walk_instr walker) il2
| OtherwiseI il -> List.iter (walker.walk_instr walker) il
| EitherI (il1, il2) ->
List.iter (walker.walk_instr walker) il1; List.iter (walk_instr walker) il2
| EnterI (e1, e2, il) ->
walker.walk_expr walker e1; walker.walk_expr walker e2;
List.iter (walk_instr walker) il
| TrapI | NopI | ReturnI None | ExitI _ | YetI _ -> ()
| AssertI e | PushI e | PopI e | PopAllI e
| ReturnI (Some e)| ExecuteI e | ExecuteSeqI e -> walker.walk_expr walker e
| LetI (e1, e2) | AppendI (e1, e2) ->
walker.walk_expr walker e1; walker.walk_expr walker e2
| PerformI (_, el) -> List.iter (walker.walk_expr walker) el
| ReplaceI (e1, p, e2) ->
walker.walk_expr walker e1; walk_path walker p; walker.walk_expr walker e2

let walk_algo (walker: unit_walker) (algo: algorithm) : unit =
match algo.it with
| RuleA (_, exprs, instrs) ->
List.iter (walker.walk_expr walker) exprs; List.iter (walk_instr walker) instrs
| FuncA (_, exprs, instrs) ->
List.iter (walker.walk_expr walker) exprs; List.iter (walk_instr walker) instrs

let base_unit_walker = { walk_algo; walk_instr; walk_expr; walk_path; walk_iter }


(* Transform walker *)

type walker = {
walk_algo: walker -> algorithm -> algorithm;
walk_instr: walker -> instr -> instr;
walk_expr: walker -> expr -> expr;
walk_path: walker -> path -> path;
walk_iter: walker -> iter -> iter;
}

let walk_iter (walker: walker) (iter: iter) : iter =
let walk_expr = walker.walk_expr walker in
match iter with
| Opt | List | List1 -> iter
| ListN (e, id_opt) -> ListN (walk_expr e, id_opt)

let walk_path (walker: walker) (path: path) : path =
let walk_expr = walker.walk_expr walker in
let it =
match path.it with
| IdxP e -> IdxP (walk_expr e)
| SliceP (e1, e2) -> SliceP (walk_expr e1, walk_expr e2)
| DotP a -> DotP a
in
{ path with it }

let walk_expr (walker: walker) (expr: expr) : expr =
let walk_iter = walker.walk_iter walker in
let walk_path = walker.walk_path walker in
let walk_expr = walker.walk_expr walker in
let it =
match expr.it with
| NumE _ | BoolE _ | VarE _ | SubE _ | GetCurStateE | GetCurFrameE
| GetCurLabelE | GetCurContextE | TopLabelE | TopFrameE | YetE _ -> expr.it
| UnE (op, e) -> UnE (op, walk_expr e)
| BinE (op, e1, e2) -> BinE (op, walk_expr e1, walk_expr e2)
| CallE (id, el) -> CallE (id, List.map walk_expr el)
| InvCallE (id, nl, el) -> InvCallE (id, nl, List.map walk_expr el)
| ListE el -> ListE (List.map walk_expr el)
| CatE (e1, e2) -> CatE (walk_expr e1, walk_expr e2)
| MemE (e1, e2) -> MemE (walk_expr e1, walk_expr e2)
| LenE e -> LenE (walk_expr e)
| StrE r -> StrE (Record.map (fun x -> x) walk_expr r)
| AccE (e, p) -> AccE (walk_expr e, walk_path p)
| ExtE (e1, ps, e2, dir) ->
ExtE (walk_expr e1, List.map walk_path ps, walk_expr e2, dir)
| UpdE (e1, ps, e2) -> UpdE (walk_expr e1, List.map walk_path ps, walk_expr e2)
| CaseE (a, el) -> CaseE (a, List.map walk_expr el)
| OptE e -> OptE (Option.map walk_expr e)
| TupE el -> TupE (List.map walk_expr el)
| InfixE (e1, a, e2) -> InfixE (walk_expr e1, a, walk_expr e2)
| ArityE e -> ArityE (walk_expr e)
| FrameE (e1_opt, e2) -> FrameE (Option.map walk_expr e1_opt, walk_expr e2)
| LabelE (e1, e2) -> LabelE (walk_expr e1, walk_expr e2)
| ContE e' -> ContE (walk_expr e')
| IterE (e, ids, iter) -> IterE (walk_expr e, ids, walk_iter iter)
| ContextKindE (a, e) -> ContextKindE (a, walk_expr e)
| IsCaseOfE (e, a) -> IsCaseOfE (walk_expr e, a)
| IsDefinedE e -> IsDefinedE (walk_expr e)
| HasTypeE (e, t) -> HasTypeE(walk_expr e, t)
| IsValidE e -> IsValidE (walk_expr e)
| TopValueE e_opt -> TopValueE (Option.map walk_expr e_opt)
| TopValuesE e -> TopValuesE (walk_expr e)
| MatchE (e1, e2) -> MatchE (walk_expr e1, walk_expr e2)
in
{ expr with it }

let walk_instr (walker: walker) (instr: instr) : instr =
let walk_path = walker.walk_path walker in
let walk_expr = walker.walk_expr walker in
let walk_instr = walker.walk_instr walker in
let it =
match instr.it with
| IfI (e, il1, il2) ->
IfI (walk_expr e, List.map walk_instr il1, List.map walk_instr il2)
| OtherwiseI il -> OtherwiseI (List.map walk_instr il)
| EitherI (il1, il2) ->
EitherI (List.map walk_instr il1, List.map walk_instr il2)
| EnterI (e1, e2, il) ->
EnterI (walk_expr e1, walk_expr e2, List.map walk_instr il)
| AssertI e -> AssertI (walk_expr e)
| PushI e -> PushI (walk_expr e)
| PopI e -> PopI (walk_expr e)
| PopAllI e -> PopAllI (walk_expr e)
| LetI (e1, e2) -> LetI (walk_expr e1, walk_expr e2)
| TrapI -> TrapI
| NopI -> NopI
| ReturnI e_opt -> ReturnI (Option.map walk_expr e_opt)
| ExecuteI e -> ExecuteI (walk_expr e)
| ExecuteSeqI e -> ExecuteSeqI (walk_expr e)
| PerformI (id, el) -> PerformI (id, List.map walk_expr el)
| ExitI _ -> instr.it
| ReplaceI (e1, p, e2) -> ReplaceI (walk_expr e1, walk_path p, walk_expr e2)
| AppendI (e1, e2) -> AppendI (walk_expr e1, walk_expr e2)
| YetI _ -> instr.it
in
{ instr with it }

let walk_algo (walker: walker) (algo: algorithm) : algorithm =
let walk_expr = walker.walk_expr walker in
let walk_instr = walker.walk_instr walker in
let it =
match algo.it with
| RuleA (name, exprs, instrs) ->
RuleA (name, List.map walk_expr exprs, List.map walk_instr instrs)
| FuncA (name, exprs, instrs) ->
FuncA (name, List.map walk_expr exprs, List.map walk_instr instrs)
in
{ algo with it }

let base_walker = { walk_algo; walk_instr; walk_expr; walk_path; walk_iter }


(* TODO: remove walker below *)

type config = {
pre_instr: instr -> instr list;
post_instr: instr -> instr list;
Expand Down
20 changes: 19 additions & 1 deletion spectec/src/al/walk.mli
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,24 @@
open Ast

type unit_walker = {
walk_algo: unit_walker -> algorithm -> unit;
walk_instr: unit_walker -> instr -> unit;
walk_expr: unit_walker -> expr -> unit;
walk_path: unit_walker -> path -> unit;
walk_iter: unit_walker -> iter -> unit;
}
type walker = {
walk_algo: walker -> algorithm -> algorithm;
walk_instr: walker -> instr -> instr;
walk_expr: walker -> expr -> expr;
walk_path: walker -> path -> path;
walk_iter: walker -> iter -> iter;
}
val base_unit_walker : unit_walker
val base_walker : walker

(* TODO: remove walker below *)

type config = {
pre_instr: instr -> instr list;
post_instr: instr -> instr list;
Expand All @@ -9,7 +28,6 @@ type config = {
post_expr: expr -> expr;
stop_cond_expr: expr -> bool;
}

val default_config : config
val walk : config -> algorithm -> algorithm
val walk_instr : config -> instr -> instr list
Expand Down

0 comments on commit 5300391

Please sign in to comment.