Fixing Pervasives.equality in extraction.

4 files changed, 129 insertions, 33 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 53bb53606f..135d3fc7cd 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -118,6 +118,17 @@ let uppercase_id id =
 
 type kind = Term | Type | Cons | Mod
 
+module KOrd =
+struct
+  type t = kind * string
+  let compare (k1, s1) (k2, s2) =
+    let c = Pervasives.compare k1 k2 (** OK *) in
+    if c = 0 then String.compare s1 s2
+    else c
+end
+
+module KMap = Map.Make(KOrd)
+
 let upperkind = function
   | Type -> lang () == Haskell
   | Term -> false
@@ -191,25 +202,32 @@ let add_global_ids, get_global_ids =
 
 let empty_env () = [], get_global_ids ()
 
-let mktable autoclean =
-  let h = Hashtbl.create 97 in
-  if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
-  (Hashtbl.replace h, Hashtbl.find h, fun () -> Hashtbl.clear h)
-
 (* We might have built [global_reference] whose canonical part is
    inaccurate. We must hence compare only the user part,
    hence using a Hashtbl might be incorrect *)
 
+let mktable_id autoclean =
+  let m = ref Id.Map.empty in
+  let clear () = m := Id.Map.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := Id.Map.add r v !m), (fun r -> Id.Map.find r !m), clear
+
 let mktable_ref autoclean =
   let m = ref Refmap'.empty in
   let clear () = m := Refmap'.empty in
   if autoclean then register_cleanup clear;
   (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
 
+let mktable_modpath autoclean =
+  let m = ref MPmap.empty in
+  let clear () = m := MPmap.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := MPmap.add r v !m), (fun r -> MPmap.find r !m), clear
+
 (* A table recording objects in the first level of all MPfile *)
 
 let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
-  mktable false
+  mktable_modpath false
 
 let get_mpfiles_content mp =
   try get_mpfiles_content mp
@@ -255,7 +273,7 @@ let params_ren_add, params_ren_mem =
 
 type visible_layer = { mp : module_path;
 		       params : module_path list;
-		       content : ((kind*string),Label.t) Hashtbl.t }
+		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
   let vis = ref [] in
@@ -269,14 +287,16 @@ let pop_visible, push_visible, get_visible =
 	  if get_phase () == Impl && modular () && is_modfile v.mp
 	  then add_mpfiles_content v.mp v.content
   and push mp mps =
-    vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
+    vis := { mp = mp; params = mps; content = KMap.empty } :: !vis
   and get () = !vis
   in (pop,push,get)
 
 let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
 let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
 let top_visible_mp () = (top_visible ()).mp
-let add_visible ks l = Hashtbl.add (top_visible ()).content ks l
+let add_visible ks l =
+  let visible = top_visible () in
+  visible.content <- KMap.add ks l visible.content
 
 (* table of local module wrappers used to provide non-ambiguous names *)
 
@@ -328,7 +348,7 @@ let modular_rename k id =
     with unique numbers *)
 
 let modfstlev_rename =
-  let add_prefixes,get_prefixes,_ = mktable true in
+  let add_prefixes,get_prefixes,_ = mktable_id true in
   fun l ->
     let coqid = Id.of_string "Coq" in
     let id = Label.to_id l in
@@ -369,7 +389,7 @@ let rec mp_renaming_fun mp = match mp with
 (* ... and its version using a cache *)
 
 and mp_renaming =
-  let add,get,_ = mktable true in
+  let add,get,_ = mktable_modpath true in
   fun x ->
     try if is_mp_bound (base_mp x) then raise Not_found; get x
     with Not_found -> let y = mp_renaming_fun x in add x y; y
@@ -414,7 +434,7 @@ let rec clash mem mp0 ks = function
   | _ :: mpl -> clash mem mp0 ks mpl
 
 let mpfiles_clash mp0 ks =
