From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/common.ml | 80 ++++++++++++++++++++++++-------------------- 1 file changed, 43 insertions(+), 37 deletions(-) (limited to 'plugins/extraction/common.ml') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index dbd280a1e..53bb53606 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -20,7 +20,7 @@ open Mlutil let string_of_id id = let s = Names.Id.to_string id in for i = 0 to String.length s - 2 do - if s.[i] = '_' && s.[i+1] = '_' then warning_id s + if s.[i] == '_' && s.[i+1] == '_' then warning_id s done; Unicode.ascii_of_ident s @@ -39,7 +39,7 @@ let pp_apply st par args = match args with (** Same as [pp_apply], but with also protection of the head by parenthesis *) let pp_apply2 st par args = - let par' = args <> [] || par in + let par' = not (List.is_empty args) || par in pp_apply (pp_par par' st) par args let pr_binding = function @@ -79,20 +79,20 @@ let is_digit = function let begins_with_CoqXX s = let n = String.length s in - n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' && + n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' && let i = ref 3 in try while !i < n do - if s.[!i] = '_' then i:=n (*Stop*) + if s.[!i] == '_' then i:=n (*Stop*) else if is_digit s.[!i] then incr i else raise Not_found done; true with Not_found -> false let unquote s = - if lang () <> Scheme then s + if lang () != Scheme then s else let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; + for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done; s let rec qualify delim = function @@ -112,14 +112,14 @@ let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id)) let uppercase_id id = let s = string_of_id id in - assert (s<>""); - if s.[0] = '_' then Id.of_string ("Coq_"^s) + assert (not (String.is_empty s)); + if s.[0] == '_' then Id.of_string ("Coq_"^s) else Id.of_string (String.capitalize s) type kind = Term | Type | Cons | Mod let upperkind = function - | Type -> lang () = Haskell + | Type -> lang () == Haskell | Term -> false | Cons | Mod -> true @@ -162,7 +162,7 @@ let push_vars ids (db,avoid) = let get_db_name n (db,_) = let id = List.nth db (pred n) in - if id = dummy_name then Id.of_string "__" else id + if Id.equal id dummy_name then Id.of_string "__" else id (*S Renamings of global objects. *) @@ -266,7 +266,7 @@ let pop_visible, push_visible, get_visible = | v :: vl -> vis := vl; (* we save the 1st-level-content of MPfile for later use *) - if get_phase () = Impl && modular () && is_modfile v.mp + 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 @@ -285,7 +285,7 @@ struct type t = ModPath.t * Label.t let compare (mp1, l1) (mp2, l2) = let c = Label.compare l1 l2 in - if c = 0 then ModPath.compare mp1 mp2 else c + if Int.equal c 0 then ModPath.compare mp1 mp2 else c end module DupMap = Map.Make(DupOrd) @@ -304,7 +304,7 @@ type reset_kind = AllButExternal | Everything let reset_renaming_tables flag = do_cleanup (); - if flag = Everything then clear_mpfiles_content () + if flag == Everything then clear_mpfiles_content () (*S Renaming functions *) @@ -320,7 +320,7 @@ let modular_rename k id = in if not (is_ok s) || (Id.Set.mem id (get_keywords ())) || - (String.length s >= 4 && String.sub s 0 4 = prefix) + (String.length s >= 4 && String.equal (String.sub s 0 4) prefix) then prefix ^ s else s @@ -350,17 +350,20 @@ let rec mp_renaming_fun mp = match mp with | _ when not (modular ()) && at_toplevel mp -> [""] | MPdot (mp,l) -> let lmp = mp_renaming mp in - if lmp = [""] then (modfstlev_rename l)::lmp - else (modular_rename Mod (Label.to_id l))::lmp + let mp = match lmp with + | [""] -> modfstlev_rename l + | _ -> modular_rename Mod (Label.to_id l) + in + mp ::lmp | MPbound mbid -> let s = modular_rename Mod (MBId.to_id mbid) in if not (params_ren_mem mp) then [s] else let i,_,_ = MBId.repr mbid in [s^"__"^string_of_int i] | MPfile _ -> assert (modular ()); (* see [at_toplevel] above *) - assert (get_phase () = Pre); + assert (get_phase () == Pre); let current_mpfile = (List.last (get_visible ())).mp in - if mp <> current_mpfile then mpfiles_add mp; + if not (ModPath.equal mp current_mpfile) then mpfiles_add mp; [string_of_modfile mp] (* ... and its version using a cache *) @@ -377,15 +380,15 @@ and mp_renaming = let ref_renaming_fun (k,r) = let mp = modpath_of_r r in let l = mp_renaming mp in - let l = if lang () <> Ocaml && not (modular ()) then [""] else l in + let l = if lang () != Ocaml && not (modular ()) then [""] else l in let s = let idg = safe_basename_of_global r in - if l = [""] (* this happens only at toplevel of the monolithic case *) - then + match l with + | [""] -> (* this happens only at toplevel of the monolithic case *) let globs = Id.Set.elements (get_global_ids ()) in let id = next_ident_away (kindcase_id k idg) globs in string_of_id id - else modular_rename k idg + | _ -> modular_rename k idg in add_global_ids (Id.of_string s); s::l @@ -406,7 +409,7 @@ let ref_renaming = let rec clash mem mp0 ks = function | [] -> false - | mp :: _ when mp = mp0 -> false + | mp :: _ when ModPath.equal mp mp0 -> false | mp :: _ when mem mp ks -> true | _ :: mpl -> clash mem mp0 ks mpl @@ -416,15 +419,18 @@ let mpfiles_clash mp0 ks = let rec params_lookup mp0 ks = function | [] -> false - | param :: _ when mp0 = param -> true + | param :: _ when ModPath.equal mp0 param -> true | param :: params -> - if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param; + let () = match ks with + | (Mod, mp) when String.equal (List.hd (mp_renaming param)) mp -> params_ren_add param + | _ -> () + in params_lookup mp0 ks params let visible_clash mp0 ks = let rec clash = function | [] -> false - | v :: _ when v.mp = mp0 -> false + | v :: _ when ModPath.equal v.mp mp0 -> false | v :: vis -> let b = Hashtbl.mem v.content ks in if b && not (is_mp_bound mp0) then true @@ -440,7 +446,7 @@ let visible_clash mp0 ks = let visible_clash_dbg mp0 ks = let rec clash = function | [] -> None - | v :: _ when v.mp = mp0 -> None + | v :: _ when ModPath.equal v.mp mp0 -> None | v :: vis -> try Some (v.mp,Hashtbl.find v.content ks) with Not_found -> @@ -483,7 +489,7 @@ let opened_libraries () = let pp_duplicate k' prefix mp rls olab = let rls', lbl = - if k'<>Mod then + if k' != Mod then (* Here rls=[s], the ref to print is ., and olab<>None *) rls, Option.get olab else @@ -492,7 +498,7 @@ let pp_duplicate k' prefix mp rls olab = in try dottify (check_duplicate prefix lbl :: rls') with Not_found -> - assert (get_phase () = Pre); (* otherwise it's too late *) + assert (get_phase () == Pre); (* otherwise it's too late *) add_duplicate prefix lbl; dottify rls let fstlev_ks k = function @@ -505,7 +511,7 @@ let fstlev_ks k = function let pp_ocaml_local k prefix mp rls olab = (* what is the largest prefix of [mp] that belongs to [visible]? *) - assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) + assert (k != Mod || not (ModPath.equal mp prefix)); (* mp as whole module isn't in itself *) let rls' = List.skipn (mp_length prefix) rls in let k's = fstlev_ks k rls' in (* Reference r / module path mp is of the form [.s.<...>]. *) @@ -517,7 +523,7 @@ let pp_ocaml_local k prefix mp rls olab = let pp_ocaml_bound base rls = (* clash with a MPbound will be detected and fixed by renaming this MPbound *) - if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls)); + if get_phase () == Pre then ignore (visible_clash base (Mod,List.hd rls)); dottify rls (* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *) @@ -526,7 +532,7 @@ let pp_ocaml_extern k base rls = match rls with | [] -> assert false | base_s :: rls' -> if (not (modular ())) (* Pseudo qualification with "" *) - || (rls' = []) (* Case of a file A.v used as a module later *) + || (List.is_empty rls') (* Case of a file A.v used as a module later *) || (not (mpfiles_mem base)) (* Module not opened *) || (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *) || (visible_clash base (fstlev_ks k rls')) (* Local conflict *) @@ -556,7 +562,7 @@ let pp_haskell_gen k mp rls = match rls with | s::rls' -> let str = pseudo_qualify rls' in let str = if is_upper str && not (upperkind k) then ("_"^str) else str in - let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in + let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in prf ^ str (* Main name printing function for a reference *) @@ -566,7 +572,7 @@ let pp_global k r = assert (List.length ls > 1); let s = List.hd ls in let mp,_,l = repr_of_r r in - if mp = top_visible_mp () then + if ModPath.equal mp (top_visible_mp ()) then (* simpliest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) @@ -582,7 +588,7 @@ let pp_global k r = let pp_module mp = let ls = mp_renaming mp in match mp with - | MPdot (mp0,l) when mp0 = top_visible_mp () -> + | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> (* simpliest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in @@ -605,7 +611,7 @@ let check_extract_ascii () = | Haskell -> "Char" | _ -> raise Not_found in - find_custom (IndRef (ind_ascii,0)) = char_type + String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) with Not_found -> false let is_list_cons l = @@ -613,7 +619,7 @@ let is_list_cons l = let is_native_char = function | MLcons(_,ConstructRef ((kn,0),1),l) -> - kn = ind_ascii && check_extract_ascii () && is_list_cons l + MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l | _ -> false let pp_native_char c = -- cgit v1.2.3