CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-20 00:41:05 +03:00
Code Issues Projects Releases Wiki Activity

Array type is beginning to work

Browse Source
This commit is contained in:
Denis Merigoux 2020-12-29 22:26:10 +01:00
parent 53e74bfcf8
commit a37357bb56
48 changed files with 806 additions and 678 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/catala/catala_surface/ast.ml
View File

@ -34,10 +34,7 @@ type primitive_typ =
| Date | Date
| Named of constructor | Named of constructor
type base_typ_data = type base_typ_data = Primitive of primitive_typ | Collection of base_typ_data Pos.marked
| Primitive of primitive_typ
| Collection of base_typ_data Pos.marked
| Optional of base_typ_data Pos.marked
type base_typ = Condition | Data of base_typ_data type base_typ = Condition | Data of base_typ_data
@ -136,6 +133,7 @@ and expression =
| EnumInject of constructor Pos.marked * expression Pos.marked option | EnumInject of constructor Pos.marked * expression Pos.marked option
| EnumProject of expression Pos.marked * constructor Pos.marked | EnumProject of expression Pos.marked * constructor Pos.marked
| StructLit of constructor Pos.marked * (ident Pos.marked * expression Pos.marked) list | StructLit of constructor Pos.marked * (ident Pos.marked * expression Pos.marked) list
| ArrayLit of expression Pos.marked list
| Ident of ident | Ident of ident
| Dotted of expression Pos.marked * ident Pos.marked | Dotted of expression Pos.marked * ident Pos.marked
(** Dotted is for both struct field projection and sub-scope variables *) (** Dotted is for both struct field projection and sub-scope variables *)

53
src/catala/catala_surface/desugaring.ml
View File

@ -336,6 +336,59 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
(fun e1 cases_d -> (Scopelang.Ast.EMatch (e1, Option.get e_uid, cases_d), pos)) (fun e1 cases_d -> (Scopelang.Ast.EMatch (e1, Option.get e_uid, cases_d), pos))
e1 e1
(LiftEnumConstructorMap.lift_box cases_d) (LiftEnumConstructorMap.lift_box cases_d)
| ArrayLit es ->
Bindlib.box_apply
(fun es -> (Scopelang.Ast.EArray es, pos))
(Bindlib.box_list (List.map rec_helper es))
| CollectionOp (op, param, collection, predicate) ->
let ctxt, param = Name_resolution.add_def_local_var ctxt param in
let collection = rec_helper collection in
let init =
match Pos.unmark op with
| Ast.Exists -> Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool false), pos)
| Ast.Forall -> Bindlib.box (Scopelang.Ast.ELit (Dcalc.Ast.LBool true), pos)
| _ ->
Name_resolution.raise_unsupported_feature "operator not supported" (Pos.get_position op)
in
let acc_var = Scopelang.Ast.Var.make ("acc", pos) in
let acc = Scopelang.Ast.make_var (acc_var, pos) in
let f_body =
match Pos.unmark op with
| Ast.Exists ->
Bindlib.box_apply2
(fun predicate acc ->
( Scopelang.Ast.EApp
((Scopelang.Ast.EOp (Dcalc.Ast.Binop Dcalc.Ast.Or), pos), [ acc; predicate ]),
pos ))
(translate_expr scope ctxt predicate)
acc
| Ast.Forall ->
Bindlib.box_apply2
(fun predicate acc ->
( Scopelang.Ast.EApp
((Scopelang.Ast.EOp (Dcalc.Ast.Binop Dcalc.Ast.And), pos), [ acc; predicate ]),
pos ))
(translate_expr scope ctxt predicate)
acc
| _ ->
Name_resolution.raise_unsupported_feature "operator not supported" (Pos.get_position op)
in
let f =
Bindlib.box_apply
(fun binder ->
( Scopelang.Ast.EAbs
( pos,
binder,
[ (Scopelang.Ast.TLit Dcalc.Ast.TBool, pos); (Scopelang.Ast.TAny, pos) ] ),
pos ))
(Bindlib.bind_mvar [| acc_var; param |] f_body)
in
Bindlib.box_apply3
(fun f collection init ->
( Scopelang.Ast.EApp
((Scopelang.Ast.EOp (Dcalc.Ast.Ternop Dcalc.Ast.Fold), pos), [ f; init; collection ]),
pos ))
f collection init
| _ -> | _ ->
Name_resolution.raise_unsupported_feature "desugaring not implemented for this expression" pos Name_resolution.raise_unsupported_feature "desugaring not implemented for this expression" pos

24
src/catala/catala_surface/lexer.ml
View File

