Support for structure updates

Closes #592

A new node is added in `desugared`, and translated into an exploded structure
literal during translation to `scopelang`. The main reason to put it there is
that it needs to be after disambiguation, since that is used to discover the
type of the structure that is being updated.
This commit is contained in:
Louis Gesbert 2024-04-11 18:30:51 +02:00 committed by Denis Merigoux
parent 68b78e7a81
commit a61ae7979f
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
17 changed files with 1656 additions and 1369 deletions

View File

@ -559,6 +559,18 @@ let rec translate_expr
Expr.make_abs (Array.of_list vs) (rec_helper ~local_vars e2) taus pos
in
Expr.eapp ~f ~args:[rec_helper e1] ~tys:[] emark
| StructReplace (e, fields) ->
let fields =
List.fold_left
(fun acc (field_id, field_expr) ->
if Ident.Map.mem (Mark.remove field_id) acc then
Message.error ~pos:(Mark.get field_expr)
"Duplicate redefinition of field@ %a" Ident.format
(Mark.remove field_id);
Ident.Map.add (Mark.remove field_id) (rec_helper field_expr) acc)
Ident.Map.empty fields
in
Expr.edstructamend ~fields ~e:(rec_helper e) ~name_opt:None emark
| StructLit (((path, s_name), _), fields) ->
let ctxt = Name_resolution.module_ctx ctxt path in
let s_uid =

View File

