diff options
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 44 |
1 files changed, 27 insertions, 17 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index b29f06c6..28f0fa4f 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -57,22 +57,34 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 +| Const_sorts _, _ -> false +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind _, _ -> false +| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 +| Const_proj _, _ -> false | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 -| _ -> false +| Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2 +| Const_univ_level _ , _ -> false +| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type _ , _ -> false let rec hash_structured_constant c = let open Hashset.Combine in match c with | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u)) - | Const_b0 t -> combinesmall 3 (Int.hash t) + | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_proj p -> combinesmall 3 (Constant.hash p) + | Const_b0 t -> combinesmall 4 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in let h = Array.fold_left fold 0 a in - combinesmall 4 (combine (Int.hash t) h) + combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + | Const_type u -> combinesmall 7 (Univ.Universe.hash u) module SConstTable = Hashtbl.Make (struct type t = structured_constant @@ -118,7 +130,7 @@ exception NotEvaluated let key rk = match !rk with | None -> raise NotEvaluated - | Some k -> (*Pp.msgnl (str"found at: "++int k);*) + | Some k -> try Ephemeron.get k with Ephemeron.InvalidKey -> raise NotEvaluated @@ -142,23 +154,22 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n -let rec slot_for_getglobal env (kn,u) = +let rec slot_for_getglobal env kn = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> (* Pp.msgnl(str"not yet evaluated");*) let pos = match cb.const_body_code with - | None -> set_global (val_of_constant (kn,u)) + | None -> set_global (val_of_constant kn) | Some code -> match Cemitcodes.force code with | BCdefined(code,pl,fv) -> - if Univ.Instance.is_empty u then - let v = eval_to_patch env (code,pl,fv) in - set_global v - else set_global (val_of_constant (kn,u)) - | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant (kn,u)) in + let v = eval_to_patch env (code,pl,fv) in + set_global v + | BCalias kn' -> slot_for_getglobal env kn' + | BCconstant -> set_global (val_of_constant kn) + in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos @@ -191,6 +202,8 @@ and slot_for_fv env fv = fill_fv_cache rv i val_of_rel env_of_rel b | Some (v, _) -> v end + | FVuniv_var idu -> + assert false and eval_to_patch env (buff,pl,fv) = (* copy code *before* patching because of nested evaluations: @@ -208,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) = List.iter patch pl; let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in -(*Pp.msgnl (str"execute code");*) eval_tcode tc vm_env and val_of_constr env c = @@ -226,5 +238,3 @@ and val_of_constr env c = let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) - - |