Defined operators for dec and money

This commit is contained in:
Denis Merigoux 2020-12-09 14:51:22 +01:00
parent ae05498049
commit be563a24f6
19 changed files with 733 additions and 539 deletions

View File

@ -18,10 +18,11 @@ install-dependencies-ocaml:
menhirLib \
dune dune-build-info \
cmdliner obelisk \
re reason \
re \
obelisk \
unionfind \
bindlib \
zarith \
ocamlgraph
init-submodules:

View File

@ -55,9 +55,23 @@ type enum_decl = {
type match_case_pattern = constructor Pos.marked list * ident Pos.marked option
type binop = And | Or | Add | Sub | Mult | Div | Lt | Lte | Gt | Gte | Eq | Neq
type op_kind = KInt | KDec | KMoney
type unop = Not | Minus
type binop =
| And
| Or
| Add of op_kind
| Sub of op_kind
| Mult of op_kind
| Div of op_kind
| Lt of op_kind
| Lte of op_kind
| Gt of op_kind
| Gte of op_kind
| Eq
| Neq
type unop = Not | Minus of op_kind
type builtin_expression = Cardinal | Now

View File

@ -19,22 +19,26 @@ module Cli = Utils.Cli
(** The optional argument subdef allows to choose between differents uids in case the expression is
a redefinition of a subvariable *)
let translate_op_kind (k : Ast.op_kind) : Dcalc.Ast.op_kind =
match k with KInt -> KInt | KDec -> KRat | KMoney -> KMoney
let translate_binop (op : Ast.binop) : Dcalc.Ast.binop =
match op with
| And -> And
| Or -> Or
| Add -> Add
| Sub -> Sub
| Mult -> Mult
| Div -> Div
| Lt -> Lt
| Lte -> Lte
| Gt -> Gt
| Gte -> Gte
| Add l -> Add (translate_op_kind l)
| Sub l -> Sub (translate_op_kind l)
| Mult l -> Mult (translate_op_kind l)
| Div l -> Div (translate_op_kind l)
| Lt l -> Lt (translate_op_kind l)
| Lte l -> Lte (translate_op_kind l)
| Gt l -> Gt (translate_op_kind l)
| Gte l -> Gte (translate_op_kind l)
| Eq -> Eq
| Neq -> Neq
let translate_unop (op : Ast.unop) : Dcalc.Ast.unop = match op with Not -> Not | Minus -> Minus
let translate_unop (op : Ast.unop) : Dcalc.Ast.unop =
match op with Not -> Not | Minus l -> Minus (translate_op_kind l)
module LiftStructFieldMap = Bindlib.Lift (Scopelang.Ast.StructFieldMap)
module LiftEnumConstructorMap = Bindlib.Lift (Scopelang.Ast.EnumConstructorMap)
@ -66,17 +70,9 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t)
match l with
| Number ((Int i, _), _) -> Scopelang.Ast.ELit (Dcalc.Ast.LInt i)
| Number ((Dec (i, f), _), _) ->
let out =
Scopelang.Ast.ELit
(Dcalc.Ast.LRat
Q.(
of_int64 i + (of_int64 f / of_float (10.0 ** ceil (log10 (Int64.to_float f))))))
in
Cli.debug_print
(Format.asprintf "%d.%d -> %a (%s)" (Int64.to_int i) (Int64.to_int f)
Scopelang.Print.format_expr (out, Pos.no_pos)
(Q.to_string (Q.of_float (ceil (log10 (Int64.to_float f))))));
out
Scopelang.Ast.ELit
(Dcalc.Ast.LRat
Q.(of_int64 i + (of_int64 f / of_float (10.0 ** ceil (log10 (Int64.to_float f))))))
| Bool b -> Scopelang.Ast.ELit (Dcalc.Ast.LBool b)
| _ -> Name_resolution.raise_unsupported_feature "literal" pos
in

View File

@ -301,9 +301,54 @@ let rec lex_code (lexbuf : lexbuf) : token =
| "->" ->
update_acc lexbuf;
ARROW
| '.' ->
| "<=", 0x24 ->
update_acc lexbuf;
DOT
LESSER_EQUAL_MONEY
| '<', 0x24 ->
update_acc lexbuf;
LESSER_MONEY
| ">=", 0x24 ->
update_acc lexbuf;
GREATER_EQUAL_MONEY
| '>', 0x24 ->
update_acc lexbuf;
GREATER_MONEY
| '+', 0x24 ->
update_acc lexbuf;
PLUSMONEY
| '-', 0x24 ->
update_acc lexbuf;
MINUSMONEY
| '*', 0x24 ->
update_acc lexbuf;
MULTMONEY
| '/', 0x24 ->
update_acc lexbuf;
DIVMONEY
| "<=." ->
update_acc lexbuf;
LESSER_EQUAL_DEC
| "<." ->
update_acc lexbuf;
LESSER_DEC
| ">=." ->
update_acc lexbuf;
GREATER_EQUAL_DEC
| ">." ->
update_acc lexbuf;
GREATER_DEC
| "+." ->
update_acc lexbuf;
PLUSDEC
| "-." ->
update_acc lexbuf;
MINUSDEC
| "*." ->
update_acc lexbuf;
MULTDEC
| "/." ->
update_acc lexbuf;
DIVDEC
| "<=" ->
update_acc lexbuf;
LESSER_EQUAL
@ -316,12 +361,27 @@ let rec lex_code (lexbuf : lexbuf) : token =
| '>' ->
update_acc lexbuf;
GREATER
| '+' ->
update_acc lexbuf;
PLUS
| '-' ->
update_acc lexbuf;
MINUS
| '*' ->
update_acc lexbuf;
MULT
| '/' ->
update_acc lexbuf;
DIV
| "!=" ->
update_acc lexbuf;
NOT_EQUAL
| '=' ->
update_acc lexbuf;
EQUAL
| '%' ->
update_acc lexbuf;
PERCENT
| '(' ->
update_acc lexbuf;
LPAREN
@ -334,21 +394,6 @@ let rec lex_code (lexbuf : lexbuf) : token =
| '}' ->
update_acc lexbuf;
RBRACKET
| '+' ->
update_acc lexbuf;
PLUS
| '-' ->
update_acc lexbuf;
MINUS
| '*' ->
update_acc lexbuf;
MULT
| '%' ->
update_acc lexbuf;
PERCENT
| '/' ->
update_acc lexbuf;
DIV
| '|' ->
update_acc lexbuf;
VERTICAL
@ -358,6 +403,9 @@ let rec lex_code (lexbuf : lexbuf) : token =
| "--" ->
update_acc lexbuf;
ALT
| '.' ->
update_acc lexbuf;
DOT
| uppercase, Star (uppercase | lowercase | '0' .. '9' | '_' | '\'') ->
(* Name of constructor *)
update_acc lexbuf;

View File

