Cleanup: definitions.ml is not for values

A module without mli is ok as long as it only contains types

Here we already stretch it a bit with some functor applications, but having
toplevel values defeats the expectation that you can safely `open` this module.
This commit is contained in:
Louis Gesbert 2023-05-17 13:26:47 +02:00
parent da04faf02f
commit ba52aae401
11 changed files with 62 additions and 57 deletions

View File

@ -14,7 +14,7 @@
License for the specific language governing permissions and limitations under
the License. *)
include Shared_ast
open Shared_ast
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr
@ -22,30 +22,32 @@ and 'm expr = (lcalc, 'm mark) gexpr
type 'm program = 'm expr Shared_ast.program
module OptionMonad = struct
let return ~(mark : 'a mark) e = Expr.einj e some_constr option_enum mark
let return ~(mark : 'a mark) e =
Expr.einj e Expr.some_constr Expr.option_enum mark
let empty ~(mark : 'a mark) =
Expr.einj (Expr.elit LUnit mark) none_constr option_enum mark
Expr.einj (Expr.elit LUnit mark) Expr.none_constr Expr.option_enum mark
let bind_var ~(mark : 'a mark) f x arg =
let cases =
EnumConstructor.Map.of_seq
(List.to_seq
[
( none_constr,
( Expr.none_constr,
let x = Var.make "_" in
Expr.eabs
(Expr.bind [| x |]
(Expr.einj (Expr.evar x mark) none_constr option_enum mark))
(Expr.einj (Expr.evar x mark) Expr.none_constr
Expr.option_enum mark))
[TLit TUnit, Expr.mark_pos mark]
mark );
(* | None x -> None x *)
( some_constr,
( Expr.some_constr,
Expr.eabs (Expr.bind [| x |] f) [TAny, Expr.mark_pos mark] mark )
(*| Some x -> f (where f contains x as a free variable) *);
])
in
Expr.ematch arg option_enum cases mark
Expr.ematch arg Expr.option_enum cases mark
let bind ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
@ -86,7 +88,7 @@ module OptionMonad = struct
~init:
(Expr.einj
(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark)
some_constr option_enum mark)
Expr.some_constr Expr.option_enum mark)
let map_var ~(mark : 'a mark) f x arg = mmap_mvar f [x] [arg] ~mark
@ -110,16 +112,16 @@ module OptionMonad = struct
EnumConstructor.Map.of_seq
(List.to_seq
[
( none_constr,
( Expr.none_constr,
let x = Var.make var_name in
Expr.eabs
(Expr.bind [| x |] (Expr.eraise NoValueProvided mark))
[TAny, Expr.mark_pos mark]
mark );
(* | None x -> raise NoValueProvided *)
some_constr, Expr.fun_id mark (* | Some x -> x*);
Expr.some_constr, Expr.fun_id mark (* | Some x -> x*);
])
in
if toplevel then Expr.ematch arg option_enum cases mark
else return ~mark (Expr.ematch arg option_enum cases mark)
if toplevel then Expr.ematch arg Expr.option_enum cases mark
else return ~mark (Expr.ematch arg Expr.option_enum cases mark)
end

View File

@ -27,13 +27,6 @@ type 'm program = 'm expr Shared_ast.program
(** {1 Option-related management}*)
(** {2 Names and types}*)
val option_enum : EnumName.t
val none_constr : EnumConstructor.t
val some_constr : EnumConstructor.t
val option_enum_config : typ EnumConstructor.Map.t
(** {2 Term building and management for the [option] monad}*)
module OptionMonad : sig

View File

@ -720,7 +720,7 @@ let translate_program (prgm : typed D.program) : untyped A.program =
prgm.decl_ctx with
ctx_enums =
prgm.decl_ctx.ctx_enums
|> EnumName.Map.add A.option_enum A.option_enum_config;
|> EnumName.Map.add Expr.option_enum Expr.option_enum_config;
}
in
let decl_ctx =

View File

@ -164,7 +164,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ) : unit =
| TStruct s -> Format.fprintf fmt "%a.t" format_to_module_name (`Sname s)
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Ast.option_enum
format_enum_name Expr.option_enum
| TEnum e -> Format.fprintf fmt "%a.t" format_to_module_name (`Ename e)
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a@]"

View File

@ -72,7 +72,7 @@ module To_jsoo = struct
Format.fprintf fmt "Js.Unsafe.any_js_array Js.t "
| TOption t ->
Format.fprintf fmt "@[<hov 2>(%a)@] %a" format_typ_with_parens t
format_enum_name Lcalc.Ast.option_enum
format_enum_name Expr.option_enum
| TEnum e -> Format.fprintf fmt "%a Js.t" format_enum_name e
| TArray t1 ->
Format.fprintf fmt "@[%a@ Js.js_array Js.t@]" format_typ_with_parens t1

View File

@ -295,13 +295,13 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
Format.fprintf fmt "%a.%a" (format_expression ctx) e1
format_struct_field_name field
| EInj (_, cons, e_name)
when EnumName.compare e_name L.option_enum = 0
&& EnumConstructor.compare cons L.none_constr = 0 ->
when EnumName.equal e_name Expr.option_enum
&& EnumConstructor.equal cons Expr.none_constr ->
(* We translate the option type with an overloading by Python's [None] *)
Format.fprintf fmt "None"
| EInj (e, cons, e_name)
when EnumName.compare e_name L.option_enum = 0
&& EnumConstructor.compare cons L.some_constr = 0 ->
when EnumName.equal e_name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
(* We translate the option type with an overloading by Python's [None] *)
format_expression ctx fmt e
| EInj (e, cons, enum_name) ->
@ -414,7 +414,7 @@ let rec format_statement
Format.fprintf fmt "@[<hov 4>if %a:@\n%a@]@\n@[<hov 4>else:@\n%a@]"
(format_expression ctx) cond (format_block ctx) b1 (format_block ctx) b2
| SSwitch (e1, e_name, [(case_none, _); (case_some, case_some_var)])
when EnumName.compare e_name L.option_enum = 0 ->
when EnumName.equal e_name Expr.option_enum ->
(* We translate the option type with an overloading by Python's [None] *)
let tmp_var = VarName.fresh ("perhaps_none_arg", Pos.no_pos) in
Format.fprintf fmt

View File

@ -433,14 +433,8 @@ and ('a, 'b, 't) base_gexpr =
}
-> ('a, < exceptions : yes ; .. >, 't) base_gexpr
let option_enum : EnumName.t = EnumName.fresh ("eoption", Pos.no_pos)
let none_constr : EnumConstructor.t = EnumConstructor.fresh ("ENone", Pos.no_pos)
let some_constr : EnumConstructor.t = EnumConstructor.fresh ("ESome", Pos.no_pos)
let option_enum_config : typ EnumConstructor.Map.t =
EnumConstructor.Map.empty
|> EnumConstructor.Map.add none_constr (TLit TUnit, Pos.no_pos)
|> EnumConstructor.Map.add some_constr (TAny, Pos.no_pos)
(* Useful for errors and printing, for example *)
(* type any_expr = AnyExpr : ('a, _ mark) gexpr -> any_expr *)
type ('a, 't) boxed_gexpr = (('a, 't) naked_gexpr Bindlib.box, 't) Marked.t
(** The annotation is lifted outside of the box for expressions *)

View File

@ -240,6 +240,16 @@ let with_ty (type m) (m : m mark) ?pos (ty : typ) : m mark =
let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
match m with Untyped { pos } -> Marked.mark pos typ | Typed { ty; _ } -> ty
(* - Predefined types (option) - *)
let option_enum = EnumName.fresh ("eoption", Pos.no_pos)
let none_constr = EnumConstructor.fresh ("ENone", Pos.no_pos)
let some_constr = EnumConstructor.fresh ("ESome", Pos.no_pos)
let option_enum_config =
EnumConstructor.Map.singleton none_constr (TLit TUnit, Pos.no_pos)
|> EnumConstructor.Map.add some_constr (TAny, Pos.no_pos)
(* - Traversal functions - *)
(* shallow map *)

View File

@ -143,7 +143,7 @@ val escopecall :
val fun_id : 'm mark -> ('a any, 'm mark) boxed_gexpr
(** Manipulation of marks *)
(** {2 Manipulation of marks} *)
val no_mark : 'm mark -> 'm mark
val mark_pos : 'm mark -> Pos.t
@ -171,6 +171,13 @@ val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
(** Returns the corresponding type on a typed expr, or [typ] (defaulting to
[TAny]) at the current position on an untyped one *)
(** {2 Predefined types} *)
val option_enum : EnumName.t
val none_constr : EnumConstructor.t
val some_constr : EnumConstructor.t
val option_enum_config : typ EnumConstructor.Map.t
(** Manipulation of marked expressions *)
val pos : ('a, 'm mark) Marked.t -> Pos.t

View File

@ -335,9 +335,8 @@ let rec evaluate_operator
| HandleDefaultOpt, [(EArray exps, _); justification; conclusion] -> (
let valid_exceptions =
ListLabels.filter exps ~f:(function
| EInj { name; cons; _ }, _
when EnumName.equal name Definitions.option_enum ->
EnumConstructor.equal cons Definitions.some_constr
| EInj { name; cons; _ }, _ when EnumName.equal name Expr.option_enum ->
EnumConstructor.equal cons Expr.some_constr
| _ -> err ())
in
@ -347,31 +346,31 @@ let rec evaluate_operator
Marked.unmark (evaluate_expr (Expr.unthunk_term_nobox justification m))
with
| EInj { name; cons; e = ELit (LBool true), _ }
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.some_constr ->
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
Marked.unmark (evaluate_expr (Expr.unthunk_term_nobox conclusion m))
| EInj { name; cons; e = (ELit (LBool false), _) as e }
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.some_constr ->
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
EInj
{
name = Definitions.option_enum;
cons = Definitions.none_constr;
name = Expr.option_enum;
cons = Expr.none_constr;
e = Marked.same_mark_as (ELit LUnit) e;
}
| EInj { name; cons; e }
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.none_constr ->
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.none_constr ->
EInj
{
name = Definitions.option_enum;
cons = Definitions.none_constr;
name = Expr.option_enum;
cons = Expr.none_constr;
e = Marked.same_mark_as (ELit LUnit) e;
}
| _ -> err ())
| [((EInj { cons; name; _ } as e), _)]
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.some_constr ->
when EnumName.equal name Expr.option_enum
&& EnumConstructor.equal cons Expr.some_constr ->
e
| [_] -> err ()
| _ -> raise (CatalaException ConflictError))
@ -584,8 +583,8 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
(fun ty ->
match Marked.unmark ty with
| TOption _ ->
(Expr.einj (Expr.elit LUnit mark_e) Definitions.none_constr
Definitions.option_enum mark_e
(Expr.einj (Expr.elit LUnit mark_e) Expr.none_constr
Expr.option_enum mark_e
: (_, _) boxed_gexpr)
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)

View File

@ -526,8 +526,8 @@ and typecheck_expr_top_down :
in
Expr.estructaccess e_struct' field name mark
| A.EInj { name; cons; e = e_enum }
when Definitions.EnumName.equal name Definitions.option_enum ->
if Definitions.EnumConstructor.equal cons Definitions.some_constr then
when Definitions.EnumName.equal name Expr.option_enum ->
if Definitions.EnumConstructor.equal cons Expr.some_constr then
let cell_type = unionfind (TAny (Any.fresh ())) in
let mark = mark_with_tau_and_unify (unionfind (TOption cell_type)) in
let e_enum' =
@ -552,12 +552,12 @@ and typecheck_expr_top_down :
in
Expr.einj e_enum' cons name mark
| A.EMatch { e = e1; name; cases }
when Definitions.EnumName.compare name Definitions.option_enum = 0 ->
when Definitions.EnumName.equal name Expr.option_enum ->
let cell_type = unionfind ~pos:e1 (TAny (Any.fresh ())) in
let t_arg = unionfind ~pos:e1 (TOption cell_type) in
let cases_ty =
ListLabels.fold_right2
[A.none_constr; A.some_constr]
[Expr.none_constr; Expr.some_constr]
[unionfind ~pos:e1 (TLit TUnit); cell_type]
~f:A.EnumConstructor.Map.add ~init:A.EnumConstructor.Map.empty
in