support contracts in nested modules now

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/contracts@10911 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

5 files changed, 114 insertions, 39 deletions

diff --git a/bytecomp/translcore.ml b/bytecomp/translcore.ml
index 94f1f7ff82..084e7e7b03 100644
--- a/bytecomp/translcore.ml
+++ b/bytecomp/translcore.ml
@@ -553,7 +553,6 @@ let contract_failed loc pathop =
 			 Const_base(Const_int line);
 			 Const_base(Const_int char);
                          Const_base(Const_string ("Blame: " ^ func_name))]))])])
-               
 
 (* Assertions *)
 
@@ -872,7 +871,7 @@ val transl_contract: Typedtree.expression_desc ->  Typedtree.expression
 
 and transl_contract cntr e callee caller =
   let cty  = e.exp_type in
-  let mkpat id ty = { pat_desc = Tpat_var id; 
+  let mkpat desc ty = { pat_desc =  desc; 
                     pat_loc  = e.exp_loc;
                     pat_type = ty;
                     pat_env  = e.exp_env } in
@@ -887,8 +886,47 @@ and transl_contract cntr e callee caller =
        *) 
         let xe = Texp_ident (Pident x, {val_type = cty; val_kind = Val_reg}) in
         let cond = Texp_ifthenelse (p, mkexp xe cty, Some callee) in
-	Texp_let (Nonrecursive, [(mkpat x cty, e)], mkexp cond cty) 
-     | Tctr_arrow (xop, c1, c2) -> 
+	Texp_let (Nonrecursive, [(mkpat (Tpat_var x) cty, e)], mkexp cond cty) 
+       (* e |>r1,r2<| {x | p} = if (try let x = e in p
+                                    with user_defined_exn -> false
+                                         others -> raise others)
+                                then e else r1
+          This forces evaluation of e, that is, if e diverges, RHS diverges;
+          However, if e throws an exception, we still test p[e/x], which may 
+          allow certain exceptions. If p[e/x] throws exceptions, we treat it
+          as false, thus raise exception r1.
+        *)
+      (*
+        let iexp i ty = Texp_ident (Pident i, 
+                         {val_type = ty; val_kind = Val_reg}) in       
+	let letexp = Texp_let (Nonrecursive, [(mkpat (Tpat_var x) cty, e)], p) in
+        let cexn_path = Predef.path_contract_failure in
+        let cexn_ctag = Cstr_exception(cexn_path) in
+        (* This is to make up a pattern Contract(loc, pathop). Since contract checking 
+         is done after type checking, we leave cstr_args as []. *)
+        let cexn_cdesc = { cstr_res = Predef.type_exn;
+                           cstr_args = []; 
+                           cstr_arity = 2;
+                           cstr_tag = cexn_ctag;
+                           cstr_consts = 2;
+                           cstr_nonconsts = 0;
+                           cstr_private = Asttypes.Public } in
+        let dummy_type_expr = { desc = Tvar; level = 0; id =0 } in
+        let loc_id = Ident.create "l" in
+        let pathop_id = Ident.create "p" in 
+        let cpat = Tpat_construct(cexn_path, cexn_cdesc, 
+                   [mkpat (Tpat_var loc_id) dummy_type_expr; 
+                    mkpat (Tpat_var pathop_id) dummy_type_expr]) in
+        let bad_exp = Texp_bad(Blame(iexp loc_id dummy_type_expr, 
+                           iexp pathop_id dummy_type_expr)) in
+        let trycond = Texp_try(mkexp letexp Predef.type_bool,
+	    [(mkpat cpat Predef.type_exn,
+              mkexp bad_exp Predef.type_exn);
+             (mkpat Tpat_any Predef.type_exn, 
+              mkexp (Texp_constant(Const_int 0)) Predef.type_bool)]) in
+        Texp_ifthenelse (mkexp trycond Predef.type_bool, e, Some callee) 
+*)
+      | Tctr_arrow (xop, c1, c2) -> 
       (* picky version:
          <<x:c1 -> c2>> e = \x. (<<c2[(<<c1>> x)/x]>> (e (<<c1>> x)))
          lax version: 
@@ -908,14 +946,14 @@ and transl_contract cntr e callee caller =
 	     let c1x_picky = transl_contract c1 xvar caller blame_x in
 	     let c2subst = subst_contract x c1x_picky c2 in 
 	     let resfun = transl_contract c2subst (mkexp resarg c2_type) callee caller in
-	     Texp_function ([(mkpat x c1_type, resfun)], Partial)
+	     Texp_function ([(mkpat (Tpat_var x) c1_type, resfun)], Partial)
          | None -> 
 	     let x = Ident.create "c" in
              let xvar = mkexp (mkident x c1_type) c1_type in
              let c1x = transl_contract c1 xvar caller callee in
    	     let resarg = Texp_apply (e, [(Some c1x, Required)]) in
              let resfun = transl_contract c2 (mkexp resarg c2_type) callee caller in
-             Texp_function ([(mkpat x c1_type, resfun)], Partial)
+             Texp_function ([(mkpat (Tpat_var x) c1_type, resfun)], Partial)
          in res
      | Tctr_tuple cs -> 
       (* <<(c1, c2)>> e = match e with 
@@ -932,7 +970,7 @@ and transl_contract cntr e callee caller =
                                             exp_type = t;
 					    exp_env = e.exp_env
 					      } in
-		   	        (mkpat i t, exp))
+		   	        (mkpat (Tpat_var i) t, exp))
                             (List.combine new_ids typs)) in
           let ces = List.map (fun (c, ei) -> transl_contract c ei callee caller) 
 			    (List.combine cs es) in
