Skip to content

Commit

Permalink
old walker removed
Browse files Browse the repository at this point in the history
  • Loading branch information
reduction-choi committed Sep 4, 2024
1 parent d09cbab commit 521eb00
Show file tree
Hide file tree
Showing 6 changed files with 233 additions and 305 deletions.
188 changes: 23 additions & 165 deletions spectec/src/al/walk.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,26 +93,26 @@ let base_unit_walker = { super=None; walk_algo; walk_instr; walk_expr; walk_path
type walker = {
super: walker option;
walk_algo: walker -> algorithm -> algorithm;
walk_instr: walker -> instr -> instr;
walk_instr: walker -> instr -> instr list;
walk_expr: walker -> expr -> expr;
walk_path: walker -> path -> path;
walk_iter: walker -> iter -> iter;
walk_arg: walker -> arg -> arg;
}

let walk_arg (walker: walker) (arg: arg) : arg =
let walk_arg' (walker: walker) (arg: arg) : arg =
let walk_expr = walker.walk_expr walker in
match arg.it with
| ExpA e -> { arg with it = ExpA (walk_expr e) }
| TypA _ -> arg

let walk_iter (walker: walker) (iter: 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_path' (walker: walker) (path: path) : path =
let walk_expr = walker.walk_expr walker in
let it =
match path.it with
Expand All @@ -122,9 +122,9 @@ let walk_path (walker: walker) (path: path) : path =
in
{ path with it }

let walk_expr (walker: walker) (expr: expr) : expr =
let walk_expr' (walker: walker) (expr: expr) : expr =
let walk_arg = walker.walk_arg walker in
let walk_iter = walker.walk_iter walker in
(* 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 =
Expand Down Expand Up @@ -153,7 +153,7 @@ let walk_expr (walker: walker) (expr: expr) : expr =
| LabelE (e1, e2) -> LabelE (walk_expr e1, walk_expr e2)
| ContE e' -> ContE (walk_expr e')
| ChooseE e' -> ChooseE (walk_expr e')
| IterE (e, ids, iter) -> IterE (walk_expr e, ids, walk_iter iter)
| IterE (e, ids, iter) -> IterE (walk_expr e, ids, (* walk_iter *) iter)
| IsCaseOfE (e, a) -> IsCaseOfE (walk_expr e, a)
| IsDefinedE e -> IsDefinedE (walk_expr e)
| HasTypeE (e, t) -> HasTypeE(walk_expr e, t)
Expand All @@ -164,20 +164,20 @@ let walk_expr (walker: walker) (expr: expr) : expr =
in
{ expr with it }

let walk_instr (walker: walker) (instr: instr) : instr =
let walk_instr' (walker: walker) (instr: instr) : instr list =
let walk_arg = walker.walk_arg walker in
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)
IfI (walk_expr e, List.concat_map walk_instr il1, List.concat_map walk_instr il2)
| OtherwiseI il -> OtherwiseI (List.concat_map walk_instr il)
| EitherI (il1, il2) ->
EitherI (List.map walk_instr il1, List.map walk_instr il2)
EitherI (List.concat_map walk_instr il1, List.concat_map walk_instr il2)
| EnterI (e1, e2, il) ->
EnterI (walk_expr e1, walk_expr e2, List.map walk_instr il)
EnterI (walk_expr e1, walk_expr e2, List.concat_map walk_instr il)
| AssertI e -> AssertI (walk_expr e)
| PushI e -> PushI (walk_expr e)
| PopI e -> PopI (walk_expr e)
Expand All @@ -196,167 +196,25 @@ let walk_instr (walker: walker) (instr: instr) : instr =
| FieldWiseAppendI (e1, e2) -> FieldWiseAppendI (walk_expr e1, walk_expr e2)
| YetI _ -> instr.it
in
{ instr with it }
[{ instr with it }]

let walk_algo (walker: walker) (algo: algorithm) : algorithm =
let walk_algo' (walker: walker) (algo: algorithm) : algorithm =
let walk_arg = walker.walk_arg walker in
let walk_instr = walker.walk_instr walker in
let it =
match algo.it with
| RuleA (name, anchor, args, instrs) ->
RuleA (name, anchor, List.map walk_arg args, List.map walk_instr instrs)
RuleA (name, anchor, List.map walk_arg args, List.concat_map walk_instr instrs)
| FuncA (name, args, instrs) ->
FuncA (name, List.map walk_arg args, List.map walk_instr instrs)
FuncA (name, List.map walk_arg args, List.concat_map walk_instr instrs)
in
{ algo with it }

let base_walker = { super=None; walk_algo; walk_instr; walk_expr; walk_path; walk_iter; walk_arg }


(* TODO: remove walker below *)