-  clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
+  clash (fun mp k -> KMap.mem k (get_mpfiles_content mp)) mp0 ks
     (List.rev (mpfiles_list ()))
 
 let rec params_lookup mp0 ks = function
@@ -432,7 +452,7 @@ let visible_clash mp0 ks =
     | [] -> false
     | v :: _ when ModPath.equal v.mp mp0 -> false
     | v :: vis ->
-	let b = Hashtbl.mem v.content ks in
+	let b = KMap.mem ks v.content in
 	if b && not (is_mp_bound mp0) then true
 	else begin
 	  if b then params_ren_add mp0;
@@ -448,7 +468,7 @@ let visible_clash_dbg mp0 ks =
     | [] -> None
     | v :: _ when ModPath.equal v.mp mp0 -> None
     | v :: vis ->
-	try Some (v.mp,Hashtbl.find v.content ks)
+	try Some (v.mp,KMap.find ks v.content)
 	with Not_found ->
 	  if params_lookup mp0 ks v.params then None
 	  else clash vis
@@ -468,7 +488,7 @@ let opened_libraries () =
     let to_open =
       List.filter
 	(fun mp ->
-	   not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
+	   not (List.exists (fun k -> KMap.mem k (get_mpfiles_content mp)) used_ks))
 	used_files
     in
     mpfiles_clear ();
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 134e01ee1f..3927ad3283 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -206,8 +206,13 @@ let oib_equal o1 o2 =
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
     Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
       eq_constr c1 c2 && Sorts.equal s1 s2
-  | ma1, ma2 -> Pervasives.(=) ma1 ma2 (** FIXME: this one is surely wrong *) end &&
-    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
+  | Polymorphic p1, Polymorphic p2 ->
+    let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in
+    List.equal eq p1.poly_param_levels p2.poly_param_levels &&
+    Univ.Universe.equal p1.poly_level p2.poly_level
+  | Monomorphic _, Polymorphic _ | Polymorphic _, Monomorphic _ -> false
+  end &&
+  Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
@@ -218,7 +223,7 @@ let mib_equal m1 m2 =
   Int.equal m1.mind_nparams m2.mind_nparams &&
   Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
   List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  Pervasives.(=) m1.mind_constraints m2.mind_constraints (** FIXME *)
+  Univ.eq_constraint m1.mind_constraints m2.mind_constraints
 
 (*S Extraction of a type. *)
 
