mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Fix var bindings in desugared->scopelang
This commit is contained in:
parent
7951661981
commit
4eeb8221f4
@ -17,6 +17,8 @@
|
||||
open Catala_utils
|
||||
open Shared_ast
|
||||
|
||||
module S = Scopelang.Ast
|
||||
|
||||
type scope_var_ctx = {
|
||||
scope_var_name : ScopeVar.t;
|
||||
scope_var_typ : naked_typ;
|
||||
@ -54,9 +56,9 @@ type 'm ctx = {
|
||||
toplevel_vars : ('m Ast.expr Var.t * naked_typ) TopdefName.Map.t;
|
||||
scope_vars :
|
||||
('m Ast.expr Var.t * naked_typ * Desugared.Ast.io) ScopeVar.Map.t;
|
||||
subscope_vars :
|
||||
('m Ast.expr Var.t * naked_typ * Desugared.Ast.io) ScopeVar.Map.t
|
||||
ScopeVar.Map.t;
|
||||
(* subscope_vars :
|
||||
* ('m Ast.expr Var.t * naked_typ * bool (\* reentrant *\)) ScopeVar.Map.t
|
||||
* ScopeVar.Map.t; *)
|
||||
date_rounding : date_rounding;
|
||||
}
|
||||
|
||||
@ -151,10 +153,10 @@ let tag_with_log_entry
|
||||
|
||||
NOTE: the choice of the exception that will be triggered and show in the
|
||||
trace is arbitrary (but deterministic). *)
|
||||
let collapse_similar_outcomes (type m) (excepts : m Scopelang.Ast.expr list) :
|
||||
m Scopelang.Ast.expr list =
|
||||
let collapse_similar_outcomes (type m) (excepts : m S.expr list) :
|
||||
m S.expr list =
|
||||
let module ExprMap = Map.Make (struct
|
||||
type t = m Scopelang.Ast.expr
|
||||
type t = m S.expr
|
||||
|
||||
let compare = Expr.compare
|
||||
let format = Expr.format
|
||||
@ -214,7 +216,7 @@ let thunk_scope_arg var_ctx e =
|
||||
Expr.make_abs [| Var.make "_" |] e [TLit TUnit, pos] pos
|
||||
| _ -> assert false
|
||||
|
||||
let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
|
||||
let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) :
|
||||
'm Ast.expr boxed =
|
||||
let m = Mark.get e in
|
||||
match Mark.remove e with
|
||||
@ -483,8 +485,6 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
|
||||
match loc with
|
||||
| ScopelangScopeVar { name = v, _; _ } ->
|
||||
[ScopeName.get_info sname; ScopeVar.get_info v]
|
||||
| SubScopeVar { scope; var = v, _; _ } ->
|
||||
[ScopeName.get_info scope; ScopeVar.get_info v]
|
||||
| ToplevelVar _ -> [])
|
||||
| _ -> []
|
||||
in
|
||||
@ -509,10 +509,6 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
|
||||
match Mark.remove f with
|
||||
| ELocation (ScopelangScopeVar { name = var }) ->
|
||||
retrieve_out_typ_or_any var ctx.scope_vars
|
||||
| ELocation (SubScopeVar { alias; var; _ }) ->
|
||||
ctx.subscope_vars
|
||||
|> ScopeVar.Map.find (Mark.remove alias)
|
||||
|> retrieve_out_typ_or_any var
|
||||
| ELocation (ToplevelVar { name }) -> (
|
||||
let typ =
|
||||
TopdefName.Map.find (Mark.remove name) ctx.decl_ctx.ctx_topdefs
|
||||
@ -568,26 +564,6 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
|
||||
| ELocation (ScopelangScopeVar { name = a }) ->
|
||||
let v, _, _ = ScopeVar.Map.find (Mark.remove a) ctx.scope_vars in
|
||||
Expr.evar v m
|
||||
| ELocation (SubScopeVar { alias = s; var = a; _ }) -> (
|
||||
try
|
||||
let v, _, _ =
|
||||
ScopeVar.Map.find (Mark.remove a)
|
||||
(ScopeVar.Map.find (Mark.remove s) ctx.subscope_vars)
|
||||
in
|
||||
Expr.evar v m
|
||||
with ScopeVar.Map.Not_found _ | ScopeVar.Map.Not_found _ ->
|
||||
Message.raise_multispanned_error
|
||||
[
|
||||
Some "Incriminated variable usage:", Expr.pos e;
|
||||
( Some "Incriminated subscope variable declaration:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove a)) );
|
||||
( Some "Incriminated subscope declaration:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove s)) );
|
||||
]
|
||||
"The variable %a.%a cannot be used here, as it is not part of subscope \
|
||||
%a's results. Maybe you forgot to qualify it as an output?"
|
||||
ScopeVar.format (Mark.remove s) ScopeVar.format (Mark.remove a)
|
||||
ScopeVar.format (Mark.remove s))
|
||||
| ELocation (ToplevelVar { name }) ->
|
||||
let path = TopdefName.path (Mark.remove name) in
|
||||
if path = [] then
|
||||
@ -602,29 +578,38 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
|
||||
| EIfThenElse _ | EAppOp _ ) as e ->
|
||||
Expr.map ~f:(translate_expr ctx) ~op:Operator.translate (e, m)
|
||||
|
||||
(** The result of a rule translation is a list of assignment, with variables and
|
||||
(** The result of a rule translation is a list of assignments, 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
|
||||
continuation yielding a [Dcalc.scope_body_expr] by giving it what should
|
||||
come later in the chain of let-bindings. *)
|
||||
let translate_rule
|
||||
(ctx : 'm ctx)
|
||||
(rule : 'm Scopelang.Ast.rule)
|
||||
(rule : 'm S.rule)
|
||||
((sigma_name, pos_sigma) : Uid.MarkedString.info) :
|
||||
('m Ast.expr scope_body_expr Bindlib.box ->
|
||||
'm Ast.expr scope_body_expr Bindlib.box)
|
||||
* 'm ctx =
|
||||
match rule with
|
||||
| Definition ((ScopelangScopeVar { name = a }, var_def_pos), tau, a_io, e) ->
|
||||
| S.ScopeVarDefinition { var; typ; e; _ }
|
||||
| S.SubScopeVarDefinition { var; typ; e } ->
|
||||
let pos_mark, _ = pos_mark_mk e in
|
||||
let a_name = ScopeVar.get_info (Mark.remove a) in
|
||||
let scope_let_kind, io = match rule with
|
||||
| S.ScopeVarDefinition {io; _} -> ScopeVarDefinition, io
|
||||
| S.SubScopeVarDefinition _ ->
|
||||
let pos = Mark.get var in
|
||||
SubScopeVarDefinition,
|
||||
{ io_input = (NoInput, pos); io_output = (false, pos) }
|
||||
| S.Assertion _ -> assert false
|
||||
in
|
||||
let a_name = ScopeVar.get_info (Mark.remove var) in
|
||||
let a_var = Var.make (Mark.remove a_name) in
|
||||
let new_e = translate_expr ctx e in
|
||||
let a_expr = Expr.make_var a_var (pos_mark var_def_pos) in
|
||||
let is_func = match Mark.remove tau with TArrow _ -> true | _ -> false in
|
||||
let a_expr = Expr.make_var a_var (pos_mark (Mark.get var)) in
|
||||
let is_func = match Mark.remove typ with TArrow _ -> true | _ -> false in
|
||||
let merged_expr =
|
||||
match Mark.remove a_io.io_input with
|
||||
| OnlyInput -> failwith "should not happen"
|
||||
match Mark.remove io.io_input with
|
||||
| OnlyInput -> assert false
|
||||
(* scopelang should not contain any definitions of input only variables *)
|
||||
| Reentrant -> merge_defaults ~is_func a_expr new_e
|
||||
| NoInput -> new_e
|
||||
@ -633,9 +618,9 @@ let translate_rule
|
||||
tag_with_log_entry merged_expr
|
||||
(VarDef
|
||||
{
|
||||
log_typ = Mark.remove tau;
|
||||
log_io_output = Mark.remove a_io.io_output;
|
||||
log_io_input = Mark.remove a_io.io_input;
|
||||
log_typ = Mark.remove typ;
|
||||
log_io_output = Mark.remove io.io_output;
|
||||
log_io_input = Mark.remove io.io_input;
|
||||
})
|
||||
[sigma_name, pos_sigma; a_name]
|
||||
in
|
||||
@ -644,10 +629,10 @@ let translate_rule
|
||||
(fun next merged_expr ->
|
||||
Cons
|
||||
( {
|
||||
scope_let_typ = tau;
|
||||
scope_let_typ = typ;
|
||||
scope_let_expr = merged_expr;
|
||||
scope_let_kind = ScopeVarDefinition;
|
||||
scope_let_pos = Mark.get a;
|
||||
scope_let_kind;
|
||||
scope_let_pos = Mark.get var;
|
||||
},
|
||||
next ))
|
||||
(Bindlib.bind_var a_var next)
|
||||
@ -655,74 +640,70 @@ let translate_rule
|
||||
{
|
||||
ctx with
|
||||
scope_vars =
|
||||
ScopeVar.Map.add (Mark.remove a)
|
||||
(a_var, Mark.remove tau, a_io)
|
||||
ScopeVar.Map.add (Mark.remove var)
|
||||
(a_var, Mark.remove typ, io)
|
||||
ctx.scope_vars;
|
||||
} )
|
||||
| Definition
|
||||
((SubScopeVar { alias = subs_index; var = subs_var; _ }, _), tau, a_io, e)
|
||||
->
|
||||
let a_name =
|
||||
Mark.map
|
||||
(fun str ->
|
||||
str ^ "." ^ Mark.remove (ScopeVar.get_info (Mark.remove subs_var)))
|
||||
(ScopeVar.get_info (Mark.remove subs_index))
|
||||
in
|
||||
let a_var = Var.make (Mark.remove a_name) in
|
||||
let new_e =
|
||||
tag_with_log_entry (translate_expr ctx e)
|
||||
(VarDef
|
||||
{
|
||||
log_typ = Mark.remove tau;
|
||||
log_io_output = false;
|
||||
log_io_input = Mark.remove a_io.Desugared.Ast.io_input;
|
||||
})
|
||||
[sigma_name, pos_sigma; a_name]
|
||||
in
|
||||
let thunked_or_nonempty_new_e =
|
||||
match a_io.Desugared.Ast.io_input with
|
||||
| Runtime.NoInput, _ -> assert false
|
||||
| Runtime.OnlyInput, _ -> new_e
|
||||
| Runtime.Reentrant, pos -> (
|
||||
match Mark.remove tau with
|
||||
| TArrow _ -> new_e
|
||||
| _ -> Mark.map_mark (Expr.with_pos pos) (Expr.thunk_term new_e))
|
||||
in
|
||||
( (fun next ->
|
||||
Bindlib.box_apply2
|
||||
(fun next thunked_or_nonempty_new_e ->
|
||||
Cons
|
||||
( {
|
||||
scope_let_pos = Mark.get a_name;
|
||||
scope_let_typ = input_var_typ (Mark.remove tau) a_io;
|
||||
scope_let_expr = thunked_or_nonempty_new_e;
|
||||
scope_let_kind = SubScopeVarDefinition;
|
||||
},
|
||||
next ))
|
||||
(Bindlib.bind_var a_var next)
|
||||
(Expr.Box.lift thunked_or_nonempty_new_e)),
|
||||
{
|
||||
ctx with
|
||||
subscope_vars =
|
||||
ScopeVar.Map.update (Mark.remove subs_index)
|
||||
(fun map ->
|
||||
match map with
|
||||
| Some map ->
|
||||
Some
|
||||
(ScopeVar.Map.add (Mark.remove subs_var)
|
||||
(a_var, Mark.remove tau, a_io)
|
||||
map)
|
||||
| None ->
|
||||
Some
|
||||
(ScopeVar.Map.singleton (Mark.remove subs_var)
|
||||
(a_var, Mark.remove tau, a_io)))
|
||||
ctx.subscope_vars;
|
||||
} )
|
||||
| Definition ((ToplevelVar _, _), _, _, _) ->
|
||||
assert false
|
||||
(* A global variable can't be defined locally. The [Definition] constructor
|
||||
could be made more specific to avoid this case, but the added complexity
|
||||
didn't seem worth it *)
|
||||
(* | S.SubScopeVarDefinition { var; origin_var; typ; scope; e } ->
|
||||
* let pos = Mark.get var in
|
||||
* let a_name = ScopeVar.get_info var in
|
||||
* let a_var = Var.make (Mark.remove a_name) in
|
||||
* let a_io =
|
||||
* { Desugared.Ast.io_input = NoInput, pos; io_output = false, pos }
|
||||
* (\* - "input subscopes" aren't allowed at the moment
|
||||
* - definitions are only for subscope *input* variables. Even if this is an "output subscope" and the variable was "input output", the output will be read from the output structure of the scope call, not from this variable.
|
||||
* *\)
|
||||
* in
|
||||
* let new_e =
|
||||
* tag_with_log_entry (translate_expr ctx e)
|
||||
* (VarDef
|
||||
* {
|
||||
* log_typ = Mark.remove typ;
|
||||
* log_io_output = false;
|
||||
* log_io_input = Mark.remove a_io.Desugared.Ast.io_input;
|
||||
* })
|
||||
* [sigma_name, pos_sigma; a_name]
|
||||
* in
|
||||
* let thunked_or_nonempty_new_e =
|
||||
* match a_io.Desugared.Ast.io_input with
|
||||
* | Runtime.NoInput, _ -> assert false
|
||||
* | Runtime.OnlyInput, _ -> new_e
|
||||
* | Runtime.Reentrant, pos -> (
|
||||
* match Mark.remove typ with
|
||||
* | TArrow _ -> new_e
|
||||
* | _ -> Mark.map_mark (Expr.with_pos pos) (Expr.thunk_term new_e))
|
||||
* in
|
||||
* ( (fun next ->
|
||||
* Bindlib.box_apply2
|
||||
* (fun next thunked_or_nonempty_new_e ->
|
||||
* Cons
|
||||
* ( {
|
||||
* scope_let_pos = Mark.get a_name;
|
||||
* scope_let_typ = input_var_typ (Mark.remove typ) a_io;
|
||||
* scope_let_expr = thunked_or_nonempty_new_e;
|
||||
* scope_let_kind = SubScopeVarDefinition;
|
||||
* },
|
||||
* next ))
|
||||
* (Bindlib.bind_var a_var next)
|
||||
* (Expr.Box.lift thunked_or_nonempty_new_e)),
|
||||
* {
|
||||
* ctx with
|
||||
* subscope_vars =
|
||||
* ScopeVar.Map.update (Mark.remove alias)
|
||||
* (fun map ->
|
||||
* match map with
|
||||
* | Some map ->
|
||||
* Some
|
||||
* (ScopeVar.Map.add (Mark.remove origin_var)
|
||||
* (a_var, Mark.remove typ, a_io)
|
||||
* map)
|
||||
* | None ->
|
||||
* Some
|
||||
* (ScopeVar.Map.singleton (Mark.remove origin_var)
|
||||
* (a_var, Mark.remove typ, a_io)))
|
||||
* ctx.subscope_vars;
|
||||
* } ) *)
|
||||
(*
|
||||
| Call (subname, subindex, m) ->
|
||||
let subscope_sig = ScopeName.Map.find subname ctx.scopes_parameters in
|
||||
let scope_sig_decl = ScopeName.Map.find subname ctx.decl_ctx.ctx_scopes in
|
||||
@ -885,6 +866,7 @@ let translate_rule
|
||||
ScopeVar.Map.empty all_subscope_output_vars_dcalc)
|
||||
ctx.subscope_vars;
|
||||
} )
|
||||
*)
|
||||
| Assertion e ->
|
||||
let new_e = translate_expr ctx e in
|
||||
let scope_let_pos = Expr.pos e in
|
||||
@ -910,7 +892,7 @@ let translate_rule
|
||||
let translate_rules
|
||||
(ctx : 'm ctx)
|
||||
(scope_name : ScopeName.t)
|
||||
(rules : 'm Scopelang.Ast.rule list)
|
||||
(rules : 'm S.rule list)
|
||||
((sigma_name, pos_sigma) : Uid.MarkedString.info)
|
||||
(mark : 'm mark)
|
||||
(scope_sig : 'm scope_sig_ctx) :
|
||||
@ -953,7 +935,7 @@ let translate_rules
|
||||
let translate_scope_decl
|
||||
(ctx : 'm ctx)
|
||||
(scope_name : ScopeName.t)
|
||||
(sigma : 'm Scopelang.Ast.scope_decl) =
|
||||
(sigma : 'm S.scope_decl) =
|
||||
let sigma_info = ScopeName.get_info sigma.scope_decl_name in
|
||||
let scope_sig =
|
||||
ScopeName.Map.find sigma.scope_decl_name ctx.scopes_parameters
|
||||
@ -1007,8 +989,9 @@ let translate_scope_decl
|
||||
or not ? *)
|
||||
Message.raise_spanned_error pos_sigma "Scope %a has no content"
|
||||
ScopeName.format scope_name
|
||||
| (Definition (_, _, _, (_, m)) | Assertion (_, m) | Call (_, _, m)) :: _ ->
|
||||
m
|
||||
| (S.ScopeVarDefinition { e; _ }
|
||||
| S.SubScopeVarDefinition { e; _ }
|
||||
| S.Assertion e) :: _ -> Mark.get e
|
||||
in
|
||||
let rules_with_return_expr, ctx =
|
||||
translate_rules ctx scope_name sigma.scope_decl_rules sigma_info scope_mark
|
||||
@ -1069,7 +1052,7 @@ let translate_scope_decl
|
||||
(Bindlib.bind_var scope_input_var
|
||||
(input_destructurings rules_with_return_expr))
|
||||
|
||||
let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
let translate_program (prgm : 'm S.program) : 'm Ast.program =
|
||||
let defs_dependencies = Scopelang.Dependency.build_program_dep_graph prgm in
|
||||
Scopelang.Dependency.check_for_cycle_in_defs defs_dependencies;
|
||||
let defs_ordering =
|
||||
@ -1094,7 +1077,7 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
as the return type of ScopeCalls) ; but input fields are used purely
|
||||
internally and need to be created here to implement the call
|
||||
convention for scopes. *)
|
||||
let module S = Scopelang.Ast in
|
||||
let module S = S in
|
||||
ScopeVar.Map.filter_map
|
||||
(fun dvar svar ->
|
||||
match Mark.remove svar.S.svar_io.Desugared.Ast.io_input with
|
||||
@ -1124,8 +1107,8 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
(fun (scope_var, svar) ->
|
||||
{
|
||||
scope_var_name = scope_var;
|
||||
scope_var_typ = Mark.remove svar.Scopelang.Ast.svar_in_ty;
|
||||
scope_var_io = svar.Scopelang.Ast.svar_io;
|
||||
scope_var_typ = Mark.remove svar.S.svar_in_ty;
|
||||
scope_var_io = svar.S.svar_io;
|
||||
})
|
||||
(ScopeVar.Map.bindings scope.scope_sig);
|
||||
scope_sig_scope_ref = scope_ref;
|
||||
@ -1142,8 +1125,8 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
in
|
||||
ModuleName.Map.fold
|
||||
(fun _ s -> ScopeName.Map.disjoint_union (process_scopes s))
|
||||
prgm.Scopelang.Ast.program_modules
|
||||
(process_scopes prgm.Scopelang.Ast.program_scopes)
|
||||
prgm.S.program_modules
|
||||
(process_scopes prgm.S.program_scopes)
|
||||
in
|
||||
let ctx_structs =
|
||||
ScopeName.Map.fold
|
||||
@ -1165,7 +1148,7 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
TopdefName.Map.mapi
|
||||
(fun name (_, ty) ->
|
||||
Var.make (Mark.remove (TopdefName.get_info name)), Mark.remove ty)
|
||||
prgm.Scopelang.Ast.program_topdefs
|
||||
prgm.S.program_topdefs
|
||||
in
|
||||
let ctx =
|
||||
{
|
||||
@ -1173,7 +1156,7 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
scope_name = None;
|
||||
scopes_parameters;
|
||||
scope_vars = ScopeVar.Map.empty;
|
||||
subscope_vars = ScopeVar.Map.empty;
|
||||
(* subscope_vars = ScopeVar.Map.empty; *)
|
||||
toplevel_vars;
|
||||
date_rounding = AbortOnRound;
|
||||
}
|
||||
@ -1222,6 +1205,6 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
|
||||
{
|
||||
code_items = Bindlib.unbox items;
|
||||
decl_ctx;
|
||||
module_name = prgm.Scopelang.Ast.program_module_name;
|
||||
module_name = prgm.S.program_module_name;
|
||||
lang = prgm.program_lang;
|
||||
}
|
||||
|
@ -25,45 +25,40 @@ open Shared_ast
|
||||
def *)
|
||||
module ScopeDef = struct
|
||||
module Base = struct
|
||||
type t =
|
||||
| Var of ScopeVar.t * StateName.t option
|
||||
| SubScopeVar of ScopeVar.t * ScopeVar.t * Pos.t
|
||||
(** In this case, the [ScopeVar.t] lives inside the context of the
|
||||
subscope's original declaration *)
|
||||
type kind =
|
||||
| Var of StateName.t option
|
||||
| SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
|
||||
|
||||
let compare x y =
|
||||
match x, y with
|
||||
| Var (x, stx), Var (y, sty) -> (
|
||||
match ScopeVar.compare x y with
|
||||
| 0 -> Option.compare StateName.compare stx sty
|
||||
| n -> n)
|
||||
| SubScopeVar (x', x, _), SubScopeVar (y', y, _) -> (
|
||||
match ScopeVar.compare x' y' with
|
||||
| 0 -> ScopeVar.compare x y
|
||||
| n -> n)
|
||||
| Var _, _ -> -1
|
||||
| _, Var _ -> 1
|
||||
type t = ScopeVar.t Mark.pos * kind
|
||||
|
||||
let get_position x =
|
||||
match x with
|
||||
| Var (x, None) -> Mark.get (ScopeVar.get_info x)
|
||||
| Var (_, Some sx) -> Mark.get (StateName.get_info sx)
|
||||
| SubScopeVar (_, _, pos) -> pos
|
||||
let compare_kind k1 k2 = match k1, k2 with
|
||||
| Var st1, Var st2 -> Option.compare StateName.compare st1 st2
|
||||
| SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } ->
|
||||
ScopeVar.compare v1 v2
|
||||
| Var _, SubScope _ -> -1
|
||||
| SubScope _, Var _ -> 1
|
||||
|
||||
let format fmt x =
|
||||
match x with
|
||||
| Var (v, None) -> ScopeVar.format fmt v
|
||||
| Var (v, Some sv) ->
|
||||
Format.fprintf fmt "%a.%a" ScopeVar.format v StateName.format sv
|
||||
| SubScopeVar (s, v, _) ->
|
||||
Format.fprintf fmt "%a.%a" ScopeVar.format s ScopeVar.format v
|
||||
let compare (v1, k1) (v2, k2) =
|
||||
match Mark.compare ScopeVar.compare v1 v2 with
|
||||
| 0 -> compare_kind k1 k2
|
||||
| n -> n
|
||||
|
||||
let hash x =
|
||||
match x with
|
||||
| Var (v, None) -> ScopeVar.hash v
|
||||
| Var (v, Some sv) -> Int.logxor (ScopeVar.hash v) (StateName.hash sv)
|
||||
| SubScopeVar (w, v, _) ->
|
||||
Int.logxor (ScopeVar.hash w) (ScopeVar.hash v)
|
||||
let get_position (v, _) = Mark.get v
|
||||
|
||||
let format ppf (v, k) =
|
||||
ScopeVar.format ppf (Mark.remove v);
|
||||
match k with
|
||||
| Var None -> ()
|
||||
| Var (Some st) -> Format.fprintf ppf ".%a" StateName.format st
|
||||
| SubScope { var_within_origin_scope = v; _ } -> Format.fprintf ppf ".%a" ScopeVar.format v
|
||||
|
||||
let hash (v, k) =
|
||||
let h0 = ScopeVar.hash (Mark.remove v) in
|
||||
match k with
|
||||
| Var (None) -> h0
|
||||
| Var (Some st) -> Int.logxor h0 (StateName.hash st)
|
||||
| SubScope { var_within_origin_scope = v; _ } ->
|
||||
Int.logxor h0 (ScopeVar.hash v)
|
||||
end
|
||||
|
||||
include Base
|
||||
@ -260,11 +255,7 @@ let free_variables (def : rule RuleName.Map.t) : Pos.t ScopeDef.Map.t =
|
||||
let usage =
|
||||
match loc with
|
||||
| DesugaredScopeVar { name; state } ->
|
||||
Some (ScopeDef.Var (Mark.remove name, state))
|
||||
| SubScopeVar { alias; var; _ } ->
|
||||
Some
|
||||
(ScopeDef.SubScopeVar
|
||||
(Mark.remove alias, Mark.remove var, Mark.get alias))
|
||||
Some (name, ScopeDef.Var state)
|
||||
| ToplevelVar _ -> None
|
||||
in
|
||||
match usage with
|
||||
|
@ -19,12 +19,13 @@
|
||||
open Catala_utils
|
||||
open Shared_ast
|
||||
|
||||
(** Inside a scope, a definition can refer either to a scope def, or a subscope
|
||||
def *)
|
||||
(** Inside a scope, a definition can refer to a variable (possibly an intermediate state thereof) or an input of a subscope. *)
|
||||
module ScopeDef : sig
|
||||
type t =
|
||||
| Var of ScopeVar.t * StateName.t option
|
||||
| SubScopeVar of ScopeVar.t * ScopeVar.t * Pos.t
|
||||
type kind =
|
||||
| Var of StateName.t option
|
||||
| SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
|
||||
|
||||
type t = ScopeVar.t Mark.pos * kind
|
||||
|
||||
val compare : t -> t -> int
|
||||
val get_position : t -> Pos.t
|
||||
|
@ -189,67 +189,25 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
|
||||
in
|
||||
(* then add the edges *)
|
||||
let g =
|
||||
let to_vertex (var, kind) = match kind with
|
||||
| Ast.ScopeDef.Var st -> Vertex.Var (Mark.remove var, st)
|
||||
| Ast.ScopeDef.SubScope _ -> Vertex.SubScope (Mark.remove var)
|
||||
in
|
||||
Ast.ScopeDef.Map.fold
|
||||
(fun def_key scope_def g ->
|
||||
let def = scope_def.Ast.scope_def_rules in
|
||||
let v_defined = to_vertex def_key in
|
||||
let fv = Ast.free_variables def in
|
||||
Ast.ScopeDef.Map.fold
|
||||
(fun fv_def fv_def_pos g ->
|
||||
match def_key, fv_def with
|
||||
| ( Ast.ScopeDef.Var (v_defined, s_defined),
|
||||
Ast.ScopeDef.Var (v_used, s_used) ) ->
|
||||
(* simple case *)
|
||||
if
|
||||
ScopeVar.equal v_used v_defined
|
||||
&& Option.equal StateName.equal s_used s_defined
|
||||
then
|
||||
(* variable definitions cannot be recursive *)
|
||||
let v_used = to_vertex fv_def in
|
||||
if Vertex.equal v_used v_defined then
|
||||
Message.raise_spanned_error fv_def_pos
|
||||
"The variable %a is used in one of its definitions, but \
|
||||
recursion is forbidden in Catala"
|
||||
Ast.ScopeDef.format def_key
|
||||
else
|
||||
let edge =
|
||||
ScopeDependencies.E.create
|
||||
(Vertex.Var (v_used, s_used))
|
||||
fv_def_pos
|
||||
(Vertex.Var (v_defined, s_defined))
|
||||
in
|
||||
ScopeDependencies.add_edge_e g edge
|
||||
| ( Ast.ScopeDef.SubScopeVar (defined, _, _),
|
||||
Ast.ScopeDef.Var (v_used, s_used) ) ->
|
||||
(* here we are defining the input of a subscope using a var of the
|
||||
scope *)
|
||||
let edge =
|
||||
ScopeDependencies.E.create
|
||||
(Vertex.Var (v_used, s_used))
|
||||
fv_def_pos (Vertex.SubScope defined)
|
||||
in
|
||||
ScopeDependencies.add_edge_e g edge
|
||||
| ( Ast.ScopeDef.SubScopeVar (defined, _, _),
|
||||
Ast.ScopeDef.SubScopeVar (used, _, _) ) ->
|
||||
(* here we are defining the input of a scope with the output of
|
||||
another subscope *)
|
||||
if ScopeVar.equal used defined then
|
||||
(* subscopes are not recursive functions *)
|
||||
Message.raise_spanned_error fv_def_pos
|
||||
"The subscope %a is used when defining one of its inputs, \
|
||||
but recursion is forbidden in Catala"
|
||||
ScopeVar.format defined
|
||||
else
|
||||
let edge =
|
||||
ScopeDependencies.E.create (Vertex.SubScope used) fv_def_pos
|
||||
(Vertex.SubScope defined)
|
||||
in
|
||||
ScopeDependencies.add_edge_e g edge
|
||||
| ( Ast.ScopeDef.Var (v_defined, s_defined),
|
||||
Ast.ScopeDef.SubScopeVar (used, _, _) ) ->
|
||||
(* finally we define a scope var with the output of a subscope *)
|
||||
let edge =
|
||||
ScopeDependencies.E.create (Vertex.SubScope used) fv_def_pos
|
||||
(Vertex.Var (v_defined, s_defined))
|
||||
in
|
||||
ScopeDependencies.add_edge_e g edge)
|
||||
Ast.ScopeDef.format def_key;
|
||||
ScopeDependencies.add_edge_e g
|
||||
(ScopeDependencies.E.create v_used fv_def_pos v_defined))
|
||||
fv g)
|
||||
scope.scope_defs g
|
||||
in
|
||||
@ -263,8 +221,6 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
|
||||
match Mark.remove used_var with
|
||||
| DesugaredScopeVar { name; state } ->
|
||||
Some (Vertex.Var (Mark.remove name, state))
|
||||
| SubScopeVar { alias; _ } ->
|
||||
Some (Vertex.SubScope (Mark.remove alias))
|
||||
| ToplevelVar _ -> None
|
||||
(* we don't add this dependency because toplevel definitions are
|
||||
outside the scope *)
|
||||
|
@ -14,6 +14,7 @@
|
||||
License for the specific language governing permissions and limitations under
|
||||
the License. *)
|
||||
|
||||
open Catala_utils
|
||||
open Shared_ast
|
||||
open Ast
|
||||
|
||||
@ -82,10 +83,11 @@ let program prg =
|
||||
let scope = ScopeName.Map.find scope_name modul.module_scopes in
|
||||
let vars =
|
||||
ScopeDef.Map.fold
|
||||
(fun var def vars ->
|
||||
match var with
|
||||
| Var (v, _states) -> ScopeVar.Map.add v def.scope_def_typ vars
|
||||
| SubScopeVar _ -> vars)
|
||||
(fun (v, kind) def vars ->
|
||||
match kind with
|
||||
| ScopeDef.Var _ -> ScopeVar.Map.add (Mark.remove v) def.scope_def_typ vars
|
||||
| ScopeDef.SubScope _ -> vars
|
||||
)
|
||||
scope.scope_defs ScopeVar.Map.empty
|
||||
in
|
||||
(* at this stage, rule resolution and the corresponding encapsulation
|
||||
|
@ -395,7 +395,7 @@ let rec translate_expr
|
||||
| Some st, [], _ ->
|
||||
Message.raise_spanned_error (Mark.get st)
|
||||
"Variable %a does not define states" ScopeVar.format uid
|
||||
| st, states, Some (Var (x'_uid, sx'), _)
|
||||
| st, states, Some (((x'_uid, _), Ast.ScopeDef.Var sx'), _)
|
||||
when ScopeVar.equal uid x'_uid -> (
|
||||
if st <> None then
|
||||
(* TODO *)
|
||||
@ -443,9 +443,10 @@ let rec translate_expr
|
||||
Expr.elocation
|
||||
(DesugaredScopeVar { name = uid, pos; state = x_state })
|
||||
emark
|
||||
| Some (SubScope _)
|
||||
(* Note: allowing access to a global variable with the same name as a
|
||||
subscope is disputable, but I see no good reason to forbid it either *)
|
||||
| Some (SubScope (uid, _, _)) ->
|
||||
Expr.elocation
|
||||
(DesugaredScopeVar { name = uid, pos; state = None })
|
||||
emark
|
||||
| None -> (
|
||||
match Ident.Map.find_opt x ctxt.local.topdefs with
|
||||
| Some v ->
|
||||
@ -472,39 +473,17 @@ let rec translate_expr
|
||||
emark
|
||||
| None ->
|
||||
Name_resolution.raise_unknown_identifier "for an external variable" name)
|
||||
| Dotted (e, ((path, x), _ppos)) -> (
|
||||
match path, Mark.remove e with
|
||||
| [], Ident ([], (y, _), None)
|
||||
when Option.fold scope ~none:false ~some:(fun s ->
|
||||
Name_resolution.is_subscope_uid s ctxt y) ->
|
||||
(* In this case, y.x is a subscope variable *)
|
||||
let subscope_uid, subscope_real_uid =
|
||||
match Ident.Map.find y scope_vars with
|
||||
| SubScope (sub, sc) -> sub, sc
|
||||
| ScopeVar _ -> assert false
|
||||
in
|
||||
let subscope_var_uid =
|
||||
Name_resolution.get_var_uid subscope_real_uid ctxt x
|
||||
in
|
||||
Expr.elocation
|
||||
(SubScopeVar
|
||||
{
|
||||
scope = subscope_real_uid;
|
||||
alias = subscope_uid, pos;
|
||||
var = subscope_var_uid, pos;
|
||||
})
|
||||
emark
|
||||
| _ ->
|
||||
(* In this case e.x is the struct field x access of expression e *)
|
||||
let e = rec_helper e in
|
||||
let rec get_str ctxt = function
|
||||
| [] -> None
|
||||
| [c] -> Some (Name_resolution.get_struct ctxt c)
|
||||
| mod_id :: path ->
|
||||
get_str (Name_resolution.get_module_ctx ctxt mod_id) path
|
||||
in
|
||||
Expr.edstructaccess ~e ~field:(Mark.remove x)
|
||||
~name_opt:(get_str ctxt path) emark)
|
||||
| Dotted (e, ((path, x), _ppos)) ->
|
||||
(* e.x is the struct field x access of expression e *)
|
||||
let e = rec_helper e in
|
||||
let rec get_str ctxt = function
|
||||
| [] -> None
|
||||
| [c] -> Some (Name_resolution.get_struct ctxt c)
|
||||
| mod_id :: path ->
|
||||
get_str (Name_resolution.get_module_ctx ctxt mod_id) path
|
||||
in
|
||||
Expr.edstructaccess ~e ~field:(Mark.remove x)
|
||||
~name_opt:(get_str ctxt path) emark
|
||||
| FunCall ((Builtin b, _), [arg]) ->
|
||||
let op, ty =
|
||||
match b with
|
||||
@ -1526,59 +1505,53 @@ let attribute_to_io (attr : S.scope_decl_context_io) : Ast.io =
|
||||
|
||||
let init_scope_defs
|
||||
(ctxt : Name_resolution.context)
|
||||
(scope_idmap : scope_var_or_subscope Ident.Map.t) :
|
||||
(scope_context : Name_resolution.scope_context) :
|
||||
Ast.scope_def Ast.ScopeDef.Map.t =
|
||||
(* Initializing the definitions of all scopes and subscope vars, with no rules
|
||||
yet inside *)
|
||||
let add_def _ v scope_def_map =
|
||||
let pos = match v with ScopeVar v | SubScope (v, _, _) -> Mark.get (ScopeVar.get_info v) in
|
||||
let new_def v_sig io = {
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = v_sig.Name_resolution.var_sig_typ;
|
||||
Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
|
||||
Ast.scope_def_parameters = v_sig.var_sig_parameters;
|
||||
Ast.scope_def_io = io;
|
||||
} in
|
||||
match v with
|
||||
| ScopeVar v -> (
|
||||
let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
|
||||
match v_sig.var_sig_states_list with
|
||||
| [] ->
|
||||
let def_key = Ast.ScopeDef.Var (v, None) in
|
||||
let def_key = ((v, pos), Ast.ScopeDef.Var None) in
|
||||
Ast.ScopeDef.Map.add def_key
|
||||
{
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = v_sig.var_sig_typ;
|
||||
Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
|
||||
Ast.scope_def_parameters = v_sig.var_sig_parameters;
|
||||
Ast.scope_def_io = attribute_to_io v_sig.var_sig_io;
|
||||
}
|
||||
(new_def v_sig (attribute_to_io v_sig.var_sig_io))
|
||||
scope_def_map
|
||||
| states ->
|
||||
let last_state = List.length states - 1 in
|
||||
let scope_def, _ =
|
||||
List.fold_left
|
||||
(fun (acc, i) state ->
|
||||
let def_key = Ast.ScopeDef.Var (v, Some state) in
|
||||
let def =
|
||||
{
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = v_sig.var_sig_typ;
|
||||
Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
|
||||
Ast.scope_def_parameters = v_sig.var_sig_parameters;
|
||||
Ast.scope_def_io =
|
||||
(* The first state should have the input I/O of the original
|
||||
variable, and the last state should have the output I/O
|
||||
of the original variable. All intermediate states shall
|
||||
have "internal" I/O.*)
|
||||
(let original_io = attribute_to_io v_sig.var_sig_io in
|
||||
let io_input =
|
||||
if i = 0 then original_io.io_input
|
||||
else NoInput, Mark.get (StateName.get_info state)
|
||||
in
|
||||
let io_output =
|
||||
if i = List.length states - 1 then original_io.io_output
|
||||
else false, Mark.get (StateName.get_info state)
|
||||
in
|
||||
{ io_input; io_output });
|
||||
}
|
||||
let def_key = (v, pos), Ast.ScopeDef.Var (Some state) in
|
||||
let original_io = attribute_to_io v_sig.var_sig_io in
|
||||
(* The first state should have the input I/O of the original
|
||||
variable, and the last state should have the output I/O
|
||||
of the original variable. All intermediate states shall
|
||||
have "internal" I/O.*)
|
||||
let io_input =
|
||||
if i = 0 then original_io.io_input
|
||||
else NoInput, Mark.get (StateName.get_info state)
|
||||
in
|
||||
let io_output =
|
||||
if i = last_state then original_io.io_output
|
||||
else false, Mark.get (StateName.get_info state)
|
||||
in
|
||||
let def = new_def v_sig { io_input; io_output } in
|
||||
Ast.ScopeDef.Map.add def_key def acc, i + 1)
|
||||
(scope_def_map, 0) states
|
||||
in
|
||||
scope_def)
|
||||
| SubScope (v0, subscope_uid) ->
|
||||
| SubScope (v0, subscope_uid, forward_out) ->
|
||||
let sub_scope_def = Name_resolution.get_scope_context ctxt subscope_uid in
|
||||
let ctxt =
|
||||
List.fold_left
|
||||
@ -1590,16 +1563,32 @@ let init_scope_defs
|
||||
ctxt
|
||||
(ScopeName.path subscope_uid)
|
||||
in
|
||||
let var_def = {
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = TStruct sub_scope_def.scope_out_struct, Mark.get (ScopeVar.get_info v0);
|
||||
Ast.scope_def_is_condition = false;
|
||||
Ast.scope_def_parameters = None;
|
||||
Ast.scope_def_io = { io_input = NoInput, Mark.get forward_out; io_output = forward_out };
|
||||
} in
|
||||
let scope_def_map =
|
||||
Ast.ScopeDef.Map.add ((v0, pos), Ast.ScopeDef.Var None) var_def scope_def_map
|
||||
in
|
||||
Ident.Map.fold
|
||||
(fun _ v scope_def_map ->
|
||||
match v with
|
||||
| SubScope _ -> scope_def_map
|
||||
| SubScope _ ->
|
||||
(* TODO: if we consider "input subscopes" at some point their inputs will need to be forwarded here *)
|
||||
scope_def_map
|
||||
| ScopeVar v ->
|
||||
(* TODO: shouldn't we ignore internal variables too at this point
|
||||
? *)
|
||||
let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
|
||||
let def_key =
|
||||
Ast.ScopeDef.SubScopeVar (v0, v, Mark.get (ScopeVar.get_info v))
|
||||
(v0, Mark.get (ScopeVar.get_info v)),
|
||||
Ast.ScopeDef.SubScope {
|
||||
name = subscope_uid;
|
||||
var_within_origin_scope = v;
|
||||
}
|
||||
in
|
||||
Ast.ScopeDef.Map.add def_key
|
||||
{
|
||||
@ -1612,7 +1601,7 @@ let init_scope_defs
|
||||
scope_def_map)
|
||||
sub_scope_def.Name_resolution.var_idmap scope_def_map
|
||||
in
|
||||
Ident.Map.fold add_def scope_idmap Ast.ScopeDef.Map.empty
|
||||
Ident.Map.fold add_def scope_context.var_idmap Ast.ScopeDef.Map.empty
|
||||
|
||||
(** Main function of this module *)
|
||||
let translate_program (ctxt : Name_resolution.context) (surface : S.program) :
|
||||
@ -1636,14 +1625,14 @@ let translate_program (ctxt : Name_resolution.context) (surface : S.program) :
|
||||
(fun _ v acc ->
|
||||
match v with
|
||||
| ScopeVar _ -> acc
|
||||
| SubScope (sub_var, sub_scope) ->
|
||||
| SubScope (sub_var, sub_scope, _) ->
|
||||
ScopeVar.Map.add sub_var sub_scope acc)
|
||||
s_context.Name_resolution.var_idmap ScopeVar.Map.empty
|
||||
in
|
||||
{
|
||||
Ast.scope_vars;
|
||||
scope_sub_scopes;
|
||||
scope_defs = init_scope_defs ctxt s_context.var_idmap;
|
||||
scope_defs = init_scope_defs ctxt s_context;
|
||||
scope_assertions = Ast.AssertionName.Map.empty;
|
||||
scope_meta_assertions = [];
|
||||
scope_options = [];
|
||||
|
@ -25,7 +25,7 @@ let detect_empty_definitions (p : program) : unit =
|
||||
ScopeDef.Map.iter
|
||||
(fun scope_def_key scope_def ->
|
||||
if
|
||||
(match scope_def_key with ScopeDef.Var _ -> true | _ -> false)
|
||||
(match scope_def_key with _, ScopeDef.Var _ -> true | _ -> false)
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules
|
||||
&& (not scope_def.scope_def_is_condition)
|
||||
&&
|
||||
@ -254,7 +254,7 @@ let detect_dead_code (p : program) : unit =
|
||||
| SubScope _ -> true
|
||||
| Var (var, state) ->
|
||||
let scope_def =
|
||||
ScopeDef.Map.find (Var (var, state)) scope.scope_defs
|
||||
ScopeDef.Map.find ((var, Pos.no_pos), ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
Mark.remove scope_def.scope_def_io.io_output
|
||||
(* A variable is initially alive if it is an output*)
|
||||
|
@ -35,6 +35,8 @@ type scope_context = {
|
||||
(** All variables, including scope variables and subscopes *)
|
||||
scope_defs_contexts : scope_def_context Ast.ScopeDef.Map.t;
|
||||
(** What is the default rule to refer to for unnamed exceptions, if any *)
|
||||
scope_in_struct : StructName.t;
|
||||
scope_out_struct : StructName.t;
|
||||
sub_scopes : ScopeName.Set.t;
|
||||
(** Other scopes referred to by this scope. Used for dependency analysis *)
|
||||
}
|
||||
@ -139,7 +141,7 @@ let get_subscope_uid
|
||||
((y, pos) : Ident.t Mark.pos) : ScopeVar.t =
|
||||
let scope = get_scope_context ctxt scope_uid in
|
||||
match Ident.Map.find_opt y scope.var_idmap with
|
||||
| Some (SubScope (sub_uid, _sub_id)) -> sub_uid
|
||||
| Some (SubScope (sub_uid, _sub_id, _)) -> sub_uid
|
||||
| _ -> raise_unknown_identifier "for a subscope of this scope" (y, pos)
|
||||
|
||||
(** [is_subscope_uid scope_uid ctxt y] returns true if [y] belongs to the
|
||||
@ -161,32 +163,18 @@ let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
|
||||
| _ -> false)
|
||||
scope.var_idmap
|
||||
|
||||
(** Retrieves the type of a scope definition from the context *)
|
||||
let get_def_typ (ctxt : context) (def : Ast.ScopeDef.t) : typ =
|
||||
let get_var_def (def: Ast.ScopeDef.t) : ScopeVar.t =
|
||||
match def with
|
||||
| Ast.ScopeDef.SubScopeVar (_, x, _)
|
||||
(* we don't need to look at the subscope prefix because [x] is already the uid
|
||||
referring back to the original subscope *)
|
||||
| Ast.ScopeDef.Var (x, _) ->
|
||||
get_var_typ ctxt x
|
||||
| ((v, _), Ast.ScopeDef.Var _)
|
||||
| (_, Ast.ScopeDef.SubScope { var_within_origin_scope = v; _ }) -> v
|
||||
|
||||
(** Retrieves the type of a scope definition from the context *)
|
||||
let get_params (ctxt : context) (def : Ast.ScopeDef.t) :
|
||||
(Uid.MarkedString.info * typ) list Mark.pos option =
|
||||
match def with
|
||||
| Ast.ScopeDef.SubScopeVar (_, x, _)
|
||||
(* we don't need to look at the subscope prefix because [x] is already the uid
|
||||
referring back to the original subscope *)
|
||||
| Ast.ScopeDef.Var (x, _) ->
|
||||
(ScopeVar.Map.find x ctxt.var_typs).var_sig_parameters
|
||||
(ScopeVar.Map.find (get_var_def def) ctxt.var_typs).var_sig_parameters
|
||||
|
||||
let is_def_cond (ctxt : context) (def : Ast.ScopeDef.t) : bool =
|
||||
match def with
|
||||
| Ast.ScopeDef.SubScopeVar (_, x, _)
|
||||
(* we don't need to look at the subscope prefix because [x] is already the uid
|
||||
referring back to the original subscope *)
|
||||
| Ast.ScopeDef.Var (x, _) ->
|
||||
is_var_cond ctxt x
|
||||
is_var_cond ctxt (get_var_def def)
|
||||
|
||||
let get_enum ctxt id =
|
||||
match Ident.Map.find (Mark.remove id) ctxt.local.typedefs with
|
||||
@ -267,6 +255,7 @@ let process_subscope_decl
|
||||
(ctxt : context)
|
||||
(decl : Surface.Ast.scope_decl_context_scope) : context =
|
||||
let name, name_pos = decl.scope_decl_context_scope_name in
|
||||
let forward_output = decl.Surface.Ast.scope_decl_context_scope_attribute.scope_decl_context_io_output in
|
||||
let (path, subscope), s_pos = decl.scope_decl_context_scope_sub_scope in
|
||||
let scope_ctxt = get_scope_context ctxt scope in
|
||||
match Ident.Map.find_opt (Mark.remove subscope) scope_ctxt.var_idmap with
|
||||
@ -274,7 +263,7 @@ let process_subscope_decl
|
||||
let info =
|
||||
match use with
|
||||
| ScopeVar v -> ScopeVar.get_info v
|
||||
| SubScope (ssc, _) -> ScopeVar.get_info ssc
|
||||
| SubScope (ssc, _, _) -> ScopeVar.get_info ssc
|
||||
in
|
||||
Message.raise_multispanned_error
|
||||
[Some "first use", Mark.get info; Some "second use", s_pos]
|
||||
@ -290,13 +279,26 @@ let process_subscope_decl
|
||||
scope_ctxt with
|
||||
var_idmap =
|
||||
Ident.Map.add name
|
||||
(SubScope (sub_scope_uid, original_subscope_uid))
|
||||
(SubScope (sub_scope_uid, original_subscope_uid, forward_output))
|
||||
scope_ctxt.var_idmap;
|
||||
sub_scopes =
|
||||
ScopeName.Set.add original_subscope_uid scope_ctxt.sub_scopes;
|
||||
}
|
||||
in
|
||||
{ ctxt with scopes = ScopeName.Map.add scope scope_ctxt ctxt.scopes }
|
||||
(* var_typs =
|
||||
* ScopeVar.Map.add uid
|
||||
* {
|
||||
* var_sig_typ = data_typ;
|
||||
* var_sig_is_condition = is_cond;
|
||||
* var_sig_parameters;
|
||||
* var_sig_io = decl.scope_decl_context_item_attribute;
|
||||
* var_sig_states_idmap = states_idmap;
|
||||
* var_sig_states_list = states_list;
|
||||
* }
|
||||
* ctxt.var_typs; *)
|
||||
|
||||
|
||||
|
||||
let is_type_cond ((typ, _) : Surface.Ast.typ) =
|
||||
match typ with
|
||||
@ -377,7 +379,7 @@ let process_data_decl
|
||||
let info =
|
||||
match use with
|
||||
| ScopeVar v -> ScopeVar.get_info v
|
||||
| SubScope (ssc, _) -> ScopeVar.get_info ssc
|
||||
| SubScope (ssc, _, _) -> ScopeVar.get_info ssc
|
||||
in
|
||||
Message.raise_multispanned_error
|
||||
[Some "First use:", Mark.get info; Some "Second use:", pos]
|
||||
@ -673,6 +675,8 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
|
||||
{
|
||||
var_idmap = Ident.Map.empty;
|
||||
scope_defs_contexts = Ast.ScopeDef.Map.empty;
|
||||
scope_in_struct = in_struct_name;
|
||||
scope_out_struct = out_struct_name;
|
||||
sub_scopes = ScopeName.Set.empty;
|
||||
}
|
||||
ctxt.scopes
|
||||
@ -762,9 +766,9 @@ let get_def_key
|
||||
| [x] ->
|
||||
let x_uid = get_var_uid scope_uid ctxt x in
|
||||
let var_sig = ScopeVar.Map.find x_uid ctxt.var_typs in
|
||||
(x_uid, pos),
|
||||
Ast.ScopeDef.Var
|
||||
( x_uid,
|
||||
match state with
|
||||
( match state with
|
||||
| Some state -> (
|
||||
try
|
||||
Some
|
||||
@ -789,19 +793,20 @@ let get_def_key
|
||||
ScopeVar.format x_uid
|
||||
else None )
|
||||
| [y; x] ->
|
||||
let (subscope_uid, subscope_real_uid) : ScopeVar.t * ScopeName.t =
|
||||
let (subscope_var, name) : ScopeVar.t * ScopeName.t =
|
||||
match Ident.Map.find_opt (Mark.remove y) scope_ctxt.var_idmap with
|
||||
| Some (SubScope (v, u)) -> v, u
|
||||
| Some (SubScope (v, u, _)) -> v, u
|
||||
| Some _ ->
|
||||
Message.raise_spanned_error pos
|
||||
"Invalid access to input variable, %a is not a subscope"
|
||||
"Invalid definition, %a is not a subscope"
|
||||
Print.lit_style (Mark.remove y)
|
||||
| None ->
|
||||
Message.raise_spanned_error pos "No definition found for subscope %a"
|
||||
Print.lit_style (Mark.remove y)
|
||||
in
|
||||
let x_uid = get_var_uid subscope_real_uid ctxt x in
|
||||
Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid, pos)
|
||||
let var_within_origin_scope = get_var_uid name ctxt x in
|
||||
(subscope_var, pos),
|
||||
Ast.ScopeDef.SubScope { name; var_within_origin_scope }
|
||||
| _ ->
|
||||
Message.raise_spanned_error pos
|
||||
"This line is defining a quantity that is neither a scope variable nor a \
|
||||
|
@ -35,6 +35,8 @@ type scope_context = {
|
||||
(** All variables, including scope variables and subscopes *)
|
||||
scope_defs_contexts : scope_def_context Ast.ScopeDef.Map.t;
|
||||
(** What is the default rule to refer to for unnamed exceptions, if any *)
|
||||
scope_in_struct : StructName.t;
|
||||
scope_out_struct : StructName.t;
|
||||
sub_scopes : ScopeName.Set.t;
|
||||
(** Other scopes referred to by this scope. Used for dependency analysis *)
|
||||
}
|
||||
@ -141,9 +143,6 @@ val is_subscope_uid : ScopeName.t -> context -> Ident.t -> bool
|
||||
val belongs_to : context -> ScopeVar.t -> ScopeName.t -> bool
|
||||
(** Checks if the var_uid belongs to the scope scope_uid *)
|
||||
|
||||
val get_def_typ : context -> Ast.ScopeDef.t -> typ
|
||||
(** Retrieves the type of a scope definition from the context *)
|
||||
|
||||
val get_params :
|
||||
context ->
|
||||
Ast.ScopeDef.t ->
|
||||
|
@ -339,7 +339,7 @@ module Commands = struct
|
||||
let get_variable_uid
|
||||
(ctxt : Desugared.Name_resolution.context)
|
||||
(scope_uid : ScopeName.t)
|
||||
(variable : string) =
|
||||
(variable : string): Desugared.Ast.ScopeDef.t =
|
||||
(* Sometimes the variable selected is of the form [a.b] *)
|
||||
let first_part, second_part =
|
||||
match String.index_opt variable '.' with
|
||||
@ -356,50 +356,20 @@ module Commands = struct
|
||||
Message.raise_error
|
||||
"Variable @{<yellow>\"%s\"@} not found inside scope @{<yellow>\"%a\"@}"
|
||||
variable ScopeName.format scope_uid
|
||||
| Some (SubScope (subscope_var_name, subscope_name)) -> (
|
||||
match second_part with
|
||||
| None ->
|
||||
Message.raise_error
|
||||
"Subscope @{<yellow>\"%a\"@} of scope @{<yellow>\"%a\"@} cannot be \
|
||||
selected by itself, please add \".<var>\" where <var> is a subscope \
|
||||
variable."
|
||||
ScopeVar.format subscope_var_name ScopeName.format scope_uid
|
||||
| Some second_part -> (
|
||||
match
|
||||
let ctxt =
|
||||
Desugared.Name_resolution.module_ctx ctxt
|
||||
(List.map
|
||||
(fun m -> ModuleName.to_string m, Pos.no_pos)
|
||||
(ScopeName.path subscope_name))
|
||||
in
|
||||
Ident.Map.find_opt second_part
|
||||
(ScopeName.Map.find subscope_name ctxt.scopes).var_idmap
|
||||
with
|
||||
| Some (ScopeVar v) ->
|
||||
Desugared.Ast.ScopeDef.SubScopeVar (subscope_var_name, v, Pos.no_pos)
|
||||
| _ ->
|
||||
| Some (ScopeVar v | SubScope (v, _, _)) ->
|
||||
let state =
|
||||
second_part |> Option.map @@ fun id ->
|
||||
let var_sig = ScopeVar.Map.find v ctxt.var_typs in
|
||||
match Ident.Map.find_opt id var_sig.var_sig_states_idmap with
|
||||
| Some state -> state
|
||||
| None ->
|
||||
Message.raise_error
|
||||
"Var @{<yellow>\"%s\"@} of subscope @{<yellow>\"%a\"@} in scope \
|
||||
@{<yellow>\"%a\"@} does not exist, please check your command line \
|
||||
arguments."
|
||||
second_part ScopeVar.format subscope_var_name ScopeName.format
|
||||
scope_uid))
|
||||
| Some (ScopeVar v) ->
|
||||
Desugared.Ast.ScopeDef.Var
|
||||
( v,
|
||||
Option.map
|
||||
(fun second_part ->
|
||||
let var_sig = ScopeVar.Map.find v ctxt.var_typs in
|
||||
match
|
||||
Ident.Map.find_opt second_part var_sig.var_sig_states_idmap
|
||||
with
|
||||
| Some state -> state
|
||||
| None ->
|
||||
Message.raise_error
|
||||
"State @{<yellow>\"%s\"@} is not found for variable \
|
||||
@{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
|
||||
second_part first_part ScopeName.format scope_uid)
|
||||
second_part )
|
||||
"State @{<yellow>\"%s\"@} is not found for variable \
|
||||
@{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
|
||||
id first_part ScopeName.format scope_uid
|
||||
in
|
||||
( (v, Pos.no_pos),
|
||||
Desugared.Ast.ScopeDef.Var state )
|
||||
|
||||
let get_output ?ext options output_file =
|
||||
let output_file = Option.map options.Global.path_rewrite output_file in
|
||||
|
@ -691,7 +691,7 @@ let format_scope_exec_args
|
||||
Message.raise_error
|
||||
"No scopes that don't require input were found, executable can't be \
|
||||
generated";
|
||||
Format.eprintf "@[<hov 2>Generating entry points for scopes:@ %a@]@."
|
||||
Message.emit_debug "@[<hov 2>Generating entry points for scopes:@ %a@]@."
|
||||
(Format.pp_print_list ~pp_sep:Format.pp_print_space (fun ppf (_, s, _) ->
|
||||
ScopeName.format ppf s))
|
||||
scopes_with_no_input;
|
||||
|
@ -39,9 +39,18 @@ let rec locations_used (e : 'm expr) : LocationSet.t =
|
||||
e LocationSet.empty
|
||||
|
||||
type 'm rule =
|
||||
| Definition of location Mark.pos * typ * Desugared.Ast.io * 'm expr
|
||||
| ScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
typ: typ;
|
||||
io: Desugared.Ast.io;
|
||||
e: 'm expr
|
||||
}
|
||||
| SubScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
typ: typ;
|
||||
e: 'm expr
|
||||
}
|
||||
| Assertion of 'm expr
|
||||
| Call of ScopeName.t * ScopeVar.t * 'm mark
|
||||
|
||||
type scope_var_ty = {
|
||||
svar_in_ty : typ;
|
||||
@ -66,16 +75,16 @@ type 'm program = {
|
||||
}
|
||||
|
||||
let type_rule decl_ctx env = function
|
||||
| Definition (loc, typ, io, expr) ->
|
||||
let expr' = Typing.expr decl_ctx ~env ~typ expr in
|
||||
Definition (loc, typ, io, Expr.unbox expr')
|
||||
| Assertion expr ->
|
||||
let typ = Mark.add (Expr.pos expr) (TLit TBool) in
|
||||
let expr' = Typing.expr decl_ctx ~env ~typ expr in
|
||||
Assertion (Expr.unbox expr')
|
||||
| Call (sc_name, ssc_name, m) ->
|
||||
let pos = Expr.mark_pos m in
|
||||
Call (sc_name, ssc_name, Typed { pos; ty = Mark.add pos TAny })
|
||||
| ScopeVarDefinition ({ typ; e; _ } as def) ->
|
||||
let e = Typing.expr decl_ctx ~env ~typ e in
|
||||
ScopeVarDefinition {def with e = Expr.unbox e}
|
||||
| SubScopeVarDefinition ({ typ; e; _ } as def) ->
|
||||
let e = Typing.expr decl_ctx ~env ~typ e in
|
||||
SubScopeVarDefinition { def with e = Expr.unbox e }
|
||||
| Assertion e ->
|
||||
let typ = Mark.add (Expr.pos e) (TLit TBool) in
|
||||
let e = Typing.expr decl_ctx ~env ~typ e in
|
||||
Assertion (Expr.unbox e)
|
||||
|
||||
let type_program (type m) (prg : m program) : typed program =
|
||||
(* Caution: this environment building code is very similar to that in
|
||||
|
@ -32,9 +32,21 @@ type 'm expr = (scopelang, 'm) gexpr
|
||||
val locations_used : 'm expr -> LocationSet.t
|
||||
|
||||
type 'm rule =
|
||||
| Definition of location Mark.pos * typ * Desugared.Ast.io * 'm expr
|
||||
| ScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
typ: typ;
|
||||
io: Desugared.Ast.io;
|
||||
e: 'm expr
|
||||
}
|
||||
| SubScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos; (** Variable within the current scope *)
|
||||
(* scope: ScopeVar.t Mark.pos; (\** Variable pointing to the *\) *)
|
||||
(* origin_var: ScopeVar.t Mark.pos;
|
||||
* reentrant: bool; *)
|
||||
typ: typ; (* non-thunked at this point for reentrant vars *)
|
||||
e: 'm expr
|
||||
}
|
||||
| Assertion of 'm expr
|
||||
| Call of ScopeName.t * ScopeVar.t * 'm mark
|
||||
|
||||
type scope_var_ty = {
|
||||
svar_in_ty : typ;
|
||||
|
@ -94,15 +94,10 @@ let rec expr_used_defs e =
|
||||
| e -> recurse_subterms e
|
||||
|
||||
let rule_used_defs = function
|
||||
| Ast.Assertion e | Ast.Definition (_, _, _, e) ->
|
||||
| Ast.Assertion e | Ast.ScopeVarDefinition { e; _} | Ast.SubScopeVarDefinition { e; _ } ->
|
||||
(* TODO: maybe this info could be passed on from previous passes without
|
||||
walking through all exprs again *)
|
||||
expr_used_defs e
|
||||
| Ast.Call (subscope, subindex, _) ->
|
||||
if ScopeName.path subscope = [] then
|
||||
VMap.singleton (Scope subscope)
|
||||
(Mark.get (ScopeVar.get_info subindex))
|
||||
else VMap.empty
|
||||
|
||||
let build_program_dep_graph (prgm : 'm Ast.program) : SDependencies.t =
|
||||
let g = SDependencies.empty in
|
||||
|
@ -58,15 +58,6 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed =
|
||||
ctx (Array.to_list vars) (Array.to_list new_vars)
|
||||
in
|
||||
Expr.eabs (Expr.bind new_vars (translate_expr ctx body)) tys m
|
||||
| ELocation (SubScopeVar { scope; alias; var }) ->
|
||||
(* When referring to a subscope variable in an expression, we are referring
|
||||
to the output, hence we take the last state. *)
|
||||
let var =
|
||||
match ScopeVar.Map.find (Mark.remove var) ctx.scope_var_mapping with
|
||||
| WholeVar new_s_var -> Mark.copy var new_s_var
|
||||
| States states -> Mark.copy var (snd (List.hd (List.rev states)))
|
||||
in
|
||||
Expr.elocation (SubScopeVar { scope; alias; var }) m
|
||||
| ELocation (DesugaredScopeVar { name; state = None }) ->
|
||||
Expr.elocation
|
||||
(ScopelangScopeVar
|
||||
@ -200,8 +191,9 @@ let def_to_exception_graph
|
||||
|
||||
let rule_to_exception_graph (scope : D.scope) = function
|
||||
| Desugared.Dependency.Vertex.Var (var, state) -> (
|
||||
let pos = Mark.get (ScopeVar.get_info var) in
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find (D.ScopeDef.Var (var, state)) scope.scope_defs
|
||||
D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
let var_def = scope_def.D.scope_def_rules in
|
||||
match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
@ -220,76 +212,62 @@ let rule_to_exception_graph (scope : D.scope) = function
|
||||
(* we do not provide any definition for an input-only variable *)
|
||||
| _ ->
|
||||
D.ScopeDef.Map.singleton
|
||||
(D.ScopeDef.Var (var, state))
|
||||
(def_to_exception_graph (D.ScopeDef.Var (var, state)) var_def))
|
||||
((var, pos), (D.ScopeDef.Var state))
|
||||
(def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
|
||||
| Desugared.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_vars_redefs_candidates =
|
||||
D.ScopeDef.Map.filter
|
||||
(fun def_key scope_def ->
|
||||
match def_key with
|
||||
| D.ScopeDef.Var _ -> false
|
||||
| D.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
|
||||
((match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput -> true
|
||||
| _ -> false)
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules))
|
||||
scope.scope_defs
|
||||
in
|
||||
let sub_scope_vars_redefs =
|
||||
D.ScopeDef.Map.mapi
|
||||
(fun def_key scope_def ->
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
match def_key with
|
||||
| D.ScopeDef.Var _ -> assert false (* should not happen *)
|
||||
| D.ScopeDef.SubScopeVar (sscope, sub_scope_var, pos) ->
|
||||
(* 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 Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput ->
|
||||
Message.raise_multispanned_error
|
||||
(( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info sscope) )
|
||||
:: ( Some "Incriminated variable:",
|
||||
Mark.get (ScopeVar.get_info sub_scope_var) )
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
D.ScopeDef.Map.fold
|
||||
(fun (sscope, kind as def_key) scope_def exc_graphs ->
|
||||
match kind with
|
||||
| D.ScopeDef.Var _ -> exc_graphs
|
||||
| D.ScopeDef.SubScope _
|
||||
when
|
||||
not (ScopeVar.equal sub_scope_index (Mark.remove sscope))
|
||||
||
|
||||
Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules
|
||||
->
|
||||
(* We exclude subscope variables that have 0 re-definitions and are
|
||||
not visible in the input of the subscope *)
|
||||
exc_graphs
|
||||
| D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
(* 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. *)
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
let () = match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput ->
|
||||
Message.raise_multispanned_error
|
||||
(( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) )
|
||||
:: ( Some "Incriminated variable:",
|
||||
Mark.get (ScopeVar.get_info var_within_origin_scope) )
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
( Some "Incriminated subscope variable definition:",
|
||||
Mark.get (RuleName.get_info rule) ))
|
||||
(RuleName.Map.keys def))
|
||||
"It is impossible to give a definition to a subscope variable \
|
||||
not tagged as input or context."
|
||||
| OnlyInput when RuleName.Map.is_empty def && not is_cond ->
|
||||
(* If the subscope variable is tagged as input, then it shall be
|
||||
defined. *)
|
||||
Message.raise_multispanned_error
|
||||
[
|
||||
( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info sscope) );
|
||||
Some "Incriminated variable:", pos;
|
||||
]
|
||||
"This subscope variable is a mandatory input but no definition \
|
||||
was provided."
|
||||
| _ -> ());
|
||||
let exc_graph = def_to_exception_graph def_key def in
|
||||
let var_pos = D.ScopeDef.get_position def_key in
|
||||
exc_graph, sub_scope_var, var_pos)
|
||||
sub_scope_vars_redefs_candidates
|
||||
in
|
||||
List.fold_left
|
||||
(fun exc_graphs (new_exc_graph, subscope_var, var_pos) ->
|
||||
D.ScopeDef.Map.add
|
||||
(D.ScopeDef.SubScopeVar (sub_scope_index, subscope_var, var_pos))
|
||||
new_exc_graph exc_graphs)
|
||||
(RuleName.Map.keys def))
|
||||
"Invalid assignment to a subscope variable that is \
|
||||
not tagged as input or context."
|
||||
| OnlyInput when RuleName.Map.is_empty def && not is_cond ->
|
||||
(* If the subscope variable is tagged as input, then it shall be
|
||||
defined. *)
|
||||
Message.raise_multispanned_error
|
||||
[
|
||||
( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) );
|
||||
Some "Incriminated variable:", Mark.get sscope;
|
||||
]
|
||||
"This subscope variable is a mandatory input but no definition \
|
||||
was provided."
|
||||
| _ -> ()
|
||||
in
|
||||
let new_exc_graph = def_to_exception_graph def_key def in
|
||||
D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
|
||||
scope.scope_defs
|
||||
D.ScopeDef.Map.empty
|
||||
(D.ScopeDef.Map.values sub_scope_vars_redefs)
|
||||
| Assertion _ -> D.ScopeDef.Map.empty (* no exceptions for assertions *)
|
||||
|
||||
let scope_to_exception_graphs (scope : D.scope) :
|
||||
@ -576,8 +554,10 @@ let translate_rule
|
||||
(exc_graphs :
|
||||
Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t) = function
|
||||
| Desugared.Dependency.Vertex.Var (var, state) -> (
|
||||
let pos = Mark.get (ScopeVar.get_info var) in
|
||||
(* TODO: this may point to the place where the variable was declared instead of the binding in the definition being explored. Needs double-checking and maybe adding more position information *)
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find (D.ScopeDef.Var (var, state)) scope.scope_defs
|
||||
D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
let var_def = scope_def.D.scope_def_rules in
|
||||
let var_params = scope_def.D.scope_def_parameters in
|
||||
@ -589,7 +569,7 @@ let translate_rule
|
||||
| OnlyInput -> []
|
||||
(* we do not provide any definition for an input-only variable *)
|
||||
| _ ->
|
||||
let scope_def_key = D.ScopeDef.Var (var, state) in
|
||||
let scope_def_key = (var, pos), D.ScopeDef.Var state in
|
||||
let expr_def =
|
||||
translate_def ctx scope_def_key var_def var_params var_typ
|
||||
scope_def.D.scope_def_io
|
||||
@ -603,97 +583,105 @@ let translate_rule
|
||||
| _ -> failwith "should not happen"
|
||||
in
|
||||
[
|
||||
Ast.Definition
|
||||
( ( ScopelangScopeVar
|
||||
{ name = scope_var, Mark.get (ScopeVar.get_info scope_var) },
|
||||
Mark.get (ScopeVar.get_info scope_var) ),
|
||||
var_typ,
|
||||
scope_def.D.scope_def_io,
|
||||
Expr.unbox expr_def );
|
||||
Ast.ScopeVarDefinition {
|
||||
var = scope_var, pos;
|
||||
typ = var_typ;
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox expr_def;
|
||||
}
|
||||
])
|
||||
| Desugared.Dependency.Vertex.SubScope sub_scope_index ->
|
||||
(* Before calling the sub_scope, we need to include all the re-definitions
|
||||
| Desugared.Dependency.Vertex.SubScope subscope_var ->
|
||||
(* Before calling the subscope, we need to include all the re-definitions
|
||||
of subscope parameters*)
|
||||
let sub_scope =
|
||||
ScopeVar.Map.find sub_scope_index scope.scope_sub_scopes
|
||||
let subscope =
|
||||
ScopeVar.Map.find subscope_var scope.scope_sub_scopes
|
||||
in
|
||||
let sub_scope_vars_redefs_candidates =
|
||||
D.ScopeDef.Map.filter
|
||||
(fun def_key scope_def ->
|
||||
match def_key with
|
||||
| D.ScopeDef.Var _ -> false
|
||||
| D.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
|
||||
((match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput -> true
|
||||
| _ -> false)
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules))
|
||||
scope.scope_defs
|
||||
let subscope_params =
|
||||
scope.scope_defs |> D.ScopeDef.Map.filter @@ fun def_key scope_def ->
|
||||
match def_key with
|
||||
| _, D.ScopeDef.Var _ -> false
|
||||
| (v, _), D.ScopeDef.SubScope _ ->
|
||||
ScopeVar.equal subscope_var v
|
||||
(* We exclude subscope variables that have 0 re-definitions and are
|
||||
not visible in the input of the subscope *)
|
||||
&& not
|
||||
(Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules)
|
||||
in
|
||||
let sub_scope_vars_redefs =
|
||||
D.ScopeDef.Map.mapi
|
||||
(fun def_key scope_def ->
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let def_typ = scope_def.scope_def_typ in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
match def_key with
|
||||
| D.ScopeDef.Var _ -> assert false (* should not happen *)
|
||||
| D.ScopeDef.SubScopeVar (_, sub_scope_var, var_pos) ->
|
||||
(* 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 Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput -> assert false (* error already raised *)
|
||||
| OnlyInput when RuleName.Map.is_empty def && not is_cond ->
|
||||
assert false (* error already raised *)
|
||||
| _ -> ());
|
||||
(* Now that all is good, we can proceed with translating this
|
||||
redefinition to a proper Scopelang term. *)
|
||||
let expr_def =
|
||||
translate_def ctx def_key def scope_def.D.scope_def_parameters
|
||||
def_typ scope_def.D.scope_def_io
|
||||
(D.ScopeDef.Map.find def_key exc_graphs)
|
||||
~is_cond ~is_subscope_var:true
|
||||
in
|
||||
let def_typ =
|
||||
Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
|
||||
in
|
||||
let subscop_real_name =
|
||||
ScopeVar.Map.find sub_scope_index scope.scope_sub_scopes
|
||||
in
|
||||
Ast.Definition
|
||||
( ( SubScopeVar
|
||||
{
|
||||
scope = subscop_real_name;
|
||||
alias = sub_scope_index, var_pos;
|
||||
var =
|
||||
(match
|
||||
ScopeVar.Map.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);
|
||||
},
|
||||
var_pos ),
|
||||
def_typ,
|
||||
scope_def.D.scope_def_io,
|
||||
Expr.unbox expr_def ))
|
||||
sub_scope_vars_redefs_candidates
|
||||
let subscope_params =
|
||||
subscope_params |> D.ScopeDef.Map.mapi @@ fun def_key scope_def ->
|
||||
let v, kind = def_key in
|
||||
let pos = Mark.get v in
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let def_typ = scope_def.scope_def_typ in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
match kind with
|
||||
| D.ScopeDef.Var _ -> assert false
|
||||
| D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
(* 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. *)
|
||||
assert (* an error should have been already raised *)
|
||||
(match scope_def.D.scope_def_io.io_input with
|
||||
| NoInput, _ -> false
|
||||
| OnlyInput, _ -> is_cond || not (RuleName.Map.is_empty def)
|
||||
| _ -> true);
|
||||
(* Now that all is good, we can proceed with translating this
|
||||
redefinition to a proper Scopelang term. *)
|
||||
let def_var =
|
||||
ScopeVar.fresh
|
||||
(String.concat "."
|
||||
[Mark.remove (ScopeVar.get_info (Mark.remove v));
|
||||
Mark.remove (ScopeVar.get_info var_within_origin_scope)],
|
||||
pos)
|
||||
in
|
||||
let expr_def =
|
||||
translate_def ctx def_key def scope_def.D.scope_def_parameters
|
||||
def_typ scope_def.D.scope_def_io
|
||||
(D.ScopeDef.Map.find def_key exc_graphs)
|
||||
~is_cond ~is_subscope_var:true
|
||||
in
|
||||
Ast.SubScopeVarDefinition {
|
||||
var = def_var, pos;
|
||||
typ = Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input;
|
||||
(* alias = v;
|
||||
* (\* var = def_var, pos; *\)
|
||||
* origin_var = var_within_origin_scope, pos;
|
||||
* typ = Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input;
|
||||
* scope = (name, pos); *)
|
||||
e = Expr.unbox expr_def;
|
||||
}
|
||||
in
|
||||
let sub_scope_vars_redefs = D.ScopeDef.Map.values sub_scope_vars_redefs in
|
||||
sub_scope_vars_redefs
|
||||
@ [
|
||||
Ast.Call
|
||||
( sub_scope,
|
||||
sub_scope_index,
|
||||
Untyped { pos = Mark.get (ScopeVar.get_info sub_scope_index) }
|
||||
);
|
||||
]
|
||||
let subscope_param_map =
|
||||
D.ScopeDef.Map.fold (fun (scope_v, _) def acc -> match def with
|
||||
| Ast.SubScopeVarDefinition { var; _ } ->
|
||||
ScopeVar.Map.add (Mark.remove scope_v)
|
||||
(Expr.elocation (ScopelangScopeVar { name = var })
|
||||
(Untyped { pos = Mark.get var }))
|
||||
acc
|
||||
| _ -> assert false)
|
||||
subscope_params ScopeVar.Map.empty
|
||||
in
|
||||
let pos = Mark.get (ScopeVar.get_info subscope_var) in
|
||||
(* TODO: see remark above about positions *)
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((subscope_var, pos), D.ScopeDef.Var None) scope.scope_defs
|
||||
in
|
||||
assert (RuleName.Map.is_empty scope_def.D.scope_def_rules);
|
||||
(* The subscope will be defined by its inputs, it's not supposed to have direct rules yet *)
|
||||
let scope_info = ScopeName.Map.find subscope ctx.decl_ctx.ctx_scopes in
|
||||
let subscope_call_expr =
|
||||
Expr.escopecall ~scope:subscope ~args:subscope_param_map (Untyped { pos })
|
||||
in
|
||||
let subscope_def =
|
||||
Ast.ScopeVarDefinition {
|
||||
var = subscope_var, pos;
|
||||
typ = TStruct scope_info.out_struct_name, Mark.get (ScopeVar.get_info subscope_var);
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox subscope_call_expr;
|
||||
}
|
||||
in
|
||||
D.ScopeDef.Map.values subscope_params @ [ subscope_def ]
|
||||
| Assertion a_name ->
|
||||
let assertion_expr =
|
||||
D.AssertionName.Map.find a_name scope.scope_assertions
|
||||
@ -721,7 +709,7 @@ let translate_scope_interface ctx scope =
|
||||
match states with
|
||||
| WholeVar ->
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find (D.ScopeDef.Var (var, None)) scope.D.scope_defs
|
||||
D.ScopeDef.Map.find ((var, Pos.no_pos), D.ScopeDef.Var None) scope.D.scope_defs
|
||||
in
|
||||
ScopeVar.Map.add
|
||||
(match ScopeVar.Map.find var ctx.scope_var_mapping with
|
||||
@ -736,7 +724,7 @@ let translate_scope_interface ctx scope =
|
||||
(fun acc (state : StateName.t) ->
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find
|
||||
(D.ScopeDef.Var (var, Some state))
|
||||
((var, Pos.no_pos), D.ScopeDef.Var (Some state))
|
||||
scope.D.scope_defs
|
||||
in
|
||||
ScopeVar.Map.add
|
||||
@ -801,52 +789,69 @@ let translate_program
|
||||
let add_scope_mappings modul ctx =
|
||||
ScopeName.Map.fold
|
||||
(fun _ scdef ctx ->
|
||||
ScopeVar.Map.fold
|
||||
(fun scope_var (states : D.var_or_states) ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info scope_var in
|
||||
let new_var =
|
||||
match states with
|
||||
| D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
|
||||
| States states ->
|
||||
let var_prefix = var_name ^ "_" in
|
||||
let state_var state =
|
||||
ScopeVar.fresh
|
||||
(Mark.map (( ^ ) var_prefix) (StateName.get_info state))
|
||||
let ctx =
|
||||
(* Add normal scope vars to the env *)
|
||||
ScopeVar.Map.fold
|
||||
(fun scope_var (states : D.var_or_states) ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info scope_var in
|
||||
let new_var =
|
||||
match states with
|
||||
| D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
|
||||
| States states ->
|
||||
let var_prefix = var_name ^ "_" in
|
||||
let state_var state =
|
||||
ScopeVar.fresh
|
||||
(Mark.map (( ^ ) var_prefix) (StateName.get_info state))
|
||||
in
|
||||
States (List.map (fun state -> state, state_var state) states)
|
||||
in
|
||||
States (List.map (fun state -> state, state_var state) states)
|
||||
in
|
||||
let reentrant =
|
||||
let state =
|
||||
match states with
|
||||
| D.WholeVar -> None
|
||||
| States (s :: _) -> Some s
|
||||
| States [] -> assert false
|
||||
in
|
||||
match
|
||||
D.ScopeDef.Map.find_opt
|
||||
(Var (scope_var, state))
|
||||
scdef.D.scope_defs
|
||||
with
|
||||
| Some
|
||||
{
|
||||
scope_def_io = { io_input = Runtime.Reentrant, _; _ };
|
||||
scope_def_typ;
|
||||
_;
|
||||
} ->
|
||||
Some scope_def_typ
|
||||
| _ -> None
|
||||
in
|
||||
{
|
||||
ctx with
|
||||
scope_var_mapping =
|
||||
ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
|
||||
reentrant_vars =
|
||||
Option.fold reentrant
|
||||
~some:(fun ty ->
|
||||
ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
|
||||
~none:ctx.reentrant_vars;
|
||||
})
|
||||
scdef.D.scope_vars ctx)
|
||||
let reentrant =
|
||||
let state =
|
||||
match states with
|
||||
| D.WholeVar -> None
|
||||
| States (s :: _) -> Some s
|
||||
| States [] -> assert false
|
||||
in
|
||||
match
|
||||
D.ScopeDef.Map.find_opt
|
||||
((scope_var, Pos.no_pos), Var state)
|
||||
scdef.D.scope_defs
|
||||
with
|
||||
| Some
|
||||
{
|
||||
scope_def_io = { io_input = Runtime.Reentrant, _; _ };
|
||||
scope_def_typ;
|
||||
_;
|
||||
} ->
|
||||
Some scope_def_typ
|
||||
| _ -> None
|
||||
in
|
||||
{
|
||||
ctx with
|
||||
scope_var_mapping =
|
||||
ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
|
||||
reentrant_vars =
|
||||
Option.fold reentrant
|
||||
~some:(fun ty ->
|
||||
ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
|
||||
~none:ctx.reentrant_vars;
|
||||
})
|
||||
scdef.D.scope_vars ctx
|
||||
in
|
||||
let ctx =
|
||||
(* Add scope vars pointing to subscope executions to the env
|
||||
(their definitions are introduced during the processing of the rules above) *)
|
||||
ScopeVar.Map.fold (fun var _ ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info var in
|
||||
let scope_var_mapping =
|
||||
let new_var = WholeVar (ScopeVar.fresh (var_name, var_pos)) in
|
||||
ScopeVar.Map.add var new_var ctx.scope_var_mapping
|
||||
in
|
||||
{ ctx with scope_var_mapping }
|
||||
)
|
||||
scdef.D.scope_sub_scopes ctx
|
||||
in
|
||||
ctx)
|
||||
modul.D.module_scopes ctx
|
||||
in
|
||||
(* Todo: since we rename all scope vars at this point, it would be better to
|
||||
|
@ -72,31 +72,29 @@ let scope ?debug ctx fmt (name, (decl, _pos)) =
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " Print.punctuation ";")
|
||||
(fun fmt rule ->
|
||||
match rule with
|
||||
| Definition (loc, typ, _, e) ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]" Print.keyword
|
||||
"let" Print.location (Mark.remove loc) Print.punctuation ":"
|
||||
| ScopeVarDefinition { var; typ; io; e; } ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %t%a@]"
|
||||
Print.keyword "let"
|
||||
ScopeVar.format (Mark.remove var)
|
||||
Print.punctuation ":"
|
||||
(Print.typ ctx) typ Print.punctuation "="
|
||||
(fun fmt e ->
|
||||
match Mark.remove loc with
|
||||
| SubScopeVar _ | ToplevelVar _ -> Print.expr () fmt e
|
||||
| ScopelangScopeVar { name = v } -> (
|
||||
match
|
||||
Mark.remove
|
||||
(ScopeVar.Map.find (Mark.remove v) decl.scope_sig).svar_io
|
||||
.io_input
|
||||
with
|
||||
| Reentrant ->
|
||||
Format.fprintf fmt "%a@ %a" Print.op_style
|
||||
"reentrant or by default" (Print.expr ?debug ()) e
|
||||
| _ -> Format.fprintf fmt "%a" (Print.expr ?debug ()) e))
|
||||
e
|
||||
(fun fmt -> match Mark.remove io.io_input with
|
||||
| Reentrant ->
|
||||
Print.op_style fmt "reentrant or by default";
|
||||
Format.pp_print_space fmt ()
|
||||
| _ -> ())
|
||||
(Print.expr ?debug ()) e
|
||||
| SubScopeVarDefinition { var; typ; e } ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]"
|
||||
Print.keyword "let"
|
||||
ScopeVar.format (Mark.remove var)
|
||||
Print.punctuation ":"
|
||||
(Print.typ ctx) typ
|
||||
Print.punctuation "="
|
||||
(Print.expr ?debug ()) e
|
||||
| Assertion e ->
|
||||
Format.fprintf fmt "%a %a" Print.keyword "assert"
|
||||
(Print.expr ?debug ()) e
|
||||
| Call (scope_name, subscope_name, _) ->
|
||||
Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call"
|
||||
ScopeName.format scope_name Print.punctuation "["
|
||||
ScopeVar.format subscope_name Print.punctuation "]"))
|
||||
(Print.expr ?debug ()) e))
|
||||
decl.scope_decl_rules
|
||||
|
||||
let print_topdef ctx ppf name (e, ty) =
|
||||
|
@ -97,7 +97,8 @@ module ScopeVar =
|
||||
|
||||
type scope_var_or_subscope =
|
||||
| ScopeVar of ScopeVar.t
|
||||
| SubScope of ScopeVar.t * ScopeName.t
|
||||
| SubScope of ScopeVar.t * ScopeName.t * bool Mark.pos
|
||||
(* The bool is true if the output of the subscope is to be forwarded *)
|
||||
|
||||
module StateName =
|
||||
Uid.Gen
|
||||
@ -437,12 +438,6 @@ type 'a glocation =
|
||||
name : ScopeVar.t Mark.pos;
|
||||
}
|
||||
-> < scopeVarSimpl : yes ; .. > glocation
|
||||
| SubScopeVar : {
|
||||
scope : ScopeName.t;
|
||||
alias : ScopeVar.t Mark.pos;
|
||||
var : ScopeVar.t Mark.pos;
|
||||
}
|
||||
-> < explicitScopes : yes ; .. > glocation
|
||||
| ToplevelVar : {
|
||||
name : TopdefName.t Mark.pos;
|
||||
}
|
||||
|
@ -550,18 +550,12 @@ let compare_location
|
||||
if cmp = 0 then StateName.compare sx sy else cmp
|
||||
| ScopelangScopeVar { name = vx, _ }, ScopelangScopeVar { name = vy, _ } ->
|
||||
ScopeVar.compare vx vy
|
||||
| ( SubScopeVar { alias = xsubindex, _; var = xsubvar, _; _ },
|
||||
SubScopeVar { alias = ysubindex, _; var = ysubvar, _; _ } ) ->
|
||||
let c = ScopeVar.compare xsubindex ysubindex in
|
||||
if c = 0 then ScopeVar.compare xsubvar ysubvar else c
|
||||
| ToplevelVar { name = vx, _ }, ToplevelVar { name = vy, _ } ->
|
||||
TopdefName.compare vx vy
|
||||
| DesugaredScopeVar _, _ -> -1
|
||||
| _, DesugaredScopeVar _ -> 1
|
||||
| ScopelangScopeVar _, _ -> -1
|
||||
| _, ScopelangScopeVar _ -> 1
|
||||
| SubScopeVar _, _ -> -1
|
||||
| _, SubScopeVar _ -> 1
|
||||
| ToplevelVar _, _ -> .
|
||||
| _, ToplevelVar _ -> .
|
||||
|
||||
|
@ -74,9 +74,6 @@ let location (type a) (fmt : Format.formatter) (l : a glocation) : unit =
|
||||
match l with
|
||||
| DesugaredScopeVar { name; _ } -> ScopeVar.format fmt (Mark.remove name)
|
||||
| ScopelangScopeVar { name; _ } -> ScopeVar.format fmt (Mark.remove name)
|
||||
| SubScopeVar { alias = subindex; var = subvar; _ } ->
|
||||
Format.fprintf fmt "%a.%a" ScopeVar.format (Mark.remove subindex)
|
||||
ScopeVar.format (Mark.remove subvar)
|
||||
| ToplevelVar { name } -> TopdefName.format fmt (Mark.remove name)
|
||||
|
||||
let external_ref fmt er =
|
||||
|
@ -406,10 +406,6 @@ module Env = struct
|
||||
let get_scope_var t sv = A.ScopeVar.Map.find_opt sv t.scope_vars
|
||||
let get_toplevel_var t v = A.TopdefName.Map.find_opt v t.toplevel_vars
|
||||
|
||||
let get_subscope_out_var t scope var =
|
||||
Option.bind (A.ScopeName.Map.find_opt scope t.scopes) (fun vmap ->
|
||||
A.ScopeVar.Map.find_opt var vmap)
|
||||
|
||||
let add v tau t = { t with vars = Var.Map.add v tau t.vars }
|
||||
let add_var v typ t = add v (ast_to_typ typ) t
|
||||
|
||||
@ -503,8 +499,6 @@ and typecheck_expr_top_down :
|
||||
match loc with
|
||||
| DesugaredScopeVar { name; _ } | ScopelangScopeVar { name } ->
|
||||
Env.get_scope_var env (Mark.remove name)
|
||||
| SubScopeVar { scope; var; _ } ->
|
||||
Env.get_subscope_out_var env scope (Mark.remove var)
|
||||
| ToplevelVar { name } -> Env.get_toplevel_var env (Mark.remove name)
|
||||
in
|
||||
let ty =
|
||||
@ -561,11 +555,11 @@ and typecheck_expr_top_down :
|
||||
| A.EDStructAccess { e = e_struct; name_opt; field } ->
|
||||
let t_struct =
|
||||
match name_opt with
|
||||
| Some name -> TStruct name
|
||||
| None -> TAny (Any.fresh ())
|
||||
| Some name -> unionfind (TStruct name)
|
||||
| None -> unionfind (TAny (Any.fresh ()))
|
||||
in
|
||||
let e_struct' =
|
||||
typecheck_expr_top_down ctx env (unionfind t_struct) e_struct
|
||||
typecheck_expr_top_down ctx env t_struct e_struct
|
||||
in
|
||||
let name =
|
||||
match UnionFind.get (ty e_struct') with
|
||||
@ -575,7 +569,7 @@ and typecheck_expr_top_down :
|
||||
"Disambiguation failed before reaching field %s" field
|
||||
| _ ->
|
||||
Message.raise_spanned_error (Expr.pos e)
|
||||
"This is not a structure, cannot access field %s (%a)" field
|
||||
"This is not a structure, cannot access field %s (found type: %a)" field
|
||||
(format_typ ctx) (ty e_struct')
|
||||
in
|
||||
let str =
|
||||
|
Loading…
Reference in New Issue
Block a user