Project

General

Profile

Revision f4cba4b8 src/typing.ml

View differences:

src/typing.ml
669 669
    let check_vd_env vd_env =
670 670
      ignore (List.fold_left add_vdecl [] vd_env)
671 671

  
672
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.locals in
672
    let type_contract env c =
673
      let vd_env = c.consts @ c.locals in
674 674
      check_vd_env vd_env;
675 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 676
      (* typing stmts *)
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) c.stmts  in
678 678
      let undefined_vars_init =
679 679
        List.fold_left
680 680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.locals
681
          ISet.empty c.locals
682 682
      in
683 683
      let _ =
684 684
        List.fold_left
......
692 692
      in
693 693
      List.iter type_pred_ee
694 694
        (
695
          spec.assume 
696
          @ spec.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) 
695
          c.assume 
696
          @ c.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) c.modes) 
698 698
        );
699 699
      (*TODO 
700 700
        enrich env locally with locals and consts
......
703 703
        For the moment, returning the provided env           
704 704
       *)
705 705
      env
706
      
706

  
707
    let rec type_spec env spec loc =
708
      match spec with
709
      | Contract c -> type_contract env c
710
      | NodeSpec id -> env
711
                     
707 712
    (** [type_node env nd loc] types node [nd] in environment env. The
708 713
    location is used for error reports. *)
709
    let type_node env nd loc =
714
    and type_node env nd loc =
710 715
      let is_main = nd.node_id = !Options.main_node in
711
      let vd_env_ol = nd.node_outputs@nd.node_locals in
712
      let vd_env =  nd.node_inputs@vd_env_ol in
716
      (* In contracts, outputs are considered as input values *)
717
      let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in
718
      let vd_env =  nd.node_inputs@nd.node_outputs@nd.node_locals in
713 719
      check_vd_env vd_env;
714 720
      let init_env = env in
715 721
      let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in
......
720 726
        List.fold_left
721 727
          (fun uvs v -> ISet.add v.var_id uvs)
722 728
          ISet.empty vd_env_ol in
729
      Format.eprintf "Undef1: %a@ " pp_iset undefined_vars_init;
723 730
      let undefined_vars =
724 731
        let eqs, auts = get_node_eqs nd in
725 732
        (* TODO XXX: il faut typer les handlers de l'automate *)
726 733
        List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
727 734
      in
735
      Format.eprintf "Undef2: %a@ " pp_iset undefined_vars;
728 736
      (* Typing asserts *)
729 737
      List.iter (fun assert_ ->
730 738
          let assert_expr =  assert_.assert_expr in
731 739
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
732 740
        )  nd.node_asserts;
733 741
      (* Typing spec/contracts *)
734
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
742
      (match nd.node_spec with
743
       | None -> ()
744
       | Some spec -> ignore (type_spec new_env spec loc));
735 745
      (* Typing annots *)
736 746
      List.iter (fun annot ->
737 747
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
......
739 749
      
740 750
      (* check that table is empty *)
741 751
      let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
752
      Format.eprintf "Localconsts: %a@ " pp_iset local_consts;
742 753
      let undefined_vars = ISet.diff undefined_vars local_consts in
754
      Format.eprintf "Undef3: %a@ " pp_iset undefined_vars;
755

  
743 756
      if (not (ISet.is_empty undefined_vars)) then
744 757
        raise (Error (loc, Undefined_var undefined_vars));
745 758
      let ty_ins = type_of_vlist nd.node_inputs in
......
757 770
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
758 771
      let new_env = Env.overwrite env delta_env in
759 772
      (* Typing spec *)
760
      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 
773
      (match nd.nodei_spec with
774
       | None -> ()
775
       | Some spec -> ignore (type_spec new_env spec loc)); 
761 776
      let ty_ins = type_of_vlist nd.nodei_inputs in
762 777
      let ty_outs = type_of_vlist nd.nodei_outputs in
763 778
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
......
865 880
    let check_env_compat header declared computed = 
866 881
      uneval_prog_generics header;
867 882
      Env.iter declared (fun k decl_type_k ->
868
          let loc = (get_imported_symbol header k).top_decl_loc in 
869
          let computed_t =
870
            instantiate (ref []) (ref []) 
871
	      (try Env.lookup_value computed k
872
	       with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
873
          (*Types.print_ty Format.std_formatter decl_type_k;
874
      Types.print_ty Format.std_formatter computed_t;*)
875
          try_unify ~sub:true ~semi:true decl_type_k computed_t loc
883
          let top = get_imported_symbol header k in
884
          let loc = top.top_decl_loc in 
885
          try
886
            let computed_t = Env.lookup_value computed k in
887
            let computed_t = instantiate (ref []) (ref []) computed_t in
888
            (*Types.print_ty Format.std_formatter decl_type_k;
889
              Types.print_ty Format.std_formatter computed_t;*)                   
890
            try_unify ~sub:true ~semi:true decl_type_k computed_t loc
891
          with Not_found ->
892
            begin
893
              (* If top is a contract we do not require the lustre
894
                 file to provide the same definition. *)
895
              match top.top_decl_desc with
896
              | Node nd -> (
897
                match nd.node_spec with
898
                | Some (Contract _) -> ()
899
                | _ -> raise (Error (loc, Declared_but_undefined k))
900
              )                                                            
901
              | _ ->
902
                 raise (Error (loc, Declared_but_undefined k))
903
            end
876 904
        )
877 905

  
878 906
    let check_typedef_top decl =

Also available in: Unified diff