CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Rename Expr.Box.inj to Expr.Box.lift

Browse Source 
it is more consistent with the naming of functions in Bindlib.
This commit is contained in:
Louis Gesbert 2022-10-21 15:33:05 +02:00
parent f9f834e30a
commit 7267543ca1
8 changed files with 41 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
compiler/desugared/ast.ml
View File

@ -139,13 +139,13 @@ module Rule = struct
match Shared_ast.Expr.compare_typ t1 t2 with
| 0 -> (
let open Bindlib in
let b1 = unbox (bind_var v1 (Expr.Box.inj r1.rule_just)) in
let b2 = unbox (bind_var v2 (Expr.Box.inj r2.rule_just)) in
let b1 = unbox (bind_var v1 (Expr.Box.lift r1.rule_just)) in
let b2 = unbox (bind_var v2 (Expr.Box.lift r2.rule_just)) in
let _, j1, j2 = unbind2 b1 b2 in
match Expr.compare j1 j2 with
| 0 ->
let b1 = unbox (bind_var v1 (Expr.Box.inj r1.rule_cons)) in
let b2 = unbox (bind_var v2 (Expr.Box.inj r2.rule_cons)) in
let b1 = unbox (bind_var v1 (Expr.Box.lift r1.rule_cons)) in
let b2 = unbox (bind_var v2 (Expr.Box.lift r2.rule_cons)) in
let _, c1, c2 = unbind2 b1 b2 in
Expr.compare c1 c2
| n -> n)

4
compiler/lcalc/compile_with_exceptions.ml
View File

@ -115,7 +115,7 @@ let rec translate_scope_lets
'm A.expr scope_body_expr Bindlib.box =
match scope_lets with
| Result e ->
Bindlib.box_apply (fun e -> Result e) (Expr.Box.inj (translate_expr ctx e))
Bindlib.box_apply (fun e -> Result e) (Expr.Box.lift (translate_expr ctx e))
| ScopeLet scope_let ->
let old_scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
@ -136,7 +136,7 @@ let rec translate_scope_lets
scope_let_expr = new_scope_let_expr;
})
new_scope_next
(Expr.Box.inj new_scope_let_expr)
(Expr.Box.lift new_scope_let_expr)
let rec translate_scopes
(decl_ctx : decl_ctx)

8
compiler/lcalc/compile_without_exceptions.ml
View File

@ -349,7 +349,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
| Result e ->
Bindlib.box_apply
(fun e -> Result e)
(Expr.Box.inj (translate_expr ~append_esome:false ctx e))
(Expr.Box.lift (translate_expr ~append_esome:false ctx e))
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
@ -379,7 +379,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
(Expr.Box.lift (translate_expr ctx ~append_esome:false expr))
(Bindlib.bind_var new_var new_next)
| ScopeLet
{
@ -406,7 +406,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
(Expr.Box.lift (translate_expr ctx ~append_esome:false expr))
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
| ScopeLet
{
@ -457,7 +457,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(Expr.Box.inj (translate_expr ctx ~append_esome:false expr))
(Expr.Box.lift (translate_expr ctx ~append_esome:false expr))
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
let translate_scope_body

14
compiler/scopelang/scope_to_dcalc.ml
View File

@ -381,7 +381,7 @@ let translate_rule
scope_let_pos = Marked.get_mark a;
})
(Bindlib.bind_var a_var next)
(Expr.Box.inj merged_expr)),
(Expr.Box.lift merged_expr)),
{
ctx with
scope_vars =
@ -434,7 +434,7 @@ let translate_rule
scope_let_kind = SubScopeVarDefinition;
})
(Bindlib.bind_var a_var next)
(Expr.Box.inj thunked_or_nonempty_new_e)),
(Expr.Box.lift thunked_or_nonempty_new_e)),
{
ctx with
subscope_vars =
@ -545,7 +545,7 @@ let translate_rule
scope_let_expr = call_expr;
})
(Bindlib.bind_var result_tuple_var next)
(Expr.Box.inj call_expr)
(Expr.Box.lift call_expr)
in
let result_bindings_lets next =
List.fold_right
@ -570,7 +570,7 @@ let translate_rule
mark_tany m pos_sigma );
})
(Bindlib.bind_var v next)
(Expr.Box.inj
(Expr.Box.lift
(Expr.make_var result_tuple_var (mark_tany m pos_sigma))),
i - 1 ))
all_subscope_output_vars_dcalc
@ -610,7 +610,7 @@ let translate_rule
scope_let_kind = Assertion;
})
(Bindlib.bind_var (Var.make "_") next)
(Expr.Box.inj new_e)),
(Expr.Box.lift new_e)),
ctx )
let translate_rules
@ -647,7 +647,7 @@ let translate_rules
( scope_lets
(Bindlib.box_apply
(fun return_exp -> Result return_exp)
(Expr.Box.inj return_exp)),
(Expr.Box.lift return_exp)),
new_ctx )
let translate_scope_decl
@ -744,7 +744,7 @@ let translate_scope_decl
mark_tany sigma.scope_mark pos_sigma );
})
(Bindlib.bind_var v next)
(Expr.Box.inj
(Expr.Box.lift
(Expr.make_var scope_input_var
(mark_tany sigma.scope_mark pos_sigma))),
i - 1 ))

