Correct types for make_some and make_none

This commit is contained in:
Denis Merigoux 2022-02-24 16:49:18 +01:00
parent c65c38a2d5
commit ddacc94de2
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3

View File

@ -93,14 +93,14 @@ let option_enum_config : (D.EnumConstructor.t * D.typ Pos.marked) list =
let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box =
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
Bindlib.box @@ mark @@ EInj (mark @@ ELit LUnit, 0, option_enum, [ (D.TLit D.TUnit, pos) ])
Bindlib.box @@ mark
@@ EInj (mark @@ ELit LUnit, 0, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox e in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ e = e in
mark @@ EInj (e, 1, option_enum, [ (D.TAny, pos) ])
mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
(** [make_matchopt_with_abs_arms 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