@@ -41,7 +41,7 @@ type context = {
4141 var_types : (Symbol .symbol_id , scheme ) Hashtbl .t ;
4242
4343 (* * Current effect context *)
44- current_effect : effect ;
44+ current_effect : eff ;
4545}
4646
4747(* Result bind - define before use *)
@@ -214,8 +214,8 @@ and ast_to_ty_arg (ctx : context) (arg : type_arg) : ty =
214214 | TyArg ty -> ast_to_ty ctx ty
215215 | NatArg _ -> TNat (NLit 0 ) (* TODO: Convert nat expr *)
216216
217- and ast_to_eff (ctx : context ) (eff : effect_expr ) : effect =
218- match eff with
217+ and ast_to_eff (ctx : context ) (e : effect_expr ) : eff =
218+ match e with
219219 | EffCon (id , _ ) -> ESingleton id.name
220220 | EffVar _id -> fresh_effvar ctx.level
221221 | EffUnion (e1 , e2 ) -> EUnion [ast_to_eff ctx e1; ast_to_eff ctx e2]
@@ -298,7 +298,7 @@ and pattern_span (pat : pattern) : Span.t =
298298 | PatAs (id , _ ) -> id.span
299299
300300(* * Synthesize (infer) the type of an expression *)
301- let rec synth (ctx : context ) (expr : expr ) : (ty * effect ) result =
301+ let rec synth (ctx : context ) (expr : expr ) : (ty * eff ) result =
302302 match expr with
303303 | ExprVar id ->
304304 let * ty = lookup_var ctx id in
@@ -502,8 +502,8 @@ let rec synth (ctx : context) (expr : expr) : (ty * effect) result =
502502 | ExprSpan (e , _span ) ->
503503 synth ctx e
504504
505- and synth_app (ctx : context ) (func_ty : ty ) (func_eff : effect )
506- (args : expr list ) (span : Span.t ) : (ty * effect ) result =
505+ and synth_app (ctx : context ) (func_ty : ty ) (func_eff : eff )
506+ (args : expr list ) (span : Span.t ) : (ty * eff ) result =
507507 match args with
508508 | [] -> Ok (func_ty, func_eff)
509509 | arg :: rest ->
@@ -527,7 +527,7 @@ and synth_app (ctx : context) (func_ty : ty) (func_eff : effect)
527527 end
528528
529529(* * Check an expression against an expected type *)
530- and check (ctx : context ) (expr : expr ) (expected : ty ) : effect result =
530+ and check (ctx : context ) (expr : expr ) (expected : ty ) : eff result =
531531 match (expr, repr expected) with
532532 (* Lambda checking *)
533533 | (ExprLambda lam , TArrow (param_ty , ret_ty , arr_eff )) ->
@@ -584,13 +584,13 @@ and check (ctx : context) (expr : expr) (expected : ty) : effect result =
584584 | _ ->
585585 check_subsumption ctx expr expected
586586
587- and check_subsumption (ctx : context ) (expr : expr ) (expected : ty ) : effect result =
587+ and check_subsumption (ctx : context ) (expr : expr ) (expected : ty ) : eff result =
588588 let * (actual, eff) = synth ctx expr in
589589 match Unify. unify actual expected with
590590 | Ok () -> Ok eff
591591 | Error e -> Error (UnificationFailed (e, expr_span expr))
592592
593- and synth_list (ctx : context ) (exprs : expr list ) : ((ty * effect ) list) result =
593+ and synth_list (ctx : context ) (exprs : expr list ) : ((ty * eff ) list) result =
594594 List. fold_right (fun expr acc ->
595595 match acc with
596596 | Error e -> Error e
@@ -600,7 +600,7 @@ and synth_list (ctx : context) (exprs : expr list) : ((ty * effect) list) result
600600 | Ok result -> Ok (result :: results)
601601 ) exprs (Ok [] )
602602
603- and check_list (ctx : context ) (exprs : expr list ) (tys : ty list ) : (effect list) result =
603+ and check_list (ctx : context ) (exprs : expr list ) (tys : ty list ) : (eff list) result =
604604 List. fold_right2 (fun expr ty acc ->
605605 match acc with
606606 | Error e -> Error e
@@ -611,7 +611,7 @@ and check_list (ctx : context) (exprs : expr list) (tys : ty list) : (effect lis
611611 ) exprs tys (Ok [] )
612612
613613and synth_record_fields (ctx : context ) (fields : (ident * expr option) list )
614- : ((string * ty * effect ) list) result =
614+ : ((string * ty * eff ) list) result =
615615 List. fold_right (fun (id , expr_opt ) acc ->
616616 match acc with
617617 | Error e -> Error e
@@ -630,7 +630,7 @@ and synth_record_fields (ctx : context) (fields : (ident * expr option) list)
630630 end
631631 ) fields (Ok [] )
632632
633- and synth_block (ctx : context ) (blk : block ) : (ty * effect ) result =
633+ and synth_block (ctx : context ) (blk : block ) : (ty * eff ) result =
634634 let * effs = List. fold_left (fun acc stmt ->
635635 let * effs = acc in
636636 let * eff = synth_stmt ctx stmt in
@@ -643,7 +643,7 @@ and synth_block (ctx : context) (blk : block) : (ty * effect) result =
643643 | None ->
644644 Ok (ty_unit, union_eff effs)
645645
646- and check_block (ctx : context ) (blk : block ) (expected : ty ) : effect result =
646+ and check_block (ctx : context ) (blk : block ) (expected : ty ) : eff result =
647647 let * effs = List. fold_left (fun acc stmt ->
648648 let * effs = acc in
649649 let * eff = synth_stmt ctx stmt in
@@ -659,7 +659,7 @@ and check_block (ctx : context) (blk : block) (expected : ty) : effect result =
659659 | Error e -> Error (UnificationFailed (e, Span. dummy))
660660 end
661661
662- and synth_stmt (ctx : context ) (stmt : stmt ) : effect result =
662+ and synth_stmt (ctx : context ) (stmt : stmt ) : eff result =
663663 match stmt with
664664 | StmtLet sl ->
665665 let ctx' = enter_level ctx in
@@ -688,7 +688,7 @@ and synth_stmt (ctx : context) (stmt : stmt) : effect result =
688688 Ok (union_eff [iter_eff; body_eff])
689689
690690and synth_binop (ctx : context ) (left : expr ) (op : binary_op ) (right : expr )
691- (span : Span.t ) : (ty * effect ) result =
691+ (span : Span.t ) : (ty * eff ) result =
692692 let * (left_ty, left_eff) = synth ctx left in
693693 let * (right_ty, right_eff) = synth ctx right in
694694 let eff = union_eff [left_eff; right_eff] in
@@ -714,7 +714,7 @@ and synth_binop (ctx : context) (left : expr) (op : binary_op) (right : expr)
714714 | Error e , _ | _ , Error e -> Error (UnificationFailed (e, span))
715715 end
716716
717- and synth_unary (ctx : context ) (op : unary_op ) (operand : expr ) : (ty * effect ) result =
717+ and synth_unary (ctx : context ) (op : unary_op ) (operand : expr ) : (ty * eff ) result =
718718 let * (operand_ty, operand_eff) = synth ctx operand in
719719 match op with
720720 | OpNeg ->
@@ -822,7 +822,7 @@ and find_field (name : string) (row : row) : ty option =
822822 else find_field name rest
823823 | RVar _ -> None
824824
825- and union_eff (effs : effect list ) : effect =
825+ and union_eff (effs : eff list ) : eff =
826826 let effs = List. filter (fun e -> e <> EPure ) effs in
827827 match effs with
828828 | [] -> EPure
0 commit comments