Propagate visibility down, missing handling in scope_to_dcalc

This commit is contained in:
Denis Merigoux 2022-02-04 14:34:25 +01:00
parent e0a52168f4
commit d8c120bf97
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
6 changed files with 19 additions and 20 deletions

View File

@ -269,8 +269,9 @@ let translate_scope (scope : Ast.scope) : Scopelang.Ast.scope_decl =
let scope_sig =
Scopelang.Ast.ScopeVarSet.fold
(fun var acc ->
let typ = (Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs).scope_def_typ in
Scopelang.Ast.ScopeVarMap.add var typ acc)
let scope_def = Ast.ScopeDefMap.find (Ast.ScopeDef.Var var) scope.scope_defs in
let typ = scope_def.scope_def_typ in
Scopelang.Ast.ScopeVarMap.add var (typ, scope_def.scope_def_visibility) acc)
scope.scope_vars Scopelang.Ast.ScopeVarMap.empty
in
{

View File

@ -118,16 +118,16 @@ let rec locations_used (e : expr Pos.marked) : LocationSet.t =
List.fold_left (fun acc e' -> LocationSet.union acc (locations_used e')) LocationSet.empty es
| ErrorOnEmpty e' -> locations_used e'
type visibility = { visibility_output : bool; visibility_input : bool }
type rule =
| Definition of location Pos.marked * typ Pos.marked * expr Pos.marked
| Assertion of expr Pos.marked
| Call of ScopeName.t * SubScopeName.t
type visibility = { visibility_output : bool; visibility_input : bool }
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : typ Pos.marked ScopeVarMap.t;
scope_sig : (typ Pos.marked * visibility) ScopeVarMap.t;
scope_decl_rules : rule list;
}

View File

@ -84,19 +84,19 @@ type expr =
val locations_used : expr Pos.marked -> LocationSet.t
type rule =
| Definition of location Pos.marked * typ Pos.marked * expr Pos.marked
| Assertion of expr Pos.marked
| Call of ScopeName.t * SubScopeName.t
type visibility = {
visibility_output : bool; (** True if present in the scope's output *)
visibility_input : bool; (** True if present in the scope's input (reentrant) *)
}
type rule =
| Definition of location Pos.marked * typ Pos.marked * expr Pos.marked
| Assertion of expr Pos.marked
| Call of ScopeName.t * SubScopeName.t
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : typ Pos.marked ScopeVarMap.t;
scope_sig : (typ Pos.marked * visibility) ScopeVarMap.t;
scope_decl_rules : rule list;
}

View File

@ -147,8 +147,10 @@ let format_scope (fmt : Format.formatter) ((name, decl) : ScopeName.t * scope_de
ScopeName.format_t name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(fun fmt (scope_var, typ) ->
Format.fprintf fmt "(%a: %a)" ScopeVar.format_t scope_var format_typ typ))
(fun fmt (scope_var, (typ, vis)) ->
Format.fprintf fmt "(%a: %a%s%s)" ScopeVar.format_t scope_var format_typ typ
(if vis.visibility_input then "|input" else "")
(if vis.visibility_output then "|output" else "")))
(ScopeVarMap.bindings decl.scope_sig)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@\n")

View File

@ -644,16 +644,12 @@ let translate_program (prgm : Ast.program) : Dcalc.Ast.program * Dependency.TVer
{
scope_sig_local_vars =
List.map
(fun (scope_var, tau) ->
(fun (scope_var, (tau, vis)) ->
let tau = translate_typ (ctx_for_typ_translation scope_name) tau in
{
scope_var_name = scope_var;
scope_var_typ = Pos.unmark tau;
scope_var_visibility =
{
visibility_input = true;
visibility_output = true (* TODO: change with info from desugared *);
};
scope_var_visibility = vis;
})
(Ast.ScopeVarMap.bindings scope.scope_sig);
scope_sig_scope_var = scope_dvar;

View File

@ -1,4 +1,4 @@
let scope TestBool (foo: bool) (bar: integer) =
let scope TestBool (foo: bool|input|output) (bar: integer|input|output) =
let bar : integer =
reentrant or by default
⟨⟨true ⊢ ⟨⟨true ⊢ 1⟩ | false ⊢ ∅ ⟩⟩ |