Add var type consistency check to e(tac)

Help/CHECK_VARTYPES_TAC.hlp

@@ -0,0 +1,22 @@
+\DOC CHECK_VARTYPES_TAC
+
+\TYPE {CHECK_VARTYPES_TAC : tactic}
+
+\SYNOPSIS
+Checks whether there are free variables in the goal with the same name
+but different types.
+
+\DESCRIBE
+Given any goal {A ?- p}, the tactic {CHECK_VARTYPES_TAC} checks whether
+there are any free variables in the conclusion and assumptions that have the
+same name but different types.
+
+{e tac} runs {CHECK_VARTYPES_TAC} after {tac} by default and detects such cases.
+
+\FAILURE
+Fails if such variables exist.
+
+\SEEALSO
+e
+
+\ENDDOC

Help/EQT_INTRO.hlp

@@ -11,7 +11,7 @@ rule, truth.
 \DESCRIBE
 {
       A |- tm
-   ---------------  EQF_INTRO
+   ---------------  EQT_INTRO
     A |- tm <=> T
 }
 

Help/e.hlp

@@ -23,7 +23,8 @@ For a description of the subgoal package, see {set_goal}.
 the tactic diverges for the goal. It will fail if there are no unproven goals.
 This could be because no goal has been set using {set_goal} or because the last
 goal set has been completely proved. It will also fail in cases when the tactic
-is invalid.
+is invalid. It will also fail if any of the resulting subgoals include free
+variables with the same name but different types ({CHECK_VARTYPES_TAC}).
 
 \EXAMPLE
 {
@@ -52,6 +53,6 @@ is invalid.
 Doing a step in an interactive goal-directed proof.
 
 \SEEALSO
-b, er, g, p, r, set_goal, top_goal, top_thm.
+b, er, g, p, r, set_goal, top_goal, top_thm, CHECK_VARTYPES_TAC.
 
 \ENDDOC

tactics.ml

@@ -922,7 +922,26 @@ let flush_goalstack() =
   let l = !current_goalstack in
   current_goalstack := [hd l];;
 
-let e tac = refine(by(VALID tac));;
+(* CHECK_VARTYPES_TAC detects whether there are variables having the same    *)
+(* name but different types.                                                 *)
+
+let CHECK_VARTYPES_TAC: tactic =
+  fun (asl,w) ->
+    let fvars_concl = freesl (w::(map (concl o snd) asl)) in
+    let fvars_dest = map dest_var fvars_concl in
+    let fvars_sorted = sort (fun (n1,_) (n2,_) -> n1 < n2) fvars_dest in
+    let rec checkfn l =
+      match l with
+      | [] -> ()
+      | h::[] -> ()
+      | (v1,ty1)::(v2,ty2)::t ->
+        if v1 = v2 && ty1 <> ty2
+        then failwith ("var " ^ v1 ^ " appearing with different types: " ^
+            (string_of_type ty1) ^ " vs. " ^ (string_of_type ty2))
+        else checkfn ((v2,ty2)::t)
+    in checkfn fvars_sorted; ALL_TAC (asl,w);;
+
+let e tac = refine(by(VALID tac THEN CHECK_VARTYPES_TAC));;
 
 let r n = refine(rotate n);;
 

unit_tests.ml

@@ -168,6 +168,17 @@ e(CONJ_TAC);;
 top_thm();;
 
 
+(* ------------------------------------------------------------------------- *)
+(* Test that e() finds same variable names with different types()            *)
+(* ------------------------------------------------------------------------- *)
+
+g `(f:num->A) (x:num) = f 1`;;
+try
+  e (SUBGOAL_THEN `x = true` ASSUME_TAC);
+  assert false;
+with Failure _ -> () | Assert_failure _ as e -> raise e;;
+
+
 (* ------------------------------------------------------------------------- *)
 (* Test functions in lib.                                                    *)
 (* ------------------------------------------------------------------------- *)