Skip to content

Commit

Permalink
Add InvCallE
Browse files Browse the repository at this point in the history
  • Loading branch information
Wonho Shin authored and Wonho Shin committed Jul 16, 2024
1 parent 3bc3fa8 commit 3dc017c
Show file tree
Hide file tree
Showing 7 changed files with 47 additions and 0 deletions.
1 change: 1 addition & 0 deletions spectec/src/al/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,7 @@ and expr' =
| TupE of expr list (* `(` (expr `,`)* `)` *)
| CaseE of atom * expr list (* atom `(` expr* `)` -- MixE/CaseE *)
| CallE of id * expr list (* id `(` expr* `)` *)
| InvCallE of id * int list * expr list (* id`_`int*`^-1(` expr* `)` *)
| IterE of expr * id list * iter (* expr (`{` id* `}`)* *)
| OptE of expr option (* expr? *)
| ListE of expr list (* `[` expr* `]` *)
Expand Down
4 changes: 4 additions & 0 deletions spectec/src/al/eq.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,10 @@ let rec eq_expr e1 e2 =
| CallE (i1, el1), CallE (i2, el2) ->
i1 = i2 &&
eq_exprs el1 el2
| InvCallE (i1, nl1, el1), InvCallE (i2, nl2, el2) ->
i1 = i2 &&
List.for_all2 (=) nl1 nl2 &&
eq_exprs el1 el2
| IterE (e1, il1, it1), IterE (e2, il2, it2) ->
eq_expr e1 e2 &&
il1 = il2 &&
Expand Down
1 change: 1 addition & 0 deletions spectec/src/al/free.ml
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ let rec free_expr expr =
| LabelE (e1, e2) -> free_expr e1 @ free_expr e2
| FrameE (e_opt, e) -> free_opt free_expr e_opt @ free_expr e
| CallE (_, el)
| InvCallE (_, _, el)
| TupE el
| ListE el
| CaseE (_, el) -> free_list free_expr el
Expand Down
13 changes: 13 additions & 0 deletions spectec/src/al/print.ml
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,16 @@ and string_of_expr expr =
sprintf "(%s %s %s)" (string_of_expr e1) (string_of_binop op) (string_of_expr e2)
| TupE el -> "(" ^ string_of_exprs ", " el ^ ")"
| CallE (id, el) -> sprintf "$%s(%s)" id (string_of_exprs ", " el)
| InvCallE (id, nl, el) ->
let id' =
if List.length nl = 0 then id
else
nl
|> List.map string_of_int
|> List.fold_left (^) ""
|> sprintf "%s_%s" id
in
sprintf "$%s^-1(%s)" id' (string_of_exprs ", " el)
| CatE (e1, e2) ->
sprintf "%s ++ %s" (string_of_expr e1) (string_of_expr e2)
| MemE (e1, e2) ->
Expand Down Expand Up @@ -422,6 +432,9 @@ and structured_string_of_expr expr =
^ ")"
| TupE el -> "TupE (" ^ structured_string_of_exprs el ^ ")"
| CallE (id, el) -> "CallE (" ^ id ^ ", [ " ^ structured_string_of_exprs el ^ " ])"
| InvCallE (id, nl, el) ->
sprintf "InvCallE (%s, [%s], [%s])"
id (string_of_list string_of_int "" nl) (structured_string_of_exprs el)
| CatE (e1, e2) ->
"CatE ("
^ structured_string_of_expr e1
Expand Down
1 change: 1 addition & 0 deletions spectec/src/al/walk.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ let rec walk_expr f e =
| UnE (op, e') -> UnE (op, new_ e')
| BinE (op, e1, e2) -> BinE (op, new_ e1, new_ e2)
| CallE (id, el) -> CallE (id, List.map new_ el)
| InvCallE (id, nl, el) -> InvCallE (id, nl, List.map new_ el)
(* TODO: Implement walker for iter *)
| ListE el -> ListE (List.map new_ el)
| CatE (e1, e2) -> CatE (new_ e1, new_ e2)
Expand Down
7 changes: 7 additions & 0 deletions spectec/src/backend-interpreter/interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,13 @@ and eval_expr env expr =
| Some v -> v
| _ -> raise (Exception.MissingReturnValue fname)
)
| InvCallE (fname, _, el) ->
(* TODO: refactor numerics function name *)
let args = List.map (eval_expr env) el in
(match call_func ("inverse_of_"^fname) args with
| Some v -> v
| _ -> raise (Exception.MissingReturnValue fname)
)
(* Data Structure *)
| ListE el -> List.map (eval_expr env) el |> listV_of_list
| CatE (e1, e2) ->
Expand Down
20 changes: 20 additions & 0 deletions spectec/src/backend-prose/render.ml
Original file line number Diff line number Diff line change
Expand Up @@ -105,6 +105,26 @@ and al_to_el_expr expr =
elel
in
Some (El.Ast.CallE (elid, elel))
| Al.Ast.InvCallE (id, nl, el) ->
let ($~) at it = it $ at in
let elid =
if List.length nl = 0 then
(id^"^-1") $ no_region
else
nl
|> List.map string_of_int
|> List.fold_left (^) ""
|> sprintf "%s_%s^-1" id
|> ($~) no_region
in
let* elel = al_to_el_exprs el in
let elel = List.map
(fun ele ->
let elarg = El.Ast.ExpA ele in
(ref elarg) $ no_region)
elel
in
Some (El.Ast.CallE (elid, elel))
| Al.Ast.CatE (e1, e2) ->
let* ele1 = al_to_el_expr e1 in
let* ele2 = al_to_el_expr e2 in
Expand Down

0 comments on commit 3dc017c

Please sign in to comment.