Project

General

Profile

Revision 217837e2 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
31
   all the pairs (env, vd_env) should be replace with just env, since
32
   vd_env is never used and the env element is always extract with a
33
   fst *)
34

  
35
   
30 36
module type EXPR_TYPE_HUB =
31 37
sig
32 38
  type type_expr 
......
663 669
    let check_vd_env vd_env =
664 670
      ignore (List.fold_left add_vdecl [] vd_env)
665 671

  
666
    let type_spec env c =
672
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.locals in
674
      check_vd_env vd_env;
675
      let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in
676
      (* typing stmts *)
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in
678
      let undefined_vars_init =
679
        List.fold_left
680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.locals
682
      in
683
      let _ =
684
        List.fold_left
685
          (type_eq (env, vd_env) (false (*is_main*)))
686
          undefined_vars_init
687
          eqs
688
      in
689
      
667 690
      (*TODO 
668 691
        enrich env locally with locals and consts
669 692
        type each pre/post as a boolean expr
......
699 722
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
700 723
        )  nd.node_asserts;
701 724
      (* Typing spec/contracts *)
702
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec (new_env, vd_env) spec));
725
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
703 726
      (* Typing annots *)
704 727
      List.iter (fun annot ->
705 728
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
......
719 742
      Env.add_value env nd.node_id ty_node
720 743

  
721 744
    let type_imported_node env nd loc =
722
      let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
723 745
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
724 746
      check_vd_env vd_env;
725
      ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
747
      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
748
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
749
      let new_env = Env.overwrite env delta_env in
750
      (* Typing spec *)
751
      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 
726 752
      let ty_ins = type_of_vlist nd.nodei_inputs in
727 753
      let ty_outs = type_of_vlist nd.nodei_outputs in
728 754
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in

Also available in: Unified diff