@ -53,12 +53,15 @@ let token_list_language_agnostic : (string * token) list =
(")", RPAREN); (")", RPAREN);
("{", LBRACKET); ("{", LBRACKET);
("}", RBRACKET); ("}", RBRACKET);
("{", LSQUARE);
("}", RSQUARE);
("+", PLUS); ("+", PLUS);
("-", MINUS); ("-", MINUS);
("*", MULT); ("*", MULT);
("/", DIV); ("/", DIV);
("|", VERTICAL); ("|", VERTICAL);
(":", COLON); (":", COLON);
(";", SEMICOLON);
("--", ALT); ("--", ALT);
] ]
@ -67,7 +70,7 @@ let token_list_language_agnostic : (string * token) list =
let token_list : (string * token) list = let token_list : (string * token) list =
[ [
("scope", SCOPE); ("scope", SCOPE);
("]", CONSEQUENCE); ("|]", CONSEQUENCE);
("data", DATA); ("data", DATA);
("fun of", DEPENDS); ("fun of", DEPENDS);
("new", DECLARATION); ("new", DECLARATION);
@ -92,13 +95,12 @@ let token_list : (string * token) list =
("equals", DEFINED_AS); ("equals", DEFINED_AS);
("match", MATCH); ("match", MATCH);
("with", WITH); ("with", WITH);
("[", UNDER_CONDITION); ("[|", UNDER_CONDITION);
("if", IF); ("if", IF);
("then", THEN); ("then", THEN);
("else", ELSE); ("else", ELSE);
("content", CONTENT); ("content", CONTENT);
("struct", STRUCT); ("struct", STRUCT);
("option", OPTIONAL);
("assert", ASSERTION); ("assert", ASSERTION);
("varies", VARIES); ("varies", VARIES);
("with parameter", WITH_V); ("with parameter", WITH_V);
@ -222,7 +224,7 @@ let rec lex_code (lexbuf : lexbuf) : token =
| "with" -> | "with" ->
update_acc lexbuf; update_acc lexbuf;
WITH WITH
| "[" -> | "[|" ->
update_acc lexbuf; update_acc lexbuf;
UNDER_CONDITION UNDER_CONDITION
| "if" -> | "if" ->
@ -243,9 +245,6 @@ let rec lex_code (lexbuf : lexbuf) : token =
| "struct" -> | "struct" ->
update_acc lexbuf; update_acc lexbuf;
STRUCT STRUCT
| "option" ->
update_acc lexbuf;
OPTIONAL
| "assert" -> | "assert" ->
update_acc lexbuf; update_acc lexbuf;
ASSERTION ASSERTION
@ -292,7 +291,7 @@ let rec lex_code (lexbuf : lexbuf) : token =
| "not" -> | "not" ->
update_acc lexbuf; update_acc lexbuf;
NOT NOT
| "]" -> | "|]" ->
update_acc lexbuf; update_acc lexbuf;
CONSEQUENCE CONSEQUENCE
| "number" -> | "number" ->
@ -464,12 +463,21 @@ let rec lex_code (lexbuf : lexbuf) : token =
| '}' -> | '}' ->
update_acc lexbuf; update_acc lexbuf;
RBRACKET RBRACKET
| '[' ->
update_acc lexbuf;
LSQUARE
| ']' ->
update_acc lexbuf;
RSQUARE
| '|' -> | '|' ->
update_acc lexbuf; update_acc lexbuf;
VERTICAL VERTICAL
| ':' -> | ':' ->
update_acc lexbuf; update_acc lexbuf;
COLON COLON
| ';' ->
update_acc lexbuf;
SEMICOLON
| "--" -> | "--" ->
update_acc lexbuf; update_acc lexbuf;
ALT ALT

13
src/catala/catala_surface/lexer_en.ml
View File

@ -55,7 +55,6 @@ let token_list_en : (string * token) list =
("else", ELSE); ("else", ELSE);
("content", CONTENT); ("content", CONTENT);
("structure", STRUCT); ("structure", STRUCT);
("optional", OPTIONAL);
("assertion", ASSERTION); ("assertion", ASSERTION);
("varies", VARIES); ("varies", VARIES);
("with", WITH_V); ("with", WITH_V);
@ -197,9 +196,6 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| "structure" -> | "structure" ->
L.update_acc lexbuf; L.update_acc lexbuf;
STRUCT STRUCT
| "optional" ->
L.update_acc lexbuf;
OPTIONAL
| "assertion" -> | "assertion" ->
L.update_acc lexbuf; L.update_acc lexbuf;
ASSERTION ASSERTION
@ -421,12 +417,21 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| '}' -> | '}' ->
L.update_acc lexbuf; L.update_acc lexbuf;
RBRACKET RBRACKET
| '[' ->
L.update_acc lexbuf;
LSQUARE
| ']' ->
L.update_acc lexbuf;
RSQUARE
| '|' -> | '|' ->
L.update_acc lexbuf; L.update_acc lexbuf;
VERTICAL VERTICAL
| ':' -> | ':' ->
L.update_acc lexbuf; L.update_acc lexbuf;
COLON COLON
| ';' ->
L.update_acc lexbuf;
SEMICOLON
| "--" -> | "--" ->
L.update_acc lexbuf; L.update_acc lexbuf;
ALT ALT

13
src/catala/catala_surface/lexer_fr.ml
View File

@ -53,7 +53,6 @@ let token_list_fr : (string * token) list =
("sinon", ELSE); ("sinon", ELSE);
("contenu", CONTENT); ("contenu", CONTENT);
("structure", STRUCT); ("structure", STRUCT);
("optionnel", OPTIONAL);
("assertion", ASSERTION); ("assertion", ASSERTION);
("varie", VARIES); ("varie", VARIES);
("avec", WITH_V); ("avec", WITH_V);
@ -200,9 +199,6 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| "structure" -> | "structure" ->
L.update_acc lexbuf; L.update_acc lexbuf;
STRUCT STRUCT
| "optionnel" ->
L.update_acc lexbuf;
OPTIONAL
| "assertion" -> | "assertion" ->
L.update_acc lexbuf; L.update_acc lexbuf;
ASSERTION ASSERTION
@ -428,12 +424,21 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| '}' -> | '}' ->
L.update_acc lexbuf; L.update_acc lexbuf;
RBRACKET RBRACKET
| '[' ->
L.update_acc lexbuf;
LSQUARE
| ']' ->
L.update_acc lexbuf;
RSQUARE
| '|' -> | '|' ->
L.update_acc lexbuf; L.update_acc lexbuf;
VERTICAL VERTICAL
| ':' -> | ':' ->
L.update_acc lexbuf; L.update_acc lexbuf;
COLON COLON
| ';' ->
L.update_acc lexbuf;
SEMICOLON
| "--" -> | "--" ->
L.update_acc lexbuf; L.update_acc lexbuf;
ALT ALT

8
src/catala/catala_surface/name_resolution.ml
View File

@ -151,12 +151,14 @@ let process_subscope_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
{ ctxt with scopes = Scopelang.Ast.ScopeMap.add scope scope_ctxt ctxt.scopes } { ctxt with scopes = Scopelang.Ast.ScopeMap.add scope scope_ctxt ctxt.scopes }
(** Process a basic type (all types except function types) *) (** Process a basic type (all types except function types) *)
let process_base_typ (ctxt : context) ((typ, typ_pos) : Ast.base_typ Pos.marked) : let rec process_base_typ (ctxt : context) ((typ, typ_pos) : Ast.base_typ Pos.marked) :
Scopelang.Ast.typ Pos.marked = Scopelang.Ast.typ Pos.marked =
match typ with match typ with
| Ast.Condition -> (Scopelang.Ast.TLit TBool, typ_pos) | Ast.Condition -> (Scopelang.Ast.TLit TBool, typ_pos)
| Ast.Data (Ast.Collection _) -> raise_unsupported_feature "collection type" typ_pos | Ast.Data (Ast.Collection t) ->
| Ast.Data (Ast.Optional _) -> raise_unsupported_feature "option type" typ_pos ( Scopelang.Ast.TArray
(Pos.unmark (process_base_typ ctxt (Ast.Data (Pos.unmark t), Pos.get_position t))),
typ_pos )
| Ast.Data (Ast.Primitive prim) -> ( | Ast.Data (Ast.Primitive prim) -> (
match prim with match prim with
| Ast.Integer -> (Scopelang.Ast.TLit TInt, typ_pos) | Ast.Integer -> (Scopelang.Ast.TLit TInt, typ_pos)

555
src/catala/catala_surface/parser.messages
View File

File diff suppressed because it is too large Load Diff

13
src/catala/catala_surface/parser.mly
View File

@ -48,7 +48,7 @@
%token LESSER_DATE GREATER_DATE LESSER_EQUAL_DATE GREATER_EQUAL_DATE %token LESSER_DATE GREATER_DATE LESSER_EQUAL_DATE GREATER_EQUAL_DATE
%token LESSER_DURATION GREATER_DURATION LESSER_EQUAL_DURATION GREATER_EQUAL_DURATION %token LESSER_DURATION GREATER_DURATION LESSER_EQUAL_DURATION GREATER_EQUAL_DURATION
%token EXISTS IN SUCH THAT NOW %token EXISTS IN SUCH THAT NOW
%token DOT AND OR LPAREN RPAREN OPTIONAL EQUAL %token DOT AND OR LPAREN RPAREN EQUAL
%token CARDINAL ASSERTION FIXED BY YEAR MONTH DAY %token CARDINAL ASSERTION FIXED BY YEAR MONTH DAY
%token PLUS MINUS MULT DIV %token PLUS MINUS MULT DIV
%token PLUSDEC MINUSDEC MULTDEC DIVDEC %token PLUSDEC MINUSDEC MULTDEC DIVDEC
@ -62,7 +62,7 @@
%token CONTEXT ENUM ELSE DATE SUM %token CONTEXT ENUM ELSE DATE SUM
%token BEGIN_METADATA END_METADATA MONEY DECIMAL %token BEGIN_METADATA END_METADATA MONEY DECIMAL
%token UNDER_CONDITION CONSEQUENCE LBRACKET RBRACKET %token UNDER_CONDITION CONSEQUENCE LBRACKET RBRACKET
%token LABEL EXCEPTION %token LABEL EXCEPTION LSQUARE RSQUARE SEMICOLON
%type <Ast.source_file_or_master> source_file_or_master %type <Ast.source_file_or_master> source_file_or_master
@ -86,18 +86,12 @@ typ_base:
collection_marked: collection_marked:
| COLLECTION { $sloc } | COLLECTION { $sloc }
optional_marked:
| OPTIONAL { $sloc }
typ: typ:
| t = typ_base { | t = typ_base {
let t, loc = t in let t, loc = t in
(Primitive t, loc) (Primitive t, loc)
} }
| collection_marked t = typ { | collection_marked t = typ {
(Optional t, $sloc)
}
| optional_marked t = typ {
(Collection t, $sloc) (Collection t, $sloc)
} }
@ -150,6 +144,9 @@ primitive_expression:
| e = struct_or_enum_inject { | e = struct_or_enum_inject {
e e
} }
| LSQUARE l = separated_list(SEMICOLON, expression) RSQUARE {
(ArrayLit l, $sloc)
}
num_literal: num_literal:
| d = INT_LITERAL { (Int d, $sloc) } | d = INT_LITERAL { (Int d, $sloc) }

253
src/catala/catala_surface/parser_errors.ml
View File

@ -13,11 +13,11 @@ let message s =
"expected another inclusion of a Catala file, since this file is a master file which can \ "expected another inclusion of a Catala file, since this file is a master file which can \
only contain inclusions of other Catala files\n" only contain inclusions of other Catala files\n"
| 8 -> "expected some text, another heading or a law article\n" | 8 -> "expected some text, another heading or a law article\n"
| 341 -> "expected a heading, an article title or some text\n" | 345 -> "expected a heading, an article title or some text\n"
| 326 -> "expected an article title, another heading or some text\n" | 330 -> "expected an article title, another heading or some text\n"
| 331 -> "expected a code block, a metadata block, more law text or a heading\n" | 335 -> "expected a code block, a metadata block, more law text or a heading\n"
| 337 -> "expected a code block, a metadata block, more law text or a heading\n" | 341 -> "expected a code block, a metadata block, more law text or a heading\n"
| 332 -> "expected a declaration or a scope use\n" | 336 -> "expected a declaration or a scope use\n"
| 22 -> "expected the name of the scope you want to use\n" | 22 -> "expected the name of the scope you want to use\n"
| 24 -> "expected a scope use precondition or a colon\n" | 24 -> "expected a scope use precondition or a colon\n"
| 25 -> "expected an expression which will act as the condition\n" | 25 -> "expected an expression which will act as the condition\n"
@ -27,145 +27,144 @@ let message s =
| 30 -> "expected a \"/\"\n" | 30 -> "expected a \"/\"\n"
| 31 -> "expected the third component of the date literal\n" | 31 -> "expected the third component of the date literal\n"
| 32 -> "expected a delimiter to finish the date literal\n" | 32 -> "expected a delimiter to finish the date literal\n"
| 57 -> "expected an operator to compose the expression on the left with\n" | 58 -> "expected an operator to compose the expression on the left with\n"
| 63 -> "expected an enum constructor to test if the expression on the left\n" | 64 -> "expected an enum constructor to test if the expression on the left\n"
| 62 -> "expected an operator to compose the expression on the left with\n" | 63 -> "expected an operator to compose the expression on the left with\n"
| 118 -> "expected an expression on the right side of the sum or minus operator\n" | 119 -> "expected an expression on the right side of the sum or minus operator\n"
| 146 -> "expected an expression on the right side of the logical operator\n" | 147 -> "expected an expression on the right side of the logical operator\n"
| 65 -> "expected an expression for the argument of this function call\n" | 66 -> "expected an expression for the argument of this function call\n"
| 106 -> "expected an expression on the right side of the comparison operator\n" | 107 -> "expected an expression on the right side of the comparison operator\n"
| 127 -> "expected an expression on the right side of the multiplication or division operator\n" | 128 -> "expected an expression on the right side of the multiplication or division operator\n"
| 120 -> "expected an operator to compose the expression on the left\n" | 121 -> "expected an operator to compose the expression on the left\n"
| 156 -> "expected an expression standing for the set you want to test for membership\n" | 157 -> "expected an expression standing for the set you want to test for membership\n"
| 58 -> "expected an identifier standing for a struct field or a subscope name\n" | 59 -> "expected an identifier standing for a struct field or a subscope name\n"
| 198 -> "expected a colon after the scope use precondition\n" | 205 -> "expected a colon after the scope use precondition\n"
| 60 -> "expected a constructor, to get the payload of this enum case\n" | 61 -> "expected a constructor, to get the payload of this enum case\n"
| 130 -> "expected the \"for\" keyword to spell the aggregation\n" | 131 -> "expected the \"for\" keyword to spell the aggregation\n"
| 131 -> "expected an identifier for the aggregation bound variable\n" | 132 -> "expected an identifier for the aggregation bound variable\n"
| 132 -> "expected the \"in\" keyword\n" | 133 -> "expected the \"in\" keyword\n"
| 133 -> | 134 ->
"expected an expression standing for the set over which to compute the aggregation operation\n" "expected an expression standing for the set over which to compute the aggregation operation\n"
| 135 -> "expected the \"for\" keyword and the expression to compute the aggregate\n" | 136 -> "expected the \"for\" keyword and the expression to compute the aggregate\n"
| 136 -> "expected an expression to compute its aggregation over the set\n" | 137 -> "expected an expression to compute its aggregation over the set\n"
| 140 -> "expected an expression to take the negation of\n" | 141 -> "expected an expression to take the negation of\n"
| 54 -> "expected an expression to take the opposite of\n" | 55 -> "expected an expression to take the opposite of\n"
| 43 -> "expected an expression to match with\n" | 43 -> "expected an expression to match with\n"
| 182 -> "expected a pattern matching case\n" | 189 -> "expected a pattern matching case\n"
| 183 -> "expected the name of the constructor for the enum case in the pattern matching\n" | 190 -> "expected the name of the constructor for the enum case in the pattern matching\n"
| 189 -> | 196 ->
"expected a binding for the constructor payload, or a colon and the matching case expression\n" "expected a binding for the constructor payload, or a colon and the matching case expression\n"
| 190 -> "expected an identifier for this enum case binding\n" | 197 -> "expected an identifier for this enum case binding\n"
| 186 -> "expected a colon and then the expression for this matching case\n" | 193 -> "expected a colon and then the expression for this matching case\n"
| 192 -> "expected a colon or a binding for the enum constructor payload\n" | 199 -> "expected a colon or a binding for the enum constructor payload\n"
| 187 -> "expected an expression for this pattern matching case\n" | 194 -> "expected an expression for this pattern matching case\n"
| 184 -> | 191 ->
"expected another match case or the rest of the expression since the previous match case is \ "expected another match case or the rest of the expression since the previous match case is \
complete\n" complete\n"
| 181 -> "expected the \"with patter\" keyword to complete the pattern matching expression\n" | 188 -> "expected the \"with patter\" keyword to complete the pattern matching expression\n"
| 44 -> "expected an expression inside the parenthesis\n" | 45 -> "expected an expression inside the parenthesis\n"
| 179 -> "unmatched parenthesis that should have been closed by here\n" | 180 -> "unmatched parenthesis that should have been closed by here\n"
| 66 -> "expected a unit for this literal, or a valid operator to complete the expression \n" | 67 -> "expected a unit for this literal, or a valid operator to complete the expression \n"
| 46 -> "expected an expression for the test of the conditional\n" | 47 -> "expected an expression for the test of the conditional\n"
| 175 -> "expected an expression the for the \"then\" branch of the conditiona\n" | 176 -> "expected an expression the for the \"then\" branch of the conditiona\n"
| 176 -> | 177 ->
"expected the \"else\" branch of this conditional expression as the \"then\" branch is \ "expected the \"else\" branch of this conditional expression as the \"then\" branch is \
complete\n" complete\n"
| 177 -> "expected an expression for the \"else\" branch of this conditional construction\n" | 178 -> "expected an expression for the \"else\" branch of this conditional construction\n"
| 174 -> "expected the \"then\" keyword as the conditional expression is complete\n" | 175 -> "expected the \"then\" keyword as the conditional expression is complete\n"
| 48 -> | 49 ->
"expected the \"all\" keyword to mean the \"for all\" construction of the universal test\n" "expected the \"all\" keyword to mean the \"for all\" construction of the universal test\n"
| 160 -> "expected an identifier for the bound variable of the universal test\n" | 161 -> "expected an identifier for the bound variable of the universal test\n"
| 161 -> "expected the \"in\" keyword for the rest of the universal test\n" | 162 -> "expected the \"in\" keyword for the rest of the universal test\n"
| 162 -> "expected the expression designating the set on which to perform the universal test\n" | 163 -> "expected the expression designating the set on which to perform the universal test\n"
| 163 -> "expected the \"we have\" keyword for this universal test\n" | 164 -> "expected the \"we have\" keyword for this universal test\n"
| 159 -> "expected an expression for the universal test\n" | 160 -> "expected an expression for the universal test\n"
| 168 -> "expected an identifier that will designate the existential witness for the test\n" | 169 -> "expected an identifier that will designate the existential witness for the test\n"
| 169 -> "expected the \"in\" keyword to continue this existential test\n" | 170 -> "expected the \"in\" keyword to continue this existential test\n"
| 170 -> "expected an expression that designates the set subject to the existential test\n" | 171 -> "expected an expression that designates the set subject to the existential test\n"
| 171 -> "expected a keyword to form the \"such that\" expression for the existential test\n" | 172 -> "expected a keyword to form the \"such that\" expression for the existential test\n"
| 172 -> "expected a keyword to complete the \"such that\" construction\n" | 173 -> "expected a keyword to complete the \"such that\" construction\n"
| 166 -> "expected an expression for the existential test\n" | 167 -> "expected an expression for the existential test\n"
| 75 -> | 76 ->
"expected a payload for the enum case constructor, or the rest of the expression (with an \ "expected a payload for the enum case constructor, or the rest of the expression (with an \
operator ?)\n" operator ?)\n"
| 76 -> "expected structure fields introduced by --\n" | 77 -> "expected structure fields introduced by --\n"
| 77 -> "expected the name of the structure field\n" | 78 -> "expected the name of the structure field\n"
| 81 -> "expected a colon\n" | 82 -> "expected a colon\n"
| 82 -> "expected the expression for this struct field\n" | 83 -> "expected the expression for this struct field\n"
| 78 -> "expected another structure field or the closing bracket\n" | 79 -> "expected another structure field or the closing bracket\n"
| 79 -> "expected the name of the structure field\n" | 80 -> "expected the name of the structure field\n"
| 150 -> "expected an expression for the content of this enum case\n" | 151 -> "expected an expression for the content of this enum case\n"
| 151 -> | 152 ->
"the expression for the content of the enum case is already well-formed, expected an \ "the expression for the content of the enum case is already well-formed, expected an \
operator to form a bigger expression\n" operator to form a bigger expression\n"
| 53 -> "expected the keyword following cardinal to compute the number of elements in a set\n" | 54 -> "expected the keyword following cardinal to compute the number of elements in a set\n"
| 199 -> "expected a scope use item: a rule, definition or assertion\n" | 206 -> "expected a scope use item: a rule, definition or assertion\n"
| 234 -> "expected the name of the variable subject to the rule\n" | 241 -> "expected the name of the variable subject to the rule\n"
| 212 -> | 219 ->
"expected a condition or a consequence for this rule, or the rest of the variable qualified \ "expected a condition or a consequence for this rule, or the rest of the variable qualified \
name\n" name\n"
| 241 -> "expected a condition or a consequence for this rule\n" | 248 -> "expected a condition or a consequence for this rule\n"
| 236 -> "expected filled or not filled for a rule consequence\n" | 243 -> "expected filled or not filled for a rule consequence\n"
| 242 -> "expected the name of the parameter for this dependent variable \n" | 249 -> "expected the name of the parameter for this dependent variable \n"
| 235 -> "expected the expression of the rule\n" | 242 -> "expected the expression of the rule\n"
| 239 -> "expected the filled keyword the this rule \n" | 246 -> "expected the filled keyword the this rule \n"
| 213 -> "expected a struct field or a sub-scope context item after the dot\n" | 220 -> "expected a struct field or a sub-scope context item after the dot\n"
| 200 -> "expected the name of the label\n" | 207 -> "expected the name of the label\n"
| 230 -> "expected a rule or a definition after the label declaration\n" | 237 -> "expected a rule or a definition after the label declaration\n"
| 231 -> "expected the label to which the exception is referring back\n" | 238 -> "expected the label to which the exception is referring back\n"
| 233 -> "expected a rule or a definition after the exception declaration\n" | 240 -> "expected a rule or a definition after the exception declaration\n"
| 246 -> "expected the name of the variable you want to define\n" | 253 -> "expected the name of the variable you want to define\n"
| 247 -> "expected the defined as keyword to introduce the definition of this variable\n" | 254 -> "expected the defined as keyword to introduce the definition of this variable\n"
| 249 -> "expected an expression for the consequence of this definition under condition\n" | 256 -> "expected an expression for the consequence of this definition under condition\n"
| 248 -> | 255 ->
"expected a expression for defining this function, introduced by the defined as keyword\n" "expected a expression for defining this function, introduced by the defined as keyword\n"
| 250 -> "expected an expression for the definition\n" | 257 -> "expected an expression for the definition\n"
| 202 -> "expected an expression that shoud be asserted during execution\n" | 209 -> "expected an expression that shoud be asserted during execution\n"
| 203 -> "expecting the name of the varying variable\n" | 210 -> "expecting the name of the varying variable\n"
| 206 -> "the variable varies with an expression that was expected here\n" | 213 -> "the variable varies with an expression that was expected here\n"
| 207 -> "expected an indication about the variation sense of the variable, or a new scope item\n" | 214 -> "expected an indication about the variation sense of the variable, or a new scope item\n"
| 205 -> "expected an indication about what this variable varies with\n" | 212 -> "expected an indication about what this variable varies with\n"
| 215 -> "expected an expression for this condition\n" | 222 -> "expected an expression for this condition\n"
| 225 -> "expected a consequence for this definition under condition\n" | 232 -> "expected a consequence for this definition under condition\n"
| 221 -> "expected an expression for this definition under condition\n" | 228 -> "expected an expression for this definition under condition\n"
| 217 -> "expected the name of the variable that should be fixed\n" | 224 -> "expected the name of the variable that should be fixed\n"
| 218 -> "expected the legislative text by which the value of the variable is fixed\n" | 225 -> "expected the legislative text by which the value of the variable is fixed\n"
| 219 -> "expected the legislative text by which the value of the variable is fixed\n" | 226 -> "expected the legislative text by which the value of the variable is fixed\n"
| 228 -> "expected a new scope use item \n" | 235 -> "expected a new scope use item \n"
| 257 -> "expected the kind of the declaration (struct, scope or enum)\n" | 264 -> "expected the kind of the declaration (struct, scope or enum)\n"
| 258 -> "expected the struct name\n" | 265 -> "expected the struct name\n"
| 259 -> "expected a colon\n" | 266 -> "expected a colon\n"
| 260 -> "expected struct data or condition\n" | 267 -> "expected struct data or condition\n"
| 261 -> "expected the name of this struct data \n" | 268 -> "expected the name of this struct data \n"
| 262 -> "expected the type of this struct data, introduced by the content keyword\n" | 269 -> "expected the type of this struct data, introduced by the content keyword\n"
| 263 -> "expected the type of this struct data\n" | 270 -> "expected the type of this struct data\n"
| 288 -> "expected the name of this struct condition\n" | 292 -> "expected the name of this struct condition\n"
| 281 -> "expected a new struct data, or another declaration or scope use\n" | 285 -> "expected a new struct data, or another declaration or scope use\n"
| 282 -> "expected the type of the parameter of this struct data function\n" | 286 -> "expected the type of the parameter of this struct data function\n"
| 286 -> "expected a new struct data, or another declaration or scope use\n" | 290 -> "expected a new struct data, or another declaration or scope use\n"
| 275 -> "expected a new struct data, or another declaration or scope use\n" | 282 -> "expected a new struct data, or another declaration or scope use\n"
| 278 -> "expected a new struct data, or another declaration or scope use\n" | 295 -> "expected the name of the scope you are declaring\n"
| 291 -> "expected the name of the scope you are declaring\n" | 296 -> "expected a colon followed by the list of context items of this scope\n"
| 292 -> "expected a colon followed by the list of context items of this scope\n" | 297 -> "expected a context item introduced by \"context\"\n"
| 293 -> "expected a context item introduced by \"context\"\n" | 298 -> "expected the name of this new context item\n"
| 294 -> "expected the name of this new context item\n" | 299 -> "expected the kind of this context item: is it a condition, a sub-scope or a data?\n"
| 295 -> "expected the kind of this context item: is it a condition, a sub-scope or a data?\n" | 300 -> "expected the name of the subscope for this context item\n"
| 296 -> "expected the name of the subscope for this context item\n" | 307 -> "expected another scope context item or the end of the scope declaration\n"
| 303 -> "expected another scope context item or the end of the scope declaration\n" | 302 -> "expected the type of this context item\n"
| 298 -> "expected the type of this context item\n" | 303 -> "expected the next context item or a dependency declaration for this item\n"
| 299 -> "expected the next context item or a dependency declaration for this item\n" | 305 -> "expected the next context item or a dependency declaration for this item\n"
| 301 -> "expected the next context item or a dependency declaration for this item\n" | 310 -> "expected the name of your enum\n"
| 306 -> "expected the name of your enum\n" | 311 -> "expected a colon\n"
| 307 -> "expected a colon\n" | 312 -> "expected an enum case\n"
| 308 -> "expected an enum case\n" | 313 -> "expected the name of an enum case \n"
| 309 -> "expected the name of an enum case \n" | 314 -> "expected a payload for your enum case, or another case or declaration \n"
| 310 -> "expected a payload for your enum case, or another case or declaration \n" | 315 -> "expected a content type\n"
| 311 -> "expected a content type\n" | 320 -> "expected another enum case, or a new declaration or scope use\n"
| 316 -> "expected another enum case, or a new declaration or scope use\n"
| 18 -> "expected a declaration or a scope use\n" | 18 -> "expected a declaration or a scope use\n"
| 19 -> "expected some text or the beginning of a code section\n" | 19 -> "expected some text or the beginning of a code section\n"
| 20 -> "expected a declaration or a scope use\n" | 20 -> "expected a declaration or a scope use\n"
| 21 -> "should not happen\n" | 21 -> "should not happen\n"
| 322 -> "expected a metadata-closing tag\n" | 326 -> "expected a metadata-closing tag\n"
| 323 -> "expected a metadata-closing tag\n" | 327 -> "expected a metadata-closing tag\n"
| _ -> raise Not_found | _ -> raise Not_found

1
src/catala/default_calculus/ast.ml
View File

@ -27,6 +27,7 @@ type typ =
| TEnum of typ Pos.marked list | TEnum of typ Pos.marked list
| TArrow of typ Pos.marked * typ Pos.marked | TArrow of typ Pos.marked * typ Pos.marked
| TArray of typ Pos.marked | TArray of typ Pos.marked
| TAny
type date = ODate.Unix.t type date = ODate.Unix.t

60
src/catala/default_calculus/interpreter.ml
View File

@ -34,13 +34,22 @@ let empty_thunked_term : Ast.expr Pos.marked =
[ (Ast.TLit Ast.TUnit, Pos.no_pos) ] [ (Ast.TLit Ast.TUnit, Pos.no_pos) ]
Pos.no_pos) Pos.no_pos)
let rec type_eq (t1 : A.typ Pos.marked) (t2 : A.typ Pos.marked) : bool =
match (Pos.unmark t1, Pos.unmark t2) with
| A.TLit tl1, A.TLit tl2 -> tl1 = tl2
| A.TTuple ts1, A.TTuple ts2 | A.TEnum ts1, A.TEnum ts2 -> (
try List.for_all2 type_eq ts1 ts2 with Invalid_argument _ -> false )
| A.TArray t1, A.TArray t2 -> type_eq t1 t2
| A.TArrow (t11, t12), A.TArrow (t21, t22) -> type_eq t11 t12 && type_eq t21 t22
| _, _ -> false
(** {1 Evaluation} *) (** {1 Evaluation} *)
let rec evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked list) : let rec evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked list) :
A.expr Pos.marked = A.expr Pos.marked =
Pos.same_pos_as Pos.same_pos_as
( match (Pos.unmark op, List.map Pos.unmark args) with ( match (Pos.unmark op, List.map Pos.unmark args) with
| A.Ternop A.Fold, [ _; _; EArray es ] -> | A.Ternop A.Fold, [ _f; _init; EArray es ] ->
Pos.unmark Pos.unmark
(List.fold_left (List.fold_left
(fun acc e' -> (fun acc e' ->
@ -133,15 +142,46 @@ let rec evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked
| A.Binop A.Eq, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 = i2)) | A.Binop A.Eq, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 = i2))
| A.Binop A.Eq, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 = i2)) | A.Binop A.Eq, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 = i2))
| A.Binop A.Eq, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 = b2)) | A.Binop A.Eq, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 = b2))
| A.Binop A.Eq, [ _; _ ] -> A.ELit (LBool false) (* comparing functions return false *) | A.Binop A.Eq, [ EArray es1; EArray es2 ] ->
| A.Binop A.Neq, [ ELit (LDuration i1); ELit (LDuration i2) ] -> A.ELit (LBool (i1 <> i2)) A.ELit
| A.Binop A.Neq, [ ELit (LDate i1); ELit (LDate i2) ] -> (LBool
A.ELit (LBool (ODate.Unix.compare i1 i2 <> 0)) ( try
| A.Binop A.Neq, [ ELit (LMoney i1); ELit (LMoney i2) ] -> A.ELit (LBool (i1 <> i2)) List.for_all2
| A.Binop A.Neq, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 <> i2)) (fun e1 e2 ->
| A.Binop A.Neq, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 <> i2)) match Pos.unmark (evaluate_operator op [ e1; e2 ]) with
| A.Binop A.Neq, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 <> b2)) | A.ELit (LBool b) -> b
| A.Binop A.Neq, [ _; _ ] -> A.ELit (LBool true) | _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ ETuple es1; ETuple es2 ] ->
A.ELit
(LBool
( try
List.for_all2
(fun (e1, _) (e2, _) ->
match Pos.unmark (evaluate_operator op [ e1; e2 ]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ EInj (e1, i1, _, ts1); EInj (e2, i2, _, ts2) ] ->
A.ELit
(LBool
( try
List.for_all2 type_eq ts1 ts2 && i1 == i2
&&
match Pos.unmark (evaluate_operator op [ e1; e2 ]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ _; _ ] -> A.ELit (LBool false) (* comparing anything else return false *)
| A.Binop A.Neq, [ _; _ ] -> (
match Pos.unmark (evaluate_operator (Pos.same_pos_as (A.Binop A.Eq) op) args) with
| A.ELit (A.LBool b) -> A.ELit (A.LBool (not b))
| _ -> assert false (*should not happen *) )
| A.Binop A.Map, [ _; A.EArray es ] -> | A.Binop A.Map, [ _; A.EArray es ] ->
A.EArray A.EArray
(List.map (List.map

18
src/catala/default_calculus/print.ml
View File

@ -46,6 +46,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked) : unit =
| TArrow (t1, t2) -> | TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2 Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1 | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1
| TAny -> Format.fprintf fmt "any"
let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit = let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
match Pos.unmark l with match Pos.unmark l with
@ -165,7 +166,7 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
| EArray es -> | EArray es ->
Format.fprintf fmt "[%a]" Format.fprintf fmt "[%a]"
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";") ~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt e -> Format.fprintf fmt "@[%a@]" format_expr e)) (fun fmt e -> Format.fprintf fmt "@[%a@]" format_expr e))
es es
| ETupleAccess (e1, n, i) -> ( | ETupleAccess (e1, n, i) -> (
@ -198,15 +199,16 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
Format.fprintf fmt "@[<hov 2>λ@ %a@ →@ %a@]" Format.fprintf fmt "@[<hov 2>λ@ %a@ →@ %a@]"
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ") ~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau) -> Format.fprintf fmt "@[(%a:@ %a)@]" format_var x format_typ tau)) (fun fmt (x, tau) ->
Format.fprintf fmt "@[<hov 2>(%a:@ %a)@]" format_var x format_typ tau))
xs_tau format_expr body xs_tau format_expr body
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) -> | EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 format_binop (op, Pos.no_pos) Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1 format_binop
format_with_parens arg2 (op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop op), _), [ arg1 ]) -> | EApp ((EOp (Unop op), _), [ arg1 ]) ->
Format.fprintf fmt "@[%a@ %a@]" format_unop (op, Pos.no_pos) format_with_parens arg1 Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_unop (op, Pos.no_pos) format_with_parens arg1
| EApp (f, args) -> | EApp (f, args) ->
Format.fprintf fmt "@[%a@ %a@]" format_expr f Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_expr f
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens)
args args
| EIfThenElse (e1, e2, e3) -> | EIfThenElse (e1, e2, e3) ->
@ -217,9 +219,9 @@ let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
| EOp (Unop op) -> Format.fprintf fmt "%a" format_unop (op, Pos.no_pos) | EOp (Unop op) -> Format.fprintf fmt "%a" format_unop (op, Pos.no_pos)
| EDefault (exceptions, just, cons) -> | EDefault (exceptions, just, cons) ->
if List.length exceptions = 0 then if List.length exceptions = 0 then
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons Format.fprintf fmt "@[<hov 2>⟨%a@ ⊢@ %a⟩@]" format_expr just format_expr cons
else else
Format.fprintf fmt "@[<hov 2>⟨%a@ |@ %a ⊢ %a ⟩@]" Format.fprintf fmt "@[<hov 2>⟨%a@ |@ @[<hov 2>%a ⊢ %a@]@ ⟩@]"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
exceptions format_expr just format_expr cons exceptions format_expr just format_expr cons
| EAssert e' -> Format.fprintf fmt "@[<hov 2>assert@ (%a)@]" format_expr e' | EAssert e' -> Format.fprintf fmt "@[<hov 2>assert@ (%a)@]" format_expr e'

