improved error msg reporting for dependent function contracts

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

2 files changed, 66 insertions, 27 deletions

diff --git a/bytecomp/translcore.ml b/bytecomp/translcore.ml
index 084e7e7b03..5b91064c57 100644
--- a/bytecomp/translcore.ml
+++ b/bytecomp/translcore.ml
@@ -884,12 +884,14 @@ and transl_contract cntr e callee caller =
           This forces evaluation of e, that is, if e diverges, RHS diverges;
           if e crashes, RHS crashes 
        *) 
+       
         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 (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)
+                                    with contract_exn -> raise 
+                                         _ -> false)
                                 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 
@@ -917,20 +919,20 @@ and transl_contract cntr e callee caller =
         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 raise_contract_exn = 
+             Texp_apply (Texp_ident( 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) -> 
+      *)
+     | Tctr_arrow (xop, c1, c2) -> 
       (* picky version:
-         <<x:c1 -> c2>> e = \x. (<<c2[(<<c1>> x)/x]>> (e (<<c1>> x)))
+         e |>r1,r2<| x:c1 -> c2 = \x. (e (x |>r2,r1<| c1)) |>r1,r2<| c2[(x |>r2,r1<| c1)/x]
          lax version: 
-         <<x:c1 -> c2>> e = \x. (<<c2>> (e (<<c1>> x))) 
+         e |>r1,r2<| x:c1 -> c2 = \x. (e (x |>r2,r1<| c1)) |>r1,r2<| c2
          we are implementing the picky version. *)      
          let c1_type = c1.contract_type in
          let c2_type = c2.contract_type in
@@ -941,11 +943,20 @@ and transl_contract cntr e callee caller =
 	     let resarg = Texp_apply (e, [(Some c1x, Required)]) in
               (* e.g. x:({a | a > 0} -> {b | true}) -> {c | x 0 > c} 
                  we want to blame the x in {c | x 0 > c} 
-  	      *)
-	     let blame_x = mkexp (Texp_bad (Blame (c2.contract_loc, None))) cty in
-	     let c1x_picky = transl_contract c1 xvar caller blame_x in
+                 This is done in translmod.ml now because it can give more
+                 previse caller-location-to-be-blamed.  
+  	     
+             let callee_path = match callee.exp_desc with
+                             | Texp_bad (Blame (loc, pathopt)) -> pathopt
+                             | Texp_unr (Blame (loc, pathopt)) -> pathopt
+                             | _ -> None
+             in
+	     let blame_x = mkexp (Texp_bad (Blame (x.exp_loc, callee_path))) cty in
+	      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
+             *)
+	     let resfun = transl_contract c2 (mkexp resarg c2_type) callee caller in
 	     Texp_function ([(mkpat (Tpat_var x) c1_type, resfun)], Partial)
          | None -> 
 	     let x = Ident.create "c" in
diff --git a/bytecomp/translmod.ml b/bytecomp/translmod.ml
index dc4d664aba..2f24c33e8b 100644
--- a/bytecomp/translmod.ml
+++ b/bytecomp/translmod.ml
@@ -381,19 +381,34 @@ let rec print_list ppf l =
    | (y::ys) -> Printtyp.path ppf y; 
                 print_list ppf ys
 
-let wrap_id_with_contract contract_decls opened_contracts caller_pathop expr = 
+(* local_fun_contracts contains x:t1 in contract x:t1 -> t2.
+   contract_decls contains contract declaration in the current module
+       contract f = {...} -> {...}
+   opened_contracts contains contracts from open ... and 
+   contracts exported from nested modules.
+*)
+let wrap_id_with_contract local_fun_contracts contract_decls opened_contracts 
+            caller_pathop expr = 
   let contracted_exp_desc = match expr.exp_desc with
        | Texp_ident (callee_path, value_desc) -> 
          begin
+          try (* lookup for dependent contract first *)
+           let id = match callee_path with
+                     | Pident(i) -> i
+                     | _ -> raise Not_found
+           in
+           let c = Ident.find_same id local_fun_contracts in
+           requiresC c expr caller_pathop (Some callee_path)                
+          with Not_found -> 
           try (* lookup for contracts in current module *)
            let c = fetch_contract_by_path callee_path contract_decls in
            requiresC c.ttopctr_desc expr caller_pathop (Some callee_path) 
           with Not_found -> 
