From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 pretyping/typeclasses.ml | 431 +++++++++++++++++++++++------------------------
 1 file changed, 213 insertions(+), 218 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 216a0611..b85c6721 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses.ml 12189 2009-06-15 05:08:44Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -21,8 +21,20 @@ open Nametab
 open Mod_subst
 open Util
 open Typeclasses_errors
+open Libobject
 (*i*)
 
+
+let add_instance_hint_ref = ref (fun id pri -> assert false)
+let register_add_instance_hint =
+  (:=) add_instance_hint_ref
+let add_instance_hint id = !add_instance_hint_ref id
+
+let set_typeclass_transparency_ref = ref (fun id pri -> assert false)
+let register_set_typeclass_transparency =
+  (:=) set_typeclass_transparency_ref
+let set_typeclass_transparency gr c = !set_typeclass_transparency_ref gr c
+
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 (* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -32,284 +44,265 @@ type rels = constr list
 (* This module defines type-classes *)
 type typeclass = {
   (* The class implementation *)
-  cl_impl : global_reference; 
+  cl_impl : global_reference;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (global_reference * bool) option list * rel_context; 
+  cl_context : (global_reference * bool) option list * rel_context;
 
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
-  
+
   (* The method implementaions as projections. *)
   cl_projs : (identifier * constant option) list;
 }
+module Gmap = Fmap.Make(RefOrdered)
 
-type typeclasses = (global_reference, typeclass) Gmap.t
+type typeclasses = typeclass Gmap.t
 
 type instance = {
   is_class: global_reference;
   is_pri: int option;
-  (* Sections where the instance should be redeclared, 
-     -1 for discard, 0 for none, mutable to avoid redeclarations 
+  (* Sections where the instance should be redeclared,
+     -1 for discard, 0 for none, mutable to avoid redeclarations
      when multiple rebuild_object happen. *)
-  is_global: int ref;
-  is_impl: constant; 
+  is_global: int;
+  is_impl: global_reference; 
 }
 
-type instances = (global_reference, instance Cmap.t) Gmap.t
+type instances = (instance Gmap.t) Gmap.t
 
 let instance_impl is = is.is_impl
 
-let new_instance cl pri glob impl = 
+let new_instance cl pri glob impl =
   let global =
-    if Lib.sections_are_opened () then 
-      if glob then Lib.sections_depth ()
-      else -1
-    else 0
+    if glob then Lib.sections_depth ()
+    else -1
   in
     { is_class = cl.cl_impl;
       is_pri = pri ;
-      is_global = ref global ;
+      is_global = global ;
       is_impl = impl }
-	
+
+(*
+ * states management
+ *)
+
 let classes : typeclasses ref = ref Gmap.empty
 
-let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty
-  
 let instances : instances ref = ref Gmap.empty
-  
-let freeze () = !classes, !methods, !instances
 
-let unfreeze (cl,m,is) = 
+let freeze () = !classes, !instances
+
+let unfreeze (cl,is) =
   classes:=cl;
-  methods:=m;
   instances:=is
-    
+
 let init () =
-  classes:= Gmap.empty; 
-  methods:= Gmap.empty;
+  classes:= Gmap.empty;
   instances:= Gmap.empty
-    
-let _ = 
+
+let _ =
   Summary.declare_summary "classes_and_instances"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init;
-      Summary.survive_module = false;
-      Summary.survive_section = true }
-
-let gmap_merge old ne =
-  Gmap.fold (fun k v acc -> Gmap.add k v acc) old ne
+      Summary.init_function = init }
 
-let cmap_union = Cmap.fold Cmap.add
+(*
+ * classes persistent object
+ *)
 
-let gmap_cmap_merge old ne =
-  let ne' = 
-    Gmap.fold (fun cl insts acc -> 
-      let oldinsts = try Gmap.find cl old with Not_found -> Cmap.empty in
-	Gmap.add cl (cmap_union oldinsts insts) acc)
-      ne Gmap.empty
-  in
-    Gmap.fold (fun cl insts acc -> 
-      if Gmap.mem cl acc then acc
-      else Gmap.add cl insts acc)
-      old ne'
+let load_class (_, cl) =
+  classes := Gmap.add cl.cl_impl cl !classes
 
-let add_instance_hint_ref = ref (fun id pri -> assert false)
-let register_add_instance_hint =
-  (:=) add_instance_hint_ref
-let add_instance_hint id = !add_instance_hint_ref id
+let cache_class = load_class
 
-let cache (_, (cl, m, inst)) =
-  classes := cl;
-  methods := m;
-  instances := inst
-    
-let load (_, (cl, m, inst)) =
-  classes := gmap_merge !classes cl;
-  methods := gmap_merge !methods m;
-  instances := gmap_cmap_merge !instances inst
-
-open Libobject
-
-let subst (_,subst,(cl,m,inst)) = 
+let subst_class (subst,cl) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst c = Mod_subst.subst_mps subst c
-  and do_subst_gr gr = fst (subst_global subst gr)
-  in
-  let do_subst_ctx ctx = 
-    list_smartmap (fun (na, b, t) ->
-      (na, Option.smartmap do_subst b, do_subst t))
-      ctx
-  in
-  let do_subst_context (grs,ctx) = 
+  and do_subst_gr gr = fst (subst_global subst gr) in
+  let do_subst_ctx ctx = list_smartmap
+    (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t))
+    ctx in
+  let do_subst_context (grs,ctx) =
     list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
-    do_subst_ctx ctx
-  in
+    do_subst_ctx ctx in
   let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, Option.smartmap do_subst_con y)) projs in
