2020-11-23 18:12:45 +03:00
|
|
|
(* This file is part of the Catala compiler, a specification language for tax and social benefits
|
|
|
|
computation rules. Copyright (C) 2020 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. *)
|
|
|
|
|
2021-01-21 23:33:04 +03:00
|
|
|
open Utils
|
2020-11-23 18:12:45 +03:00
|
|
|
|
2021-01-29 18:24:20 +03:00
|
|
|
type scope_sigs_ctx =
|
2021-02-01 17:57:19 +03:00
|
|
|
(* list of scope variables with their types *)
|
2021-03-23 12:59:43 +03:00
|
|
|
((Ast.ScopeVar.t * Dcalc.Ast.typ) list
|
2021-02-01 17:57:19 +03:00
|
|
|
* (* var representing the scope *) Dcalc.Ast.Var.t
|
|
|
|
* (* var representing the scope input inside the scope func *) Dcalc.Ast.Var.t
|
|
|
|
* (* scope input *) Ast.StructName.t
|
2021-03-23 12:59:43 +03:00
|
|
|
* (* scope output *) Ast.StructName.t)
|
2021-02-01 17:57:19 +03:00
|
|
|
Ast.ScopeMap.t
|
2020-11-26 19:06:32 +03:00
|
|
|
|
2020-11-23 20:51:06 +03:00
|
|
|
type ctx = {
|
2020-12-04 18:40:17 +03:00
|
|
|
structs : Ast.struct_ctx;
|
|
|
|
enums : Ast.enum_ctx;
|
2020-12-10 18:58:32 +03:00
|
|
|
scope_name : Ast.ScopeName.t;
|
2020-11-27 13:37:21 +03:00
|
|
|
scopes_parameters : scope_sigs_ctx;
|
2020-11-23 20:51:06 +03:00
|
|
|
scope_vars : (Dcalc.Ast.Var.t * Dcalc.Ast.typ) Ast.ScopeVarMap.t;
|
|
|
|
subscope_vars : (Dcalc.Ast.Var.t * Dcalc.Ast.typ) Ast.ScopeVarMap.t Ast.SubScopeMap.t;
|
|
|
|
local_vars : Dcalc.Ast.Var.t Ast.VarMap.t;
|
|
|
|
}
|
|
|
|
|
2020-12-04 18:40:17 +03:00
|
|
|
let empty_ctx (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx) (scopes_ctx : scope_sigs_ctx)
|
2020-12-10 18:58:32 +03:00
|
|
|
(scope_name : Ast.ScopeName.t) =
|
2020-11-23 20:51:06 +03:00
|
|
|
{
|
2020-12-04 16:41:20 +03:00
|
|
|
structs = struct_ctx;
|
|
|
|
enums = enum_ctx;
|
2020-12-10 18:58:32 +03:00
|
|
|
scope_name;
|
2020-11-26 19:06:32 +03:00
|
|
|
scopes_parameters = scopes_ctx;
|
2020-11-23 20:51:06 +03:00
|
|
|
scope_vars = Ast.ScopeVarMap.empty;
|
|
|
|
subscope_vars = Ast.SubScopeMap.empty;
|
|
|
|
local_vars = Ast.VarMap.empty;
|
|
|
|
}
|
2020-11-23 18:12:45 +03:00
|
|
|
|
2020-12-04 20:48:16 +03:00
|
|
|
let rec translate_typ (ctx : ctx) (t : Ast.typ Pos.marked) : Dcalc.Ast.typ Pos.marked =
|
|
|
|
Pos.same_pos_as
|
2021-03-23 12:59:43 +03:00
|
|
|
(match Pos.unmark t with
|
2020-12-09 16:51:22 +03:00
|
|
|
| Ast.TLit l -> Dcalc.Ast.TLit l
|
2020-12-04 20:48:16 +03:00
|
|
|
| Ast.TArrow (t1, t2) -> Dcalc.Ast.TArrow (translate_typ ctx t1, translate_typ ctx t2)
|
|
|
|
| Ast.TStruct s_uid ->
|
|
|
|
let s_fields = Ast.StructMap.find s_uid ctx.structs in
|
2021-01-14 02:17:24 +03:00
|
|
|
Dcalc.Ast.TTuple (List.map (fun (_, t) -> translate_typ ctx t) s_fields, Some s_uid)
|
2020-12-04 20:48:16 +03:00
|
|
|
| Ast.TEnum e_uid ->
|
|
|
|
let e_cases = Ast.EnumMap.find e_uid ctx.enums in
|
2021-01-14 02:17:24 +03:00
|
|
|
Dcalc.Ast.TEnum (List.map (fun (_, t) -> translate_typ ctx t) e_cases, e_uid)
|
2020-12-30 00:26:10 +03:00
|
|
|
| Ast.TArray t1 -> Dcalc.Ast.TArray (translate_typ ctx (Pos.same_pos_as t1 t))
|
2021-03-23 12:59:43 +03:00
|
|
|
| Ast.TAny -> Dcalc.Ast.TAny)
|
2020-12-04 20:48:16 +03:00
|
|
|
t
|
|
|
|
|
2020-11-26 17:48:26 +03:00
|
|
|
let merge_defaults (caller : Dcalc.Ast.expr Pos.marked Bindlib.box)
|
|
|
|
(callee : Dcalc.Ast.expr Pos.marked Bindlib.box) : Dcalc.Ast.expr Pos.marked Bindlib.box =
|
|
|
|
let caller =
|
|
|
|
Dcalc.Ast.make_app caller
|
|
|
|
[ Bindlib.box (Dcalc.Ast.ELit Dcalc.Ast.LUnit, Pos.no_pos) ]
|
|
|
|
Pos.no_pos
|
|
|
|
in
|
|
|
|
let body =
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun caller callee ->
|
|
|
|
( Dcalc.Ast.EDefault
|
2020-12-18 17:59:15 +03:00
|
|
|
([ caller ], (Dcalc.Ast.ELit (Dcalc.Ast.LBool true), Pos.no_pos), callee),
|
2020-11-26 17:48:26 +03:00
|
|
|
Pos.no_pos ))
|
|
|
|
caller callee
|
|
|
|
in
|
2020-11-27 13:54:22 +03:00
|
|
|
body
|
2020-11-23 18:12:45 +03:00
|
|
|
|
2021-01-21 23:33:04 +03:00
|
|
|
let tag_with_log_entry (e : Dcalc.Ast.expr Pos.marked Bindlib.box) (l : Dcalc.Ast.log_entry)
|
|
|
|
(markings : Utils.Uid.MarkedString.info list) : Dcalc.Ast.expr Pos.marked Bindlib.box =
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun e ->
|
|
|
|
( Dcalc.Ast.EApp
|
|
|
|
((Dcalc.Ast.EOp (Dcalc.Ast.Unop (Dcalc.Ast.Log (l, markings))), Pos.get_position e), [ e ]),
|
|
|
|
Pos.get_position e ))
|
|
|
|
e
|
|
|
|
|
2020-11-26 15:38:42 +03:00
|
|
|
let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) : Dcalc.Ast.expr Pos.marked Bindlib.box
|
|
|
|
=
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun (x : Dcalc.Ast.expr) -> Pos.same_pos_as x e)
|
2021-03-23 12:59:43 +03:00
|
|
|
(match Pos.unmark e with
|
2020-11-27 20:36:38 +03:00
|
|
|
| EVar v -> Bindlib.box_var (Ast.VarMap.find (Pos.unmark v) ctx.local_vars)
|
2020-11-26 15:38:42 +03:00
|
|
|
| ELit l -> Bindlib.box (Dcalc.Ast.ELit l)
|
2020-12-04 16:41:20 +03:00
|
|
|
| EStruct (struct_name, e_fields) ->
|
|
|
|
let struct_sig = Ast.StructMap.find struct_name ctx.structs in
|
|
|
|
let d_fields, remaining_e_fields =
|
|
|
|
List.fold_right
|
|
|
|
(fun (field_name, _) (d_fields, e_fields) ->
|
2021-04-29 18:46:56 +03:00
|
|
|
let field_e = Ast.StructFieldMap.find field_name e_fields in
|
2020-12-04 16:41:20 +03:00
|
|
|
let field_d = translate_expr ctx field_e in
|
|
|
|
(field_d :: d_fields, Ast.StructFieldMap.remove field_name e_fields))
|
|
|
|
struct_sig ([], e_fields)
|
|
|
|
in
|
|
|
|
if Ast.StructFieldMap.cardinal remaining_e_fields > 0 then
|
|
|
|
Errors.raise_spanned_error
|
2021-01-03 22:36:04 +03:00
|
|
|
(Format.asprintf "The fields \"%a\" do not belong to the structure %a"
|
|
|
|
Ast.StructName.format_t struct_name
|
2020-12-04 16:41:20 +03:00
|
|
|
(Format.pp_print_list
|
|
|
|
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
|
|
|
|
(fun fmt (field_name, _) ->
|
|
|
|
Format.fprintf fmt "%a" Ast.StructFieldName.format_t field_name))
|
|
|
|
(Ast.StructFieldMap.bindings remaining_e_fields))
|
|
|
|
(Pos.get_position e)
|
|
|
|
else
|
2021-01-14 02:17:24 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun d_fields -> Dcalc.Ast.ETuple (d_fields, Some struct_name))
|
|
|
|
(Bindlib.box_list d_fields)
|
2020-12-04 16:41:20 +03:00
|
|
|
| EStructAccess (e1, field_name, struct_name) ->
|
|
|
|
let struct_sig = Ast.StructMap.find struct_name ctx.structs in
|
|
|
|
let _, field_index =
|
2020-12-05 19:27:08 +03:00
|
|
|
try List.assoc field_name (List.mapi (fun i (x, y) -> (x, (y, i))) struct_sig)
|
|
|
|
with Not_found ->
|
|
|
|
Errors.raise_spanned_error
|
2021-01-03 22:36:04 +03:00
|
|
|
(Format.asprintf "The field \"%a\" does not belong to the structure %a"
|
2020-12-05 19:27:08 +03:00
|
|
|
Ast.StructFieldName.format_t field_name Ast.StructName.format_t struct_name)
|
|
|
|
(Pos.get_position e)
|
2020-12-04 16:41:20 +03:00
|
|
|
in
|
|
|
|
let e1 = translate_expr ctx e1 in
|
2020-12-05 20:12:53 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun e1 ->
|
2021-01-05 17:33:30 +03:00
|
|
|
Dcalc.Ast.ETupleAccess
|
|
|
|
( e1,
|
|
|
|
field_index,
|
2021-01-14 02:17:24 +03:00
|
|
|
Some struct_name,
|
2021-01-05 17:33:30 +03:00
|
|
|
List.map (fun (_, t) -> translate_typ ctx t) struct_sig ))
|
2020-12-05 20:12:53 +03:00
|
|
|
e1
|
2020-12-04 16:41:20 +03:00
|
|
|
| EEnumInj (e1, constructor, enum_name) ->
|
|
|
|
let enum_sig = Ast.EnumMap.find enum_name ctx.enums in
|
|
|
|
let _, constructor_index =
|
2020-12-05 19:27:08 +03:00
|
|
|
try List.assoc constructor (List.mapi (fun i (x, y) -> (x, (y, i))) enum_sig)
|
|
|
|
with Not_found ->
|
|
|
|
Errors.raise_spanned_error
|
2021-01-03 22:36:04 +03:00
|
|
|
(Format.asprintf "The constructor \"%a\" does not belong to the enum %a"
|
2020-12-05 19:27:08 +03:00
|
|
|
Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
|
|
|
|
(Pos.get_position e)
|
2020-12-04 16:41:20 +03:00
|
|
|
in
|
|
|
|
let e1 = translate_expr ctx e1 in
|
|
|
|
Bindlib.box_apply
|
2020-12-04 20:48:16 +03:00
|
|
|
(fun e1 ->
|
|
|
|
Dcalc.Ast.EInj
|
2020-12-05 20:12:53 +03:00
|
|
|
( e1,
|
|
|
|
constructor_index,
|
2021-01-14 02:17:24 +03:00
|
|
|
enum_name,
|
2020-12-05 20:12:53 +03:00
|
|
|
List.map (fun (_, t) -> translate_typ ctx t) enum_sig ))
|
2020-12-04 16:41:20 +03:00
|
|
|
e1
|
|
|
|
| EMatch (e1, enum_name, cases) ->
|
|
|
|
let enum_sig = Ast.EnumMap.find enum_name ctx.enums in
|
|
|
|
let d_cases, remaining_e_cases =
|
|
|
|
List.fold_right
|
|
|
|
(fun (constructor, _) (d_cases, e_cases) ->
|
|
|
|
let case_e =
|
2020-12-05 20:12:53 +03:00
|
|
|
try Ast.EnumConstructorMap.find constructor e_cases
|
|
|
|
with Not_found ->
|
|
|
|
Errors.raise_spanned_error
|
2020-12-09 12:36:09 +03:00
|
|
|
(Format.asprintf
|
|
|
|
"The constructor %a of enum %a is missing from this pattern matching"
|
2020-12-05 20:12:53 +03:00
|
|
|
Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
|
|
|
|
(Pos.get_position e)
|
2020-12-04 16:41:20 +03:00
|
|
|
in
|
|
|
|
let case_d = translate_expr ctx case_e in
|
|
|
|
(case_d :: d_cases, Ast.EnumConstructorMap.remove constructor e_cases))
|
|
|
|
enum_sig ([], cases)
|
|
|
|
in
|
|
|
|
if Ast.EnumConstructorMap.cardinal remaining_e_cases > 0 then
|
|
|
|
Errors.raise_spanned_error
|
|
|
|
(Format.asprintf "Patter matching is incomplete for enum %a: missing cases %a"
|
|
|
|
Ast.EnumName.format_t enum_name
|
|
|
|
(Format.pp_print_list
|
|
|
|
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
|
|
|
|
(fun fmt (case_name, _) ->
|
|
|
|
Format.fprintf fmt "%a" Ast.EnumConstructor.format_t case_name))
|
|
|
|
(Ast.EnumConstructorMap.bindings remaining_e_cases))
|
|
|
|
(Pos.get_position e)
|
|
|
|
else
|
|
|
|
let e1 = translate_expr ctx e1 in
|
|
|
|
Bindlib.box_apply2
|
2021-01-14 02:17:24 +03:00
|
|
|
(fun d_fields e1 -> Dcalc.Ast.EMatch (e1, d_fields, enum_name))
|
2020-12-04 16:41:20 +03:00
|
|
|
(Bindlib.box_list d_cases) e1
|
2020-11-26 15:38:42 +03:00
|
|
|
| EApp (e1, args) ->
|
2021-01-21 01:29:50 +03:00
|
|
|
(* We insert various log calls to record arguments and outputs of user-defined functions
|
|
|
|
belonging to scopes *)
|
|
|
|
let e1_func = translate_expr ctx e1 in
|
|
|
|
let markings l =
|
|
|
|
match l with
|
|
|
|
| Ast.ScopeVar (v, _) ->
|
|
|
|
[ Ast.ScopeName.get_info ctx.scope_name; Ast.ScopeVar.get_info v ]
|
|
|
|
| Ast.SubScopeVar (s, _, (v, _)) -> [ Ast.ScopeName.get_info s; Ast.ScopeVar.get_info v ]
|
|
|
|
in
|
|
|
|
let e1_func =
|
|
|
|
match Pos.unmark e1 with
|
2021-01-21 23:33:04 +03:00
|
|
|
| ELocation l -> tag_with_log_entry e1_func Dcalc.Ast.BeginCall (markings l)
|
2021-01-21 01:29:50 +03:00
|
|
|
| _ -> e1_func
|
|
|
|
in
|
|
|
|
let new_args = List.map (translate_expr ctx) args in
|
|
|
|
let new_args =
|
|
|
|
match (Pos.unmark e1, new_args) with
|
|
|
|
| ELocation l, [ new_arg ] ->
|
|
|
|
[
|
2021-04-05 20:06:32 +03:00
|
|
|
tag_with_log_entry new_arg (Dcalc.Ast.VarDef Dcalc.Ast.TAny)
|
2021-01-21 23:33:04 +03:00
|
|
|
(markings l @ [ Pos.same_pos_as "input" e ]);
|
2021-01-21 01:29:50 +03:00
|
|
|
]
|
|
|
|
| _ -> new_args
|
|
|
|
in
|
|
|
|
let new_e =
|
2021-01-21 23:33:04 +03:00
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun e' u -> (Dcalc.Ast.EApp (e', u), Pos.get_position e))
|
|
|
|
e1_func (Bindlib.box_list new_args)
|
2021-01-21 01:29:50 +03:00
|
|
|
in
|
|
|
|
let new_e =
|
|
|
|
match Pos.unmark e1 with
|
|
|
|
| ELocation l ->
|
2021-01-21 23:33:04 +03:00
|
|
|
tag_with_log_entry
|
2021-04-05 20:06:32 +03:00
|
|
|
(tag_with_log_entry new_e (Dcalc.Ast.VarDef Dcalc.Ast.TAny)
|
2021-01-21 23:33:04 +03:00
|
|
|
(markings l @ [ Pos.same_pos_as "output" e ]))
|
|
|
|
Dcalc.Ast.EndCall (markings l)
|
2021-01-21 01:29:50 +03:00
|
|
|
| _ -> new_e
|
|
|
|
in
|
2021-01-21 23:33:04 +03:00
|
|
|
Bindlib.box_apply Pos.unmark new_e
|
2021-04-03 12:49:13 +03:00
|
|
|
| EAbs ((binder, pos_binder), typ) ->
|
2020-11-24 12:28:39 +03:00
|
|
|
let xs, body = Bindlib.unmbind binder in
|
2020-11-27 20:36:38 +03:00
|
|
|
let new_xs = Array.map (fun x -> Dcalc.Ast.Var.make (Bindlib.name_of x, Pos.no_pos)) xs in
|
2020-11-24 12:28:39 +03:00
|
|
|
let both_xs = Array.map2 (fun x new_x -> (x, new_x)) xs new_xs in
|
2020-11-23 20:51:06 +03:00
|
|
|
let body =
|
2020-11-24 12:28:39 +03:00
|
|
|
translate_expr
|
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
local_vars =
|
|
|
|
Array.fold_left
|
|
|
|
(fun local_vars (x, new_x) -> Ast.VarMap.add x new_x local_vars)
|
|
|
|
ctx.local_vars both_xs;
|
|
|
|
}
|
|
|
|
body
|
2020-11-23 20:51:06 +03:00
|
|
|
in
|
2020-11-26 15:38:42 +03:00
|
|
|
let binder = Bindlib.bind_mvar new_xs body in
|
2020-12-04 20:48:16 +03:00
|
|
|
Bindlib.box_apply
|
2021-04-03 12:49:13 +03:00
|
|
|
(fun b -> Dcalc.Ast.EAbs ((b, pos_binder), List.map (translate_typ ctx) typ))
|
2020-12-04 20:48:16 +03:00
|
|
|
binder
|
2020-12-18 17:59:15 +03:00
|
|
|
| EDefault (excepts, just, cons) ->
|
2021-01-21 23:33:04 +03:00
|
|
|
let just = tag_with_log_entry (translate_expr ctx just) Dcalc.Ast.PosRecordIfTrueBool [] in
|
2020-11-26 15:38:42 +03:00
|
|
|
Bindlib.box_apply3
|
2021-01-21 23:33:04 +03:00
|
|
|
(fun e j c -> Dcalc.Ast.EDefault (e, j, c))
|
2020-12-18 17:59:15 +03:00
|
|
|
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
|
2021-01-21 23:33:04 +03:00
|
|
|
just (translate_expr ctx cons)
|
2020-11-23 20:51:06 +03:00
|
|
|
| ELocation (ScopeVar a) ->
|
2020-11-27 20:36:38 +03:00
|
|
|
Bindlib.box_var (fst (Ast.ScopeVarMap.find (Pos.unmark a) ctx.scope_vars))
|
2020-11-27 13:37:21 +03:00
|
|
|
| ELocation (SubScopeVar (_, s, a)) -> (
|
|
|
|
try
|
2020-11-27 20:36:38 +03:00
|
|
|
Bindlib.box_var
|
|
|
|
(fst
|
|
|
|
(Ast.ScopeVarMap.find (Pos.unmark a)
|
|
|
|
(Ast.SubScopeMap.find (Pos.unmark s) ctx.subscope_vars)))
|
2020-11-27 13:37:21 +03:00
|
|
|
with Not_found ->
|
|
|
|
Errors.raise_spanned_error
|
|
|
|
(Format.asprintf
|
2020-12-10 20:11:43 +03:00
|
|
|
"The variable %a.%a cannot be used here,\n\
|
|
|
|
as subscope %a's results will not have been computed yet" Ast.SubScopeName.format_t
|
|
|
|
(Pos.unmark s) Ast.ScopeVar.format_t (Pos.unmark a) Ast.SubScopeName.format_t
|
|
|
|
(Pos.unmark s))
|
2021-03-23 12:59:43 +03:00
|
|
|
(Pos.get_position e))
|
2020-11-24 00:26:26 +03:00
|
|
|
| EIfThenElse (cond, et, ef) ->
|
2020-11-26 15:38:42 +03:00
|
|
|
Bindlib.box_apply3
|
|
|
|
(fun c t f -> Dcalc.Ast.EIfThenElse (c, t, f))
|
|
|
|
(translate_expr ctx cond) (translate_expr ctx et) (translate_expr ctx ef)
|
2020-12-28 01:53:02 +03:00
|
|
|
| EOp op -> Bindlib.box (Dcalc.Ast.EOp op)
|
2021-04-03 16:07:49 +03:00
|
|
|
| ErrorOnEmpty e' ->
|
|
|
|
Bindlib.box_apply (fun e' -> Dcalc.Ast.ErrorOnEmpty e') (translate_expr ctx e')
|
2020-12-28 01:53:02 +03:00
|
|
|
| EArray es ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun es -> Dcalc.Ast.EArray es)
|
2021-03-23 12:59:43 +03:00
|
|
|
(Bindlib.box_list (List.map (translate_expr ctx) es)))
|
2020-11-23 18:12:45 +03:00
|
|
|
|
2021-10-28 16:24:39 +03:00
|
|
|
(** The result of a rule translation is a list of assignment, with variables and expressions. We
|
|
|
|
also return the new translation context available after the assignment to use in later rule
|
|
|
|
translations. The list is actually a list of list because we want to group in assignments that
|
|
|
|
are independent of each other to speed up the translation by minimizing Bindlib.bind_mvar *)
|
|
|
|
let translate_rule (ctx : ctx) (rule : Ast.rule)
|
2021-12-09 13:58:42 +03:00
|
|
|
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) : Dcalc.Ast.scope_let list * ctx =
|
2020-11-23 20:51:06 +03:00
|
|
|
match rule with
|
2020-11-26 12:38:13 +03:00
|
|
|
| Definition ((ScopeVar a, var_def_pos), tau, e) ->
|
2020-11-23 20:51:06 +03:00
|
|
|
let a_name = Ast.ScopeVar.get_info (Pos.unmark a) in
|
|
|
|
let a_var = Dcalc.Ast.Var.make a_name in
|
2020-12-04 20:48:16 +03:00
|
|
|
let tau = translate_typ ctx tau in
|
2020-11-26 17:48:26 +03:00
|
|
|
let new_e = translate_expr ctx e in
|
2020-12-10 18:58:32 +03:00
|
|
|
let a_expr = Dcalc.Ast.make_var (a_var, var_def_pos) in
|
|
|
|
let merged_expr =
|
2020-12-09 13:23:03 +03:00
|
|
|
Bindlib.box_apply
|
2021-04-03 16:07:49 +03:00
|
|
|
(fun merged_expr -> (Dcalc.Ast.ErrorOnEmpty merged_expr, Pos.get_position a_name))
|
2021-01-21 23:33:04 +03:00
|
|
|
(merge_defaults a_expr new_e)
|
2020-12-09 13:23:03 +03:00
|
|
|
in
|
2020-12-11 12:51:46 +03:00
|
|
|
let merged_expr =
|
2021-04-05 20:06:32 +03:00
|
|
|
tag_with_log_entry merged_expr
|
|
|
|
(Dcalc.Ast.VarDef (Pos.unmark tau))
|
|
|
|
[ (sigma_name, pos_sigma); a_name ]
|
2020-12-11 12:51:46 +03:00
|
|
|
in
|
2021-12-09 15:54:10 +03:00
|
|
|
( [
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a);
|
|
|
|
Dcalc.Ast.scope_let_typ = tau;
|
2021-12-10 18:54:51 +03:00
|
|
|
Dcalc.Ast.scope_let_expr = merged_expr;
|
2021-12-09 15:54:10 +03:00
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.ScopeVarDefinition;
|
|
|
|
};
|
|
|
|
],
|
2021-10-28 16:24:39 +03:00
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
scope_vars = Ast.ScopeVarMap.add (Pos.unmark a) (a_var, Pos.unmark tau) ctx.scope_vars;
|
|
|
|
} )
|
2020-11-26 19:06:32 +03:00
|
|
|
| Definition ((SubScopeVar (_subs_name, subs_index, subs_var), var_def_pos), tau, e) ->
|
|
|
|
let a_name =
|
|
|
|
Pos.map_under_mark
|
2020-11-27 13:37:21 +03:00
|
|
|
(fun str -> str ^ "." ^ Pos.unmark (Ast.ScopeVar.get_info (Pos.unmark subs_var)))
|
|
|
|
(Ast.SubScopeName.get_info (Pos.unmark subs_index))
|
2020-11-26 19:06:32 +03:00
|
|
|
in
|
2021-10-28 16:24:39 +03:00
|
|
|
let a_var = Dcalc.Ast.Var.make a_name in
|
2020-12-04 20:48:16 +03:00
|
|
|
let tau = translate_typ ctx tau in
|
2020-12-11 12:51:46 +03:00
|
|
|
let new_e =
|
2021-04-05 20:06:32 +03:00
|
|
|
tag_with_log_entry (translate_expr ctx e)
|
|
|
|
(Dcalc.Ast.VarDef (Pos.unmark tau))
|
2021-01-21 23:33:04 +03:00
|
|
|
[ (sigma_name, pos_sigma); a_name ]
|
2020-12-11 12:51:46 +03:00
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let silent_var = Dcalc.Ast.Var.make ("_", Pos.no_pos) in
|
|
|
|
let thunked_new_e =
|
|
|
|
Dcalc.Ast.make_abs
|
|
|
|
(Array.of_list [ silent_var ])
|
|
|
|
new_e var_def_pos
|
2020-12-09 16:51:22 +03:00
|
|
|
[ (Dcalc.Ast.TLit TUnit, var_def_pos) ]
|
2020-11-27 13:37:21 +03:00
|
|
|
var_def_pos
|
|
|
|
in
|
2021-12-09 15:54:10 +03:00
|
|
|
( [
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_var = (a_var, Pos.get_position a_name);
|
|
|
|
Dcalc.Ast.scope_let_typ =
|
|
|
|
(Dcalc.Ast.TArrow ((TLit TUnit, var_def_pos), tau), var_def_pos);
|
2021-12-10 18:54:51 +03:00
|
|
|
Dcalc.Ast.scope_let_expr = thunked_new_e;
|
2021-12-09 15:54:10 +03:00
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.SubScopeVarDefinition;
|
|
|
|
};
|
|
|
|
],
|
2021-10-28 16:24:39 +03:00
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
subscope_vars =
|
|
|
|
Ast.SubScopeMap.update (Pos.unmark subs_index)
|
|
|
|
(fun map ->
|
|
|
|
match map with
|
|
|
|
| Some map ->
|
|
|
|
Some (Ast.ScopeVarMap.add (Pos.unmark subs_var) (a_var, Pos.unmark tau) map)
|
|
|
|
| None ->
|
|
|
|
Some (Ast.ScopeVarMap.singleton (Pos.unmark subs_var) (a_var, Pos.unmark tau)))
|
|
|
|
ctx.subscope_vars;
|
|
|
|
} )
|
2020-11-27 13:37:21 +03:00
|
|
|
| Call (subname, subindex) ->
|
2021-02-01 17:57:19 +03:00
|
|
|
let ( all_subscope_vars,
|
|
|
|
scope_dcalc_var,
|
|
|
|
_,
|
|
|
|
called_scope_input_struct,
|
|
|
|
called_scope_return_struct ) =
|
2021-01-29 18:24:20 +03:00
|
|
|
Ast.ScopeMap.find subname ctx.scopes_parameters
|
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let subscope_vars_defined =
|
|
|
|
try Ast.SubScopeMap.find subindex ctx.subscope_vars
|
|
|
|
with Not_found -> Ast.ScopeVarMap.empty
|
|
|
|
in
|
|
|
|
let subscope_var_not_yet_defined subvar =
|
|
|
|
not (Ast.ScopeVarMap.mem subvar subscope_vars_defined)
|
|
|
|
in
|
2021-02-01 17:57:19 +03:00
|
|
|
let pos_call = Pos.get_position (Ast.SubScopeName.get_info subindex) in
|
2020-11-27 13:37:21 +03:00
|
|
|
let subscope_args =
|
|
|
|
List.map
|
|
|
|
(fun (subvar, _) ->
|
|
|
|
if subscope_var_not_yet_defined subvar then
|
|
|
|
Bindlib.box Dcalc.Interpreter.empty_thunked_term
|
|
|
|
else
|
|
|
|
let a_var, _ = Ast.ScopeVarMap.find subvar subscope_vars_defined in
|
2021-02-01 17:57:19 +03:00
|
|
|
Dcalc.Ast.make_var (a_var, pos_call))
|
2020-11-27 13:37:21 +03:00
|
|
|
all_subscope_vars
|
|
|
|
in
|
2021-02-01 17:57:19 +03:00
|
|
|
let subscope_struct_arg =
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun subscope_args ->
|
|
|
|
(Dcalc.Ast.ETuple (subscope_args, Some called_scope_input_struct), pos_call))
|
|
|
|
(Bindlib.box_list subscope_args)
|
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let all_subscope_vars_dcalc =
|
|
|
|
List.map
|
|
|
|
(fun (subvar, tau) ->
|
|
|
|
let sub_dcalc_var =
|
|
|
|
Dcalc.Ast.Var.make
|
|
|
|
(Pos.map_under_mark
|
|
|
|
(fun s -> Pos.unmark (Ast.SubScopeName.get_info subindex) ^ "." ^ s)
|
|
|
|
(Ast.ScopeVar.get_info subvar))
|
|
|
|
in
|
|
|
|
(subvar, tau, sub_dcalc_var))
|
|
|
|
all_subscope_vars
|
|
|
|
in
|
2020-12-11 12:51:46 +03:00
|
|
|
let subscope_func =
|
2021-01-21 23:33:04 +03:00
|
|
|
tag_with_log_entry
|
|
|
|
(Dcalc.Ast.make_var
|
|
|
|
(scope_dcalc_var, Pos.get_position (Ast.SubScopeName.get_info subindex)))
|
|
|
|
Dcalc.Ast.BeginCall
|
|
|
|
[
|
|
|
|
(sigma_name, pos_sigma);
|
|
|
|
Ast.SubScopeName.get_info subindex;
|
|
|
|
Ast.ScopeName.get_info subname;
|
|
|
|
]
|
2020-12-11 12:51:46 +03:00
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let call_expr =
|
2021-01-21 23:33:04 +03:00
|
|
|
tag_with_log_entry
|
|
|
|
(Bindlib.box_apply2
|
2021-02-01 17:57:19 +03:00
|
|
|
(fun e u -> (Dcalc.Ast.EApp (e, [ u ]), Pos.no_pos))
|
|
|
|
subscope_func subscope_struct_arg)
|
2021-01-21 23:33:04 +03:00
|
|
|
Dcalc.Ast.EndCall
|
|
|
|
[
|
|
|
|
(sigma_name, pos_sigma);
|
|
|
|
Ast.SubScopeName.get_info subindex;
|
|
|
|
Ast.ScopeName.get_info subname;
|
|
|
|
]
|
2020-12-30 14:02:09 +03:00
|
|
|
in
|
2021-12-09 20:42:36 +03:00
|
|
|
|
2021-10-28 16:24:39 +03:00
|
|
|
let result_tuple_var = Dcalc.Ast.Var.make ("result", pos_sigma) in
|
2020-12-11 12:51:46 +03:00
|
|
|
let result_tuple_typ =
|
2021-01-14 02:17:24 +03:00
|
|
|
( Dcalc.Ast.TTuple
|
2021-01-29 18:24:20 +03:00
|
|
|
( List.map (fun (_, tau, _) -> (tau, pos_sigma)) all_subscope_vars_dcalc,
|
|
|
|
Some called_scope_return_struct ),
|
2020-12-11 12:51:46 +03:00
|
|
|
pos_sigma )
|
|
|
|
in
|
2021-12-09 20:42:36 +03:00
|
|
|
let call_scope_let =
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_var = (result_tuple_var, pos_sigma);
|
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.CallingSubScope;
|
|
|
|
Dcalc.Ast.scope_let_typ = result_tuple_typ;
|
2021-12-10 18:54:51 +03:00
|
|
|
Dcalc.Ast.scope_let_expr = call_expr;
|
2021-12-09 20:42:36 +03:00
|
|
|
}
|
|
|
|
in
|
|
|
|
let result_bindings_lets =
|
|
|
|
List.mapi
|
|
|
|
(fun i (_, tau, v) ->
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_var = (v, pos_sigma);
|
|
|
|
Dcalc.Ast.scope_let_typ = (tau, pos_sigma);
|
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringSubScopeResults;
|
|
|
|
Dcalc.Ast.scope_let_expr =
|
2021-12-10 18:54:51 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun r ->
|
|
|
|
( Dcalc.Ast.ETupleAccess
|
|
|
|
( r,
|
|
|
|
i,
|
|
|
|
Some called_scope_return_struct,
|
|
|
|
List.map (fun (_, t, _) -> (t, pos_sigma)) all_subscope_vars_dcalc ),
|
|
|
|
pos_sigma ))
|
|
|
|
(Dcalc.Ast.make_var (result_tuple_var, pos_sigma));
|
2021-12-09 20:42:36 +03:00
|
|
|
})
|
|
|
|
all_subscope_vars_dcalc
|
|
|
|
in
|
|
|
|
( call_scope_let :: result_bindings_lets,
|
2021-10-28 16:24:39 +03:00
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
subscope_vars =
|
|
|
|
Ast.SubScopeMap.add subindex
|
|
|
|
(List.fold_left
|
|
|
|
(fun acc (var, tau, dvar) -> Ast.ScopeVarMap.add var (dvar, tau) acc)
|
|
|
|
Ast.ScopeVarMap.empty all_subscope_vars_dcalc)
|
|
|
|
ctx.subscope_vars;
|
|
|
|
} )
|
2020-12-10 20:11:43 +03:00
|
|
|
| Assertion e ->
|
|
|
|
let new_e = translate_expr ctx e in
|
2021-12-09 15:54:10 +03:00
|
|
|
( [
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_var =
|
|
|
|
(Dcalc.Ast.Var.make ("_", Pos.get_position e), Pos.get_position e);
|
|
|
|
Dcalc.Ast.scope_let_typ = (Dcalc.Ast.TLit TUnit, Pos.get_position e);
|
|
|
|
Dcalc.Ast.scope_let_expr =
|
2021-12-10 18:54:51 +03:00
|
|
|
Bindlib.box_apply (fun new_e -> Pos.same_pos_as (Dcalc.Ast.EAssert new_e) e) new_e;
|
2021-12-09 15:54:10 +03:00
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.Assertion;
|
|
|
|
};
|
|
|
|
],
|
2021-10-28 16:24:39 +03:00
|
|
|
ctx )
|
2020-11-23 20:51:06 +03:00
|
|
|
|
2021-10-28 16:24:39 +03:00
|
|
|
let translate_rules (ctx : ctx) (rules : Ast.rule list)
|
2021-01-29 18:24:20 +03:00
|
|
|
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info)
|
2021-12-09 13:58:42 +03:00
|
|
|
(sigma_return_struct_name : Ast.StructName.t) :
|
2021-12-10 19:22:54 +03:00
|
|
|
Dcalc.Ast.scope_let list * Dcalc.Ast.expr Pos.marked Bindlib.box * ctx =
|
2021-12-09 13:58:42 +03:00
|
|
|
let scope_lets, new_ctx =
|
2021-10-28 16:24:39 +03:00
|
|
|
List.fold_left
|
2021-12-09 13:58:42 +03:00
|
|
|
(fun (scope_lets, ctx) rule ->
|
|
|
|
let new_scope_lets, new_ctx = translate_rule ctx rule (sigma_name, pos_sigma) in
|
|
|
|
(scope_lets @ new_scope_lets, new_ctx))
|
|
|
|
([], ctx) rules
|
2021-10-28 16:24:39 +03:00
|
|
|
in
|
|
|
|
let scope_variables = Ast.ScopeVarMap.bindings new_ctx.scope_vars in
|
|
|
|
let return_exp =
|
2021-12-10 19:22:54 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun args -> (Dcalc.Ast.ETuple (args, Some sigma_return_struct_name), pos_sigma))
|
|
|
|
(Bindlib.box_list
|
|
|
|
(List.map
|
|
|
|
(fun (_, (dcalc_var, _)) -> Dcalc.Ast.make_var (dcalc_var, pos_sigma))
|
|
|
|
scope_variables))
|
2021-10-28 16:24:39 +03:00
|
|
|
in
|
2021-12-09 13:58:42 +03:00
|
|
|
(scope_lets, return_exp, new_ctx)
|
2020-11-26 15:38:42 +03:00
|
|
|
|
2020-12-04 18:40:17 +03:00
|
|
|
let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
|
2020-12-10 18:58:32 +03:00
|
|
|
(sctx : scope_sigs_ctx) (scope_name : Ast.ScopeName.t) (sigma : Ast.scope_decl) :
|
2021-12-09 01:56:03 +03:00
|
|
|
Dcalc.Ast.scope_body * Dcalc.Ast.struct_ctx =
|
2020-12-10 18:58:32 +03:00
|
|
|
let ctx = empty_ctx struct_ctx enum_ctx sctx scope_name in
|
2020-12-11 12:51:46 +03:00
|
|
|
let sigma_info = Ast.ScopeName.get_info sigma.scope_decl_name in
|
2021-02-01 17:57:19 +03:00
|
|
|
let scope_variables, _, scope_input_var, scope_input_struct_name, scope_return_struct_name =
|
|
|
|
Ast.ScopeMap.find sigma.scope_decl_name sctx
|
|
|
|
in
|
|
|
|
let pos_sigma = Pos.get_position sigma_info in
|
2021-12-09 13:58:42 +03:00
|
|
|
let rules, return_exp, ctx =
|
|
|
|
translate_rules ctx sigma.scope_decl_rules sigma_info scope_return_struct_name
|
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let scope_variables =
|
|
|
|
List.map
|
|
|
|
(fun (x, tau) ->
|
|
|
|
let dcalc_x, _ = Ast.ScopeVarMap.find x ctx.scope_vars in
|
|
|
|
(x, tau, dcalc_x))
|
|
|
|
scope_variables
|
|
|
|
in
|
2021-02-01 17:57:19 +03:00
|
|
|
(* first we create variables from the fields of the input struct *)
|
2021-12-09 13:58:42 +03:00
|
|
|
let input_destructurings =
|
|
|
|
List.mapi
|
|
|
|
(fun i (_, tau, v) ->
|
|
|
|
{
|
|
|
|
Dcalc.Ast.scope_let_kind = Dcalc.Ast.DestructuringInputStruct;
|
2021-12-09 15:54:10 +03:00
|
|
|
Dcalc.Ast.scope_let_var = (v, pos_sigma);
|
2021-12-10 19:22:54 +03:00
|
|
|
Dcalc.Ast.scope_let_typ =
|
|
|
|
(Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma);
|
2021-12-09 13:58:42 +03:00
|
|
|
Dcalc.Ast.scope_let_expr =
|
2021-12-10 18:54:51 +03:00
|
|
|
Bindlib.box_apply
|
|
|
|
(fun r ->
|
|
|
|
( Dcalc.Ast.ETupleAccess
|
|
|
|
( r,
|
|
|
|
i,
|
|
|
|
Some scope_input_struct_name,
|
|
|
|
List.map
|
|
|
|
(fun (_, t, _) ->
|
|
|
|
( Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (t, pos_sigma)),
|
|
|
|
pos_sigma ))
|
|
|
|
scope_variables ),
|
|
|
|
pos_sigma ))
|
|
|
|
(Dcalc.Ast.make_var (scope_input_var, pos_sigma));
|
2021-12-09 13:58:42 +03:00
|
|
|
})
|
|
|
|
scope_variables
|
2021-02-01 17:57:19 +03:00
|
|
|
in
|
2021-01-29 18:24:20 +03:00
|
|
|
let scope_return_struct_fields =
|
|
|
|
List.map
|
|
|
|
(fun (_, tau, dvar) ->
|
2021-02-01 17:57:19 +03:00
|
|
|
let struct_field_name =
|
|
|
|
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_out", pos_sigma)
|
|
|
|
in
|
2021-01-29 18:24:20 +03:00
|
|
|
(struct_field_name, (tau, pos_sigma)))
|
|
|
|
scope_variables
|
|
|
|
in
|
2021-02-01 17:57:19 +03:00
|
|
|
let scope_input_struct_fields =
|
|
|
|
List.map
|
|
|
|
(fun (_, tau, dvar) ->
|
|
|
|
let struct_field_name =
|
|
|
|
Ast.StructFieldName.fresh (Bindlib.name_of dvar ^ "_in", pos_sigma)
|
|
|
|
in
|
|
|
|
( struct_field_name,
|
|
|
|
(Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma) ))
|
|
|
|
scope_variables
|
|
|
|
in
|
2021-01-29 18:24:20 +03:00
|
|
|
let new_struct_ctx =
|
2021-02-01 17:57:19 +03:00
|
|
|
Ast.StructMap.add scope_input_struct_name scope_input_struct_fields
|
|
|
|
(Ast.StructMap.singleton scope_return_struct_name scope_return_struct_fields)
|
2021-01-29 18:24:20 +03:00
|
|
|
in
|
2021-12-10 00:59:39 +03:00
|
|
|
( {
|
|
|
|
Dcalc.Ast.scope_body_lets = input_destructurings @ rules;
|
2021-12-10 19:22:54 +03:00
|
|
|
Dcalc.Ast.scope_body_result = return_exp;
|
2021-12-10 18:30:36 +03:00
|
|
|
Dcalc.Ast.scope_body_input_struct = scope_input_struct_name;
|
|
|
|
Dcalc.Ast.scope_body_output_struct = scope_return_struct_name;
|
|
|
|
Dcalc.Ast.scope_body_arg = scope_input_var;
|
2021-12-10 00:59:39 +03:00
|
|
|
},
|
2021-01-29 18:24:20 +03:00
|
|
|
new_struct_ctx )
|
2020-11-27 13:37:21 +03:00
|
|
|
|
2021-12-09 01:56:03 +03:00
|
|
|
let translate_program (prgm : Ast.program) : Dcalc.Ast.program * Dependency.TVertex.t list =
|
2020-11-25 20:00:34 +03:00
|
|
|
let scope_dependencies = Dependency.build_program_dep_graph prgm in
|
2020-12-06 14:32:36 +03:00
|
|
|
Dependency.check_for_cycle_in_scope scope_dependencies;
|
2021-01-29 01:46:39 +03:00
|
|
|
let types_ordering = Dependency.check_type_cycles prgm.program_structs prgm.program_enums in
|
2020-11-25 20:00:34 +03:00
|
|
|
let scope_ordering = Dependency.get_scope_ordering scope_dependencies in
|
2020-12-04 20:48:16 +03:00
|
|
|
let struct_ctx = prgm.program_structs in
|
|
|
|
let enum_ctx = prgm.program_enums in
|
2021-01-28 02:28:28 +03:00
|
|
|
let ctx_for_typ_translation scope_name =
|
|
|
|
empty_ctx struct_ctx enum_ctx Ast.ScopeMap.empty scope_name
|
|
|
|
in
|
|
|
|
let dummy_scope = Ast.ScopeName.fresh ("dummy", Pos.no_pos) in
|
2021-01-14 02:17:24 +03:00
|
|
|
let decl_ctx =
|
|
|
|
{
|
2021-01-28 02:28:28 +03:00
|
|
|
Dcalc.Ast.ctx_structs =
|
|
|
|
Ast.StructMap.map
|
|
|
|
(List.map (fun (x, y) -> (x, translate_typ (ctx_for_typ_translation dummy_scope) y)))
|
|
|
|
struct_ctx;
|
|
|
|
Dcalc.Ast.ctx_enums =
|
|
|
|
Ast.EnumMap.map
|
|
|
|
(List.map (fun (x, y) -> (x, (translate_typ (ctx_for_typ_translation dummy_scope)) y)))
|
|
|
|
enum_ctx;
|
2021-01-14 02:17:24 +03:00
|
|
|
}
|
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let sctx : scope_sigs_ctx =
|
2020-12-10 18:58:32 +03:00
|
|
|
Ast.ScopeMap.mapi
|
|
|
|
(fun scope_name scope ->
|
2020-11-27 13:37:21 +03:00
|
|
|
let scope_dvar = Dcalc.Ast.Var.make (Ast.ScopeName.get_info scope.Ast.scope_decl_name) in
|
2021-01-29 18:24:20 +03:00
|
|
|
let scope_return_struct_name =
|
|
|
|
Ast.StructName.fresh
|
|
|
|
(Pos.map_under_mark (fun s -> s ^ "_out") (Ast.ScopeName.get_info scope_name))
|
|
|
|
in
|
2021-02-01 17:57:19 +03:00
|
|
|
let scope_input_var =
|
|
|
|
Dcalc.Ast.Var.make
|
|
|
|
(Pos.map_under_mark (fun s -> s ^ "_in") (Ast.ScopeName.get_info scope_name))
|
|
|
|
in
|
|
|
|
let scope_input_struct_name =
|
|
|
|
Ast.StructName.fresh
|
|
|
|
(Pos.map_under_mark (fun s -> s ^ "_in") (Ast.ScopeName.get_info scope_name))
|
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
( List.map
|
2020-12-04 20:48:16 +03:00
|
|
|
(fun (scope_var, tau) ->
|
2021-01-28 02:28:28 +03:00
|
|
|
let tau = translate_typ (ctx_for_typ_translation scope_name) tau in
|
2021-01-29 18:24:20 +03:00
|
|
|
|
2020-12-04 20:48:16 +03:00
|
|
|
(scope_var, Pos.unmark tau))
|
2020-11-27 13:37:21 +03:00
|
|
|
(Ast.ScopeVarMap.bindings scope.scope_sig),
|
2021-01-29 18:24:20 +03:00
|
|
|
scope_dvar,
|
2021-02-01 17:57:19 +03:00
|
|
|
scope_input_var,
|
|
|
|
scope_input_struct_name,
|
2021-01-29 18:24:20 +03:00
|
|
|
scope_return_struct_name ))
|
2020-12-04 18:40:17 +03:00
|
|
|
prgm.program_scopes
|
2020-11-27 13:37:21 +03:00
|
|
|
in
|
2020-11-25 20:00:34 +03:00
|
|
|
(* the resulting expression is the list of definitions of all the scopes, ending with the
|
|
|
|
top-level scope. *)
|
2021-12-09 01:56:03 +03:00
|
|
|
let (scopes, decl_ctx)
|
|
|
|
: (Ast.ScopeName.t * Dcalc.Ast.expr Bindlib.var * Dcalc.Ast.scope_body) list * _ =
|
2021-01-28 15:58:59 +03:00
|
|
|
List.fold_right
|
2021-12-09 01:56:03 +03:00
|
|
|
(fun scope_name
|
|
|
|
((scopes, decl_ctx) :
|
|
|
|
(Ast.ScopeName.t * Dcalc.Ast.expr Bindlib.var * Dcalc.Ast.scope_body) list * _) ->
|
2021-01-28 15:58:59 +03:00
|
|
|
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in
|
2021-12-09 01:56:03 +03:00
|
|
|
let scope_body, scope_out_struct =
|
2021-01-29 18:24:20 +03:00
|
|
|
translate_scope_decl struct_ctx enum_ctx sctx scope_name scope
|
|
|
|
in
|
2021-12-09 01:56:03 +03:00
|
|
|
let _, dvar, _, _, _ = Ast.ScopeMap.find scope_name sctx in
|
2021-01-29 18:24:20 +03:00
|
|
|
let decl_ctx =
|
|
|
|
{
|
|
|
|
decl_ctx with
|
|
|
|
Dcalc.Ast.ctx_structs =
|
|
|
|
Ast.StructMap.union
|
|
|
|
(fun _ _ -> assert false (* should not happen *))
|
2021-02-01 17:57:19 +03:00
|
|
|
decl_ctx.Dcalc.Ast.ctx_structs scope_out_struct;
|
2021-01-29 18:24:20 +03:00
|
|
|
}
|
|
|
|
in
|
2021-12-09 01:56:03 +03:00
|
|
|
((scope_name, dvar, scope_body) :: scopes, decl_ctx))
|
|
|
|
scope_ordering ([], decl_ctx)
|
2021-01-28 15:58:59 +03:00
|
|
|
in
|
2021-12-09 01:56:03 +03:00
|
|
|
({ scopes; decl_ctx }, types_ordering)
|