-	    try (* lookup for contracts in opened modules *)
-	      let c = Tbl.generic_find Path.cmpPath_byname callee_path opened_contracts in 
-              requiresC (core_contract_from_iface c.Types.ttopctr_desc) 
+	  try (* lookup for contracts in opened modules *)
+	   let c = Tbl.generic_find Path.cmpPath_byname callee_path opened_contracts in 
+             requiresC (core_contract_from_iface c.Types.ttopctr_desc) 
 		        expr caller_pathop (Some callee_path) 
- 	    with Not_found -> 	    
+ 	  with Not_found -> 	    
              (* Format.fprintf Format.std_formatter "%s" (name callee_path); *)
 	      expr.exp_desc
          end
@@ -408,8 +423,10 @@ val contract_id_in_expr: core_contract list ->
                          Path.t option -> 
                          expression -> expression
 *)
-let contract_id_in_expr contract_decls opened_contracts caller_pathop expr = 
-    map_expression (wrap_id_with_contract contract_decls 
+let contract_id_in_expr local_fun_contracts contract_decls opened_contracts 
+                        caller_pathop expr = 
+    map_expression (wrap_id_with_contract local_fun_contracts
+                                          contract_decls 
 		                          opened_contracts 
 		                          caller_pathop) expr    
 
@@ -427,21 +444,28 @@ val contract_id_in_contract: core_contract list ->
                          core_contract -> core_contract
 
 *)
-let rec contract_id_in_contract contract_decls opened_contracts caller_pathop c = 
+let rec contract_id_in_contract local_fun_contracts contract_decls opened_contracts 
+                                caller_pathop c = 
   let new_desc = match c.contract_desc with
 	  | Tctr_pred (id, e) -> 
-              let ce = contract_id_in_expr contract_decls opened_contracts
-                                                 caller_pathop e in
+              let ce = contract_id_in_expr local_fun_contracts 
+                                           contract_decls 
+                                           opened_contracts
+                                           caller_pathop e in
               let expanded_ce = deep_transl_contract ce in
               Tctr_pred (id, expanded_ce)
           | Tctr_arrow (idopt, c1, c2) -> 
-	      let new_c1 = contract_id_in_contract contract_decls 
+	      let new_c1 = contract_id_in_contract local_fun_contracts contract_decls 
                                    opened_contracts caller_pathop c1 in
-	      let new_c2 = contract_id_in_contract contract_decls 
+              let new_local = match idopt with 
+                              | Some (id) -> Ident.add id c1 local_fun_contracts
+                              | None -> local_fun_contracts               
+              in
+	      let new_c2 = contract_id_in_contract new_local contract_decls 
                                    opened_contracts caller_pathop c2 in
               Tctr_arrow (idopt, new_c1, new_c2)
           | Tctr_tuple (cs) -> 
-              Tctr_tuple (List.map (fun c -> contract_id_in_contract 
+              Tctr_tuple (List.map (fun c -> contract_id_in_contract local_fun_contracts
 			   contract_decls opened_contracts caller_pathop c) cs)
   in {c with contract_desc = new_desc}
 
@@ -456,7 +480,8 @@ let rec transl_str_contracts contract_decls opened_contracts strs =
                        | Tpat_var p -> Some (Pident p)
                        | others -> None
        in
-       let cexpr = contract_id_in_expr contract_decls 
+       let cexpr = contract_id_in_expr Ident.empty 
+                                       contract_decls 
 	                               opened_contracts
 	                               fpathop expr in 
        let expanded_cexpr = deep_transl_contract  cexpr in 
@@ -532,8 +557,11 @@ and transl_contracts (str, cc) =
   in
   let (tstr_contracts, mty_opened_contracts) = extract_contracts str in
   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)
+                 let new_c_desc = contract_id_in_contract 
+                                    Ident.empty
+                                    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 checked_tstr_contracts mty_opened_contracts str, cc)