Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
2e98995c
Commit
2e98995c
authored
Sep 14, 2013
by
MARCHE Claude
Browse files
Interp: removed debug msgs and add tests with Fibonacci
parent
61750d2b
Changes
2
Hide whitespace changes
Inline
Side-by-side
examples/fibonacci.mlw
View file @
2e98995c
...
...
@@ -144,4 +144,10 @@ module FibonacciLogarithmic
let fibo n requires { n >= 0 } ensures { result = fib n } =
let _, b = logfib n in b
let test0 () = fibo 0
let test1 () = fibo 1
let test7 () = fibo 7
let test42 () = fibo 42
end
src/whyml/mlw_interp.ml
View file @
2e98995c
...
...
@@ -622,7 +622,7 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
(
fun
_
_
->
assert
false
)
subst
env'
.
regenv
}
in
(*
*)
(*
eprintf "@[Evaluating function body of %s in regenv: %a@\nand state: %a@]@."
ps.ps_name.Ident.id_string
(Pp.print_list Pp.comma
...
...
@@ -632,9 +632,12 @@ let rec eval_expr env (s:state) (e : expr) : result * state =
Mlw_pretty.print_reg r2))
(Mreg.bindings env''.regenv)
print_state s';
*)
let
r
,
s''
=
eval_expr
env''
s'
lam
.
l_expr
in
(*
printf "@[ -> result: %a@\nstate: %a@]@."
print_result r print_state s'';
*)
r
,
s''
|
_
->
Irred
e
,
s
end
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment