Various small fixes to resolve conversations

This commit is contained in:
Denis Merigoux 2023-04-21 14:51:15 +02:00
parent d384db4e71
commit 32ee2a0c72
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
10 changed files with 8862 additions and 14682 deletions

View File

@ -154,7 +154,7 @@ let driver source_file (options : Cli.options) : int =
| exception Sys_error _ -> ())
options.plugins_dirs;
Cli.set_option_globals options;
Printexc.record_backtrace options.debug;
if options.debug then Printexc.record_backtrace true;
Cli.debug_print "Reading files...";
let filename = ref "" in
(match source_file with
@ -426,6 +426,10 @@ let driver source_file (options : Cli.options) : int =
as backend -> (
Cli.debug_print "Compiling program into lambda calculus...";
let prgm =
if options.trace && options.avoid_exceptions then
Errors.raise_error
"Option --avoid_exceptions is not compatible with option \
--trace";
if options.avoid_exceptions then
Shared_ast.Program.untype
@@ Lcalc.Compile_without_exceptions.translate_program prgm

View File

@ -21,103 +21,105 @@ and 'm expr = (lcalc, 'm mark) gexpr
type 'm program = 'm expr Shared_ast.program
let monad_return ~(mark : 'a mark) e = Expr.einj e some_constr option_enum mark
module OptionMonad = struct
let return ~(mark : 'a mark) e = Expr.einj e some_constr option_enum mark
let monad_empty ~(mark : 'a mark) =
Expr.einj (Expr.elit LUnit mark) none_constr option_enum mark
let empty ~(mark : 'a mark) =
Expr.einj (Expr.elit LUnit mark) none_constr option_enum mark
let monad_bind_var ~(mark : 'a mark) f x arg =
let cases =
EnumConstructor.Map.of_seq
(List.to_seq
[
( none_constr,
let x = Var.make "_" in
Expr.eabs
(Expr.bind [| x |]
(Expr.einj (Expr.evar x mark) none_constr option_enum mark))
[TLit TUnit, Expr.mark_pos mark]
mark );
(* | None x -> None x *)
( 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
let bind_var ~(mark : 'a mark) f x arg =
let cases =
EnumConstructor.Map.of_seq
(List.to_seq
[
( none_constr,
let x = Var.make "_" in
Expr.eabs
(Expr.bind [| x |]
(Expr.einj (Expr.evar x mark) none_constr option_enum mark))
[TLit TUnit, Expr.mark_pos mark]
mark );
(* | None x -> None x *)
( 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
let monad_bind ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
(* todo modify*)
monad_bind_var f x arg ~mark
let bind ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
(* todo modify*)
bind_var f x arg ~mark
let monad_bind_cont ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
monad_bind_var (f x) x arg ~mark
let bind_cont ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
bind_var (f x) x arg ~mark
let monad_mbind_mvar ~(mark : 'a mark) f xs args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ ->
None *)
ListLabels.fold_left2 xs args ~f:(monad_bind_var ~mark)
~init:(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark)
let mbind_mvar ~(mark : 'a mark) f xs args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _
-> None *)
ListLabels.fold_left2 xs args ~f:(bind_var ~mark)
~init:(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark)
let monad_mbind ~(mark : 'a mark) ~(var_name : string) f args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ ->
None *)
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
monad_mbind_mvar f vars args ~mark
let mbind ~(mark : 'a mark) ~(var_name : string) f args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _
-> None *)
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
mbind_mvar f vars args ~mark
let monad_mbind_cont ~(mark : 'a mark) ~(var_name : string) f args =
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
ListLabels.fold_left2 vars args ~f:(monad_bind_var ~mark) ~init:(f vars)
(* monad_mbind_mvar (f vars) vars args ~mark *)
let mbind_cont ~(mark : 'a mark) ~(var_name : string) f args =
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
ListLabels.fold_left2 vars args ~f:(bind_var ~mark) ~init:(f vars)
(* mbind_mvar (f vars) vars args ~mark *)
let monad_mmap_mvar ~(mark : 'a mark) f xs args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ ->
None *)
ListLabels.fold_left2 xs args ~f:(monad_bind_var ~mark)
~init:
(Expr.einj
(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark)
some_constr option_enum mark)
let mmap_mvar ~(mark : 'a mark) f xs args =
(* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _
-> None *)
ListLabels.fold_left2 xs args ~f:(bind_var ~mark)
~init:
(Expr.einj
(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark)
some_constr option_enum mark)
let monad_map_var ~(mark : 'a mark) f x arg = monad_mmap_mvar f [x] [arg] ~mark
let map_var ~(mark : 'a mark) f x arg = mmap_mvar f [x] [arg] ~mark
let monad_map ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
monad_map_var f x arg ~mark
let map ~(mark : 'a mark) ~(var_name : string) f arg =
let x = Var.make var_name in
map_var f x arg ~mark
let monad_mmap ~(mark : 'a mark) ~(var_name : string) f args =
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
monad_mmap_mvar f vars args ~mark
let mmap ~(mark : 'a mark) ~(var_name : string) f args =
let vars =
ListLabels.mapi args ~f:(fun i _ ->
Var.make (Format.sprintf "%s_%i" var_name i))
in
mmap_mvar f vars args ~mark
let monad_error_on_empty
~(mark : 'a mark)
~(var_name : string)
?(toplevel = false)
arg =
let cases =
EnumConstructor.Map.of_seq
(List.to_seq
[
( 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*);
])
in
if toplevel then Expr.ematch arg option_enum cases mark
else monad_return ~mark (Expr.ematch arg option_enum cases mark)
let error_on_empty
~(mark : 'a mark)
~(var_name : string)
?(toplevel = false)
arg =
let cases =
EnumConstructor.Map.of_seq
(List.to_seq
[
( 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*);
])
in
if toplevel then Expr.ematch arg option_enum cases mark
else return ~mark (Expr.ematch arg option_enum cases mark)
end

View File

@ -36,77 +36,79 @@ val option_enum_config : typ EnumConstructor.Map.t
(** {2 Term building and management for the [option] monad}*)
val monad_return :
mark:'m mark -> ('a any, 'm mark) boxed_gexpr -> ('a, 'm mark) boxed_gexpr
module OptionMonad : sig
val return :
mark:'m mark -> ('a any, 'm mark) boxed_gexpr -> ('a, 'm mark) boxed_gexpr
val monad_empty : mark:'m mark -> ('a any, 'm mark) boxed_gexpr
val empty : mark:'m mark -> ('a any, 'm mark) boxed_gexpr
val monad_bind_var :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val bind_var :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val monad_bind :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val bind :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val monad_bind_cont :
mark:'m mark ->
var_name:string ->
(('a any, 'm mark) gexpr Var.t -> ('a, 'm mark) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val bind_cont :
mark:'m mark ->
var_name:string ->
(('a any, 'm mark) gexpr Var.t -> ('a, 'm mark) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val monad_mbind_mvar :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val mbind_mvar :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val monad_mbind :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val mbind :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val monad_mbind_cont :
mark:'m mark ->
var_name:string ->
(('a any, 'm mark) gexpr Var.t list -> ('a, 'm mark) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val mbind_cont :
mark:'m mark ->
var_name:string ->
(('a any, 'm mark) gexpr Var.t list -> ('a, 'm mark) boxed_gexpr) ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val monad_error_on_empty :
mark:'m mark ->
var_name:string ->
?toplevel:bool ->
((< exceptions : yes ; .. > as 'a), 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val error_on_empty :
mark:'m mark ->
var_name:string ->
?toplevel:bool ->
((< exceptions : yes ; .. > as 'a), 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val monad_map :
mark:'m mark ->
var_name:string ->
((< exceptions : no ; .. > as 'a), 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val map :
mark:'m mark ->
var_name:string ->
((< exceptions : no ; .. > as 'a), 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr
val monad_mmap_mvar :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val mmap_mvar :
mark:'m mark ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) gexpr Var.t list ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val monad_mmap :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
val mmap :
mark:'m mark ->
var_name:string ->
('a any, 'm mark) boxed_gexpr ->
('a, 'm mark) boxed_gexpr list ->
('a, 'm mark) boxed_gexpr
end

View File

@ -113,7 +113,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
match Marked.unmark e with
| EVar x ->
if (Var.Map.find x ctx.ctx_vars).info_pure then
Ast.monad_return (Expr.evar (trans_var ctx x) m) ~mark
Ast.OptionMonad.return (Expr.evar (trans_var ctx x) m) ~mark
else Expr.evar (trans_var ctx x) m
| EApp { f = EVar v, _; args = [(ELit LUnit, _)] } ->
(* Invariant: as users cannot write thunks, it can only come from prior
@ -121,7 +121,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
assert (not (Var.Map.find v ctx.ctx_vars).info_pure);
Expr.evar (trans_var ctx v) m
| EAbs { binder; tys = [(TLit TUnit, _)] } ->
(* this is to be used with Ast.monad_bind. *)
(* this is to be used with Ast.OptionMonad.bind. *)
let _, body = Bindlib.unmbind binder in
trans ctx body
| EAbs { binder; tys } ->
@ -141,7 +141,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
let body' = trans ctx' body in
let binder' = Expr.bind (Array.map Var.translate vars) body' in
Ast.monad_return ~mark (Expr.eabs binder' tys m)
Ast.OptionMonad.return ~mark (Expr.eabs binder' tys m)
| EDefault { excepts; just; cons } ->
let excepts' = List.map (trans ctx) excepts in
let just' = trans ctx just in
@ -155,11 +155,11 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
(Expr.eop Op.HandleDefaultOpt [TAny, pos; TAny, pos; TAny, pos] m')
[Expr.earray excepts' m; Expr.thunk_term just' m; Expr.thunk_term cons' m]
pos
| ELit l -> Ast.monad_return ~mark (Expr.elit l m)
| EEmptyError -> Ast.monad_empty ~mark
| ELit l -> Ast.OptionMonad.return ~mark (Expr.elit l m)
| EEmptyError -> Ast.OptionMonad.empty ~mark
| EErrorOnEmpty arg ->
let arg' = trans ctx arg in
Ast.monad_error_on_empty arg' ~mark ~toplevel:false
Ast.OptionMonad.error_on_empty arg' ~mark ~toplevel:false
~var_name:ctx.ctx_context_name
| EApp { f = EVar scope, _; args = [(EStruct { fields; name }, _)] }
when (Var.Map.find scope ctx.ctx_vars).is_scope ->
@ -167,7 +167,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
always return (or raise panic exceptions like AssertionFailed,
NoValueProvided or Conflict) a structure that can contain optionnal
elements. Hence, to call a scope, we don't need to use the monad bind. *)
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.evar (trans_var ctx scope) mark)
[
@ -182,10 +182,11 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
As every function of type [a -> b] but top-level scopes is built using
this function, returning a function of type [a -> b option], we should
use [Ast.monad_mbind]. *)
use [Ast.OptionMonad.mbind]. *)
let f_var = Var.make ctx.ctx_context_name in
Ast.monad_bind_var ~mark
(Ast.monad_mbind ~var_name:ctx.ctx_context_name (Expr.evar f_var mark)
Ast.OptionMonad.bind_var ~mark
(Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Expr.evar f_var mark)
(List.map (trans ctx) args)
~mark)
f_var (trans ctx f)
@ -193,8 +194,9 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
(* This occurs when calling a subscope function. The same encoding as the
one for [EApp (Var _) _] if the variable is not a scope works. *)
let f_var = Var.make ctx.ctx_context_name in
Ast.monad_bind_var ~mark
(Ast.monad_mbind ~var_name:ctx.ctx_context_name (Expr.evar f_var mark)
Ast.OptionMonad.bind_var ~mark
(Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Expr.evar f_var mark)
(List.map (trans ctx) args)
~mark)
f_var (trans ctx f)
@ -214,7 +216,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
ctx_context_name = Bindlib.name_of var;
}
in
Ast.monad_bind_var (trans ctx' body) var' (trans ctx arg) ~mark
Ast.OptionMonad.bind_var (trans ctx' body) var' (trans ctx arg) ~mark
| EApp { f = EApp { f = EOp { op = Op.Log _; _ }, _; args = _ }, _; _ } ->
Errors.raise_internal_error
"Parameter trace is incompatible with parameter avoid_exceptions: some \
@ -229,12 +231,13 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let f' =
Ast.monad_bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1; x2 |]
(Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name ~mark
(Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
~mark
(fun vars ->
Expr.eapp (Expr.evar f m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -244,20 +247,21 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
m))
(trans ctx f)
in
Ast.monad_mbind ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Expr.eop (trans_op Op.Fold) tys opmark)
[f'; Ast.monad_return ~mark (trans ctx init); trans ctx l]
[f'; Ast.OptionMonad.return ~mark (trans ctx init); trans ctx l]
~mark
| EApp { f = EOp { op = Op.Reduce; tys }, opmark; args = [f; init; l] } ->
let x1 = Var.make "f" in
let x2 = Var.make "init" in
let f' =
Ast.monad_bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1; x2 |]
(Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name ~mark
(Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
~mark
(fun vars ->
Expr.eapp (Expr.evar f m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -267,9 +271,9 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
m))
(trans ctx f)
in
Ast.monad_mbind ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind ~var_name:ctx.ctx_context_name
(Expr.eop (trans_op Op.Reduce) tys opmark)
[f'; Ast.monad_return ~mark (trans ctx init); trans ctx l]
[f'; Ast.OptionMonad.return ~mark (trans ctx init); trans ctx l]
~mark
| EApp { f = EOp { op = Op.Map; tys }, opmark; args = [f; l] } ->
(* The funtion [f] has type [a -> option b], but Map needs a function of
@ -277,12 +281,13 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
option -> option b]. *)
let x1 = Var.make "f" in
let f' =
Ast.monad_bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1 |]
(Ast.monad_mbind_cont ~mark ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind_cont ~mark
~var_name:ctx.ctx_context_name
(fun vars ->
Expr.eapp (Expr.evar f m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -292,9 +297,9 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
m))
(trans ctx f)
in
Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun vars ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.eop (trans_op Op.Map) tys opmark)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -308,14 +313,15 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
the result. *)
let x1 = Var.make ctx.ctx_context_name in
let f' =
Ast.monad_bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun f ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eabs
(Expr.bind [| x1 |]
(Ast.monad_error_on_empty ~toplevel:true ~mark
(Ast.OptionMonad.error_on_empty ~toplevel:true ~mark
~var_name:ctx.ctx_context_name
(Ast.monad_mbind_cont ~mark ~var_name:ctx.ctx_context_name
(Ast.OptionMonad.mbind_cont ~mark
~var_name:ctx.ctx_context_name
(fun vars ->
Expr.eapp (Expr.evar f m)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -325,9 +331,9 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
m))
(trans ctx f)
in
Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun vars ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.eapp
(Expr.eop (trans_op Op.Filter) tys opmark)
(ListLabels.map vars ~f:(fun v -> Expr.evar v m))
@ -345,7 +351,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
Print.operator op
| EApp { f = EOp { op; tys }, opmark; args } ->
let res =
Ast.monad_mmap ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mmap ~var_name:ctx.ctx_context_name
(Expr.eop (trans_op op) tys opmark)
(List.map (trans ctx) args)
~mark
@ -377,58 +383,64 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
Expr.eabs binder tys m
| _ -> assert false)
in
Ast.monad_bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
(fun e -> Expr.ematch (Expr.evar e m) name cases m)
(trans ctx e) ~mark
| EArray args ->
Ast.monad_mbind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont ~mark ~var_name:ctx.ctx_context_name
(fun vars ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.earray
(List.map (fun v -> Ast.monad_return ~mark (Expr.evar v m)) vars)
(List.map
(fun v -> Ast.OptionMonad.return ~mark (Expr.evar v m))
vars)
mark))
(List.map (trans ctx) args)
| EStruct { name; fields } ->
let fields_name, fields = List.split (StructField.Map.bindings fields) in
Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun xs ->
let fields =
ListLabels.fold_right2 fields_name
(List.map (fun x -> Ast.monad_return ~mark (Expr.evar x mark)) xs)
(List.map
(fun x -> Ast.OptionMonad.return ~mark (Expr.evar x mark))
xs)
~f:StructField.Map.add ~init:StructField.Map.empty
in
Ast.monad_return ~mark (Expr.estruct name fields mark))
Ast.OptionMonad.return ~mark (Expr.estruct name fields mark))
(List.map (trans ctx) fields)
~mark
| EIfThenElse { cond; etrue; efalse } ->
Ast.monad_bind_cont ~mark ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~mark ~var_name:ctx.ctx_context_name
(fun cond ->
Expr.eifthenelse (Expr.evar cond mark) (trans ctx etrue)
(trans ctx efalse) mark)
(trans ctx cond)
| EInj { name; cons; e } ->
Ast.monad_bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
(fun e ->
Ast.monad_return ~mark (Expr.einj (Expr.evar e mark) cons name mark))
Ast.OptionMonad.return ~mark
(Expr.einj (Expr.evar e mark) cons name mark))
(trans ctx e) ~mark
| EStructAccess { name; e; field } ->
Ast.monad_bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
(fun e -> Expr.estructaccess (Expr.evar e mark) field name mark)
(trans ctx e) ~mark
| ETuple args ->
Ast.monad_mbind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.mbind_cont ~var_name:ctx.ctx_context_name
(fun xs ->
Ast.monad_return ~mark
Ast.OptionMonad.return ~mark
(Expr.etuple (List.map (fun x -> Expr.evar x mark) xs) mark))
(List.map (trans ctx) args)
~mark
| ETupleAccess { e; index; size } ->
Ast.monad_bind_cont ~var_name:ctx.ctx_context_name
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
(fun e -> Expr.etupleaccess (Expr.evar e mark) index size mark)
(trans ctx e) ~mark
| EAssert e ->
Ast.monad_bind_cont ~var_name:ctx.ctx_context_name
(fun e -> Ast.monad_return ~mark (Expr.eassert (Expr.evar e mark) mark))
Ast.OptionMonad.bind_cont ~var_name:ctx.ctx_context_name
(fun e ->
Ast.OptionMonad.return ~mark (Expr.eassert (Expr.evar e mark) mark))
(trans ctx e) ~mark
| EApp _ ->
Errors.raise_spanned_error (Expr.pos e)
@ -548,7 +560,7 @@ let rec trans_scope_let (ctx : typed ctx) (s : typed D.expr scope_let) =
let scope_let_next = Bindlib.bind_var next_var next_body in
let scope_let_expr =
Expr.Box.lift
@@ Ast.monad_error_on_empty ~mark ~toplevel:true
@@ Ast.OptionMonad.error_on_empty ~mark ~toplevel:true
~var_name:ctx.ctx_context_name
(trans { ctx with ctx_context_name = Bindlib.name_of next_var } e)
in

View File

@ -341,13 +341,8 @@ let rec evaluate_operator
let valid_exceptions =
ListLabels.filter exps ~f:(function
| EInj { name; cons; _ }, _
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.some_constr ->
true
| EInj { name; cons; _ }, _
when EnumName.equal name Definitions.option_enum
&& EnumConstructor.equal cons Definitions.none_constr ->
false
when EnumName.equal name Definitions.option_enum ->
EnumConstructor.equal cons Definitions.some_constr
| _ -> err ())
in

View File

@ -213,7 +213,9 @@ let compare (type a1 a2) (t1 : a1 t) (t2 : a2 t) =
| Eq_mon_mon, Eq_mon_mon
| Eq_dat_dat, Eq_dat_dat
| Eq_dur_dur, Eq_dur_dur
| Fold, Fold |HandleDefault, HandleDefault | HandleDefaultOpt, HandleDefaultOpt -> 0
| Fold, Fold
| HandleDefault, HandleDefault
| HandleDefaultOpt, HandleDefaultOpt -> 0
| Not, _ -> -1 | _, Not -> 1
| Length, _ -> -1 | _, Length -> 1
| GetDay, _ -> -1 | _, GetDay -> 1

View File

@ -536,8 +536,7 @@ let typ ctx = typ (Some ctx)
let expr_debug ?debug = expr_aux ?debug None Bindlib.empty_ctxt
let expr ?debug ctx = expr_aux ?debug (Some ctx) Bindlib.empty_ctxt
let scope_let_kind ?(debug = true) _ctx fmt k =
let _ = debug in
let scope_let_kind ?debug:(_debug = true) _ctx fmt k =
match k with
| DestructuringInputStruct -> keyword fmt "get"
| ScopeVarDefinition -> keyword fmt "set"

View File

@ -526,26 +526,23 @@ and typecheck_expr_top_down :
in
Expr.estructaccess e_struct' field name mark
| A.EInj { name; cons; e = e_enum }
when Definitions.EnumName.compare name Definitions.option_enum = 0
&& Definitions.EnumConstructor.compare cons Definitions.some_constr = 0
->
let cell_type = unionfind (TAny (Any.fresh ())) in
let mark = mark_with_tau_and_unify (unionfind (TOption cell_type)) in
let e_enum' =
typecheck_expr_top_down ~leave_unresolved ctx env cell_type e_enum
in
Expr.einj e_enum' cons name mark
| A.EInj { name; cons; e = e_enum }
when Definitions.EnumName.compare name Definitions.option_enum = 0
&& Definitions.EnumConstructor.compare cons Definitions.none_constr = 0
->
let cell_type = unionfind (TAny (Any.fresh ())) in
let mark = mark_with_tau_and_unify (unionfind (TOption cell_type)) in
let e_enum' =
typecheck_expr_top_down ~leave_unresolved ctx env (unionfind (TLit TUnit))
e_enum
in
Expr.einj e_enum' cons name mark
when Definitions.EnumName.equal name Definitions.option_enum ->
if Definitions.EnumConstructor.equal cons Definitions.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' =
typecheck_expr_top_down ~leave_unresolved ctx env cell_type e_enum
in
Expr.einj e_enum' cons name mark
else
(* None constructor *)
let cell_type = unionfind (TAny (Any.fresh ())) in
let mark = mark_with_tau_and_unify (unionfind (TOption cell_type)) in
let e_enum' =
typecheck_expr_top_down ~leave_unresolved ctx env
(unionfind (TLit TUnit)) e_enum
in
Expr.einj e_enum' cons name mark
| A.EInj { name; cons; e = e_enum } ->
let mark = mark_with_tau_and_unify (unionfind (TEnum name)) in
let e_enum' =

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff