Revision f4cba4b8 src/typing.ml
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