diff options
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | pretyping/termops.ml | 15 | ||||
| -rw-r--r-- | pretyping/termops.mli | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 44 | ||||
| -rw-r--r-- | printing/printer.mli | 16 | ||||
| -rw-r--r-- | toplevel/assumptions.ml (renamed from library/assumptions.ml) | 91 | ||||
| -rw-r--r-- | toplevel/assumptions.mli (renamed from library/assumptions.mli) | 23 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
10 files changed, 127 insertions, 75 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 74f36f6f5..07b48ed57 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -110,7 +110,6 @@ Loadpath Goptions Decls Heads -Assumptions Keys Locusops Miscops @@ -204,6 +203,7 @@ Hints Himsg Cerrors Locality +Assumptions Vernacinterp Dischargedhypsmap Discharge diff --git a/library/library.mllib b/library/library.mllib index eca28c822..920657365 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -16,5 +16,4 @@ Dischargedhypsmap Goptions Decls Heads -Assumptions Keys diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9f04faa83..937471cf7 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -453,26 +453,29 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_binders g f n acc c = match kind_of_term c with +let fold_constr_with_full_binders g f n acc c = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (_,t,c) -> f (g n) (f n acc t) c - | Lambda (_,t,c) -> f (g n) (f n acc t) c - | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = iterate g (Array.length tl) n in + let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = iterate g (Array.length tl) n in + let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd +let fold_constr_with_binders g f n acc c = + fold_constr_with_full_binders (fun _ x -> g x) f n acc c + (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at each binder traversal; it is not recursive and the order with which diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2552c67e6..4581e2310 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -84,6 +84,10 @@ val map_constr_with_full_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b +val fold_constr_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + val iter_constr_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 652542825..33b95c2f5 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -713,7 +713,33 @@ let prterm = pr_lconstr (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) -open Assumptions +type context_object = + | Variable of Id.t (* A section variable or a Let definition *) + | Axiom of constant * (Label.t * Context.rel_context * types) list + | Opaque of constant (* An opaque constant. *) + | Transparent of constant + +(* Defines a set of [assumption] *) +module OrderedContextObject = +struct + type t = context_object + let compare x y = + match x , y with + | Variable i1 , Variable i2 -> Id.compare i1 i2 + | Axiom (k1,_) , Axiom (k2, _) -> con_ord k1 k2 + | Opaque k1 , Opaque k2 -> con_ord k1 k2 + | Transparent k1 , Transparent k2 -> con_ord k1 k2 + | Axiom _ , Variable _ -> 1 + | Opaque _ , Variable _ + | Opaque _ , Axiom _ -> 1 + | Transparent _ , Variable _ + | Transparent _ , Axiom _ + | Transparent _ , Opaque _ -> 1 + | _ , _ -> -1 +end + +module ContextObjectSet = Set.Make (OrderedContextObject) +module ContextObjectMap = Map.Make (OrderedContextObject) let pr_assumptionset env s = if ContextObjectMap.is_empty s then @@ -729,15 +755,29 @@ let pr_assumptionset env s = try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in + let safe_pr_ltype_relctx (rctx, typ) = + let sigma, env = get_current_context () in + let env = Environ.push_rel_context rctx env in + try str " " ++ pr_ltype_env env sigma typ + with e when Errors.noncritical e -> mt () + in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) - | Axiom kn -> + | Axiom (kn,[]) -> let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in (v, ax :: a, o, tr) + | Axiom (kn,l) -> + let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++ + cut() ++ + prlist_with_sep cut (fun (lbl, ctx, ty) -> + str " used in " ++ str (Names.Label.to_string lbl) ++ + str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) + l in + (v, ax :: a, o, tr) | Opaque kn -> let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in (v, a, opq :: o, tr) diff --git a/printing/printer.mli b/printing/printer.mli index a469a8dbe..5f56adbe6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -160,10 +160,20 @@ val emacs_str : string -> string val prterm : constr -> std_ppcmds (** = pr_lconstr *) -(** spiwack: printer function for sets of Environ.assumption. - It is used primarily by the Print Assumption command. *) +(** Declarations for the "Print Assumption" command *) +type context_object = + | Variable of Id.t (** A section variable or a Let definition *) + (** An axiom and the type it inhabits (if an axiom of the empty type) *) + | Axiom of constant * (Label.t * Context.rel_context * types) list + | Opaque of constant (** An opaque constant. *) + | Transparent of constant (** A transparent constant *) + +module ContextObjectSet : Set.S with type elt = context_object +module ContextObjectMap : CMap.ExtS + with type key = context_object and module Set := ContextObjectSet + val pr_assumptionset : - env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds + env -> Term.types ContextObjectMap.t -> std_ppcmds val pr_goal_by_id : string -> std_ppcmds diff --git a/library/assumptions.ml b/toplevel/assumptions.ml index 62645b236..fff7e2e21 100644 --- a/library/assumptions.ml +++ b/toplevel/assumptions.ml @@ -22,34 +22,7 @@ open Term open Declarations open Mod_subst open Globnames - -type context_object = - | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | Opaque of constant (* An opaque constant. *) - | Transparent of constant - -(* Defines a set of [assumption] *) -module OrderedContextObject = -struct - type t = context_object - let compare x y = - match x , y with - | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> con_ord k1 k2 - | Opaque k1 , Opaque k2 -> con_ord k1 k2 - | Transparent k1 , Transparent k2 -> con_ord k1 k2 - | Axiom _ , Variable _ -> 1 - | Opaque _ , Variable _ - | Opaque _ , Axiom _ -> 1 - | Transparent _ , Variable _ - | Transparent _ , Axiom _ - | Transparent _ , Opaque _ -> 1 - | _ , _ -> -1 -end - -module ContextObjectSet = Set.Make (OrderedContextObject) -module ContextObjectMap = Map.Make (OrderedContextObject) +open Printer (** 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] @@ -161,7 +134,16 @@ let lookup_constant cst = (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) -let rec traverse accu t = match kind_of_term t with + +let label_of = function + | ConstRef kn -> pi3 (repr_con kn) + | IndRef (kn,_) + | 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 traverse_object accu body (VarRef id) @@ -173,22 +155,42 @@ let rec traverse accu t = match kind_of_term t with | Construct (cst, _) -> traverse_object accu (fun () -> None) (ConstructRef cst) | Meta _ | Evar _ -> assert false -| _ -> Constr.fold traverse accu t - -and traverse_object (curr, data) body obj = - let data = - if Refmap.mem obj data then data - else match body () with - | None -> Refmap.add obj Refset.empty data +| Case (_,oty,c,[||]) -> + (* non dependent match on an inductive with no constructors *) + begin match Constr.(kind oty, kind c) with + | Lambda(Anonymous,_,oty), Const (kn, _) + when Vars.noccurn 1 oty && + not (Declareops.constant_has_body (lookup_constant kn)) -> + let body () = Global.body_of_constant_body (lookup_constant kn) in + 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 + end +| _ -> Termops.fold_constr_with_full_binders push (traverse current) ctx accu t + +and traverse_object ?inhabits (curr, data, ax2ty) body obj = + let data, ax2ty = + let already_in = Refmap.mem obj data in + match body () with + | None -> + let data = + if not already_in then Refmap.add obj Refset.empty data else data in + let ax2ty = + if Option.is_empty inhabits then ax2ty else + let ty = Option.get inhabits in + try let l = Refmap.find obj ax2ty in Refmap.add obj (ty::l) ax2ty + with Not_found -> Refmap.add obj [ty] ax2ty in + data, ax2ty | Some body -> - let (contents, data) = traverse (Refset.empty, data) body in - Refmap.add obj contents data + let contents,data,ax2ty = + traverse (label_of obj) [] (Refset.empty,data,ax2ty) body in + Refmap.add obj contents data, ax2ty in - (Refset.add obj curr, data) + (Refset.add obj curr, data, ax2ty) -let traverse t = +let traverse current t = let () = modcache := MPmap.empty in - traverse (Refset.empty, Refmap.empty) t + traverse current [] (Refset.empty, Refmap.empty, Refmap.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 @@ -198,10 +200,10 @@ let type_of_constant cb = match cb.Declarations.const_type with | Declarations.TemplateArity (ctx, arity) -> Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) -let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = +let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let (idts, knst) = st in (** Only keep the transitive dependencies *) - let (_, graph) = traverse t in + 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 @@ -211,7 +213,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = let cb = lookup_constant kn in if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in - ContextObjectMap.add (Axiom kn) t accu + let l = try Refmap.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (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 diff --git a/library/assumptions.mli b/toplevel/assumptions.mli index bb36a9725..a608fe505 100644 --- a/library/assumptions.mli +++ b/toplevel/assumptions.mli @@ -10,19 +10,7 @@ open Util open Names open Term open Globnames - -(** A few declarations for the "Print Assumption" command - @author spiwack *) -type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - | Axiom of constant (** An axiom or a constant. *) - | Opaque of constant (** An opaque constant. *) - | Transparent of constant (** A transparent constant *) - -(** AssumptionSet.t is a set of [assumption] *) -module ContextObjectSet : Set.S with type elt = context_object -module ContextObjectMap : Map.ExtS - with type key = context_object and module Set := ContextObjectSet +open Printer (** Collects all the objects on which a term directly relies, bypassing kernel opacity, together with the recursive dependence DAG of objects. @@ -31,11 +19,14 @@ module ContextObjectMap : Map.ExtS sealed inside opaque modules. Do not try to do anything fancy with those terms apart from printing them, otherwise demons may fly out of your nose. *) -val traverse : constr -> (Refset.t * Refset.t Refmap.t) +val traverse : + Label.t -> constr -> + (Refset.t * Refset.t Refmap.t * + (label * Context.rel_context * types) list Refmap.t) (** Collects all the assumptions (optionally including opaque definitions) on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr -> - Term.types ContextObjectMap.t + ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> + global_reference -> constr -> Term.types ContextObjectMap.t diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index bf0f305ab..5aa7d428a 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -10,6 +10,7 @@ Obligations Command Classes Record +Assumptions Vernacinterp Mltop Vernacentries diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2af28de98..6c5f10c20 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1663,10 +1663,11 @@ let vernac_print = function dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) - let cstr = printable_constr_of_global (smart_global r) in + let gr = smart_global r in + let cstr = printable_constr_of_global gr in let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = - Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in + Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) | PrintStrategy r -> print_strategy r |