Output scopes and subscope variable rework done

This commit is contained in:
Louis Gesbert 2024-03-29 18:39:20 +01:00
parent 852bebd357
commit cde9a66295
12 changed files with 206 additions and 147 deletions

View File

@ -53,6 +53,7 @@ module Make (X : Info) (S : Style) () : Id with type info = X.info = struct
let format ppf t =
Format.pp_open_stag ppf (Ocolor_format.Ocolor_style_tag S.style);
X.format ppf t.info;
(* Format.pp_print_int ppf t.id; (* uncomment for precise uid debug *) *)
Format.pp_close_stag ppf ()
end

View File

@ -31,6 +31,15 @@ module ScopeDef = struct
type t = ScopeVar.t Mark.pos * kind
let equal_kind k1 k2 = match k1, k2 with
| Var s1, Var s2 -> Option.equal StateName.equal s1 s2
| SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } -> ScopeVar.equal v1 v2
| (Var _ | SubScope _), _ -> false
let equal (v1, k1) (v2, k2) =
ScopeVar.equal (Mark.remove v1) (Mark.remove v2) &&
equal_kind k1 k2
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; _ } ->
@ -45,20 +54,22 @@ module ScopeDef = struct
let get_position (v, _) = Mark.get v
let format ppf (v, k) =
ScopeVar.format ppf (Mark.remove v);
match k with
let format_kind ppf = function
| Var None -> ()
| Var (Some st) -> Format.fprintf ppf ".%a" StateName.format st
| Var (Some st) -> Format.fprintf ppf "@%a" StateName.format st
| SubScope { var_within_origin_scope = v; _ } -> Format.fprintf ppf ".%a" ScopeVar.format v
let format ppf (v, k) =
ScopeVar.format ppf (Mark.remove v);
format_kind ppf k
let hash_kind = function
| Var (None) -> 0
| Var (Some st) -> StateName.hash st
| SubScope { var_within_origin_scope = v; _ } -> ScopeVar.hash 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)
Int.logxor (ScopeVar.hash (Mark.remove v)) (hash_kind k)
end
include Base
@ -238,10 +249,8 @@ type program = {
let rec locations_used e : LocationSet.t =
match e with
| ELocation l, m -> LocationSet.singleton (l, Expr.mark_pos m)
| EAbs { binder; _ }, _ ->
let _, body = Bindlib.unmbind binder in
locations_used body
| ELocation l, m ->
LocationSet.singleton (l, Expr.mark_pos m)
| e ->
Expr.shallow_fold
(fun e -> LocationSet.union (locations_used e))

View File

@ -25,8 +25,14 @@ module ScopeDef : sig
| Var of StateName.t option
| SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
val equal_kind : kind -> kind -> bool
val compare_kind : kind -> kind -> int
val format_kind : Format.formatter -> kind -> unit
val hash_kind : kind -> int
type t = ScopeVar.t Mark.pos * kind
val equal : t -> t -> bool
val compare : t -> t -> int
val get_position : t -> Pos.t
val format : Format.formatter -> t -> unit

View File

@ -35,14 +35,12 @@ open Shared_ast
module Vertex = struct
type t =
| Var of ScopeVar.t * StateName.t option
| SubScope of ScopeVar.t
| Assertion of Ast.AssertionName.t
let hash x =
match x with
| Var (x, None) -> ScopeVar.hash x
| Var (x, Some sx) -> Int.logxor (ScopeVar.hash x) (StateName.hash sx)
| SubScope x -> ScopeVar.hash x
| Assertion a -> Ast.AssertionName.hash a
let compare x y =
@ -51,35 +49,27 @@ module Vertex = struct
match ScopeVar.compare x y with
| 0 -> Option.compare StateName.compare xst yst
| n -> n)
| SubScope x, SubScope y -> ScopeVar.compare x y
| Assertion a, Assertion b -> Ast.AssertionName.compare a b
| Var _, _ -> -1
| _, Var _ -> 1
| SubScope _, Assertion _ -> -1
| Assertion _, SubScope _ -> 1
| SubScope _, _ -> .
| _, SubScope _ -> .
let equal x y =
match x, y with
| Var (x, sx), Var (y, sy) ->
ScopeVar.equal x y && Option.equal StateName.equal sx sy
| SubScope x, SubScope y -> ScopeVar.equal x y
| Assertion a, Assertion b -> Ast.AssertionName.equal a b
| (Var _ | SubScope _ | Assertion _), _ -> false
| (Var _ | Assertion _), _ -> false
let format (fmt : Format.formatter) (x : t) : unit =
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
| SubScope v -> ScopeVar.format fmt v
| Assertion a -> Ast.AssertionName.format fmt a
let info = function
| Var (v, None) -> ScopeVar.get_info v
| Var (_, Some sv) -> StateName.get_info sv
| SubScope v -> ScopeVar.get_info v
| Assertion a -> Ast.AssertionName.get_info a
end
@ -179,7 +169,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
let g =
ScopeVar.Map.fold
(fun (v : ScopeVar.t) _ g ->
ScopeDependencies.add_vertex g (Vertex.SubScope v))
ScopeDependencies.add_vertex g (Vertex.Var (v, None)))
scope.scope_sub_scopes g
in
let g =
@ -191,7 +181,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
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)
| Ast.ScopeDef.SubScope _ -> Vertex.Var (Mark.remove var, None)
in
Ast.ScopeDef.Map.fold
(fun def_key scope_def g ->

View File

@ -36,7 +36,6 @@ open Shared_ast
module Vertex : sig
type t =
| Var of Shared_ast.ScopeVar.t * Shared_ast.StateName.t option
| SubScope of Shared_ast.ScopeVar.t
| Assertion of Ast.AssertionName.t
val format : Format.formatter -> t -> unit

View File

@ -252,7 +252,6 @@ let detect_dead_code (p : program) : unit =
let is_alive (v : Dependency.ScopeDependencies.vertex) =
match v with
| Assertion _ -> true
| SubScope _ -> true
| Var (var, state) ->
let scope_def =
ScopeDef.Map.find ((var, Pos.no_pos), ScopeDef.Var state) scope.scope_defs
@ -261,25 +260,19 @@ let detect_dead_code (p : program) : unit =
(* A variable is initially alive if it is an output*)
in
let is_alive = Reachability.analyze is_alive scope_dependencies in
ScopeVar.Map.iter
(fun var states ->
let emit_unused_warning () =
Message.emit_spanned_warning
(Mark.get (ScopeVar.get_info var))
"This variable is dead code; it does not contribute to computing \
any of scope \"%a\" outputs. Did you forget something?"
ScopeName.format scope_name
in
match states with
| WholeVar ->
if not (is_alive (Var (var, None))) then emit_unused_warning ()
| States states ->
List.iter
(fun state ->
if not (is_alive (Var (var, Some state))) then
emit_unused_warning ())
states)
scope.scope_vars)
let emit_unused_warning vx =
Message.emit_spanned_warning
(Mark.get (Dependency.Vertex.info vx))
"Unused varible: %a does not contribute to computing \
any of scope %a outputs. Did you forget something?"
Dependency.Vertex.format vx
ScopeName.format scope_name
in
Dependency.ScopeDependencies.iter_vertex (fun vx ->
if not (is_alive vx) &&
Dependency.ScopeDependencies.succ scope_dependencies vx = []
then emit_unused_warning vx)
scope_dependencies)
p.program_root.module_scopes
let lint_program (p : program) : unit =

