Commit eabd287d authored by Mário Pereira's avatar Mário Pereira
Browse files

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr/gitroot/why3/why3 into new_system

parents fe19c708 2c0d4f34
use import int.Int
use import ref.Ref
let rec test (m n: ref int) : unit
variant { !m }
requires { !m >= 0 }
ensures { !m = 0 /\ !n = !(old m) + !(old n) }
= if !m > 0 then begin
m := !m - 1;
test m n;
n := !n + 1
end
......@@ -47,9 +47,9 @@ syn cluster whyContained contains=whyTodo,whyImport,whyExport,whyTheoryContents
" ,whyPreDef,whyModParam,whyModParam1,whyPreMPRestr,whyMPRestr,whyMPRestr1,whyMPRestr2,whyMPRestr3,whyModRHS,whyFuncWith,whyFuncStruct,whyModTypeRestr,whyModTRWith,whyWith,whyWithRest,whyModType,whyFullMod,whyVal
" Enclosing delimiters
syn region whyEncl transparent matchgroup=whyKeyword start="(" matchgroup=whyKeyword end=")" contains=ALLBUT,@whyContained,whyParenErr
syn region whyEncl transparent matchgroup=whyKeyword start="{" matchgroup=whyKeyword end="}" contains=ALLBUT,@whyContained,whyBraceErr
syn region whyEncl transparent matchgroup=whyKeyword start="\[" matchgroup=whyKeyword end="\]" contains=ALLBUT,@whyContained,whyBrackErr
syn region whyEncl transparent matchgroup=whyKeyChar start="(" matchgroup=whyKeyChar end=")" contains=ALLBUT,@whyContained,whyParenErr
syn region whyEncl transparent matchgroup=whyKeyChar start="{" matchgroup=whyKeyChar end="}" contains=ALLBUT,@whyContained,whyBraceErr
syn region whyEncl transparent start="\[" end="\]" contains=ALLBUT,@whyContained,whyBrackErr
" Comments
syn region whyComment start="(\*" end="\*)" contains=whyComment,whyTodo
......@@ -111,7 +111,7 @@ syn region whyString start=+"+ skip=+\\\\\|\\"+ end=+"+
syn match whyOperator "->"
syn match whyOperator "<->\?"
syn match whyOperator "/\\"
syn match whyOperator "\\[/!?]\?"
syn match whyOperator "\\/"
syn match whyOperator "&&"
syn match whyOperator "<>"
syn match whyKeyChar "|"
......@@ -184,9 +184,9 @@ if version >= 508 || !exists("did_why_syntax_inits")
HiLink whyConstructor Constant
HiLink whyKeyword Keyword
HiLink whyKeyChar Keyword
HiLink whyAnyVar Keyword
HiLink whyOperator Keyword
HiLink whyKeyChar Operator
HiLink whyAnyVar Operator
HiLink whyOperator Operator
HiLink whySpec Identifier
HiLink whyNumber Number
......
......@@ -769,6 +769,8 @@ let t_open_quant (vl,b,tl,f) =
let tl = tr_map (t_subst_unsafe m) tl in
vl, tl, t_subst_unsafe m f
let t_clone_bound_id (v,_,_) = id_clone v.vs_name
(** open bindings with optimized closing callbacks *)
let t_open_bound_cb tb =
......@@ -1514,6 +1516,9 @@ let t_if_simp f1 f2 f3 = match f1.t_node, f2.t_node, f3.t_node with
let small t = match t.t_node with
| Tvar _ | Tconst _ -> true
(* NOTE: shouldn't we allow this?
| Tapp (_,[]) -> true
*)
| _ -> false
let t_let_simp e ((v,b,t) as bt) =
......
......@@ -162,6 +162,7 @@ val t_open_branch : term_branch -> pattern * term
val t_open_quant : term_quant -> vsymbol list * trigger * term
val t_open_bound_with : term -> term_bound -> term
val t_clone_bound_id : term_bound -> preid
(** open bindings with optimized closing callbacks *)
......
......@@ -1152,13 +1152,13 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
| DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
let ld, env = var_defn uloc env dldf in
let e2 = expr uloc env de in
e_let ld e2
e_let_check e2 ld
| DElet (dldf,de) ->
let ldl, env = sym_defn uloc env dldf in
List.fold_left e_let_check (expr uloc env de) ldl
| DErec (drdf,de) ->
let ld, env = rec_defn uloc env drdf in
e_let ld (expr uloc env de)
e_let_check (expr uloc env de) ld
| DEnot de ->
e_not (expr uloc env de)
| DEand (de1,de2) ->
......
......@@ -1156,6 +1156,10 @@ let open_post_with t q = match q.t_node with
| Teps bf -> t_open_bound_with t bf
| _ -> invalid_arg "Ity.open_post_with"
let clone_post_result q = match q.t_node with
| Teps bf -> t_clone_bound_id bf
| _ -> invalid_arg "Ity.clone_post_result"
type cty = {
cty_args : pvsymbol list;
cty_pre : pre list;
......
......@@ -388,6 +388,7 @@ type post = term (** postcondition: eps result . post_fmla *)
val open_post : post -> vsymbol * term
val open_post_with : term -> post -> term
val clone_post_result : post -> preid
val create_post : vsymbol -> term -> post
......
This diff is collapsed.
......@@ -138,7 +138,7 @@ let test_extract fmt m =
let rec do_extract_module ?fname m =
test_extract (Format.formatter_of_out_channel stdout) m;
let extract_use m' =
let _extract_use m' =
let fname =
if m'.mod_theory.Theory.th_path = [] then fname else None
in
......
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