@ -83,7 +83,50 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed =
})
m
| ELocation (ToplevelVar v) -> Expr.elocation (ToplevelVar v) m
| EDStructAccess _ ->
| EDStructAmend { name_opt = Some name; e; fields } ->
let str_fields = StructName.Map.find name ctx.decl_ctx.ctx_structs in
let fields =
Ident.Map.fold
(fun id e ->
match
StructName.Map.find name
(Ident.Map.find id ctx.decl_ctx.ctx_struct_fields)
with
| field -> StructField.Map.add field (translate_expr ctx e)
| exception (Ident.Map.Not_found _ | StructName.Map.Not_found _) ->
Message.error ~pos:(Expr.pos e)
~fmt_pos:
[
( (fun ppf ->
Format.fprintf ppf "Declaration of structure %a"
StructName.format name),
Mark.get (StructName.get_info name) );
]
"Field %a@ does@ not@ belong@ to@ structure@ %a" Ident.format id
StructName.format name)
fields StructField.Map.empty
in
if StructField.Map.cardinal fields = StructField.Map.cardinal str_fields
then
Message.warning ~pos:(Expr.mark_pos m)
"All fields of@ %a@ are@ rewritten@ in@ this@ replacement."
StructName.format name;
let orig_var = Var.make "orig" in
let orig_e = Expr.evar orig_var (Mark.get e) in
let fields =
StructField.Map.mapi
(fun field _ty ->
match StructField.Map.find_opt field fields with
| Some e -> e
| None -> Expr.estructaccess ~name ~field ~e:orig_e m)
str_fields
in
Expr.make_let_in orig_var
(TStruct name, Expr.pos e)
(translate_expr ctx e)
(Expr.estruct ~name ~fields m)
(Expr.mark_pos m)
| EDStructAmend { name_opt = None; _ } | EDStructAccess _ ->
assert false (* This shouldn't appear in desugared after disambiguation *)
| EScopeCall { scope; args } ->
Expr.escopecall ~scope

View File

@ -527,6 +527,12 @@ and ('a, 'b, 'm) base_gexpr =
args : ('a, 'm) gexpr ScopeVar.Map.t;
}
-> ('a, < explicitScopes : yes ; .. >, 'm) base_gexpr
| EDStructAmend : {
name_opt : StructName.t option;
e : ('a, 'm) gexpr;
fields : ('a, 'm) gexpr Ident.Map.t;
}
-> ('a, < syntacticNames : yes ; .. >, 'm) base_gexpr
| EDStructAccess : {
name_opt : StructName.t option;
e : ('a, 'm) gexpr;

View File

@ -56,6 +56,10 @@ module Box = struct
let lift : ('a, 't) boxed_gexpr -> ('a, 't) gexpr B.box =
fun em -> B.box_apply (fun e -> Mark.add (Mark.get em) e) (Mark.remove em)
module LiftIdentMap = Bindlib.Lift (Ident.Map)
let lift_identmap = LiftIdentMap.lift_box
module LiftStruct = Bindlib.Lift (StructField.Map)
let lift_struct = LiftStruct.lift_box
@ -156,6 +160,14 @@ let estruct ~name ~(fields : ('a, 't) boxed_gexpr StructField.Map.t) mark =
(fun fields -> EStruct { name; fields })
(Box.lift_struct (StructField.Map.map Box.lift fields))
let edstructamend ~name_opt ~e ~(fields : ('a, 't) boxed_gexpr Ident.Map.t) mark
=
Mark.add mark
@@ Bindlib.box_apply2
(fun e fields -> EDStructAmend { name_opt; e; fields })
(Box.lift e)
(Box.lift_identmap (Ident.Map.map Box.lift fields))
let edstructaccess ~name_opt ~field ~e =
Box.app1 e @@ fun e -> EDStructAccess { name_opt; field; e }
@ -305,6 +317,9 @@ let map
| EStruct { name; fields } ->
let fields = StructField.Map.map f fields in
estruct ~name ~fields m
| EDStructAmend { name_opt; e; fields } ->
let fields = Ident.Map.map f fields in
edstructamend ~name_opt ~e:(f e) ~fields m
| EDStructAccess { name_opt; field; e } ->
edstructaccess ~name_opt ~field ~e:(f e) m
| EStructAccess { name; field; e } -> estructaccess ~name ~field ~e:(f e) m
@ -345,6 +360,8 @@ let shallow_fold
| EErrorOnEmpty e -> acc |> f e
| ECatch { body; handler; _ } -> acc |> f body |> f handler
| EStruct { fields; _ } -> acc |> StructField.Map.fold (fun _ -> f) fields
| EDStructAmend { e; fields; _ } ->
acc |> f e |> Ident.Map.fold (fun _ -> f) fields
| EDStructAccess { e; _ } -> acc |> f e
| EStructAccess { e; _ } -> acc |> f e
| EMatch { e; cases; _ } ->
@ -434,6 +451,16 @@ let map_gather
(acc, StructField.Map.empty)
in
acc, estruct ~name ~fields m
| EDStructAmend { name_opt; e; fields } ->
let acc, e = f e in
let acc, fields =
Ident.Map.fold
(fun cons e (acc, fields) ->
let acc1, e = f e in
join acc acc1, Ident.Map.add cons e fields)
fields (acc, Ident.Map.empty)
in
acc, edstructamend ~name_opt ~e ~fields m
| EDStructAccess { name_opt; field; e } ->
let acc, e = f e in
acc, edstructaccess ~name_opt ~field ~e m
@ -618,6 +645,11 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| ( EStruct { name = s1; fields = fields1 },
EStruct { name = s2; fields = fields2 } ) ->
StructName.equal s1 s2 && StructField.Map.equal equal fields1 fields2
| ( EDStructAmend { name_opt = s1; e = e1; fields = fields1 },
EDStructAmend { name_opt = s2; e = e2; fields = fields2 } ) ->
Option.equal StructName.equal s1 s2
&& equal e1 e2
&& Ident.Map.equal equal fields1 fields2
| ( EDStructAccess { e = e1; field = f1; name_opt = s1 },
EDStructAccess { e = e2; field = f2; name_opt = s2 } ) ->
Option.equal StructName.equal s1 s2 && Ident.equal f1 f2 && equal e1 e2
@ -641,8 +673,8 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _
| EAbs _ | EApp _ | EAppOp _ | EAssert _ | EDefault _ | EPureDefault _
| EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _
| ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _
| EMatch _ | EScopeCall _ | ECustom _ ),
| ELocation _ | EStruct _ | EDStructAmend _ | EDStructAccess _
| EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ | ECustom _ ),
_ ) ->
false
@ -685,6 +717,11 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
EStruct {name=name2; fields=field_map2 } ->
StructName.compare name1 name2 @@< fun () ->
StructField.Map.compare compare field_map1 field_map2
| EDStructAmend {name_opt=n1; e=e1; fields=field_map1},
EDStructAmend {name_opt=n2; e=e2; fields=field_map2} ->
compare e1 e2 @@< fun () ->
Ident.Map.compare compare field_map1 field_map2 @@< fun () ->
Option.compare StructName.compare n1 n2
| EDStructAccess {e=e1; field=field_name1; name_opt=struct_name1},
EDStructAccess {e=e2; field=field_name2; name_opt=struct_name2} ->
compare e1 e2 @@< fun () ->
@ -748,6 +785,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| EIfThenElse _, _ -> -1 | _, EIfThenElse _ -> 1
| ELocation _, _ -> -1 | _, ELocation _ -> 1
| EStruct _, _ -> -1 | _, EStruct _ -> 1
| EDStructAmend _, _ -> -1 | _, EDStructAmend _ -> 1
| EDStructAccess _, _ -> -1 | _, EDStructAccess _ -> 1
| EStructAccess _, _ -> -1 | _, EStructAccess _ -> 1
| EMatch _, _ -> -1 | _, EMatch _ -> 1
@ -895,6 +933,8 @@ let rec size : type a. (a, 't) gexpr -> int =
| ELocation _ -> 1
| EStruct { fields; _ } ->
StructField.Map.fold (fun _ e acc -> acc + 1 + size e) fields 0
| EDStructAmend { e; fields; _ } ->
1 + size e + Ident.Map.fold (fun _ e acc -> acc + 1 + size e) fields 0
| EDStructAccess { e; _ } -> 1 + size e
| EStructAccess { e; _ } -> 1 + size e
| EMatch { e; cases; _ } ->

View File

@ -132,6 +132,13 @@ val estruct :
'm mark ->
('a any, 'm) boxed_gexpr
val edstructamend :
name_opt:StructName.t option ->
e:('a, 'm) boxed_gexpr ->
fields:('a, 'm) boxed_gexpr Ident.Map.t ->
'm mark ->
((< syntacticNames : yes ; .. > as 'a), 'm) boxed_gexpr
val edstructaccess :
name_opt:StructName.t option ->
field:Ident.t ->

View File

@ -423,6 +423,7 @@ module Precedence = struct
| ETupleAccess _ -> Dot
| ELocation _ -> Contained
| EScopeCall _ -> App
| EDStructAmend _ -> App
| EDStructAccess _ | EStructAccess _ -> Dot
| EAssert _ -> App
| EDefault _ -> Contained
@ -681,6 +682,14 @@ module ExprGen (C : EXPR_PARAM) = struct
| EDStructAccess { e; field; _ } ->
Format.fprintf fmt "@[<hv 2>%a%a@,%a%a%a@]" (lhs exprc) e punctuation
"." punctuation "\"" Ident.format field punctuation "\""
| EDStructAmend { e; fields; _ } ->
Format.fprintf fmt "@[<hv 2>@[<hov>%a %a@ with@]@ %a@;<1 -2>%a@]"
punctuation "{" (lhs exprc) e
(Ident.Map.format_bindings ~pp_sep:Format.pp_print_space
(fun fmt pp_field_name field_expr ->
Format.fprintf fmt "@[<hv 2>%t %a@ %a%a@]" pp_field_name
punctuation "=" (lhs exprc) field_expr punctuation ";"))
fields punctuation "}"
| EStruct { name; fields } ->
if StructField.Map.is_empty fields then (
punctuation fmt "{";
@ -1127,7 +1136,7 @@ module UserFacing = struct
| EApp _ | EAppOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _
| EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _
| EDStructAccess _ | ECustom _ ->
| EDStructAmend _ | EDStructAccess _ | ECustom _ ->
fallback ppf e
let expr :

View File

@ -548,6 +548,25 @@ and typecheck_expr_top_down :
fields
in
Expr.estruct ~name ~fields mark
| A.EDStructAmend { name_opt = _; e; fields } ->
let e = typecheck_expr_top_down ctx env tau e in
let name =
match UnionFind.get (ty e) with
| TStruct name, _ -> name
| TAny _, _ -> failwith "Disambiguation failure"
| _ ->
Message.error ~pos:(Expr.pos e)
"This expression has type %a, where a structure was expected"
(format_typ ctx) (ty e)
in
let fields = A.Ident.Map.map (typecheck_expr_bottom_up ctx env) fields in
(* Note: here we identify the structure name, and type the fields
individually, but without enforcing any consistency constraint between
the two. This is fine because this construction only appears in
Desugared, where it is used for disambiguation. In later passes this is
rewritten into a struct literal, so no need to anticipate name resolution
and duplicate the checks here. *)
Expr.edstructamend ~name_opt:(Some name) ~e ~fields context_mark
| A.EDStructAccess { e = e_struct; name_opt; field } ->
let t_struct =
match name_opt with

View File

@ -187,6 +187,7 @@ and naked_expression =
| EnumInject of (path * uident Mark.pos) Mark.pos * expression option
| StructLit of
(path * uident Mark.pos) Mark.pos * (lident Mark.pos * expression) list
| StructReplace of expression * (lident Mark.pos * expression) list
| ArrayLit of expression list
| Tuple of expression list
| Ident of path * lident Mark.pos * lident Mark.pos option

View File

@ -206,6 +206,9 @@ module R = Re.Pcre
#ifndef MR_LIST_EMPTY
#define MR_LIST_EMPTY MS_LIST_EMPTY
#endif
#ifndef MR_BUT_REPLACE
#define MR_BUT_REPLACE MS_BUT_REPLACE
#endif
#ifndef MR_CARDINAL
#define MR_CARDINAL MS_CARDINAL
#endif
@ -316,6 +319,7 @@ let token_list : (string * token) list =
(MS_MINIMUM, MINIMUM);
(MS_IS, IS);
(MS_LIST_EMPTY, LIST_EMPTY);
(MS_BUT_REPLACE, BUT_REPLACE);
(MS_CARDINAL, CARDINAL);
(MS_YEAR, YEAR);
(MS_MONTH, MONTH);
@ -570,6 +574,9 @@ let rec lex_code (lexbuf : lexbuf) : token =
| MR_LIST_EMPTY ->
L.update_acc lexbuf;
LIST_EMPTY
| MR_BUT_REPLACE ->
L.update_acc lexbuf;
BUT_REPLACE
| MR_CARDINAL ->
L.update_acc lexbuf;
CARDINAL

View File

@ -83,6 +83,8 @@
#define MS_IS "is"
#define MS_LIST_EMPTY "list empty"
#define MR_LIST_EMPTY "list", space_plus, "empty"
#define MS_BUT_REPLACE "but replace"
#define MR_BUT_REPLACE "but", space_plus, "replace"
#define MS_CARDINAL "number"
#define MS_YEAR "year"
#define MS_MONTH "month"

View File

@ -103,6 +103,8 @@
#define MS_IS "est"
#define MS_LIST_EMPTY "liste vide"
#define MR_LIST_EMPTY "liste", space_plus, "vide"
#define MS_BUT_REPLACE "mais en rempla\195\167ant"
#define MR_BUT_REPLACE "mais", space_plus, "en", space_plus, "rempla", 0xE7, "ant"
#define MS_CARDINAL "nombre"
#define MS_YEAR "an"
#define MS_MONTH "mois"

View File

@ -95,6 +95,8 @@
#define MS_IS "jest"
#define MS_LIST_EMPTY "lista pusta"
#define MR_LIST_EMPTY "lista", space_plus, "pusta"
#define MS_BUT_REPLACE "ale zastąpić"
#define MR_BUT_REPLACE "ale", space_plus, "zast", 0x0105, "pi", 0x0107
#define MS_CARDINAL "liczba"
#define MS_YEAR "rok"
#define MS_MONTH "miesiąc"

File diff suppressed because it is too large Load Diff

View File

@ -37,7 +37,7 @@ end>
%nonassoc GREATER GREATER_EQUAL LESSER LESSER_EQUAL EQUAL NOT_EQUAL
%left PLUS MINUS PLUSPLUS
%left MULT DIV
%right apply OF CONTAINS FOR SUCH WITH
%right apply OF CONTAINS FOR SUCH WITH BUT_REPLACE
%right COMMA
%right unop_expr
%right CONTENT
@ -218,6 +218,13 @@ let naked_expression ==
WITH ; c = constructor_binding ; {
TestMatchCase (e, (c, Pos.from_lpos $sloc))
}
| e = expression ;
BUT_REPLACE ;
LBRACE ;
fields = nonempty_list(preceded (ALT, struct_content_field)) ;
RBRACE ; {
StructReplace (e, fields)
}
| e1 = expression ;
CONTAINS ;
e2 = expression ; {

View File

@ -55,6 +55,6 @@
%token BEGIN_METADATA MONEY DECIMAL
%token UNDER_CONDITION CONSEQUENCE LBRACE RBRACE
%token LABEL EXCEPTION LBRACKET RBRACKET SEMICOLON
%token MAXIMUM MINIMUM IS LIST_EMPTY
%token MAXIMUM MINIMUM IS LIST_EMPTY BUT_REPLACE
%%

View File

@ -0,0 +1,36 @@
```catala
declaration structure Str:
data fld1 content integer
data fld2 content money
data fld3 content date
declaration scope S:
internal s0 content Str
output s1 content Str
scope S:
definition s0 equals Str {
-- fld1: 0
-- fld2: $1
-- fld3: |2003-01-01|
}
definition s1 equals s0 but replace { --fld1: 0 -- flx1: 99 }
```
```catala-test-inline
$ catala test-scope S
[ERROR] Field flx1 does not belong to structure Str
┌─⯈ tests/struct/bad/struct_update.catala_en:17.60-17.62:
└──┐
17 │ definition s1 equals s0 but replace { --fld1: 0 -- flx1: 99 }
│ ‾‾
Declaration of structure Str
┌─⯈ tests/struct/bad/struct_update.catala_en:2.23-2.26:
└─┐
2 │ declaration structure Str:
│ ‾‾‾
#return code 123#
```

View File

@ -0,0 +1,47 @@
```catala
declaration structure Str:
data fld1 content integer
data fld2 content money
data fld3 content date
declaration scope S:
internal s0 content Str
output s1 content Str
output s2 content Str
output s3 content Str
output s4 content Str
output s5 content Str
scope S:
definition s0 equals Str {
-- fld1: 0
-- fld2: $1
-- fld3: |2003-01-01|
}
definition s1 equals s0 but replace { -- fld1: 99 }
definition s2 equals s0 but replace { -- fld2: $99 }
definition s3 equals s2 but replace { -- fld1: 99 -- fld3: |2099-01-01| }
definition s4 equals s3 but replace { -- fld1: 100 -- fld2: $100 -- fld3: |2100-01-01| }
definition s5 equals s0
but replace { -- fld1: 99 }
but replace { -- fld2: $99 }
but replace { -- fld1: 100 -- fld3 : |2100-01-01| }
```
```catala-test-inline
$ catala test-scope S
[WARNING] All fields of Str are rewritten in this replacement.
┌─⯈ tests/struct/good/struct_update.catala_en:25.24-25.91:
└──┐
25 │ definition s4 equals s3 but replace { -- fld1: 100 -- fld2: $100 -- fld3: |2100-01-01| }
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
[RESULT] Computation successful! Results:
[RESULT] s1 = Str { -- fld1: 99 -- fld2: $1.00 -- fld3: 2003-01-01 }
[RESULT] s2 = Str { -- fld1: 0 -- fld2: $99.00 -- fld3: 2003-01-01 }
[RESULT] s3 = Str { -- fld1: 99 -- fld2: $99.00 -- fld3: 2099-01-01 }
[RESULT] s4 = Str { -- fld1: 100 -- fld2: $100.00 -- fld3: 2100-01-01 }
[RESULT] s5 = Str { -- fld1: 100 -- fld2: $99.00 -- fld3: 2100-01-01 }
```