diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 8375316003..b60b2d6d04 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -104,6 +104,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of Projection.t * 'constr | Int of Uint63.t + | Float of Float64.t (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term @@ -241,6 +242,9 @@ let mkRef (gr,u) = let open GlobRef in match gr with (* Constructs a primitive integer *) let mkInt i = Int i +(* Constructs a primitive float number *) +let mkFloat f = Float f + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -446,7 +450,7 @@ let decompose_appvect c = let fold f acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> acc + | Construct _ | Int _ | Float _) -> acc | Cast (c,_,t) -> f (f acc c) t | Prod (_,t,c) -> f (f acc t) c | Lambda (_,t,c) -> f (f acc t) c @@ -466,7 +470,7 @@ let fold f acc c = match kind c with let iter f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f c; f t | Prod (_,t,c) -> f t; f c | Lambda (_,t,c) -> f t; f c @@ -486,7 +490,7 @@ let iter f c = match kind c with let iter_with_binders g f n c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c @@ -512,7 +516,7 @@ let iter_with_binders g f n c = match kind c with let fold_constr_with_binders g f n acc c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> acc + | Construct _ | Int _ | Float _) -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (_na,t,c) -> f (g n) (f n acc t) c | Lambda (_na,t,c) -> f (g n) (f n acc t) c @@ -608,7 +612,7 @@ let map_return_predicate_with_full_binders g f l ci p = let map_gen userview f c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> c + | Construct _ | Int _ | Float _) -> c | Cast (b,k,t) -> let b' = f b in let t' = f t in @@ -673,7 +677,7 @@ let map = map_gen false let fold_map f accu c = match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> accu, c + | Construct _ | Int _ | Float _) -> accu, c | Cast (b,k,t) -> let accu, b' = f accu b in let accu, t' = f accu t in @@ -733,7 +737,7 @@ let fold_map f accu c = match kind c with let map_with_binders g f l c0 = match kind c0 with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> c0 + | Construct _ | Int _ | Float _) -> c0 | Cast (c, k, t) -> let c' = f l c in let t' = f l t in @@ -810,7 +814,7 @@ let lift n = liftn n 1 let fold_with_full_binders g f n acc c = let open Context.Rel.Declaration in match kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ -> acc + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc | Cast (c,_, t) -> f n (f n acc c) t | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c @@ -852,6 +856,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Int i1, Int i2 -> Uint63.equal i1 i2 + | Float f1, Float f2 -> Float64.equal f1 f2 | Sort s1, Sort s2 -> leq_sorts s1 s2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 @@ -878,7 +883,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t Int.equal ln1 ln2 && Array.equal_norefl (eq 0) tl1 tl2 && Array.equal_norefl (eq 0) bl1 bl2 | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ - | CoFix _ | Int _), _ -> false + | CoFix _ | Int _ | Float _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -1055,6 +1060,8 @@ let constr_ord_int f t1 t2 = | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 | Proj _, _ -> -1 | _, Proj _ -> 1 | Int i1, Int i2 -> Uint63.compare i1 i2 + | Int _, _ -> -1 | _, Int _ -> 1 + | Float f1, Float f2 -> Float64.total_compare f1 f2 let rec compare m n= constr_ord_int compare m n @@ -1139,9 +1146,10 @@ let hasheq t1 t2 = && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 | Int i1, Int i2 -> i1 == i2 + | Float f1, Float f2 -> Float64.equal f1 f2 | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ - | Fix _ | CoFix _ | Int _), _ -> false + | Fix _ | CoFix _ | Int _ | Float _), _ -> false (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) @@ -1247,6 +1255,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Int i -> let (h,l) = Uint63.to_int2 i in (t, combinesmall 18 (combine h l)) + | Float f -> (t, combinesmall 19 (Float64.hash f)) and sh_rec t = let (y, h) = hash_term t in @@ -1311,6 +1320,7 @@ let rec hash t = | Proj (p,c) -> combinesmall 17 (combine (Projection.hash p) (hash c)) | Int i -> combinesmall 18 (Uint63.hash i) + | Float f -> combinesmall 19 (Float64.hash f) and hash_term_array t = Array.fold_left (fun acc t -> combine (hash t) acc) 0 t @@ -1455,3 +1465,4 @@ let rec debug_print c = cut() ++ str":=" ++ debug_print bd) (Array.to_list fixl)) ++ str"}") | Int i -> str"Int("++str (Uint63.to_string i) ++ str")" + | Float i -> str"Float("++str (Float64.to_string i) ++ str")" |