tests de l'alpha équiv, commentaire de mon code

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 * Types.ty
-  | HRight of hlam * Types.ty
+  | HLeft of hlam * Types.ty (* l (M : t) *)
+  | HRight of hlam * Types.ty (* r (M : t) *)
   | Ref of hlam ref
   | Hole
 

main.ml

@@ -81,6 +81,7 @@ let check_via_coq (e : lam) (t : ty) : unit =
     then ""
     else "intro. " ^ repeat_intro (n-1)
   in
+  (* build checker.v *)
   let m = fill_ty_map StringMap.empty t in
   let (ty_vars, intro_n) = intro_of_ty m in
   let goal_ty = string_of_ty t in
@@ -120,7 +121,8 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
 
     try
       match get_instr () with
-      Cmd c -> begin match c with
+      Cmd c ->
+        begin match c with
         Goal ty ->
           let rh = Ref (ref Hole) in
           [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
@@ -132,6 +134,8 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
           | Some (h, t) ->
             let l = lam_of_hlam h
             |> beta_reduce in
+            (* uncaught Could_not_infer but won't happened
+               because exact only allow typable terms *)
             if Typing.typecheck [] l t then begin
               print_string "Ok";
               (cg, (g, gs))::sq |> interactive get_instr
@@ -144,6 +148,8 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
             end
           end
         | Check -> begin match cg with
+          (* !! Doesn't work with terms containing exfalso
+                and Left / Right !! *)
           None ->
             print_error "No current goal" "";
             (cg, (g, gs))::sq |> interactive get_instr

proof.ml

@@ -1,6 +1,6 @@
 open Hlam
 open Lam
-  open Types
+open Types
 
 type context = (id * id * hlam * Types.ty) list
 type goal = hlam * Types.ty * context
@@ -40,19 +40,16 @@ let clean_proof ((g, gs) : proof) : (hlam ref * hlam ref) list ref * proof =
     | None -> None
   in assoc, (g', List.map (clean_goal assoc) gs)
 
-let goal_is_over ((g, _) : proof) : bool =
-  match g with
-  None -> true
-  | Some _ -> false
-
+(* typecheck e t cs types e against t in the typing environment defined
+   by cs *)
 let typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
   let gam_of_ctx : context -> Types.gam =
-    let f = fun (_, var_id, _, ty) -> (var_id, ty) in
-    List.map f
+    (fun (_, var_id, _, ty) -> (var_id, ty)) |>
+    List.map
   in
   let g = gam_of_ctx cs in
   try Typing.typecheck g e expected_t
-  with _ -> raise (TacticFailed "unable to type")
+  with Typing.Could_not_infer -> raise (TacticFailed "couldn't not infer all variable types")
 
 let rec get_term_by_id (hyp : id) : context -> hlam option =
   function
@@ -71,10 +68,13 @@ let next_goal (gs : goal list) : (goal option * goal list) =
   [] -> None, []
   | g :: gs -> Some g, gs
 
-let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
-  match g with
+let get_goal : goal option -> hlam * ty * context =
+  function
   None -> raise (TacticFailed "no current goal")
-  | Some (h, expected_t, cs) ->
+  | Some g -> g
+
+let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
+  let (h, expected_t, cs) = get_goal g in
   if typecheck e expected_t cs
   then
     begin
@@ -84,9 +84,7 @@ let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
   else raise (TacticFailed "type mismatch")
 
 let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, expected_t, cs) ->
+  let (h, expected_t, cs) = get_goal g in
   match get_term_by_id hyp cs with
   Some h' ->
     if typecheck (lam_of_hlam h') expected_t cs
@@ -99,19 +97,15 @@ let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
   | None -> raise (TacticFailed "")
 
 let tact_assumption ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   match get_term_by_type goal_ty cs with
-    None -> (* failwith "assumption failed" *) (g, gs)
+  None -> raise (TacticFailed "no such hypothesis")
   | Some h' ->
     fill h h';
     next_goal gs
 
 let tact_intro ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   match goal_ty with
   Arr (t1, t2) ->
     let (hyp_id, var_id) = get_fresh_hyp () in
@@ -119,13 +113,10 @@ let tact_intro ((g, gs) : proof) : proof =
     let new_h = Ref (ref Hole) in
     fill h (HFun ((var_id, t1), new_h));
     Some (new_h, t2, cs), gs
-    | _ -> (* failwith "expected function" *) (* (g, gs) *)
-            raise (TacticFailed "expected function")
+  | _ -> raise (TacticFailed "expected an implication")
 
 let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   (* subgoal 2 : new_t -> goal_ty *)
   let arrow_h = Ref (ref Hole) in
   let arrow_goal = (arrow_h, Arr (new_t, goal_ty), cs) in
@@ -136,12 +127,19 @@ let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
   Some (new_h, new_t, cs), gs
 
 let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
+  (* check if hypothesis suits apply *)
   let rec is_implied (goal_ty : ty) (t : ty) : bool =
     match t with
     t when t = goal_ty -> true
     | Arr (_, t2) -> is_implied goal_ty t2
     | _ -> false
   in
+  (* supposes is_implied goal_ty impl_ty
+   goal_ty : conclusion of the implication
+   impl_ty : type of the implication
+   impl_h : building the term we will apply to goal_h
+   goal_h : hole of the current goal
+   h : current hole of impl_h*)
   let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
   (goal_h : hlam) (h : hlam) (cs : context) (gs : goal list) : proof =
     match impl_ty with
@@ -151,12 +149,15 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
       let _ = fill goal_h impl_h in
       Some (sub_h, t1, cs), gs
     | Arr (t1, t2) ->
-      let sub_h = Ref (ref Hole) in
-      let new_h = Ref (ref Hole) in
+      (* transforms impl_h from ((f ?x_0) ?) to (((f ?x_0) ?x_1) ?)
+      where ? is h and ?x_i are holes associated with
+      the proof of x_i*)
+      let sub_h = Ref (ref Hole) in (* proof of t1 *)
+      let new_h = Ref (ref Hole) in (* proof of t2 *)
       let _ = fill h sub_h in
       let impl_h = HApp (impl_h, new_h) in
-      let gs = (sub_h, t1, cs) :: gs in
-      generate_goals goal_ty t2 impl_h goal_h new_h cs gs
+      let gs = (sub_h, t1, cs) :: gs in (* add the proof of t1 to goals *)
+      generate_goals goal_ty t2 impl_h goal_h new_h cs gs (* generate_goals for the proof of t2 *)
     | _ -> failwith "impossible"
   in
   let rec get_hyp : context -> (hlam * ty) = function
@@ -164,9 +165,7 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
     | (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
     | _ :: cs -> get_hyp cs
   in
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (goal_h, goal_ty, cs) ->
+  let (goal_h, goal_ty, cs) = get_goal g in
   let impl_h, impl_ty = get_hyp cs in
   let new_h = Ref (ref Hole) in
   let impl_h_2 = HApp (impl_h, new_h) in
@@ -183,9 +182,7 @@ let tact_intros : proof -> proof =
   in push
 
 let tact_split ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   match goal_ty with
   | And(t1, t2) ->
     let h1 = Ref (ref Hole) in
@@ -196,9 +193,7 @@ let tact_split ((g, gs) : proof) : proof =
 
 
 let tact_right ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   match goal_ty with
   | Or(_, t_r) as t ->
     let new_h = Ref (ref Hole) in
@@ -207,9 +202,7 @@ let tact_right ((g, gs) : proof) : proof =
   | _ -> raise (TacticFailed "Not a disjunction")
 
 let tact_left ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
+  let (h, goal_ty, cs) = get_goal g in
   match goal_ty with
   | Or(t_l, _) as t->
     let new_h = Ref (ref Hole) in
@@ -231,7 +224,3 @@ let rec apply_tactic (p : proof) (t : tactic) : proof =
   | TLeft -> tact_left p
   | TTry t -> try apply_tactic p t with TacticFailed _ -> p
 
-
-let tact_try (p : proof) (t : tactic) : proof =
-  try apply_tactic p t
-  with TacticFailed _ -> p

tests/alpha_equiv/free_var_1.lam

@@ -0,0 +1 @@
+x & x

tests/alpha_equiv/free_var_2.lam

@@ -0,0 +1 @@
+x & y

tests/alpha_equiv/free_var_3.lam

@@ -0,0 +1 @@
+x (fun (y : A) => y) & x (fun (z : A) => z)

tests/alpha_equiv/not_same_but_same_order.lam

@@ -0,0 +1 @@
+(fun (x : A) => fun (y : B) => x y) & (fun (x : A) => fun (y : B) => y x)

tests/alpha_equiv/not_same_free.lam

@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (z : A) => z)

tests/alpha_equiv/same_but_different_order.lam

@@ -0,0 +1 @@
+(fun (x : A) => fun (y : B) => x y) & (fun (y : A) => fun (x : B) => y x) 

tests/alpha_equiv/same_free.lam

@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (y : A) => z)

tests/alpha_equiv/same_term_but_not_same_type.lam

@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (y : B) => z)

tests/free_or_not.lam

@@ -0,0 +1 @@
+(fun (z : A) => (fun (x : A) => z)) (fun (y : A) => z)