297
src/catala/default_calculus/typing.ml
View File

@ -22,6 +22,15 @@ module Cli = Utils.Cli
(** {1 Types and unification} *) (** {1 Types and unification} *)
module Any =
Utils.Uid.Make
(struct
type info = unit
let format_info fmt () = Format.fprintf fmt "any"
end)
()
(** We do not reuse {!type: Dcalc.Ast.typ} because we have to include a new [TAny] variant. Indeed, (** We do not reuse {!type: Dcalc.Ast.typ} because we have to include a new [TAny] variant. Indeed,
error terms can have any type and this has to be captured by the type sytem. *) error terms can have any type and this has to be captured by the type sytem. *)
type typ = type typ =
@ -30,23 +39,32 @@ type typ =
| TTuple of typ Pos.marked UnionFind.elem list | TTuple of typ Pos.marked UnionFind.elem list
| TEnum of typ Pos.marked UnionFind.elem list | TEnum of typ Pos.marked UnionFind.elem list
| TArray of typ Pos.marked UnionFind.elem | TArray of typ Pos.marked UnionFind.elem
| TAny | TAny of Any.t
let rec format_typ (fmt : Format.formatter) (ty : typ Pos.marked UnionFind.elem) : unit = let typ_needs_parens (t : typ Pos.marked UnionFind.elem) : bool =
let ty_repr = UnionFind.get (UnionFind.find ty) in let t = UnionFind.get (UnionFind.find t) in
match Pos.unmark ty_repr with match Pos.unmark t with TArrow _ | TArray _ -> true | _ -> false
let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked UnionFind.elem) : unit =
let format_typ_with_parens (fmt : Format.formatter) (t : typ Pos.marked UnionFind.elem) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" format_typ t
else Format.fprintf fmt "%a" format_typ t
in
let typ = UnionFind.get (UnionFind.find typ) in
match Pos.unmark typ with
| TLit l -> Format.fprintf fmt "%a" Print.format_tlit l | TLit l -> Format.fprintf fmt "%a" Print.format_tlit l
| TAny -> Format.fprintf fmt "any type"
| TTuple ts -> | TTuple ts ->
Format.fprintf fmt "(%a)" Format.fprintf fmt "(%a)"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt " * ") format_typ) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt " *@ ") format_typ)
ts ts
| TEnum ts -> | TEnum ts ->
Format.fprintf fmt "(%a)" Format.fprintf fmt "(%a)"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt " + ") format_typ) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt " +@ ") format_typ)
ts ts
| TArrow (t1, t2) -> Format.fprintf fmt "%a → %a" format_typ t1 format_typ t2 | TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1 | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1
| TAny d -> Format.fprintf fmt "any[%d]" (Any.hash d)
(** Raises an error if unification cannot be performed *) (** Raises an error if unification cannot be performed *)
let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFind.elem) : unit = let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFind.elem) : unit =
@ -55,21 +73,14 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin
let t2_repr = UnionFind.get (UnionFind.find t2) in let t2_repr = UnionFind.get (UnionFind.find t2) in
match (t1_repr, t2_repr) with match (t1_repr, t2_repr) with
| (TLit tl1, _), (TLit tl2, _) when tl1 = tl2 -> () | (TLit tl1, _), (TLit tl2, _) when tl1 = tl2 -> ()
| (TArrow (t11, t12), t1_pos), (TArrow (t21, t22), t2_pos) -> ( | (TArrow (t11, t12), _), (TArrow (t21, t22), _) ->
try unify t11 t21;
unify t11 t21; unify t12 t22
unify t12 t22
with Errors.StructuredError (msg, err_pos) ->
Errors.raise_multispanned_error msg
( err_pos
@ [
(Some (Format.asprintf "Type %a coming from expression:" format_typ t1), t1_pos);
(Some (Format.asprintf "Type %a coming from expression:" format_typ t2), t2_pos);
] ) )
| (TTuple ts1, _), (TTuple ts2, _) -> List.iter2 unify ts1 ts2 | (TTuple ts1, _), (TTuple ts2, _) -> List.iter2 unify ts1 ts2
| (TEnum ts1, _), (TEnum ts2, _) -> List.iter2 unify ts1 ts2 | (TEnum ts1, _), (TEnum ts2, _) -> List.iter2 unify ts1 ts2
| (TAny, _), (TAny, _) -> ignore (UnionFind.union t1 t2) | (TArray t1', _), (TArray t2', _) -> unify t1' t2'
| (TAny, _), t_repr | t_repr, (TAny, _) -> | (TAny _, _), (TAny _, _) -> ignore (UnionFind.union t1 t2)
| (TAny _, _), t_repr | t_repr, (TAny _, _) ->
let t_union = UnionFind.union t1 t2 in let t_union = UnionFind.union t1 t2 in
ignore (UnionFind.set t_union t_repr) ignore (UnionFind.set t_union t_repr)
| (_, t1_pos), (_, t2_pos) -> | (_, t1_pos), (_, t2_pos) ->
@ -94,12 +105,12 @@ let op_type (op : A.operator Pos.marked) : typ Pos.marked UnionFind.elem =
let mt = UnionFind.make (TLit TMoney, pos) in let mt = UnionFind.make (TLit TMoney, pos) in
let dut = UnionFind.make (TLit TDuration, pos) in let dut = UnionFind.make (TLit TDuration, pos) in
let dat = UnionFind.make (TLit TDate, pos) in let dat = UnionFind.make (TLit TDate, pos) in
let any = UnionFind.make (TAny, pos) in let any = UnionFind.make (TAny (Any.fresh ()), pos) in
let array_any = UnionFind.make (TArray any, pos) in let array_any = UnionFind.make (TArray any, pos) in
let any2 = UnionFind.make (TAny, pos) in let any2 = UnionFind.make (TAny (Any.fresh ()), pos) in
let arr x y = UnionFind.make (TArrow (x, y), pos) in let arr x y = UnionFind.make (TArrow (x, y), pos) in
match Pos.unmark op with match Pos.unmark op with
| A.Ternop A.Fold -> arr (arr any2 (arr any any2)) (arr array_any any2) | A.Ternop A.Fold -> arr (arr any2 (arr any any2)) (arr any2 (arr array_any any2))
| A.Binop (A.And | A.Or) -> arr bt (arr bt bt) | A.Binop (A.And | A.Or) -> arr bt (arr bt bt)
| A.Binop (A.Add KInt | A.Sub KInt | A.Mult KInt | A.Div KInt) -> arr it (arr it it) | A.Binop (A.Add KInt | A.Sub KInt | A.Mult KInt | A.Div KInt) -> arr it (arr it it)
| A.Binop (A.Add KRat | A.Sub KRat | A.Mult KRat | A.Div KRat) -> arr rt (arr rt rt) | A.Binop (A.Add KRat | A.Sub KRat | A.Mult KRat | A.Div KRat) -> arr rt (arr rt rt)
@ -138,6 +149,7 @@ let rec ast_to_typ (ty : A.typ) : typ =
| A.TTuple ts -> TTuple (List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts) | A.TTuple ts -> TTuple (List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts)
| A.TEnum ts -> TEnum (List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts) | A.TEnum ts -> TEnum (List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts)
| A.TArray t -> TArray (UnionFind.make (Pos.map_under_mark ast_to_typ t)) | A.TArray t -> TArray (UnionFind.make (Pos.map_under_mark ast_to_typ t))
| A.TAny -> TAny (Any.fresh ())
let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked = let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked =
Pos.map_under_mark Pos.map_under_mark
@ -147,7 +159,7 @@ let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked =
| TTuple ts -> A.TTuple (List.map typ_to_ast ts) | TTuple ts -> A.TTuple (List.map typ_to_ast ts)
| TEnum ts -> A.TEnum (List.map typ_to_ast ts) | TEnum ts -> A.TEnum (List.map typ_to_ast ts)
| TArrow (t1, t2) -> A.TArrow (typ_to_ast t1, typ_to_ast t2) | TArrow (t1, t2) -> A.TArrow (typ_to_ast t1, typ_to_ast t2)
| TAny -> A.TLit A.TUnit | TAny _ -> A.TAny
| TArray t1 -> A.TArray (typ_to_ast t1)) | TArray t1 -> A.TArray (typ_to_ast t1))
(UnionFind.get (UnionFind.find ty)) (UnionFind.get (UnionFind.find ty))
@ -158,123 +170,130 @@ type env = typ Pos.marked A.VarMap.t
(** Infers the most permissive type from an expression *) (** Infers the most permissive type from an expression *)
let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.marked UnionFind.elem let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.marked UnionFind.elem
= =
match Pos.unmark e with let out =
| EVar v -> ( match Pos.unmark e with
match A.VarMap.find_opt (Pos.unmark v) env with | EVar v -> (
| Some t -> UnionFind.make t match A.VarMap.find_opt (Pos.unmark v) env with
| None -> | Some t -> UnionFind.make t
Errors.raise_spanned_error "Variable not found in the current context" | None ->
(Pos.get_position e) ) Errors.raise_spanned_error "Variable not found in the current context"
| ELit (LBool _) -> UnionFind.make (Pos.same_pos_as (TLit TBool) e) (Pos.get_position e) )
| ELit (LInt _) -> UnionFind.make (Pos.same_pos_as (TLit TInt) e) | ELit (LBool _) -> UnionFind.make (Pos.same_pos_as (TLit TBool) e)
| ELit (LRat _) -> UnionFind.make (Pos.same_pos_as (TLit TRat) e) | ELit (LInt _) -> UnionFind.make (Pos.same_pos_as (TLit TInt) e)
| ELit (LMoney _) -> UnionFind.make (Pos.same_pos_as (TLit TMoney) e) | ELit (LRat _) -> UnionFind.make (Pos.same_pos_as (TLit TRat) e)
| ELit (LDate _) -> UnionFind.make (Pos.same_pos_as (TLit TDate) e) | ELit (LMoney _) -> UnionFind.make (Pos.same_pos_as (TLit TMoney) e)
| ELit (LDuration _) -> UnionFind.make (Pos.same_pos_as (TLit TDuration) e) | ELit (LDate _) -> UnionFind.make (Pos.same_pos_as (TLit TDate) e)
| ELit LUnit -> UnionFind.make (Pos.same_pos_as (TLit TUnit) e) | ELit (LDuration _) -> UnionFind.make (Pos.same_pos_as (TLit TDuration) e)
| ELit LEmptyError -> UnionFind.make (Pos.same_pos_as TAny e) | ELit LUnit -> UnionFind.make (Pos.same_pos_as (TLit TUnit) e)
| ETuple es -> | ELit LEmptyError -> UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e)
let ts = List.map (fun (e, _) -> typecheck_expr_bottom_up env e) es in | ETuple es ->
UnionFind.make (Pos.same_pos_as (TTuple ts) e) let ts = List.map (fun (e, _) -> typecheck_expr_bottom_up env e) es in
| ETupleAccess (e1, n, _) -> ( UnionFind.make (Pos.same_pos_as (TTuple ts) e)
let t1 = typecheck_expr_bottom_up env e1 in | ETupleAccess (e1, n, _) -> (
match Pos.unmark (UnionFind.get (UnionFind.find t1)) with let t1 = typecheck_expr_bottom_up env e1 in
| TTuple ts -> ( match Pos.unmark (UnionFind.get (UnionFind.find t1)) with
| TTuple ts -> (
match List.nth_opt ts n with
| Some t' -> t'
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d"
n (List.length ts))
(Pos.get_position e1) )
| _ ->
Errors.raise_spanned_error
(Format.asprintf "Expected a tuple, got a %a" format_typ t1)
(Pos.get_position e1) )
| EInj (e1, n, _, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =
match List.nth_opt ts n with match List.nth_opt ts n with
| Some t' -> t' | Some ts_n -> ts_n
| None -> | None ->
Errors.raise_spanned_error Errors.raise_spanned_error
(Format.asprintf (Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d" n "Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts)) (List.length ts))
(Pos.get_position e1) ) (Pos.get_position e)
| _ ->
Errors.raise_spanned_error
(Format.asprintf "Expected a tuple, got a %a" format_typ t1)
(Pos.get_position e1) )
| EInj (e1, n, _, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =
match List.nth_opt ts n with
| Some ts_n -> ts_n
| None ->
Errors.raise_spanned_error
(Format.asprintf
"Expression should have a sum type with at least %d cases but only has %d" n
(List.length ts))
(Pos.get_position e)
in
typecheck_expr_top_down env e1 ts_n;
UnionFind.make (Pos.same_pos_as (TEnum ts) e)
| EMatch (e1, es) ->
let enum_cases = List.map (fun (e', _) -> UnionFind.make (Pos.same_pos_as TAny e')) es in
let t_e1 = UnionFind.make (Pos.same_pos_as (TEnum enum_cases) e1) in
typecheck_expr_top_down env e1 t_e1;
let t_ret = UnionFind.make (Pos.same_pos_as TAny e) in
List.iteri
(fun i (es', _) ->
let enum_t = List.nth enum_cases i in
let t_es' = UnionFind.make (Pos.same_pos_as (TArrow (enum_t, t_ret)) es') in
typecheck_expr_top_down env es' t_es')
es;
t_ret
| EAbs (pos_binder, binder, taus) ->
let xs, body = Bindlib.unmbind binder in
if Array.length xs = List.length taus then
let xstaus = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let env =
List.fold_left
(fun env (x, tau) ->
A.VarMap.add x (ast_to_typ (Pos.unmark tau), Pos.get_position tau) env)
env xstaus
in in
List.fold_right typecheck_expr_top_down env e1 ts_n;
(fun t_arg (acc : typ Pos.marked UnionFind.elem) -> UnionFind.make (Pos.same_pos_as (TEnum ts) e)
UnionFind.make | EMatch (e1, es) ->
(TArrow (UnionFind.make (Pos.map_under_mark ast_to_typ t_arg), acc), pos_binder)) let enum_cases =
taus List.map (fun (e', _) -> UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e')) es
(typecheck_expr_bottom_up env body) in
else let t_e1 = UnionFind.make (Pos.same_pos_as (TEnum enum_cases) e1) in
Errors.raise_spanned_error typecheck_expr_top_down env e1 t_e1;
(Format.asprintf "function has %d variables but was supplied %d types" (Array.length xs) let t_ret = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
(List.length taus)) List.iteri
pos_binder (fun i (es', _) ->
| EApp (e1, args) -> let enum_t = List.nth enum_cases i in
let t_args = List.map (typecheck_expr_bottom_up env) args in let t_es' = UnionFind.make (Pos.same_pos_as (TArrow (enum_t, t_ret)) es') in
let t_ret = UnionFind.make (Pos.same_pos_as TAny e) in typecheck_expr_top_down env es' t_es')
let t_app = es;
List.fold_right t_ret
(fun t_arg acc -> UnionFind.make (Pos.same_pos_as (TArrow (t_arg, acc)) e)) | EAbs (pos_binder, binder, taus) ->
t_args t_ret let xs, body = Bindlib.unmbind binder in
in if Array.length xs = List.length taus then
typecheck_expr_top_down env e1 t_app; let xstaus = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
t_ret let env =
| EOp op -> op_type (Pos.same_pos_as op e) List.fold_left
| EDefault (excepts, just, cons) -> (fun env (x, tau) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as (TLit TBool) just)); A.VarMap.add x (ast_to_typ (Pos.unmark tau), Pos.get_position tau) env)
let tcons = typecheck_expr_bottom_up env cons in env xstaus
List.iter (fun except -> typecheck_expr_top_down env except tcons) excepts; in
tcons List.fold_right
| EIfThenElse (cond, et, ef) -> (fun t_arg (acc : typ Pos.marked UnionFind.elem) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as (TLit TBool) cond)); UnionFind.make
let tt = typecheck_expr_bottom_up env et in (TArrow (UnionFind.make (Pos.map_under_mark ast_to_typ t_arg), acc), pos_binder))
typecheck_expr_top_down env ef tt; taus
tt (typecheck_expr_bottom_up env body)
| EAssert e' -> else
typecheck_expr_top_down env e' (UnionFind.make (Pos.same_pos_as (TLit TBool) e')); Errors.raise_spanned_error
UnionFind.make (Pos.same_pos_as (TLit TUnit) e') (Format.asprintf "function has %d variables but was supplied %d types" (Array.length xs)
| EArray es -> (List.length taus))
let cell_type = UnionFind.make (Pos.same_pos_as TAny e) in pos_binder
List.iter | EApp (e1, args) ->
(fun e' -> let t_args = List.map (typecheck_expr_bottom_up env) args in
let t_e' = typecheck_expr_bottom_up env e' in let t_ret = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
unify cell_type t_e') let t_app =
es; List.fold_right
UnionFind.make (Pos.same_pos_as (TArray cell_type) e) (fun t_arg acc -> UnionFind.make (Pos.same_pos_as (TArrow (t_arg, acc)) e))
t_args t_ret
in
typecheck_expr_top_down env e1 t_app;
t_ret
| EOp op -> op_type (Pos.same_pos_as op e)
| EDefault (excepts, just, cons) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as (TLit TBool) just));
let tcons = typecheck_expr_bottom_up env cons in
List.iter (fun except -> typecheck_expr_top_down env except tcons) excepts;
tcons
| EIfThenElse (cond, et, ef) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as (TLit TBool) cond));
let tt = typecheck_expr_bottom_up env et in
typecheck_expr_top_down env ef tt;
tt
| EAssert e' ->
typecheck_expr_top_down env e' (UnionFind.make (Pos.same_pos_as (TLit TBool) e'));
UnionFind.make (Pos.same_pos_as (TLit TUnit) e')
| EArray es ->
let cell_type = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
List.iter
(fun e' ->
let t_e' = typecheck_expr_bottom_up env e' in
unify cell_type t_e')
es;
UnionFind.make (Pos.same_pos_as (TArray cell_type) e)
in
(* Cli.debug_print (Format.asprintf "Found type of %a: %a" Print.format_expr e format_typ out); *)
out
(** Checks whether the expression can be typed with the provided type *) (** Checks whether the expression can be typed with the provided type *)
and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked) and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
(tau : typ Pos.marked UnionFind.elem) : unit = (tau : typ Pos.marked UnionFind.elem) : unit =
(* Cli.debug_print (Format.asprintf "Typechecking %a : %a" Print.format_expr e format_typ tau); *)
match Pos.unmark e with match Pos.unmark e with
| EVar v -> ( | EVar v -> (
match A.VarMap.find_opt (Pos.unmark v) env with match A.VarMap.find_opt (Pos.unmark v) env with
@ -289,12 +308,12 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
| ELit (LDate _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TDate) e)) | ELit (LDate _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TDate) e))
| ELit (LDuration _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TDuration) e)) | ELit (LDuration _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TDuration) e))
| ELit LUnit -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TUnit) e)) | ELit LUnit -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TUnit) e))
| ELit LEmptyError -> unify tau (UnionFind.make (Pos.same_pos_as TAny e)) | ELit LEmptyError -> unify tau (UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e))
| ETuple es -> ( | ETuple es -> (
let tau' = UnionFind.get (UnionFind.find tau) in let tau' = UnionFind.get (UnionFind.find tau) in
match Pos.unmark tau' with match Pos.unmark tau' with
| TTuple ts -> List.iter2 (fun (e, _) t -> typecheck_expr_top_down env e t) es ts | TTuple ts -> List.iter2 (fun (e, _) t -> typecheck_expr_top_down env e t) es ts
| TAny -> | TAny _ ->
unify tau unify tau
(UnionFind.make (UnionFind.make
(Pos.same_pos_as (Pos.same_pos_as
@ -316,7 +335,7 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
"expression should have a tuple type with at least %d elements but only has %d" n "expression should have a tuple type with at least %d elements but only has %d" n
(List.length t1s)) (List.length t1s))
(Pos.get_position e1) ) (Pos.get_position e1) )
| TAny -> | TAny _ ->
(* Include total number of cases in ETupleAccess to continue typechecking at this point *) (* Include total number of cases in ETupleAccess to continue typechecking at this point *)
Errors.raise_spanned_error Errors.raise_spanned_error
"The precise type of this expression cannot be inferred.\n\ "The precise type of this expression cannot be inferred.\n\
@ -341,10 +360,12 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
typecheck_expr_top_down env e1 ts_n; typecheck_expr_top_down env e1 ts_n;
unify (UnionFind.make (Pos.same_pos_as (TEnum ts) e)) tau unify (UnionFind.make (Pos.same_pos_as (TEnum ts) e)) tau
| EMatch (e1, es) -> | EMatch (e1, es) ->
let enum_cases = List.map (fun (e', _) -> UnionFind.make (Pos.same_pos_as TAny e')) es in let enum_cases =
List.map (fun (e', _) -> UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e')) es
in
let t_e1 = UnionFind.make (Pos.same_pos_as (TEnum enum_cases) e1) in let t_e1 = UnionFind.make (Pos.same_pos_as (TEnum enum_cases) e1) in
typecheck_expr_top_down env e1 t_e1; typecheck_expr_top_down env e1 t_e1;
let t_ret = UnionFind.make (Pos.same_pos_as TAny e) in let t_ret = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
List.iteri List.iteri
(fun i (es', _) -> (fun i (es', _) ->
let enum_t = List.nth enum_cases i in let enum_t = List.nth enum_cases i in
@ -401,7 +422,7 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
typecheck_expr_top_down env e' (UnionFind.make (Pos.same_pos_as (TLit TBool) e')); typecheck_expr_top_down env e' (UnionFind.make (Pos.same_pos_as (TLit TBool) e'));
unify tau (UnionFind.make (Pos.same_pos_as (TLit TUnit) e')) unify tau (UnionFind.make (Pos.same_pos_as (TLit TUnit) e'))
| EArray es -> | EArray es ->
let cell_type = UnionFind.make (Pos.same_pos_as TAny e) in let cell_type = UnionFind.make (Pos.same_pos_as (TAny (Any.fresh ())) e) in
List.iter List.iter
(fun e' -> (fun e' ->
let t_e' = typecheck_expr_bottom_up env e' in let t_e' = typecheck_expr_bottom_up env e' in

2
src/catala/scope_language/ast.ml
View File

@ -80,6 +80,8 @@ type typ =
| TStruct of StructName.t | TStruct of StructName.t
| TEnum of EnumName.t | TEnum of EnumName.t
| TArrow of typ Pos.marked * typ Pos.marked | TArrow of typ Pos.marked * typ Pos.marked
| TArray of typ
| TAny
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} library, based on (** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} library, based on
higher-order abstract syntax*) higher-order abstract syntax*)

