diff options
Diffstat (limited to 'toplevel/assumptions.ml')
| -rw-r--r-- | toplevel/assumptions.ml | 126 |
1 files changed, 107 insertions, 19 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 2a3e6536..45c539e2 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -15,7 +15,7 @@ Module-traversing code: Pierre Letouzey *) open Pp -open Errors +open CErrors open Util open Names open Term @@ -23,6 +23,7 @@ open Declarations open Mod_subst open Globnames open Printer +open Context.Named.Declaration (** For a constant c in a module sealed by an interface (M:T and not M<:T), [Global.lookup_constant] may return a [constant_body] @@ -141,22 +142,20 @@ let label_of = function | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn) | VarRef id -> Label.of_id id -let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx - let rec traverse current ctx accu t = match kind_of_term t with | Var id -> - let body () = match Global.lookup_named id with (_, body, _) -> body in + let body () = Global.lookup_named id |> get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> let body () = Global.body_of_constant_body (lookup_constant kn) in traverse_object accu body (ConstRef kn) -| Ind (ind, _) -> - traverse_object accu (fun () -> None) (IndRef ind) -| Construct (cst, _) -> - traverse_object accu (fun () -> None) (ConstructRef cst) +| Ind ((mind, _) as ind, _) -> + traverse_inductive accu mind (IndRef ind) +| Construct (((mind, _), _) as cst, _) -> + traverse_inductive accu mind (ConstructRef cst) | Meta _ | Evar _ -> assert false | Case (_,oty,c,[||]) -> - (* non dependent match on an inductive with no constructors *) + (* non dependent match on an inductive with no constructors *) begin match Constr.(kind oty, kind c) with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && @@ -165,9 +164,11 @@ let rec traverse current ctx accu t = match kind_of_term t with traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - Termops.fold_constr_with_full_binders push (traverse current) ctx accu t + Termops.fold_constr_with_full_binders + Context.Rel.add (traverse current) ctx accu t end -| _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t +| _ -> Termops.fold_constr_with_full_binders + Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = let data, ax2ty = @@ -185,14 +186,87 @@ and traverse_object ?inhabits (curr, data, ax2ty) body obj = | Some body -> if already_in then data, ax2ty else let contents,data,ax2ty = - traverse (label_of obj) [] (Refset_env.empty,data,ax2ty) body in + traverse (label_of obj) Context.Rel.empty + (Refset_env.empty,data,ax2ty) body in Refmap_env.add obj contents data, ax2ty in (Refset_env.add obj curr, data, ax2ty) +(** Collects the references occurring in the declaration of mutual inductive + definitions. All the constructors and names of a mutual inductive + definition share exactly the same dependencies. Also, there is no explicit + dependency between mutually defined inductives and constructors. *) +and traverse_inductive (curr, data, ax2ty) mind obj = + let firstind_ref = (IndRef (mind, 0)) in + let label = label_of obj in + let data, ax2ty = + (* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data + where I_0, I_1, ... are in the same mutual definition and c_ij + are all their constructors. *) + if Refmap_env.mem firstind_ref data then data, ax2ty else + let mib = Global.lookup_mind mind in + (* Collects references of parameters *) + let param_ctx = mib.mind_params_ctxt in + let nparam = List.length param_ctx in + let accu = + traverse_context label Context.Rel.empty + (Refset_env.empty, data, ax2ty) param_ctx + in + (* Build the context of all arities *) + let arities_ctx = + let global_env = Global.env () in + Array.fold_left (fun accu oib -> + let pspecif = Univ.in_punivs (mib, oib) in + let ind_type = Inductive.type_of_inductive global_env pspecif in + let ind_name = Name oib.mind_typename in + Context.Rel.add (Context.Rel.Declaration.LocalAssum (ind_name, ind_type)) accu) + Context.Rel.empty mib.mind_packets + in + (* For each inductive, collects references in their arity and in the type + of constructors*) + let (contents, data, ax2ty) = Array.fold_left (fun accu oib -> + let arity_wo_param = + List.rev (List.skipn nparam (List.rev oib.mind_arity_ctxt)) + in + let accu = + traverse_context + label param_ctx accu arity_wo_param + in + Array.fold_left (fun accu cst_typ -> + let param_ctx, cst_typ_wo_param = Term.decompose_prod_n_assum nparam cst_typ in + let ctx = Context.(Rel.fold_outside Context.Rel.add ~init:arities_ctx param_ctx) in + traverse label ctx accu cst_typ_wo_param) + accu oib.mind_user_lc) + accu mib.mind_packets + in + (* Maps all these dependencies to inductives and constructors*) + let data = Array.fold_left_i (fun n data oib -> + let ind = (mind, n) in + let data = Refmap_env.add (IndRef ind) contents data in + Array.fold_left_i (fun k data _ -> + Refmap_env.add (ConstructRef (ind, k+1)) contents data + ) data oib.mind_consnames) data mib.mind_packets + in + data, ax2ty + in + (Refset_env.add obj curr, data, ax2ty) + +(** Collects references in a rel_context. *) +and traverse_context current ctx accu ctxt = + snd (Context.Rel.fold_outside (fun decl (ctx, accu) -> + match decl with + | Context.Rel.Declaration.LocalDef (_,c,t) -> + let accu = traverse current ctx (traverse current ctx accu t) c in + let ctx = Context.Rel.add decl ctx in + ctx, accu + | Context.Rel.Declaration.LocalAssum (_,t) -> + let accu = traverse current ctx accu t in + let ctx = Context.Rel.add decl ctx in + ctx, accu) ctxt ~init:(ctx, accu)) + let traverse current t = let () = modcache := MPmap.empty in - traverse current [] (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t + traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t (** Hopefully bullet-proof function to recover the type of a constant. It just ignores all the universe stuff. There are many issues that can arise when @@ -208,15 +282,23 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let (_, graph, ax2ty) = traverse (label_of gr) t in let fold obj _ accu = match obj with | VarRef id -> - let (_, body, t) = Global.lookup_named id in - if Option.is_empty body then ContextObjectMap.add (Variable id) t accu + let decl = Global.lookup_named id in + if is_local_assum decl then + let t = Context.Named.Declaration.get_type decl in + ContextObjectMap.add (Variable id) t accu else accu | ConstRef kn -> - let cb = lookup_constant kn in - if not (Declareops.constant_has_body cb) then + let cb = lookup_constant kn in + let accu = + if cb.const_typing_flags.check_guarded then accu + else + let l = try Refmap_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu + in + if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then let t = type_of_constant cb in let l = try Refmap_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (kn,l)) t accu + ContextObjectMap.add (Axiom (Constant kn,l)) t accu else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu @@ -225,6 +307,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = ContextObjectMap.add (Transparent kn) t accu else accu - | IndRef _ | ConstructRef _ -> accu + | IndRef (m,_) | ConstructRef ((m,_),_) -> + let mind = Global.lookup_mind m in + if mind.mind_typing_flags.check_guarded then + accu + else + let l = try Refmap_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu in Refmap_env.fold fold graph ContextObjectMap.empty |