Project

General

Profile

Revision 59020713 src/typing.ml

View differences:

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