2020-11-25 12:49:53 +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. *)
|
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** Translation from {!module: Desugared.Ast} to {!module: Scopelang.Ast} *)
|
|
|
|
|
2021-01-21 23:33:04 +03:00
|
|
|
open Utils
|
2020-11-25 16:35:26 +03:00
|
|
|
|
2022-03-01 12:15:44 +03:00
|
|
|
(** {1 Expression translation}*)
|
|
|
|
|
|
|
|
type target_scope_vars =
|
|
|
|
| WholeVar of Scopelang.Ast.ScopeVar.t
|
2022-03-01 22:41:01 +03:00
|
|
|
| States of (Ast.StateName.t * Scopelang.Ast.ScopeVar.t) list
|
2022-03-01 12:15:44 +03:00
|
|
|
|
|
|
|
type ctx = {
|
2022-03-01 22:41:01 +03:00
|
|
|
scope_var_mapping : target_scope_vars Ast.ScopeVarMap.t;
|
|
|
|
var_mapping : Scopelang.Ast.Var.t Ast.VarMap.t;
|
2022-03-01 12:15:44 +03:00
|
|
|
}
|
|
|
|
|
2022-03-01 22:41:01 +03:00
|
|
|
let rec translate_expr (ctx : ctx) (e : Ast.expr Pos.marked) :
|
|
|
|
Scopelang.Ast.expr Pos.marked Bindlib.box =
|
|
|
|
match Pos.unmark e with
|
|
|
|
| Ast.ELocation (SubScopeVar (s_name, ss_name, s_var)) ->
|
|
|
|
(* When referring to a subscope variable in an expression, we are referring to the output,
|
|
|
|
hence we take the last state. *)
|
|
|
|
let new_s_var =
|
|
|
|
match Ast.ScopeVarMap.find (Pos.unmark s_var) ctx.scope_var_mapping with
|
|
|
|
| WholeVar new_s_var -> Pos.same_pos_as new_s_var s_var
|
|
|
|
| States states -> Pos.same_pos_as (snd (List.hd (List.rev states))) s_var
|
|
|
|
in
|
|
|
|
Bindlib.box
|
|
|
|
(Scopelang.Ast.ELocation (SubScopeVar (s_name, ss_name, new_s_var)), Pos.get_position e)
|
|
|
|
| Ast.ELocation (ScopeVar (s_var, None)) ->
|
|
|
|
Bindlib.box
|
|
|
|
( Scopelang.Ast.ELocation
|
2022-03-01 12:15:44 +03:00
|
|
|
(ScopeVar
|
2022-03-01 22:41:01 +03:00
|
|
|
(match Ast.ScopeVarMap.find (Pos.unmark s_var) ctx.scope_var_mapping with
|
2022-03-01 12:15:44 +03:00
|
|
|
| WholeVar new_s_var -> Pos.same_pos_as new_s_var s_var
|
2022-03-01 22:41:01 +03:00
|
|
|
| States _ -> failwith "should not happen")),
|
|
|
|
Pos.get_position e )
|
|
|
|
| Ast.ELocation (ScopeVar (s_var, Some state)) ->
|
|
|
|
Bindlib.box
|
|
|
|
( Scopelang.Ast.ELocation
|
2022-03-01 12:15:44 +03:00
|
|
|
(ScopeVar
|
2022-03-01 22:41:01 +03:00
|
|
|
(match Ast.ScopeVarMap.find (Pos.unmark s_var) ctx.scope_var_mapping with
|
2022-03-01 12:15:44 +03:00
|
|
|
| WholeVar _ -> failwith "should not happen"
|
2022-03-01 22:41:01 +03:00
|
|
|
| States states -> Pos.same_pos_as (List.assoc state states) s_var)),
|
|
|
|
Pos.get_position e )
|
|
|
|
| Ast.EVar v ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun v -> Pos.same_pos_as v e)
|
|
|
|
(Bindlib.box_var (Ast.VarMap.find (Pos.unmark v) ctx.var_mapping))
|
|
|
|
| EStruct (s_name, fields) ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_fields -> (Scopelang.Ast.EStruct (s_name, new_fields), Pos.get_position e))
|
|
|
|
(Scopelang.Ast.StructFieldMapLift.lift_box
|
|
|
|
(Scopelang.Ast.StructFieldMap.map (translate_expr ctx) fields))
|
|
|
|
| EStructAccess (e1, s_name, f_name) ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_e1 -> (Scopelang.Ast.EStructAccess (new_e1, s_name, f_name), Pos.get_position e))
|
|
|
|
(translate_expr ctx e1)
|
|
|
|
| EEnumInj (e1, cons, e_name) ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_e1 -> (Scopelang.Ast.EEnumInj (new_e1, cons, e_name), Pos.get_position e))
|
|
|
|
(translate_expr ctx e1)
|
|
|
|
| EMatch (e1, e_name, arms) ->
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun new_e1 new_arms ->
|
|
|
|
(Scopelang.Ast.EMatch (new_e1, e_name, new_arms), Pos.get_position e))
|
|
|
|
(translate_expr ctx e1)
|
|
|
|
(Scopelang.Ast.EnumConstructorMapLift.lift_box
|
|
|
|
(Scopelang.Ast.EnumConstructorMap.map (translate_expr ctx) arms))
|
|
|
|
| ELit l -> Bindlib.box (Scopelang.Ast.ELit l, Pos.get_position e)
|
|
|
|
| EAbs ((binder, binder_pos), typs) ->
|
|
|
|
let vars, body = Bindlib.unmbind binder in
|
|
|
|
let new_vars =
|
|
|
|
Array.map (fun var -> Scopelang.Ast.Var.make (Bindlib.name_of var, binder_pos)) vars
|
|
|
|
in
|
|
|
|
let ctx =
|
|
|
|
List.fold_left2
|
|
|
|
(fun ctx var new_var ->
|
|
|
|
{ ctx with var_mapping = Ast.VarMap.add var new_var ctx.var_mapping })
|
|
|
|
ctx (Array.to_list vars) (Array.to_list new_vars)
|
|
|
|
in
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_binder ->
|
|
|
|
(Scopelang.Ast.EAbs ((new_binder, binder_pos), typs), Pos.get_position e))
|
|
|
|
(Bindlib.bind_mvar new_vars (translate_expr ctx body))
|
|
|
|
| EApp (e1, args) ->
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun new_e1 new_args -> (Scopelang.Ast.EApp (new_e1, new_args), Pos.get_position e))
|
|
|
|
(translate_expr ctx e1)
|
|
|
|
(Bindlib.box_list (List.map (translate_expr ctx) args))
|
|
|
|
| EOp op -> Bindlib.box (Scopelang.Ast.EOp op, Pos.get_position e)
|
|
|
|
| EDefault (excepts, just, cons) ->
|
|
|
|
Bindlib.box_apply3
|
|
|
|
(fun new_excepts new_just new_cons ->
|
|
|
|
(Scopelang.Ast.EDefault (new_excepts, new_just, new_cons), Pos.get_position e))
|
|
|
|
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
|
|
|
|
(translate_expr ctx just) (translate_expr ctx cons)
|
|
|
|
| EIfThenElse (e1, e2, e3) ->
|
|
|
|
Bindlib.box_apply3
|
|
|
|
(fun new_e1 new_e2 new_e3 ->
|
|
|
|
(Scopelang.Ast.EIfThenElse (new_e1, new_e2, new_e3), Pos.get_position e))
|
|
|
|
(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
|
|
|
|
| EArray args ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_args -> (Scopelang.Ast.EArray new_args, Pos.get_position e))
|
|
|
|
(Bindlib.box_list (List.map (translate_expr ctx) args))
|
|
|
|
| ErrorOnEmpty e1 ->
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun new_e1 -> (Scopelang.Ast.ErrorOnEmpty new_e1, Pos.get_position e))
|
|
|
|
(translate_expr ctx e1)
|
2022-03-01 12:15:44 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** {1 Rule tree construction} *)
|
|
|
|
|
2022-01-05 12:42:46 +03:00
|
|
|
(** Intermediate representation for the exception tree of rules for a particular scope definition. *)
|
|
|
|
type rule_tree =
|
|
|
|
| Leaf of Ast.rule list (** Rules defining a base case piecewise. List is non-empty. *)
|
|
|
|
| Node of rule_tree list * Ast.rule list
|
|
|
|
(** A list of exceptions to a non-empty list of rules defining a base case piecewise. *)
|
2020-11-25 18:51:19 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** Transforms a flat list of rules into a tree, taking into account the priorities declared between
|
2021-01-13 21:07:35 +03:00
|
|
|
rules *)
|
|
|
|
let def_map_to_tree (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t) : rule_tree list =
|
|
|
|
let exc_graph = Dependency.build_exceptions_graph def def_info in
|
|
|
|
Dependency.check_for_exception_cycle exc_graph;
|
|
|
|
(* we start by the base cases: they are the vertices which have no successors *)
|
|
|
|
let base_cases =
|
|
|
|
Dependency.ExceptionsDependencies.fold_vertex
|
|
|
|
(fun v base_cases ->
|
|
|
|
if Dependency.ExceptionsDependencies.out_degree exc_graph v = 0 then v :: base_cases
|
|
|
|
else base_cases)
|
|
|
|
exc_graph []
|
2020-12-18 17:59:15 +03:00
|
|
|
in
|
2022-01-05 12:42:46 +03:00
|
|
|
let rec build_tree (base_cases : Ast.RuleSet.t) : rule_tree =
|
|
|
|
let exceptions = Dependency.ExceptionsDependencies.pred exc_graph base_cases in
|
|
|
|
let base_case_as_rule_list =
|
|
|
|
List.map (fun r -> Ast.RuleMap.find r def) (List.of_seq (Ast.RuleSet.to_seq base_cases))
|
|
|
|
in
|
2021-01-13 21:07:35 +03:00
|
|
|
match exceptions with
|
2022-01-05 12:42:46 +03:00
|
|
|
| [] -> Leaf base_case_as_rule_list
|
|
|
|
| _ -> Node (List.map build_tree exceptions, base_case_as_rule_list)
|
2020-11-25 18:51:19 +03:00
|
|
|
in
|
2021-01-13 21:07:35 +03:00
|
|
|
List.map build_tree base_cases
|
2020-11-25 18:51:19 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** From the {!type: rule_tree}, builds an {!constructor: Dcalc.Ast.EDefault} expression in the
|
|
|
|
scope language. The [~toplevel] parameter is used to know when to place the toplevel binding in
|
|
|
|
the case of functions. *)
|
2022-03-06 16:15:09 +03:00
|
|
|
let rec rule_tree_to_expr ~(toplevel : bool) (ctx : ctx) (def_pos : Pos.t)
|
|
|
|
(is_func : Ast.Var.t option) (tree : rule_tree) : Scopelang.Ast.expr Pos.marked Bindlib.box =
|
2022-01-05 12:42:46 +03:00
|
|
|
let exceptions, base_rules =
|
2020-12-18 17:59:15 +03:00
|
|
|
match tree with Leaf r -> ([], r) | Node (exceptions, r) -> (exceptions, r)
|
|
|
|
in
|
2020-11-25 18:51:19 +03:00
|
|
|
(* because each rule has its own variable parameter and we want to convert the whole rule tree
|
|
|
|
into a function, we need to perform some alpha-renaming of all the expressions *)
|
2022-03-06 16:15:09 +03:00
|
|
|
let substitute_parameter (e : Ast.expr Pos.marked Bindlib.box) (rule : Ast.rule) :
|
|
|
|
Ast.expr Pos.marked Bindlib.box =
|
2022-01-05 12:42:46 +03:00
|
|
|
match (is_func, rule.Ast.rule_parameter) with
|
2020-11-25 18:51:19 +03:00
|
|
|
| Some new_param, Some (old_param, _) ->
|
2020-11-27 18:27:10 +03:00
|
|
|
let binder = Bindlib.bind_var old_param e in
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun binder new_param -> Bindlib.subst binder new_param)
|
|
|
|
binder (Bindlib.box_var new_param)
|
2020-11-25 18:51:19 +03:00
|
|
|
| None, None -> e
|
|
|
|
| _ -> assert false
|
|
|
|
(* should not happen *)
|
|
|
|
in
|
2022-03-06 16:15:09 +03:00
|
|
|
let ctx =
|
|
|
|
match is_func with
|
|
|
|
| None -> ctx
|
|
|
|
| Some new_param -> (
|
|
|
|
match Ast.VarMap.find_opt new_param ctx.var_mapping with
|
|
|
|
| None ->
|
|
|
|
let new_param_scope = Scopelang.Ast.Var.make (Bindlib.name_of new_param, def_pos) in
|
|
|
|
{ ctx with var_mapping = Ast.VarMap.add new_param new_param_scope ctx.var_mapping }
|
|
|
|
| Some _ ->
|
|
|
|
(* We only create a mapping if none exists because [rule_tree_to_expr] is called
|
|
|
|
recursively on the exceptions of the tree and we don't want to create a new Scopelang
|
|
|
|
variable for the parameter at each tree level. *)
|
|
|
|
ctx)
|
|
|
|
in
|
2022-01-05 12:42:46 +03:00
|
|
|
let base_just_list =
|
|
|
|
List.map (fun rule -> substitute_parameter rule.Ast.rule_just rule) base_rules
|
|
|
|
in
|
|
|
|
let base_cons_list =
|
|
|
|
List.map (fun rule -> substitute_parameter rule.Ast.rule_cons rule) base_rules
|
|
|
|
in
|
2022-03-06 16:15:09 +03:00
|
|
|
let translate_and_unbox_list (list : Ast.expr Pos.marked Bindlib.box list) :
|
|
|
|
Scopelang.Ast.expr Pos.marked Bindlib.box list =
|
|
|
|
List.map
|
|
|
|
(fun e ->
|
|
|
|
(* There are two levels of boxing here, the outermost is introduced by the [translate_expr]
|
|
|
|
function for which all of the bindings should have been closed by now, so we can safely
|
|
|
|
unbox. *)
|
|
|
|
Bindlib.unbox (Bindlib.box_apply (translate_expr ctx) e))
|
|
|
|
list
|
|
|
|
in
|
2022-01-05 12:42:46 +03:00
|
|
|
let default_containing_base_cases =
|
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun base_just_list base_cons_list ->
|
|
|
|
( Scopelang.Ast.EDefault
|
|
|
|
( List.map2
|
|
|
|
(fun base_just base_cons ->
|
|
|
|
(Scopelang.Ast.EDefault ([], base_just, base_cons), Pos.get_position base_just))
|
|
|
|
base_just_list base_cons_list,
|
|
|
|
(Scopelang.Ast.ELit (Dcalc.Ast.LBool false), def_pos),
|
|
|
|
(Scopelang.Ast.ELit Dcalc.Ast.LEmptyError, def_pos) ),
|
|
|
|
def_pos ))
|
2022-03-06 16:15:09 +03:00
|
|
|
(Bindlib.box_list (translate_and_unbox_list base_just_list))
|
|
|
|
(Bindlib.box_list (translate_and_unbox_list base_cons_list))
|
2022-01-05 12:42:46 +03:00
|
|
|
in
|
2020-12-18 17:59:15 +03:00
|
|
|
let exceptions =
|
2022-03-06 16:15:09 +03:00
|
|
|
Bindlib.box_list (List.map (rule_tree_to_expr ~toplevel:false ctx def_pos is_func) exceptions)
|
2020-12-18 17:59:15 +03:00
|
|
|
in
|
2020-11-27 18:27:10 +03:00
|
|
|
let default =
|
2022-01-05 12:42:46 +03:00
|
|
|
Bindlib.box_apply2
|
|
|
|
(fun exceptions default_containing_base_cases ->
|
|
|
|
( Scopelang.Ast.EDefault
|
|
|
|
( exceptions,
|
|
|
|
(Scopelang.Ast.ELit (Dcalc.Ast.LBool true), def_pos),
|
|
|
|
default_containing_base_cases ),
|
|
|
|
def_pos ))
|
|
|
|
exceptions default_containing_base_cases
|
2020-11-27 18:27:10 +03:00
|
|
|
in
|
2022-01-05 12:42:46 +03:00
|
|
|
match (is_func, (List.hd base_rules).Ast.rule_parameter) with
|
2020-11-25 18:51:19 +03:00
|
|
|
| None, None -> default
|
|
|
|
| Some new_param, Some (_, typ) ->
|
2020-11-27 18:27:10 +03:00
|
|
|
if toplevel then
|
2020-12-31 02:28:26 +03:00
|
|
|
(* When we're creating a function from multiple defaults, we must check that the result
|
|
|
|
returned by the function is not empty *)
|
|
|
|
let default =
|
|
|
|
Bindlib.box_apply
|
|
|
|
(fun (default : Scopelang.Ast.expr * Pos.t) ->
|
2021-04-03 16:07:49 +03:00
|
|
|
(Scopelang.Ast.ErrorOnEmpty default, def_pos))
|
2020-12-31 02:28:26 +03:00
|
|
|
default
|
|
|
|
in
|
2022-03-06 16:15:09 +03:00
|
|
|
Scopelang.Ast.make_abs
|
|
|
|
(Array.of_list [ Ast.VarMap.find new_param ctx.var_mapping ])
|
|
|
|
default def_pos [ typ ] def_pos
|
2020-11-27 18:27:10 +03:00
|
|
|
else default
|
2020-12-14 19:00:42 +03:00
|
|
|
| _ -> (* should not happen *) assert false
|
2020-11-25 18:51:19 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** {1 AST translation} *)
|
2020-11-25 18:51:19 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** Translates a definition inside a scope, the resulting expression should be an {!constructor:
|
|
|
|
Dcalc.Ast.EDefault} *)
|
2022-03-06 16:15:09 +03:00
|
|
|
let translate_def (ctx : ctx) (def_info : Ast.ScopeDef.t) (def : Ast.rule Ast.RuleMap.t)
|
2022-02-09 17:56:48 +03:00
|
|
|
(typ : Scopelang.Ast.typ Pos.marked) (io : Scopelang.Ast.io) ~(is_cond : bool)
|
|
|
|
~(is_subscope_var : bool) : Scopelang.Ast.expr Pos.marked =
|
2020-11-25 16:35:26 +03:00
|
|
|
(* Here, we have to transform this list of rules into a default tree. *)
|
2022-01-28 19:31:31 +03:00
|
|
|
let is_def_func = match Pos.unmark typ with Scopelang.Ast.TArrow (_, _) -> true | _ -> false in
|
|
|
|
let is_rule_func _ (r : Ast.rule) : bool = Option.is_some r.Ast.rule_parameter in
|
|
|
|
let all_rules_func = Ast.RuleMap.for_all is_rule_func def in
|
|
|
|
let all_rules_not_func = Ast.RuleMap.for_all (fun n r -> not (is_rule_func n r)) def in
|
|
|
|
let is_def_func_param_typ : Scopelang.Ast.typ Pos.marked option =
|
|
|
|
if is_def_func && all_rules_func then
|
2020-12-09 12:36:09 +03:00
|
|
|
match Pos.unmark typ with
|
|
|
|
| Scopelang.Ast.TArrow (t_param, _) -> Some t_param
|
|
|
|
| _ ->
|
|
|
|
Errors.raise_spanned_error
|
|
|
|
(Format.asprintf
|
|
|
|
"The definitions of %a are function but its type, %a, is not a function type"
|
|
|
|
Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ)
|
|
|
|
(Pos.get_position typ)
|
2022-01-28 19:31:31 +03:00
|
|
|
else if (not is_def_func) && all_rules_not_func then None
|
2020-11-25 18:51:19 +03:00
|
|
|
else
|
|
|
|
Errors.raise_multispanned_error
|
|
|
|
"some definitions of the same variable are functions while others aren't"
|
2021-03-23 12:59:43 +03:00
|
|
|
(List.map
|
|
|
|
(fun (_, r) ->
|
2022-01-05 11:14:43 +03:00
|
|
|
( Some "This definition is a function:",
|
|
|
|
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
|
2022-01-28 19:31:31 +03:00
|
|
|
(Ast.RuleMap.bindings (Ast.RuleMap.filter is_rule_func def))
|
2020-11-25 18:51:19 +03:00
|
|
|
@ List.map
|
2020-11-27 18:27:10 +03:00
|
|
|
(fun (_, r) ->
|
|
|
|
( Some "This definition is not a function:",
|
2022-01-05 11:14:43 +03:00
|
|
|
Pos.get_position (Bindlib.unbox r.Ast.rule_cons) ))
|
2022-01-28 19:31:31 +03:00
|
|
|
(Ast.RuleMap.bindings (Ast.RuleMap.filter (fun n r -> not (is_rule_func n r)) def)))
|
2020-11-25 18:51:19 +03:00
|
|
|
in
|
2021-01-13 21:07:35 +03:00
|
|
|
let top_list = def_map_to_tree def_info def in
|
2020-12-31 02:28:26 +03:00
|
|
|
let top_value =
|
2022-01-28 19:31:31 +03:00
|
|
|
(if is_cond then Ast.always_false_rule else Ast.empty_rule) Pos.no_pos is_def_func_param_typ
|
2020-12-31 02:28:26 +03:00
|
|
|
in
|
2022-01-28 19:31:31 +03:00
|
|
|
if
|
2022-02-09 17:56:48 +03:00
|
|
|
Ast.RuleMap.cardinal def = 0
|
|
|
|
&& is_subscope_var
|
2022-01-28 19:31:31 +03:00
|
|
|
(* Here we have a special case for the empty definitions. Indeed, we could use the code for the
|
|
|
|
regular case below that would create a convoluted default always returning empty error, and
|
|
|
|
this would be correct. But it gets more complicated with functions. Indeed, if we create an
|
|
|
|
empty definition for a subscope argument whose type is a function, we get something like [fun
|
|
|
|
() -> (fun real_param -> < ... >)] that is passed as an argument to the subscope. The
|
|
|
|
sub-scope de-thunks but the de-thunking does not return empty error, signalling there is not
|
|
|
|
reentrant variable, because functions are values! So the subscope does not see that there is
|
|
|
|
not reentrant variable and does not pick its internal definition instead. See
|
|
|
|
[test/test_scope/subscope_function_arg_not_defined.catala_en] for a test case exercising that
|
|
|
|
subtlety.
|
|
|
|
|
2022-01-31 15:55:25 +03:00
|
|
|
To avoid this complication we special case here and put an empty error for all subscope
|
|
|
|
variables that are not defined. It covers the subtlety with functions described above but
|
|
|
|
also conditions with the false default value. *)
|
2022-02-09 17:56:48 +03:00
|
|
|
&& not
|
|
|
|
(is_cond
|
|
|
|
&& match Pos.unmark io.Scopelang.Ast.io_input with OnlyInput -> true | _ -> false)
|
|
|
|
(* However, this special case suffers from an exception: when a condition is defined as an
|
|
|
|
OnlyInput to a subscope, since the [false] default value will not be provided by the calee
|
|
|
|
scope, it has to be placed in the caller. *)
|
2022-01-28 19:31:31 +03:00
|
|
|
then (ELit LEmptyError, Pos.no_pos)
|
|
|
|
else
|
|
|
|
Bindlib.unbox
|
2022-03-06 16:15:09 +03:00
|
|
|
(rule_tree_to_expr ~toplevel:true ctx
|
2022-01-28 19:31:31 +03:00
|
|
|
(Ast.ScopeDef.get_position def_info)
|
2022-03-06 16:15:09 +03:00
|
|
|
(Option.map
|
|
|
|
(fun _ -> Ast.Var.make ("param", Ast.ScopeDef.get_position def_info))
|
|
|
|
is_def_func_param_typ)
|
2022-01-28 19:31:31 +03:00
|
|
|
(match top_list with
|
|
|
|
| [] ->
|
|
|
|
(* In this case, there are no rules to define the expression *)
|
|
|
|
Leaf [ top_value ]
|
|
|
|
| _ -> Node (top_list, [ top_value ])))
|
2020-11-25 16:35:26 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** Translates a scope *)
|
2022-03-06 16:15:09 +03:00
|
|
|
let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
|
2020-11-25 16:35:26 +03:00
|
|
|
let scope_dependencies = Dependency.build_scope_dependencies scope in
|
|
|
|
Dependency.check_for_cycle scope scope_dependencies;
|
|
|
|
let scope_ordering = Dependency.correct_computation_ordering scope_dependencies in
|
|
|
|
let scope_decl_rules =
|
|
|
|
List.flatten
|
|
|
|
(List.map
|
|
|
|
(fun vertex ->
|
|
|
|
match vertex with
|
2022-03-06 16:15:09 +03:00
|
|
|
| Dependency.Vertex.Var (var, state) -> (
|
|
|
|
let scope_def =
|
|
|
|
Ast.ScopeDefMap.find (Ast.ScopeDef.Var (var, state)) scope.scope_defs
|
|
|
|
in
|
2022-01-05 11:14:43 +03:00
|
|
|
let var_def = scope_def.scope_def_rules in
|
|
|
|
let var_typ = scope_def.scope_def_typ in
|
|
|
|
let is_cond = scope_def.scope_def_is_condition in
|
2022-02-09 17:34:13 +03:00
|
|
|
match Pos.unmark scope_def.Ast.scope_def_io.io_input with
|
2022-02-09 13:37:52 +03:00
|
|
|
| OnlyInput when not (Ast.RuleMap.is_empty var_def) ->
|
2022-02-09 17:34:13 +03:00
|
|
|
(* If the variable is tagged as input, then it shall not be redefined. *)
|
2022-02-09 13:37:52 +03:00
|
|
|
Errors.raise_multispanned_error
|
|
|
|
"It is impossible to give a definition to a scope variable tagged as input."
|
2022-03-06 16:15:09 +03:00
|
|
|
((Some "Incriminated variable:", Pos.get_position (Ast.ScopeVar.get_info var))
|
2022-02-09 13:37:52 +03:00
|
|
|
:: List.map
|
|
|
|
(fun (rule, _) ->
|
|
|
|
( Some "Incriminated variable definition:",
|
|
|
|
Pos.get_position (Ast.RuleName.get_info rule) ))
|
|
|
|
(Ast.RuleMap.bindings var_def))
|
2022-02-09 17:34:13 +03:00
|
|
|
| OnlyInput -> [] (* we do not provide any definition for an input-only variable *)
|
|
|
|
| _ ->
|
|
|
|
let expr_def =
|
2022-03-06 16:15:09 +03:00
|
|
|
translate_def ctx
|
|
|
|
(Ast.ScopeDef.Var (var, state))
|
|
|
|
var_def var_typ scope_def.Ast.scope_def_io ~is_cond ~is_subscope_var:false
|
|
|
|
in
|
|
|
|
let scope_var =
|
|
|
|
match (Ast.ScopeVarMap.find var ctx.scope_var_mapping, state) with
|
|
|
|
| WholeVar v, None -> v
|
|
|
|
| States states, Some state -> List.assoc state states
|
|
|
|
| _ -> failwith "should not happen"
|
2022-02-09 17:34:13 +03:00
|
|
|
in
|
|
|
|
[
|
|
|
|
Scopelang.Ast.Definition
|
|
|
|
( ( Scopelang.Ast.ScopeVar
|
2022-03-06 16:15:09 +03:00
|
|
|
( scope_var,
|
|
|
|
Pos.get_position (Scopelang.Ast.ScopeVar.get_info scope_var) ),
|
|
|
|
Pos.get_position (Scopelang.Ast.ScopeVar.get_info scope_var) ),
|
2022-02-09 17:34:13 +03:00
|
|
|
var_typ,
|
2022-02-10 12:09:58 +03:00
|
|
|
scope_def.Ast.scope_def_io,
|
2022-02-09 17:34:13 +03:00
|
|
|
expr_def );
|
|
|
|
])
|
2020-11-25 16:35:26 +03:00
|
|
|
| Dependency.Vertex.SubScope sub_scope_index ->
|
|
|
|
(* Before calling the sub_scope, we need to include all the re-definitions of
|
|
|
|
subscope parameters*)
|
|
|
|
let sub_scope =
|
|
|
|
Scopelang.Ast.SubScopeMap.find sub_scope_index scope.scope_sub_scopes
|
|
|
|
in
|
2022-02-06 20:52:18 +03:00
|
|
|
let sub_scope_vars_redefs_candidates =
|
|
|
|
Ast.ScopeDefMap.filter
|
|
|
|
(fun def_key scope_def ->
|
|
|
|
match def_key with
|
|
|
|
| Ast.ScopeDef.Var _ -> false
|
|
|
|
| Ast.ScopeDef.SubScopeVar (sub_scope_index', _) ->
|
|
|
|
sub_scope_index = sub_scope_index'
|
|
|
|
(* We exclude subscope variables that have 0 re-definitions and are not
|
|
|
|
visible in the input of the subscope *)
|
|
|
|
&& not
|
2022-02-07 12:30:36 +03:00
|
|
|
((match Pos.unmark scope_def.Ast.scope_def_io.io_input with
|
2022-02-07 20:18:23 +03:00
|
|
|
| Scopelang.Ast.NoInput -> true
|
|
|
|
| _ -> false)
|
2022-02-06 20:52:18 +03:00
|
|
|
&& Ast.RuleMap.is_empty scope_def.scope_def_rules))
|
|
|
|
scope.scope_defs
|
|
|
|
in
|
2020-11-25 16:35:26 +03:00
|
|
|
let sub_scope_vars_redefs =
|
|
|
|
Ast.ScopeDefMap.mapi
|
2022-01-05 11:14:43 +03:00
|
|
|
(fun def_key scope_def ->
|
|
|
|
let def = scope_def.Ast.scope_def_rules in
|
|
|
|
let def_typ = scope_def.scope_def_typ in
|
|
|
|
let is_cond = scope_def.scope_def_is_condition in
|
2020-11-25 16:35:26 +03:00
|
|
|
match def_key with
|
|
|
|
| Ast.ScopeDef.Var _ -> assert false (* should not happen *)
|
|
|
|
| Ast.ScopeDef.SubScopeVar (_, sub_scope_var) ->
|
2022-02-07 20:18:23 +03:00
|
|
|
(* This definition redefines a variable of the correct subscope. But we
|
|
|
|
have to check that this redefinition is allowed with respect to the io
|
|
|
|
parameters of that subscope variable. *)
|
|
|
|
(match Pos.unmark scope_def.Ast.scope_def_io.io_input with
|
|
|
|
| Scopelang.Ast.NoInput ->
|
|
|
|
Errors.raise_multispanned_error
|
|
|
|
"It is impossible to give a definition to a subscope variable not \
|
|
|
|
tagged as input or context."
|
2022-02-09 19:22:04 +03:00
|
|
|
((Some "Incriminated subscope:", Ast.ScopeDef.get_position def_key)
|
|
|
|
:: ( Some "Incriminated variable:",
|
2022-03-06 16:15:09 +03:00
|
|
|
Pos.get_position (Ast.ScopeVar.get_info sub_scope_var) )
|
2022-02-07 20:18:23 +03:00
|
|
|
:: List.map
|
|
|
|
(fun (rule, _) ->
|
2022-02-09 19:22:04 +03:00
|
|
|
( Some "Incriminated subscope variable definition:",
|
2022-02-07 20:18:23 +03:00
|
|
|
Pos.get_position (Ast.RuleName.get_info rule) ))
|
|
|
|
(Ast.RuleMap.bindings def))
|
2022-02-09 19:22:04 +03:00
|
|
|
| OnlyInput when Ast.RuleMap.is_empty def && not is_cond ->
|
|
|
|
(* If the subscope variable is tagged as input, then it shall be
|
|
|
|
defined. *)
|
|
|
|
Errors.raise_multispanned_error
|
|
|
|
"This subscope variable is a mandatory input but no definition was \
|
|
|
|
provided."
|
|
|
|
[
|
|
|
|
(Some "Incriminated subscope:", Ast.ScopeDef.get_position def_key);
|
|
|
|
( Some "Incriminated variable:",
|
2022-03-06 16:15:09 +03:00
|
|
|
Pos.get_position (Ast.ScopeVar.get_info sub_scope_var) );
|
2022-02-09 19:22:04 +03:00
|
|
|
]
|
2022-02-07 20:18:23 +03:00
|
|
|
| _ -> ());
|
|
|
|
(* Now that all is good, we can proceed with translating this redefinition
|
|
|
|
to a proper Scopelang term. *)
|
2022-01-28 19:31:31 +03:00
|
|
|
let expr_def =
|
2022-03-06 16:15:09 +03:00
|
|
|
translate_def ctx def_key def def_typ scope_def.Ast.scope_def_io ~is_cond
|
2022-02-09 17:56:48 +03:00
|
|
|
~is_subscope_var:true
|
2022-01-28 19:31:31 +03:00
|
|
|
in
|
2020-11-25 16:35:26 +03:00
|
|
|
let subscop_real_name =
|
|
|
|
Scopelang.Ast.SubScopeMap.find sub_scope_index scope.scope_sub_scopes
|
|
|
|
in
|
2022-03-06 16:15:09 +03:00
|
|
|
let var_pos = Pos.get_position (Ast.ScopeVar.get_info sub_scope_var) in
|
2020-11-25 16:35:26 +03:00
|
|
|
Scopelang.Ast.Definition
|
2020-11-26 12:38:13 +03:00
|
|
|
( ( Scopelang.Ast.SubScopeVar
|
|
|
|
( subscop_real_name,
|
|
|
|
(sub_scope_index, var_pos),
|
2022-03-06 16:15:09 +03:00
|
|
|
match
|
|
|
|
Ast.ScopeVarMap.find sub_scope_var ctx.scope_var_mapping
|
|
|
|
with
|
|
|
|
| WholeVar v -> (v, var_pos)
|
|
|
|
| States states ->
|
|
|
|
(* When defining a sub-scope variable, we always define its
|
|
|
|
first state in the sub-scope. *)
|
|
|
|
(snd (List.hd states), var_pos) ),
|
2020-11-26 12:38:13 +03:00
|
|
|
var_pos ),
|
2020-11-25 16:35:26 +03:00
|
|
|
def_typ,
|
2022-02-10 12:09:58 +03:00
|
|
|
scope_def.Ast.scope_def_io,
|
2020-11-25 16:35:26 +03:00
|
|
|
expr_def ))
|
2022-02-06 20:52:18 +03:00
|
|
|
sub_scope_vars_redefs_candidates
|
2020-11-25 16:35:26 +03:00
|
|
|
in
|
|
|
|
let sub_scope_vars_redefs =
|
|
|
|
List.map snd (Ast.ScopeDefMap.bindings sub_scope_vars_redefs)
|
|
|
|
in
|
|
|
|
sub_scope_vars_redefs @ [ Scopelang.Ast.Call (sub_scope, sub_scope_index) ])
|
|
|
|
scope_ordering)
|
|
|
|
in
|
2022-03-06 16:15:09 +03:00
|
|
|
(* Then, after having computed all the scopes variables, we add the assertions. TODO: the
|
|
|
|
assertions should be interleaved with the definitions! *)
|
2020-12-10 20:11:43 +03:00
|
|
|
let scope_decl_rules =
|
|
|
|
scope_decl_rules
|
2022-03-06 16:15:09 +03:00
|
|
|
@ List.map
|
|
|
|
(fun e ->
|
|
|
|
let scope_e = translate_expr ctx e in
|
|
|
|
Bindlib.unbox (Bindlib.box_apply (fun scope_e -> Scopelang.Ast.Assertion scope_e) scope_e))
|
|
|
|
(Bindlib.unbox (Bindlib.box_list scope.Ast.scope_assertions))
|
2020-12-10 20:11:43 +03:00
|
|
|
in
|
2020-11-27 13:37:21 +03:00
|
|
|
let scope_sig =
|
2022-03-06 16:15:09 +03:00
|
|
|
Ast.ScopeVarMap.fold
|
|
|
|
(fun var (states : Ast.var_or_states) acc ->
|
|
|
|
match states with
|
|
|
|
| WholeVar ->
|
|
|
|
let scope_def = Ast.ScopeDefMap.find (Ast.ScopeDef.Var (var, None)) scope.scope_defs in
|
|
|
|
let typ = scope_def.scope_def_typ in
|
|
|
|
Scopelang.Ast.ScopeVarMap.add
|
|
|
|
(match Ast.ScopeVarMap.find var ctx.scope_var_mapping with
|
|
|
|
| WholeVar v -> v
|
|
|
|
| States _ -> failwith "should not happen")
|
|
|
|
(typ, scope_def.scope_def_io) acc
|
|
|
|
| States states ->
|
|
|
|
(* What happens in the case of variables with multiple states is interesting. We need to
|
|
|
|
create as many Scopelang.Var entries in the scope signature as there are states. *)
|
|
|
|
List.fold_left
|
|
|
|
(fun acc (state : Ast.StateName.t) ->
|
|
|
|
let scope_def =
|
|
|
|
Ast.ScopeDefMap.find (Ast.ScopeDef.Var (var, Some state)) scope.scope_defs
|
|
|
|
in
|
|
|
|
Scopelang.Ast.ScopeVarMap.add
|
|
|
|
(match Ast.ScopeVarMap.find var ctx.scope_var_mapping with
|
|
|
|
| WholeVar _ -> failwith "should not happen"
|
|
|
|
| States states' -> List.assoc state states')
|
|
|
|
(scope_def.scope_def_typ, scope_def.scope_def_io)
|
|
|
|
acc)
|
|
|
|
acc states)
|
2020-11-27 13:37:21 +03:00
|
|
|
scope.scope_vars Scopelang.Ast.ScopeVarMap.empty
|
|
|
|
in
|
|
|
|
{
|
|
|
|
Scopelang.Ast.scope_decl_name = scope.scope_uid;
|
|
|
|
Scopelang.Ast.scope_decl_rules;
|
|
|
|
Scopelang.Ast.scope_sig;
|
|
|
|
}
|
2020-11-25 16:35:26 +03:00
|
|
|
|
2020-12-14 19:00:42 +03:00
|
|
|
(** {1 API} *)
|
|
|
|
|
2020-11-25 16:35:26 +03:00
|
|
|
let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
|
2022-03-06 16:15:09 +03:00
|
|
|
(* First we give mappings to all the locations between Desugared and Scopelang. This involves
|
|
|
|
creating a new Scopelang scope variable for every state of a Desugared variable. *)
|
|
|
|
let ctx =
|
|
|
|
Scopelang.Ast.ScopeMap.fold
|
|
|
|
(fun _scope scope_decl ctx ->
|
|
|
|
Ast.ScopeVarMap.fold
|
|
|
|
(fun scope_var (states : Ast.var_or_states) ctx ->
|
|
|
|
match states with
|
|
|
|
| Ast.WholeVar ->
|
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
scope_var_mapping =
|
|
|
|
Ast.ScopeVarMap.add scope_var
|
|
|
|
(WholeVar (Scopelang.Ast.ScopeVar.fresh (Ast.ScopeVar.get_info scope_var)))
|
|
|
|
ctx.scope_var_mapping;
|
|
|
|
}
|
|
|
|
| States states ->
|
|
|
|
{
|
|
|
|
ctx with
|
|
|
|
scope_var_mapping =
|
|
|
|
Ast.ScopeVarMap.add scope_var
|
|
|
|
(States
|
|
|
|
(List.map
|
|
|
|
(fun state ->
|
|
|
|
( state,
|
|
|
|
Scopelang.Ast.ScopeVar.fresh
|
|
|
|
(let state_name, state_pos = Ast.StateName.get_info state in
|
|
|
|
( Pos.unmark (Ast.ScopeVar.get_info scope_var) ^ "_" ^ state_name,
|
|
|
|
state_pos )) ))
|
|
|
|
states))
|
|
|
|
ctx.scope_var_mapping;
|
|
|
|
})
|
|
|
|
scope_decl.Ast.scope_vars ctx)
|
|
|
|
pgrm.Ast.program_scopes
|
|
|
|
{ scope_var_mapping = Ast.ScopeVarMap.empty; var_mapping = Ast.VarMap.empty }
|
|
|
|
in
|
2020-12-04 18:40:17 +03:00
|
|
|
{
|
2022-03-06 16:15:09 +03:00
|
|
|
Scopelang.Ast.program_scopes =
|
|
|
|
Scopelang.Ast.ScopeMap.map (translate_scope ctx) pgrm.program_scopes;
|
2020-12-04 18:40:17 +03:00
|
|
|
Scopelang.Ast.program_structs = pgrm.program_structs;
|
|
|
|
Scopelang.Ast.program_enums = pgrm.program_enums;
|
|
|
|
}
|