@@ -292,7 +297,7 @@ let rec extract_type env db j c args =
 		      (* The more precise is [mlt'], extracted after reduction *)
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if Pervasives.(=) (expand env mlt) (expand env mlt') then mlt else mlt') (** FIXME *)
+		      if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt')
 	   | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
 	       (match cb.const_body with
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 22e7080e14..1a4cfb45fa 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -53,6 +53,22 @@ let new_meta _ =
   incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
+let rec eq_ml_type t1 t2 = match t1, t2 with
+| Tarr (tl1, tr1), Tarr (tl2, tr2) ->
+  eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
+| Tglob (gr1, t1), Tglob (gr2, t2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+| Tvar i1, Tvar i2 -> Int.equal i1 i2
+| Tvar' i1, Tvar' i2 -> Int.equal i1 i2
+| Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
+| Tdummy k1, Tdummy k2 -> k1 == k2
+| Tunknown, Tunknown -> true
+| Taxiom, Taxiom -> true
+| _ -> false
+
+and eq_ml_meta m1 m2 =
+ Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
+
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
 let type_subst_list l t =
@@ -342,6 +358,54 @@ let type_expunge env t =
 
 let mlapp f a = if List.is_empty a then f else MLapp (f,a)
 
+(** Equality *)
+
+let eq_ml_ident i1 i2 = match i1, i2 with
+| Dummy, Dummy -> true
+| Id id1, Id id2 -> Id.equal id1 id2
+| Tmp id1, Tmp id2 -> Id.equal id1 id2
+| _ -> false
+
+let rec eq_ml_ast t1 t2 = match t1, t2 with
+| MLrel i1, MLrel i2 ->
+  Int.equal i1 i2
+| MLapp (f1, t1), MLapp (f2, t2) ->
+  eq_ml_ast f1 f2 && List.equal eq_ml_ast t1 t2
+| MLlam (na1, t1), MLlam (na2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast t1 t2
+| MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
+| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
+  eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+| MLtuple t1, MLtuple t2 ->
+  List.equal eq_ml_ast t1 t2
+| MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
+  eq_ml_type t1 t2 && eq_ml_ast c1 c2 && Array.equal eq_ml_branch p1 p2
+| MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
+  Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
+| MLexn e1, MLexn e2 -> String.equal e1 e2
+| MLdummy, MLdummy -> true
+| MLaxiom, MLaxiom -> true
+| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
+| _ -> false
+
+and eq_ml_pattern p1 p2 = match p1, p2 with
+| Pcons (gr1, p1), Pcons (gr2, p2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+| Ptuple p1, Ptuple p2 ->
+  List.equal eq_ml_pattern p1 p2
+| Prel i1, Prel i2 ->
+  Int.equal i1 i2
+| Pwild, Pwild -> true
+| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| _ -> false
+
+and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
+  List.equal eq_ml_ident id1 id2 &&
+  eq_ml_pattern p1 p2 &&
+  eq_ml_ast t1 t2
+
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
 
@@ -708,7 +772,7 @@ let branch_as_fun typ (l,p,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons _ as cons' when Pervasives.(=) cons' (ast_lift n cons) -> MLrel (n+1) (*FIXME*)
+    | MLcons _ as cons' when eq_ml_ast cons' (ast_lift n cons) -> MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
@@ -737,22 +801,28 @@ let branch_as_cst (l,_,c) =
    element and its positions. *)
 
 let census_add, census_max, census_clean =
-  let h = Hashtbl.create 13 in
-  let clear () = Hashtbl.clear h in
-  let add e i =
-    let s = try Hashtbl.find h e with Not_found -> Int.Set.empty in
-    Hashtbl.replace h e (Int.Set.add i s)
+  let h = ref [] in
+  let clearf () = h := [] in
+  let rec add k v = function
+  | [] -> raise Not_found
+  | (k', s) as p :: l ->
+    if eq_ml_ast k k' then (k', Int.Set.add v s) :: l
+    else p :: add k v l
+  in
+  let addf k i =
+    try h := add k i !h
+    with Not_found -> h := (k, Int.Set.singleton i) :: !h
   in
-  let max e0 =
-    let len = ref 0 and lst = ref Int.Set.empty and elm = ref e0 in
-    Hashtbl.iter
-      (fun e s ->
+  let maxf k =
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+    List.iter
+      (fun (e, s) ->
 	 let n = Int.Set.cardinal s in
 	 if n > !len then begin len := n; lst := s; elm := e end)
-      h;
+      !h;
     (!elm,!lst)
   in
-  (add,max,clear)
+  (addf,maxf,clearf)
 
 (* [factor_branches] return the longest possible list of branches
    that have the same factorization, either as a function or as a
@@ -1142,7 +1212,7 @@ let normalize a =
   let o = optims () in
   let rec norm a =
     let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
-    if Pervasives.(=) a a' then a else norm a' (** FIXME *)
+    if eq_ml_ast a a' then a else norm a'
   in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1257,7 +1327,7 @@ let rec non_stricts add cand = function
 	   let n = List.length i in
 	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
-	   List.merge Pervasives.compare cand c) [] v
+	   List.merge Int.compare cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index bd8d549a21..f25f0bb89d 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -67,6 +67,7 @@ val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
 val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type
 
+val eq_ml_type : ml_type -> ml_type -> bool
 val isDummy : ml_type -> bool
 val isKill : sign -> bool