Skip to content

Commit

Permalink
Test expectations
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Oct 27, 2023
1 parent 3d7f74d commit 08e26ac
Show file tree
Hide file tree
Showing 5 changed files with 6,635 additions and 4,013 deletions.
15 changes: 9 additions & 6 deletions spectec/src/middlend/sub.ml
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,9 @@ let register_alias (env : env) (id : id) (id2 : id) =
let injection_name (sub : id) (sup : id) = sup.it ^ "_" ^ sub.it $ no_region

let var_of_typ typ = match typ.it with
| VarT id -> id
| _ -> error typ.at ("Non-variable type expression not supported:\n" ^ Il.Print.string_of_typ typ)
| VarT id -> Some id
| NumT _ -> None
| _ -> error typ.at ("Non-variable or number type expression not supported:\n" ^ Il.Print.string_of_typ typ)

(* Step 1 and 4: Collect SubE occurrences, and replace with function *)

Expand All @@ -83,10 +84,12 @@ let rec t_exp env exp =
let exp' = t_exp2 env exp in
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)}
begin match var_of_typ sub_ty, var_of_typ sup_ty with
| Some sub, Some sup ->
env.pairs <- S.add (sub, sup) env.pairs;
{ exp' with it = CallE (injection_name sub sup, e)}
| _, _ -> exp'
end
| _ -> exp'

(* Traversal boilerplate *)
Expand Down
Loading

0 comments on commit 08e26ac

Please sign in to comment.