summaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml109
1 files changed, 57 insertions, 52 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 86168a1f..8680e578 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: typeclasses.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -35,25 +35,24 @@ type typeclass = {
cl_impl : global_reference;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : ((global_reference * bool) option * rel_declaration) list;
+ 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) list;
+ cl_projs : (identifier * constant option) list;
}
type typeclasses = (global_reference, typeclass) Gmap.t
-type globality = int option
-
type instance = {
is_class: global_reference;
is_pri: int option;
- is_global: globality;
(* Sections where the instance should be redeclared,
- Some n for n sections, None for discard at end of section. *)
+ -1 for discard, 0 for none, mutable to avoid redeclarations
+ when multiple rebuild_object happen. *)
+ is_global: int ref;
is_impl: constant;
}
@@ -64,13 +63,13 @@ let instance_impl is = is.is_impl
let new_instance cl pri glob impl =
let global =
if Lib.sections_are_opened () then
- if glob then Some (Lib.sections_depth ())
- else None
- else Some 0
+ if glob then Lib.sections_depth ()
+ else -1
+ else 0
in
{ is_class = cl.cl_impl;
is_pri = pri ;
- is_global = global ;
+ is_global = ref global ;
is_impl = impl }
let classes : typeclasses ref = ref Gmap.empty
@@ -112,7 +111,7 @@ let gmap_cmap_merge old ne =
ne Gmap.empty
in
Gmap.fold (fun cl insts acc ->
- if Gmap.mem cl ne' then acc
+ if Gmap.mem cl acc then acc
else Gmap.add cl insts acc)
old ne'
@@ -138,23 +137,21 @@ let subst (_,subst,(cl,m,inst)) =
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr)
in
- let do_subst_named ctx =
+ 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_ctx ctx =
- list_smartmap (fun (cl, (na, b, t)) ->
- (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b) cl,
- (na, Option.smartmap do_subst b, do_subst t)))
- ctx
+ let do_subst_context (grs,ctx) =
+ list_smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
+ do_subst_ctx ctx
in
- let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs 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_ctx cl.cl_context;
- cl_props = do_subst_named cl.cl_props;
+ 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
@@ -173,14 +170,18 @@ let subst (_,subst,(cl,m,inst)) =
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)) =
- let discharge_context subst rel =
+ let discharge_rel_context subst n rel =
let ctx, _ =
List.fold_right
- (fun (gr, (id, b, t)) (ctx, k) ->
- let gr' = Option.map (fun (gr, b) -> Lib.discharge_global gr, b) gr in
- ((gr', (id, Option.map (substn_vars k subst) b, substn_vars k subst t)) :: ctx), succ k)
- rel ([], 0)
+ (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 =
@@ -189,17 +190,22 @@ let discharge (_,(cl,m,inst)) =
| 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 @
+ 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
- { cl with cl_impl = cl_impl';
- cl_context =
- List.map (fun (na,impl,b,t) -> None, (Name na,b,t)) ctx @
- (discharge_context (List.map (fun (na, _, _, _) -> na) ctx) cl.cl_context);
- cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
+ 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
@@ -220,13 +226,13 @@ let rebuild (cl,m,inst) =
let inst =
Gmap.map (fun insts ->
Cmap.fold (fun k is insts ->
- match is.is_global with
- | None -> insts
- | Some 0 -> Cmap.add k is insts
- | Some n ->
+ match !(is.is_global) with
+ | -1 -> insts
+ | 0 -> Cmap.add k is insts
+ | n ->
add_instance_hint is.is_impl is.is_pri;
- let is' = { is with is_global = Some (pred n) }
- in Cmap.add k is' insts) insts Cmap.empty)
+ is.is_global := pred n;
+ Cmap.add k is insts) insts Cmap.empty)
inst
in (cl, m, inst)
@@ -247,7 +253,10 @@ let update () =
let add_class c =
classes := Gmap.add c.cl_impl c !classes;
- methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs;
+ 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 ()
let class_info c =
@@ -255,7 +264,7 @@ let class_info c =
with _ -> not_a_class (Global.env()) (constr_of_global c)
let instance_constructor cl args =
- let pars = fst (list_chop (List.length cl.cl_context) args) in
+ let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
match cl.cl_impl with
| IndRef ind -> applistc (mkConstruct (ind, 1)) args,
applistc (mkInd ind) pars
@@ -319,19 +328,15 @@ let is_implicit_arg k =
| InternalHole -> true
| _ -> false
-let class_of_constr c =
- let extract_cl c =
- try Some (class_info (global_of_constr c)) with _ -> None
- in
- match kind_of_term c with
- App (c, _) -> extract_cl c
- | _ -> extract_cl c
-
-let dest_class_app c =
- let cl c = class_info (global_of_constr c) in
- match kind_of_term c with
- App (c, args) -> cl c, args
- | _ -> cl 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
+
+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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 21:58:05 +0000