no need for sqlite3 anymore for IDE

experimental distance of terms dropped

configure.in

@@ -320,22 +320,22 @@ if test "$enable_ide" = yes ; then
    fi
 fi
 
-# checking for sqlite3
-if test "$enable_ide" = yes ; then
-   if test "$USEOCAMLFIND" = yes; then
-      SQLITE3LIB=$(ocamlfind query sqlite3)
-   fi
-   if test -n "$SQLITE3LIB";then
-      echo "ocamlfind found sqlite3 in $SQLITE3LIB"
-   else
-      SQLITE3LIB="+sqlite3"
-      AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
-      if test "$enable_ide" = no; then
-        AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
-   	reason_ide=" (sqlite3 not found)"
-      fi
-   fi
-fi
+dnl # checking for sqlite3
+dnl if test "$enable_ide" = yes ; then
+dnl    if test "$USEOCAMLFIND" = yes; then
+dnl       SQLITE3LIB=$(ocamlfind query sqlite3)
+dnl    fi
+dnl    if test -n "$SQLITE3LIB";then
+dnl       echo "ocamlfind found sqlite3 in $SQLITE3LIB"
+dnl    else
+dnl       SQLITE3LIB="+sqlite3"
+dnl       AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_ide=no)
+dnl       if test "$enable_ide" = no; then
+dnl         AC_MSG_WARN(Lib sqlite3 not found, IDE disabled.)
+dnl    	reason_ide=" (sqlite3 not found)"
+dnl       fi
+dnl    fi
+dnl fi
 
 # checking for sqlite3
 if test "$enable_bench" = yes ; then