3
src/catala/scope_language/dependency.ml
View File

@ -149,7 +149,8 @@ let rec get_structs_or_enums_in_type (t : Ast.typ Pos.marked) : TVertexSet.t =
| Ast.TEnum e -> TVertexSet.singleton (TVertex.Enum e) | Ast.TEnum e -> TVertexSet.singleton (TVertex.Enum e)
| Ast.TArrow (t1, t2) -> | Ast.TArrow (t1, t2) ->
TVertexSet.union (get_structs_or_enums_in_type t1) (get_structs_or_enums_in_type t2) TVertexSet.union (get_structs_or_enums_in_type t1) (get_structs_or_enums_in_type t2)
| Ast.TLit _ -> TVertexSet.empty | Ast.TLit _ | Ast.TAny -> TVertexSet.empty
| Ast.TArray t1 -> get_structs_or_enums_in_type (Pos.same_pos_as t1 t)
let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TDependencies.t = let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TDependencies.t =
let g = TDependencies.empty in let g = TDependencies.empty in

2
src/catala/scope_language/print.ml
View File

@ -42,6 +42,8 @@ let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked) : unit =
| TEnum e -> Format.fprintf fmt "%a" Ast.EnumName.format_t e | TEnum e -> Format.fprintf fmt "%a" Ast.EnumName.format_t e
| TArrow (t1, t2) -> | TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2 Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ (Pos.same_pos_as t1 typ)
| TAny -> Format.fprintf fmt "any"
let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit = let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
let format_with_parens (fmt : Format.formatter) (e : expr Pos.marked) = let format_with_parens (fmt : Format.formatter) (e : expr Pos.marked) =

