Allow access to intermediate variable states

Through the syntax `var_name state state_name`.

Addresses #567, but
- requires documentation
- explicitely accessing states of the variable being defined is not allowed at
  the moment (warning proposed in #567 requires a whole-expression check, which
  is better done some place else entirely)
This commit is contained in:
Louis Gesbert 2024-02-12 18:15:48 +01:00
parent 36866a919b
commit bf0ef0b1f5
6 changed files with 350 additions and 278 deletions

View File

@ -360,14 +360,17 @@ let rec translate_expr
correct calendar day")
in
Expr.elit lit emark
| Ident ([], (x, pos)) -> (
| Ident ([], (x, pos), state) -> (
(* first we check whether this is a local var, then we resort to scope-wide
variables, then global variables *)
match Ident.Map.find_opt x local_vars with
| Some uid ->
match Ident.Map.find_opt x local_vars, state with
| Some uid, None ->
Expr.make_var uid emark
(* the whole box thing is to accomodate for this case *)
| None -> (
| Some uid, Some state ->
Message.raise_spanned_error (Mark.get state)
"%a is a local variable, it has no states" Print.var uid
| None, state -> (
match Ident.Map.find_opt x scope_vars with
| Some (ScopeVar uid) ->
(* If the referenced variable has states, then here are the rules to
@ -376,36 +379,55 @@ let rec translate_expr
the previous state in the chain. *)
let x_sig = ScopeVar.Map.find uid ctxt.var_typs in
let x_state =
match x_sig.var_sig_states_list with
| [] -> None
| states -> (
match inside_definition_of with
| Some (Var (x'_uid, sx'), _) when ScopeVar.compare uid x'_uid = 0
-> (
match sx' with
| None ->
failwith
"inconsistent state: inside a definition of a variable with \
no state but variable has states"
| Some inside_def_state ->
if StateName.compare inside_def_state (List.hd states) = 0 then
Message.raise_spanned_error pos
"It is impossible to refer to the variable you are \
defining when defining its first state."
else
(* Tricky: we have to retrieve in the list the previous state
with respect to the state that we are defining. *)
let rec find_prev_state = function
| [] -> None
| st0 :: st1 :: _ when StateName.equal inside_def_state st1
->
Some st0
| _ :: states -> find_prev_state states
in
find_prev_state states)
| _ ->
(* we take the last state in the chain *)
Some (List.hd (List.rev states)))
match state, x_sig.var_sig_states_list, inside_definition_of with
| None, [], _ -> None
| 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'), _)
when ScopeVar.equal uid x'_uid -> (
if st <> None then
(* TODO *)
Message.raise_spanned_error
(Mark.get (Option.get st))
"Referring to a previous state of the variable being defined \
is not supported at the moment.";
match sx' with
| None ->
failwith
"inconsistent state: inside a definition of a variable with no \
state but variable has states"
| Some inside_def_state ->
if StateName.compare inside_def_state (List.hd states) = 0 then
Message.raise_spanned_error pos
"It is impossible to refer to the variable you are defining \
when defining its first state."
else
(* Tricky: we have to retrieve in the list the previous state
with respect to the state that we are defining. *)
let rec find_prev_state = function
| [] -> None
| st0 :: st1 :: _ when StateName.equal inside_def_state st1 ->
Some st0
| _ :: states -> find_prev_state states
in
find_prev_state states)
| Some st, states, _ -> (
match
Ident.Map.find_opt (Mark.remove st) x_sig.var_sig_states_idmap
with
| None ->
Message.raise_multispanned_error
~suggestion:(List.map StateName.to_string states)
[
None, Mark.get st;
Some "Variable defined here", Mark.get (ScopeVar.get_info uid);
]
"Reference to unknown variable state"
| some -> some)
| _, states, _ ->
(* we take the last state in the chain *)
Some (List.hd (List.rev states))
in
Expr.elocation
(DesugaredScopeVar { name = uid, pos; state = x_state })
@ -416,13 +438,21 @@ let rec translate_expr
| None -> (
match Ident.Map.find_opt x ctxt.local.topdefs with
| Some v ->
if state <> None then
Message.raise_spanned_error pos
"Access to intermediate states is only allowed for variables of \
the current scope";
Expr.elocation
(ToplevelVar { name = v, Mark.get (TopdefName.get_info v) })
emark
| None ->
Name_resolution.raise_unknown_identifier
"for a local, scope-wide or global variable" (x, pos))))
| Ident (path, name) -> (
| Ident (_ :: _, (_, pos), Some _) ->
Message.raise_spanned_error pos
"Access to intermediate states is only allowed for variables of the \
current scope"
| Ident (path, name, None) -> (
let ctxt = Name_resolution.module_ctx ctxt path in
match Ident.Map.find_opt (Mark.remove name) ctxt.local.topdefs with
| Some v ->
@ -433,7 +463,7 @@ let rec translate_expr
Name_resolution.raise_unknown_identifier "for an external variable" name)
| Dotted (e, ((path, x), _ppos)) -> (
match path, Mark.remove e with
| [], Ident ([], (y, _))
| [], 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 *)

View File

@ -189,7 +189,8 @@ and naked_expression =
(path * uident Mark.pos) Mark.pos * (lident Mark.pos * expression) list
| ArrayLit of expression list
| Tuple of expression list
| Ident of path * lident Mark.pos
| Ident of path * lident Mark.pos * lident Mark.pos option
(* path, ident, state *)
| Dotted of expression * (path * lident Mark.pos) Mark.pos
(** Dotted is for both struct field projection and sub-scope variables *)

File diff suppressed because it is too large Load Diff

View File

@ -164,14 +164,21 @@ let mbinder ==
let expression :=
| e = addpos(naked_expression) ; <>
let state_qualifier ==
| STATE ; state = addpos(LIDENT); <>
let naked_expression ==
| id = addpos(LIDENT) ; {
match Localisation.lex_builtin (Mark.remove id) with
| Some b -> Builtin b
| None -> Ident ([], id)
| id = addpos(LIDENT) ; state = option(state_qualifier) ; {
match Localisation.lex_builtin (Mark.remove id), state with
| Some b, None -> Builtin b
| Some _, Some _ ->
Message.raise_spanned_error
(Pos.from_lpos $loc(id))
"Invalid use of built-in @{<bold>%s@}" (Mark.remove id)
| None, state -> Ident ([], id, state)
}
| uid = uident ; DOT ; qlid = qlident ; {
let path, lid = qlid in Ident (uid :: path, lid)
let path, lid = qlid in Ident (uid :: path, lid, None)
}
| l = literal ; {
Literal l

View File

@ -29,10 +29,6 @@ $ catala Interpret -s A
[RESULT] foo = 3
```
```catala-test-inline
$ catala Typecheck
[RESULT] Typechecking successful!
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid-exceptions --optimize
[RESULT] Computation successful! Results:

View File

@ -0,0 +1,38 @@
# Accesses to intermediate variable states
```catala
declaration scope A:
output foo content integer
state s1
state s2
state s3
state s4
output bar content integer
scope A:
definition foo state s1 equals 1
definition foo state s2 equals foo + 1
definition foo state s3 equals foo + 1
definition foo state s4 equals bar + 1
definition bar equals foo state s3 + foo state s2
```
```catala-test-inline
$ catala interpret -s A
[RESULT] Computation successful! Results:
[RESULT] bar = 5
[RESULT] foo = 6
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid-exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] bar = 5
[RESULT] foo = 6
```