@@ -964,9 +1002,8 @@ and subst_contract v e cntr =
 
 (* deep_transl_contract takes e and expands all ei |><| ci in e *)
 and deep_transl_contract expr = 
-     Typedtree.map_expression (fun ei -> match ei.exp_desc with
-          | Texp_contract (c, e, r1, r2) -> 
-            transl_contract c e r1 r2
+      Typedtree.map_expression (fun ei -> match ei.exp_desc with
+          | Texp_contract (c, e, r1, r2) -> transl_contract c e r1 r2
           | _ -> ei) expr
    
 
diff --git a/bytecomp/translmod.ml b/bytecomp/translmod.ml
index 4ca9978ee9..dc4d664aba 100644
--- a/bytecomp/translmod.ml
+++ b/bytecomp/translmod.ml
@@ -27,6 +27,12 @@ open Translobj
 open Translcore
 open Translclass
 
+(* naxu's temp function starts *)
+
+let fmt_contract_declaration ppf (cdecl:Types.contract_declaration) = 
+  !Oprint.out_contract_declaration ppf cdecl 
+
+(* naxu's temp function ends. *)
 
 type module_coercion = Types.module_coercion
 
@@ -343,7 +349,7 @@ and transl_structure fields cc rootpath  = function
            rebind_idents 0 fields ids)
   | Tstr_contract(decls) :: rem -> 
       transl_structure fields cc rootpath rem
-  | Tstr_mty_contracts(decls) :: rem ->
+  | Tstr_mty_contracts(tbl) :: rem ->
       transl_structure fields cc rootpath rem
   | Tstr_opened_contracts(tbl) :: rem -> 
       transl_structure fields cc rootpath rem
@@ -388,6 +394,7 @@ let wrap_id_with_contract contract_decls opened_contracts caller_pathop expr =
               requiresC (core_contract_from_iface c.Types.ttopctr_desc) 
 		        expr caller_pathop (Some callee_path) 
  	    with Not_found -> 	    
+             (* Format.fprintf Format.std_formatter "%s" (name callee_path); *)
 	      expr.exp_desc
          end
        | others -> others
@@ -513,7 +520,7 @@ and transl_contracts (str, cc) =
         match xs with
            | [] -> ([], Tbl.empty)		 
            | (Tstr_mty_contracts(t) :: rem) ->
-               let (current_contracts, mty_opened_contracts) = extract_contracts rem in
+               let (current_contracts, mty_opened_contracts) = extract_contracts rem in 
                (current_contracts, Tbl.merge t mty_opened_contracts)
 	   | (Tstr_opened_contracts(t) :: rem) ->
 	       let (current_contracts, mty_opened_contracts) = extract_contracts rem in
@@ -524,12 +531,12 @@ and transl_contracts (str, cc) =
            | (_::rem) -> extract_contracts rem
   in
   let (tstr_contracts, mty_opened_contracts) = extract_contracts str in
-  let new_tstr_contracts = List.map (fun c -> 
+  let checked_tstr_contracts = List.map (fun c -> 
                  let new_c_desc = contract_id_in_contract tstr_contracts 
 				    mty_opened_contracts (Some c.ttopctr_id)
                                     c.ttopctr_desc in
                  {c with ttopctr_desc = new_c_desc}) tstr_contracts in
-  (transl_str_contracts new_tstr_contracts mty_opened_contracts str, cc)
+  (transl_str_contracts checked_tstr_contracts mty_opened_contracts str, cc)
 
 
 
@@ -855,7 +862,7 @@ let transl_toplevel_item = function
       Llet(Strict, mid, transl_module Tcoerce_none None modl, set_idents 0 ids)
   | Tstr_contract(decls) ->
       lambda_unit
-  | Tstr_mty_contracts(decls) -> 
+  | Tstr_mty_contracts(tbl) -> 
       lambda_unit
   | Tstr_opened_contracts(tbl) ->
       lambda_unit
diff --git a/typing/env.ml b/typing/env.ml
index fb53963ebf..a118fad56f 100644
--- a/typing/env.ml
+++ b/typing/env.ml
@@ -34,8 +34,6 @@ type summary =
     Env_empty
   | Env_value of summary * Ident.t * value_description
   | Env_type of summary * Ident.t * type_declaration
-  (* Env_contract contains contracts in the current module,
-     opened contracts are kept in Tstr_opened_contracts *)
   | Env_contract of summary * Path.t * contract_declaration
   | Env_exception of summary * Ident.t * exception_declaration
   | Env_module of summary * Ident.t * module_type
diff --git a/typing/subst.ml b/typing/subst.ml
index 8c1005ff59..ed396f4028 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -282,7 +282,7 @@ let rec rename_bound_idents s idents = function
       rename_bound_idents (add_modtype id (Tmty_ident(Pident id')) s)
                           (id' :: idents) sg
   | Tsig_value(id, _) :: sg ->
-      let id' = Ident.rename id in
+      let id' = Ident.rename id in 
       rename_bound_idents (add_value id (Pident id') s) (id' :: idents) sg 
   | (Tsig_exception(id, _) | 
      Tsig_class(id, _, _) | Tsig_cltype(id, _, _)) :: sg ->
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 631a91f541..89f4f23ce3 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -232,11 +232,11 @@ and approx_sig env ssg =
       | Psig_contract cdecls -> 
 	  let typed_cdecls = Typedecl.transl_contract_decls env cdecls in
 	  let iface_cdecls = List.map Typedtree.contract_declaration_to_iface typed_cdecls in
-          let sg = List.map (fun c -> Tsig_contract (head c.Types.ttopctr_id, c, Trec_not)) 
+          let sg = List.map (fun c -> Tsig_contract (Path.head c.Types.ttopctr_id, c, Trec_not)) 
 	                    iface_cdecls in
-          (* let newenv = List.fold_right (fun (i,c) -> 
-	                  Env.enter_contract (Pident i) c) 
-	                  typed_cdecls env in *)
+          (* let newenv = List.fold_right (fun c -> 
+	                  Env.enter_contract c.Types.ttopctr_id c) 
+	                  iface_cdecls env in *)
 	  sg @ approx_sig env srem
       | _ ->
           approx_sig env srem
@@ -417,7 +417,9 @@ and transl_signature env sg =
             let rem = transl_sig env srem in
             map_rec' (fun rs (id, decl) -> 
 	                  Tsig_contract(id, decl, rs)) cdecls rem
-    in transl_sig env sg
+    in transl_sig env sg 
+
+
 
 and transl_modtype_info env sinfo =
   match sinfo with
@@ -674,6 +676,32 @@ and type_structure anchor env sstr scope =
   let type_names = ref StringSet.empty
   and module_names = ref StringSet.empty
   and modtype_names = ref StringSet.empty in
+  (* we want to put contracts in local modules in Tstr_mty_contracts(..) *)
+  let extract_contracts_from_sig id sg env1 = 
+             Env.fetch_contracts (Env.open_signature (Pident id) sg env1) in  
+  let rec extract_contracts id mty env1 = match mty with
+           | Tmty_ident(path) -> Tbl.empty
+           | Tmty_signature(sg) -> extract_contracts_from_sig id sg env1
+           | Tmty_functor(id, mty1, mty2) -> 
+              Tbl.merge (extract_contracts id mty1 env1) 
+                        (extract_contracts id mty2 env1)
+  (* it is easier for programmers to declare a contract for a function 
+     before function definition, but we can only typecheck the contract after
+     inferring the type for the function. So we re-order the sstr such that
+     the contract is after the function definition. *)
+  in 
+  let rec re_order xs = match xs with
+       | [] -> []
+       | [x] -> [x]
+       | (x::y::rem) -> begin match (x,y) with
+         | ({pstr_desc = Pstr_contract (ds)}, {pstr_desc = Pstr_open(m)}) ->
+                   x :: y :: (re_order rem)
+         | ({pstr_desc = Pstr_contract (ds1)}, {pstr_desc = Pstr_contract(ds2)}) ->
+                   re_order ({y with pstr_desc = Pstr_contract(ds1@ds2)} :: rem)
+         | ({pstr_desc = Pstr_contract (ds)}, _) -> y :: re_order (x :: rem)
+         | (_, _) -> x :: re_order (y :: rem)
+         end
+  in
   let rec type_struct env sstr =
     Ctype.init_def(Ident.current_time());
     match sstr with
@@ -728,7 +756,10 @@ and type_structure anchor env sstr scope =
            type-check contracts. Contracts are declared before function definitions,
            so type-checking of contracts occurs at 
            the end of type_structure after type_struct is called. *) 
-        type_struct env srem 
+        let contract_decls = Typedecl.transl_contract_decls env sdecls in 
+        let (str_rem, sig_rem, final_env) = type_struct env srem in
+        let newstr = (Tstr_contract contract_decls) :: str_rem in
+        (newstr, sig_rem, final_env)
     | {pstr_desc = Pstr_exception(name, sarg)} :: srem ->
         let arg = Typedecl.transl_exception env sarg in
         let (id, newenv) = Env.enter_exception name arg env in
@@ -749,7 +780,8 @@ and type_structure anchor env sstr scope =
         let mty = enrich_module_type anchor name modl.mod_type env in
         let (id, newenv) = Env.enter_module name mty env in
         let (str_rem, sig_rem, final_env) = type_struct newenv srem in
-        (Tstr_module(id, modl) :: str_rem,
+        (Tstr_module(id, modl) :: 
+         Tstr_mty_contracts(extract_contracts id mty newenv) :: str_rem,
          Tsig_module(id, modl.mod_type, Trec_not) :: sig_rem,
          final_env)
     | {pstr_desc = Pstr_recmodule sbind; pstr_loc = loc} :: srem ->
@@ -779,17 +811,9 @@ and type_structure anchor env sstr scope =
         check "module type" loc modtype_names name;
         let mty = transl_modtype env smty in
         let (id, newenv) = Env.enter_modtype name (Tmodtype_manifest mty) env in
-        let extract_contracts_from_sig sg = 
-             Env.fetch_contracts (Env.open_signature (Pident id) sg newenv) in           
-        let rec extract_contracts mty = match mty with
-           | Tmty_ident(path) -> Tbl.empty
-           | Tmty_signature(sg) -> extract_contracts_from_sig sg
-           | Tmty_functor(id, mty1, mty2) -> 
-              Tbl.merge (extract_contracts mty1) (extract_contracts mty1)
-        in
         let (str_rem, sig_rem, final_env) = type_struct newenv srem in
         (Tstr_modtype(id, mty) :: 
-         Tstr_mty_contracts(extract_contracts mty) :: str_rem,
+         Tstr_mty_contracts(extract_contracts id mty newenv) :: str_rem,
          Tsig_modtype(id, Tmodtype_manifest mty) :: sig_rem,
          final_env)
     | {pstr_desc = Pstr_open lid; pstr_loc = loc} :: srem ->
@@ -860,9 +884,17 @@ and type_structure anchor env sstr scope =
   in
   if !Clflags.annotations
   then List.iter (function {pstr_loc = l} -> Stypes.record_phrase l) sstr;
-  let (str, sg, finalenv) = type_struct env sstr in
-  (* filter out all contracts from both sstr and finalenv; 
-     type-check contracts with finalenv *)
+  let (str, sg, finalenv) = type_struct env (re_order sstr) in
+  let rec extract_typed_contracts xs = 
+           match xs with
+           | [] -> []
+           | (Tstr_contract(ds) :: rem) -> 
+	            ds@extract_typed_contracts rem 
+           | (_::rem) -> extract_typed_contracts rem
+  in 
+  (* OLD code: filter out all contracts from both sstr and finalenv; 
+     type-check contracts with finalenv. The lookup_value fetches wrong type 
+     due to shadowing if we have Pstr_open after Pstr_conract 
   let rec extract_contracts xs = 
            match xs with
            | [] -> []
@@ -871,10 +903,11 @@ and type_structure anchor env sstr scope =
   in 
   let pstr_contracts = extract_contracts sstr in
   let contract_decls = Typedecl.transl_contract_decls finalenv pstr_contracts in 
-  let newstr = (Tstr_contract contract_decls) :: str in
+  let newstr = (Tstr_contract contract_decls) :: str in *)
+  let contract_decls = extract_typed_contracts str in 
   (* In newstr2, we put opened contracts as Tstr_opened_contracts *)
   let opened_contracts = Env.fetch_contracts finalenv in
-  let newstr2 = (Tstr_opened_contracts opened_contracts) :: newstr in
+  let newstr2 = (Tstr_opened_contracts opened_contracts) :: str in
   (* put contract in .ml in inferred sig *)
   let newsg = sg @ (List.map (fun c -> 
                    Tsig_contract (Path.head c.ttopctr_id,