@ -269,9 +269,54 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| "->" ->
L.update_acc lexbuf;
ARROW
| '.' ->
| "<=", 0x24 ->
L.update_acc lexbuf;
DOT
LESSER_EQUAL_MONEY
| '<', 0x24 ->
L.update_acc lexbuf;
LESSER_MONEY
| ">=", 0x24 ->
L.update_acc lexbuf;
GREATER_EQUAL_MONEY
| '>', 0x24 ->
L.update_acc lexbuf;
GREATER_MONEY
| '+', 0x24 ->
L.update_acc lexbuf;
PLUSMONEY
| '-', 0x24 ->
L.update_acc lexbuf;
MINUSMONEY
| '*', 0x24 ->
L.update_acc lexbuf;
MULTMONEY
| '/', 0x24 ->
L.update_acc lexbuf;
DIVMONEY
| "<=." ->
L.update_acc lexbuf;
LESSER_EQUAL_DEC
| "<." ->
L.update_acc lexbuf;
LESSER_DEC
| ">=." ->
L.update_acc lexbuf;
GREATER_EQUAL_DEC
| ">." ->
L.update_acc lexbuf;
GREATER_DEC
| "+." ->
L.update_acc lexbuf;
PLUSDEC
| "-." ->
L.update_acc lexbuf;
MINUSDEC
| "*." ->
L.update_acc lexbuf;
MULTDEC
| "/." ->
L.update_acc lexbuf;
DIVDEC
| "<=" ->
L.update_acc lexbuf;
LESSER_EQUAL
@ -284,12 +329,27 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| '>' ->
L.update_acc lexbuf;
GREATER
| '+' ->
L.update_acc lexbuf;
PLUS
| '-' ->
L.update_acc lexbuf;
MINUS
| '*' ->
L.update_acc lexbuf;
MULT
| '/' ->
L.update_acc lexbuf;
DIV
| "!=" ->
L.update_acc lexbuf;
NOT_EQUAL
| '=' ->
L.update_acc lexbuf;
EQUAL
| '%' ->
L.update_acc lexbuf;
PERCENT
| '(' ->
L.update_acc lexbuf;
LPAREN
@ -302,21 +362,6 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| '}' ->
L.update_acc lexbuf;
RBRACKET
| '+' ->
L.update_acc lexbuf;
PLUS
| '-' ->
L.update_acc lexbuf;
MINUS
| '*' ->
L.update_acc lexbuf;
MULT
| '%' ->
L.update_acc lexbuf;
PERCENT
| '/' ->
L.update_acc lexbuf;
DIV
| '|' ->
L.update_acc lexbuf;
VERTICAL
@ -326,6 +371,9 @@ let rec lex_code_en (lexbuf : lexbuf) : token =
| "--" ->
L.update_acc lexbuf;
ALT
| '.' ->
L.update_acc lexbuf;
DOT
| uppercase, Star (uppercase | lowercase | '0' .. '9' | '_' | '\'') ->
(* Name of constructor *)
L.update_acc lexbuf;

View File

@ -278,9 +278,54 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| "->" ->
L.update_acc lexbuf;
ARROW
| '.' ->
| "<=", 0x20AC ->
L.update_acc lexbuf;
DOT
LESSER_EQUAL_MONEY
| '<', 0x20AC ->
L.update_acc lexbuf;
LESSER_MONEY
| ">=", 0x20AC ->
L.update_acc lexbuf;
GREATER_EQUAL_MONEY
| '>', 0x20AC ->
L.update_acc lexbuf;
GREATER_MONEY
| '+', 0x20AC ->
L.update_acc lexbuf;
PLUSMONEY
| '-', 0x20AC ->
L.update_acc lexbuf;
MINUSMONEY
| '*', 0x20AC ->
L.update_acc lexbuf;
MULTMONEY
| '/', 0x20AC ->
L.update_acc lexbuf;
DIVMONEY
| "<=." ->
L.update_acc lexbuf;
LESSER_EQUAL_DEC
| "<." ->
L.update_acc lexbuf;
LESSER_DEC
| ">=." ->
L.update_acc lexbuf;
GREATER_EQUAL_DEC
| ">." ->
L.update_acc lexbuf;
GREATER_DEC
| "+." ->
L.update_acc lexbuf;
PLUSDEC
| "-." ->
L.update_acc lexbuf;
MINUSDEC
| "*." ->
L.update_acc lexbuf;
MULTDEC
| "/." ->
L.update_acc lexbuf;
DIVDEC
| "<=" ->
L.update_acc lexbuf;
LESSER_EQUAL
@ -293,12 +338,27 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| '>' ->
L.update_acc lexbuf;
GREATER
| '+' ->
L.update_acc lexbuf;
PLUS
| '-' ->
L.update_acc lexbuf;
MINUS
| '*' ->
L.update_acc lexbuf;
MULT
| '/' ->
L.update_acc lexbuf;
DIV
| "!=" ->
L.update_acc lexbuf;
NOT_EQUAL
| '=' ->
L.update_acc lexbuf;
EQUAL
| '%' ->
L.update_acc lexbuf;
PERCENT
| '(' ->
L.update_acc lexbuf;
LPAREN
@ -311,21 +371,6 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| '}' ->
L.update_acc lexbuf;
RBRACKET
| '+' ->
L.update_acc lexbuf;
PLUS
| '-' ->
L.update_acc lexbuf;
MINUS
| '*' ->
L.update_acc lexbuf;
MULT
| '%' ->
L.update_acc lexbuf;
PERCENT
| '/' ->
L.update_acc lexbuf;
DIV
| '|' ->
L.update_acc lexbuf;
VERTICAL
@ -335,6 +380,9 @@ let rec lex_code_fr (lexbuf : lexbuf) : token =
| "--" ->
L.update_acc lexbuf;
ALT
| '.' ->
L.update_acc lexbuf;
DOT
| uppercase, Star (uppercase | lowercase | '0' .. '9' | '_' | '\'') ->
(* Name of constructor *)
L.update_acc lexbuf;

View File