-  let subst_class k cl classes = 
-    let k = do_subst_gr k in
-    let cl' = { cl_impl = k;
-		cl_context = do_subst_context cl.cl_context;
-		cl_props = do_subst_ctx cl.cl_props;
-		cl_projs = do_subst_projs cl.cl_projs; }
-    in 
-    let cl' = if cl' = cl then cl else cl' in
-      Gmap.add k cl' classes
-  in
-  let classes = Gmap.fold subst_class cl Gmap.empty in
-  let subst_inst k insts instances =
-    let k = do_subst_gr k in
-    let insts' = 
-      Cmap.fold (fun cst is acc -> 
-	let cst = do_subst_con cst in
-	let is' = { is with is_class = k; is_impl = cst } in
-	  Cmap.add cst (if is' = is then is else is') acc) insts Cmap.empty
-    in Gmap.add k insts' instances
-  in
-  let instances = Gmap.fold subst_inst inst Gmap.empty in
-    (classes, m, instances)
-
-let rel_of_variable_context ctx = 
-  List.fold_right (fun (n,_,b,t) (ctx', subst)->
-    let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
-      (decl :: ctx', n :: subst)) ctx ([], [])
-    
-let discharge (_,(cl,m,inst)) =
+  { cl_impl = do_subst_gr cl.cl_impl;
+    cl_context = do_subst_context cl.cl_context;
+    cl_props = do_subst_ctx cl.cl_props;
+    cl_projs = do_subst_projs cl.cl_projs; }
+
+let discharge_class (_,cl) =
+  let repl = Lib.replacement_context () in
+  let rel_of_variable_context ctx = List.fold_right
+    ( fun (n,_,b,t) (ctx', subst) ->
+	let decl = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
+	(decl :: ctx', n :: subst)
+    ) ctx ([], []) in
   let discharge_rel_context subst n rel =
+    let rel = map_rel_context (Cooking.expmod_constr repl) rel in
     let ctx, _ =
       List.fold_right
-	(fun (id, b, t) (ctx, k) -> 
-	  (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
+	(fun (id, b, t) (ctx, k) ->
+	   (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
 	rel ([], n)
     in ctx
   in
   let abs_context cl =
     match cl.cl_impl with
-    | VarRef _ | ConstructRef _ -> assert false
-    | ConstRef cst -> Lib.section_segment_of_constant cst
-    | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind
-  in
+      | VarRef _ | ConstructRef _ -> assert false
+      | ConstRef cst -> Lib.section_segment_of_constant cst
+      | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
   let discharge_context ctx' subst (grs, ctx) =
-    let grs' = List.map (fun _ -> None) subst @ 
+    let grs' = List.map (fun _ -> None) subst @
       list_smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
-    in grs', discharge_rel_context subst 1 ctx @ ctx'
-  in
-  let subst_class k cl acc = 
-    let cl_impl' = Lib.discharge_global cl.cl_impl in
-    let cl' =
-      if cl_impl' == cl.cl_impl then cl
-      else
-	let ctx = abs_context cl in
-	let ctx', subst = rel_of_variable_context ctx in
-	  { cl_impl = cl_impl';
-	    cl_context = discharge_context ctx' subst cl.cl_context;
-	    cl_props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props;
-	    cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
-    in Gmap.add cl_impl' cl' acc
-  in
-  let classes = Gmap.fold subst_class cl Gmap.empty in
-  let subst_inst k insts acc =
-    let k' = Lib.discharge_global k in
-    let insts' =
-      Cmap.fold (fun k is acc ->
-	let impl = Lib.discharge_con is.is_impl in
-	let is = { is with is_class = k'; is_impl = impl } in
-	  Cmap.add impl is acc)
-	insts Cmap.empty
-    in Gmap.add k' insts' acc
-  in
-  let instances = Gmap.fold subst_inst inst Gmap.empty in
-    Some (classes, m, instances)
-      
-let rebuild (cl,m,inst) =
-  let inst = 
-    Gmap.map (fun insts -> 
-      Cmap.fold (fun k is insts -> 
-	match !(is.is_global) with
-	  | -1 -> insts
-	  | 0 -> Cmap.add k is insts
-	  | n -> 
-	      add_instance_hint is.is_impl is.is_pri;
-	      is.is_global := pred n;
-	      Cmap.add k is insts) insts Cmap.empty)
-      inst
-  in (cl, m, inst)
-
-let (input,output) = 
+    in grs', discharge_rel_context subst 1 ctx @ ctx' in
+  let cl_impl' = Lib.discharge_global cl.cl_impl in
+  if cl_impl' == cl.cl_impl then cl else
+    let ctx = abs_context cl in
+    let ctx, subst = rel_of_variable_context ctx in
+    let context = discharge_context ctx subst cl.cl_context in
+    let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
+    { cl_impl = cl_impl';
+      cl_context = context;
+      cl_props = props;
+      cl_projs = list_smartmap (fun (x, y) -> x, Option.smartmap Lib.discharge_con y) cl.cl_projs }
+
+let rebuild_class cl = cl
+
+let (class_input,class_output) =
   declare_object
     { (default_object "type classes state") with
-      cache_function = cache;
-      load_function = (fun _ -> load);
-      open_function = (fun _ -> load);
-      classify_function = (fun (_,x) -> Substitute x);
-      discharge_function = discharge;
-      rebuild_function = rebuild;
-      subst_function = subst;
-      export_function = (fun x -> Some x) }
-
-let update () = 
-  Lib.add_anonymous_leaf (input (!classes, !methods, !instances))
-
-let add_class c = 
-  classes := Gmap.add c.cl_impl c !classes;
-  methods := List.fold_left (fun acc x -> 
-    match snd x with
-    | Some m -> Gmap.add m c.cl_impl acc
-    | None -> acc) !methods c.cl_projs;
-  update ()
+      cache_function = cache_class;
+      load_function = (fun _ -> load_class);
+      open_function = (fun _ -> load_class);
+      classify_function = (fun x -> Substitute x);
+      discharge_function = (fun a -> Some (discharge_class a));
+      rebuild_function = rebuild_class;
+      subst_function = subst_class }
+
+let add_class cl =
+  Lib.add_anonymous_leaf (class_input cl)
+
+
+(*
+ * instances persistent object
+ *)
+
+let load_instance (_,inst) = 
+  let insts = 
+    try Gmap.find inst.is_class !instances 
+    with Not_found -> Gmap.empty in
+  let insts = Gmap.add inst.is_impl inst insts in
+  instances := Gmap.add inst.is_class insts !instances
+
+let cache_instance = load_instance
+
+let subst_instance (subst,inst) = 
+  { inst with 
+      is_class = fst (subst_global subst inst.is_class);
+      is_impl = fst (subst_global subst inst.is_impl) }
+
+let discharge_instance (_,inst) =
+  if inst.is_global <= 0 then None
+  else Some 
+    { inst with 
+      is_global = pred inst.is_global;
+      is_class = Lib.discharge_global inst.is_class;
+      is_impl = Lib.discharge_global inst.is_impl }
     
-let class_info c = 
+let rebuild_instance inst =
+  add_instance_hint inst.is_impl inst.is_pri;
+  inst
+
+let classify_instance inst =
+  if inst.is_global = -1 then Dispose
+  else Substitute inst
+
+let (instance_input,instance_output) =
+  declare_object
+    { (default_object "type classes instances state") with
+      cache_function = cache_instance;
+      load_function = (fun _ -> load_instance);
+      open_function = (fun _ -> load_instance);
+      classify_function = classify_instance;
+      discharge_function = discharge_instance;
+      rebuild_function = rebuild_instance;
+      subst_function = subst_instance }
+
+let add_instance i =
+  Lib.add_anonymous_leaf (instance_input i);
+  add_instance_hint i.is_impl i.is_pri
+
+open Declarations
+
+let add_constant_class cst =
+  let ty = Typeops.type_of_constant (Global.env ()) cst in
+  let ctx, arity = decompose_prod_assum ty in
+  let tc = 
+    { cl_impl = ConstRef cst;
+      cl_context = (List.map (const None) ctx, ctx);
+      cl_props = [(Anonymous, None, arity)];
+      cl_projs = []
+    }
+  in add_class tc;
+    set_typeclass_transparency (EvalConstRef cst) false
+      
+let add_inductive_class ind =
+  let mind, oneind = Global.lookup_inductive ind in
+  let k =
+    let ctx = oneind.mind_arity_ctxt in
+    let ty = Inductive.type_of_inductive_knowing_parameters
+      (push_rel_context ctx (Global.env ()))
+	  oneind (Termops.extended_rel_vect 0 ctx)
+    in
+      { cl_impl = IndRef ind;
+	cl_context = List.map (const None) ctx, ctx;
+	cl_props = [Anonymous, None, ty];
+	cl_projs = [] }
+  in add_class k
+      
+(*
+ * interface functions
+ *)
+
+let class_info c =
   try Gmap.find c !classes
   with _ -> not_a_class (Global.env()) (constr_of_global c)
 
-let instance_constructor cl args = 
-  let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
+let instance_constructor cl args =
+  let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
+  let pars = fst (list_chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
 	  applistc (mkInd ind) pars
       | ConstRef cst -> list_last args, applistc (mkConst cst) pars
       | _ -> assert false
-	  
+
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
 
 let cmapl_add x y m =
   try
     let l = Gmap.find x m in
-    Gmap.add x (Cmap.add y.is_impl y l) m
+    Gmap.add x (Gmap.add y.is_impl y l) m
   with Not_found ->
-    Gmap.add x (Cmap.add y.is_impl y Cmap.empty) m
+    Gmap.add x (Gmap.add y.is_impl y Gmap.empty) m
 
-let cmap_elements c = Cmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = Gmap.fold (fun k v acc -> v :: acc) c []
 
-let instances_of c = 
+let instances_of c =
   try cmap_elements (Gmap.find c.cl_impl !instances) with Not_found -> []
 
-let add_instance i =
-  let cl = class_info i.is_class in
-  instances := cmapl_add cl.cl_impl i !instances;
-  add_instance_hint i.is_impl i.is_pri;
-  update ()
-
 let all_instances () = 
   Gmap.fold (fun k v acc -> 
-    Cmap.fold (fun k v acc -> v :: acc) v acc)
+    Gmap.fold (fun k v acc -> v :: acc) v acc)
     !instances []
 
 let instances r = 
-  let cl = class_info r in instances_of cl
-    
-let method_typeclass ref = 
-  match ref with 
-    | ConstRef c -> 
-	class_info (Gmap.find c !methods)
-    | _ -> raise Not_found
+  let cl = class_info r in instances_of cl    
       
 let is_class gr = 
   Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
-  
-let is_method c =
-  Gmap.mem c !methods
 
 let is_instance = function
   | ConstRef c ->
@@ -320,18 +313,20 @@ let is_instance = function
       (match Decls.variable_kind v with
       | IsDefinition Instance -> true
       | _ -> false)
+  | ConstructRef (ind,_) -> 
+      is_class (IndRef ind)
   | _ -> false
 
-let is_implicit_arg k = 
+let is_implicit_arg k =
   match k with
-      ImplicitArg (ref, (n, id)) -> true
+      ImplicitArg (ref, (n, id), b) -> true
     | InternalHole -> true
     | _ -> false
 
-let global_class_of_constr env c = 
+let global_class_of_constr env c =
   try class_info (global_of_constr c)
   with Not_found -> not_a_class env c
-      
+
 let dest_class_app env c =
   let cl, args = decompose_app c in
     global_class_of_constr env cl, args
@@ -339,49 +334,49 @@ let dest_class_app env c =
 let class_of_constr c = try Some (fst (dest_class_app (Global.env ()) c)) with _ -> None
 
 (* To embed a boolean for resolvability status.
-   This is essentially a hack to mark which evars correspond to 
-   goals and do not need to be resolved when we have nested [resolve_all_evars] 
+   This is essentially a hack to mark which evars correspond to
+   goals and do not need to be resolved when we have nested [resolve_all_evars]
    calls (e.g. when doing apply in an External hint in typeclass_instances).
    Would be solved by having real evars-as-goals. *)
 
 let ((bool_in : bool -> Dyn.t),
     (bool_out : Dyn.t -> bool)) = Dyn.create "bool"
-  
+
 let bool_false = bool_in false
 
 let is_resolvable evi =
   match evi.evar_extra with
       Some t -> if Dyn.tag t = "bool" then bool_out t else true
     | None -> true
-	
-let mark_unresolvable evi = 
+
+let mark_unresolvable evi =
   { evi with evar_extra = Some bool_false }
-    
+
 let mark_unresolvables sigma =
   Evd.fold (fun ev evi evs ->
     Evd.add evs ev (mark_unresolvable evi))
     sigma Evd.empty
-    
-let rec is_class_type c =
+
+let rec is_class_type evd c =
   match kind_of_term c with
-  | Prod (_, _, t) -> is_class_type t
+  | Prod (_, _, t) -> is_class_type evd t
+  | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
   | _ -> class_of_constr c <> None
 
-let is_class_evar evi = 
-  is_class_type evi.Evd.evar_concl
-    
+let is_class_evar evd evi =
+  is_class_type evd evi.Evd.evar_concl
+
 let has_typeclasses evd =
-  Evd.fold (fun ev evi has -> has || 
-    (evi.evar_body = Evar_empty && is_class_evar evi && is_resolvable evi))
+  Evd.fold (fun ev evi has -> has ||
+    (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd =
-  if not (has_typeclasses (Evd.evars_of evd)) then evd
-  else
-    !solve_instanciations_problem env evd onlyargs split fail
+  if not (has_typeclasses evd) then evd
+  else !solve_instanciations_problem env evd onlyargs split fail
 
 let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
-- 
cgit v1.2.3