type config = {
pre_instr: instr -> instr list;
post_instr: instr -> instr list;
stop_cond_instr: instr -> bool;

pre_expr: expr -> expr;
post_expr: expr -> expr;
stop_cond_expr: expr -> bool;
let base_walker = { super=None;
walk_algo = walk_algo';
walk_instr = walk_instr';
walk_expr = walk_expr';
walk_path = walk_path';
walk_iter = walk_iter';
walk_arg = walk_arg'
}

let id x = x
let ids x = [ x ]
let fls _ = false
let default_config = {
pre_instr = ids;
post_instr = ids;
stop_cond_instr = fls;

pre_expr = id;
post_expr = id;
stop_cond_expr = fls;
}

let rec walk_expr f e =
let { pre_expr = pre; post_expr = post; stop_cond_expr = stop_cond; _ } = f in
let new_ = walk_expr f in

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

let e1 = pre e in
let e2 = if stop_cond e1 then e1 else super_walk e1 in
let e3 = post e2 in
e3

and walk_path f p =
let pre = id in
let post = id in

let p' =
( match (pre p).it with
| IdxP e -> IdxP (walk_expr f e)
| SliceP (e1, e2) -> SliceP (walk_expr f e1, walk_expr f e2)
| DotP a -> DotP a )
in
let p = { p with it = p' } in

post p

and walk_arg f a =
match a.it with
| ExpA e -> { a with it = ExpA (walk_expr f e) }
| TypA _ -> a

let rec walk_instr f (instr:instr) : instr list =
let { pre_instr = pre; post_instr = post; stop_cond_instr = stop_cond; _ } = f in
let new_ = List.concat_map (walk_instr f) in
let new_e = walk_expr f in
let new_a = walk_arg f in

let super_walk i =
let i' =
match i.it with
| IfI (e, il1, il2) -> IfI (new_e e, new_ il1, new_ il2)
| OtherwiseI il -> OtherwiseI (new_ il)
| EitherI (il1, il2) -> EitherI (new_ il1, new_ il2)
| AssertI e -> AssertI (new_e e)
| PushI e -> PushI (new_e e)
| PopI e -> PopI (new_e e)
| PopAllI e -> PopAllI (new_e e)
| LetI (e1, e2) -> LetI (new_e e1, new_e e2)
| TrapI -> TrapI
| ThrowI e -> ThrowI (new_e e)
| NopI -> NopI
| ReturnI e_opt -> ReturnI (Option.map new_e e_opt)
| EnterI (e1, e2, il) -> EnterI (new_e e1, new_e e2, new_ il)
| ExecuteI e -> ExecuteI (new_e e)
| ExecuteSeqI e -> ExecuteSeqI (new_e e)
| PerformI (id, al) -> PerformI (id, List.map new_a al)
| ExitI _ -> i.it
| ReplaceI (e1, p, e2) -> ReplaceI (new_e e1, walk_path f p, new_e e2)
| AppendI (e1, e2) -> AppendI (new_e e1, new_e e2)
| FieldWiseAppendI (e1, e2) -> FieldWiseAppendI (new_e e1, new_e e2)
| YetI _ -> i.it in
{ i with it = i' }
in

let il1 = pre instr in
let il2 = List.map (fun i -> if stop_cond i then i else super_walk i) il1 in
let il3 = List.concat_map post il2 in
il3

and walk_instrs f = walk_instr f |> List.concat_map

let walk' f algo' = match algo' with
| RuleA (a, anchor, params, body) -> RuleA (a, anchor, params, walk_instrs f body)
| FuncA (id, params, body) -> FuncA (id, params, walk_instrs f body)
let walk f algo = Source.map (walk' f) algo
21 changes: 1 addition & 20 deletions spectec/src/al/walk.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,30 +12,11 @@ type unit_walker = {
type walker = {
super: walker option;
walk_algo: walker -> algorithm -> algorithm;
walk_instr: walker -> instr -> instr;
walk_instr: walker -> instr -> instr list;
walk_expr: walker -> expr -> expr;
walk_path: walker -> path -> path;
walk_iter: walker -> iter -> iter;
walk_arg: walker -> arg -> arg;
}
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;
stop_cond_instr: instr -> bool;

pre_expr: expr -> expr;
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
val walk_instrs : config -> instr list -> instr list
val walk_expr : config -> expr -> expr
val walk_path : config -> path -> path
val walk_arg : config -> arg -> arg
22 changes: 14 additions & 8 deletions spectec/src/backend-interpreter/ds.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -341,14 +341,20 @@ let init algos =
(* Initialize info_map *)
let init_info algo =
let algo_name = name_of_algo algo in
let config = {
Walk.default_config with pre_instr =
(fun i ->
let info = Info.make_info algo_name i in
Info.add i.note info;
[i])
} in
Walk.walk config algo
let pre_instr = (fun i ->
let info = Info.make_info algo_name i in
Info.add i.note info;
[i])
in
let walk_instr walker instr =
let instr1 = pre_instr instr in
List.concat_map (Al.Walk.base_walker.walk_instr walker) instr1
in
let walker = { Walk.base_walker with
walk_instr = walk_instr;
}
in
walker.walk_algo walker algo
in
List.map init_info algos |> ignore;

Expand Down
11 changes: 9 additions & 2 deletions spectec/src/backend-prose/gen.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,9 +135,16 @@ let get_rel_kind def =
| _ -> OtherRel

let transpile_expr =
Al.Walk.walk_expr { Al.Walk.default_config with
post_expr = fun expr -> expr |> Il2al.Transpile.simplify_record_concat |> Il2al.Transpile.reduce_comp
let post_expr = fun expr -> expr |> Il2al.Transpile.simplify_record_concat |> Il2al.Transpile.reduce_comp in
let walk_expr walker expr =
let expr1 = Al.Walk.base_walker.walk_expr walker expr in
post_expr expr1
in
let walker = { Al.Walk.base_walker with
walk_expr = walk_expr;
}
in
walker.walk_expr walker

let exp_to_expr e = translate_exp e |> transpile_expr
let exp_to_argexpr es = translate_argexp es |> List.map transpile_expr
Expand Down
Loading

0 comments on commit 521eb00

Please sign in to comment.