@ -96,15 +96,16 @@ let process_subscope_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
let process_base_typ (ctxt : context) ((typ, typ_pos) : Ast.base_typ Pos.marked) :
Scopelang.Ast.typ Pos.marked =
match typ with
| Ast.Condition -> (Scopelang.Ast.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.Optional _) -> raise_unsupported_feature "option type" typ_pos
| Ast.Data (Ast.Primitive prim) -> (
match prim with
| Ast.Integer -> (Scopelang.Ast.TInt, typ_pos)
| Ast.Decimal -> (Scopelang.Ast.TRat, typ_pos)
| Ast.Money | Ast.Date -> raise_unsupported_feature "value type" typ_pos
| Ast.Boolean -> (Scopelang.Ast.TBool, typ_pos)
| Ast.Integer -> (Scopelang.Ast.TLit TInt, typ_pos)
| Ast.Decimal -> (Scopelang.Ast.TLit TRat, typ_pos)
| Ast.Money -> (Scopelang.Ast.TLit TMoney, typ_pos)
| Ast.Date -> raise_unsupported_feature "date type" typ_pos
| Ast.Boolean -> (Scopelang.Ast.TLit TBool, typ_pos)
| Ast.Text -> raise_unsupported_feature "text type" typ_pos
| Ast.Named ident -> (
match Desugared.Ast.IdentMap.find_opt ident ctxt.struct_idmap with
@ -297,7 +298,7 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
(fun cases ->
let typ =
match cdecl.Ast.enum_decl_case_typ with
| None -> (Scopelang.Ast.TUnit, cdecl_pos)
| None -> (Scopelang.Ast.TLit TUnit, cdecl_pos)
| Some typ -> process_type ctxt typ
in
match cases with

File diff suppressed because it is too large Load Diff

View File

@ -42,11 +42,16 @@
%token COLON ALT DATA VERTICAL
%token OF INTEGER COLLECTION
%token RULE CONDITION DEFINED_AS
%token EXISTS IN SUCH THAT NOW LESSER GREATER
%token LESSER GREATER LESSER_EQUAL GREATER_EQUAL
%token LESSER_DEC GREATER_DEC LESSER_EQUAL_DEC GREATER_EQUAL_DEC
%token LESSER_MONEY GREATER_MONEY LESSER_EQUAL_MONEY GREATER_EQUAL_MONEY
%token EXISTS IN SUCH THAT NOW
%token DOT AND OR LPAREN RPAREN OPTIONAL EQUAL
%token CARDINAL LESSER_EQUAL GREATER_EQUAL
%token ASSERTION FIXED BY YEAR
%token PLUS MINUS MULT DIV MATCH WITH VARIES WITH_V
%token CARDINAL ASSERTION FIXED BY YEAR
%token PLUS MINUS MULT DIV
%token PLUSDEC MINUSDEC MULTDEC DIVDEC
%token PLUSMONEY MINUSMONEY MULTMONEY DIVMONEY
%token MATCH WITH VARIES WITH_V
%token FOR ALL WE_HAVE INCREASING DECREASING
%token NOT BOOLEAN PERCENT ARROW
%token SCOPE FILLED NOT_EQUAL DEFINITION
@ -177,10 +182,18 @@ literal:
| FALSE { (Bool false, $sloc) }
compare_op:
| LESSER { (Lt, $sloc) }
| LESSER_EQUAL { (Lte, $sloc) }
| GREATER { (Gt, $sloc) }
| GREATER_EQUAL { (Gte, $sloc) }
| LESSER { (Lt KInt, $sloc) }
| LESSER_EQUAL { (Lte KInt, $sloc) }
| GREATER { (Gt KInt, $sloc) }
| GREATER_EQUAL { (Gte KInt, $sloc) }
| LESSER_DEC { (Lt KDec, $sloc) }
| LESSER_EQUAL_DEC { (Lte KDec, $sloc) }
| GREATER_DEC { (Gt KDec, $sloc) }
| GREATER_EQUAL_DEC { (Gte KDec, $sloc) }
| LESSER_MONEY { (Lt KMoney, $sloc) }
| LESSER_EQUAL_MONEY { (Lte KMoney, $sloc) }
| GREATER_MONEY { (Gt KMoney, $sloc) }
| GREATER_EQUAL_MONEY { (Gte KMoney, $sloc) }
| EQUAL { (Eq, $sloc) }
| NOT_EQUAL { (Neq, $sloc) }
@ -208,8 +221,12 @@ base_expression:
}
mult_op:
| MULT { (Mult, $sloc) }
| DIV { (Div, $sloc) }
| MULT { (Mult KInt, $sloc) }
| DIV { (Div KInt, $sloc) }
| MULTDEC { (Mult KDec, $sloc) }
| DIVDEC { (Div KDec, $sloc) }
| MULTMONEY { (Mult KMoney, $sloc) }
| DIVMONEY { (Div KMoney, $sloc) }
mult_expression:
| e = base_expression { e }
@ -218,11 +235,17 @@ mult_expression:
}
sum_op:
| PLUS { (Add, $sloc) }
| MINUS { (Sub, $sloc) }
| PLUSMONEY { (Add KMoney, $sloc) }
| MINUSMONEY { (Sub KMoney, $sloc) }
| PLUSDEC { (Add KDec, $sloc) }
| MINUSDEC { (Sub KDec, $sloc) }
| PLUS { (Add KInt, $sloc) }
| MINUS { (Sub KInt, $sloc) }
sum_unop:
| MINUS { (Minus, $sloc) }
| MINUS { (Minus KInt, $sloc) }
| MINUSDEC { (Minus KDec, $sloc) }
| MINUSMONEY { (Minus KMoney, $sloc) }
sum_expression:
| e = mult_expression { e }

View File

@ -11,10 +11,10 @@ let message s =
| 7 ->
"expected another inclusion of a Catala file, since this file is a master file which can \
only contain inclusions of other Catala files\n"
| 283 -> "expected some text, another heading or a law article\n"
| 288 -> "expected a code block, a metadata block, more law text or a heading\n"
| 295 -> "expected a code block, a metadata block, more law text or a heading\n"
| 290 -> "expected a declaration or a scope use\n"
| 301 -> "expected some text, another heading or a law article\n"
| 306 -> "expected a code block, a metadata block, more law text or a heading\n"
| 313 -> "expected a code block, a metadata block, more law text or a heading\n"
| 308 -> "expected a declaration or a scope use\n"
| 21 -> "expected the name of the scope you want to use\n"
| 23 -> "expected a scope use precondition or a colon\n"
| 24 -> "expected an expression which will act as the condition\n"
@ -24,133 +24,133 @@ let message s =
| 29 -> "expected a \"/\"\n"
| 30 -> "expected the third component of the date literal\n"
| 31 -> "expected a delimiter to finish the date literal\n"
| 53 -> "expected an operator to compose the expression on the left with\n"
| 59 -> "expected an enum constructor to test if the expression on the left\n"
| 58 -> "expected an operator to compose the expression on the left with\n"
| 88 -> "expected an expression on the right side of the sum or minus operator\n"
| 112 -> "expected an expression on the right side of the logical operator\n"
| 61 -> "expected an expression for the argument of this function call\n"
| 84 -> "expected an expression on the right side of the comparison operator\n"
| 93 -> "expected an expression on the right side of the multiplication or division operator\n"
| 90 -> "expected an operator to compose the expression on the left\n"
| 122 -> "expected an expression standing for the set you want to test for membership\n"
| 54 -> "expected an identifier standing for a struct field or a subscope name\n"
| 164 -> "expected a colon after the scope use precondition\n"
| 56 -> "expected a constructor, to get the payload of this enum case\n"
| 96 -> "expected the \"for\" keyword to spell the aggregation\n"
| 97 -> "expected an identifier for the aggregation bound variable\n"
| 98 -> "expected the \"in\" keyword\n"
| 99 ->
| 55 -> "expected an operator to compose the expression on the left with\n"
| 61 -> "expected an enum constructor to test if the expression on the left\n"
| 60 -> "expected an operator to compose the expression on the left with\n"
| 102 -> "expected an expression on the right side of the sum or minus operator\n"
| 130 -> "expected an expression on the right side of the logical operator\n"
| 63 -> "expected an expression for the argument of this function call\n"
| 94 -> "expected an expression on the right side of the comparison operator\n"
| 111 -> "expected an expression on the right side of the multiplication or division operator\n"
| 104 -> "expected an operator to compose the expression on the left\n"
| 140 -> "expected an expression standing for the set you want to test for membership\n"
| 56 -> "expected an identifier standing for a struct field or a subscope name\n"
| 182 -> "expected a colon after the scope use precondition\n"
| 58 -> "expected a constructor, to get the payload of this enum case\n"
| 114 -> "expected the \"for\" keyword to spell the aggregation\n"
| 115 -> "expected an identifier for the aggregation bound variable\n"
| 116 -> "expected the \"in\" keyword\n"
| 117 ->
"expected an expression standing for the set over which to compute the aggregation operation\n"
| 101 -> "expected the \"for\" keyword and the expression to compute the aggregate\n"
| 102 -> "expected an expression to compute its aggregation over the set\n"
| 106 -> "expected an expression to take the negation of\n"
| 50 -> "expected an expression to take the opposite of\n"
| 39 -> "expected an expression to match with\n"
| 148 -> "expected a pattern matching case\n"
| 149 -> "expected the name of the constructor for the enum case in the pattern matching\n"
| 155 ->
| 119 -> "expected the \"for\" keyword and the expression to compute the aggregate\n"
| 120 -> "expected an expression to compute its aggregation over the set\n"
| 124 -> "expected an expression to take the negation of\n"
| 52 -> "expected an expression to take the opposite of\n"
| 41 -> "expected an expression to match with\n"
| 166 -> "expected a pattern matching case\n"
| 167 -> "expected the name of the constructor for the enum case in the pattern matching\n"
| 173 ->
"expected a binding for the constructor payload, or a colon and the matching case expression\n"
| 156 -> "expected an identifier for this enum case binding\n"
| 152 -> "expected a colon and then the expression for this matching case\n"
| 158 -> "expected a colon or a binding for the enum constructor payload\n"
| 153 -> "expected an expression for this pattern matching case\n"
| 150 ->
| 174 -> "expected an identifier for this enum case binding\n"
| 170 -> "expected a colon and then the expression for this matching case\n"
| 176 -> "expected a colon or a binding for the enum constructor payload\n"
| 171 -> "expected an expression for this pattern matching case\n"
| 168 ->
"expected another match case or the rest of the expression since the previous match case is \
complete\n"
| 147 -> "expected the \"with patter\" keyword to complete the pattern matching expression\n"
| 40 -> "expected an expression inside the parenthesis\n"
| 145 -> "unmatched parenthesis that should have been closed by here\n"
| 62 -> "expected a unit for this literal, or a valid operator to complete the expression \n"
| 42 -> "expected an expression for the test of the conditional\n"
| 141 -> "expected an expression the for the \"then\" branch of the conditiona\n"
| 142 ->
| 165 -> "expected the \"with patter\" keyword to complete the pattern matching expression\n"
| 42 -> "expected an expression inside the parenthesis\n"
| 163 -> "unmatched parenthesis that should have been closed by here\n"
| 64 -> "expected a unit for this literal, or a valid operator to complete the expression \n"
| 44 -> "expected an expression for the test of the conditional\n"
| 159 -> "expected an expression the for the \"then\" branch of the conditiona\n"
| 160 ->
"expected the \"else\" branch of this conditional expression as the \"then\" branch is \
complete\n"
| 143 -> "expected an expression for the \"else\" branch of this conditional construction\n"
| 140 -> "expected the \"then\" keyword as the conditional expression is complete\n"
| 44 ->
| 161 -> "expected an expression for the \"else\" branch of this conditional construction\n"
| 158 -> "expected the \"then\" keyword as the conditional expression is complete\n"
| 46 ->
"expected the \"all\" keyword to mean the \"for all\" construction of the universal test\n"
| 126 -> "expected an identifier for the bound variable of the universal test\n"
| 127 -> "expected the \"in\" keyword for the rest of the universal test\n"
| 128 -> "expected the expression designating the set on which to perform the universal test\n"
| 129 -> "expected the \"we have\" keyword for this universal test\n"
| 125 -> "expected an expression for the universal test\n"
| 134 -> "expected an identifier that will designate the existential witness for the test\n"
| 135 -> "expected the \"in\" keyword to continue this existential test\n"
| 136 -> "expected an expression that designates the set subject to the existential test\n"
| 137 -> "expected a keyword to form the \"such that\" expression for the existential test\n"
| 138 -> "expected a keyword to complete the \"such that\" construction\n"
| 132 -> "expected an expression for the existential test\n"
| 69 ->
| 144 -> "expected an identifier for the bound variable of the universal test\n"
| 145 -> "expected the \"in\" keyword for the rest of the universal test\n"
| 146 -> "expected the expression designating the set on which to perform the universal test\n"
| 147 -> "expected the \"we have\" keyword for this universal test\n"
| 143 -> "expected an expression for the universal test\n"
| 152 -> "expected an identifier that will designate the existential witness for the test\n"
| 153 -> "expected the \"in\" keyword to continue this existential test\n"
| 154 -> "expected an expression that designates the set subject to the existential test\n"
| 155 -> "expected a keyword to form the \"such that\" expression for the existential test\n"
| 156 -> "expected a keyword to complete the \"such that\" construction\n"
| 150 -> "expected an expression for the existential test\n"
| 71 ->
"expected a payload for the enum case constructor, or the rest of the expression (with an \
operator ?)\n"
| 116 -> "expected an expression for the content of this enum case\n"
| 117 ->
| 134 -> "expected an expression for the content of this enum case\n"
| 135 ->
"the expression for the content of the enum case is already well-formed, expected an \
operator to form a bigger expression\n"
| 49 -> "expected the keyword following cardinal to compute the number of elements in a set\n"
| 165 -> "expected a scope use item: a rule, definition or assertion\n"
| 166 -> "expected the name of the variable subject to the rule\n"
| 185 ->
| 51 -> "expected the keyword following cardinal to compute the number of elements in a set\n"
| 183 -> "expected a scope use item: a rule, definition or assertion\n"
| 184 -> "expected the name of the variable subject to the rule\n"
| 203 ->
"expected a condition or a consequence for this rule, or the rest of the variable qualified \
name\n"
| 180 -> "expected a condition or a consequence for this rule\n"
| 171 -> "expected filled or not filled for a rule consequence\n"
| 181 -> "expected the name of the parameter for this dependent variable \n"
| 168 -> "expected the expression of the rule\n"
| 174 -> "expected the filled keyword the this rule \n"
| 186 -> "expected a struct field or a sub-scope context item after the dot\n"
| 188 -> "expected the name of the variable you want to define\n"
| 189 -> "expected the defined as keyword to introduce the definition of this variable\n"
| 191 -> "expected an expression for the consequence of this definition under condition\n"
| 190 ->
| 198 -> "expected a condition or a consequence for this rule\n"
| 189 -> "expected filled or not filled for a rule consequence\n"
| 199 -> "expected the name of the parameter for this dependent variable \n"
| 186 -> "expected the expression of the rule\n"
| 192 -> "expected the filled keyword the this rule \n"
| 204 -> "expected a struct field or a sub-scope context item after the dot\n"
| 206 -> "expected the name of the variable you want to define\n"
| 207 -> "expected the defined as keyword to introduce the definition of this variable\n"
| 209 -> "expected an expression for the consequence of this definition under condition\n"
| 208 ->
"expected a expression for defining this function, introduced by the defined as keyword\n"
| 192 -> "expected an expression for the definition\n"
| 195 -> "expected an expression that shoud be asserted during execution\n"
| 196 -> "expecting the name of the varying variable\n"
| 198 -> "the variable varies with an expression that was expected here\n"
| 199 -> "expected an indication about the variation sense of the variable, or a new scope item\n"
| 197 -> "expected an indication about what this variable varies with\n"
| 169 -> "expected an expression for this condition\n"
| 177 -> "expected a consequence for this definition under condition\n"
| 208 -> "expected an expression for this definition under condition\n"
| 204 -> "expected the name of the variable that should be fixed\n"
| 205 -> "expected the legislative text by which the value of the variable is fixed\n"
| 206 -> "expected the legislative text by which the value of the variable is fixed\n"
| 212 -> "expected a new scope use item \n"
| 215 -> "expected the kind of the declaration (struct, scope or enum)\n"
| 216 -> "expected the struct name\n"
| 217 -> "expected a colon\n"
| 218 -> "expected struct data or condition\n"
| 219 -> "expected the name of this struct data \n"
| 220 -> "expected the type of this struct data, introduced by the content keyword\n"
| 221 -> "expected the type of this struct data\n"
| 245 -> "expected the name of this struct condition\n"
| 238 -> "expected a new struct data, or another declaration or scope use\n"
| 239 -> "expected the type of the parameter of this struct data function\n"
| 243 -> "expected a new struct data, or another declaration or scope use\n"
| 232 -> "expected a new struct data, or another declaration or scope use\n"
| 235 -> "expected a new struct data, or another declaration or scope use\n"
| 248 -> "expected the name of the scope you are declaring\n"
| 249 -> "expected a colon followed by the list of context items of this scope\n"
| 250 -> "expected a context item introduced by \"context\"\n"
| 251 -> "expected the name of this new context item\n"
| 252 -> "expected the kind of this context item: is it a condition, a sub-scope or a data?\n"
| 253 -> "expected the name of the subscope for this context item\n"
| 260 -> "expected the next context item, or another declaration or scope use\n"
| 255 -> "expected the type of this context item\n"
| 256 -> "expected the next context item or a dependency declaration for this item\n"
| 258 -> "expected the next context item or a dependency declaration for this item\n"
| 263 -> "expected the name of your enum\n"
| 264 -> "expected a colon\n"
| 265 -> "expected an enum case\n"
| 266 -> "expected the name of an enum case \n"
| 267 -> "expected a payload for your enum case, or another case or declaration \n"
| 268 -> "expected a content type\n"
| 273 -> "expected another enum case, or a new declaration or scope use\n"
| 210 -> "expected an expression for the definition\n"
| 213 -> "expected an expression that shoud be asserted during execution\n"
| 214 -> "expecting the name of the varying variable\n"
| 216 -> "the variable varies with an expression that was expected here\n"
| 217 -> "expected an indication about the variation sense of the variable, or a new scope item\n"
| 215 -> "expected an indication about what this variable varies with\n"
| 187 -> "expected an expression for this condition\n"
| 195 -> "expected a consequence for this definition under condition\n"
| 226 -> "expected an expression for this definition under condition\n"
| 222 -> "expected the name of the variable that should be fixed\n"
| 223 -> "expected the legislative text by which the value of the variable is fixed\n"
| 224 -> "expected the legislative text by which the value of the variable is fixed\n"
| 230 -> "expected a new scope use item \n"
| 233 -> "expected the kind of the declaration (struct, scope or enum)\n"
| 234 -> "expected the struct name\n"
| 235 -> "expected a colon\n"
| 236 -> "expected struct data or condition\n"
| 237 -> "expected the name of this struct data \n"
| 238 -> "expected the type of this struct data, introduced by the content keyword\n"
| 239 -> "expected the type of this struct data\n"
| 263 -> "expected the name of this struct condition\n"
| 256 -> "expected a new struct data, or another declaration or scope use\n"
| 257 -> "expected the type of the parameter of this struct data function\n"
| 261 -> "expected a new struct data, or another declaration or scope use\n"
| 250 -> "expected a new struct data, or another declaration or scope use\n"
| 253 -> "expected a new struct data, or another declaration or scope use\n"
| 266 -> "expected the name of the scope you are declaring\n"
| 267 -> "expected a colon followed by the list of context items of this scope\n"
| 268 -> "expected a context item introduced by \"context\"\n"
| 269 -> "expected the name of this new context item\n"
| 270 -> "expected the kind of this context item: is it a condition, a sub-scope or a data?\n"
| 271 -> "expected the name of the subscope for this context item\n"
| 278 -> "expected the next context item, or another declaration or scope use\n"
| 273 -> "expected the type of this context item\n"
| 274 -> "expected the next context item or a dependency declaration for this item\n"
| 276 -> "expected the next context item or a dependency declaration for this item\n"
| 281 -> "expected the name of your enum\n"
| 282 -> "expected a colon\n"
| 283 -> "expected an enum case\n"
| 284 -> "expected the name of an enum case \n"
| 285 -> "expected a payload for your enum case, or another case or declaration \n"
| 286 -> "expected a content type\n"
| 291 -> "expected another enum case, or a new declaration or scope use\n"
| 17 -> "expected a declaration or a scope use\n"
| 19 -> "expected a declaration or a scope use\n"
| 279 ->
| 297 ->
"should not happen, please file an issue at https://github.com/CatalaLang/catala/issues\n"
| _ -> raise Not_found

View File

@ -15,20 +15,33 @@
module Pos = Utils.Pos
module Uid = Utils.Uid
type typ_lit = TBool | TUnit | TInt | TRat | TMoney
type typ =
| TBool
| TUnit
| TInt
| TRat
| TLit of typ_lit
| TTuple of typ Pos.marked list
| TEnum of typ Pos.marked list
| TArrow of typ Pos.marked * typ Pos.marked
type lit = LBool of bool | LEmptyError | LInt of Int64.t | LRat of Q.t | LUnit
type lit = LBool of bool | LEmptyError | LInt of Int64.t | LRat of Q.t | LMoney of Z.t | LUnit
type binop = And | Or | Add | Sub | Mult | Div | Lt | Lte | Gt | Gte | Eq | Neq
type op_kind = KInt | KRat | KMoney
type unop = Not | Minus | ErrorOnEmpty
type binop =
| And
| Or
| Add of op_kind
| Sub of op_kind
| Mult of op_kind
| Div of op_kind
| Lt of op_kind
| Lte of op_kind
| Gt of op_kind
| Gte of op_kind
| Eq
| Neq
type unop = Not | Minus of op_kind | ErrorOnEmpty
type operator = Binop of binop | Unop of unop

View File

@ -26,10 +26,10 @@ let evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked lis
( match (Pos.unmark op, List.map Pos.unmark args) with
| A.Binop A.And, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 && b2))
| A.Binop A.Or, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 || b2))
| A.Binop A.Add, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.add i1 i2))
| A.Binop A.Sub, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.sub i1 i2))
| A.Binop A.Mult, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.mul i1 i2))
| A.Binop A.Div, [ ELit (LInt i1); ELit (LInt i2) ] ->
| A.Binop (A.Add KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.add i1 i2))
| A.Binop (A.Sub KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.sub i1 i2))
| A.Binop (A.Mult KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LInt (Int64.mul i1 i2))
| A.Binop (A.Div KInt), [ ELit (LInt i1); ELit (LInt i2) ] ->
if i2 <> Int64.zero then A.ELit (LInt (Int64.div i1 i2))
else
Errors.raise_multispanned_error "division by zero at runtime"
@ -37,10 +37,10 @@ let evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked lis
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 2));
]
| A.Binop A.Add, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.add i1 i2))
| A.Binop A.Sub, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.sub i1 i2))
| A.Binop A.Mult, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.mul i1 i2))
| A.Binop A.Div, [ ELit (LRat i1); ELit (LRat i2) ] ->
| A.Binop (A.Add KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.add i1 i2))
| A.Binop (A.Sub KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.sub i1 i2))
| A.Binop (A.Mult KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LRat (Q.mul i1 i2))
| A.Binop (A.Div KRat), [ ELit (LRat i1); ELit (LRat i2) ] ->
if i2 <> Q.zero then A.ELit (LRat (Q.div i1 i2))
else
Errors.raise_multispanned_error "division by zero at runtime"
@ -48,24 +48,25 @@ let evaluate_operator (op : A.operator Pos.marked) (args : A.expr Pos.marked lis
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 2));
]
| A.Binop A.Lt, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 < i2))
| A.Binop A.Lte, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 <= i2))
| A.Binop A.Gt, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 > i2))
| A.Binop A.Gte, [ 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.Lt, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 < i2))
| A.Binop A.Lte, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 <= i2))
| A.Binop A.Gt, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 > i2))
| A.Binop A.Gte, [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 >= i2))
| A.Binop (A.Lt KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 < i2))
| A.Binop (A.Lte KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 <= i2))
| A.Binop (A.Gt KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 > i2))
| A.Binop (A.Gte KInt), [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 >= i2))
| A.Binop (A.Lt KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 < i2))
| A.Binop (A.Lte KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 <= i2))
| A.Binop (A.Gt KRat), [ ELit (LRat i1); ELit (LRat i2) ] -> A.ELit (LBool Q.(i1 > i2))
| A.Binop (A.Gte KRat), [ 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 (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.Neq, [ ELit (LInt i1); ELit (LInt i2) ] -> A.ELit (LBool (i1 <> i2))
| A.Binop A.Neq, [ ELit (LBool b1); ELit (LBool b2) ] -> A.ELit (LBool (b1 <> b2))
| A.Binop A.Neq, [ _; _ ] -> A.ELit (LBool true)
| A.Binop _, ([ ELit LEmptyError; _ ] | [ _; ELit LEmptyError ]) -> A.ELit LEmptyError
| A.Unop (A.Minus KInt), [ ELit (LInt i) ] -> A.ELit (LInt (Int64.sub Int64.zero i))
| A.Unop (A.Minus KRat), [ ELit (LRat i) ] -> A.ELit (LRat (Q.sub Q.zero i))
| A.Unop A.Not, [ ELit (LBool b) ] -> A.ELit (LBool (not b))
| A.Unop A.Minus, [ ELit (LInt i) ] -> A.ELit (LInt (Int64.sub Int64.zero i))
| A.Unop A.ErrorOnEmpty, [ e' ] ->
if e' = A.ELit LEmptyError then
Errors.raise_spanned_error
@ -206,7 +207,9 @@ let empty_thunked_term : Ast.expr Pos.marked =
(Ast.make_abs
(Array.of_list [ silent ])
(Bindlib.box (Ast.ELit Ast.LEmptyError, Pos.no_pos))
Pos.no_pos [ (Ast.TUnit, Pos.no_pos) ] Pos.no_pos)
Pos.no_pos
[ (Ast.TLit Ast.TUnit, Pos.no_pos) ]
Pos.no_pos)
let interpret_program (e : Ast.expr Pos.marked) : (Ast.Var.t * Ast.expr Pos.marked) list =
match Pos.unmark (evaluate_expr e) with

View File

@ -24,10 +24,11 @@ let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked) : unit =
else Format.fprintf fmt "%a" format_typ t
in
match Pos.unmark typ with
| TUnit -> Format.fprintf fmt "unit"
| TBool -> Format.fprintf fmt "bool"
| TInt -> Format.fprintf fmt "int"
| TRat -> Format.fprintf fmt "dec"
| TLit TUnit -> Format.fprintf fmt "unit"
| TLit TBool -> Format.fprintf fmt "bool"
| TLit TInt -> Format.fprintf fmt "int"
| TLit TRat -> Format.fprintf fmt "dec"
| TLit TMoney -> Format.fprintf fmt "money"
| TTuple ts ->
Format.fprintf fmt "(%a)"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt " *@ ") format_typ)
@ -46,26 +47,27 @@ let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
| LEmptyError -> Format.fprintf fmt ""
| LUnit -> Format.fprintf fmt "()"
| LRat i -> Format.fprintf fmt "%f" (Q.to_float i)
| LMoney e -> Format.fprintf fmt "$%.2f" Q.(to_float (of_bigint e / of_int 100))
let format_binop (fmt : Format.formatter) (op : binop Pos.marked) : unit =
Format.fprintf fmt "%s"
( match Pos.unmark op with
| Add -> "+"
| Sub -> "-"
| Mult -> "*"
| Div -> "/"
| Add _ -> "+"
| Sub _ -> "-"
| Mult _ -> "*"
| Div _ -> "/"
| And -> "&&"
| Or -> "||"
| Eq -> "=="
| Neq -> "!="
| Lt -> "<"
| Lte -> "<="
| Gt -> ">"
| Gte -> ">=" )
| Lt _ -> "<"
| Lte _ -> "<="
| Gt _ -> ">"
| Gte _ -> ">=" )
let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
Format.fprintf fmt "%s"
(match Pos.unmark op with Minus -> "-" | Not -> "~" | ErrorOnEmpty -> "error_on_empty")
(match Pos.unmark op with Minus _ -> "-" | Not -> "~" | ErrorOnEmpty -> "error_on_empty")
let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ -> true | _ -> false

