Revision 59020713
Added by Pierre-Loïc Garoche almost 6 years ago
| src/typing.ml | ||
|---|---|---|
| 27 | 27 |
open Format |
| 28 | 28 |
|
| 29 | 29 |
|
| 30 |
(* TODO general remark: expect in the add_vdelc, it seems to me that
|
|
| 30 |
(* TODO general remark: except in the add_vdecl, it seems to me that
|
|
| 31 | 31 |
all the pairs (env, vd_env) should be replace with just env, since |
| 32 | 32 |
vd_env is never used and the env element is always extract with a |
| 33 | 33 |
fst *) |
| ... | ... | |
| 686 | 686 |
undefined_vars_init |
| 687 | 687 |
eqs |
| 688 | 688 |
in |
| 689 |
|
|
| 689 |
(* Typing each predicate expr *) |
|
| 690 |
let type_pred_ee ee : unit= |
|
| 691 |
type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool |
|
| 692 |
in |
|
| 693 |
List.iter type_pred_ee |
|
| 694 |
( |
|
| 695 |
spec.assume |
|
| 696 |
@ spec.guarantees |
|
| 697 |
@ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) |
|
| 698 |
); |
|
| 690 | 699 |
(*TODO |
| 691 | 700 |
enrich env locally with locals and consts |
| 692 | 701 |
type each pre/post as a boolean expr |
Also available in: Unified diff
Some progress on EMF bqckend. Refactoring machines code