4
src/catala/scope_language/scope_to_dcalc.ml
View File

@ -54,7 +54,9 @@ let rec translate_typ (ctx : ctx) (t : Ast.typ Pos.marked) : Dcalc.Ast.typ Pos.m
Dcalc.Ast.TTuple (List.map (fun (_, t) -> translate_typ ctx t) s_fields) Dcalc.Ast.TTuple (List.map (fun (_, t) -> translate_typ ctx t) s_fields)
| Ast.TEnum e_uid -> | Ast.TEnum e_uid ->
let e_cases = Ast.EnumMap.find e_uid ctx.enums in let e_cases = Ast.EnumMap.find e_uid ctx.enums in
Dcalc.Ast.TEnum (List.map (fun (_, t) -> translate_typ ctx t) e_cases) ) Dcalc.Ast.TEnum (List.map (fun (_, t) -> translate_typ ctx t) e_cases)
| Ast.TArray t1 -> Dcalc.Ast.TArray (translate_typ ctx (Pos.same_pos_as t1 t))
| Ast.TAny -> Dcalc.Ast.TAny )
t t
let merge_defaults (caller : Dcalc.Ast.expr Pos.marked Bindlib.box) let merge_defaults (caller : Dcalc.Ast.expr Pos.marked Bindlib.box)