View File

@ -21,10 +21,7 @@ module A = Ast
module Cli = Utils.Cli
type typ =
| TUnit
| TInt
| TBool
| TRat
| TLit of A.typ_lit
| TArrow of typ Pos.marked UnionFind.elem * typ Pos.marked UnionFind.elem
| TTuple of typ Pos.marked UnionFind.elem list
| TEnum of typ Pos.marked UnionFind.elem list
@ -33,10 +30,11 @@ type typ =
let rec format_typ (fmt : Format.formatter) (ty : typ Pos.marked UnionFind.elem) : unit =
let ty_repr = UnionFind.get (UnionFind.find ty) in
match Pos.unmark ty_repr with
| TUnit -> Format.fprintf fmt "unit"
| TBool -> Format.fprintf fmt "bool"
| TInt -> Format.fprintf fmt "int"
| TRat -> Format.fprintf fmt "dec"
| TLit TUnit -> Format.fprintf fmt "unit"
| TLit TBool -> Format.fprintf fmt "bool"
| TLit TInt -> Format.fprintf fmt "int"
| TLit TRat -> Format.fprintf fmt "dec"
| TLit TMoney -> Format.fprintf fmt "money"
| TAny -> Format.fprintf fmt "any type"
| TTuple ts ->
Format.fprintf fmt "(%a)"
@ -53,8 +51,7 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin
let t1_repr = UnionFind.get (UnionFind.find t1) in
let t2_repr = UnionFind.get (UnionFind.find t2) in
match (t1_repr, t2_repr) with
| (TUnit, _), (TUnit, _) | (TBool, _), (TBool, _) | (TInt, _), (TInt, _) | (TRat, _), (TRat, _) ->
()
| (TLit tl1, _), (TLit tl2, _) when tl1 = tl2 -> ()
| (TArrow (t11, t12), _), (TArrow (t21, t22), _) ->
unify t11 t21;
unify t12 t22
@ -68,8 +65,8 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin
(* TODO: if we get weird error messages, then it means that we should use the persistent
version of the union-find data structure. *)
Errors.raise_multispanned_error
(Format.asprintf "Error during typechecking, type mismatch: cannot unify %a and %a"
format_typ t1 format_typ t2)
(Format.asprintf "Error during typechecking, types %a and %a are incompatible" format_typ t1
format_typ t2)
[
(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);
@ -77,24 +74,30 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin
let op_type (op : A.operator Pos.marked) : typ Pos.marked UnionFind.elem =
let pos = Pos.get_position op in
let bt = UnionFind.make (TBool, pos) in
let bt = UnionFind.make (TLit TBool, pos) in
let it = UnionFind.make (TLit TInt, pos) in
let rt = UnionFind.make (TLit TRat, pos) in
let mt = UnionFind.make (TLit TMoney, pos) in
let any = UnionFind.make (TAny, pos) in
let arr x y = UnionFind.make (TArrow (x, y), pos) in
match Pos.unmark op with
| A.Binop (A.And | A.Or) -> arr bt (arr bt bt)
| A.Binop (A.Add | A.Sub | A.Mult | A.Div) -> arr any (arr any any)
| A.Binop (A.Lt | A.Lte | A.Gt | A.Gte) -> arr any (arr any bt)
| 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 KMoney | A.Sub KMoney | A.Mult KMoney | A.Div KMoney) -> arr mt (arr mt mt)
| A.Binop (A.Lt KInt | A.Lte KInt | A.Gt KInt | A.Gte KInt) -> arr it (arr it bt)
| A.Binop (A.Lt KRat | A.Lte KRat | A.Gt KRat | A.Gte KRat) -> arr rt (arr rt bt)
| A.Binop (A.Lt KMoney | A.Lte KMoney | A.Gt KMoney | A.Gte KMoney) -> arr mt (arr mt bt)
| A.Binop (A.Eq | A.Neq) -> arr any (arr any bt)
| A.Unop A.Minus -> arr any any
| A.Unop (A.Minus KInt) -> arr it it
| A.Unop (A.Minus KRat) -> arr rt rt
| A.Unop (A.Minus KMoney) -> arr mt mt
| A.Unop A.Not -> arr bt bt
| A.Unop A.ErrorOnEmpty -> arr any any
let rec ast_to_typ (ty : A.typ) : typ =
match ty with
| A.TUnit -> TUnit
| A.TBool -> TBool
| A.TRat -> TRat
| A.TInt -> TInt
| A.TLit l -> TLit l
| A.TArrow (t1, t2) ->
TArrow
( UnionFind.make (Pos.map_under_mark ast_to_typ t1),
@ -106,14 +109,11 @@ let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked =
Pos.map_under_mark
(fun ty ->
match ty with
| TUnit -> A.TUnit
| TBool -> A.TBool
| TInt -> A.TInt
| TRat -> A.TRat
| TLit l -> A.TLit l
| TTuple ts -> A.TTuple (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)
| TAny -> A.TUnit)
| TAny -> A.TLit A.TUnit)
(UnionFind.get (UnionFind.find ty))
type env = typ Pos.marked A.VarMap.t
@ -127,10 +127,11 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e) )
| ELit (LBool _) -> UnionFind.make (Pos.same_pos_as TBool e)
| ELit (LInt _) -> UnionFind.make (Pos.same_pos_as TInt e)
| ELit (LRat _) -> UnionFind.make (Pos.same_pos_as TRat e)
| ELit LUnit -> UnionFind.make (Pos.same_pos_as TUnit e)
| ELit (LBool _) -> UnionFind.make (Pos.same_pos_as (TLit TBool) e)
| ELit (LInt _) -> UnionFind.make (Pos.same_pos_as (TLit TInt) e)
| ELit (LRat _) -> UnionFind.make (Pos.same_pos_as (TLit TRat) e)
| ELit (LMoney _) -> UnionFind.make (Pos.same_pos_as (TLit TMoney) e)
| ELit LUnit -> UnionFind.make (Pos.same_pos_as (TLit TUnit) e)
| ELit LEmptyError -> UnionFind.make (Pos.same_pos_as TAny e)
| ETuple es ->
let ts = List.map (fun (e, _) -> typecheck_expr_bottom_up env e) es in
@ -209,12 +210,12 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m
t_ret
| EOp op -> op_type (Pos.same_pos_as op e)
| EDefault (just, cons, subs) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as TBool just));
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 sub -> typecheck_expr_top_down env sub tcons) subs;
tcons
| EIfThenElse (cond, et, ef) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as TBool cond));
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
@ -228,10 +229,11 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e) )
| ELit (LBool _) -> unify tau (UnionFind.make (Pos.same_pos_as TBool e))
| ELit (LInt _) -> unify tau (UnionFind.make (Pos.same_pos_as TInt e))
| ELit (LRat _) -> unify tau (UnionFind.make (Pos.same_pos_as TRat e))
| ELit LUnit -> unify tau (UnionFind.make (Pos.same_pos_as TUnit e))
| ELit (LBool _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TBool) e))
| ELit (LInt _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TInt) e))
| ELit (LRat _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TRat) e))
| ELit (LMoney _) -> unify tau (UnionFind.make (Pos.same_pos_as (TLit TMoney) 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))
| ETuple es -> (
let tau' = UnionFind.get (UnionFind.find tau) in
@ -333,11 +335,11 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
let op_typ = op_type (Pos.same_pos_as op e) in
unify op_typ tau
| EDefault (just, cons, subs) ->
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as TBool just));
typecheck_expr_top_down env just (UnionFind.make (Pos.same_pos_as (TLit TBool) just));
typecheck_expr_top_down env cons tau;
List.iter (fun sub -> typecheck_expr_top_down env sub tau) subs
| EIfThenElse (cond, et, ef) ->
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as TBool cond));
typecheck_expr_top_down env cond (UnionFind.make (Pos.same_pos_as (TLit TBool) cond));
typecheck_expr_top_down env et tau;
typecheck_expr_top_down env ef tau

