diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 /kernel/vm.ml | |
| parent | bafb198e539998a4a64b2045a7e85125890f196e (diff) | |
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index d4a86cb49..b6a39b042 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -169,7 +169,7 @@ type whd = let rec whd_accu a stk = let stk = - if Obj.size a = 2 then stk + if Int.equal (Obj.size a) 2 then stk else Zapp (Obj.obj a) :: stk in let at = Obj.field a 1 in match Obj.tag at with @@ -211,7 +211,7 @@ let whd_val : values -> whd = let tag = Obj.tag o in if tag = accu_tag then ( - if Obj.size o = 1 then Obj.obj o (* sort *) + if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) else if is_accumulate (fun_code o) then whd_accu o [] else (Vprod(Obj.obj o))) @@ -255,7 +255,7 @@ let arg args i = let apply_arguments vf vargs = let n = nargs vargs in - if n = 0 then vf + if Int.equal n 0 then vf else begin push_ra stop; @@ -265,7 +265,7 @@ let apply_arguments vf vargs = let apply_vstack vf vstk = let n = Array.length vstk in - if n = 0 then vf + if Int.equal n 0 then vf else begin push_ra stop; @@ -502,7 +502,7 @@ let type_of_switch sw = interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = - if arity = 0 then ((Obj.magic tag):values) + if Int.equal arity 0 then ((Obj.magic tag):values) else let b = Obj.new_block tag arity in for i = 0 to arity - 1 do |