2
syntax_highlighting/en/ace/mode-catala_en.js
View File

@ -70,7 +70,7 @@ ace.define("ace/mode/catala_en_highlighting_rules", ["require", "exports", "modu
}, },
{ {
"token": "punctuation", "token": "punctuation",
"regex": "(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))" "regex": "(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})"
}, },
{ {
"token": "keyword.operator", "token": "keyword.operator",

2
syntax_highlighting/en/atom/grammars/catala_en.cson
View File

@ -116,7 +116,7 @@
'name' : 'constant.numeric.catala_en' 'name' : 'constant.numeric.catala_en'
} }
{ {
'match' : '(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))' 'match' : '(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})'
'name' : 'punctuation.catala_en' 'name' : 'punctuation.catala_en'
} }
{ {

2
syntax_highlighting/en/catala_en.iro
View File

@ -235,7 +235,7 @@ code : context {
: pattern { : pattern {
regex \= (\-\-|\;|\.|\,|\:|\(|\)) regex \= (\-\-|\;|\.|\,|\:|\(|\)|\[|\]|\{|\})
styles [] = .punctuation; styles [] = .punctuation;
} }

3
syntax_highlighting/en/pygments/catala_en.py
View File

@ -31,7 +31,8 @@ class CatalaEnLexer(RegexLexer):
(u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)), (u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)),
(u'\\b(true|false)\\b', bygroups(Keyword.Constant)), (u'\\b(true|false)\\b', bygroups(Keyword.Constant)),
(u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)), (u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)),
(u'(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))', bygroups(Operator)), (u'(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})', bygroups(
Operator)),
(u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\$|%|year|month|day)', (u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\$|%|year|month|day)',
bygroups(Operator)), bygroups(Operator)),
(u'\\b(integer|boolean|date|money|text|decimal|number|sum|now)\\b', (u'\\b(integer|boolean|date|money|text|decimal|number|sum|now)\\b',

2
syntax_highlighting/en/vscode/syntaxes/catalavs.xml
View File

@ -185,7 +185,7 @@
</dict> </dict>
<dict> <dict>
<key>match</key> <key>match</key>
<string>(\-\-|\;|\.|\,|\:|\(|\))</string> <string>(\-\-|\;|\.|\,|\:|\(|\)|\[|\]|\{|\})</string>
<key>name</key> <key>name</key>
<string>punctuation.catala_en</string> <string>punctuation.catala_en</string>
</dict> </dict>

2
syntax_highlighting/fr/ace/mode-catala_fr.js
View File

@ -70,7 +70,7 @@ ace.define("ace/mode/catala_fr_highlighting_rules", ["require", "exports", "modu
}, },
{ {
"token": "punctuation", "token": "punctuation",
"regex": "(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))" "regex": "(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})"
}, },
{ {
"token": "keyword.operator", "token": "keyword.operator",

2
syntax_highlighting/fr/atom/grammars/catala_fr.cson
View File

@ -116,7 +116,7 @@
'name' : 'constant.numeric.catala_fr' 'name' : 'constant.numeric.catala_fr'
} }
{ {
'match' : '(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))' 'match' : '(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})'
'name' : 'punctuation.catala_fr' 'name' : 'punctuation.catala_fr'
} }
{ {

2
syntax_highlighting/fr/catala_fr.iro
View File

@ -235,7 +235,7 @@ code : context {
: pattern { : pattern {
regex \= (\-\-|\;|\.|\,|\:|\(|\)) regex \= (\-\-|\;|\.|\,|\:|\(|\)|\[|\]|\{|\})
styles [] = .punctuation; styles [] = .punctuation;
} }

3
syntax_highlighting/fr/pygments/catala_fr.py
View File

@ -31,7 +31,8 @@ class CatalaFrLexer(RegexLexer):
(u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)), (u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)),
(u'\\b(vrai|faux)\\b', bygroups(Keyword.Constant)), (u'\\b(vrai|faux)\\b', bygroups(Keyword.Constant)),
(u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)), (u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)),
(u'(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\))', bygroups(Operator)), (u'(\\-\\-|\\;|\\.|\\,|\\:|\\(|\\)|\\[|\\]|\\{|\\})', bygroups(
Operator)),
(u'(\\-\\>|\\+|\\-|\\*|/|\\!|non|ou|et|=|>|<|\u20ac|%|an|mois|jour)', (u'(\\-\\>|\\+|\\-|\\*|/|\\!|non|ou|et|=|>|<|\u20ac|%|an|mois|jour)',
bygroups(Operator)), bygroups(Operator)),
(u'\\b(entier|bool\xe9en|date|argent|texte|d\xe9cimal|d\xe9cret|loi|nombre|somme|date_aujourd_hui)\\b', (u'\\b(entier|bool\xe9en|date|argent|texte|d\xe9cimal|d\xe9cret|loi|nombre|somme|date_aujourd_hui)\\b',

2
syntax_highlighting/fr/vscode/syntaxes/catalavs.xml
View File

@ -185,7 +185,7 @@
</dict> </dict>
<dict> <dict>
<key>match</key> <key>match</key>
<string>(\-\-|\;|\.|\,|\:|\(|\))</string> <string>(\-\-|\;|\.|\,|\:|\(|\)|\[|\]|\{|\})</string>
<key>name</key> <key>name</key>
<string>punctuation.catala_fr</string> <string>punctuation.catala_fr</string>
</dict> </dict>

2
syntax_highlighting/nv/atom/grammars/catala_nv.cson
View File

@ -116,7 +116,7 @@
'name' : 'constant.numeric.catala_nv' 'name' : 'constant.numeric.catala_nv'
} }
{ {
'match' : '(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[|\\])' 'match' : '(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[\\||\\|\\]|\\[|\\]|\\{|\\})'
'name' : 'punctuation.catala_nv' 'name' : 'punctuation.catala_nv'
} }
{ {

2
syntax_highlighting/nv/catala_nv.iro
View File

@ -235,7 +235,7 @@ code : context {
: pattern { : pattern {
regex \= (\-\-|\;|\.|\,|\:=|\:|\(|\)|\[|\]) regex \= (\-\-|\;|\.|\,|\:=|\:|\(|\)|\[\||\|\]|\[|\]|\{|\})
styles [] = .punctuation; styles [] = .punctuation;
} }

2
syntax_highlighting/nv/pygments/catala_nv.py
View File

@ -31,7 +31,7 @@ class CatalaNvLexer(RegexLexer):
(u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)), (u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)),
(u'\\b(true|false)\\b', bygroups(Keyword.Constant)), (u'\\b(true|false)\\b', bygroups(Keyword.Constant)),
(u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)), (u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)),
(u'(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[|\\])', (u'(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[\\||\\|\\]|\\[|\\]|\\{|\\})',
bygroups(Operator)), bygroups(Operator)),
(u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\\$|%|year|month|day)', (u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\\$|%|year|month|day)',
bygroups(Operator)), bygroups(Operator)),

