on force l'annotation sur le OU

affichage.ml

@@ -19,7 +19,6 @@ let rec string_of_ty = function
     let s1 = string_of_ty t1 in
     let s2 = string_of_ty t2 in
     "(" ^ s1 ^ " \\/ " ^ s2 ^ ")"
-  | Unknown -> "Unknown"
 
 let rec string_of_expr = function
   Fun ((s, t), e) ->
@@ -35,10 +34,14 @@ let rec string_of_expr = function
     "exf (" ^ s_e ^ " : " ^ s_ty ^ ")"
   | Pair (e1, e2) ->
     "("^(string_of_expr e1)^", "^(string_of_expr e2)^")"
-  | Left e ->
-    "l("^(string_of_expr e)^")"
-  | Right e ->
-    "r("^(string_of_expr e)^")"
+  | Left (e, t) ->
+    let s_e = string_of_expr e in
+    let s_ty = string_of_ty t in
+    "l (" ^ s_e ^ " : " ^ s_ty ^ ")"
+  | Right (e, t) ->
+    let s_e = string_of_expr e in
+    let s_ty = string_of_ty t in
+    "r (" ^ s_e ^ " : " ^ s_ty ^ ")"
 
 let rec string_of_hlam = function
   HFun ((s, t), e) ->
@@ -54,10 +57,14 @@ let rec string_of_hlam = function
     "exf (" ^ s_e ^ " : " ^ s_ty ^ ")"
   | HPair (e1, e2) ->
     "("^(string_of_hlam e1)^", "^(string_of_hlam e2)^")"
-  | HLeft e ->
-    "l("^(string_of_hlam e)^")"
-  | HRight e ->
-    "r("^(string_of_hlam e)^")"
+  | HLeft (e, t) ->
+    let s_e = string_of_hlam e in
+    let s_ty = string_of_ty t in
+    "l (" ^ s_e ^ " : " ^ s_ty ^ ")"
+  | HRight (e, t) ->
+    let s_e = string_of_hlam e in
+    let s_ty = string_of_ty t in
+    "r (" ^ s_e ^ " : " ^ s_ty ^ ")"
   | Ref e ->
     "{"^(string_of_hlam !e)^"}"
   | Hole -> "?"

hlam.ml

@@ -8,8 +8,8 @@ type hlam = (* hollow lam *)
   | HVar of id
   | HExf of hlam * Types.ty
   | HPair of hlam * hlam
-  | HLeft of hlam
-  | HRight of hlam
+  | HLeft of hlam * Types.ty
+  | HRight of hlam * Types.ty
   | Ref of hlam ref
   | Hole
 
@@ -22,8 +22,8 @@ let clean_hlam assoc (h : hlam) : hlam =
     | HVar s -> HVar s
     | HExf (h, t) -> HExf (clean h, t)
     | HPair (h1, h2) -> HPair (clean h1, clean h2)
-    | HLeft h -> HLeft (clean h)
-    | HRight h -> HRight (clean h)
+    | HLeft (h, t) -> HLeft (clean h, t)
+    | HRight (h, t) -> HRight (clean h, t)
     | Ref (hr) ->
       match List.assq_opt hr !assoc with
         None -> let new_h = ref (clean !hr)
@@ -49,12 +49,12 @@ let rec hlam_of_lam : lam -> hlam = function
   | Exf (e, t) ->
     let e = hlam_of_lam e in
     HExf (e, t)
-  | Pair (l1, l2) ->
-    HPair (hlam_of_lam l1, hlam_of_lam l2)
-  | Left l ->
-    HLeft (hlam_of_lam l)
-  | Right l ->
-    HRight (hlam_of_lam l)
+  | Pair (e1, e2) ->
+    HPair (hlam_of_lam e1, hlam_of_lam e2)
+  | Left (e, t) ->
+    HLeft (hlam_of_lam e, t)
+  | Right (e, t) ->
+    HRight (hlam_of_lam e, t)
 
 let rec lam_of_hlam : hlam -> lam = function
   HFun ((x, t), e) ->
@@ -68,11 +68,11 @@ let rec lam_of_hlam : hlam -> lam = function
   | HExf (e, t) ->
     let e = lam_of_hlam e in
     Exf (e, t)
-  | HPair (h1, h2) ->
-    Pair (lam_of_hlam h1, lam_of_hlam h2)
-  | HLeft h ->
-    Left (lam_of_hlam h)
-  | HRight h ->
-    Right (lam_of_hlam h)
+  | HPair (e1, e2) ->
+    Pair (lam_of_hlam e1, lam_of_hlam e2)
+  | HLeft (e, t) ->
+    Left (lam_of_hlam e, t)
+  | HRight (e, t) ->
+    Right (lam_of_hlam e, t)
   | Ref e_ref -> lam_of_hlam !e_ref
   | Hole -> raise (TacticFailed "can not translate unclosed terms")

lam.ml

@@ -8,8 +8,8 @@ type lam =
   | Var of id
   | Exf of lam * Types.ty
   | Pair of lam * lam
