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

Porting the interpreter to the marked AST

Browse Source
This commit is contained in:
Louis Gesbert 2022-06-23 14:06:11 +02:00
parent 6cc2e9a07b
commit 4eb5933ad0
23 changed files with 729 additions and 633 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
compiler/dcalc/ast.ml
View File

@ -250,7 +250,7 @@ let with_ty (type m) (ty : Infer.unionfind_typ) (x : ('a, m) marked) :
| Typed m -> Typed { m with ty })
(Marked.unmark x)
let evar v mark = Bindlib.box_apply (fun v' -> v', mark) (Bindlib.box_var v)
let evar v mark = Bindlib.box_apply (Marked.mark mark) (Bindlib.box_var v)
let etuple args s mark =
Bindlib.box_apply (fun args -> ETuple (args, s), mark) (Bindlib.box_list args)
@ -395,22 +395,22 @@ let map_exprs_in_scopes ~f ~varf scopes =
let new_next = Bindlib.bind_var (varf var_next) acc in
Bindlib.box_apply2
(fun scope_body_expr scope_next ->
ScopeDef {
ScopeDef
{
scope_def with
scope_body = { scope_def.scope_body with scope_body_expr };
scope_next;
})
new_scope_body_expr
new_next)
~init:(Bindlib.box Nil)
scopes
new_scope_body_expr new_next)
~init:(Bindlib.box Nil) scopes
type 'm var = 'm expr Bindlib.var
type 'm vars = 'm expr Bindlib.mvar
let new_var s = Bindlib.new_var (fun x -> EVar x) s
module Var = struct
type t = V : 'm var -> t
type t = V : 'a expr Bindlib.var -> t
(* We use this trivial GADT to make the 'm parameter disappear under an
existential. It's fine for a use as keys only.
(bindlib defines [any_var] similarly but it's not exported)
@ -418,7 +418,7 @@ module Var = struct
let t v = V v
let make (s : string) : t = V (new_var s)
let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)
let compare (V x) (V y) = Bindlib.compare_vars x y
end
@ -426,50 +426,89 @@ end
module VarSet = Set.Make (Var)
module VarMap = Map.Make (Var)
(* let rec free_vars_expr (e : untyped marked_expr) : VarSet.t = match
Marked.unmark e with | EVar v -> VarSet.singleton v | ETuple (es, _) | EArray
es -> es |> List.map free_vars_expr |> List.fold_left VarSet.union
VarSet.empty | ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 |
EInj (e1, _, _, _) -> free_vars_expr e1 | EApp (e1, es) | EMatch (e1, es, _)
-> e1 :: es |> List.map free_vars_expr |> List.fold_left VarSet.union
VarSet.empty | EDefault (es, ejust, econs) -> ejust :: econs :: es |>
List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EOp _ |
ELit _ -> VarSet.empty | EIfThenElse (e1, e2, e3) -> [e1; e2; e3] |> List.map
free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EAbs (binder, _)
-> let vs, body = Bindlib.unmbind binder in Array.fold_right VarSet.remove vs
(free_vars_expr body)
(** {[
let rec free_vars_expr (e : untyped marked_expr) : VarSet.t =
match Marked.unmark e with
| EVar v -> VarSet.singleton v
| ETuple (es, _) | EArray es ->
es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| ETupleAccess (e1, _, _, _)
| EAssert e1
| ErrorOnEmpty e1
| EInj (e1, _, _, _) ->
free_vars_expr e1
| EApp (e1, es) | EMatch (e1, es, _) ->
e1 :: es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EDefault (es, ejust, econs) ->
ejust :: econs :: es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EOp _ | ELit _ -> VarSet.empty
| EIfThenElse (e1, e2, e3) ->
[e1; e2; e3] |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EAbs (binder, _) ->
let vs, body = Bindlib.unmbind binder in
Array.fold_right VarSet.remove vs (free_vars_expr body)
module VarMap = Map.Make (Var(struct type t = untyped end)) module VarSet =
Set.Make (Var(struct type t = untyped end))
module VarMap = Map.Make (Var (struct
type t = untyped
end))
let rec free_vars_expr (e : expr) : VarSet.t = match Marked.unmark e with |
EVar (v, _) -> VarSet.singleton v | ETuple (es, _) | EArray es -> es |>
List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty |
ETupleAccess (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 | EInj (e1, _, _,
_) -> free_vars_expr e1 | EApp (e1, es) | EMatch (e1, es, _) -> e1 :: es |>
List.map free_vars_expr |> List.fold_left VarSet.union VarSet.empty |
EDefault (es, ejust, econs) -> ejust :: econs :: es |> List.map
free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EOp _ | ELit _
-> VarSet.empty | EIfThenElse (e1, e2, e3) -> [e1; e2; e3] |> List.map
free_vars_expr |> List.fold_left VarSet.union VarSet.empty | EAbs ((binder,
_), _) -> let vs, body = Bindlib.unmbind binder in Array.fold_right
VarSet.remove vs (free_vars_expr body)
module VarSet = Set.Make (Var (struct
type t = untyped
end))
let rec free_vars_expr (e : expr) : VarSet.t =
match Marked.unmark e with
| EVar (v, _) -> VarSet.singleton v
| ETuple (es, _) | EArray es ->
es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| ETupleAccess (e1, _, _, _)
| EAssert e1
| ErrorOnEmpty e1
| EInj (e1, _, _, _) ->
free_vars_expr e1
| EApp (e1, es) | EMatch (e1, es, _) ->
e1 :: es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EDefault (es, ejust, econs) ->
ejust :: econs :: es |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EOp _ | ELit _ -> VarSet.empty
| EIfThenElse (e1, e2, e3) ->
[e1; e2; e3] |> List.map free_vars_expr
|> List.fold_left VarSet.union VarSet.empty
| EAbs ((binder, _), _) ->
let vs, body = Bindlib.unmbind binder in
Array.fold_right VarSet.remove vs (free_vars_expr body)
let rec free_vars_scope_body_expr (scope_lets : expr scope_body_expr) :
VarSet.t = match scope_lets with | Result e -> free_vars_expr e | ScopeLet {
scope_let_expr = e; scope_let_next = next; _ } -> let v, body =
Bindlib.unbind next in VarSet.union (free_vars_expr e) (VarSet.remove v
(free_vars_scope_body_expr body))
VarSet.t =
match scope_lets with
| Result e -> free_vars_expr e
| ScopeLet { scope_let_expr = e; scope_let_next = next; _ } ->
let v, body = Bindlib.unbind next in
VarSet.union (free_vars_expr e)
(VarSet.remove v (free_vars_scope_body_expr body))
let free_vars_scope_body (scope_body : expr scope_body) : VarSet.t = let {
scope_body_expr = binder; _ } = scope_body in let v, body = Bindlib.unbind
binder in VarSet.remove v (free_vars_scope_body_expr body)
let free_vars_scope_body (scope_body : expr scope_body) : VarSet.t =
let { scope_body_expr = binder; _ } = scope_body in
let v, body = Bindlib.unbind binder in
VarSet.remove v (free_vars_scope_body_expr body)
let rec free_vars_scopes (scopes : expr scopes) : VarSet.t = match scopes
with | Nil -> VarSet.empty | ScopeDef { scope_body = body; scope_next = next;
_ } -> let v, next = Bindlib.unbind next in VarSet.union (VarSet.remove v
(free_vars_scopes next)) (free_vars_scope_body body) (* type vars = expr
Bindlib.mvar *) *)
let rec free_vars_scopes (scopes : expr scopes) : VarSet.t =
match scopes with
| Nil -> VarSet.empty
| ScopeDef { scope_body = body; scope_next = next; _ } ->
let v, next = Bindlib.unbind next in
VarSet.union
(VarSet.remove v (free_vars_scopes next))
(free_vars_scope_body body)
(* type vars = expr Bindlib.mvar *)
]}*)
let make_var ((x, mark) : ('m expr Bindlib.var, 'm) marked) :
'm marked_expr Bindlib.box =
@ -746,9 +785,18 @@ let rec unfold_scopes
mark_witness main_scope)
scope_pos
let rec find_scope name vars = function
| Nil -> raise Not_found
| ScopeDef {scope_name; scope_body; _} when scope_name = name ->
List.rev vars, scope_body
| ScopeDef {scope_next; _} ->
let var, next = Bindlib.unbind scope_next in
find_scope name (var :: vars) next
let build_whole_program_expr (p : 'm program) (main_scope : ScopeName.t) =
let _, main_scope_body = find_scope main_scope [] p.scopes in
unfold_scopes ~box_expr ~make_abs ~make_let_in p.decl_ctx p.scopes
p.mark_witness (ScopeName main_scope)
(get_scope_body_mark main_scope_body) (ScopeName main_scope)
let rec expr_size (e : 'm marked_expr) : int =
match Marked.unmark e with

10
compiler/dcalc/ast.mli
View File

@ -229,6 +229,7 @@ type 'm program = { decl_ctx : decl_ctx; scopes : ('m expr, 'm) scopes }
(** {2 Manipulation of marks} *)
val no_mark: 'm mark -> 'm mark
val mark_pos: 'm mark -> Pos.t
val pos: ('a, 'm) marked -> Pos.t
val ty: ('a, typed) marked -> typ
val with_ty: Infer.unionfind_typ -> ('a, 'm) marked -> ('a, typed) marked
@ -402,12 +403,11 @@ type 'm var = 'm expr Bindlib.var
val new_var: string -> 'm var
(** {2 Boxed term constructors} *)
module Var : sig
type t
val t: 'm var -> t
val make : string -> t
val t: 'm expr Bindlib.var -> t
val get: t -> 'm expr Bindlib.var
val compare : t -> t -> int
end
@ -422,7 +422,9 @@ module VarSet : Set.S with type elt = Var.t
(* type vars = expr Bindlib.mvar *)
val make_var : ('m expr Bindlib.var, 'm) marked -> 'm marked_expr Bindlib.box
val make_var : ('m var, 'm) marked -> 'm marked_expr Bindlib.box
(** {2 Boxed term constructors} *)
type ('e, 'm) make_abs_sig =
'e Bindlib.mvar ->

127
compiler/dcalc/interpreter.ml
View File

@ -30,27 +30,29 @@ let log_indent = ref 0
let rec evaluate_operator
(ctx : Ast.decl_ctx)
(op : A.operator Marked.pos)
(args : 'm A.marked_expr list) : 'm A.marked_expr =
(op : A.operator)
(pos : Pos.t)
(args : 'm A.marked_expr list) : 'm A.expr =
(* Try to apply [div] and if a [Division_by_zero] exceptions is catched, use
[op] to raise multispanned errors. *)
let apply_div_or_raise_err (div : unit -> 'm A.expr) (op : A.operator Marked.pos)
let apply_div_or_raise_err (div : unit -> 'm A.expr)
: 'm A.expr =
try div ()
with Division_by_zero ->
Errors.raise_multispanned_error
[
Some "The division operator:", Marked.get_mark op;
Some "The division operator:", pos;
Some "The null denominator:", Ast.pos (List.nth args 1);
]
"division by zero at runtime"
in
let get_binop_args_pos (arg0::arg1::_ : ('m A.expr * 'm) list) :
(string option * Pos.t) list =
let get_binop_args_pos = function
| (arg0::arg1::_ : 'm A.marked_expr list) ->
[
None, Ast.pos arg0;
None, Ast.pos arg1;
]
| _ -> assert false
in
(* Try to apply [cmp] and if a [UncomparableDurations] exceptions is catched,
use [args] to raise multispanned errors. *)
@ -63,8 +65,7 @@ let rec evaluate_operator
"Cannot compare together durations that cannot be converted to a \
precise number of days"
in
Marked.same_mark_as
(match Marked.unmark op, List.map Marked.unmark args with
match op, List.map Marked.unmark args with
| A.Ternop A.Fold, [_f; _init; EArray es] ->
Marked.unmark
(List.fold_left
@ -85,7 +86,7 @@ let rec evaluate_operator
| A.Binop (A.Mult KInt), [ELit (LInt i1); ELit (LInt i2)] ->
A.ELit (LInt Runtime.(i1 *! i2))
| A.Binop (A.Div KInt), [ELit (LInt i1); ELit (LInt i2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2))) op
apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2)))
| A.Binop (A.Add KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LRat Runtime.(i1 +& i2))
| A.Binop (A.Sub KRat), [ELit (LRat i1); ELit (LRat i2)] ->
@ -93,7 +94,7 @@ let rec evaluate_operator
| A.Binop (A.Mult KRat), [ELit (LRat i1); ELit (LRat i2)] ->
A.ELit (LRat Runtime.(i1 *& i2))
| A.Binop (A.Div KRat), [ELit (LRat i1); ELit (LRat i2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2))) op
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2)))
| A.Binop (A.Add KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
A.ELit (LMoney Runtime.(m1 +$ m2))
| A.Binop (A.Sub KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
@ -101,7 +102,7 @@ let rec evaluate_operator
| A.Binop (A.Mult KMoney), [ELit (LMoney m1); ELit (LRat m2)] ->
A.ELit (LMoney Runtime.(m1 *$ m2))
| A.Binop (A.Div KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2))) op
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2)))
| A.Binop (A.Add KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
A.ELit (LDuration Runtime.(d1 +^ d2))
| A.Binop (A.Sub KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
@ -118,7 +119,6 @@ let rec evaluate_operator
Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot divide durations that cannot be converted to a precise \
number of days")
op
| A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] ->
A.ELit (LDuration Runtime.(d1 *^ i1))
| A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] ->
@ -180,7 +180,7 @@ let rec evaluate_operator
(try
List.for_all2
(fun e1 e2 ->
match Marked.unmark (evaluate_operator ctx op [e1; e2]) with
match evaluate_operator ctx op pos [e1; e2] with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
@ -194,7 +194,7 @@ let rec evaluate_operator
&& List.for_all2
(fun e1 e2 ->
match
Marked.unmark (evaluate_operator ctx op [e1; e2])
evaluate_operator ctx op pos [e1; e2]
with
| A.ELit (LBool b) -> b
| _ -> assert false
@ -207,7 +207,7 @@ let rec evaluate_operator
(try
en1 = en2 && i1 = i2
&&
match Marked.unmark (evaluate_operator ctx op [e1; e2]) with
match evaluate_operator ctx op pos [e1; e2] with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
@ -216,8 +216,7 @@ let rec evaluate_operator
A.ELit (LBool false) (* comparing anything else return false *)
| A.Binop A.Neq, [_; _] -> (
match
Marked.unmark
(evaluate_operator ctx (Marked.same_mark_as (A.Binop A.Eq) op) args)
evaluate_operator ctx (A.Binop A.Eq) pos args
with
| A.ELit (A.LBool b) -> A.ELit (A.LBool (not b))
| _ -> assert false (*should not happen *))
@ -240,7 +239,7 @@ let rec evaluate_operator
| A.ELit (A.LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Marked.get_mark (List.nth args 0))
(A.pos (List.nth args 0))
"This predicate evaluated to something else than a boolean \
(should not happen if the term was well-typed)")
es)
@ -285,7 +284,7 @@ let rec evaluate_operator
let expr_str =
Format.asprintf "%a"
(Print.format_expr ctx ~debug:false)
(e', Pos.no_pos)
(List.hd args)
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
@ -294,7 +293,6 @@ let rec evaluate_operator
in
Cli.with_style [ANSITerminal.green] "%s" expr_str)
| PosRecordIfTrueBool -> (
let pos = Marked.get_mark op in
match pos <> Pos.no_pos, e' with
| true, ELit (LBool true) ->
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) ""
@ -316,24 +314,23 @@ let rec evaluate_operator
| A.Unop _, [ELit LEmptyError] -> A.ELit LEmptyError
| _ ->
Errors.raise_multispanned_error
([Some "Operator:", Marked.get_mark op]
([Some "Operator:", pos]
@ List.mapi
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1)
(Print.format_expr ctx ~debug:true)
arg),
Marked.get_mark arg ))
A.pos arg ))
args)
"Operator applied to the wrong arguments\n\
(should not happen if the term was well-typed)")
op
(should not happen if the term was well-typed)"
and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
'm A.marked_expr =
match Marked.unmark e with
| EVar _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"free variable found at evaluation (should not happen if term was \
well-typed"
| EApp (e1, args) -> (
@ -345,17 +342,17 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
evaluate_expr ctx
(Bindlib.msubst binder (Array.of_list (List.map Marked.unmark args)))
else
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder)
(List.length args)
| EOp op ->
Marked.same_mark_as
(Marked.unmark (evaluate_operator ctx (Marked.same_mark_as op e1) args))
(evaluate_operator ctx op (A.pos e) args)
e
| ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed")
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
@ -373,19 +370,19 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
| Some s, Some s' when s = s' -> ()
| _ ->
Errors.raise_multispanned_error
[None, Marked.get_mark e; None, Marked.get_mark e1]
[None, A.pos e; None, A.pos e1]
"Error during tuple access: not the same structs (should not happen \
if the term was well-typed)");
match List.nth_opt es n with
| Some e' -> e'
| None ->
Errors.raise_spanned_error (Marked.get_mark e1)
Errors.raise_spanned_error (A.pos e1)
"The tuple has %d components but the %i-th element was requested \
(should not happen if the term was well-type)"
(List.length es) n)
| ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark e1)
Errors.raise_spanned_error (A.pos e1)
"The expression %a should be a tuple with %d components but is not \
(should not happen if the term was well-typed)"
(Print.format_expr ctx ~debug:true)
@ -400,14 +397,14 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
| A.EInj (e1, n, e_name', _) ->
if e_name <> e_name' then
Errors.raise_multispanned_error
[None, Marked.get_mark e; None, Marked.get_mark e1]
[None, A.pos e; None, A.pos e1]
"Error during match: two different enums found (should not happend \
if the term was well-typed)";
let es_n =
match List.nth_opt es n with
| Some es_n -> es_n
| None ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"sum type index error (should not happend if the term was \
well-typed)"
in
@ -415,7 +412,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
evaluate_expr ctx new_e
| A.ELit A.LEmptyError -> Marked.same_mark_as (A.ELit A.LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark e1)
Errors.raise_spanned_error (A.pos e1)
"Expected a term having a sum type as an argument to a match (should \
not happend if the term was well-typed")
| EDefault (exceptions, just, cons) -> (
@ -429,7 +426,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
| ELit (LBool true) -> evaluate_expr ctx cons
| ELit (LBool false) -> Marked.same_mark_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"Default justification has not been reduced to a boolean at \
evaluation (should not happen if the term was well-typed")
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
@ -438,7 +435,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
(List.map
(fun except ->
( Some "This consequence has a valid justification:",
Marked.get_mark except ))
A.pos except ))
(List.filter (fun sub -> not (is_empty_error sub)) exceptions))
"There is a conflict between multiple valid consequences for assigning \
the same variable.")
@ -448,7 +445,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
| ELit (LBool false) -> evaluate_expr ctx ef
| ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark cond)
Errors.raise_spanned_error (A.pos cond)
"Expected a boolean literal for the result of this condition (should \
not happen if the term was well-typed)")
| EArray es ->
@ -459,7 +456,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
| ErrorOnEmpty e' ->
let e' = evaluate_expr ctx e' in
if Marked.unmark e' = A.ELit LEmptyError then
Errors.raise_spanned_error (Marked.get_mark e')
Errors.raise_spanned_error (A.pos e')
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
else e'
@ -470,45 +467,64 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : 'm A.marked_expr) :
match Marked.unmark e' with
| Ast.ErrorOnEmpty
( EApp
( (Ast.EOp (Binop op), pos_op),
( (Ast.EOp (Binop op), _),
[((ELit _, _) as e1); ((ELit _, _) as e2)] ),
_ )
| EApp
( (Ast.EOp (Ast.Unop (Ast.Log _)), _),
[
( Ast.EApp
( (Ast.EOp (Binop op), pos_op),
( (Ast.EOp (Binop op), _),
[((ELit _, _) as e1); ((ELit _, _) as e2)] ),
_ );
] )
| EApp
( (Ast.EOp (Binop op), pos_op),
( (Ast.EOp (Binop op), _),
[((ELit _, _) as e1); ((ELit _, _) as e2)] ) ->
Errors.raise_spanned_error (Marked.get_mark e')
Errors.raise_spanned_error (A.pos e')
"Assertion failed: %a %a %a"
(Print.format_expr ctx ~debug:false)
e1 Print.format_binop (op, pos_op)
e1 Print.format_binop op
(Print.format_expr ctx ~debug:false)
e2
| _ ->
Cli.debug_format "%a" (Print.format_expr ctx) e';
Errors.raise_spanned_error (Marked.get_mark e') "Assertion failed")
Errors.raise_spanned_error (A.pos e') "Assertion failed")
| ELit LEmptyError -> Marked.same_mark_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error (Marked.get_mark e')
Errors.raise_spanned_error (A.pos e')
"Expected a boolean literal for the result of this assertion (should \
not happen if the term was well-typed)")
(** {1 API} *)
let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Marked.pos) :
(Uid.MarkedString.info * Ast.expr Marked.pos) list =
match Marked.unmark (evaluate_expr ctx e) with
| Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _)]) -> (
let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in
let interpret_program: 'm. Ast.decl_ctx -> 'm Ast.marked_expr -> (Uid.MarkedString.info * 'm Ast.marked_expr) list =
fun
(ctx : Ast.decl_ctx) (e : 'm Ast.marked_expr) :
(Uid.MarkedString.info * 'm Ast.marked_expr) list ->
match evaluate_expr ctx e with
| Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _) as targs]), mark_e ->
begin
let application_term =
List.map (fun ty ->
Ast.empty_thunked_term (A.map_mark (fun pos -> pos)
(fun _ -> A.Infer.ast_to_typ ty) mark_e))
taus
in
let to_interpret =
( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in), Pos.no_pos]),
Pos.no_pos )
( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in),
A.fold_marks
(fun pos_l -> List.hd pos_l)
(fun _ -> A.Infer.ast_to_typ targs)
(List.map Marked.get_mark application_term)
]),
A.map_mark (fun pos -> pos)
(fun ty -> match UnionFind.get ty with
| A.Infer.TArrow (_, t_out), _ -> t_out
| _ ->
Errors.raise_spanned_error (A.pos e)
"(bug) Result of interpretation doesn't have the expected type")
mark_e )
in
match Marked.unmark (evaluate_expr ctx to_interpret) with
| Ast.ETuple (args, Some s_out) ->
@ -519,10 +535,11 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Marked.pos) :
in
List.map2 (fun arg var -> var, arg) args s_out_fields
| _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"The interpretation of a program should always yield a struct \
corresponding to the scope variables")
corresponding to the scope variables"
end
| _ ->
Errors.raise_spanned_error (Marked.get_mark e)
Errors.raise_spanned_error (A.pos e)
"The interpreter can only interpret terms starting with functions having \
thunked arguments"

