From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- pretyping/typeclasses.ml | 109 +++++++++++++++++++++++++---------------------- 1 file changed, 57 insertions(+), 52 deletions(-) (limited to 'pretyping/typeclasses.ml') 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 -- cgit v1.2.3