24
compiler/shared_ast/expr.ml
View File

@ -53,12 +53,24 @@ module Box = struct
xb0 xb1 (B.box_list xbl),
mark )
let inj : ('a, 't) boxed_gexpr -> ('a, 't) gexpr B.box =
let lift : ('a, 't) boxed_gexpr -> ('a, 't) gexpr B.box =
fun em ->
B.box_apply (fun e -> Marked.mark (Marked.get_mark em) e) (Marked.unmark em)
module LiftStruct = Bindlib.Lift (StructFieldMap)
let lift_struct = LiftStruct.lift_box
module LiftEnum = Bindlib.Lift (EnumConstructorMap)
let lift_enum = LiftEnum.lift_box
module LiftScopeVars = Bindlib.Lift (ScopeVarMap)
let lift_scope_vars = LiftScopeVars.lift_box
end
let bind vars e = Bindlib.bind_mvar vars (Box.inj e)
let bind vars e = Bindlib.bind_mvar vars (Box.lift e)
let subst binder vars =
Bindlib.msubst binder (Array.of_list (List.map Marked.unmark vars))
@ -97,11 +109,10 @@ let ecatch e1 exn e2 = Box.app2 e1 e2 @@ fun e1 e2 -> ECatch (e1, exn, e2)
let elocation loc = Box.app0 @@ ELocation loc
let estruct name (fields : ('a, 't) boxed_gexpr StructFieldMap.t) mark =
let module Lift = Bindlib.Lift (StructFieldMap) in
Marked.mark mark
@@ Bindlib.box_apply
(fun fields -> EStruct (name, fields))
(Lift.lift_box (StructFieldMap.map Box.inj fields))
(Box.lift_struct (StructFieldMap.map Box.lift fields))
let estructaccess e1 field struc =
Box.app1 e1 @@ fun e1 -> EStructAccess (e1, field, struc)
@ -109,12 +120,11 @@ let estructaccess e1 field struc =
let eenuminj e1 cons enum = Box.app1 e1 @@ fun e1 -> EEnumInj (e1, cons, enum)
let ematchs e1 enum cases mark =
let module Lift = Bindlib.Lift (EnumConstructorMap) in
Marked.mark mark
@@ Bindlib.box_apply2
(fun e1 cases -> EMatchS (e1, enum, cases))
(Box.inj e1)
(Lift.lift_box (EnumConstructorMap.map Box.inj cases))
(Box.lift e1)
(Box.lift_enum (EnumConstructorMap.map Box.lift cases))
(* - Manipulation of marks - *)

4
compiler/shared_ast/expr.mli
View File

@ -335,9 +335,9 @@ module Box : sig
the latter would force us to resolve the box every time we need to recover
the annotation, which happens often. It's more efficient and convenient to
add the annotation outside of the box, and delay its injection (using
[box_inj]) to when the parent term gets built. *)
[lift]) to when the parent term gets built. *)
val inj : ('a, 't) boxed_gexpr -> ('a, 't) gexpr Bindlib.box
val lift : ('a, 't) boxed_gexpr -> ('a, 't) gexpr Bindlib.box
(** Inject the annotation within the box, to use e.g. when a [gexpr box] is
required for building parent terms *)

4
compiler/shared_ast/scope.ml
View File

@ -45,9 +45,9 @@ let map_exprs_in_lets :
(fun scope_let_next scope_let_expr ->
ScopeLet { scope_let with scope_let_next; scope_let_expr })
(Bindlib.bind_var (varf var_next) acc)
(Expr.Box.inj (f scope_let.scope_let_expr)))
(Expr.Box.lift (f scope_let.scope_let_expr)))
~init:(fun res ->
Bindlib.box_apply (fun res -> Result res) (Expr.Box.inj (f res)))
Bindlib.box_apply (fun res -> Result res) (Expr.Box.lift (f res)))
scope_body_expr
let rec fold_left ~f ~init scopes =

6
compiler/shared_ast/typing.ml
View File

@ -508,7 +508,7 @@ and typecheck_expr_top_down :
env (Array.to_list xs) tau_args
in
let body' = typecheck_expr_top_down ctx env t_ret body in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.inj body') in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') in
Expr.eabs binder' t_args mark
| A.EApp (e1, args) ->
let t_args = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args in
@ -585,7 +585,7 @@ let rec scope_body_expr ctx env ty_out body_expr =
| A.Result e ->
let e' = wrap_expr ctx (typecheck_expr_top_down ctx env ty_out) e in
let e' = Expr.map_marks ~f:get_ty_mark e' in
Bindlib.box_apply (fun e -> A.Result e) (Expr.Box.inj e')
Bindlib.box_apply (fun e -> A.Result e) (Expr.Box.lift e')
| A.ScopeLet
{
scope_let_kind;
@ -615,7 +615,7 @@ let rec scope_body_expr ctx env ty_out body_expr =
scope_let_next;
scope_let_pos;
})
(Expr.Box.inj (Expr.map_marks ~f:get_ty_mark e))
(Expr.Box.lift (Expr.map_marks ~f:get_ty_mark e))
scope_let_next
let scope_body ctx env body =