258
compiler/lcalc/ast.ml
View File

@ -28,128 +28,99 @@ type lit =
type except = ConflictError | EmptyError | NoValueProvided | Crash
type marked_expr = expr Marked.pos
type 'm mark = 'm D.mark
and expr =
| EVar of expr Bindlib.var
| ETuple of marked_expr list * D.StructName.t option
type 'm marked_expr = ('m expr, 'm) D.marked
and 'm expr =
| EVar of 'm expr Bindlib.var
| ETuple of 'm marked_expr list * D.StructName.t option
(** The [MarkedString.info] is the former struct field name*)
| ETupleAccess of
marked_expr * int * D.StructName.t option * D.typ Marked.pos list
'm marked_expr * int * D.StructName.t option * D.typ Marked.pos list
(** The [MarkedString.info] is the former struct field name *)
| EInj of marked_expr * int * D.EnumName.t * D.typ Marked.pos list
| EInj of 'm marked_expr * int * D.EnumName.t * D.typ Marked.pos list
(** The [MarkedString.info] is the former enum case name *)
| EMatch of marked_expr * marked_expr list * D.EnumName.t
| EMatch of 'm marked_expr * 'm marked_expr list * D.EnumName.t
(** The [MarkedString.info] is the former enum case name *)
| EArray of marked_expr list
| EArray of 'm marked_expr list
| ELit of lit
| EAbs of (expr, marked_expr) Bindlib.mbinder * D.typ Marked.pos list
| EApp of marked_expr * marked_expr list
| EAssert of marked_expr
| EAbs of ('m expr, 'm marked_expr) Bindlib.mbinder * D.typ Marked.pos list
| EApp of 'm marked_expr * 'm marked_expr list
| EAssert of 'm marked_expr
| EOp of D.operator
| EIfThenElse of marked_expr * marked_expr * marked_expr
| EIfThenElse of 'm marked_expr * 'm marked_expr * 'm marked_expr
| ERaise of except
| ECatch of marked_expr * except * marked_expr
| ECatch of 'm marked_expr * except * 'm marked_expr
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : expr Dcalc.Ast.scopes }
type 'm program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : ('m expr, 'm) Dcalc.Ast.scopes }
let evar (v : expr Bindlib.var) (pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun v' -> v', pos) (Bindlib.box_var v)
(* <copy-paste from dcalc/ast.ml> *)
let etuple
(args : expr Marked.pos Bindlib.box list)
(s : Dcalc.Ast.StructName.t option)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun args -> ETuple (args, s), pos) (Bindlib.box_list args)
let evar v mark = Bindlib.box_apply (Marked.mark mark) (Bindlib.box_var v)
let etupleaccess
(e1 : expr Marked.pos Bindlib.box)
(i : int)
(s : Dcalc.Ast.StructName.t option)
(typs : Dcalc.Ast.typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), pos) e1
let etuple args s mark =
Bindlib.box_apply (fun args -> ETuple (args, s), mark) (Bindlib.box_list args)
let einj
(e1 : expr Marked.pos Bindlib.box)
(i : int)
(e_name : Dcalc.Ast.EnumName.t)
(typs : Dcalc.Ast.typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), pos) e1
let etupleaccess e1 i s typs mark =
Bindlib.box_apply (fun e1 -> ETupleAccess (e1, i, s, typs), mark) e1
let ematch
(arg : expr Marked.pos Bindlib.box)
(arms : expr Marked.pos Bindlib.box list)
(e_name : Dcalc.Ast.EnumName.t)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
let einj e1 i e_name typs mark =
Bindlib.box_apply (fun e1 -> EInj (e1, i, e_name, typs), mark) e1
let ematch arg arms e_name mark =
Bindlib.box_apply2
(fun arg arms -> EMatch (arg, arms, e_name), pos)
(fun arg arms -> EMatch (arg, arms, e_name), mark)
arg (Bindlib.box_list arms)
let earray (args : expr Marked.pos Bindlib.box list) (pos : Pos.t) :
expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun args -> EArray args, pos) (Bindlib.box_list args)
let earray args mark =
Bindlib.box_apply (fun args -> EArray args, mark) (Bindlib.box_list args)
let elit (l : lit) (pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box (ELit l, pos)
let elit l mark = Bindlib.box (ELit l, mark)
let eabs
(binder : (expr, expr Marked.pos) Bindlib.mbinder Bindlib.box)
(typs : Dcalc.Ast.typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun binder -> EAbs (binder, typs), pos) binder
let eabs binder typs mark =
Bindlib.box_apply (fun binder -> EAbs (binder, typs), mark) binder
let eapp
(e1 : expr Marked.pos Bindlib.box)
(args : expr Marked.pos Bindlib.box list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
let eapp e1 args mark =
Bindlib.box_apply2
(fun e1 args -> EApp (e1, args), pos)
(fun e1 args -> EApp (e1, args), mark)
e1 (Bindlib.box_list args)
let eassert (e1 : expr Marked.pos Bindlib.box) (pos : Pos.t) :
expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun e1 -> EAssert e1, pos) e1
let eassert e1 mark = Bindlib.box_apply (fun e1 -> EAssert e1, mark) e1
let eop (op : Dcalc.Ast.operator) (pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box (EOp op, pos)
let eop op mark = Bindlib.box (EOp op, mark)
let eraise (e1 : except) (pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box (ERaise e1, pos)
let ecatch
(e1 : expr Marked.pos Bindlib.box)
(exn : except)
(e2 : expr Marked.pos Bindlib.box)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), pos) e1 e2
let eifthenelse
(e1 : expr Marked.pos Bindlib.box)
(e2 : expr Marked.pos Bindlib.box)
(e3 : expr Marked.pos Bindlib.box)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
let eifthenelse e1 e2 e3 pos =
Bindlib.box_apply3 (fun e1 e2 e3 -> EIfThenElse (e1, e2, e3), pos) e1 e2 e3
type 'm var = 'm expr Bindlib.var
type 'm vars = 'm expr Bindlib.mvar
let new_var s = Bindlib.new_var (fun x -> EVar x) s
module Var = struct
type t = expr Bindlib.var
type t = V : 'a var -> t
(* See Dcalc.Ast.var *)
let make (s : string) : t =
Bindlib.new_var (fun (x : expr Bindlib.var) : expr -> EVar x) s
let t v = V v
let compare x y = Bindlib.compare_vars x y
let get (V v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)
let compare (V x) (V y) = Bindlib.compare_vars x y
end
module VarMap = Map.Make (Var)
module VarSet = Set.Make (Var)
module VarMap = Map.Make (Var)
type vars = expr Bindlib.mvar
(* </copy-paste> *)
let map_expr
(ctx : 'a)
~(f : 'a -> expr Marked.pos -> expr Marked.pos Bindlib.box)
(e : expr Marked.pos) : expr Marked.pos Bindlib.box =
let eraise e1 pos =
Bindlib.box (ERaise e1, pos)
let ecatch e1 exn e2 pos =
Bindlib.box_apply2 (fun e1 e2 -> ECatch (e1, exn, e2), pos) e1 e2
let map_expr ctx ~f e =
match Marked.unmark e with
| EVar v -> evar v (Marked.get_mark e)
| EApp (e1, args) ->
@ -173,41 +144,50 @@ let map_expr
| ECatch (e1, exn, e2) -> ecatch (f ctx e1) exn (f ctx e2) (Marked.get_mark e)
(** See [Bindlib.box_term] documentation for why we are doing that. *)
let box_expr (e : expr Marked.pos) : expr Marked.pos Bindlib.box =
let box_expr (e : 'm marked_expr) : 'm marked_expr Bindlib.box =
let rec id_t () e = map_expr () ~f:id_t e in
id_t () e
let make_var ((x, pos) : Var.t Marked.pos) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x)
let make_var (x, mark) =
Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x)
let make_abs
(xs : vars)
(e : expr Marked.pos Bindlib.box)
(taus : D.typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun b -> EAbs (b, taus), pos) (Bindlib.bind_mvar xs e)
let make_abs xs e taus mark =
Bindlib.box_apply (fun b -> EAbs (b, taus), mark) (Bindlib.bind_mvar xs e)
let make_app
(e : expr Marked.pos Bindlib.box)
(u : expr Marked.pos Bindlib.box list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_app e u mark =
Bindlib.box_apply2 (fun e u -> EApp (e, u), mark) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
(tau : D.typ Marked.pos)
(e1 : expr Marked.pos Bindlib.box)
(e2 : expr Marked.pos Bindlib.box)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
make_app (make_abs (Array.of_list [x]) e2 [tau] pos) [e1] pos
let make_let_in x tau e1 e2 pos =
let m_e1 = Marked.get_mark (Bindlib.unbox e1) in
let m_e2 = Marked.get_mark (Bindlib.unbox e2) in
let m_abs =
D.map_mark2
(fun _ _ -> pos)
(fun m1 m2 -> UnionFind.make (D.Infer.TArrow (m1.ty, m2.ty), m1.pos))
m_e1 m_e2
in
make_app (make_abs [| x |] e2 [tau] m_abs) [e1] m_e2
let make_multiple_let_in
(xs : Var.t array)
(taus : D.typ Marked.pos list)
(e1 : expr Marked.pos Bindlib.box list)
(e2 : expr Marked.pos Bindlib.box)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
make_app (make_abs xs e2 taus pos) e1 pos
let make_multiple_let_in xs taus e1s e2 pos =
(* let m_e1s = List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s in *)
let m_e1s =
D.fold_marks List.hd (fun tys ->
UnionFind.make
(D.Infer.TTuple
(List.map (fun t -> t.D.ty) tys, None),
(List.hd tys).D.pos)
)
(List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s)
in
let m_e2 = Marked.get_mark (Bindlib.unbox e2) in
let m_abs =
D.map_mark2
(fun _ _ -> pos)
(fun m1 m2 ->
UnionFind.make (D.Infer.TArrow (m1.ty, m2.ty), pos))
m_e1s m_e2
in
make_app (make_abs xs e2 taus m_abs) e1s m_e2
let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
@ -222,29 +202,33 @@ let some_constr : D.EnumConstructor.t =
let option_enum_config : (D.EnumConstructor.t * D.typ Marked.pos) list =
[none_constr, (D.TLit D.TUnit, Pos.no_pos); some_constr, (D.TAny, Pos.no_pos)]
let make_none (pos : Pos.t) : expr Marked.pos Bindlib.box =
let mark : 'a -> 'a Marked.pos = Marked.mark pos in
(* FIXME: proper typing in all the constructors below *)
let make_none m =
let mark = Marked.mark m in
let tunit = D.TLit D.TUnit, D.mark_pos m in
Bindlib.box @@ mark
@@ EInj
(mark @@ ELit LUnit, 0, option_enum, [D.TLit D.TUnit, pos; D.TAny, pos])
(Marked.mark (D.map_mark (fun pos -> pos) (fun _ -> D.Infer.ast_to_typ tunit) m)
(ELit LUnit),
0,
option_enum,
[D.TLit D.TUnit, Pos.no_pos; D.TAny, Pos.no_pos])
let make_some (e : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box =
let pos = Marked.get_mark @@ Bindlib.unbox e in
let mark : 'a -> 'a Marked.pos = Marked.mark pos in
let make_some e =
let m = Marked.get_mark @@ Bindlib.unbox e in
let mark = Marked.mark m in
begin[@ocamlformat "disable"]
let+ e = e in
mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ])
mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, D.mark_pos m); (D.TAny, D.mark_pos m) ])
end
(** [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 form [EAbs ...].*)
let make_matchopt_with_abs_arms
(arg : expr Marked.pos Bindlib.box)
(e_none : expr Marked.pos Bindlib.box)
(e_some : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box =
let pos = Marked.get_mark @@ Bindlib.unbox arg in
let mark : 'a -> 'a Marked.pos = Marked.mark pos in
let make_matchopt_with_abs_arms arg e_none e_some =
let m = Marked.get_mark @@ Bindlib.unbox arg in
let mark = Marked.mark m in
begin[@ocamlformat "disable"]
let+ arg = arg
and+ e_none = e_none
@ -256,20 +240,14 @@ let make_matchopt_with_abs_arms
[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 Marked.pos)
(arg : expr Marked.pos Bindlib.box)
(e_none : expr Marked.pos Bindlib.box)
(e_some : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box =
let x = Var.make "_" in
let make_matchopt m v tau arg e_none e_some =
let x = new_var "_" in
make_matchopt_with_abs_arms arg
(make_abs (Array.of_list [x]) e_none [D.TLit D.TUnit, pos] pos)
(make_abs (Array.of_list [v]) e_some [tau] pos)
(make_abs (Array.of_list [x]) e_none [D.TLit D.TUnit, D.mark_pos m] m)
(make_abs (Array.of_list [v]) e_some [tau] m)
let handle_default = Var.make "handle_default"
let handle_default_opt = Var.make "handle_default_opt"
let handle_default = Var.t (new_var "handle_default")
let handle_default_opt = Var.t (new_var "handle_default_opt")
type binder = (expr, expr Marked.pos) Bindlib.binder
type 'm binder = ('m expr, 'm marked_expr) Bindlib.binder

180
compiler/lcalc/ast.mli
View File

@ -34,153 +34,159 @@ type lit =
type except = ConflictError | EmptyError | NoValueProvided | Crash
type marked_expr = expr Marked.pos
type 'm mark = 'm Dcalc.Ast.mark
and expr =
| EVar of expr Bindlib.var
| ETuple of marked_expr list * Dcalc.Ast.StructName.t option
type 'm marked_expr = ('m expr, 'm) Dcalc.Ast.marked
and 'm expr =
| EVar of 'm expr Bindlib.var
| ETuple of 'm marked_expr list * Dcalc.Ast.StructName.t option
(** The [MarkedString.info] is the former struct field name*)
| ETupleAccess of
marked_expr
'm marked_expr
* int
* Dcalc.Ast.StructName.t option
* Dcalc.Ast.typ Marked.pos list
(** The [MarkedString.info] is the former struct field name *)
| EInj of
marked_expr * int * Dcalc.Ast.EnumName.t * Dcalc.Ast.typ Marked.pos list
'm marked_expr * int * Dcalc.Ast.EnumName.t * Dcalc.Ast.typ Marked.pos list
(** The [MarkedString.info] is the former enum case name *)
| EMatch of marked_expr * marked_expr list * Dcalc.Ast.EnumName.t
| EMatch of 'm marked_expr * 'm marked_expr list * Dcalc.Ast.EnumName.t
(** The [MarkedString.info] is the former enum case name *)
| EArray of marked_expr list
| EArray of 'm marked_expr list
| ELit of lit
| EAbs of (expr, marked_expr) Bindlib.mbinder * Dcalc.Ast.typ Marked.pos list
| EApp of marked_expr * marked_expr list
| EAssert of marked_expr
| EAbs of ('m expr, 'm marked_expr) Bindlib.mbinder * Dcalc.Ast.typ Marked.pos list
| EApp of 'm marked_expr * 'm marked_expr list
| EAssert of 'm marked_expr
| EOp of Dcalc.Ast.operator
| EIfThenElse of marked_expr * marked_expr * marked_expr
| EIfThenElse of 'm marked_expr * 'm marked_expr * 'm marked_expr
| ERaise of except
| ECatch of marked_expr * except * marked_expr
| ECatch of 'm marked_expr * except * 'm marked_expr
type program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : (expr, Dcalc.Ast.untyped) Dcalc.Ast.scopes }
type 'm program = { decl_ctx : Dcalc.Ast.decl_ctx; scopes : ('m expr, 'm) Dcalc.Ast.scopes }
(** {1 Variable helpers} *)
module Var : sig
type t = expr Bindlib.var
type 'm var = 'm expr Bindlib.var
type 'm vars = 'm expr Bindlib.mvar
val make : string -> t
module Var : sig
type t
val t: 'm expr Bindlib.var -> t
val get: t -> 'm expr Bindlib.var
val compare : t -> t -> int
end
module VarMap : Map.S with type key = Var.t
module VarSet : Set.S with type elt = Var.t
type vars = expr Bindlib.mvar
type binder = (expr, expr Marked.pos) Bindlib.binder
val new_var: string -> 'm var
(** {1 Boxed constructors}*)
type 'm binder = ('m expr, 'm marked_expr) Bindlib.binder
val evar : expr Bindlib.var -> Pos.t -> expr Marked.pos Bindlib.box
(** {1 Boxed constructors} *)
val evar : 'm expr Bindlib.var -> 'm mark -> 'm marked_expr Bindlib.box
val etuple :
expr Marked.pos Bindlib.box list ->
'm marked_expr Bindlib.box list ->
Dcalc.Ast.StructName.t option ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val etupleaccess :
expr Marked.pos Bindlib.box ->
'm marked_expr Bindlib.box ->
int ->
Dcalc.Ast.StructName.t option ->
Dcalc.Ast.typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val einj :
expr Marked.pos Bindlib.box ->
'm marked_expr Bindlib.box ->
int ->
Dcalc.Ast.EnumName.t ->
Dcalc.Ast.typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val ematch :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box list ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box list ->
Dcalc.Ast.EnumName.t ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val earray :
expr Marked.pos Bindlib.box list -> Pos.t -> expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box list -> 'm mark -> 'm marked_expr Bindlib.box
val elit : lit -> Pos.t -> expr Marked.pos Bindlib.box
val elit : lit -> 'm mark -> 'm marked_expr Bindlib.box
val eabs :
(expr, expr Marked.pos) Bindlib.mbinder Bindlib.box ->
('m expr, 'm marked_expr) Bindlib.mbinder Bindlib.box ->
Dcalc.Ast.typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val eapp :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box list ->
'm mark ->
'm marked_expr Bindlib.box
val eassert :
expr Marked.pos Bindlib.box -> Pos.t -> expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box -> 'm mark -> 'm marked_expr Bindlib.box
val eop : Dcalc.Ast.operator -> Pos.t -> expr Marked.pos Bindlib.box
val eop : Dcalc.Ast.operator -> 'm mark -> 'm marked_expr Bindlib.box
val eifthenelse :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm mark ->
'm marked_expr Bindlib.box
val ecatch :
expr Marked.pos Bindlib.box ->
'm marked_expr Bindlib.box ->
except ->
expr Marked.pos Bindlib.box ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm mark ->
'm marked_expr Bindlib.box
val eraise : except -> Pos.t -> expr Marked.pos Bindlib.box
val eraise : except -> 'm mark -> 'm marked_expr Bindlib.box
(** {1 Language terms construction}*)
val make_var : Var.t Marked.pos -> expr Marked.pos Bindlib.box
val make_var : ('m var, 'm) Dcalc.Ast.marked -> 'm marked_expr Bindlib.box
val make_abs :
vars ->
expr Marked.pos Bindlib.box ->
'm vars ->
'm marked_expr Bindlib.box ->
Dcalc.Ast.typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm mark ->
'm marked_expr Bindlib.box
val make_app :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box list ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box list ->
'm mark ->
'm marked_expr Bindlib.box
val make_let_in :
Var.t ->
'm var ->
Dcalc.Ast.typ Marked.pos ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box
val make_multiple_let_in :
Var.t array ->
'm vars ->
Dcalc.Ast.typ Marked.pos list ->
expr Marked.pos Bindlib.box list ->
expr Marked.pos Bindlib.box ->
'm marked_expr Bindlib.box list ->
'm marked_expr Bindlib.box ->
Pos.t ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box
val option_enum : Dcalc.Ast.EnumName.t
val none_constr : Dcalc.Ast.EnumConstructor.t
@ -189,29 +195,29 @@ val some_constr : Dcalc.Ast.EnumConstructor.t
val option_enum_config :
(Dcalc.Ast.EnumConstructor.t * Dcalc.Ast.typ Marked.pos) list
val make_none : Pos.t -> expr Marked.pos Bindlib.box
val make_some : expr Marked.pos Bindlib.box -> expr Marked.pos Bindlib.box
val make_none : 'm mark -> 'm marked_expr Bindlib.box
val make_some : 'm marked_expr Bindlib.box -> 'm marked_expr Bindlib.box
val make_matchopt_with_abs_arms :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box
val make_matchopt :
Pos.t ->
Var.t ->
'm mark ->
'm var ->
Dcalc.Ast.typ Marked.pos ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr Bindlib.box ->
'm marked_expr 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 box_expr : expr Marked.pos -> expr Marked.pos Bindlib.box
val box_expr : 'm marked_expr -> 'm marked_expr Bindlib.box
(** {1 Special symbols}*)
(** {1 Special symbols} *)
val handle_default : Var.t
val handle_default_opt : Var.t

145
compiler/lcalc/closure_conversion.ml
View File

@ -21,46 +21,51 @@ module D = Dcalc.Ast
(** TODO: This version is not yet debugged and ought to be specialized when
Lcalc has more structure. *)
type closure = { name : Var.t; expr : expr Marked.pos Bindlib.box }
type ctx = { name_context : string; globally_bound_vars : VarSet.t }
(** Returns the expression with closed closures and the set of free variables
inside this new expression. Implementation guided by
http://gallium.inria.fr/~fpottier/mpri/cours04.pdf#page=9. *)
let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
expr Marked.pos Bindlib.box * VarSet.t =
let closure_conversion_expr (type m) (ctx: ctx) (e: m marked_expr) : m marked_expr Bindlib.box =
let module MVarSet = Set.Make(struct
type t = m var
let compare = Bindlib.compare_vars
end) in
let rec aux e =
match Marked.unmark e with
| EVar v ->
( Bindlib.box_apply
(fun new_v -> new_v, Marked.get_mark e)
(Bindlib.box_var v),
VarSet.diff (VarSet.singleton v) ctx.globally_bound_vars )
if VarSet.mem (Var.t v) ctx.globally_bound_vars
then MVarSet.empty
else MVarSet.singleton v)
| ETuple (args, s) ->
let new_args, free_vars =
List.fold_left
(fun (new_args, free_vars) arg ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union new_free_vars free_vars)
([], VarSet.empty) args
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union new_free_vars free_vars)
([], MVarSet.empty) args
in
( Bindlib.box_apply
(fun new_args -> ETuple (List.rev new_args, s), Marked.get_mark e)
(Bindlib.box_list new_args),
free_vars )
| ETupleAccess (e1, n, s, typs) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
let new_e1, free_vars = aux e1 in
( Bindlib.box_apply
(fun new_e1 -> ETupleAccess (new_e1, n, s, typs), Marked.get_mark e)
new_e1,
free_vars )
| EInj (e1, n, e_name, typs) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
let new_e1, free_vars = aux e1 in
( Bindlib.box_apply
(fun new_e1 -> EInj (new_e1, n, e_name, typs), Marked.get_mark e)
new_e1,
free_vars )
| EMatch (e1, arms, e_name) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
let new_e1, free_vars = aux e1 in
(* We do not close the clotures inside the arms of the match expression,
since they get a special treatment at compilation to Scalc. *)
let new_arms, free_vars =
@ -69,13 +74,13 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
match Marked.unmark arm with
| EAbs (binder, typs) ->
let vars, body = Bindlib.unmbind binder in
let new_body, new_free_vars = closure_conversion_expr ctx body in
let new_body, new_free_vars = aux body in
let new_binder = Bindlib.bind_mvar vars new_body in
( Bindlib.box_apply
(fun new_binder -> EAbs (new_binder, typs), Marked.get_mark arm)
new_binder
:: new_arms,
VarSet.union free_vars new_free_vars )
MVarSet.union free_vars new_free_vars )
| _ -> failwith "should not happen")
arms ([], free_vars)
in
@ -89,25 +94,25 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
let new_args, free_vars =
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union free_vars new_free_vars)
args ([], MVarSet.empty)
in
( Bindlib.box_apply
(fun new_args -> EArray new_args, Marked.get_mark e)
(Bindlib.box_list new_args),
free_vars )
| ELit l -> Bindlib.box (ELit l, Marked.get_mark e), VarSet.empty
| ELit l -> Bindlib.box (ELit l, Marked.get_mark e), MVarSet.empty
| EApp ((EAbs (binder, typs_abs), e1_pos), args) ->
(* let-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in
let new_body, free_vars = closure_conversion_expr ctx body in
let new_body, free_vars = aux body in
let new_binder = Bindlib.bind_mvar vars new_body in
let new_args, free_vars =
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union free_vars new_free_vars)
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union free_vars new_free_vars)
args ([], free_vars)
in
( Bindlib.box_apply2
@ -119,40 +124,39 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
free_vars )
| EAbs (binder, typs) ->
(* λ x.t *)
let binder_pos = Marked.get_mark e in
let binder_mark = Marked.get_mark e in
let binder_pos = D.mark_pos binder_mark in
(* Converting the closure. *)
let vars, body = Bindlib.unmbind binder in
(* t *)
let new_body, body_vars = closure_conversion_expr ctx body in
let new_body, body_vars = aux body in
(* [[t]] *)
let extra_vars =
VarSet.diff body_vars (VarSet.of_list (Array.to_list vars))
MVarSet.diff body_vars (MVarSet.of_list (Array.to_list vars))
in
let extra_vars_list = VarSet.elements extra_vars in
let extra_vars_list = MVarSet.elements extra_vars in
(* x1, ..., xn *)
let code_var = Var.make ctx.name_context in
let code_var = new_var ctx.name_context in
(* code *)
let inner_c_var = Var.make "env" in
let inner_c_var = new_var "env" in
let any_ty = Dcalc.Ast.TAny, binder_pos in
let new_closure_body =
make_multiple_let_in
(Array.of_list extra_vars_list)
(List.init (List.length extra_vars_list) (fun _ ->
Dcalc.Ast.TAny, binder_pos))
(List.map (fun _ -> any_ty) extra_vars_list)
(List.mapi
(fun i _ ->
Bindlib.box_apply
(fun inner_c_var ->
( ETupleAccess
( (inner_c_var, binder_pos),
( (inner_c_var, binder_mark),
i + 1,
None,
List.init
(List.length extra_vars_list + 1)
(fun _ -> Dcalc.Ast.TAny, binder_pos) ),
binder_pos ))
List.map (fun _ -> any_ty) extra_vars_list),
binder_mark ))
(Bindlib.box_var inner_c_var))
extra_vars_list)
new_body binder_pos
new_body (D.mark_pos binder_mark)
in
let new_closure =
make_abs
@ -162,14 +166,14 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
(Marked.get_mark e)
in
( make_let_in code_var
(Dcalc.Ast.TAny, Marked.get_mark e)
(Dcalc.Ast.TAny, D.pos e)
new_closure
(Bindlib.box_apply2
(fun code_var extra_vars ->
( ETuple
( (code_var, binder_pos)
( (code_var, binder_mark)
:: List.map
(fun extra_var -> extra_var, binder_pos)
(fun extra_var -> extra_var, binder_mark)
extra_vars,
None ),
Marked.get_mark e ))
@ -178,29 +182,29 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
(List.map
(fun extra_var -> Bindlib.box_var extra_var)
extra_vars_list)))
(Marked.get_mark e),
(D.pos e),
extra_vars )
| EApp ((EOp op, pos_op), args) ->
(* This corresponds to an operator call, which we don't want to transform*)
let new_args, free_vars =
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union free_vars new_free_vars)
args ([], MVarSet.empty)
in
( Bindlib.box_apply
(fun new_e2 -> EApp ((EOp op, pos_op), new_e2), Marked.get_mark e)
(Bindlib.box_list new_args),
free_vars )
| EApp ((EVar v, v_pos), args) when VarSet.mem v ctx.globally_bound_vars ->
| EApp ((EVar v, v_pos), args) when VarSet.mem (Var.t v) ctx.globally_bound_vars ->
(* This corresponds to a scope call, which we don't want to transform*)
let new_args, free_vars =
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union free_vars new_free_vars)
args ([], VarSet.empty)
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union free_vars new_free_vars)
args ([], MVarSet.empty)
in
( Bindlib.box_apply2
(fun new_v new_e2 -> EApp ((new_v, v_pos), new_e2), Marked.get_mark e)
@ -208,19 +212,19 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
(Bindlib.box_list new_args),
free_vars )
| EApp (e1, args) ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
let env_var = Var.make "env" in
let code_var = Var.make "code" in
let new_e1, free_vars = aux e1 in
let env_var = new_var "env" in
let code_var = new_var "code" in
let new_args, free_vars =
List.fold_right
(fun arg (new_args, free_vars) ->
let new_arg, new_free_vars = closure_conversion_expr ctx arg in
new_arg :: new_args, VarSet.union free_vars new_free_vars)
let new_arg, new_free_vars = aux arg in
new_arg :: new_args, MVarSet.union free_vars new_free_vars)
args ([], free_vars)
in
let call_expr =
make_let_in code_var
(Dcalc.Ast.TAny, Marked.get_mark e)
(Dcalc.Ast.TAny, D.pos e)
(Bindlib.box_apply
(fun env_var ->
( ETupleAccess
@ -235,50 +239,50 @@ let rec closure_conversion_expr (ctx : ctx) (e : expr Marked.pos) :
Marked.get_mark e ))
(Bindlib.box_var code_var) (Bindlib.box_var env_var)
(Bindlib.box_list new_args))
(Marked.get_mark e)
(D.pos e)
in
( make_let_in env_var
(Dcalc.Ast.TAny, Marked.get_mark e)
new_e1 call_expr (Marked.get_mark e),
(Dcalc.Ast.TAny, D.pos e)
new_e1 call_expr (D.pos e),
free_vars )
| EAssert e1 ->
let new_e1, free_vars = closure_conversion_expr ctx e1 in
let new_e1, free_vars = aux e1 in
( Bindlib.box_apply (fun new_e1 -> EAssert new_e1, Marked.get_mark e) new_e1,
free_vars )
| EOp op -> Bindlib.box (EOp op, Marked.get_mark e), VarSet.empty
| EOp op -> Bindlib.box (EOp op, Marked.get_mark e), MVarSet.empty
| EIfThenElse (e1, e2, e3) ->
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
let new_e3, free_vars3 = closure_conversion_expr ctx e3 in
let new_e1, free_vars1 = aux e1 in
let new_e2, free_vars2 = aux e2 in
let new_e3, free_vars3 = aux e3 in
( Bindlib.box_apply3
(fun new_e1 new_e2 new_e3 ->
EIfThenElse (new_e1, new_e2, new_e3), Marked.get_mark e)
new_e1 new_e2 new_e3,
VarSet.union (VarSet.union free_vars1 free_vars2) free_vars3 )
MVarSet.union (MVarSet.union free_vars1 free_vars2) free_vars3 )
| ERaise except ->
Bindlib.box (ERaise except, Marked.get_mark e), VarSet.empty
Bindlib.box (ERaise except, Marked.get_mark e), MVarSet.empty
| ECatch (e1, except, e2) ->
let new_e1, free_vars1 = closure_conversion_expr ctx e1 in
let new_e2, free_vars2 = closure_conversion_expr ctx e2 in
let new_e1, free_vars1 = aux e1 in
let new_e2, free_vars2 = aux e2 in
( Bindlib.box_apply2
(fun new_e1 new_e2 ->
ECatch (new_e1, except, new_e2), Marked.get_mark e)
new_e1 new_e2,
VarSet.union free_vars1 free_vars2 )
MVarSet.union free_vars1 free_vars2 )
in
let e', _vars = aux e in
e'
let closure_conversion (p : program) : program Bindlib.box =
let closure_conversion (p : 'm program) : 'm program Bindlib.box =
let new_scopes, _ =
D.fold_left_scope_defs
~f:
(fun ((acc_new_scopes, global_vars) :
(expr D.scopes Bindlib.box -> expr D.scopes Bindlib.box)
* VarSet.t) (scope : expr D.scope_def) (scope_var : Var.t) ->
~f:(fun (acc_new_scopes, global_vars) scope scope_var ->
(* [acc_new_scopes] represents what has been translated in the past, it
needs a continuation to attach the rest of the translated scopes. *)
let scope_input_var, scope_body_expr =
Bindlib.unbind scope.scope_body.scope_body_expr
in
let global_vars = VarSet.add scope_var global_vars in
let global_vars = VarSet.add (Var.t scope_var) global_vars in
let ctx =
{
name_context =
@ -288,7 +292,8 @@ let closure_conversion (p : program) : program Bindlib.box =
in
let new_scope_lets =
D.map_exprs_in_scope_lets
~f:(fun e -> fst (closure_conversion_expr ctx e))
~f:(closure_conversion_expr ctx)
~varf:(fun v -> v)
scope_body_expr
in
let new_scope_body_expr =

19
compiler/lcalc/closure_conversion.mli Normal file
View File

@ -0,0 +1,19 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2022 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
val closure_conversion: 'm Ast.program -> 'm Ast.program Bindlib.box
(** Warning/todo: no effort was yet made to ensure
correct propagation of type annotations in the typed case *)

70
compiler/lcalc/compile_with_exceptions.ml
View File

@ -18,11 +18,11 @@ open Utils
module D = Dcalc.Ast
module A = Ast
type ctx = A.Var.t D.VarMap.t
type 'm ctx = 'm A.var D.VarMap.t
(** This environment contains a mapping between the variables in Dcalc and their
correspondance in Lcalc. *)
let translate_lit (l : D.lit) : A.expr =
let translate_lit (l : D.lit) : 'm A.expr =
match l with
| D.LBool l -> A.ELit (A.LBool l)
| D.LInt i -> A.ELit (A.LInt i)
@ -33,38 +33,38 @@ let translate_lit (l : D.lit) : A.expr =
| D.LDuration d -> A.ELit (A.LDuration d)
| D.LEmptyError -> A.ERaise A.EmptyError
let thunk_expr (e : A.expr Marked.pos Bindlib.box) (pos : Pos.t) :
A.expr Marked.pos Bindlib.box =
let dummy_var = A.Var.make "_" in
A.make_abs [| dummy_var |] e [D.TAny, pos] pos
let thunk_expr (e : 'm A.marked_expr Bindlib.box) (mark: 'm A.mark) :
'm A.marked_expr Bindlib.box =
let dummy_var = A.new_var "_" in
A.make_abs [| dummy_var |] e [D.TAny, D.mark_pos mark] mark
let rec translate_default
(ctx : ctx)
(exceptions : D.expr Marked.pos list)
(just : D.expr Marked.pos)
(cons : D.expr Marked.pos)
(pos_default : Pos.t) : A.expr Marked.pos Bindlib.box =
(ctx : 'm ctx)
(exceptions : 'm D.marked_expr list)
(just : 'm D.marked_expr)
(cons : 'm D.marked_expr)
(mark_default : 'm D.mark) : 'm A.marked_expr Bindlib.box =
let exceptions =
List.map
(fun except -> thunk_expr (translate_expr ctx except) pos_default)
(fun except -> thunk_expr (translate_expr ctx except) mark_default)
exceptions
in
let exceptions =
A.make_app
(A.make_var (A.handle_default, pos_default))
(A.make_var (A.Var.get A.handle_default, mark_default))
[
A.earray exceptions pos_default;
thunk_expr (translate_expr ctx just) pos_default;
thunk_expr (translate_expr ctx cons) pos_default;
A.earray exceptions mark_default;
thunk_expr (translate_expr ctx just) mark_default;
thunk_expr (translate_expr ctx cons) mark_default;
]
pos_default
mark_default
in
exceptions
and translate_expr (ctx : ctx) (e : D.expr Marked.pos) :
A.expr Marked.pos Bindlib.box =
and translate_expr (ctx : 'm ctx) (e : 'm D.marked_expr) :
'm A.marked_expr Bindlib.box =
match Marked.unmark e with
| D.EVar v -> A.make_var (D.VarMap.find v ctx, Marked.get_mark e)
| D.EVar v -> A.make_var (D.VarMap.find (D.Var.t v) ctx, Marked.get_mark e)
| D.ETuple (args, s) ->
A.etuple (List.map (translate_expr ctx) args) s (Marked.get_mark e)
| D.ETupleAccess (e1, i, s, ts) ->
@ -96,8 +96,8 @@ and translate_expr (ctx : ctx) (e : D.expr Marked.pos) :
let ctx, lc_vars =
Array.fold_right
(fun var (ctx, lc_vars) ->
let lc_var = A.Var.make (Bindlib.name_of var) in
D.VarMap.add var lc_var ctx, lc_var :: lc_vars)
let lc_var = A.new_var (Bindlib.name_of var) in
D.VarMap.add (D.Var.t var) lc_var ctx, lc_var :: lc_vars)
vars (ctx, [])
in
let lc_vars = Array.of_list lc_vars in
@ -117,18 +117,18 @@ and translate_expr (ctx : ctx) (e : D.expr Marked.pos) :
let rec translate_scope_lets
(decl_ctx : D.decl_ctx)
(ctx : A.Var.t D.VarMap.t)
(scope_lets : D.expr D.scope_body_expr) :
A.expr D.scope_body_expr Bindlib.box =
(ctx : 'm ctx)
(scope_lets : ('m D.expr, 'm) D.scope_body_expr) :
('m A.expr, 'm) D.scope_body_expr Bindlib.box =
match scope_lets with
| Result e -> Bindlib.box_apply (fun e -> D.Result e) (translate_expr ctx e)
| ScopeLet scope_let ->
let old_scope_let_var, scope_let_next =
Bindlib.unbind scope_let.scope_let_next
in
let new_scope_let_var = A.Var.make (Bindlib.name_of old_scope_let_var) in
let new_scope_let_var = A.new_var (Bindlib.name_of old_scope_let_var) in
let new_scope_let_expr = translate_expr ctx scope_let.scope_let_expr in
let new_ctx = D.VarMap.add old_scope_let_var new_scope_let_var ctx in
let new_ctx = D.VarMap.add (D.Var.t old_scope_let_var) new_scope_let_var ctx in
let new_scope_next = translate_scope_lets decl_ctx new_ctx scope_let_next in
let new_scope_next = Bindlib.bind_var new_scope_let_var new_scope_next in
Bindlib.box_apply2
@ -145,29 +145,29 @@ let rec translate_scope_lets
let rec translate_scopes
(decl_ctx : D.decl_ctx)
(ctx : A.Var.t D.VarMap.t)
(scopes : D.expr D.scopes) : A.expr D.scopes Bindlib.box =
(ctx : 'm ctx)
(scopes : ('m D.expr, 'm) D.scopes) : ('m A.expr, 'm) D.scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box D.Nil
| ScopeDef scope_def ->
let old_scope_var, scope_next = Bindlib.unbind scope_def.scope_next in
let new_scope_var =
A.Var.make (Marked.unmark (D.ScopeName.get_info scope_def.scope_name))
A.new_var (Marked.unmark (D.ScopeName.get_info scope_def.scope_name))
in
let old_scope_input_var, scope_body_expr =
Bindlib.unbind scope_def.scope_body.scope_body_expr
in
let new_scope_input_var =
A.Var.make (Bindlib.name_of old_scope_input_var)
A.new_var (Bindlib.name_of old_scope_input_var)
in
let new_ctx = D.VarMap.add old_scope_input_var new_scope_input_var ctx in
let new_ctx = D.VarMap.add (D.Var.t old_scope_input_var) new_scope_input_var ctx in
let new_scope_body_expr =
translate_scope_lets decl_ctx new_ctx scope_body_expr
in
let new_scope_body_expr =
Bindlib.bind_var new_scope_input_var new_scope_body_expr
in
let new_scope : A.expr D.scope_body Bindlib.box =
let new_scope : ('m A.expr, 'm) D.scope_body Bindlib.box =
Bindlib.box_apply
(fun new_scope_body_expr ->
{
@ -179,7 +179,7 @@ let rec translate_scopes
})
new_scope_body_expr
in
let new_ctx = D.VarMap.add old_scope_var new_scope_var new_ctx in
let new_ctx = D.VarMap.add (D.Var.t old_scope_var) new_scope_var new_ctx in
let scope_next =
Bindlib.bind_var new_scope_var
(translate_scopes decl_ctx new_ctx scope_next)
@ -194,7 +194,7 @@ let rec translate_scopes
})
new_scope scope_next
let translate_program (prgm : D.program) : A.program =
let translate_program (prgm : 'm D.program) : 'm A.program =
{
scopes =
Bindlib.unbox (translate_scopes prgm.decl_ctx D.VarMap.empty prgm.scopes);

4
compiler/lcalc/compile_with_exceptions.mli
View File

@ -15,6 +15,6 @@
the License. *)
(** Translation from the default calculus to the lambda calculus. This
translation uses exceptions handle empty default terms. *)
translation uses exceptions to handle empty default terms. *)
val translate_program : Dcalc.Ast.typed Dcalc.Ast.program -> Ast.program
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

157
compiler/lcalc/compile_without_exceptions.ml
View File

@ -40,12 +40,12 @@ module A = Ast
hoisted and later handled by the [translate_expr] function. Every other
cases is found in the translate_and_hoist function. *)
type hoists = D.expr Marked.pos A.VarMap.t
type 'm hoists = 'm D.marked_expr A.VarMap.t
(** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
type info = {
expr : A.expr Marked.pos Bindlib.box;
var : A.expr Bindlib.var;
type 'm info = {
expr : 'm A.marked_expr Bindlib.box;
var : 'm A.expr Bindlib.var;
is_pure : bool;
}
(** Information about each encontered Dcalc variable is stored inside a context
@ -54,19 +54,19 @@ type info = {
indicating whenever the variable can be an EmptyError and hence should be
matched (false) or if it never can be EmptyError (true). *)
let pp_info (fmt : Format.formatter) (info : info) =
let pp_info (fmt : Format.formatter) (info : 'm info) =
Format.fprintf fmt "{var: %a; is_pure: %b}" Print.format_var info.var
info.is_pure
type ctx = {
type 'm ctx = {
decl_ctx : D.decl_ctx;
vars : info D.VarMap.t;
vars : 'm info D.VarMap.t;
(** information context about variables in the current scope *)
}
let _pp_ctx (fmt : Format.formatter) (ctx : ctx) =
let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * info) =
Format.fprintf fmt "%a: %a" Dcalc.Print.format_var v pp_info info
let _pp_ctx (fmt : Format.formatter) (ctx : 'm ctx) =
let pp_binding (fmt : Format.formatter) ((v, info) : D.Var.t * 'm info) =
Format.fprintf fmt "%a: %a" Dcalc.Print.format_var (D.Var.get v) pp_info info
in
let pp_bindings =
@ -79,10 +79,10 @@ let _pp_ctx (fmt : Format.formatter) (ctx : ctx) =
(** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a
slightly better way. *)
let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
let find ?(info : string = "none") (n : 'm D.var) (ctx : 'm ctx) : 'm info =
(* let _ = Format.asprintf "Searching for variable %a inside context %a"
Dcalc.Print.format_var n pp_ctx ctx |> Cli.debug_print in *)
try D.VarMap.find n ctx.vars
try D.VarMap.find (D.Var.t n) ctx.vars
with Not_found ->
Errors.raise_spanned_error Pos.no_pos
"Internal Error: Variable %a was not found in the current environment. \
@ -93,16 +93,16 @@ let find ?(info : string = "none") (n : D.Var.t) (ctx : ctx) : info =
var, creating a unique corresponding variable in Lcalc, with the
corresponding expression, and the boolean is_pure. It is usefull for
debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *)
let add_var (pos : Pos.t) (var : D.Var.t) (is_pure : bool) (ctx : ctx) : ctx =
let new_var = A.Var.make (Bindlib.name_of var) in
let expr = A.make_var (new_var, pos) in
let add_var (mark : 'm D.mark) (var : 'm D.var) (is_pure : bool) (ctx : 'm ctx) : 'm ctx =
let new_var = A.new_var (Bindlib.name_of var) in
let expr = A.make_var (new_var, mark) in
(* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Dcalc.Print.format_var
var Print.format_var new_var; *)
{
ctx with
vars =
D.VarMap.update var
D.VarMap.update (D.Var.t var)
(fun _ -> Some { expr; var = new_var; is_pure })
ctx.vars;
}
@ -161,8 +161,8 @@ let disjoint_union_maps (pos : Pos.t) (cs : 'a A.VarMap.t list) : 'a A.VarMap.t
the equivalence between the execution of e and the execution of e' are
equivalent in an environement where each variable v, where (v, e_v) is in
hoists, has the non-empty value in e_v. *)
let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
A.expr Marked.pos Bindlib.box * hoists =
let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.marked_expr) :
'm A.marked_expr Bindlib.box * 'm hoists =
let pos = Marked.get_mark e in
match Marked.unmark e with
(* empty-producing/using terms. We hoist those. (D.EVar in some cases,
@ -174,46 +174,46 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
assumption can change in the future, and this case is here for this
reason. *)
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = A.Var.make (Bindlib.name_of v) in
let v' = A.new_var (Bindlib.name_of v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Dcalc.Print.format_var v
Print.format_var v'; *)
A.make_var (v', pos), A.VarMap.singleton v' e
A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e
else (find ~info:"should never happend" v ctx).expr, A.VarMap.empty
| D.EApp ((D.EVar v, p), [(D.ELit D.LUnit, _)]) ->
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = A.Var.make (Bindlib.name_of v) in
let v' = A.new_var (Bindlib.name_of v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Dcalc.Print.format_var v
Print.format_var v'; *)
A.make_var (v', pos), A.VarMap.singleton v' (D.EVar v, p)
A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') (D.EVar v, p)
else
Errors.raise_spanned_error pos
Errors.raise_spanned_error (D.pos e)
"Internal error: an pure variable was found in an unpure environment."
| D.EDefault (_exceptions, _just, _cons) ->
let v' = A.Var.make "default_term" in
A.make_var (v', pos), A.VarMap.singleton v' e
let v' = A.new_var "default_term" in
A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e
| D.ELit D.LEmptyError ->
let v' = A.Var.make "empty_litteral" in
A.make_var (v', pos), A.VarMap.singleton v' e
let v' = A.new_var "empty_litteral" in
A.make_var (v', pos), A.VarMap.singleton (A.Var.t v') e
(* This one is a very special case. It transform an unpure expression
environement to a pure expression. *)
| ErrorOnEmpty arg ->
(* [ match arg with | None -> raise NoValueProvided | Some v -> {{ v }} ] *)
let silent_var = A.Var.make "_" in
let x = A.Var.make "non_empty_argument" in
let silent_var = A.new_var "_" in
let x = A.new_var "non_empty_argument" in
let arg' = translate_expr ctx arg in
( A.make_matchopt_with_abs_arms arg'
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos))
[D.TAny, pos]
[D.TAny, D.pos e]
pos)
(A.make_abs [| x |] (A.make_var (x, pos)) [D.TAny, pos] pos),
(A.make_abs [| x |] (A.make_var (x, pos)) [D.TAny, D.pos e] pos),
A.VarMap.empty )
(* pure terms *)
| D.ELit l -> A.elit (translate_lit l pos) pos, A.VarMap.empty
| D.ELit l -> A.elit (translate_lit l (D.pos e)) pos, A.VarMap.empty
| D.EIfThenElse (e1, e2, e3) ->
let e1', h1 = translate_and_hoist ctx e1 in
let e2', h2 = translate_and_hoist ctx e2 in
@ -223,7 +223,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
(*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' =
e3' in (A.EIfThenElse (e1', e2', e3'), pos) in *)
e', disjoint_union_maps pos [h1; h2; h3]
e', disjoint_union_maps (D.pos e) [h1; h2; h3]
| D.EAssert e1 ->
(* same behavior as in the ICFP paper: if e1 is empty, then no error is
raised. *)
@ -260,7 +260,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
args |> List.map (translate_and_hoist ctx) |> List.split
in
let hoists = disjoint_union_maps pos (h1 :: h_args) in
let hoists = disjoint_union_maps (D.pos e) (h1 :: h_args) in
let e' = A.eapp e1' args' pos in
e', hoists
| ETuple (args, s) ->
@ -268,7 +268,7 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
args |> List.map (translate_and_hoist ctx) |> List.split
in
let hoists = disjoint_union_maps pos h_args in
let hoists = disjoint_union_maps (D.pos e) h_args in
A.etuple args' s pos, hoists
| ETupleAccess (e1, i, s, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
@ -284,17 +284,17 @@ let rec translate_and_hoist (ctx : ctx) (e : D.expr Marked.pos) :
cases |> List.map (translate_and_hoist ctx) |> List.split
in
let hoists = disjoint_union_maps pos (h1 :: h_cases) in
let hoists = disjoint_union_maps (D.pos e) (h1 :: h_cases) in
let e' = A.ematch e1' cases' en pos in
e', hoists
| EArray es ->
let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
A.earray es' pos, disjoint_union_maps pos hoists
A.earray es' pos, disjoint_union_maps (D.pos e) hoists
| EOp op -> Bindlib.box (A.EOp op, pos), A.VarMap.empty
and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) :
A.expr Marked.pos Bindlib.box =
and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.marked_expr) :
'm A.marked_expr Bindlib.box =
let e', hoists = translate_and_hoist ctx e in
let hoists = A.VarMap.bindings hoists in
@ -305,10 +305,10 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) :
(Format.pp_print_list Print.format_var) (List.map fst hoists); *)
ListLabels.fold_left hoists
~init:(if append_esome then A.make_some e' else e')
~f:(fun acc (v, (hoist, pos_hoist)) ->
~f:(fun acc (v, (hoist, mark_hoist)) ->
(* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.format_var
v; *)
let c' : A.expr Marked.pos Bindlib.box =
let c' : 'm A.marked_expr Bindlib.box =
match hoist with
(* Here we have to handle only the cases appearing in hoists, as defined
the [translate_and_hoist] function. *)
@ -319,37 +319,37 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) :
let cons' = translate_expr ctx cons in
(* calls handle_option. *)
A.make_app
(A.make_var (A.handle_default_opt, pos_hoist))
(A.make_var (A.Var.get A.handle_default_opt, mark_hoist))
[
Bindlib.box_apply
(fun excep' -> A.EArray excep', pos_hoist)
(fun excep' -> A.EArray excep', mark_hoist)
(Bindlib.box_list excep');
just';
cons';
]
pos_hoist
| D.ELit D.LEmptyError -> A.make_none pos_hoist
mark_hoist
| D.ELit D.LEmptyError -> A.make_none mark_hoist
| D.EAssert arg ->
let arg' = translate_expr ctx arg in
(* [ match arg with | None -> raise NoValueProvided | Some v -> assert
{{ v }} ] *)
let silent_var = A.Var.make "_" in
let x = A.Var.make "assertion_argument" in
let silent_var = A.new_var "_" in
let x = A.new_var "assertion_argument" in
A.make_matchopt_with_abs_arms arg'
(A.make_abs [| silent_var |]
(Bindlib.box (A.ERaise A.NoValueProvided, pos_hoist))
[D.TAny, pos_hoist]
pos_hoist)
(Bindlib.box (A.ERaise A.NoValueProvided, mark_hoist))
[D.TAny, D.mark_pos mark_hoist]
mark_hoist)
(A.make_abs [| x |]
(Bindlib.box_apply
(fun arg -> A.EAssert arg, pos_hoist)
(A.make_var (x, pos_hoist)))
[D.TAny, pos_hoist]
pos_hoist)
(fun arg -> A.EAssert arg, mark_hoist)
(A.make_var (x, mark_hoist)))
[D.TAny, D.mark_pos mark_hoist]
mark_hoist)
| _ ->
Errors.raise_spanned_error pos_hoist
Errors.raise_spanned_error (D.mark_pos mark_hoist)
"Internal Error: An term was found in a position where it should \
not be"
in
@ -358,11 +358,11 @@ and translate_expr ?(append_esome = true) (ctx : ctx) (e : D.expr Marked.pos) :
] *)
(* Cli.debug_print @@ Format.asprintf "build matchopt using %a"
Print.format_var v; *)
A.make_matchopt pos_hoist v (D.TAny, pos_hoist) c' (A.make_none pos_hoist)
A.make_matchopt mark_hoist (A.Var.get v) (D.TAny, D.mark_pos mark_hoist) c' (A.make_none mark_hoist)
acc)
let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
A.expr D.scope_body_expr Bindlib.box =
let rec translate_scope_let (ctx : 'm ctx) (lets : ('m D.expr, 'm) D.scope_body_expr) :
('m A.expr, 'm) D.scope_body_expr Bindlib.box =
match lets with
| Result e ->
Bindlib.box_apply
@ -372,7 +372,7 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = D.EAbs (binder, _), _;
scope_let_expr = D.EAbs (binder, _), emark;
scope_let_next = next;
scope_let_pos = pos;
} ->
@ -384,7 +384,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var
var; *)
let ctx' = add_var pos var var_is_pure ctx in
let vmark =
D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) emark
in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
let new_next = translate_scope_let ctx' next in
Bindlib.box_apply2
@ -403,7 +406,7 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = (D.ErrorOnEmpty _, _) as expr;
scope_let_expr = (D.ErrorOnEmpty _, emark) as expr;
scope_let_next = next;
scope_let_pos = pos;
} ->
@ -412,7 +415,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var
var; *)
let ctx' = add_var pos var var_is_pure ctx in
let vmark =
D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) emark
in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
Bindlib.box_apply2
(fun new_expr new_next ->
@ -464,7 +470,10 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Dcalc.Print.format_var
var; *)
let ctx' = add_var pos var var_is_pure ctx in
let vmark =
D.map_mark (fun _ -> pos) (fun _ -> D.Infer.ast_to_typ typ) (Marked.get_mark expr)
in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
Bindlib.box_apply2
(fun new_expr new_next ->
@ -481,8 +490,8 @@ let rec translate_scope_let (ctx : ctx) (lets : D.expr D.scope_body_expr) :
let translate_scope_body
(scope_pos : Pos.t)
(ctx : ctx)
(body : D.expr D.scope_body) : A.expr D.scope_body Bindlib.box =
(ctx : 'm ctx)
(body : ('m D.expr, 'm) D.scope_body) : ('m A.expr, 'm) D.scope_body Bindlib.box =
match body with
| {
scope_body_expr = result;
@ -490,7 +499,11 @@ let translate_scope_body
scope_body_output_struct = output_struct;
} ->
let v, lets = Bindlib.unbind result in
let ctx' = add_var scope_pos v true ctx in
let vmark =
let m = match lets with Result e | ScopeLet { scope_let_expr=e; _} -> Marked.get_mark e in
D.map_mark (fun _ -> scope_pos) (fun ty -> ty) m
in
let ctx' = add_var vmark v true ctx in
let v' = (find ~info:"variable that was just created" v ctx').var in
Bindlib.box_apply
(fun new_expr ->
@ -501,13 +514,17 @@ let translate_scope_body
})
(Bindlib.bind_var v' (translate_scope_let ctx' lets))
let rec translate_scopes (ctx : ctx) (scopes : D.expr D.scopes) :
A.expr D.scopes Bindlib.box =
let rec translate_scopes (ctx : 'm ctx) (scopes : ('m D.expr, 'm) D.scopes) :
('m A.expr, 'm) D.scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box D.Nil
| ScopeDef { scope_name; scope_body; scope_next } ->
let scope_var, next = Bindlib.unbind scope_next in
let new_ctx = add_var Pos.no_pos scope_var true ctx in
let vmark =
match Bindlib.unbind scope_body.scope_body_expr with _, (Result e | ScopeLet { scope_let_expr=e; _}) -> Marked.get_mark e
in
let new_ctx = add_var vmark scope_var true ctx in
let new_scope_name =
(find ~info:"variable that was just created" scope_var new_ctx).var
in
@ -523,7 +540,7 @@ let rec translate_scopes (ctx : ctx) (scopes : D.expr D.scopes) :
new_body
(Bindlib.bind_var new_scope_name tail)
let translate_program (prgm : D.program) : A.program =
let translate_program (prgm : 'm D.program) : 'm A.program =
let inputs_structs =
D.fold_left_scope_defs prgm.scopes ~init:[] ~f:(fun acc scope_def _ ->
scope_def.D.scope_body.scope_body_input_struct :: acc)

2
compiler/lcalc/compile_without_exceptions.mli
View File

@ -19,4 +19,4 @@
transformation is one piece to permit to compile toward legacy languages
that does not contains exceptions. *)
val translate_program : Dcalc.Ast.typed Dcalc.Ast.program -> Ast.program
val translate_program : 'm Dcalc.Ast.program -> 'm Ast.program

26
compiler/lcalc/optimizations.ml
View File

@ -20,9 +20,9 @@ let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x y = Bindlib.box_pair x y
let visitor_map
(t : 'a -> expr Marked.pos -> expr Marked.pos Bindlib.box)
(t : 'a -> 'm marked_expr -> 'm marked_expr Bindlib.box)
(ctx : 'a)
(e : expr Marked.pos) : expr Marked.pos Bindlib.box =
(e : 'm marked_expr) : 'm marked_expr Bindlib.box =
(* calls [t ctx] on every direct childs of [e], then rebuild an abstract
syntax tree modified. Used in other transformations. *)
let default_mark e' = Marked.same_mark_as e' e in
@ -66,7 +66,7 @@ let visitor_map
default_mark @@ ECatch (e1, exn, e2)
| ERaise _ | ELit _ | EOp _ -> Bindlib.box e
let rec iota_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box
let rec iota_expr (_ : unit) (e : 'm marked_expr) : 'm marked_expr Bindlib.box
=
let default_mark e' = Marked.mark (Marked.get_mark e) e' in
match Marked.unmark e with
@ -86,7 +86,7 @@ let rec iota_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box
visitor_map iota_expr () e'
| _ -> visitor_map iota_expr () e
let rec beta_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box
let rec beta_expr (_ : unit) (e : 'm marked_expr) : 'm marked_expr Bindlib.box
=
let default_mark e' = Marked.same_mark_as e' e in
match Marked.unmark e with
@ -100,20 +100,20 @@ let rec beta_expr (_ : unit) (e : expr Marked.pos) : expr Marked.pos Bindlib.box
| _ -> default_mark @@ EApp (e1, args))
| _ -> visitor_map beta_expr () e
let iota_optimizations (p : program) : program =
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) p.scopes in
let iota_optimizations (p : 'm program) : 'm program =
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(iota_expr ()) ~varf:(fun v -> v) p.scopes in
{ p with scopes = Bindlib.unbox new_scopes }
(* TODO: beta optimizations apply inlining of the program. We left the inclusion
of beta-optimization as future work since its produce code that is harder to
read, and can produce exponential blowup of the size of the generated
program. *)
let _beta_optimizations (p : program) : program =
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) p.scopes in
let _beta_optimizations (p : 'm program) : 'm program =
let new_scopes = Dcalc.Ast.map_exprs_in_scopes ~f:(beta_expr ()) ~varf:(fun v -> v) p.scopes in
{ p with scopes = Bindlib.unbox new_scopes }
let rec peephole_expr (_ : unit) (e : expr Marked.pos) :
expr Marked.pos Bindlib.box =
let rec peephole_expr (_ : unit) (e : 'm marked_expr) :
'm marked_expr Bindlib.box =
let default_mark e' = Marked.mark (Marked.get_mark e) e' in
match Marked.unmark e with
@ -140,11 +140,11 @@ let rec peephole_expr (_ : unit) (e : expr Marked.pos) :
| _ -> default_mark @@ ECatch (e1, except, e2))
| _ -> visitor_map peephole_expr () e
let peephole_optimizations (p : program) : program =
let peephole_optimizations (p : 'm program) : 'm program =
let new_scopes =
Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ()) p.scopes
Dcalc.Ast.map_exprs_in_scopes ~f:(peephole_expr ()) ~varf:(fun v -> v) p.scopes
in
{ p with scopes = Bindlib.unbox new_scopes }
let optimize_program (p : program) : program =
let optimize_program (p : 'm program) : 'm program =
p |> iota_optimizations |> peephole_optimizations

4
compiler/lcalc/optimizations.mli
View File

@ -16,4 +16,6 @@
open Ast
val optimize_program : program -> program
val optimize_program : 'm program -> 'm program
(** Warning/todo: no effort was yet made to ensure
correct propagation of type annotations in the typed case *)

48
compiler/lcalc/print.ml
View File

@ -68,19 +68,19 @@ let format_keyword (fmt : Format.formatter) (s : string) : unit =
let format_punctuation (fmt : Format.formatter) (s : string) : unit =
Format.fprintf fmt "%a" (Utils.Cli.format_with_style [ANSITerminal.cyan]) s
let needs_parens (e : expr Marked.pos) : bool =
let needs_parens (e : 'm marked_expr) : bool =
match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
let format_var (fmt : Format.formatter) (v : 'm Ast.var) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let rec format_expr
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(e : expr Marked.pos) : unit =
(e : 'm marked_expr) : unit =
let format_expr = format_expr ctx ~debug in
let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) =
let format_with_parens (fmt : Format.formatter) (e : 'm marked_expr) =
if needs_parens e then
Format.fprintf fmt "%a%a%a" format_punctuation "(" format_expr e
format_punctuation ")"
@ -136,23 +136,21 @@ let rec format_expr
format_expr e))
(List.combine es
(List.map fst (Dcalc.Ast.EnumMap.find e_name ctx.ctx_enums)))
| ELit l -> Format.fprintf fmt "%a" format_lit (Marked.same_mark_as l e)
| ELit l -> Format.fprintf fmt "%a" format_lit (Marked.mark (Dcalc.Ast.pos e) l)
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
(fun fmt (x, tau, arg) ->
(fun fmt ((x, tau), arg) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@ %a@]@\n"
format_keyword "let" format_var x format_punctuation ":"
(Dcalc.Print.format_typ ctx)
tau format_punctuation "=" format_expr arg format_keyword "in"))
xs_tau_arg format_expr body
(Marked.unmark tau) format_punctuation "=" format_expr arg format_keyword "in"))
(List.combine (List.combine (Array.to_list xs) taus) args)
format_expr body
| EAbs (binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>%a %a %a@ %a@]" format_punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -160,21 +158,22 @@ let rec format_expr
Format.fprintf fmt "%a%a%a %a%a" format_punctuation "(" format_var x
format_punctuation ":"
(Dcalc.Print.format_typ ctx)
tau format_punctuation ")"))
xs_tau format_punctuation "→" format_expr body
(Marked.unmark tau) format_punctuation ")"))
(List.combine (Array.to_list xs) taus)
format_punctuation "→" format_expr body
| EApp
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2
op format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2
Dcalc.Print.format_binop op format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Dcalc.Print.format_unop
(op, Pos.no_pos) format_with_parens arg1
op format_with_parens arg1
| EApp (f, args) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_expr f
(Format.pp_print_list
@ -186,11 +185,11 @@ let rec format_expr
format_expr e1 format_keyword "then" format_expr e2 format_keyword "else"
format_expr e3
| EOp (Ternop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_ternop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_ternop op
| EOp (Binop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_binop op
| EOp (Unop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_unop op
| ECatch (e1, exn, e2) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a ->@ %a@]" format_keyword "try"
format_with_parens e1 format_keyword "with" format_exception exn
@ -202,14 +201,13 @@ let rec format_expr
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" format_keyword "assert"
format_punctuation "(" format_expr e' format_punctuation ")"
let format_scope
?(debug : bool = false)
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
((n, s) : Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body) : unit =
let format_scope ?(debug=false) ctx fmt (n, s) =
Format.fprintf fmt "@[<hov 2>%a %a =@ %a@]" format_keyword "let"
Dcalc.Ast.ScopeName.format_t n (format_expr ctx ~debug)
(Bindlib.unbox
(Dcalc.Ast.build_whole_scope_expr ~make_abs:Ast.make_abs
~make_let_in:Ast.make_let_in ~box_expr:Ast.box_expr ctx s
(Marked.get_mark (Dcalc.Ast.ScopeName.get_info n))))
(Dcalc.Ast.map_mark
(fun _ -> Marked.get_mark (Dcalc.Ast.ScopeName.get_info n))
(fun ty -> ty)
(Dcalc.Ast.get_scope_body_mark s))))

6
compiler/lcalc/print.mli
View File

@ -24,19 +24,19 @@ val begins_with_uppercase : string -> bool
(** {1 Formatters} *)
val format_lit : Format.formatter -> Ast.lit Marked.pos -> unit
val format_var : Format.formatter -> Ast.Var.t -> unit
val format_var : Format.formatter -> 'm Ast.var -> unit
val format_exception : Format.formatter -> Ast.except -> unit
val format_expr :
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Ast.expr Marked.pos ->
'm Ast.marked_expr ->
unit
val format_scope :
?debug:bool ->
Dcalc.Ast.decl_ctx ->
Format.formatter ->
Dcalc.Ast.ScopeName.t * Ast.expr Dcalc.Ast.scope_body ->
Dcalc.Ast.ScopeName.t * ('m Ast.expr, 'm) Dcalc.Ast.scope_body ->
unit

29
compiler/lcalc/to_ocaml.ml
View File

@ -40,13 +40,13 @@ let find_enum (en : D.EnumName.t) (ctx : D.decl_ctx) :
let format_lit (fmt : Format.formatter) (l : lit Marked.pos) : unit =
match Marked.unmark l with
| LBool b ->
Dcalc.Print.format_lit fmt (Marked.same_mark_as (Dcalc.Ast.LBool b) l)
Dcalc.Print.format_lit fmt (Dcalc.Ast.LBool b)
| LInt i ->
Format.fprintf fmt "integer_of_string@ \"%s\"" (Runtime.integer_to_string i)
| LUnit -> Dcalc.Print.format_lit fmt (Marked.same_mark_as Dcalc.Ast.LUnit l)
| LUnit -> Dcalc.Print.format_lit fmt Dcalc.Ast.LUnit
| LRat i ->
Format.fprintf fmt "decimal_of_string \"%a\"" Dcalc.Print.format_lit
(Marked.same_mark_as (Dcalc.Ast.LRat i) l)
(Dcalc.Ast.LRat i)
| LMoney e ->
Format.fprintf fmt "money_of_cents_string@ \"%s\""
(Runtime.integer_to_string (Runtime.money_to_cents e))
@ -221,7 +221,7 @@ let rec format_typ (fmt : Format.formatter) (typ : Dcalc.Ast.typ Marked.pos) :
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ_with_parens t1
| TAny -> Format.fprintf fmt "_"
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
let format_var (fmt : Format.formatter) (v : 'm var) : unit =
let lowercase_name = to_lowercase (to_ascii (Bindlib.name_of v)) in
let lowercase_name =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\\.")
@ -236,7 +236,7 @@ let format_var (fmt : Format.formatter) (v : Var.t) : unit =
else if lowercase_name = "_" then Format.fprintf fmt "%s" lowercase_name
else Format.fprintf fmt "%s_" lowercase_name
let needs_parens (e : expr Marked.pos) : bool =
let needs_parens (e : 'm marked_expr) : bool =
match Marked.unmark e with
| EApp ((EAbs (_, _), _), _)
| ELit (LBool _ | LUnit)
@ -261,9 +261,9 @@ let format_exception (fmt : Format.formatter) (exc : except Marked.pos) : unit =
let rec format_expr
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(e : expr Marked.pos) : unit =
(e : 'm marked_expr) : unit =
let format_expr = format_expr ctx in
let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) =
let format_with_parens (fmt : Format.formatter) (e : 'm marked_expr) =
if needs_parens e then Format.fprintf fmt "(%a)" format_expr e
else Format.fprintf fmt "%a" format_expr e
in
@ -326,7 +326,7 @@ let rec format_expr
(* should not happen *))
e))
(List.combine es (List.map fst (find_enum e_name ctx)))
| ELit l -> Format.fprintf fmt "%a" format_lit (Marked.same_mark_as l e)
| ELit l -> Format.fprintf fmt "%a" format_lit (Marked.mark (D.pos e) l)
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
@ -363,8 +363,9 @@ let rec format_expr
when !Cli.trace_flag ->
Format.fprintf fmt "(log_variable_definition@ %a@ (%a)@ %a)" format_uid_list
info typ_embedding_name (tau, Pos.no_pos) format_with_parens arg1
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), pos), [arg1])
| EApp ((EOp (Unop (D.Log (D.PosRecordIfTrueBool, _))), m), [arg1])
when !Cli.trace_flag ->
let pos = D.mark_pos m in
Format.fprintf fmt
"(log_decision_taken@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a)"
@ -398,11 +399,11 @@ let rec format_expr
"@[<hov 2>if @ %a@ then@ ()@ else@ raise AssertionFailed@]"
format_with_parens e'
| ERaise exc ->
Format.fprintf fmt "raise@ %a" format_exception (exc, Marked.get_mark e)
Format.fprintf fmt "raise@ %a" format_exception (exc, D.pos e)
| ECatch (e1, exc, e2) ->
Format.fprintf fmt "@[<hov 2>try@ %a@ with@ %a@ ->@ %a@]" format_with_parens
e1 format_exception
(exc, Marked.get_mark e)
(exc, D.pos e)
format_with_parens e2
let format_struct_embedding
@ -510,7 +511,7 @@ let format_ctx
let rec format_scope_body_expr
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(scope_lets : Ast.expr Dcalc.Ast.scope_body_expr) : unit =
(scope_lets : ('m Ast.expr, 'm) Dcalc.Ast.scope_body_expr) : unit =
match scope_lets with
| Dcalc.Ast.Result e -> format_expr ctx fmt e
| Dcalc.Ast.ScopeLet scope_let ->
@ -526,7 +527,7 @@ let rec format_scope_body_expr
let rec format_scopes
(ctx : Dcalc.Ast.decl_ctx)
(fmt : Format.formatter)
(scopes : Ast.expr Dcalc.Ast.scopes) : unit =
(scopes : ('m Ast.expr, 'm) Dcalc.Ast.scopes) : unit =
match scopes with
| Dcalc.Ast.Nil -> ()
| Dcalc.Ast.ScopeDef scope_def ->
@ -543,7 +544,7 @@ let rec format_scopes
let format_program
(fmt : Format.formatter)
(p : Ast.program)
(p : 'm Ast.program)
(type_ordering : Scopelang.Dependency.TVertex.t list) : unit =
Cli.style_flag := false;
Format.fprintf fmt

2
compiler/lcalc/to_ocaml.mli
View File

@ -17,5 +17,5 @@
(** Formats a lambda calculus program into a valid OCaml program *)
val format_program :
Format.formatter -> Ast.program -> Scopelang.Dependency.TVertex.t list -> unit
Format.formatter -> 'm Ast.program -> Scopelang.Dependency.TVertex.t list -> unit
(** Usage [format_program fmt p type_dependencies_ordering] *)

2
compiler/plugin.ml
View File

@ -20,7 +20,7 @@ type 'ast gen = {
apply : string option -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit;
}
type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen
type t = Lcalc of Dcalc.Ast.typed Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen
let name = function Lcalc { name; _ } | Scalc { name; _ } -> name
let backend_plugins : (string, t) Hashtbl.t = Hashtbl.create 17

