clarify make_matchopt + lcalc's ast ocamlformat

This commit is contained in:
Alain 2022-02-02 12:23:52 +01:00
parent 67ccfb0122
commit d7c422d33c
4 changed files with 86 additions and 86 deletions

View File

@ -24,32 +24,35 @@ type lit =
| LDate of Runtime.date
| LDuration of Runtime.duration
type except = ConflictError | EmptyError | NoValueProvided | Crash
[@@deriving show]
type except = ConflictError | EmptyError | NoValueProvided | Crash [@@deriving show]
let bla = fun _ b fmt x ->
let bla _ b fmt x =
let xs, body = Bindlib.unmbind x in
let xs = xs
|> Array.to_list
|> List.map (fun x -> (Bindlib.name_of x ^ "_" ^ (string_of_int @@ Bindlib.uid_of x)))
let xs =
xs |> Array.to_list
|> List.map (fun x -> Bindlib.name_of x ^ "_" ^ string_of_int @@ Bindlib.uid_of x)
|> String.concat ", "
in
Format.fprintf fmt "Binder(%a, %a)" Format.pp_print_string xs b body
type expr =
| EVar of (expr Bindlib.var [@polyprinter fun _ fmt x -> Format.fprintf fmt "%s_%d" (Bindlib.name_of x) (Bindlib.uid_of x)]) Pos.marked
| ETuple of expr Pos.marked list * (D.StructName.t [@opaque]) option
| EVar of
(expr Bindlib.var
[@polyprinter
fun _ fmt x -> Format.fprintf fmt "%s_%d" (Bindlib.name_of x) (Bindlib.uid_of x)])
Pos.marked
| ETuple of expr Pos.marked list * (D.StructName.t[@opaque]) option
(** The [MarkedString.info] is the former struct field name*)
| ETupleAccess of expr Pos.marked * int * (D.StructName.t [@opaque]) option * D.typ Pos.marked list
| ETupleAccess of expr Pos.marked * int * (D.StructName.t[@opaque]) option * D.typ Pos.marked list
(** The [MarkedString.info] is the former struct field name *)
| EInj of expr Pos.marked * int * (D.EnumName.t [@opaque]) * D.typ Pos.marked list
| EInj of expr Pos.marked * int * (D.EnumName.t[@opaque]) * D.typ Pos.marked list
(** The [MarkedString.info] is the former enum case name *)
| EMatch of expr Pos.marked * expr Pos.marked list * (D.EnumName.t [@opaque])
| EMatch of expr Pos.marked * expr Pos.marked list * (D.EnumName.t[@opaque])
(** The [MarkedString.info] is the former enum case name *)
| EArray of expr Pos.marked list
| ELit of (lit [@opaque])
| EAbs of ((expr, expr Pos.marked) Bindlib.mbinder [@polyprinter bla]) Pos.marked * D.typ Pos.marked list
| ELit of (lit[@opaque])
| EAbs of
((expr, expr Pos.marked) Bindlib.mbinder[@polyprinter bla]) Pos.marked * D.typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of D.operator
@ -116,80 +119,76 @@ let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let make_some' (e : expr Pos.marked) : expr = EInj (e, 1, option_enum, [])
let make_matchopt (e : expr Pos.marked Bindlib.box) (e_none : expr Pos.marked Bindlib.box)
(** [make_matchopt_dumb arg e_none e_some] build an expression [match arg with |None -> e_none | Some -> e_some] and requires e_some and e_none to be in the form [EAbs ...].*)
let make_matchopt_dumb (arg : expr Pos.marked Bindlib.box) (e_none : expr Pos.marked Bindlib.box)
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox e in
let pos = Pos.get_position @@ Bindlib.unbox arg in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ e = e and+ e_none = e_none and+ e_some = e_some in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some in
mark @@ EMatch (e, [ e_none; e_some ], option_enum)
mark @@ EMatch (arg, [ e_none; e_some ], option_enum)
let make_matchopt'
(pos: Pos.t)
(tau: D.typ Pos.marked)
(arg: expr Pos.marked Bindlib.box)
(e_none: expr Pos.marked Bindlib.box)
(e_some: expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box)
: expr Pos.marked Bindlib.box =
let x = Var.make ("unit", pos) in
let v = Var.make ("v", pos) in
make_matchopt arg
(make_abs (Array.of_list [x]) (e_none) (pos) [D.TLit D.TUnit, pos] pos)
(make_abs (Array.of_list [v]) (e_some (let+ v = Bindlib.box_var v in (v, pos))) pos [tau] pos)
;;
let make_matchopt''
(pos: Pos.t)
(v: Var.t)
(tau: D.typ Pos.marked)
(arg: expr Pos.marked Bindlib.box)
(e_none: expr Pos.marked Bindlib.box)
(e_some: expr Pos.marked Bindlib.box)
: expr Pos.marked Bindlib.box =
(** [make_matchopt pos v tau arg e_none e_some] builds an expression [match arg with | None () -> e_none | Some v -> e_some]. It binds v to e_some, permitting it to be used inside the expression. There is no requirements on the form of both e_some and e_none. *)
let make_matchopt (pos : Pos.t) (v : Var.t) (tau : D.typ Pos.marked)
(arg : expr Pos.marked Bindlib.box) (e_none : expr Pos.marked Bindlib.box)
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
(* todo: replace this "unit" variable by the [()] pattern *)
let x = Var.make ("unit", pos) in
make_matchopt arg
(make_abs (Array.of_list [x]) e_none pos [D.TLit D.TUnit, pos] pos)
(make_abs (Array.of_list [v]) e_some pos [tau] pos)
make_matchopt_dumb arg
(make_abs (Array.of_list [ x ]) e_none pos [ (D.TLit D.TUnit, pos) ] pos)
(make_abs (Array.of_list [ v ]) e_some pos [ tau ] pos)
let make_bindopt
(pos: Pos.t)
(tau: D.typ Pos.marked)
(e1: expr Pos.marked Bindlib.box)
(e2: expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box)
: expr Pos.marked Bindlib.box =
let make_matchopt' (pos : Pos.t) (tau : D.typ Pos.marked) (arg : expr Pos.marked Bindlib.box)
(e_none : expr Pos.marked Bindlib.box)
(e_some : expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box) :
expr Pos.marked Bindlib.box =
let x = Var.make ("unit", pos) in
let v = Var.make ("v", pos) in
make_matchopt' pos tau e1 (make_none pos) e2
make_matchopt_dumb arg
(make_abs (Array.of_list [ x ]) e_none pos [ (D.TLit D.TUnit, pos) ] pos)
(make_abs
(Array.of_list [ v ])
(e_some
(let+ v = Bindlib.box_var v in
(v, pos)))
pos [ tau ] pos)
let make_bindmopt
(pos: Pos.t)
(taus: D.typ Pos.marked list)
(e1s: expr Pos.marked Bindlib.box list)
(e2s: expr Pos.marked Bindlib.box list -> expr Pos.marked Bindlib.box)
: expr Pos.marked Bindlib.box =
let make_bindopt (pos : Pos.t) (tau : D.typ Pos.marked) (e1 : expr Pos.marked Bindlib.box)
(e2 : expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box
=
make_matchopt' pos tau e1 (make_none pos) e2
let make_bindmopt (pos : Pos.t) (taus : D.typ Pos.marked list)
(e1s : expr Pos.marked Bindlib.box list)
(e2s : expr Pos.marked Bindlib.box list -> expr Pos.marked Bindlib.box) :
expr Pos.marked Bindlib.box =
let dummy = Var.make ("unit", pos) in
let vs = List.mapi (fun i _ -> Var.make (Format.sprintf "v_%i" i, pos)) e1s in
let e1' final = List.combine (List.combine vs taus) e1s
|> List.fold_left (fun acc ((x, tau), arg) ->
make_matchopt arg
(make_abs (Array.of_list [dummy]) (make_none pos) pos [D.TLit D.TUnit, pos] pos)
(make_abs (Array.of_list [x]) acc pos [tau] pos)
) final
let e1' final =
List.combine (List.combine vs taus) e1s
|> List.fold_left
(fun acc ((x, tau), arg) ->
make_matchopt_dumb arg
(make_abs (Array.of_list [ dummy ]) (make_none pos) pos [ (D.TLit D.TUnit, pos) ] pos)
(make_abs (Array.of_list [ x ]) acc pos [ tau ] pos))
final
in
e1' (make_some (e2s (List.map (fun v -> let+ v = Bindlib.box_var v in (v, pos)) vs)))
e1'
(make_some
(e2s
(List.map
(fun v ->
let+ v = Bindlib.box_var v in
(v, pos))
vs)))
let handle_default = Var.make ("handle_default", Pos.no_pos)

View File

@ -30,8 +30,7 @@ type lit =
| LDate of Runtime.date
| LDuration of Runtime.duration
type except = ConflictError | EmptyError | NoValueProvided | Crash
[@@deriving show]
type except = ConflictError | EmptyError | NoValueProvided | Crash [@@deriving show]
type expr =
| EVar of expr Bindlib.var Pos.marked
@ -45,8 +44,9 @@ type expr =
| EMatch of expr Pos.marked * expr Pos.marked list * Dcalc.Ast.EnumName.t
(** The [MarkedString.info] is the former enum case name *)
| EArray of expr Pos.marked list
| ELit of (lit [@opaque])
| EAbs of ((expr, expr Pos.marked) Bindlib.mbinder [@opaque]) Pos.marked * Dcalc.Ast.typ Pos.marked list
| ELit of (lit[@opaque])
| EAbs of
((expr, expr Pos.marked) Bindlib.mbinder[@opaque]) Pos.marked * Dcalc.Ast.typ Pos.marked list
| EApp of expr Pos.marked * expr Pos.marked list
| EAssert of expr Pos.marked
| EOp of Dcalc.Ast.operator
@ -106,23 +106,22 @@ val make_some : expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box
val make_some' : expr Pos.marked -> expr
val make_matchopt :
val make_matchopt_dumb :
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box
(** [e' = make_matchopt'' pos v e e_none e_some]
Builds the term corresponding to [match e with | None -> fun () -> e_none |Some -> fun v -> e_some].
*)
val make_matchopt'':
val make_matchopt :
Pos.t ->
Var.t ->
Dcalc.Ast.typ Pos.marked ->
Dcalc.Ast.typ Pos.marked ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box ->
expr Pos.marked Bindlib.box
(** [e' = make_matchopt'' pos v e e_none e_some] Builds the term corresponding to
[match e with | None -> fun () -> e_none |Some -> fun v -> e_some]. *)
val make_bindopt :
Pos.t ->
@ -131,10 +130,10 @@ val make_bindopt :
(expr Pos.marked Bindlib.box -> expr Pos.marked Bindlib.box) ->
expr Pos.marked Bindlib.box
val make_bindmopt:
(Pos.t) ->
(Dcalc.Ast.typ Pos.marked list) ->
(expr Pos.marked Bindlib.box list) ->
val make_bindmopt :
Pos.t ->
Dcalc.Ast.typ Pos.marked list ->
expr Pos.marked Bindlib.box list ->
(expr Pos.marked Bindlib.box list -> expr Pos.marked Bindlib.box) ->
expr Pos.marked Bindlib.box

View File

@ -227,7 +227,7 @@ let rec translate_expr (ctx: ctx) (e: D.expr Pos.marked)
let arg' = translate_expr ctx arg in
A.make_matchopt arg'
A.make_matchopt_dumb arg'
(A.make_abs [| unit |] (Bindlib.box (A.ERaise A.NoValueProvided, pos_c)) pos_c [D.TAny, pos_c] pos_c)
(A.make_abs [| x |] ((A.make_var (x, pos_c))) pos_c [D.TAny, pos_c] pos_c)
@ -244,7 +244,7 @@ let rec translate_expr (ctx: ctx) (e: D.expr Pos.marked)
let unit = A.Var.make ("unit", pos_c) in
let x = A.Var.make ("assertion_argument", pos_c) in
A.make_matchopt arg'
A.make_matchopt_dumb arg'
(A.make_abs [| unit |] (Bindlib.box (A.ERaise A.NoValueProvided, pos_c)) pos_c [D.TAny, pos_c] pos_c)
(A.make_abs [| x |] (Bindlib.box_apply (fun arg -> A.EAssert arg, pos_c) (A.make_var (x, pos_c))) pos_c [D.TAny, pos_c] pos_c)
@ -257,7 +257,7 @@ let rec translate_expr (ctx: ctx) (e: D.expr Pos.marked)
| Some {{ v }} -> {{ acc }}
end
] *)
A.make_matchopt'' pos_c v (D.TAny, pos_c) c' (A.make_none pos_c) acc
A.make_matchopt pos_c v (D.TAny, pos_c) c' (A.make_none pos_c) acc
)
;;

View File

@ -1,7 +1,9 @@
(library
(name lcalc)
(public_name catala.lcalc)
(libraries bindlib dcalc scopelang runtime))
(libraries bindlib dcalc scopelang runtime)
(preprocess
(pps visitors.ppx ppx_deriving.show)))
(documentation
(package catala)