diff options
Diffstat (limited to 'kernel/constr.ml')
| -rw-r--r-- | kernel/constr.ml | 145 |
1 files changed, 78 insertions, 67 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 8375316003..15e5c512ed 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -16,7 +16,7 @@ (* Optimization of substitution functions by Chet Murthy *) (* Optimization of lifting functions by Bruno Barras, Mar 1997 *) (* Hash-consing by Bruno Barras in Feb 1998 *) -(* Restructuration of Coq of the type-checking kernel by Jean-Christophe +(* Restructuration of Coq of the type-checking kernel by Jean-Christophe Filliâtre, 1999 *) (* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *) (* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) @@ -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, @@ -919,7 +924,7 @@ let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *) let eq_constr_univs univs m n = if m == n then true - else + else let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = @@ -928,11 +933,11 @@ let eq_constr_univs univs m n = let leq_constr_univs univs m n = if m == n then true - else + else let eq_universes _ _ = UGraph.check_eq_instances univs in - let eq_sorts s1 s2 = s1 == s2 || + let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in - let leq_sorts s1 s2 = s1 == s2 || + let leq_sorts s1 s2 = s1 == s2 || UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -944,17 +949,17 @@ let leq_constr_univs univs m n = let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty - else + else let cstrs = ref Constraint.empty in let eq_universes _ _ = UGraph.check_eq_instances univs in - let eq_sorts s1 s2 = + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else - (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_eq univs u1 u2 then true + else + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in let rec eq_constr' nargs m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n @@ -964,23 +969,23 @@ let eq_constr_univs_infer univs m n = let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty - else + else let cstrs = ref Constraint.empty in let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in - let eq_sorts s1 s2 = + let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_eq univs u1 u2 then true - else (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_eq univs u1 u2 then true + else (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in - let leq_sorts s1 s2 = + let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if UGraph.check_leq univs u1 u2 then true - else + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if UGraph.check_leq univs u1 u2 then true + else (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in cstrs := Univ.Constraint.union c !cstrs; true @@ -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 *) @@ -1175,54 +1183,54 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let rec hash_term t = match t with | Var i -> - (Var (sh_id i), combinesmall 1 (Id.hash i)) + (Var (sh_id i), combinesmall 1 (Id.hash i)) | Sort s -> - (Sort (sh_sort s), combinesmall 2 (Sorts.hash s)) + (Sort (sh_sort s), combinesmall 2 (Sorts.hash s)) | Cast (c, k, t) -> - let c, hc = sh_rec c in - let t, ht = sh_rec t in - (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht)) + let c, hc = sh_rec c in + let t, ht = sh_rec t in + (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht)) | Prod (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in + let t, ht = sh_rec t + and c, hc = sh_rec c in (Prod (sh_na na, t, c), combinesmall 4 (combine3 (hash_annot Name.hash na) ht hc)) | Lambda (na,t,c) -> - let t, ht = sh_rec t - and c, hc = sh_rec c in + let t, ht = sh_rec t + and c, hc = sh_rec c in (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (hash_annot Name.hash na) ht hc)) | LetIn (na,b,t,c) -> - let b, hb = sh_rec b in - let t, ht = sh_rec t in - let c, hc = sh_rec c in + let b, hb = sh_rec b in + let t, ht = sh_rec t in + let c, hc = sh_rec c in (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc)) | App (c,l) -> - let c, hc = sh_rec c in - let l, hl = hash_term_array l in - (App (c,l), combinesmall 7 (combine hl hc)) + let c, hc = sh_rec c in + let l, hl = hash_term_array l in + (App (c,l), combinesmall 7 (combine hl hc)) | Evar (e,l) -> - let l, hl = hash_term_array l in - (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) + let l, hl = hash_term_array l in + (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Const (c,u) -> - let c' = sh_con c in - let u', hu = sh_instance u in - (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) + let c' = sh_con c in + let u', hu = sh_instance u in + (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu)) | Ind (ind,u) -> - let u', hu = sh_instance u in - (Ind (sh_ind ind, u'), - combinesmall 10 (combine (ind_syntactic_hash ind) hu)) + let u', hu = sh_instance u in + (Ind (sh_ind ind, u'), + combinesmall 10 (combine (ind_syntactic_hash ind) hu)) | Construct (c,u) -> - let u', hu = sh_instance u in - (Construct (sh_construct c, u'), - combinesmall 11 (combine (constructor_syntactic_hash c) hu)) + let u', hu = sh_instance u in + (Construct (sh_construct c, u'), + combinesmall 11 (combine (constructor_syntactic_hash c) hu)) | Case (ci,p,c,bl) -> - let p, hp = sh_rec p - and c, hc = sh_rec c in - let bl,hbl = hash_term_array bl in + let p, hp = sh_rec p + and c, hc = sh_rec c in + let bl,hbl = hash_term_array bl in let hbl = combine (combine hc hp) hbl in - (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) + (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl) | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in @@ -1230,16 +1238,16 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (Fix (ln,(lna,tl,bl)), combinesmall 13 h) | CoFix(ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in - let tl,htl = hash_term_array tl in + let tl,htl = hash_term_array tl in let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in let fold accu na = combine (hash_annot Name.hash na) accu in let hna = Array.fold_left fold 0 lna in let h = combine3 hna hbl htl in (CoFix (ln,(lna,tl,bl)), combinesmall 14 h) | Meta n -> - (t, combinesmall 15 n) + (t, combinesmall 15 n) | Rel n -> - (t, combinesmall 16 n) + (t, combinesmall 16 n) | Proj (p,c) -> let c, hc = sh_rec c in let p' = Projection.hcons p in @@ -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")" |