2
syntax_highlighting/nv/vscode/syntaxes/catalavs.xml
View File

@ -185,7 +185,7 @@
</dict> </dict>
<dict> <dict>
<key>match</key> <key>match</key>
<string>(\-\-|\;|\.|\,|\:=|\:|\(|\)|\[|\])</string> <string>(\-\-|\;|\.|\,|\:=|\:|\(|\)|\[\||\|\]|\[|\]|\{|\})</string>
<key>name</key> <key>name</key>
<string>punctuation.catala_nv</string> <string>punctuation.catala_nv</string>
</dict> </dict>

18
tests/test_array/simple.catala Normal file
View File

@ -0,0 +1,18 @@
@Article@
/*
new scope A:
param x content set int
scope A:
def x := [0; 4+5; 8*8]
new scope B:
param a scope A
param y content bool
param z content bool
scope B:
def y := exists m in a.x such that m = 9
def z := for all m in a.x we have m > 0
*/

2
tests/test_array/simple.catala.A.out Normal file
View File

@ -0,0 +1,2 @@
[RESULT] Computation successful! Results:
[RESULT] x = [0;9;64]

3
tests/test_array/simple.catala.B.out Normal file
View File

@ -0,0 +1,3 @@
[RESULT] Computation successful! Results:
[RESULT] y = true
[RESULT] z = false

