1 files changed, 38 insertions, 47 deletions

diff --git a/library/heads.ml b/library/heads.ml
index f49d1cb5..5c153b06 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -1,19 +1,18 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
 open Term
+open Vars
 open Mod_subst
 open Environ
-open Libnames
-open Nameops
+open Globnames
 open Libobject
 open Lib
 
@@ -39,38 +38,25 @@ type head_approximation =
 
 module Evalreford = struct
   type t = evaluable_global_reference
-  let compare x y = 
-     let make_name = function
-      | EvalConstRef con -> 
-	  EvalConstRef(constant_of_kn(canonical_con con))
-      | k -> k
-     in 
-       Pervasives.compare (make_name x) (make_name y)
+  let compare gr1 gr2 = match gr1, gr2 with
+  | EvalVarRef id1, EvalVarRef id2 -> Id.compare id1 id2
+  | EvalVarRef _, EvalConstRef _ -> -1
+  | EvalConstRef c1, EvalConstRef c2 ->
+    Constant.CanOrd.compare c1 c2
+  | EvalConstRef _, EvalVarRef _ -> 1
 end
 
 module Evalrefmap =
   Map.Make (Evalreford)
 
 
-let head_map = ref Evalrefmap.empty
-
-let init () = head_map := Evalrefmap.empty
-
-let freeze () = !head_map
-
-let unfreeze hm = head_map := hm
-
-let _ =
-  Summary.declare_summary "Head_decl"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
+let head_map = Summary.ref Evalrefmap.empty ~name:"Head_decl"
 
 let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
 let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
 
 let kind_of_head env t =
-  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with
+  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
@@ -80,18 +66,27 @@ let kind_of_head env t =
         match pi2 (lookup_named id env) with
         | Some c -> aux k l c b
         | None -> NotImmediatelyComputableHead)
-  | Const cst ->
+  | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
        with Not_found -> assert false)
   | Construct _ | CoFix _ ->
       if b then NotImmediatelyComputableHead else ConstructorHead
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
   | Cast (c,_,_) -> aux k l c b
-  | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
-  | Lambda (_,_,c) -> aux k (List.tl l) (subst1 (List.hd l) c) b
+  | Lambda (_,_,c) ->
+    begin match l with
+    | [] ->
+      let () = assert (not b) in
+      aux (k + 1) [] c b
+    | h :: l -> aux k l (subst1 h c) b
+    end
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
+  | Proj (p,c) ->
+      (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
+       with Not_found -> assert false)
+
   | Case (_,_,c,_) -> aux k [] c true
   | Fix ((i,j),_) ->
       let n = i.(j) in
@@ -113,18 +108,26 @@ let kind_of_head env t =
           k+n-m,[],a
         else
           (* enough arguments to [cst] *)
-          k,list_skipn n l,List.nth l (i-1) in
-      let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in
-      aux k' l' a (with_subcase or with_case)
+          k,List.skipn n l,List.nth l (i-1) in
+      let l' = List.make q (mkMeta 0) @ rest in
+      aux k' l' a (with_subcase || with_case)
   | ConstructorHead when with_case -> NotImmediatelyComputableHead
   | x -> x
   in aux 0 [] t false
 
+(* FIXME: maybe change interface here *)
 let compute_head = function
 | EvalConstRef cst ->
-    (match constant_opt_value (Global.env()) cst with
+   let env = Global.env() in
+   let cb = Environ.lookup_constant cst env in
+   let is_Def = function Declarations.Def _ -> true | _ -> false in
+   let body = 
+     if cb.Declarations.const_proj = None && is_Def cb.Declarations.const_body
+     then Declareops.body_of_constant (Environ.opaque_tables env) cb else None 
+   in
+     (match body with
      | None -> RigidHead (RigidParameter cst)
-     | Some c -> kind_of_head (Global.env()) c)
+     | Some c -> kind_of_head env c)
 | EvalVarRef id ->
     (match pi2 (Global.lookup_named id) with
      | Some c when not (Decls.variable_opacity id) ->
@@ -147,8 +150,8 @@ let cache_head o =
 
 let subst_head_approximation subst = function
   | RigidHead (RigidParameter cst) as k ->
-      let cst,c = subst_con subst cst in
-      if isConst c && eq_constant (destConst c) cst then
+      let cst,c = subst_con_kn subst cst in
+      if isConst c && eq_constant (fst (destConst c)) cst then
         (* A change of the prefix of the constant *)
         k
       else
@@ -181,15 +184,3 @@ let inHead : head_obj -> obj =
 let declare_head c =
   let hd = compute_head c in
   add_anonymous_leaf (inHead (c,hd))
-
-(** Printing *)
-
-let pr_head = function
-| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst
-| RigidHead (RigidType) -> str "rigid type"
-| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id
-| ConstructorHead -> str "constructor"
-| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt())
-| NotImmediatelyComputableHead -> str "unknown"
-
-