examples/power/power.mlw_Power_Power_sum_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Parameter power: Z -> Z  -> Z.
+
+
+Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).
+
+Axiom Power_s : forall (x:Z) (n:Z), (0%Z <  n)%Z -> ((power x
+  n) = (x * (power x (n - 1%Z)%Z))%Z).
+
+Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).
+
+Theorem Power_sum : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z ->
+  ((0%Z <= m)%Z -> ((power x (n + m)%Z) = ((power x n) * (power x m))%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_1.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Zdiv.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
+
+Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
+
+Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
+
+Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) <  (Zabs y))%Z).
+
+Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
+
+Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x).
+
+Parameter sum_multiple_3_5_lt: Z  -> Z.
+
+
+Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
+
+Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((Zmod n 3%Z) = 0%Z)) /\
+  ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
+
+Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((Zmod n 3%Z) = 0%Z) \/
+  ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
+
+Theorem Closed_formula : forall (n:Z), (0%Z <= n)%Z -> let n3 :=
+  (Zdiv n 3%Z) in let n5 := (Zdiv n 5%Z) in let n15 := (Zdiv n 15%Z) in
+  let s :=
+  (Zdiv ((((3%Z * n3)%Z * (n3 + 1%Z)%Z)%Z + ((5%Z * n5)%Z * (n5 + 1%Z)%Z)%Z)%Z - ((15%Z * n15)%Z * (n15 + 1%Z)%Z)%Z)%Z 2%Z) in
+  (s = (sum_multiple_3_5_lt (n + 1%Z)%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+apply Zlt_lower_bound_ind.
+intros n Hind Hpos.
+assert (h: (n = 0 \/ n > 0)%Z) by omega.
+destruct h.
+(* case n=0 *)
+subst; simpl.
+rewrite Zdiv_0_l.
+replace 1%Z with (0 + 1)%Z by omega.
+rewrite SumYes; auto.
+rewrite SumEmpty; auto.
+(* case n > 0 *)
+assert (h: (n mod 3 = 0 \/ n mod 3 <> 0)%Z) by omega.
+destruct h.
+(* case n mod 3 = 0 *)
+assert (h: (n mod 5 = 0 \/ n mod 5 <> 0)%Z) by omega.
+destruct h.
+(* case n mod 3 = 0 and n mod 5 = 0 *)
+rewrite SumYes; auto.
+rewrite <- Hind; auto.
+
+SearchAbout Zdiv.
+rewrite <- (Z_div_exact_full_2 n 3).
+
+assert (h: (n mod 5 = 0 \/ n mod 5 <> 0)%Z) by omega.
+destruct h.
+   
+rewrite Zdiv0.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_2.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Zdiv.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
+
+Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
+
+Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
+
+Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) <  (Zabs y))%Z).
+
+Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
+
+Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x).
+
+Parameter sum_multiple_3_5_lt: Z  -> Z.
+
+
+Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
+
+Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((Zmod n 3%Z) = 0%Z)) /\
+  ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
+
+Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((Zmod n 3%Z) = 0%Z) \/
+  ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
+
+Axiom div_minus1_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((Zmod (x + 1%Z)%Z y) = 0%Z) ->
+  ((Zdiv (x + 1%Z)%Z y) = ((Zdiv x y) + 1%Z)%Z)).
+
+Axiom div_minus1_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((Zmod (x + 1%Z)%Z y) = 0%Z)) -> ((Zdiv (x + 1%Z)%Z y) = (Zdiv x y))).
+
+Definition closed_formula(n:Z): Z := let n3 := (Zdiv n 3%Z) in let n5 :=
+  (Zdiv n 5%Z) in let n15 := (Zdiv n 15%Z) in
+  (Zdiv ((((3%Z * n3)%Z * (n3 + 1%Z)%Z)%Z + ((5%Z * n5)%Z * (n5 + 1%Z)%Z)%Z)%Z - ((15%Z * n15)%Z * (n15 + 1%Z)%Z)%Z)%Z 2%Z).
+
+Axiom mod_15 : forall (n:Z), (0%Z <= n)%Z -> (((Zmod n 15%Z) = 0%Z) <->
+  (((Zmod n 3%Z) = 0%Z) /\ ((Zmod n 5%Z) = 0%Z))).
+
+Axiom Closed_formula_0 : ((sum_multiple_3_5_lt (0%Z + 1%Z)%Z) = (closed_formula 0%Z)).
+
+Axiom Closed_formula_n_1 : forall (n:Z), (0%Z <= n)%Z ->
+  (((closed_formula n) = (sum_multiple_3_5_lt n)) ->
+  (((~ ((Zmod n 3%Z) = 0%Z)) /\ ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)))).
+
+Axiom Closed_formula_n_2 : forall (n:Z), (0%Z <= n)%Z ->
+  (((closed_formula n) = (sum_multiple_3_5_lt n)) ->
+  ((((Zmod n 3%Z) = 0%Z) \/ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)))).
+
+Definition p(n:Z): Prop :=
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)).
+
+Axiom Induction : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
+  ((0%Z <= k)%Z /\ (k <  n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
+  (0%Z <= n)%Z -> (p n).
+
+Parameter bound:  Z.
+
+
+Axiom Induction_bound : (forall (n:Z), ((bound ) <= n)%Z -> ((forall (k:Z),
+  (((bound ) <= k)%Z /\ (k <  n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
+  ((bound ) <= n)%Z -> (p n).
+
+Theorem Closed_formula : forall (n:Z), (0%Z <= n)%Z ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (closed_formula n)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+apply Induction.
+unfold p.
+intros n Hpos Hind.
+assert (h: (n=0 \/ 0 < n)%Z) by omega.
+destruct h.
+subst; apply Closed_formula_0.
+assert (h:(Zmod n 3 = 0 \/ Zmod n 5 = 0)
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler001/euler001.mlw_SumMultiple_Closed_formula_n_1_1.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Zdiv.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
+
+Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
+
+Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
+
+Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) <  (Zabs y))%Z).
+
+Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
+
+Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x).
+
+Parameter sum_multiple_3_5_lt: Z  -> Z.
+
+
+Axiom SumEmpty : ((sum_multiple_3_5_lt 0%Z) = 0%Z).
+
+Axiom SumNo : forall (n:Z), (0%Z <= n)%Z -> (((~ ((Zmod n 3%Z) = 0%Z)) /\
+  ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = (sum_multiple_3_5_lt n))).
+
+Axiom SumYes : forall (n:Z), (0%Z <= n)%Z -> ((((Zmod n 3%Z) = 0%Z) \/
+  ((Zmod n 5%Z) = 0%Z)) ->
+  ((sum_multiple_3_5_lt (n + 1%Z)%Z) = ((sum_multiple_3_5_lt n) + n)%Z)).
+
+Axiom div_minus1_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  (((Zmod (x + 1%Z)%Z y) = 0%Z) ->
+  ((Zdiv (x + 1%Z)%Z y) = ((Zdiv x y) + 1%Z)%Z)).
+
+Axiom div_minus1_2 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((~ ((Zmod (x + 1%Z)%Z y) = 0%Z)) -> ((Zdiv (x + 1%Z)%Z y) = (Zdiv x y))).
+
+Definition closed_formula(n:Z): Z := let n3 := (Zdiv n 3%Z) in let n5 :=
+  (Zdiv n 5%Z) in let n15 := (Zdiv n 15%Z) in
+  (Zdiv ((((3%Z * n3)%Z * (n3 + 1%Z)%Z)%Z + ((5%Z * n5)%Z * (n5 + 1%Z)%Z)%Z)%Z - ((15%Z * n15)%Z * (n15 + 1%Z)%Z)%Z)%Z 2%Z).
+
+Axiom mod_15 : forall (n:Z), (0%Z <= n)%Z -> (((Zmod n 15%Z) = 0%Z) <->
+  (((Zmod n 3%Z) = 0%Z) /\ ((Zmod n 5%Z) = 0%Z))).
+
+Axiom Closed_formula_0 : ((closed_formula 0%Z) = (sum_multiple_3_5_lt 0%Z)).
+
+Theorem Closed_formula_n_1 : forall (n:Z), (0%Z <= n)%Z ->
+  (((closed_formula n) = (sum_multiple_3_5_lt n)) ->
+  (((~ ((Zmod n 3%Z) = 0%Z)) /\ ~ ((Zmod n 5%Z) = 0%Z)) ->
+  ((closed_formula (n + 1%Z)%Z) = (sum_multiple_3_5_lt (n + 1%Z)%Z)))).
+(* YOU MAY EDIT THE PROOF BELOW *)
+unfold closed_formula.
+intros n Hnpos Hind (H3,H5).
+rewrite div_minus1_2; auto with zarith.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/programs/euler002/euler002.mlw_FibOnlyEven_fib_even_1.v

+(* Beware! Only edit allowed sections below    *)
+(* This file is generated by Why3's Coq driver *)
+Require Import ZArith.
+Require Import Rbase.
+Require Import Zdiv.
+Parameter ghost : forall (a:Type), Type.
+
+Definition unit  := unit.
+
+Parameter ignore: forall (a:Type), a  -> unit.
+
+Implicit Arguments ignore.
+
+Parameter label_ : Type.
+
+Parameter at1: forall (a:Type), a -> label_  -> a.
+
+Implicit Arguments at1.
+
+Parameter old: forall (a:Type), a  -> a.
+
+Implicit Arguments old.
+
+Parameter fib: Z  -> Z.
+
+
+Axiom fib0 : ((fib 0%Z) = 1%Z).
+
+Axiom fib1 : ((fib 1%Z) = 2%Z).
+
+Axiom fibn : forall (n:Z), (2%Z <= n)%Z ->
+  ((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z).
+
+Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
+
+Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z).
+
+Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
+  ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z).
+
+Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
+  ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) <  (Zabs y))%Z).
+
+Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z).
+
+Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x).
+
+Theorem fib_even : forall (n:Z), (0%Z <= n)%Z ->
+  (((Zmod (fib n) 2%Z) = 0%Z) <-> ((Zmod n 3%Z) = 1%Z)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+apply Zlt_lower_bound_ind.
+intros n Hind Hnpos.
+assert (h: (n=0 \/ n=1 \/ n >= 2)%Z) by omega; clear Hnpos.
+destruct h as [h0|[h1|hn]].
+subst n; rewrite fib0; intuition.
+subst n; rewrite fib1; intuition.
+rewrite fibn; auto with zarith.
+rewrite Zplus_mod.
+assert (h: (0 <= (n mod 3) < 3)%Z).
+  apply Z_mod_lt; auto with zarith.
+assert (h':( n mod 3 = 0 \/ n mod 3 = 1 \/ n mod 3 = 2)%Z) 
+  by omega.
+clear h. 
+destruct h' as [h0|[h1|h2]].
+split; auto with zarith.
+  
+SearchAbout Zmod.
+assert 
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

src/core/term.ml

@@ -1253,6 +1253,32 @@ module Hterm_alpha = Hashtbl.Make (struct
   let hash = t_hash_alpha
 end)
 
+(* binder-free term/formula matching *)
+
+(* exception NoMatch *)
+
+(* let rec t_match s t1 t2 = *)
+(*   if not (oty_equal t1.t_ty t2.t_ty) then raise NoMatch else *)
+(*   match t1.t_node, t2.t_node with *)
+(*     | Tconst c1, Tconst c2 when c1 = c2 -> s *)
+(*     | Tvar v1, _ -> *)
+(*         Mvs.change v1 (function *)
+(*           | None -> Some t2 *)
+(*           | Some t1 as r when t_equal t1 t2 -> r *)
+(*           | _ -> raise NoMatch) s *)
+(*     | Tapp (s1,l1), Tapp (s2,l2) when ls_equal s1 s2 -> *)
+(*         List.fold_left2 t_match s l1 l2 *)
+(*     | Tif (f1,t1,e1), Tif (f2,t2,e2) -> *)
+(*         t_match (t_match (t_match s f1 f2) t1 t2) e1 e2 *)
+(*     | Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) when op1 = op2 -> *)
+(*         t_match (t_match s f1 f2) g1 g2 *)
+(*     | Tnot f1, Tnot f2 -> *)
+(*         t_match s f1 f2 *)
+(*     | Ttrue, Ttrue *)
+(*     | Tfalse, Tfalse -> *)
+(*         s *)
+(*     | _ -> raise NoMatch *)
+
 (* occurrence check *)
 
 let rec t_occurs r t =

src/ide/session.ml

@@ -799,6 +799,26 @@ let reload_proof obsolete goal pid old_a =
   in
   !notify_fun (Goal a.proof_goal)
 
+
+
+(*
+let reload_proof ~provers obsolete goal pid old_a =
+  try
+    let p = Util.Mstr.find pid provers in
+    let old_res = old_a.proof_state in
+    let obsolete = obsolete or old_a.proof_obsolete in
+    (* eprintf "proof_obsolete : %b@." obsolete; *)
+    let a =
+      raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
+	~edit:old_a.edited_as goal p old_res
+    in
+    !notify_fun (Goal a.proof_goal)
+  with Not_found ->
+    eprintf
+      "Warning: prover %s appears in database but is not installed.@."
+      pid
+*)
+
 let rec reload_any_goal parent gid gname sum t old_goal goal_obsolete =
   let info = get_explanation gid (Task.task_goal_fmla t) in
   let exp = match old_goal with None -> true | Some g -> g.goal_expanded in
@@ -884,6 +904,52 @@ and reload_trans  _goal_obsolete goal _ tr =
 
        new_new_goals_map = [ [ (g1, h2) ; (g2, h1) ; (g3, fresh) ; ]
 
+       TODO: use the distance Term.t_dist to obtain a better match
+
+       other solution: sort in some arbitrary total order
+
+       g1 < g2 < ... <
+
+       h1 < h2 < ... <
+
+       then identical goals can be detected by a merge_like algorithm :
+
+       if merged list starts with g :
+
+       g1 < ... gk <= h1 < ... < 
+
+       then g1 .. g{k-1} are new and gk associated to h1, and then 
+       recursively merge g{k+1} ... and h2 ...
+
+       otherwise, list starts
+
+       h1 < ... hk <= g1 <= ... < 
+
+       ....
+
+       Another formulation :
+
+       if merged list starts with
+       
+       1) g1 g2 ... 
+       
+       associate g1 to nothing and recursively process g2 ...
+
+       2) g1 h1 g2 ... with d(g1,h1) < d(h1,g2)
+
+       associate g1 to h1 and recursively process g2 ...
+
+       3) g1 h1 g2 ... with d(g1,h1) > d(h1,g2)
+       
+       ?
+
+       4) g1 h1 h2 ...
+
+       
+       PRELIMINARY: store the shape of the conclusion of the goal in the XML
+       file. 
+
+
     *)
     let rec associate_remaining_goals new_goals_map remaining acc =
       match new_goals_map with