4
tests/test_bool/test_bool.catala
View File

@ -7,6 +7,6 @@ new scope TestBool :
scope TestBool : scope TestBool :
def bar := 1 def bar := 1
def foo [ bar >= 0 ] := true def foo [| bar >= 0 |] := true
def foo [ bar < 0 ] := false def foo [| bar < 0 |] := false
*/ */

4
tests/test_default/conflict.catala
View File

@ -5,6 +5,6 @@ new scope A:
param x content int param x content int
scope A: scope A:
def x [true] := 1 def x [|true|] := 1
def x [true] := 0 def x [|true|] := 0
*/ */

8
tests/test_default/conflict.catala.A.out
View File

@ -3,11 +3,11 @@
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_default/conflict.catala [ERROR] --> test_default/conflict.catala
[ERROR] | [ERROR] |
[ERROR] 8 | def x [true] := 1 [ERROR] 8 | def x [|true|] := 1
[ERROR] | ^^^^ [ERROR] | ^^^^
[ERROR] [ERROR]
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_default/conflict.catala [ERROR] --> test_default/conflict.catala
[ERROR] | [ERROR] |
[ERROR] 9 | def x [true] := 0 [ERROR] 9 | def x [|true|] := 0
[ERROR] | ^^^^ [ERROR] | ^^^^

6
tests/test_default/empty_with_rules.catala
View File

@ -7,7 +7,7 @@ new scope A:
scope A: scope A:
def y := 1 def y := 1
def x [y = 2] := 1 def x [|y = 2|] := 1
def x [y = 3] := 1 def x [|y = 3|] := 1
def x [y = 4] := 1 def x [|y = 4|] := 1
*/ */

4
tests/test_func/func.catala
View File

@ -11,8 +11,8 @@ new scope R:
param r content int param r content int
scope S: scope S:
def f of x [ (x >= x) ] := x + x def f of x [| (x >= x) |] := x + x
def f of x [ not b ] := x * x def f of x [| not b |] := x * x
def b := false def b := false
def out := f of 5 def out := f of 5

8
tests/test_func/func.catala.S.out
View File

@ -3,11 +3,11 @@
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_func/func.catala [ERROR] --> test_func/func.catala
[ERROR] | [ERROR] |
[ERROR] 14 | def f of x [ (x >= x) ] := x + x [ERROR] 14 | def f of x [| (x >= x) |] := x + x
[ERROR] | ^^^^^^ [ERROR] | ^^^^^^
[ERROR] [ERROR]
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_func/func.catala [ERROR] --> test_func/func.catala
[ERROR] | [ERROR] |
[ERROR] 15 | def f of x [ not b ] := x * x [ERROR] 15 | def f of x [| not b |] := x * x
[ERROR] | ^^^^^ [ERROR] | ^^^^^

24
tests/test_money/no_mingle.catala.A.out
View File

@ -11,27 +11,3 @@
[ERROR] | [ERROR] |
[ERROR] 4 | new scope A: [ERROR] 4 | new scope A:
[ERROR] | ^ [ERROR] | ^
[ERROR]
[ERROR] Type decimal → money coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^
[ERROR]
[ERROR] Type money → any type coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^^^^^
[ERROR]
[ERROR] Type money → decimal → money coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^
[ERROR]
[ERROR] Type money → money → any type coming from expression:
[ERROR] --> test_money/no_mingle.catala
[ERROR] |
[ERROR] 12 | def z := (x *$ y)
[ERROR] | ^^^^^^

8
tests/test_scope/cycle_in_scope.catala
View File

@ -7,9 +7,9 @@ new scope A :
param z content int param z content int
scope A: scope A:
def y [x < 0] := - x def y [|x < 0|] := - x
def y [x >= 0] := x def y [|x >= 0|] := x
def z [y >= 1] := 10 / y def z [|y >= 1|] := 10 / y
def z [y < 1] := y def z [|y < 1|] := y
def x := z def x := z
*/ */

8
tests/test_scope/cycle_in_scope.catala.A.out
View File

@ -21,8 +21,8 @@
[ERROR] Used here in the definition of another cycle variable z: [ERROR] Used here in the definition of another cycle variable z:
[ERROR] --> test_scope/cycle_in_scope.catala [ERROR] --> test_scope/cycle_in_scope.catala
[ERROR] | [ERROR] |
[ERROR] 13 | def z [y < 1] := y [ERROR] 13 | def z [|y < 1|] := y
[ERROR] | ^ [ERROR] | ^
[ERROR] [ERROR]
[ERROR] Cycle variable x, declared: [ERROR] Cycle variable x, declared:
[ERROR] --> test_scope/cycle_in_scope.catala [ERROR] --> test_scope/cycle_in_scope.catala
@ -33,5 +33,5 @@
[ERROR] Used here in the definition of another cycle variable y: [ERROR] Used here in the definition of another cycle variable y:
[ERROR] --> test_scope/cycle_in_scope.catala [ERROR] --> test_scope/cycle_in_scope.catala
[ERROR] | [ERROR] |
[ERROR] 11 | def y [x >= 0] := x [ERROR] 11 | def y [|x >= 0|] := x
[ERROR] | ^ [ERROR] | ^

8
tests/test_scope/scope.catala
View File

@ -8,8 +8,8 @@ new scope A:
scope A: scope A:
def c := false def c := false
def a [ c ] := 42 def a [| c |] := 42
def a [ not c ] := 0 def a [| not c |] := 0
def b [ not c ] := 1337 def b [| not c |] := 1337
def b [ not c ] := 0 def b [| not c |] := 0
*/ */

8
tests/test_scope/scope.catala.A.out
View File

@ -3,11 +3,11 @@
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_scope/scope.catala [ERROR] --> test_scope/scope.catala
[ERROR] | [ERROR] |
[ERROR] 13 | def b [ not c ] := 1337 [ERROR] 13 | def b [| not c |] := 1337
[ERROR] | ^^^^^ [ERROR] | ^^^^^
[ERROR] [ERROR]
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_scope/scope.catala [ERROR] --> test_scope/scope.catala
[ERROR] | [ERROR] |
[ERROR] 14 | def b [ not c ] := 0 [ERROR] 14 | def b [| not c |] := 0
[ERROR] | ^^^^^ [ERROR] | ^^^^^

2
tests/test_scope/sub_scope.catala
View File

@ -20,5 +20,5 @@ scope A:
scope B: scope B:
def a := 42 def a := 42
def b := scopeA.b def b := scopeA.b
def scopeA.a [ a > 0 ] := scopeAbis.a_base def scopeA.a [| a > 0 |] := scopeAbis.a_base
*/ */

6
tests/test_scope/sub_sub_scope.catala
View File

@ -20,9 +20,9 @@ scope A:
def u := true def u := true
scope B: scope B:
def a2.x [ a1.u ] := 1 def a2.x [| a1.u |] := 1
def y [ a2.x = 1 ] := 1 def y [| a2.x = 1 |] := 1
def y [ a2.x + 1 = 2 ] := 1 def y [| a2.x + 1 = 2 |] := 1
scope C: scope C:
def a.x := 2 def a.x := 2

8
tests/test_scope/sub_sub_scope.catala.B.out
View File

@ -3,11 +3,11 @@
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_scope/sub_sub_scope.catala [ERROR] --> test_scope/sub_sub_scope.catala
[ERROR] | [ERROR] |
[ERROR] 24 | def y [ a2.x = 1 ] := 1 [ERROR] 24 | def y [| a2.x = 1 |] := 1
[ERROR] | ^^^^^^^^ [ERROR] | ^^^^^^^^
[ERROR] [ERROR]
[ERROR] This justification is true: [ERROR] This justification is true:
[ERROR] --> test_scope/sub_sub_scope.catala [ERROR] --> test_scope/sub_sub_scope.catala
[ERROR] | [ERROR] |
[ERROR] 25 | def y [ a2.x + 1 = 2 ] := 1 [ERROR] 25 | def y [| a2.x + 1 = 2 |] := 1
[ERROR] | ^^^^^^^^^^^^ [ERROR] | ^^^^^^^^^^^^