-  | Left of lam
-  | Right of lam
+  | Left of lam * Types.ty
+  | Right of lam * Types.ty
 
 (** alpha renaming in a deterministic way
     if readable is set to true, original variable's names are used to rename *)
@@ -33,8 +33,8 @@ let alpha_convert ?(readable=false) (e : lam) : lam =
     | Var v -> Var (get_ren_var v g)
     | Exf (e, t) -> Exf (alpha_aux e g, t)
     | Pair (e1, e2) -> Pair (alpha_aux e1 g, alpha_aux e2 g)
-    | Left e -> Left (alpha_aux e g)
-    | Right e -> Right (alpha_aux e g)
+    | Left (e, t) -> Left (alpha_aux e g, t)
+    | Right (e, t) -> Right (alpha_aux e g, t)
   in alpha_aux e []
 
 
@@ -63,8 +63,8 @@ let rec subst (m : lam) (n : lam) (x : id) : lam =
     let e1 = subst e1 n x in
     let e2 = subst e2 n x in
     Pair (e1, e2)
-  | Left e -> Left (subst e n x)
-  | Right e -> Right (subst e n x)
+  | Left (e, t) -> Left (subst e n x, t)
+  | Right (e, t) -> Right (subst e n x, t)
 
 (* INVARIANT : e has already been alpha-converted *)
 let rec betastep (e : lam) : lam option =
@@ -100,15 +100,15 @@ let rec betastep (e : lam) : lam option =
       end
     | Some e1 -> Some (Pair (e1, e2))
     end
-  | Left e ->
+  | Left (e, t) ->
     begin match betastep e with
     None -> None
-    | Some e -> Some (Left e)
+    | Some e -> Some (Left (e, t))
     end
-  | Right e ->
+  | Right (e, t) ->
     begin match betastep e with
     None -> None
-    | Some e -> Some (Right e)
+    | Some e -> Some (Right (e, t))
     end
   | Var _ -> None
   | Exf (e, t) ->

parser.mly

@@ -73,10 +73,10 @@ expression:
                             { Exf (e, t) }
   | LPAREN e1=expression COMMA e2=expression RPAREN
                             { Pair(e1, e2) }
-  | L LPAREN e=expression RPAREN
-                            { Left(e) }
-  | R LPAREN e=expression RPAREN
-                            { Right(e) }
+  | L LPAREN e=expression COLON t=ty RPAREN
+                            { Left(e, t) }
+  | R LPAREN e=expression COLON t=ty RPAREN
+                            { Right(e, t) }
   | e=app_expr              { e }
 
 app_expr:

proof.ml

@@ -199,10 +199,10 @@ let tact_right ((g, gs) : proof) : proof =
   None -> raise (TacticFailed "no current goal")
   | Some (h, goal_ty, cs) ->
     match goal_ty with
-    | Or(_, t) ->
+    | Or(_, t_r) as t ->
       let new_h = Ref (ref Hole) in
-      fill h (HRight new_h);
-      Some (new_h, t, cs), gs
+      fill h (HRight (new_h, t));
+      Some (new_h, t_r, cs), gs
     | _ -> raise (TacticFailed "Not a disjunction")
 
 let tact_left ((g, gs) : proof) : proof =
@@ -210,10 +210,10 @@ let tact_left ((g, gs) : proof) : proof =
   None -> raise (TacticFailed "no current goal")
   | Some (h, goal_ty, cs) ->
     match goal_ty with
-    | Or(t, _) ->
+    | Or(t_l, _) as t->
       let new_h = Ref (ref Hole) in
-      fill h (HLeft new_h);
-      Some (new_h, t, cs), gs
+      fill h (HLeft (new_h, t));
+      Some (new_h, t_l, cs), gs
     | _ -> raise (TacticFailed "Not a disjunction")
 
 let apply_tactic (p : proof) (t : tactic) : proof =

types.ml

@@ -6,6 +6,5 @@ type ty =
   | And of ty * ty
   | Or of ty * ty
   | Bot
-  | Unknown (* for Or *)
 
 type gam = (ty_id * ty) list

typing.ml

@@ -1,6 +1,8 @@
 open Types
 open Lam
 
+exception Could_not_infer
+
 let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool =
   match e with
   Var x -> (List.assoc x g) = expected_t
@@ -25,16 +27,17 @@ let rec typecheck (g : gam) (e : lam) (expected_t : ty) : bool =
         (typecheck g e1 t1) && (typecheck g e2 t2)
       | _ -> false
     end
-  | Left e ->
+  | Left (e, t) when t = expected_t ->
     begin match expected_t with
-      Or (t, _) -> typecheck g e t
+      Or (t_l, _) -> typecheck g e t_l
       | _ -> false
     end
-  | Right e ->
+  | Right (e, t) when t = expected_t ->
     begin match expected_t with
-      Or (_, t) -> typecheck g e t
+      Or (_, t_r) -> typecheck g e t_r
       | _ -> false
     end
+  | Left _ | Right _ -> false
 
 
 and typeinfer (g : gam) (e : lam) : ty =
@@ -49,19 +52,31 @@ and typeinfer (g : gam) (e : lam) : ty =
     Arr (t1, t2) ->
       if typecheck g e2 t1
       then t2
-      else failwith "couldn't infer"
-    | _ -> failwith "couldn't infer"
+      else  raise Could_not_infer
+    | _ ->  raise Could_not_infer
     end
   | Exf (e, t) ->
     if typecheck g e t
     then Bot
-    else failwith "couldn't infer"
+    else  raise Could_not_infer
   | Pair (e1, e2) ->
     And (
       typeinfer g e1,
       typeinfer g e2
     )
-  | Left e ->
-    Or (typeinfer g e, Unknown)
-  | Right e ->
-    Or (Unknown, typeinfer g e)
+  | Left (e, t) ->
+    begin match t with
+    Or (t_l, _) ->
+      if typecheck g e t_l
+      then t
+      else  raise Could_not_infer
+    | _ ->  raise Could_not_infer
+    end
+  | Right (e, t) ->
+    begin match t with
+    Or (_, t_r) ->
+      if typecheck g e t_r
+      then t
+      else  raise Could_not_infer
+    | _ ->  raise Could_not_infer
+    end