src/ide/termcode.ml

+(* distance of two terms *)
+
+let dist_bool b = if b then 0.0 else 1.0
+
+let average l =
+  let n,s = List.fold_left (fun (n,s) x -> (n+1,s+.x)) (0,0.0) l in
+  float n *. s
+
+let rec pat_dist p1 p2 =
+  if ty_equal p1.pat_ty p2.pat_ty then
+    match p1.pat_node, p2.pat_node with
+      | Pwild, Pwild | Pvar _, Pvar _ -> 0.0
+      | Papp (f1, l1), Papp (f2, l2) ->
+	  if ls_equal f1 f2 then
+	    0.5 *. average (List.map2 pat_dist l1 l2)
+	  else 1.0
+      | Pas (p1, _), Pas (p2, _) -> pat_dist p1 p2
+      | Por (p1, q1), Por (p2, q2) ->
+	  0.5 *. average [pat_dist p1 p2 ; pat_dist q1 q2 ]
+      | _ -> 1.0
+  else 1.0
+
+let rec t_dist c1 c2 m1 m2 e1 e2 = 
+  let t_d = t_dist c1 c2 m1 m2 in
+  match e1.t_node, e2.t_node with
+    | Tvar v1, Tvar v2 -> 
+	begin 
+	  try dist_bool (Mvs.find v1 m1 = Mvs.find v2 m2)
+	  with Not_found -> 1.0
+	end
+    | Tconst c1, Tconst c2 -> 0.5 *. dist_bool (c1 = c2)
+    | Tapp(ls1,tl1), Tapp(ls2,tl2) ->
+	if ls_equal ls1 ls2 then
+	  0.5 *. average (List.map2 t_d tl1 tl2)
+	else 1.0 
+    | Tif(c1,t1,e1), Tif(c2,t2,e2) ->
+	0.5 *. average [t_d c1 c2 ; t_d t1 t2 ; t_d e1 e2]
+    | Tlet(t1,b1), Tlet(t2,b2) ->
+        let u1,e1 = t_open_bound b1 in
+        let u2,e2 = t_open_bound b2 in
+        let m1 = vs_rename_alpha c1 m1 u1 in
+        let m2 = vs_rename_alpha c2 m2 u2 in
+        0.5 *. average [t_d t1 t2; t_dist c1 c2 m1 m2 e1 e2]
+    | Tcase (t1,bl1), Tcase (t2,bl2) ->
+	if List.length bl1 = List.length bl2 then
+          let br_dist ((pat1,_,_) as b1) ((pat2,_,_) as b2) =
+            let p1,e1 = t_open_branch b1 in
+            let p2,e2 = t_open_branch b2 in
+            let m1 = pat_rename_alpha c1 m1 p1 in
+            let m2 = pat_rename_alpha c2 m2 p2 in
+            average [pat_dist pat1 pat2 ; t_dist c1 c2 m1 m2 e1 e2]
+          in
+          0.5 *. average (t_d t1 t2 :: List.map2 br_dist bl1 bl2)
+	else
+	  1.0
+    | Teps b1, Teps b2 ->
+        let u1,e1 = t_open_bound b1 in
+        let u2,e2 = t_open_bound b2 in
+        let m1 = vs_rename_alpha c1 m1 u1 in
+        let m2 = vs_rename_alpha c2 m2 u2 in
+        0.5 *. t_dist c1 c2 m1 m2 e1 e2
+    | Tquant (q1,((vl1,_,_,_) as b1)), Tquant (q2,((vl2,_,_,_) as b2)) ->
+        if q1 = q2 &&
+          list_all2 (fun v1 v2 -> ty_equal v1.vs_ty v2.vs_ty) vl1 vl2 
+	then
+          let vl1,_,e1 = t_open_quant b1 in
+          let vl2,_,e2 = t_open_quant b2 in
+          let m1 = vl_rename_alpha c1 m1 vl1 in
+          let m2 = vl_rename_alpha c2 m2 vl2 in
+          0.5 *. t_dist c1 c2 m1 m2 e1 e2
+	else
+	  1.0
+    | Tbinop (a,f1,g1), Tbinop (b,f2,g2) ->
+        if a = b then 0.5 *. average [ t_d f1 f2 ; t_d g1 g2]
+	else 1.0
+    | Tnot f1, Tnot f2 -> 0.5 *. t_d f1 f2
+    | Ttrue, Ttrue | Tfalse, Tfalse -> 0.0
+    | _ -> 1.0
+
+
+let t_dist t1 t2 = t_dist (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty t1 t2
+
+(* similarity code of terms, or of "shapes" 
+
+example: 
+
+  shape(forall x:int, x * x >= 0) =
+         Forall(Int,App(infix_gteq,App(infix_st,Tvar 0,Tvar 0),Const(0)))
+       i.e: de bruijn indexes, first-order term
+
+ code of a shape: maps shapes into real numbers in [0..1], such that 
+
+        compare t1 t2 = code (shape t1) -. code (shape t2)
+
+       is a good comparison operator
+
+       code(n:int) = 1 / (1+abs(n))
+            so code(0) = 1, code(1) = 0.5, 
+
+       code(x:real) = 1 / (1+abs x)
+
+       code(ConstInt n) = h (n) / 3
+       code(ConstReal x) = (2 + h (x)) / 3
+
+       more generally, for any type t = C0 x | ... | Cn x
+           code(Ci x) = (2i + h(x)) / (2n+1)
+         
+*)
+
+
+    
+