Commit 13c359c8 authored by François Bobot's avatar François Bobot

Merge branch 'master' into 'colibri'

# Conflicts:
#   examples/stdlib/tagset/why3session.xml
parents 08e24f3a 1aca8fe6
:x: marks a potential source of incompatibility
Standard library
* set library revamped
- set.Fset
type `set` -> type `fset` and `choose` -> `pick`
- `appset.Appset` -> `set.SetApp` and `impset.Impset` -> `set.SetImp`
type `t` -> `set` and `.contents` -> `.to_fset`
`empty` -> `empty ()`
* the `set` library has been revamped :x:
- in `set.Fset`, type `set` becomes `fset`; `choose` becomes `pick`
- module `appset.Appset` becomes `set.SetApp`;
`impset.Impset` becomes `set.SetImp`
- in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
Language
* It is now possible to give a name to requires and assertions.
`requires Hyp { a = 3 }` tries to give the name `Hyp` to the corresponding
hypothesis after introduction. This uses the attribute [@hyp_name:] which is
now reserved.
Tools
* why3prove counterexamples output is not JSON by default. To restore previous
behavior, pass the argument --json
* counterexamples given by `why3prove` are no longer printed using JSON
by default; pass option `--json` to restore the previous behavior
API
* function Call_provers.print_prover_result now takes an additional boolean
argument ~json_model which state if the counterexamples are printed with json
format :x:
* `Call_provers.print_prover_result` now takes an additional argument
`~json_model` to indicate whether counterexamples are printed using JSON :x:
* Counterexamples: indices of array are now model_value. :x:
* ITP constructor Task now contain the location of the goal :x:
Transformations
* Improvement of apply/rewrite in presence of let. Solve a bug that prevents
applying hypothesis with nested let-bindings :x:
* Adding arguments to transformations without arguments is now forbidden
(previously ignored):x:
* Fix crash of eliminate_unknown_types
* Giving too many arguments to a transformation do not display a popup anymore
* Fix behavior of induction_arg_ty_lex (now equivalent to induction_ty_lex)
* `apply`/`rewrite` behaves better in presence of `let`;
hypotheses with nested let-bindings can now be applied :x:
* passing arguments to argument-free transformations is now forbidden
(previously ignored) :x:
* passing too many arguments to a transformation does not display a popup anymore
* `induction_arg_ty_lex` is now equivalent to `induction_ty_lex`
* `induction_arg_pr` now takes an optional argument that indicates what to
generalize in the induction
* `destruct` now destruct `not p` into `p -> false`. `destruct_rec` is
allowed to further destruct afterwards.
`destruct` can also destruct `true` and `false`.
* decision procedures used for reflection now must be declared explicitly using
`meta reflection val <function_name>` :x:
* `remove` should not raise unnecessary popups anymore. Added `remove_rec`.
`bisect` should not raise unnecessary popups too.
Counterexamples
* Improved display of counterexamples in Task view
IDE
* display of counterexamples in the Task view has been improved
* auto jumping to next unproved goal can now be disabled in the preferences
* add a "reset proofs" command in the Tools menu. It removes all proofs in
the session
* strategies can now be defined using %t (resp. %m) for using a prover with
the default timelimit (resp. memlimit)
Realizations
* Added experimental realizations for new Set theories in both Isabelle and
Coq
Provers
* support for CVC4 1.7 (released April 9, 2019)
* support for Alt-Ergo 2.3.0 (released February 11, 2019)
Version 1.2.0, February 11, 2019
--------------------------------
......@@ -42,7 +69,6 @@ Drivers
be replaced by `syntax literal` and/or `syntax function` :x:
Language
* the `any` expression is now always ghost :x:
* a syntactic sugar called "auto-dereference" is introduced, so as
to avoid, on simple programs, the heavy use of `(!)` character on
references; see details in Section A.1 of the manual
......
......@@ -974,7 +974,7 @@ COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime Coprime
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET_FILES = Set Cardinal Fset FsetInduction FsetInt FsetSum SetApp SetAppInt SetImp SetImpInt
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
......
......@@ -44,6 +44,12 @@ decide_fail () {
# Inconsistent results between two runs
"bench/ce/ref_mono_Z3,4.6.0_SP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_WP")
is_xfail=integer_values;;
# Inconsistent results between two runs
"bench/ce/floats_Z3,4.6.0_SP")
is_xfail=integer_values;;
*) is_xfail=none;;
esac
}
......@@ -71,12 +77,15 @@ run () {
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
# This ad hoc sed removes diff between Timeout and Unknown (unknown)
# when running from platform with different speed.
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' | \
sed -r 's/(Timeout.*$|Unknown \(unknown\).*$)/Timeout or Unknown/' | \
# ad hoc sed to remove the directory of the stdlib that can be found
# inside labels attribute [@at:'Old:loc:/home/.../stdlib/array.mlw
# TODO temporary as this comes from incorrect locations generated in
# a[i] <- x like terms.
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' >> "$f.out"
sed -r 's/\:loc\:.*\]/\:loc\:location\]/' | \
# Remove steps informations
sed -r 's/Unknown \(sat\).*$/Unknown \(sat\)/' | \
sed -r 's/Valid \(.*$/Valid/' >> "$f.out"
str_oracle=$(tr -d ' \n' < "${oracle_file}")
str_out=$(tr -d ' \n' < "$f.out")
decide_fail $f
......
......@@ -42,3 +42,11 @@ goal t1 : forall t:map int int, i : int.
get (set t 0 42) i = get t i
end
module OtherIndices
use map.Map
goal g : forall m: map real real. m 0.1 = 0.0 \/ m 0.2 = m 0.1
end
\ No newline at end of file
......@@ -29,15 +29,19 @@ a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......@@ -45,24 +49,30 @@ Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -29,15 +29,19 @@ a at 'Old, [[@introduced], [@at:'Old],
[@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......@@ -45,24 +49,30 @@ Line 38:
a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
[@at:'Old:loc:location] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : "1" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"indice" : {"type" : "Integer" , "val" : "1" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "0" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -34,7 +34,8 @@ a at 'Old, [[@introduced], [@at:'Old],
"val" : "2" } }] } }
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......@@ -48,14 +49,16 @@ a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -34,7 +34,8 @@ a at 'Old, [[@introduced], [@at:'Old],
"val" : "2" } }] } }
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......@@ -48,14 +49,16 @@ a, [[@introduced], [@at:'Old], [@at:'Old:loc:location],
Line 40:
a, [[@introduced], [@model_trace:a]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
Line 41:
a, [[@introduced]] = {"type" : "Record" ,
"val" : {"Field" : [{"field" : "elts" , "value" : {"type" : "Array" ,
"val" : [{"indice" : "0" , "value" : {"type" : "Integer" , "val" : "42" } },
"val" : [{"indice" : {"type" : "Integer" , "val" : "0" } ,
"value" : {"type" : "Integer" , "val" : "42" } },
{"others" : {"type" : "Integer" , "val" : "4" } }] } }, {"field" : "length" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }] } }
......
......@@ -7,7 +7,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 5:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -22,7 +22,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 7:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -37,7 +37,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 9:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -52,7 +52,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 11:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -67,7 +67,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "17\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 13:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -82,7 +82,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 15:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -97,7 +97,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 17:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -112,7 +112,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 19:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -124,30 +124,30 @@ Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 21:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "2" } }
"val" : "0" } }
bench/ce/floats.mlw T32 g10: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
Line 63:
zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "340282346638528859811704183484516925440" }
File floats.mlw:
Line 23:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
"value" : {"type" : "Integer" ,
"val" : "10" } }
"val" : "1" } }
bench/ce/floats.mlw T64 g1: Timeout or Unknown
Counter-example model:File ieee_float.mlw:
......@@ -157,7 +157,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 31:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -172,7 +172,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "5\/4" } }
Line 222:
max_int, [] = {"type" : "Integer" ,
"val" : "-1" }
"val" : "179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368" }
File floats.mlw:
Line 33:
x, [[@introduced]] = {"proj_name" : "t'real" , "type" : "Proj" ,
......@@ -187,7 +187,7 @@ zeroF, [] = {"proj_name" : "t'real" , "type" : "Proj" ,
"val" : "0" } }
Line 222:
max_int, [] = {"type" : "Integer" ,