6
compiler/plugin.mli
View File

@ -22,7 +22,9 @@ type 'ast gen = {
apply : string option -> 'ast -> Scopelang.Dependency.TVertex.t list -> unit;
}
type t = Lcalc of Lcalc.Ast.program gen | Scalc of Scalc.Ast.program gen
type t =
| Lcalc of Dcalc.Ast.typed Lcalc.Ast.program gen
| Scalc of Scalc.Ast.program gen
val find : string -> t
(** Find a registered plugin *)
@ -40,7 +42,7 @@ module PluginAPI : sig
name:string ->
extension:string ->
(string option ->
Lcalc.Ast.program ->
Dcalc.Ast.typed Lcalc.Ast.program ->
Scopelang.Dependency.TVertex.t list ->
unit) ->
unit

75
compiler/scalc/compile_from_lambda.ml
View File

@ -29,15 +29,15 @@ type ctxt = {
(* Expressions can spill out side effect, hence this function also returns a
list of statements to be prepended before the expression is evaluated *)
let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
let rec translate_expr (ctxt : ctxt) (expr : 'm L.marked_expr) :
A.block * A.expr Marked.pos =
match Marked.unmark expr with
| L.EVar v ->
let local_var =
try A.EVar (L.VarMap.find v ctxt.var_dict)
with Not_found -> A.EFunc (L.VarMap.find v ctxt.func_dict)
try A.EVar (L.VarMap.find (L.Var.t v) ctxt.var_dict)
with Not_found -> A.EFunc (L.VarMap.find (L.Var.t v) ctxt.func_dict)
in
[], (local_var, Marked.get_mark expr)
[], (local_var, D.pos expr)
| L.ETuple (args, Some s_name) ->
let args_stmts, new_args =
List.fold_left
@ -48,7 +48,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
in
let new_args = List.rev new_args in
let args_stmts = List.rev args_stmts in
args_stmts, (A.EStruct (new_args, s_name), Marked.get_mark expr)
args_stmts, (A.EStruct (new_args, s_name), D.pos expr)
| L.ETuple (_, None) ->
failwith "Non-struct tuples cannot be compiled to scalc"
| L.ETupleAccess (e1, num_field, Some s_name, _) ->
@ -58,7 +58,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
(List.nth (D.StructMap.find s_name ctxt.decl_ctx.ctx_structs) num_field)
in
( e1_stmts,
(A.EStructFieldAccess (new_e1, field_name, s_name), Marked.get_mark expr)
(A.EStructFieldAccess (new_e1, field_name, s_name), D.pos expr)
)
| L.ETupleAccess (_, _, None, _) ->
failwith "Non-struct tuples cannot be compiled to scalc"
@ -67,7 +67,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
let cons_name =
fst (List.nth (D.EnumMap.find e_name ctxt.decl_ctx.ctx_enums) num_cons)
in
e1_stmts, (A.EInj (new_e1, cons_name, e_name), Marked.get_mark expr)
e1_stmts, (A.EInj (new_e1, cons_name, e_name), D.pos expr)
| L.EApp (f, args) ->
let f_stmts, new_f = translate_expr ctxt f in
let args_stmts, new_args =
@ -78,7 +78,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
([], []) args
in
let new_args = List.rev new_args in
f_stmts @ args_stmts, (A.EApp (new_f, new_args), Marked.get_mark expr)
f_stmts @ args_stmts, (A.EApp (new_f, new_args), D.pos expr)
| L.EArray args ->
let args_stmts, new_args =
List.fold_left
@ -88,9 +88,9 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
([], []) args
in
let new_args = List.rev new_args in
args_stmts, (A.EArray new_args, Marked.get_mark expr)
| L.EOp op -> [], (A.EOp op, Marked.get_mark expr)
| L.ELit l -> [], (A.ELit l, Marked.get_mark expr)
args_stmts, (A.EArray new_args, D.pos expr)
| L.EOp op -> [], (A.EOp op, D.pos expr)
| L.ELit l -> [], (A.ELit l, D.pos expr)
| _ ->
let tmp_var =
A.LocalName.fresh
@ -103,7 +103,7 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
let v = Marked.unmark (A.LocalName.get_info v) in
let tmp_rex = Re.Pcre.regexp "^temp_" in
if Re.Pcre.pmatch ~rex:tmp_rex v then v else "temp_" ^ v),
Marked.get_mark expr )
D.pos expr )
in
let ctxt =
{
@ -114,20 +114,21 @@ let rec translate_expr (ctxt : ctxt) (expr : L.expr Marked.pos) :
in
let tmp_stmts = translate_statements ctxt expr in
( ( A.SLocalDecl
((tmp_var, Marked.get_mark expr), (D.TAny, Marked.get_mark expr)),
Marked.get_mark expr )
((tmp_var, D.pos expr), (D.TAny, D.pos expr)),
D.pos expr )
:: tmp_stmts,
(A.EVar tmp_var, Marked.get_mark expr) )
(A.EVar tmp_var, D.pos expr) )
and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
and translate_statements (ctxt : ctxt) (block_expr : 'm L.marked_expr) :
A.block =
match Marked.unmark block_expr with
| L.EAssert e ->
(* Assertions are always encapsulated in a unit-typed let binding *)
let e_stmts, new_e = translate_expr ctxt e in
e_stmts @ [A.SAssert (Marked.unmark new_e), Marked.get_mark block_expr]
| L.EApp ((L.EAbs (binder, taus), binder_pos), args) ->
e_stmts @ [A.SAssert (Marked.unmark new_e), D.pos block_expr]
| L.EApp ((L.EAbs (binder, taus), binder_mark), args) ->
(* This defines multiple local variables at the time *)
let binder_pos = D.mark_pos binder_mark in
let vars, body = Bindlib.unmbind binder in
let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in
let ctxt =
@ -136,7 +137,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
var_dict =
List.fold_left
(fun var_dict (x, _) ->
L.VarMap.add x
L.VarMap.add (L.Var.t x)
(A.LocalName.fresh (Bindlib.name_of x, binder_pos))
var_dict)
ctxt.var_dict vars_tau;
@ -145,14 +146,14 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
let local_decls =
List.map
(fun (x, tau) ->
( A.SLocalDecl ((L.VarMap.find x ctxt.var_dict, binder_pos), tau),
( A.SLocalDecl ((L.VarMap.find (L.Var.t x) ctxt.var_dict, binder_pos), tau),
binder_pos ))
vars_tau
in
let vars_args =
List.map2
(fun (x, tau) arg ->
(L.VarMap.find x ctxt.var_dict, binder_pos), tau, arg)
(L.VarMap.find (L.Var.t x) ctxt.var_dict, binder_pos), tau, arg)
vars_tau args
in
let def_blocks =
@ -174,11 +175,11 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
local_decls @ List.flatten def_blocks @ rest_of_block
| L.EAbs (binder, taus) ->
let vars, body = Bindlib.unmbind binder in
let binder_pos = Marked.get_mark block_expr in
let binder_pos = D.pos block_expr in
let vars_tau = List.map2 (fun x tau -> x, tau) (Array.to_list vars) taus in
let closure_name =
match ctxt.inside_definition_of with
| None -> A.LocalName.fresh (ctxt.context_name, Marked.get_mark block_expr)
| None -> A.LocalName.fresh (ctxt.context_name, D.pos block_expr)
| Some x -> x
in
let ctxt =
@ -187,7 +188,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
var_dict =
List.fold_left
(fun var_dict (x, _) ->
L.VarMap.add x
L.VarMap.add (L.Var.t x)
(A.LocalName.fresh (Bindlib.name_of x, binder_pos))
var_dict)
ctxt.var_dict vars_tau;
@ -202,7 +203,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
func_params =
List.map
(fun (var, tau) ->
(L.VarMap.find var ctxt.var_dict, binder_pos), tau)
(L.VarMap.find (L.Var.t var) ctxt.var_dict, binder_pos), tau)
vars_tau;
func_body = new_body;
} ),
@ -219,10 +220,10 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
assert (Array.length vars = 1);
let var = vars.(0) in
let scalc_var =
A.LocalName.fresh (Bindlib.name_of var, Marked.get_mark arg)
A.LocalName.fresh (Bindlib.name_of var, D.pos arg)
in
let ctxt =
{ ctxt with var_dict = L.VarMap.add var scalc_var ctxt.var_dict }
{ ctxt with var_dict = L.VarMap.add (L.Var.t var) scalc_var ctxt.var_dict }
in
let new_arg = translate_statements ctxt body in
(new_arg, scalc_var) :: new_args
@ -232,18 +233,18 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
in
let new_args = List.rev new_args in
e1_stmts
@ [A.SSwitch (new_e1, e_name, new_args), Marked.get_mark block_expr]
@ [A.SSwitch (new_e1, e_name, new_args), D.pos block_expr]
| L.EIfThenElse (cond, e_true, e_false) ->
let cond_stmts, s_cond = translate_expr ctxt cond in
let s_e_true = translate_statements ctxt e_true in
let s_e_false = translate_statements ctxt e_false in
cond_stmts
@ [A.SIfThenElse (s_cond, s_e_true, s_e_false), Marked.get_mark block_expr]
@ [A.SIfThenElse (s_cond, s_e_true, s_e_false), D.pos block_expr]
| L.ECatch (e_try, except, e_catch) ->
let s_e_try = translate_statements ctxt e_try in
let s_e_catch = translate_statements ctxt e_catch in
[A.STryExcept (s_e_try, except, s_e_catch), Marked.get_mark block_expr]
| L.ERaise except -> [A.SRaise except, Marked.get_mark block_expr]
[A.STryExcept (s_e_try, except, s_e_catch), D.pos block_expr]
| L.ERaise except -> [A.SRaise except, D.pos block_expr]
| _ -> (
let e_stmts, new_e = translate_expr ctxt block_expr in
e_stmts
@ -259,7 +260,7 @@ and translate_statements (ctxt : ctxt) (block_expr : L.expr Marked.pos) :
( (match ctxt.inside_definition_of with
| None -> A.SReturn (Marked.unmark new_e)
| Some x -> A.SLocalDef (Marked.same_mark_as x new_e, new_e)),
Marked.get_mark block_expr );
D.pos block_expr );
])
let rec translate_scope_body_expr
@ -267,7 +268,7 @@ let rec translate_scope_body_expr
(decl_ctx : D.decl_ctx)
(var_dict : A.LocalName.t L.VarMap.t)
(func_dict : A.TopLevelName.t L.VarMap.t)
(scope_expr : L.expr D.scope_body_expr) : A.block =
(scope_expr : ('m L.expr, 'm) D.scope_body_expr) : A.block =
match scope_expr with
| Result e ->
let block, new_e =
@ -287,7 +288,7 @@ let rec translate_scope_body_expr
let let_var_id =
A.LocalName.fresh (Bindlib.name_of let_var, scope_let.scope_let_pos)
in
let new_var_dict = L.VarMap.add let_var let_var_id var_dict in
let new_var_dict = L.VarMap.add (L.Var.t let_var) let_var_id var_dict in
(match scope_let.scope_let_kind with
| D.Assertion ->
translate_statements
@ -322,7 +323,7 @@ let rec translate_scope_body_expr
@ translate_scope_body_expr scope_name decl_ctx new_var_dict func_dict
scope_let_next
let translate_program (p : L.program) : A.program =
let translate_program (p : 'm L.program) : A.program =
{
decl_ctx = p.L.decl_ctx;
scopes =
@ -339,7 +340,7 @@ let translate_program (p : L.program) : A.program =
A.LocalName.fresh (Bindlib.name_of scope_input_var, input_pos)
in
let var_dict =
L.VarMap.singleton scope_input_var scope_input_var_id
L.VarMap.singleton (L.Var.t scope_input_var) scope_input_var_id
in
let new_scope_body =
translate_scope_body_expr scope_def.D.scope_name p.decl_ctx
@ -348,7 +349,7 @@ let translate_program (p : L.program) : A.program =
let func_id =
A.TopLevelName.fresh (Bindlib.name_of scope_var, Pos.no_pos)
in
let func_dict = L.VarMap.add scope_var func_id func_dict in
let func_dict = L.VarMap.add (L.Var.t scope_var) func_id func_dict in
( func_dict,
{
Ast.scope_body_name = scope_def.D.scope_name;

18
compiler/scalc/print.ml
View File

@ -80,15 +80,15 @@ let rec format_expr
((EOp (Binop ((Dcalc.Ast.Map | Dcalc.Ast.Filter) as op)), _), [arg1; arg2])
->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg1 format_with_parens arg2
op format_with_parens arg1 format_with_parens arg2
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop (op, Pos.no_pos) format_with_parens arg2
Dcalc.Print.format_binop op format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Dcalc.Print.format_unop
(op, Pos.no_pos) format_with_parens arg1
op format_with_parens arg1
| EApp (f, args) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_expr f
(Format.pp_print_list
@ -96,11 +96,11 @@ let rec format_expr
format_with_parens)
args
| EOp (Ternop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_ternop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_ternop op
| EOp (Binop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_binop op
| EOp (Unop op) ->
Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos)
Format.fprintf fmt "%a" Dcalc.Print.format_unop op
let rec format_statement
(decl_ctx : Dcalc.Ast.decl_ctx)
@ -118,7 +118,7 @@ let rec format_statement
Format.fprintf fmt "%a%a %a@ %a%a" Dcalc.Print.format_punctuation "("
LocalName.format_t name Dcalc.Print.format_punctuation ":"
(Dcalc.Print.format_typ decl_ctx)
typ Dcalc.Print.format_punctuation ")"))
(Marked.unmark typ) Dcalc.Print.format_punctuation ")"))
func.func_params Dcalc.Print.format_punctuation "="
(format_block decl_ctx ~debug)
func.func_body
@ -127,7 +127,7 @@ let rec format_statement
"decl" LocalName.format_t (Marked.unmark name)
Dcalc.Print.format_punctuation ":"
(Dcalc.Print.format_typ decl_ctx)
typ
(Marked.unmark typ)
| SLocalDef (name, expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" LocalName.format_t
(Marked.unmark name) Dcalc.Print.format_punctuation "="
@ -204,7 +204,7 @@ let format_scope
Format.fprintf fmt "%a%a %a@ %a%a" Dcalc.Print.format_punctuation "("
LocalName.format_t name Dcalc.Print.format_punctuation ":"
(Dcalc.Print.format_typ decl_ctx)
typ Dcalc.Print.format_punctuation ")"))
(Marked.unmark typ) Dcalc.Print.format_punctuation ")"))
body.scope_body_func.func_params Dcalc.Print.format_punctuation "="
(format_block decl_ctx ~debug)
body.scope_body_func.func_body

2
compiler/scalc/to_python.ml
View File

@ -30,7 +30,7 @@ let format_lit (fmt : Format.formatter) (l : L.lit Marked.pos) : unit =
| LUnit -> Format.fprintf fmt "Unit()"
| LRat i ->
Format.fprintf fmt "decimal_of_string(\"%a\")" Dcalc.Print.format_lit
(Marked.same_mark_as (Dcalc.Ast.LRat i) l)
(Dcalc.Ast.LRat i)
| LMoney e ->
Format.fprintf fmt "money_of_cents_string(\"%s\")"
(Runtime.integer_to_string (Runtime.money_to_cents e))

2
compiler/scopelang/scope_to_dcalc.ml
View File

@ -556,7 +556,7 @@ let translate_rule
should have been defined (even an empty definition, if they're
not defined by any rule in the source code) by the translation
from desugared to the scope language. *)
Bindlib.box Dcalc.Ast.empty_thunked_term
Bindlib.box (Dcalc.Ast.empty_thunked_term (Untyped {pos = pos_call}))
else
let a_var, _, _ =
Ast.ScopeVarMap.find subvar.scope_var_name subscope_vars_defined