programs: construct 'any'

parent 3d24980f
......@@ -101,6 +101,7 @@ echo ""
echo "=== Parsing programs ==="
pgml_options=--parse-only
programs bench/programs/bad-typing
programs bench/programs/good
programs examples/programs
echo ""
......
......@@ -29,7 +29,7 @@
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("and" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
`(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
"Minimal highlighting for Why mode")
......
......@@ -95,7 +95,7 @@ and expr_desc =
| Ecast of expr * Ptree.pty
| Eany of type_c
(* TODO: post?, ghost *)
(* TODO: ghost *)
and triple = pre * expr * post
......
......@@ -96,6 +96,7 @@ and dexpr_desc =
| DEassert of assertion_kind * Ptree.lexpr
| DEghost of dexpr
| DElabel of string * dexpr
| DEany of dtype_c
and dtriple = dpre * dexpr * dpost
......@@ -163,6 +164,7 @@ and expr_desc =
| Eassert of assertion_kind * Term.fmla
| Eghost of expr
| Elabel of string * expr
| Eany of type_c
and recfun = Term.vsymbol * binder list * variant option * triple
......
......@@ -343,9 +343,9 @@ and dexpr_desc env loc = function
let ty = pure_type env ty in
expected_type e1 ty;
e1.dexpr_desc, ty
| Pgm_ptree.Eany _c ->
(* let c = dtype_c env c in *)
(* DEany c, c.dc_result_type *)assert false (*TODO*)
| Pgm_ptree.Eany c ->
let c = dtype_c env c in
DEany c, dpurify env c.dc_result_type
and dletrec env dl =
(* add all functions into environment *)
......@@ -520,6 +520,9 @@ and expr_desc uc env denv = function
let v = create_vsymbol (id_fresh s) ty in
let env = Mstr.add s v env in
Elabel (s, expr uc env e1)
| DEany c ->
let c = type_c uc env c in
Eany c
and letrec uc env dl =
(* add all functions into env, and compute local env *)
......@@ -620,9 +623,11 @@ End:
*)
(*
TODO:
- tuples
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified
- ghost / effects
*)
......@@ -54,6 +54,11 @@ parameter r : int ref
let foo = g 2 r
let p12 () =
let x = any int in
x + any int
(*
Local Variables:
compile-command: "unset LANG; make -C .. testl"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment