Permalink
Browse files

More monomorphizations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 1d436a1 commit 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 ppedrot committed Nov 13, 2012
View
@@ -205,7 +205,7 @@ EXTEND
let t, g = interp_entry_name false None e sep in
GramNonTerminal (!@loc, t, g, Some (Names.id_of_string s))
| s = STRING ->
- if s = "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+ if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
GramTerminal s
] ]
;
View
@@ -84,7 +84,7 @@ EXTEND
rule:
[ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
->
- if s = "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+ if String.equal s "" then Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
(Some s,l,<:expr< fun () -> $e$ >>)
| "[" ; "-" ; l = LIST1 args ; "]" ; "->" ; "[" ; e = Pcaml.expr ; "]" ->
(None,l,<:expr< fun () -> $e$ >>)
View
@@ -1703,7 +1703,7 @@ let main files =
let windows_actions = GAction.action_group ~name:"Windows" () in
let help_actions = GAction.action_group ~name:"Help" () in
let add_gen_actions menu_name act_grp l =
- let no_under = Util.string_map (fun x -> if x = '_' then '-' else x) in
+ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x) in
let add_simple_template menu_name act_grp text =
let text' =
let l = String.length text - 1 in
View
@@ -1,6 +1,6 @@
let ui_m = GAction.ui_manager ();;
-let no_under = Util.string_map (fun x -> if x = '_' then '-' else x)
+let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
let list_items menu li =
let res_buf = Buffer.create 500 in
View
@@ -73,9 +73,10 @@ let local_binder_loc = function
| LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
| LocalRawAssum ([],_,_) -> assert false
-let local_binders_loc bll =
- if bll = [] then Loc.ghost else
- Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
+let local_binders_loc bll = match bll with
+ | [] -> Loc.ghost
+ | h :: l ->
+ Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
View
@@ -179,16 +179,17 @@ let push_local sz r =
(*i Compilation of variables *)
-let find_at el l =
+let find_at f l =
let rec aux n = function
| [] -> raise Not_found
- | hd :: tl -> if hd = el then n else aux (n+1) tl
+ | hd :: tl -> if f hd then n else aux (n + 1) tl
in aux 1 l
let pos_named id r =
let env = !(r.in_env) in
let cid = FVnamed id in
- try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
+ let f = function FVnamed id' -> id_eq id id' | _ -> false in
+ try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
with Not_found ->
let pos = env.size in
r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev};
@@ -206,7 +207,8 @@ let pos_rel i r sz =
let i = i - r.nb_rec in
let db = FVrel(i) in
let env = !(r.in_env) in
- try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
+ let f = function FVrel j -> Int.equal i j | _ -> false in
+ try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
with Not_found ->
let pos = env.size in
r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
@@ -357,7 +359,7 @@ let rec str_const c =
let oip = oib.mind_packets.(j) in
let num,arity = oip.mind_reloc_tbl.(i-1) in
let nparams = oib.mind_nparams in
- if nparams + arity = Array.length args then
+ if Int.equal (nparams + arity) (Array.length args) then
(* spiwack: *)
(* 1/ tries to compile the constructor in an optimal way,
it is supposed to work only if the arguments are
@@ -609,7 +611,7 @@ let rec compile_constr reloc c sz cont =
let lbl_sw = Label.create () in
let sz_b,branch,is_tailcall =
match branch1 with
- | Kreturn k -> assert (k = sz); sz, branch1, true
+ | Kreturn k -> assert (Int.equal k sz); sz, branch1, true
| _ -> sz+3, Kjump, false
in
let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -632,7 +634,7 @@ let rec compile_constr reloc c sz cont =
let nargs = List.length args in
let lbl_b,code_b =
label_code(
- if nargs = arity then
+ if Int.equal nargs arity then
Kpushfields arity ::
compile_constr (push_param arity sz_b reloc)
body (sz_b+arity) (add_pop arity (branch :: !c))
@@ -844,7 +846,7 @@ let op_compilation n op =
fun kn fc reloc args sz cont ->
if not fc then raise Not_found else
let nargs = Array.length args in
- if nargs=n then (*if it is a fully applied addition*)
+ if Int.equal nargs n then (*if it is a fully applied addition*)
let (escape, labeled_cont) = make_branch cont in
let else_lbl = Label.create () in
comp_args compile_constr reloc args sz
@@ -854,7 +856,7 @@ let op_compilation n op =
(* works as comp_app with nargs = n and non-tailcall cont*)
Kgetglobal (get_allias !global_env kn)::
Kapply n::labeled_cont)))
- else if nargs=0 then
+ else if Int.equal nargs 0 then
code_construct kn cont
else
comp_app (fun _ _ _ cont -> code_construct kn cont)
View
@@ -327,7 +327,7 @@ and fterm =
let fterm_of v = v.term
let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
+let is_val v = match v.norm with Norm -> true | _ -> false
let mk_atom c = {norm=Norm;term=FAtom c}
@@ -426,9 +426,9 @@ let rec lft_fconstr n ft =
| FLOCKED -> assert false
| _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
- if k=0 then f else lft_fconstr k f
+ if Int.equal k 0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
- if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
+ if Int.equal k 0 then v else Array.map (fun f -> lft_fconstr k f) v
let clos_rel e i =
match expand_rel i e with
@@ -452,7 +452,7 @@ let compact_stack head stk =
(* Put an update mark in the stack, only if needed *)
let zupdate m s =
- if !share & m.norm = Red
+ if !share && begin match m.norm with Red -> true | _ -> false end
then
let s' = compact_stack m s in
let _ = m.term <- FLOCKED in
@@ -760,7 +760,7 @@ let rec reloc_rargs_rec depth stk =
match stk with
Zapp args :: s ->
Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
- | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
+ | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s
| _ -> stk
let reloc_rargs depth stk =
@@ -771,13 +771,13 @@ let rec drop_parameters depth n argstk =
Zapp args::s ->
let q = Array.length args in
if n > q then drop_parameters depth (n-q) s
- else if n = q then reloc_rargs depth s
+ else if Int.equal n q then reloc_rargs depth s
else
let aft = Array.sub args n (q-n) in
reloc_rargs depth (append_stack aft s)
| Zshift(k)::s -> drop_parameters (depth-k) n s
| [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
- if n=0 then []
+ if Int.equal n 0 then []
else anomaly
"ill-typed term: found a match on a partially applied constructor"
| _ -> assert false
View
@@ -127,7 +127,7 @@ let subst_const_def sub = function
| OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
let subst_const_body sub cb = {
- const_hyps = (assert (cb.const_hyps=[]); []);
+ const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
const_body = subst_const_def sub cb.const_body;
const_type = subst_const_type sub cb.const_type;
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
@@ -341,7 +341,7 @@ let subst_mind sub mib =
{ mind_record = mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
- mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+ mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
View
@@ -49,8 +49,9 @@ let named_context_val env = env.env_named_context,env.env_named_vals
let rel_context env = env.env_rel_context
let empty_context env =
- env.env_rel_context = empty_rel_context
- && env.env_named_context = empty_named_context
+ match env.env_rel_context, env.env_named_context with
+ | [], [] -> true
+ | _ -> false
(* Rel context *)
let lookup_rel n env =
@@ -321,7 +322,7 @@ let apply_to_hyp (ctxt,vals) id f =
let rec aux rtail ctxt vals =
match ctxt, vals with
| (idc,c,ct as d)::ctxt, v::vals ->
- if idc = id then
+ if id_eq idc id then
(f ctxt d rtail)::ctxt, v::vals
else
let ctxt',vals' = aux (d::rtail) ctxt vals in
@@ -334,7 +335,7 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
let rec aux ctxt vals =
match ctxt,vals with
| (idc,c,ct as d)::ctxt, v::vals ->
- if idc = id then
+ if id_eq idc id then
let sign = ctxt,vals in
push_named_context_val (f d sign) sign
else
@@ -348,7 +349,7 @@ let insert_after_hyp (ctxt,vals) id d check =
let rec aux ctxt vals =
match ctxt, vals with
| (idc,c,ct)::ctxt', v::vals' ->
- if idc = id then begin
+ if id_eq idc id then begin
check ctxt;
push_named_context_val d (ctxt,vals)
end else
View
@@ -49,7 +49,7 @@ let rec reloc_rel n = function
let rec is_lift_id = function
| ELID -> true
- | ELSHFT(e,n) -> n=0 & is_lift_id e
+ | ELSHFT(e,n) -> Int.equal n 0 & is_lift_id e
| ELLFT (_,e) -> is_lift_id e
(*********************)
View
@@ -190,7 +190,7 @@ let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
(* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
the situation where a non-Prop singleton inductive becomes Prop
when applied to Prop params *)
- if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort
+ if not polyprop && not (is_type0m_univ ar.poly_level) && is_prop_sort s
then raise (SingletonInductiveBecomesProp mip.mind_typename);
mkArity (List.rev ctx,s)
View
@@ -31,6 +31,8 @@ type delta_hint =
module Deltamap = struct
type t = module_path MPmap.t * delta_hint KNmap.t
let empty = MPmap.empty, KNmap.empty
+ let is_empty (mm, km) =
+ MPmap.is_empty mm && KNmap.is_empty km
let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
let find_mp mp map = MPmap.find mp (fst map)
@@ -391,10 +393,10 @@ let subst_mps sub c =
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
- | _ when mp = mpfrom -> mpto
+ | _ when mp_eq mp mpfrom -> mpto
| MPdot (mp1,l) ->
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
- if mp1==mp1' then mp
+ if mp1 == mp1' then mp
else MPdot (mp1',l)
| _ -> mp
@@ -406,7 +408,7 @@ let replace_mp_in_kn mpfrom mpto kn =
let rec mp_in_mp mp mp1 =
match mp1 with
- | _ when mp1 = mp -> true
+ | _ when mp_eq mp1 mp -> true
| MPdot (mp2,l) -> mp_in_mp mp mp2
| _ -> false
@@ -483,7 +485,7 @@ let update_delta_resolver resolver1 resolver2 =
let add_delta_resolver resolver1 resolver2 =
if resolver1 == resolver2 then
resolver2
- else if resolver2 = empty_delta_resolver then
+ else if Deltamap.is_empty resolver2 then
resolver1
else
Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
@@ -522,13 +524,13 @@ let join subst1 subst2 =
Umap.join subst2 subst
let rec occur_in_path mbi = function
- | MPbound bid' -> mbi = bid'
+ | MPbound bid' -> mod_bound_id_eq mbi bid'
| MPdot (mp1,_) -> occur_in_path mbi mp1
| _ -> false
let occur_mbid mbi sub =
let check_one mbi' (mp,_) =
- if mbi = mbi' || occur_in_path mbi mp then raise Exit
+ if mod_bound_id_eq mbi mbi' || occur_in_path mbi mp then raise Exit
in
try
Umap.iter_mbi check_one sub;
View
@@ -138,10 +138,10 @@ let module_body_of_type mp mtb =
mod_retroknowledge = []}
let check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then () else
+ if mp_eq mp1 mp2 then () else
let mb1=lookup_module mp1 env in
let mb2=lookup_module mp2 env in
- if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2)
+ if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2)
then ()
else error_not_equal_modpaths mp1 mp2
@@ -184,7 +184,7 @@ and subst_structure sub do_delta sign =
and subst_module sub do_delta mb =
let mp = subst_mp sub mb.mod_mp in
- let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then
+ let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then
add_mp mb.mod_mp mp
empty_delta_resolver sub else sub in
let id_delta = (fun x y-> x) in
@@ -557,7 +557,7 @@ and clean_expr l = function
| SEBfunctor (mbid,sigt,str) as s->
let str_clean = clean_expr l str in
let sig_clean = clean_expr l sigt.typ_expr in
- if str_clean == str && sig_clean = sigt.typ_expr then
+ if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
| SEBstruct str as s->
let str_clean = Util.List.smartmap (clean_struct l) str in
Oops, something went wrong.

0 comments on commit 98f3621

Please sign in to comment.