View File

@ -190,31 +190,8 @@ let def_to_exception_graph
exc_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 ((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
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
(* If the variable is tagged as input, then it shall not be redefined. *)
Message.raise_multispanned_error
((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
:: List.map
(fun rule ->
( Some "Incriminated variable definition:",
Mark.get (RuleName.get_info rule) ))
(RuleName.Map.keys var_def))
"It is impossible to give a definition to a scope variable tagged as \
input."
| OnlyInput -> D.ScopeDef.Map.empty
(* we do not provide any definition for an input-only variable *)
| _ ->
D.ScopeDef.Map.singleton
((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 ->
| Desugared.Dependency.Vertex.Var (var, None)
when ScopeVar.Map.mem var scope.scope_sub_scopes ->
(* Before calling the sub_scope, we need to include all the re-definitions
of subscope parameters*)
D.ScopeDef.Map.fold
@ -223,7 +200,7 @@ let rule_to_exception_graph (scope : D.scope) = function
| D.ScopeDef.Var _ -> exc_graphs
| D.ScopeDef.SubScope _
when
not (ScopeVar.equal sub_scope_index (Mark.remove sscope))
not (ScopeVar.equal var (Mark.remove sscope))
||
Mark.remove scope_def.D.scope_def_io.io_input = NoInput
&& RuleName.Map.is_empty scope_def.scope_def_rules
@ -268,6 +245,30 @@ let rule_to_exception_graph (scope : D.scope) = function
D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
scope.scope_defs
D.ScopeDef.Map.empty
| Desugared.Dependency.Vertex.Var (var, state) ->
(let pos = Mark.get (ScopeVar.get_info var) in
let scope_def =
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
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
(* If the variable is tagged as input, then it shall not be redefined. *)
Message.raise_multispanned_error
((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
:: List.map
(fun rule ->
( Some "Incriminated variable definition:",
Mark.get (RuleName.get_info rule) ))
(RuleName.Map.keys var_def))
"It is impossible to give a definition to a scope variable tagged as \
input."
| OnlyInput -> D.ScopeDef.Map.empty
(* we do not provide any definition for an input-only variable *)
| _ ->
D.ScopeDef.Map.singleton
((var, pos), (D.ScopeDef.Var state))
(def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
| Assertion _ -> D.ScopeDef.Map.empty (* no exceptions for assertions *)
let scope_to_exception_graphs (scope : D.scope) :
@ -552,60 +553,57 @@ let translate_rule
ctx
(scope : D.scope)
(exc_graphs :
Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t) = function
| Desugared.Dependency.Vertex.Var (var, state) -> (
if ScopeVar.Map.mem var scope.scope_sub_scopes then []
(* this case is handled below, the correct scopecall expression needs to be inserted after the definition of the subscope input vars *)
else
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 ((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
let var_typ = scope_def.D.scope_def_typ in
let is_cond = scope_def.D.scope_def_is_condition in
match Mark.remove scope_def.D.scope_def_io.io_input with
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
assert false (* error already raised *)
| OnlyInput -> []
(* we do not provide any definition for an input-only variable *)
| _ ->
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
(D.ScopeDef.Map.find scope_def_key exc_graphs)
~is_cond ~is_subscope_var:false
in
let scope_var =
match ScopeVar.Map.find var ctx.scope_var_mapping, state with
| WholeVar v, None -> v
| States states, Some state -> List.assoc state states
| _ -> assert false
in
[
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 subscope_var ->
(match ScopeVar.Map.find_opt var scope.scope_sub_scopes with
| None ->
(let var_def = scope_def.D.scope_def_rules in
let var_params = scope_def.D.scope_def_parameters in
let var_typ = scope_def.D.scope_def_typ in
let is_cond = scope_def.D.scope_def_is_condition in
match Mark.remove scope_def.D.scope_def_io.io_input with
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
assert false (* error already raised *)
| OnlyInput -> []
(* we do not provide any definition for an input-only variable *)
| _ ->
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
(D.ScopeDef.Map.find scope_def_key exc_graphs)
~is_cond ~is_subscope_var:false
in
let scope_var =
match ScopeVar.Map.find var ctx.scope_var_mapping, state with
| WholeVar v, None -> v
| States states, Some state -> List.assoc state states
| _ -> assert false
in
[
Ast.ScopeVarDefinition {
var = scope_var, pos;
typ = var_typ;
io = scope_def.D.scope_def_io;
e = Expr.unbox expr_def;
}
])
| Some subscope ->
(* Before calling the subscope, we need to include all the re-definitions
of subscope parameters *)
let subscope =
ScopeVar.Map.find subscope_var scope.scope_sub_scopes
in
let subscope_params =
D.ScopeDef.Map.fold (fun def_key scope_def acc ->
match def_key with
| _, D.ScopeDef.Var _ -> acc
| (v, _), D.ScopeDef.SubScope _
when
not (ScopeVar.equal subscope_var v)
not (ScopeVar.equal var v)
||
Mark.remove scope_def.D.scope_def_io.io_input = NoInput
&& RuleName.Map.is_empty scope_def.scope_def_rules
@ -645,39 +643,34 @@ let translate_rule
scope.scope_defs ScopeVar.Map.empty
in
let subscope_param_map =
ScopeVar.Map.map (fun (var, pos, _, _) -> Expr.evar var (Untyped {pos}))
ScopeVar.Map.map (fun (_, _, _, expr) -> expr)
subscope_params
in
let pos = Mark.get (ScopeVar.get_info subscope_var) in
(* TODO: see remark above about positions *)
let subscope_call_expr =
Expr.escopecall ~scope:subscope ~args:subscope_param_map (Untyped { pos })
in
let subscope_expr =
ScopeVar.Map.fold (fun _ (var, pos, typ, expr) acc ->
Expr.make_let_in var typ expr acc pos)
subscope_params subscope_call_expr
in
let scope_def =
D.ScopeDef.Map.find ((subscope_var, pos), D.ScopeDef.Var None) scope.scope_defs
in
let subscope_expr = subscope_call_expr in
(* ScopeVar.Map.fold (fun _ (var, pos, typ, expr) acc ->
* Expr.make_let_in var typ expr acc pos)
* subscope_params subscope_call_expr
* 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_var_dcalc =
match ScopeVar.Map.find subscope_var ctx.scope_var_mapping with
match ScopeVar.Map.find var ctx.scope_var_mapping with
| WholeVar v -> v
| _ -> assert false
in
let subscope_def =
Ast.ScopeVarDefinition {
var = subscope_var_dcalc, pos;
typ = TStruct scope_info.out_struct_name, Mark.get (ScopeVar.get_info subscope_var);
typ = TStruct scope_info.out_struct_name, Mark.get (ScopeVar.get_info var);
io = scope_def.D.scope_def_io;
e = Expr.unbox_closed subscope_expr;
}
in
[ subscope_def ]
[ subscope_def ])
| Assertion a_name ->
let assertion_expr =
D.AssertionName.Map.find a_name scope.scope_assertions

View File

@ -537,17 +537,11 @@ let compare_location
(x : a glocation Mark.pos)
(y : a glocation Mark.pos) =
match Mark.remove x, Mark.remove y with
| ( DesugaredScopeVar { name = vx; state = None },
DesugaredScopeVar { name = vy; state = None } )
| ( DesugaredScopeVar { name = vx; state = Some _ },
DesugaredScopeVar { name = vy; state = None } )
| ( DesugaredScopeVar { name = vx; state = None },
DesugaredScopeVar { name = vy; state = Some _ } ) ->
ScopeVar.compare (Mark.remove vx) (Mark.remove vy)
| ( DesugaredScopeVar { name = x, _; state = Some sx },
DesugaredScopeVar { name = y, _; state = Some sy } ) ->
let cmp = ScopeVar.compare x y in
if cmp = 0 then StateName.compare sx sy else cmp
| ( DesugaredScopeVar { name = vx; state = sx },
DesugaredScopeVar { name = vy; state = sy } ) ->
(match Mark.compare ScopeVar.compare vx vy with
| 0 -> Option.compare StateName.compare sx sy
| n -> n)
| ScopelangScopeVar { name = vx, _ }, ScopelangScopeVar { name = vy, _ } ->
ScopeVar.compare vx vy
| ToplevelVar { name = vx, _ }, ToplevelVar { name = vy, _ } ->

View File

@ -586,18 +586,35 @@ and typecheck_expr_top_down :
let candidate_structs =
try A.Ident.Map.find field ctx.ctx_struct_fields
with A.Ident.Map.Not_found _ ->
Message.raise_spanned_error
(Expr.mark_pos context_mark)
"Field @{<yellow>\"%s\"@} does not belong to structure \
@{<yellow>\"%a\"@} (no structure defines it)"
field A.StructName.format name
match
A.ScopeName.Map.choose_opt @@
A.ScopeName.Map.filter
(fun _ { A.out_struct_name; _ } -> A.StructName.equal out_struct_name name)
ctx.ctx_scopes
with
| Some (scope_out, _) ->
Message.raise_multispanned_error_full
[None, Expr.mark_pos context_mark;
Some (fun ppf -> Format.fprintf ppf "Subscope %a is declared here" A.ScopeName.format scope_out),
Mark.get (A.StructName.get_info name)]
"Variable @{<yellow>\"%s\"@} is not a declared output of scope %a."
field A.ScopeName.format scope_out
~suggestion:(List.map A.StructField.to_string (A.StructField.Map.keys str))
| None ->
Message.raise_multispanned_error
[None, Expr.mark_pos context_mark;
Some "Structure definition", Mark.get (A.StructName.get_info name)]
"Field @{<yellow>\"%s\"@} does not belong to structure \
@{<yellow>\"%a\"@}."
field A.StructName.format name
~suggestion:(A.Ident.Map.keys ctx.ctx_struct_fields)
in
try A.StructName.Map.find name candidate_structs
with A.StructName.Map.Not_found _ ->
Message.raise_spanned_error
(Expr.mark_pos context_mark)
"@[<hov>Field @{<yellow>\"%s\"@}@ does not belong to@ structure \
@{<yellow>\"%a\"@},@ but to %a@]"
@{<yellow>\"%a\"@}@ (however, structure %a defines it)@]"
field A.StructName.format name
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf "@ or@ ")

View File

@ -0,0 +1,47 @@
```catala
declaration scope A:
output ao content integer
declaration scope S:
a scope A
output so content integer
scope A:
definition ao equals 99
scope S:
definition so equals
let a equals A { -- ao: 42 } in
a.ao
```
```catala-test-inline
$ catala test-scope S
[RESULT] Computation successful! Results:
[RESULT] so = 99
```
```catala
declaration scope A2:
input output io content integer
output x content integer
declaration scope S2:
a scope A2
b scope A2
output c1 content integer
output c2 content integer
scope A2:
definition x equals 0
scope S2:
definition a.io equals 1
definition b.io equals 2
definition c1 equals a.io
definition c2 equals b.io
```

View File

@ -7,6 +7,7 @@ declaration scope A:
declaration scope B:
output a scope A
output b content integer
scope A:
definition o equals i
@ -14,10 +15,18 @@ scope A:
scope B:
definition a.i equals 99
definition a.io equals 100
definition b equals a.o
```
```catala-test-inline
$ catala test-scope B
[RESULT] Computation successful!
[ERROR]
"a": unknown identifier for a local, scope-wide or global variable
┌─⯈ tests/scope/good/out_sub_scope.catala_en:18.23-18.24:
└──┐
18 │ definition b equals a.o
│ ‾
#return code 123#
```

View File

@ -21,6 +21,7 @@ scope B:
definition a equals 42
definition b equals scopeA.b
definition scopeA.a under condition a > 0 consequence equals scopeAbis.a_base
definition scopeA.a under condition a > 10 consequence equals 0
```