WIP

typing/typer.ml

@@ -879,6 +879,9 @@ and type_check' loc env ed constr precise = match ed with
       t0 := Types.cup !t0 te;
       (ed,verify loc (Types.cap te (Types.descr t)) constr)
 
+  | Subst (e,sigma) ->
+      (ed, type_check env e constr precise)
+
   | Abstraction a ->
       let t =
         try Types.Arrow.check_strenghten a.fun_typ constr 
@@ -890,11 +893,17 @@ and type_check' loc env ed constr precise = match ed with
         | None -> env
         | Some f -> enter_value f a.fun_typ env 
       in
+      (* I check the body with all possible t1 -> t2 types *)
       List.iter (fun (t1,t2) ->
 	   let acc = a.fun_body.br_accept in 
 	   if not (Types.subtype t1 acc) then
 	     raise_loc loc (NonExhaustive (Types.diff t1 acc));
-	   ignore (type_check_branches loc env t1 a.fun_body t2 false)
+         let su = type_check_branches loc env t1 a.fun_body t2 false in
+         let sigma = (* Tallying. su t2 *) [] in
+         (* p_j : t_j -> e^j_i sigma_{H_i} *)
+         List.iter (fun br -> 
+           br.body.exp_descr <- Subst(br.body,sigma) 
+         ) a.fun_body.br_branches
 	) a.fun_iface;
       (ed,t)
 
@@ -1107,7 +1116,9 @@ and branches_aux loc env targ tres constr precise = function
         branches_aux loc env targ tres constr precise rem
       else begin
         b.br_used <- true;
-	  let res = Patterns.filter targ' p in (* t_
+	  let res = Patterns.filter targ' p in (* t_i // p_i *)
+        (* update gamma *)
+        let env = { env with gamma = IdMap.merge env.gamma res } in
 	  let res = IdMap.map Types.descr res in
 	  
 	  b.br_vars_empty <-
@@ -1115,9 +1126,10 @@ and branches_aux loc env targ tres constr precise = function
 	      IdMap.filter (fun x t -> Types.subtype t Sequence.nil_type)
 		(IdMap.restrict res b.br_vars_empty));
 
+        (* update delta *)
 	  let env' = enter_values (IdMap.get res) env in
-	  let t = type_check env' b.br_body constr precise in
-        b.br_typ <- t;
+
+	  let t = type_check env' b.br_body constr precise in (* s_i^j *)
 	  let tres = if precise then Types.cup t tres else tres in
 	  let targ'' = Types.diff targ acc in
 	  if (Types.non_empty targ'') then