View File

@ -65,10 +65,7 @@ module LocationSet = Set.Make (struct
end)
type typ =
| TBool
| TUnit
| TInt
| TRat
| TLit of Dcalc.Ast.typ_lit
| TStruct of StructName.t
| TEnum of EnumName.t
| TArrow of typ Pos.marked * typ Pos.marked

View File

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

View File

@ -37,10 +37,11 @@ let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked) : unit =
else Format.fprintf fmt "%a" format_typ t
in
match Pos.unmark typ with
| TUnit -> Format.fprintf fmt "unit"
| TBool -> Format.fprintf fmt "bool"
| TInt -> Format.fprintf fmt "int"
| TRat -> Format.fprintf fmt "dec"
| TLit TUnit -> Format.fprintf fmt "unit"
| TLit TBool -> Format.fprintf fmt "bool"
| TLit TInt -> Format.fprintf fmt "int"
| TLit TRat -> Format.fprintf fmt "dec"
| TLit TMoney -> Format.fprintf fmt "money"
| TStruct s -> Format.fprintf fmt "%a" Ast.StructName.format_t s
| TEnum e -> Format.fprintf fmt "%a" Ast.EnumName.format_t e
| TArrow (t1, t2) ->

View File

@ -45,10 +45,7 @@ let hole_var : Dcalc.Ast.Var.t = Dcalc.Ast.Var.make ("·", Pos.no_pos)
let rec translate_typ (ctx : ctx) (t : Ast.typ Pos.marked) : Dcalc.Ast.typ Pos.marked =
Pos.same_pos_as
( match Pos.unmark t with
| Ast.TUnit -> Dcalc.Ast.TUnit
| Ast.TBool -> Dcalc.Ast.TBool
| Ast.TInt -> Dcalc.Ast.TInt
| Ast.TRat -> Dcalc.Ast.TRat
| Ast.TLit l -> Dcalc.Ast.TLit l
| Ast.TArrow (t1, t2) -> Dcalc.Ast.TArrow (translate_typ ctx t1, translate_typ ctx t2)
| Ast.TStruct s_uid ->
let s_fields = Ast.StructMap.find s_uid ctx.structs in
@ -299,7 +296,7 @@ let rec translate_rule (ctx : ctx) (rule : Ast.rule) (rest : Ast.rule list) (pos
Dcalc.Ast.make_abs
(Array.of_list [ Pos.unmark a_var ])
next_e var_def_pos
[ (Dcalc.Ast.TArrow ((TUnit, var_def_pos), tau), var_def_pos) ]
[ (Dcalc.Ast.TArrow ((TLit TUnit, var_def_pos), tau), var_def_pos) ]
(Pos.get_position e)
in
let new_e = translate_expr ctx e in
@ -308,7 +305,7 @@ let rec translate_rule (ctx : ctx) (rule : Ast.rule) (rest : Ast.rule list) (pos
Dcalc.Ast.make_abs
(Array.of_list [ silent_var ])
new_e var_def_pos
[ (Dcalc.Ast.TUnit, var_def_pos) ]
[ (Dcalc.Ast.TLit TUnit, var_def_pos) ]
var_def_pos
in
let out_e = Dcalc.Ast.make_app intermediate_e [ thunked_new_e ] (Pos.get_position e) in
@ -416,7 +413,7 @@ let translate_scope_decl (struct_ctx : Ast.struct_ctx) (enum_ctx : Ast.enum_ctx)
rules pos_sigma
(List.map
(fun (_, tau, _) ->
(Dcalc.Ast.TArrow ((Dcalc.Ast.TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma))
(Dcalc.Ast.TArrow ((Dcalc.Ast.TLit TUnit, pos_sigma), (tau, pos_sigma)), pos_sigma))
scope_variables)
pos_sigma
@ -425,7 +422,7 @@ let build_scope_typ_from_sig (scope_sig : (Ast.ScopeVar.t * Dcalc.Ast.typ) list)
let result_typ = (Dcalc.Ast.TTuple (List.map (fun (_, tau) -> (tau, pos)) scope_sig), pos) in
List.fold_right
(fun (_, arg_t) acc ->
(Dcalc.Ast.TArrow ((Dcalc.Ast.TArrow ((TUnit, pos), (arg_t, pos)), pos), acc), pos))
(Dcalc.Ast.TArrow ((Dcalc.Ast.TArrow ((TLit TUnit, pos), (arg_t, pos)), pos), acc), pos))
scope_sig result_typ
let translate_program (prgm : Ast.program) (top_level_scope_name : Ast.ScopeName.t) :

View File

@ -9,5 +9,5 @@ new scope A:
scope A:
def x := 84.648665
def y := 4.368297
def z := x / y
def z := x /. y
*/