summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /toplevel
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml12
-rw-r--r--toplevel/classes.ml343
-rw-r--r--toplevel/classes.mli27
-rw-r--r--toplevel/command.ml166
-rw-r--r--toplevel/command.mli12
-rw-r--r--toplevel/coqinit.ml27
-rw-r--r--toplevel/coqtop.ml58
-rw-r--r--toplevel/himsg.ml92
-rw-r--r--toplevel/metasyntax.ml65
-rw-r--r--toplevel/metasyntax.mli6
-rw-r--r--toplevel/mltop.ml4100
-rw-r--r--toplevel/mltop.mli19
-rw-r--r--toplevel/protectedtoplevel.ml9
-rw-r--r--toplevel/record.ml186
-rw-r--r--toplevel/record.mli17
-rw-r--r--toplevel/toplevel.ml10
-rw-r--r--toplevel/usage.ml19
-rw-r--r--toplevel/usage.mli7
-rw-r--r--toplevel/vernac.ml72
-rw-r--r--toplevel/vernacentries.ml289
-rw-r--r--toplevel/vernacexpr.ml131
21 files changed, 883 insertions, 784 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 49b9ce7a..82709db4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto_ind_decl.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: auto_ind_decl.ml 11671 2008-12-12 12:43:03Z herbelin $ i*)
open Tacmach
open Util
@@ -530,13 +530,13 @@ let compute_bl_tact ind lnamesparrec nparrec =
tclORELSE reflexivity (Equality.discr_tac false None)
);
simpl_in_hyp
- ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
+ ((Rawterm.all_occurrences_expr,freshz),InHyp);
(*
repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
tclREPEAT (
tclTHENSEQ [
- apply_in false freshz [(andb_prop()),Rawterm.NoBindings];
+ apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
fun gl ->
let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
in
@@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
Pfedit.by ( tclTHENSEQ [
intros_using fresh_first_intros;
intros_using [freshn;freshm];
- assert_as true (dl,Genarg.IntroIdentifier freshH) (
- mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+ assert_tac (Name freshH) (
+ mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
) ]);
(*we do this so we don't have to prove the same goal twice *)
Pfedit.by ( tclTHEN
@@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
unfold_constr (Lazy.force Coqlib.coq_not_ref);
intro;
Equality.subst_all;
- assert_as true (dl,Genarg.IntroIdentifier freshH3)
+ assert_tac (Name freshH3)
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
]);
Pfedit.by
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 511befd8..04945040 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: classes.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: classes.ml 11800 2009-01-18 18:34:15Z msozeau $ i*)
(*i*)
open Names
@@ -32,19 +32,23 @@ open Topconstr
open Decl_kinds
open Entries
-let hint_db = "typeclass_instances"
+let typeclasses_db = "typeclass_instances"
let qualid_of_con c =
Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+let set_rigid c =
+ Auto.add_hints false [typeclasses_db]
+ (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
+
let _ =
Typeclasses.register_add_instance_hint
(fun inst pri ->
Flags.silently (fun () ->
- Auto.add_hints false [hint_db]
+ Auto.add_hints false [typeclasses_db]
(Vernacexpr.HintsResolve
- [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
-
+ [pri, false, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
+
let declare_instance_cst glob con =
let instance = Typeops.type_of_constant (Global.env ()) con in
let _, r = decompose_prod_assum instance in
@@ -67,207 +71,27 @@ type binder_list = (identifier located * bool * constr_expr) list
(* Calls to interpretation functions. *)
-let interp_binders_evars isevars env avoid l =
- List.fold_left
- (fun (env, ids, params) ((loc, i), t) ->
- let n = Name i in
- let t' = interp_binder_evars isevars env n t in
- let d = (i,None,t') in
- (push_named d env, i :: ids, d::params))
- (env, avoid, []) l
-
-let interp_typeclass_context_evars isevars env avoid l =
- List.fold_left
- (fun (env, ids, params) (iid, bk, l) ->
- let t' = interp_binder_evars isevars env (snd iid) l in
- let i = match snd iid with
- | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids
- | Name id -> id
- in
- let d = (i,None,t') in
- (push_named d env, i :: ids, d::params))
- (env, avoid, []) l
-
let interp_type_evars evdref env ?(impls=([],[])) typ =
let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
-
-let mk_interning_data env na impls typ =
- let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
- in (na, ([], impl, Notation.compute_arguments_scope typ))
-let interp_fields_evars isevars env avoid l =
- List.fold_left
- (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) ->
- let impl, t' = interp_type_evars isevars env ~impls t in
- let data = mk_interning_data env i impl t' in
- let d = (Name i,None,t') in
- (push_rel d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
- (env, [], avoid, [], ([], [])) l
-
(* Declare everything in the parameters as implicit, and the class instance as well *)
open Topconstr
-
-let implicits_of_context ctx =
- list_map_i (fun i name ->
- let explname =
- match name with
- | Name n -> Some n
- | Anonymous -> None
- in ExplByPos (i, explname), (true, true))
- 1 (List.rev (Anonymous :: (List.map pi1 ctx)))
-
-let degenerate_decl (na,b,t) =
- let id = match na with
- | Name id -> id
- | Anonymous -> anomaly "Unnamed record variable" in
- match b with
- | None -> (id, Entries.LocalAssum t)
- | Some b -> (id, Entries.LocalDef b)
-
-let name_typeclass_binder avoid = function
- | LocalRawAssum ([loc, Anonymous], bk, c) ->
- let name =
- let id =
- match c with
- CApp (_, (_, CRef (Ident (loc,id))), _) -> id
- | _ -> id_of_string "assum"
- in Implicit_quantifiers.make_fresh avoid (Global.env ()) id
- in LocalRawAssum ([loc, Name name], bk, c), Idset.add name avoid
- | x -> x, avoid
-
-let name_typeclass_binders avoid l =
- let l', avoid =
- List.fold_left
- (fun (binders, avoid) b -> let b', avoid = name_typeclass_binder avoid b in
- b' :: binders, avoid)
- ([], avoid) l
- in List.rev l', avoid
-
-let new_class id par ar sup props =
- let env0 = Global.env() in
- let isevars = ref (Evd.create_evar_defs Evd.empty) in
- let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env0) in
- let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in
- let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in
- let sup, bound = name_typeclass_binders bound sup in
- let supnames =
- List.fold_left (fun acc b ->
- match b with
- LocalRawAssum (nl, _, _) -> nl @ acc
- | LocalRawDef _ -> assert(false))
- [] sup
- in
-
- (* Interpret the arity *)
- let arity_imps, fullarity =
- let ar =
- match ar with
- Some ar -> ar | None -> (dummy_loc, Rawterm.RType None)
- in
- let arity = CSort (fst ar, snd ar) in
- let term = prod_constr_expr (prod_constr_expr arity par) sup in
- interp_type_evars isevars env0 term
- in
- let ctx_params, arity = decompose_prod_assum fullarity in
- let env_params = push_rel_context ctx_params env0 in
- (* Interpret the definitions and propositions *)
- let env_props, prop_impls, bound, ctx_props, _ =
- interp_fields_evars isevars env_params bound props
- in
- let subs = List.map (fun ((loc, id), b, _) -> b) props in
- (* Instantiate evars and check all are resolved *)
- let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
- let isevars = Typeclasses.resolve_typeclasses env_props isevars in
- let sigma = Evd.evars_of isevars in
- let ctx_params = Evarutil.nf_rel_context_evar sigma ctx_params in
- let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in
- let arity = Reductionops.nf_evar sigma arity in
- let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
- let fieldimpls =
- (* Make the class and all params implicits in the projections *)
- let ctx_impls = implicits_of_context ctx_params in
- let len = succ (List.length ctx_params) in
- List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
- in
- let impl, projs =
- let params = ctx_params and fields = ctx_props in
- List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
- match fields with
- [(Name proj_name, _, field)] ->
- let class_body = it_mkLambda_or_LetIn field params in
- let class_type =
- match ar with
- Some _ -> Some (it_mkProd_or_LetIn arity params)
- | None -> None
- in
- let class_entry =
- { const_entry_body = class_body;
- const_entry_type = class_type;
- const_entry_opaque = false;
- const_entry_boxed = false }
- in
- let cst = Declare.declare_constant (snd id)
- (DefinitionEntry class_entry, IsDefinition Definition)
- in
- let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
- let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
- let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
- let proj_entry =
- { const_entry_body = proj_body;
- const_entry_type = Some proj_type;
- const_entry_opaque = false;
- const_entry_boxed = false }
- in
- let proj_cst = Declare.declare_constant proj_name
- (DefinitionEntry proj_entry, IsDefinition Definition)
- in
- let cref = ConstRef cst in
- Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
- Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
- cref, [proj_name, proj_cst]
- | _ ->
- let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
- let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
- let kn = Record.declare_structure (snd id) idb arity_imps
- params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
- in
- IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
- fields (Recordops.lookup_projections (kn,0)))
- in
- let ctx_context =
- List.map (fun ((na, b, t) as d) ->
- match Typeclasses.class_of_constr t with
- | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d)
- | None -> (None, d))
- ctx_params
- in
- let k =
- { cl_impl = impl;
- cl_context = ctx_context;
- cl_props = ctx_props;
- cl_projs = projs }
- in
- List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p))
- k.cl_projs subs;
- add_class k
-
-type binder_def_list = (identifier located * identifier located list * constr_expr) list
-
-let binders_of_lidents l =
- List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
-
let type_ctx_instance isevars env ctx inst subst =
let (s, _) =
List.fold_left2
- (fun (subst, instctx) (na, _, t) ce ->
+ (fun (subst, instctx) (na, b, t) ce ->
let t' = substl subst t in
- let c = interp_casted_constr_evars isevars env ce t' in
- let d = na, Some c, t' in
- c :: subst, d :: instctx)
+ let c' =
+ match b with
+ | None -> interp_casted_constr_evars isevars env ce t'
+ | Some b -> substl subst b
+ in
+ let d = na, Some c', t' in
+ c' :: subst, d :: instctx)
(subst, []) (List.rev ctx) inst
in s
@@ -284,27 +108,10 @@ let id_of_class cl =
open Pp
let ($$) g f = fun x -> g (f x)
-
-let default_on_free_vars =
- Flags.if_verbose
- (fun fvs ->
- match fvs with
- [] -> ()
- | l -> msgnl (str"Implicitly generalizing " ++
- prlist_with_sep (fun () -> str", ") Nameops.pr_id l ++ str"."))
-
-let fail_on_free_vars = function
- [] -> ()
- | [fv] ->
- errorlabstrm "Classes"
- (str"Unbound variable " ++ Nameops.pr_id fv ++ str".")
- | fvs -> errorlabstrm "Classes"
- (str"Unbound variables " ++
- prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".")
let instance_hook k pri global imps ?hook cst =
let inst = Typeclasses.new_instance k pri global cst in
- Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+ Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps;
Typeclasses.add_instance inst;
(match hook with Some h -> h cst | None -> ())
@@ -323,51 +130,30 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
instance_hook k pri global imps ?hook kn;
id
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars)
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
let env = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
- let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
- let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
let tclass =
match bk with
- | Implicit ->
- let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
- let k = class_info (Nametab.global id) in
- let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
- let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
- if needlen <> applen then
- mismatched_params env (List.map fst par) (List.map snd k.cl_context);
- let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
- (fun avoid (clname, (id, _, t)) ->
- match clname with
- Some (cl, b) ->
- let t =
- if b then
- let _k = class_info cl in
- CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None))))
- else CHole (Util.dummy_loc, None)
- in t, avoid
- | None -> failwith ("new instance: under-applied typeclass"))
- par (List.rev k.cl_context)
- in Topconstr.CAppExpl (loc, (None, id), pars)
-
- | Explicit -> cl
+ | Implicit ->
+ Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
+ (fun avoid (clname, (id, _, t)) ->
+ match clname with
+ | Some (cl, b) ->
+ let t = CHole (Util.dummy_loc, None) in
+ t, avoid
+ | None -> failwith ("new instance: under-applied typeclass"))
+ cl
+ | Explicit -> cl
in
- let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
- let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
- on_free_vars (List.rev fvs @ List.rev gen_ids);
- let gen_idset = Implicit_quantifiers.ids_of_list gen_ids in
- let bound = Idset.union gen_idset ctx_bound in
- let gen_ctx = Implicit_quantifiers.binder_list_of_ids gen_ids in
- let ctx, avoid = name_typeclass_binders bound ctx in
- let ctx = List.append ctx (List.rev gen_ctx) in
+ let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
let k, ctx', imps, subst =
let c = Command.generalize_constr_expr tclass ctx in
let imps, c' = interp_type_evars isevars env c in
let ctx, c = decompose_prod_assum c' in
- let cl, args = Typeclasses.dest_class_app c in
- cl, ctx, imps, List.rev (Array.to_list args)
+ let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
+ cl, ctx, imps, List.rev args
in
let id =
match snd instid with
@@ -384,7 +170,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses env !isevars;
let sigma = Evd.evars_of !isevars in
- let substctx = List.map (Evarutil.nf_evar sigma) subst in
+ let subst = List.map (Evarutil.nf_evar sigma) subst in
if Lib.is_modtype () then
begin
let _, ty_constr = instance_constructor k (List.rev subst) in
@@ -399,31 +185,48 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
end
else
begin
+ let props =
+ match props with
+ | CRecord (loc, _, fs) ->
+ if List.length fs > List.length k.cl_props then
+ mismatched_props env' (List.map snd fs) k.cl_props;
+ fs
+ | _ ->
+ if List.length k.cl_props <> 1 then
+ errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
+ else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
+ in
let subst =
- let props =
- List.map (fun (x, l, d) ->
- x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
- props
- in
- if List.length props > List.length k.cl_props then
- mismatched_props env' (List.map snd props) k.cl_props;
- let props, rest =
- List.fold_left
- (fun (props, rest) (id,_,_) ->
- try
- let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
- let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
- Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
- c :: props, rest'
- with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
- ([], props) k.cl_props
- in
- if rest <> [] then
- unbound_method env' k.cl_impl (fst (List.hd rest))
- else
- type_ctx_instance isevars env' k.cl_props props substctx
+ match k.cl_props with
+ | [(na,b,ty)] ->
+ let term = match props with [] -> CHole (Util.dummy_loc, None)
+ | [(_,f)] -> f | _ -> assert false in
+ let ty' = substl subst ty in
+ let c = interp_casted_constr_evars isevars env' term ty' in
+ c :: subst
+ | _ ->
+ let props, rest =
+ List.fold_left
+ (fun (props, rest) (id,b,_) ->
+ try
+ let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+ let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
+ Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+ c :: props, rest'
+ with Not_found ->
+ (CHole (Util.dummy_loc, None) :: props), rest)
+ ([], props) k.cl_props
+ in
+ if rest <> [] then
+ unbound_method env' k.cl_impl (fst (List.hd rest))
+ else
+ type_ctx_instance isevars env' k.cl_props props subst
+ in
+ let subst = List.fold_left2
+ (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+ [] subst (k.cl_props @ snd k.cl_context)
in
- let app, ty_constr = instance_constructor k (List.rev subst) in
+ let app, ty_constr = instance_constructor k subst in
let termtype =
let t = it_mkProd_or_LetIn ty_constr ctx' in
Evarutil.nf_isevar !isevars t
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index f149ac72..1bbf29a6 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: classes.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
(*i*)
open Names
@@ -29,27 +29,6 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
val mismatched_props : env -> constr_expr list -> rel_context -> 'a
-type binder_list = (identifier located * bool * constr_expr) list
-type binder_def_list = (identifier located * identifier located list * constr_expr) list
-
-val binders_of_lidents : identifier located list -> local_binder list
-
-val name_typeclass_binders : Idset.t ->
- Topconstr.local_binder list ->
- Topconstr.local_binder list * Idset.t
-
-val new_class : identifier located ->
- local_binder list ->
- Vernacexpr.sort_expr located option ->
- local_binder list ->
- binder_list -> unit
-
-(* By default, print the free variables that are implicitely generalized. *)
-
-val default_on_free_vars : identifier list -> unit
-
-val fail_on_free_vars : identifier list -> unit
-
(* Instance declaration *)
val declare_instance : bool -> identifier located -> unit
@@ -69,8 +48,8 @@ val new_instance :
?global:bool -> (* Not global by default. *)
local_binder list ->
typeclass_constraint ->
- binder_def_list ->
- ?on_free_vars:(identifier list -> unit) ->
+ constr_expr ->
+ ?generalize:bool ->
?tac:Proof_type.tactic ->
?hook:(constant -> unit) ->
int option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3688c347..b50c9bbd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: command.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
open Pp
open Util
@@ -136,7 +136,7 @@ let red_constant_entry bl ce = function
let declare_global_definition ident ce local imps =
let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
if local = Local && Flags.is_verbose() then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
@@ -166,8 +166,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
hook local r
let syntax_definition ident (vars,c) local onlyparse =
- let pat = interp_aconstr [] vars c in
- Syntax_def.declare_syntactic_definition local ident onlyparse pat
+ let ((vars,_),pat) = interp_aconstr [] (vars,[]) c in
+ let onlyparse = onlyparse or Metasyntax.is_not_printable pat in
+ Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -189,7 +190,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) =
let kn =
declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
assumption_message ident;
if local=Local & Flags.is_verbose () then
msg_warning (pr_id ident ++ str" is declared as a parameter" ++
@@ -339,13 +340,26 @@ let (inDec,outDec) =
let start_hook = ref ignore
let set_start_hook = (:=) start_hook
-let start_proof id kind c ?init_tac hook =
+let start_proof id kind c ?init_tac ?(compute_guard=false) hook =
let sign = Global.named_context () in
let sign = clear_proofs sign in
!start_hook c;
- Pfedit.start_proof id kind sign c ?init_tac:init_tac hook
-
-let save id const (locality,kind) hook =
+ Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
+
+let adjust_guardness_conditions const =
+ (* Try all combinations... not optimal *)
+ match kind_of_term const.const_entry_body with
+ | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+ let possible_indexes =
+ List.map (fun c ->
+ interval 0 (List.length (fst (Sign.decompose_lam_assum c))))
+ (Array.to_list fixdefs) in
+ let indexes = search_guard dummy_loc (Global.env()) possible_indexes fixdecls in
+ { const with const_entry_body = mkFix ((indexes,0),fixdecls) }
+ | c -> const
+
+let save id const do_guard (locality,kind) hook =
+ let const = if do_guard then adjust_guardness_conditions const else const in
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
@@ -366,9 +380,9 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named opacity =
- let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
- save id const persistence hook
+ save id const do_guard persistence hook
let make_eq_decidability ind =
(* fetching data *)
@@ -442,7 +456,7 @@ let declare_eliminations sp =
(* 3b| Mutual inductive definitions *)
-let compute_interning_datas env l nal typl impll =
+let compute_interning_datas env ty l nal typl impll =
let mk_interning_data na typ impls =
let idl, impl =
let impl =
@@ -452,7 +466,7 @@ let compute_interning_datas env l nal typl impll =
let sub_impl' = List.filter is_status_implicit sub_impl in
(List.map name_of_implicit sub_impl', impl)
in
- (na, (idl, impl, compute_arguments_scope typ)) in
+ (na, (ty, idl, impl, compute_arguments_scope typ)) in
(l, list_map3 mk_interning_data nal typl impll)
let declare_interning_data (_,impls) (df,c,scope) =
@@ -511,7 +525,9 @@ let interp_mutual paramsl indl notations finite =
check_all_names_different indl;
let env0 = Global.env() in
let evdref = ref (Evd.create_evar_defs Evd.empty) in
- let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in
+ let (env_params, ctx_params), userimpls =
+ interp_context_evars ~fail_anonymous:false evdref env0 paramsl
+ in
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -526,7 +542,7 @@ let interp_mutual paramsl indl notations finite =
(* Compute interpretation metadatas *)
let indimpls = List.map (fun _ -> userimpls) fullarities in
- let impls = compute_interning_datas env0 params indnames fullarities indimpls in
+ let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
@@ -539,6 +555,7 @@ let interp_mutual paramsl indl notations finite =
(* Instantiate evars and check all are resolved *)
let evd,_ = consider_remaining_unif_problems env_params !evdref in
+ let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
let sigma = evars_of evd in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
@@ -604,7 +621,7 @@ let prepare_inductive ntnl indl =
let indl =
List.map (fun ((_,indname),_,ar,lc) -> {
ind_name = indname;
- ind_arity = ar;
+ ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Rawterm.RType None)) ar;
ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
}) indl in
List.fold_right Option.List.cons ntnl [], indl
@@ -624,12 +641,10 @@ let declare_mutual_with_eliminations isrecord mie impls =
let (_,kn) = declare_mind isrecord mie in
list_iter_i (fun i (indimpls, constrimpls) ->
let ind = (kn,i) in
- maybe_declare_manual_implicits false (IndRef ind)
- (is_implicit_args()) indimpls;
+ maybe_declare_manual_implicits false (IndRef ind) indimpls;
list_iter_i
(fun j impls ->
- maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
- (is_implicit_args()) impls)
+ maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
constrimpls)
impls;
if_verbose ppnl (minductive_message names);
@@ -784,7 +799,7 @@ let declare_fix boxed kind f def t imps =
} in
let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
let gr = ConstRef kn in
- maybe_declare_manual_implicits false gr (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false gr imps;
gr
let prepare_recursive_declaration fixnames fixtypes fixdefs =
@@ -831,7 +846,7 @@ let interp_recursive fixkind l boxed =
let env_rec = push_named_types env fixnames fixtypes in
(* Get interpretation metadatas *)
- let impls = compute_interning_datas env [] fixnames fixtypes fiximps in
+ let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in
let notations = List.fold_right Option.List.cons ntnl [] in
(* Interp bodies with rollback because temp use of notations/implicit *)
@@ -1044,13 +1059,12 @@ let build_combined_scheme name schemes =
(* 4.1| Support for mutually proved theorems *)
let retrieve_first_recthm = function
- | VarRef id ->
- (pi2 (Global.lookup_named id),variable_opacity id)
- | ConstRef cst ->
- let {const_body=body;const_opaque=opaq} =
- Global.lookup_constant cst in
- (Option.map Declarations.force body,opaq)
- | _ -> assert false
+ | VarRef id ->
+ (pi2 (Global.lookup_named id),variable_opacity id)
+ | ConstRef cst ->
+ let {const_body=body;const_opaque=opaq} = Global.lookup_constant cst in
+ (Option.map Declarations.force body,opaq)
+ | _ -> assert false
let default_thm_id = id_of_string "Unnamed_thm"
@@ -1108,19 +1122,19 @@ let look_for_mutual_statements thms =
(* common coinductive conclusion *)
let n = List.length thms in
let inds = List.map (fun (id,(t,_) as x) ->
- let (hyps,ccl) = splay_prod_assum (Global.env()) Evd.empty t in
+ let (hyps,ccl) = Sign.decompose_prod_assum t in
let whnf_hyp_hds = map_rel_context_with_binders
(fun i c -> fst (whd_betadeltaiota_stack (Global.env()) Evd.empty (lift i c)))
hyps in
let ind_hyps =
- List.filter ((<>) None) (list_map_i (fun i (_,b,t) ->
+ List.flatten (list_map_i (fun i (_,b,t) ->
match kind_of_term t with
| Ind (kn,_ as ind) when
let mind = Global.lookup_mind kn in
- mind.mind_ntypes = n & mind.mind_finite & b = None ->
- Some (ind,x,i)
+ mind.mind_finite & b = None ->
+ [ind,x,i]
| _ ->
- None) 1 whnf_hyp_hds) in
+ []) 1 (List.rev whnf_hyp_hds)) in
let ind_ccl =
let cclenv = push_rel_context hyps (Global.env()) in
let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
@@ -1128,53 +1142,45 @@ let look_for_mutual_statements thms =
| Ind (kn,_ as ind) when
let mind = Global.lookup_mind kn in
mind.mind_ntypes = n & not mind.mind_finite ->
- Some (ind,x,0)
+ [ind,x,0]
| _ ->
- None in
+ [] in
ind_hyps,ind_ccl) thms in
let inds_hyps,ind_ccls = List.split inds in
- let is_same_ind kn = function Some ((kn',_),_,_) -> kn = kn' | _ -> false in
- let compare_kn ((kn,i),_,_) ((kn,i'),_,_) = i - i' in
+ let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> kn = kn' in
(* Check if all conclusions are coinductive in the same type *)
+ (* (degenerated cartesian product since there is at most one coind ccl) *)
let same_indccl =
- match ind_ccls with
- | (Some ((kn,_),_,_ as x))::rest when List.for_all (is_same_ind kn) rest
- -> Some (x :: List.map Option.get rest)
- | _ -> None in
+ list_cartesians_filter (fun hyp oks ->
+ if List.for_all (of_same_mutind hyp) oks
+ then Some (hyp::oks) else None) [] ind_ccls in
+ let ordered_same_indccl =
+ List.filter (list_for_all_i (fun i ((kn,j),_,_) -> i=j) 0) same_indccl in
(* Check if some hypotheses are inductive in the same type *)
let common_same_indhyp =
- let rec find_same_ind inds =
- match inds with
- | []::_ ->
- []
- | (Some ((kn,_),_,_) as x :: hyps_thms1)::other_thms ->
- let others' = List.map (List.filter (is_same_ind kn)) other_thms in
- (x,others')::find_same_ind (hyps_thms1::other_thms)
- | (None::hyps_thm1)::other_thms ->
- find_same_ind (hyps_thm1::other_thms)
- | [] ->
- assert false in
- find_same_ind inds_hyps in
- let common_inds,finite =
- match same_indccl, common_same_indhyp with
- | None, [(x,rest)] when List.for_all (fun l -> List.length l = 1) rest ->
- (* One occurrence of common inductive hyps and no common coind ccls *)
- Option.get x::List.map (fun x -> Option.get (List.hd x)) rest,
- false
- | Some indccl, [] ->
- (* One occurrence of common coind ccls and no common inductive hyps *)
+ list_cartesians_filter (fun hyp oks ->
+ if List.for_all (of_same_mutind hyp) oks
+ then Some (hyp::oks) else None) [] inds_hyps in
+ let ordered_inds,finite =
+ match ordered_same_indccl, common_same_indhyp with
+ | indccl::rest, _ ->
+ assert (rest=[]);
+ (* One occ. of common coind ccls and no common inductive hyps *)
+ if common_same_indhyp <> [] then
+ if_verbose warning "Assuming mutual coinductive statements.";
+ flush_all ();
indccl, true
- | _ ->
- error
- ("Cannot find a common mutual inductive premise or coinductive" ^
- " conclusion in the statements") in
- let ordered_inds = List.sort compare_kn common_inds in
- list_iter_i (fun i' ((kn,i),_,_) ->
- if i <> i' then
- error
- ("Cannot find distinct (co)inductive types of the same family" ^
- "of mutual (co)inductive types"))
- ordered_inds;
+ | [], _::_ ->
+ if same_indccl <> [] &&
+ list_distinct (List.map pi1 (List.hd same_indccl)) then
+ if_verbose warn (strbrk "Coinductive statements do not follow the order of definition, assume the proof to be by induction."); flush_all ();
+ (* assume the largest indices as possible *)
+ list_last common_same_indhyp, false
+ | _, [] ->
+ error
+ ("Cannot find common (mutual) inductive premises or coinductive" ^
+ " conclusions in the statements.")
+ in
let nl,thms = List.split (List.map (fun (_,x,i) -> (i,x)) ordered_inds) in
let rec_tac =
if finite then
@@ -1182,6 +1188,7 @@ let look_for_mutual_statements thms =
| (id,_)::l -> Hiddentac.h_mutual_cofix true id l
| _ -> assert false
else
+ (* nl is dummy: it will be recomputed at Qed-time *)
match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
| (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
| _ -> assert false in
@@ -1208,9 +1215,10 @@ let start_proof_com kind thms hook =
list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
- maybe_declare_manual_implicits false ref (is_implicit_args ()) imps;
+ maybe_declare_manual_implicits false ref imps;
hook strength ref) thms_data in
- start_proof id kind t ?init_tac:rec_tac hook
+ start_proof id kind t ?init_tac:rec_tac
+ ~compute_guard:(rec_tac<>None) hook
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
@@ -1220,17 +1228,17 @@ let check_anonymity id save_ident =
*)
let save_anonymous opacity save_ident =
- let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,persistence,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
- save save_ident const persistence hook
+ save save_ident const do_guard persistence hook
let save_anonymous_with_strength kind opacity save_ident =
- let id,(const,_,hook) = Pfedit.cook_proof !save_hook in
+ let id,(const,do_guard,_,hook) = Pfedit.cook_proof !save_hook in
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save save_ident const (Global, Proof kind) hook
+ save save_ident const do_guard (Global, Proof kind) hook
let admit () =
let (id,k,typ,hook) = Pfedit.current_proof_statement () in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8ac8c234..b42fafd0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: command.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: command.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
(*i*)
open Util
@@ -56,17 +56,19 @@ val declare_assumption : identifier located list ->
val declare_interning_data : 'a * Constrintern.implicits_env ->
string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
-val compute_interning_datas : Environ.env -> 'a list -> 'b list ->
+val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type ->
+ 'a list -> 'b list ->
Term.types list ->Impargs.manual_explicitation list list ->
'a list *
- ('b * (Names.identifier list * Impargs.implicits_list *
+ ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list *
Topconstr.scope_name option list))
list
val check_mutuality : Environ.env -> definition_object_kind ->
(identifier * types) list -> unit
-val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
+val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) *
+ decl_notation) list -> bool -> unit
val declare_mutual_with_eliminations :
bool -> Entries.mutual_inductive_entry ->
@@ -107,7 +109,7 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val set_start_hook : (types -> unit) -> unit
val start_proof : identifier -> goal_kind -> types ->
- ?init_tac:Proof_type.tactic -> declaration_hook -> unit
+ ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
val start_proof_com : goal_kind ->
(lident option * (local_binder list * constr_expr)) list ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 884589e7..d32a773d 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqinit.ml 10901 2008-05-07 18:53:48Z letouzey $ *)
+(* $Id: coqinit.ml 11749 2009-01-05 14:01:04Z notin $ *)
open Pp
open System
@@ -93,16 +93,11 @@ let theories_dirs_map = [
"theories/Init", "Init"
]
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
let init_load_path () =
- let coqlib =
- (* variable COQLIB overrides the default library *)
- getenv_else "COQLIB"
- (if Coq_config.local || !Flags.boot then Coq_config.coqtop
- else Coq_config.coqlib) in
+ let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
let dirs = "states" :: ["contrib"] in
- let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
(* first user-contrib *)
if Sys.file_exists user_contrib then
Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
@@ -114,8 +109,6 @@ let init_load_path () =
List.iter
(fun (s,alias) -> Mltop.add_rec_path (coqlib/s) (Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
theories_dirs_map;
- (* then camlp4lib *)
- add_ml_include camlp4;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
(* additional loadpath, given with -I -include -R options *)
@@ -129,13 +122,13 @@ let init_library_roots () =
(* Initialises the Ocaml toplevel before launching it, so that it can
find the "include" file in the *source* directory *)
-(* We only assume that the variable COQTOP is set *)
let init_ocaml_path () =
- let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+ let coqsrc = Coq_config.coqsrc in
let add_subdir dl =
- Mltop.add_ml_dir (List.fold_left (/) coqtop dl)
+ Mltop.add_ml_dir (List.fold_left (/) coqsrc dl)
in
- List.iter add_subdir
- [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
- [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
- [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
+ Mltop.add_ml_dir (Envars.coqlib ());
+ List.iter add_subdir
+ [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
+ [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
+ [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f8c57ad2..f5d1d142 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
+(* $Id: coqtop.ml 11830 2009-01-22 06:45:13Z notin $ *)
open Pp
open Util
@@ -21,7 +21,8 @@ open Coqinit
let get_version_date () =
try
- let ch = open_in (Coq_config.coqlib^"/revision") in
+ let coqlib = Envars.coqlib () in
+ let ch = open_in (Filename.concat coqlib "revision") in
let ver = input_line ch in
let rev = input_line ch in
(ver,rev)
@@ -51,7 +52,9 @@ let set_batch_mode () = batch_mode := true
let toplevel_default_name = make_dirpath [id_of_string "Top"]
let toplevel_name = ref (Some toplevel_default_name)
-let set_toplevel_name dir = toplevel_name := Some dir
+let set_toplevel_name dir =
+ if dir = empty_dirpath then error "Need a non empty toplevel module name";
+ toplevel_name := Some dir
let unset_toplevel_name () = toplevel_name := None
let remove_top_ml () = Mltop.remove ()
@@ -68,16 +71,16 @@ let outputstate = ref ""
let set_outputstate s = outputstate:=s
let outputstate () = if !outputstate <> "" then extern_state !outputstate
-let check_coq_overwriting p =
- if string_of_id (list_last (repr_dirpath p)) = "Coq" then
- error "The \"Coq\" logical root directory is reserved for the Coq library"
-
let set_default_include d = push_include (d,Nameops.default_root_prefix)
let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
let set_include d p =
- let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p)
+ let p = dirpath_of_string p in
+ Library.check_coq_overwriting p;
+ push_include (d,p)
let set_rec_include d p =
- let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
+ let p = dirpath_of_string p in
+ Library.check_coq_overwriting p;
+ push_rec_include(d,p)
let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
@@ -85,8 +88,8 @@ let add_load_vernacular verb s =
let load_vernacular () =
List.iter
(fun (s,b) ->
- if Flags.do_translate () then
- with_option translate_file (Vernac.load_vernac b) s
+ if Flags.do_beautify () then
+ with_option beautify_file (Vernac.load_vernac b) s
else
Vernac.load_vernac b s)
(List.rev !load_vernacular_list)
@@ -110,13 +113,13 @@ let add_compile verbose s =
compile_list := (verbose,s) :: !compile_list
let compile_files () =
let init_state = States.freeze() in
- let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+ let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
List.iter
(fun (v,f) ->
States.unfreeze init_state;
- Constrintern.coqdoc_unfreeze coqdoc_init_state;
- if Flags.do_translate () then
- with_option translate_file (Vernac.compile v) f
+ Dumpglob.coqdoc_unfreeze coqdoc_init_state;
+ if Flags.do_beautify () then
+ with_option beautify_file (Vernac.compile v) f
else
Vernac.compile v f)
(List.rev !compile_list)
@@ -132,7 +135,7 @@ let set_opt () = re_exec_version := "opt"
let re_exec is_ide =
let s = !re_exec_version in
- let is_native = (Mltop.get()) = Mltop.Native in
+ let is_native = Mltop.is_native in
(* Unix.readlink is not implemented on Windows architectures :-(
let prog =
try Unix.readlink "/proc/self/exe"
@@ -177,8 +180,10 @@ let usage () =
let warning s = msg_warning (str s)
+
let ide_args = ref []
let parse_args is_ide =
+ let glob_opt = ref false in
let rec parse = function
| [] -> ()
| "-with-geoproof" :: s :: rem ->
@@ -240,21 +245,25 @@ let parse_args is_ide =
| "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
| "-load-vernac-object" :: [] -> usage ()
- | "-dump-glob" :: f :: rem -> dump_into_file f; parse rem
+ | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
+ (* À ne pas documenter : l'option 'stdout' n'étant
+ éventuellement utile que pour le debugging... *)
+ | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
| "-dump-glob" :: [] -> usage ()
+ | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
| "-require" :: f :: rem -> add_require f; parse rem
| "-require" :: [] -> usage ()
- | "-compile" :: f :: rem -> add_compile false f; parse rem
+ | "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
| "-compile" :: [] -> usage ()
- | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
+ | "-compile-verbose" :: f :: rem -> add_compile true f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
| "-compile-verbose" :: [] -> usage ()
| "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
- | "-translate" :: rem -> make_translate true; parse rem
+ | "-beautify" :: rem -> make_beautify true; parse rem
| "-unsafe" :: f :: rem -> add_unsafe f; parse rem
| "-unsafe" :: [] -> usage ()
@@ -265,10 +274,15 @@ let parse_args is_ide =
| "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
| "-emacs-U" :: rem -> Flags.print_emacs := true;
Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-
+
| "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
- | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
+ | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
+ | "-coqlib" :: [] -> usage ()
+
+ | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0
+
+ | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0
| ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 41783faa..f733a3d5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: himsg.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Util
@@ -312,7 +312,13 @@ let explain_occur_check env ev rhs =
str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++
pt ++ spc () ++ str "that would depend on itself."
-let explain_hole_kind env = function
+let pr_ne_context_of header footer env =
+ if Environ.rel_context env = empty_rel_context &
+ Environ.named_context env = empty_named_context
+ then footer
+ else pr_ne_context_of header env
+
+let explain_hole_kind env evi = function
| QuestionMark _ -> str "this placeholder"
| CasesType ->
str "the type of this pattern-matching problem"
@@ -326,7 +332,12 @@ let explain_hole_kind env = function
pr_id id ++ spc () ++ str "of" ++
spc () ++ Nametab.pr_global_env Idset.empty c
| InternalHole ->
- str "an internal placeholder"
+ str "an internal placeholder" ++
+ Option.cata (fun evi ->
+ let env = Evd.evar_env evi in
+ str " of type " ++ pr_lconstr_env env evi.evar_concl ++
+ pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env)
+ (mt ()) evi
| TomatchTypeParameter (tyi,n) ->
str "the " ++ nth n ++
str " argument of the inductive type (" ++ pr_inductive env tyi ++
@@ -340,7 +351,7 @@ let explain_not_clean env ev t k =
let env = make_all_name_different env in
let id = Evd.string_of_existential ev in
let var = pr_lconstr_env env t in
- str "Tried to instantiate " ++ explain_hole_kind env k ++
+ str "Tried to instantiate " ++ explain_hole_kind env None k ++
str " (" ++ str id ++ str ")" ++ spc () ++
str "with a term using variable " ++ var ++ spc () ++
str "which is not in its scope."
@@ -350,25 +361,20 @@ let explain_unsolvability = function
| Some (SeveralInstancesFound n) ->
strbrk " (several distinct possible instances found)"
-let pr_ne_context_of header footer env =
- if Environ.rel_context env = empty_rel_context &
- Environ.named_context env = empty_named_context then footer
- else pr_ne_context_of header env
-
let explain_typeclass_resolution env evi k =
match k with
- InternalHole | ImplicitArg _ ->
- (match Typeclasses.class_of_constr evi.evar_concl with
- | Some c ->
- let env = Evd.evar_env evi in
- fnl () ++ str "Could not find an instance for " ++
- pr_lconstr_env env evi.evar_concl ++
- pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
- | None -> mt())
- | _ -> mt()
-
+ | GoalEvar | InternalHole | ImplicitArg _ ->
+ (match Typeclasses.class_of_constr evi.evar_concl with
+ | Some c ->
+ let env = Evd.evar_env evi in
+ fnl () ++ str "Could not find an instance for " ++
+ pr_lconstr_env env evi.evar_concl ++
+ pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
+ | None -> mt())
+ | _ -> mt()
+
let explain_unsolvable_implicit env evi k explain =
- str "Cannot infer " ++ explain_hole_kind env k ++
+ str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++
explain_unsolvability explain ++ str "." ++
explain_typeclass_resolution env evi k
@@ -500,7 +506,7 @@ let explain_no_instance env (_,id) l =
str "applied to arguments" ++ spc () ++
prlist_with_sep pr_spc (pr_lconstr_env env) l
-let pr_constraints env evm =
+let pr_constraints printenv env evm =
let l = Evd.to_list evm in
let (ev, evi) = List.hd l in
if List.for_all (fun (ev', evi') ->
@@ -508,7 +514,7 @@ let pr_constraints env evm =
then
let pe = pr_ne_context_of (str "In environment:") (mt ())
(reset_with_named_context evi.evar_hyps env) in
- pe ++ fnl () ++
+ (if printenv then pe ++ fnl () else mt ()) ++
prlist_with_sep (fun () -> fnl ())
(fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
else
@@ -518,13 +524,13 @@ let explain_unsatisfiable_constraints env evd constr =
let evm = Evd.evars_of evd in
match constr with
| None ->
- str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++
- pr_constraints env evm
+ str"Unable to satisfy the following constraints:" ++ fnl() ++
+ pr_constraints true env evm
| Some (evi, k) ->
explain_unsolvable_implicit env evi k None ++ fnl () ++
if List.length (Evd.to_list evm) > 1 then
- str"With the following meta variables:" ++
- fnl() ++ Evd.pr_evar_map evm
+ str"With the following constraints:" ++ fnl() ++
+ pr_constraints false env evm
else mt ()
let explain_mismatched_contexts env c i j =
@@ -572,6 +578,10 @@ let explain_non_linear_proof c =
str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
spc () ++ str "because a metavariable has several occurrences."
+let explain_meta_in_type c =
+ str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
+ str " of another meta"
+
let explain_refiner_error = function
| BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
| UnresolvedBindings t -> explain_refiner_unresolved_bindings t
@@ -580,6 +590,7 @@ let explain_refiner_error = function
| IntroNeedsProduct -> explain_intro_needs_product ()
| DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
| NonLinearProof c -> explain_non_linear_proof c
+ | MetaInType c -> explain_meta_in_type c
(* Inductive errors *)
@@ -618,8 +629,8 @@ let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_lconstr_env_at_top env c in
let pv1 = pr_lconstr_env env v1 in
let pv2 = pr_lconstr_env env v2 in
- str "The " ++ nth n ++ str " argument of " ++ pv2 ++ brk(1,1) ++
- str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc ++ str "."
+ str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
+ str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
let error_same_names_types id =
str "The name" ++ spc () ++ pr_id id ++ spc () ++
@@ -640,17 +651,16 @@ let error_not_an_arity id =
let error_bad_entry () =
str "Bad inductive definition."
-let error_not_allowed_case_analysis dep kind i =
- str (if dep then "Dependent" else "Non dependent") ++
- str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++
- str "is not allowed for inductive definition: " ++
- pr_inductive (Global.env()) i ++ str "."
+let error_large_non_prop_inductive_not_in_type () =
+ str "Large non-propositional inductive types must be in Type."
-let error_bad_induction dep indid kind =
- str (if dep then "Dependent" else "Non dependent") ++
- str " induction for type " ++ pr_id indid ++
- str " and sort " ++ pr_sort kind ++ spc () ++
- str "is not allowed."
+(* Recursion schemes errors *)
+
+let error_not_allowed_case_analysis isrec kind i =
+ str (if isrec then "Induction" else "Case analysis") ++
+ strbrk " on sort " ++ pr_sort kind ++
+ strbrk " is not allowed for inductive definition " ++
+ pr_inductive (Global.env()) i ++ str "."
let error_not_mutual_in_scheme ind ind' =
if ind = ind' then
@@ -674,13 +684,13 @@ let explain_inductive_error = function
| SameNamesOverlap idl -> error_same_names_overlap idl
| NotAnArity id -> error_not_an_arity id
| BadEntry -> error_bad_entry ()
+ | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type ()
(* Recursion schemes errors *)
let explain_recursion_scheme_error = function
- | NotAllowedCaseAnalysis (dep,k,i) ->
- error_not_allowed_case_analysis dep k i
- | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
+ | NotAllowedCaseAnalysis (isrec,k,i) ->
+ error_not_allowed_case_analysis isrec k i
| NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
(* Pattern-matching errors *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 89ba6aac..6a75b99c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *)
open Pp
open Util
@@ -281,22 +281,22 @@ let rec find_pattern xl = function
error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
let rec interp_list_parser hd = function
- | [] -> [], List.rev hd
+ | [] -> [], [], List.rev hd
| NonTerminal id :: tl when id = ldots_var ->
let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
- let yl,tl'' = interp_list_parser [] tl' in
- (* We remember the second copy of each recursive part variable to *)
- (* remove it afterwards *)
- y::yl, SProdList (x,sl) :: tl''
+ let yl,xl,tl'' = interp_list_parser [] tl' in
+ (* We remember each pair of variable denoting a recursive part to *)
+ (* remove the second copy of it afterwards *)
+ (y,x)::yl, x::xl, SProdList (x,sl) :: tl''
| (Terminal _ | Break _) as s :: tl ->
if hd = [] then
- let yl,tl' = interp_list_parser [] tl in
- yl, s :: tl'
+ let yl,xl,tl' = interp_list_parser [] tl in
+ yl, xl, s :: tl'
else
interp_list_parser (s::hd) tl
| NonTerminal _ as x :: tl ->
- let yl,tl' = interp_list_parser [x] tl in
- yl, List.rev_append hd tl'
+ let yl,xl,tl' = interp_list_parser [x] tl in
+ yl, xl, List.rev_append hd tl'
| SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
(* Find non-terminal tokens of notation *)
@@ -345,10 +345,20 @@ let is_numeral symbs =
let analyse_notation_tokens l =
let vars,l = raw_analyse_notation_tokens l in
- let recvars,l = interp_list_parser [] l in
- ((if recvars = [] then [] else ldots_var::recvars), vars, l)
-
-let remove_vars = List.fold_right List.remove_assoc
+ let extrarecvars,recvars,l = interp_list_parser [] l in
+ (if extrarecvars = [] then [], [], vars, l
+ else extrarecvars, recvars, list_subtract vars recvars, l)
+
+let remove_extravars extrarecvars (vars,recvars) =
+ let vars =
+ List.fold_right (fun (x,y) l ->
+ if List.assoc x l <> List.assoc y recvars then
+ error
+ "Two end variables of a recursive notation are not in the same scope."
+ else
+ List.remove_assoc x l)
+ extrarecvars (List.remove_assoc ldots_var vars) in
+ (vars,recvars)
(**********************************************************************)
(* Build pretty-printing rules *)
@@ -400,7 +410,7 @@ let is_operator s =
let l = String.length s in l <> 0 &
(s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or
s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
- s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~')
+ s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$')
let is_prod_ident = function
| Terminal s when is_letter s.[0] or s.[0] = '_' -> true
@@ -422,7 +432,7 @@ let make_hunks etyps symbols from =
| NonTerminal m :: prods ->
let i = list_index m vars in
let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
- let u = UnpMetaVar (i ,prec) in
+ let u = UnpMetaVar (i,prec) in
if prods <> [] && is_non_terminal (List.hd prods) then
u :: add_break 1 (make CanBreak prods)
else
@@ -745,7 +755,7 @@ let check_rule_productivity l =
error "A recursive notation must start with at least one symbol."
let is_not_printable = function
- | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
+ | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
| _ -> false
let find_precedence lev etyps symbols =
@@ -814,7 +824,7 @@ let compute_syntax_data (df,modifiers) =
(* Notation defaults to NONA *)
let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
let toks = split_notation_string df in
- let (recvars,vars,symbols) = analyse_notation_tokens toks in
+ let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let need_squash = (symbols <> symbols') in
@@ -833,7 +843,7 @@ let compute_syntax_data (df,modifiers) =
let prec = (n,List.map (assoc_of_type n) typs) in
let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
let df' = (Lib.library_dp(),df) in
- let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in
+ let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
(i_data,sy_data)
(**********************************************************************)
@@ -939,14 +949,15 @@ let add_notation_in_scope local df c mods scope =
let sy_rules = make_syntax_rules sy_data in
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
(* Declare interpretation *)
- let (onlyparse,recvars,vars,df') = i_data in
- let (acvars,ac) = interp_aconstr [] vars c in
- let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in
+ let (onlyparse,extrarecvars,recvars,vars,df') = i_data in
+ let (acvars,ac) = interp_aconstr [] (vars,recvars) c in
+ let a = (remove_extravars extrarecvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
- Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+ Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
let add_notation_interpretation_core local df names c scope onlyparse =
- let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
+ let dfs = split_notation_string df in
+ let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in
(* Redeclare pa/pp rules *)
if not (is_numeral symbs) then begin
let sy_rules = recover_notation_syntax (make_notation_key symbs) in
@@ -954,10 +965,10 @@ let add_notation_interpretation_core local df names c scope onlyparse =
end;
(* Declare interpretation *)
let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
- let (acvars,ac) = interp_aconstr names vars c in
- let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
+ let (acvars,ac) = interp_aconstr names (vars,recvars) c in
+ let a = (remove_extravars extrarecvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
- Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+ Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
(* Notations without interpretation (Reserved Notation) *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index c3bdadfa..fefc0b27 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: metasyntax.mli 9677 2007-02-24 14:17:54Z herbelin $ i*)
+(*i $Id: metasyntax.mli 11481 2008-10-20 19:23:51Z herbelin $ i*)
(*i*)
open Util
@@ -56,3 +56,7 @@ val print_grammar : string -> unit
(* Removes quotes in a notation *)
val standardize_locatable_notation : string -> string
+
+(* Evaluate whether a notation is not printable *)
+
+val is_not_printable : aconstr -> bool
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index ac30f890..176f336b 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
* camlp4deps will not work for this file unless Makefile system enhanced.
*)
-(* $Id: mltop.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *)
open Util
open Pp
@@ -47,8 +47,10 @@ open Vernacinterp
(* This path is where we look for .cmo *)
let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath path =
- coq_mlpath_copy := path :: !coq_mlpath_copy
+let keep_copy_mlpath path =
+ let cpath = canonical_path_name path in
+ let filter path' = (cpath <> canonical_path_name path') in
+ coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
(* If there is a toplevel under Coq *)
type toplevel = {
@@ -62,17 +64,18 @@ type toplevel = {
type kind_load =
| WithTop of toplevel
| WithoutTop
- | Native
(* Must be always initialized *)
-let load = ref Native
+let load = ref WithoutTop
-(* Sets and initializes the kind of loading *)
-let set kload = load := kload
-let get () = !load
+(* Are we in a native version of Coq? *)
+let is_native = IFDEF Byte THEN false ELSE true END
-(* Resets load *)
-let remove ()= load := Native
+(* Sets and initializes a toplevel (if any) *)
+let set_top toplevel = load := WithTop toplevel
+
+(* Removes the toplevel (if any) *)
+let remove ()= load := WithoutTop
(* Tests if an Ocaml toplevel runs under Coq *)
let is_ocaml_top () =
@@ -81,10 +84,7 @@ let is_ocaml_top () =
|_ -> false
(* Tests if we can load ML files *)
-let enable_load () =
- match !load with
- | WithTop _ | WithoutTop -> true
- |_ -> false
+let has_dynlink = IFDEF HasDynlink THEN true ELSE false END
(* Runs the toplevel loop of Ocaml *)
let ocaml_toploop () =
@@ -103,24 +103,21 @@ let dir_ml_load s =
str s ++ str" to Coq code."))
(* TO DO: .cma loading without toplevel *)
| WithoutTop ->
- IFDEF Byte THEN
+ IFDEF HasDynlink THEN
(* WARNING
* if this code section starts to use a module not used elsewhere
* in this file, the Makefile dependency logic needs to be updated.
*)
- let _,gname = where_in_path true !coq_mlpath_copy s in
+ let warn = Flags.is_verbose() in
+ let _,gname = where_in_path ~warn !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
- Dynlink.add_interfaces
- [(String.capitalize (Filename.chop_suffix
- (Filename.basename gname) ".cmo"))]
- [Filename.dirname gname]
with | Dynlink.Error a ->
errorlabstrm "Mltop.load_object" (str (Dynlink.error_message a))
- ELSE () END
- | Native ->
- errorlabstrm "Mltop.no_load_object"
- (str"Loading of ML object file forbidden in a native Coq.")
+ ELSE
+ errorlabstrm "Mltop.no_load_object"
+ (str"Loading of ML object file forbidden in a native Coq.")
+ END
(* Dynamic interpretation of .ml *)
let dir_ml_use s =
@@ -132,7 +129,7 @@ let dir_ml_use s =
let add_ml_dir s =
match !load with
| WithTop t -> t.add_dir s; keep_copy_mlpath s
- | WithoutTop -> keep_copy_mlpath s
+ | WithoutTop when has_dynlink -> keep_copy_mlpath s
| _ -> ()
(* For Rec Add ML Path *)
@@ -182,15 +179,44 @@ let mod_of_name name =
in
String.capitalize base
-let file_of_name name =
- let bname = String.uncapitalize name in
- let fname = make_suffix bname ".cmo" in
- if (is_in_path !coq_mlpath_copy fname) then fname
- else let fname=make_suffix bname ".cma" in
- if (is_in_path !coq_mlpath_copy fname) then fname
+let get_ml_object_suffix name =
+ if Filename.check_suffix name ".cmo" then
+ Some ".cmo"
+ else if Filename.check_suffix name ".cma" then
+ Some ".cma"
+ else if Filename.check_suffix name ".cmxs" then
+ Some ".cmxs"
else
+ None
+
+let file_of_name name =
+ let name = String.uncapitalize name in
+ let suffix = get_ml_object_suffix name in
+ let fail s =
errorlabstrm "Mltop.load_object"
- (str"File not found on loadpath : " ++ str (bname^".cm[oa]"))
+ (str"File not found on loadpath : " ++ str s) in
+ if is_native then
+ let name = match suffix with
+ | Some ((".cmo"|".cma") as suffix) ->
+ (Filename.chop_suffix name suffix) ^ ".cmxs"
+ | Some ".cmxs" -> name
+ | _ -> name ^ ".cmxs"
+ in
+ if is_in_path !coq_mlpath_copy name then name else fail name
+ else
+ let (full, base) = match suffix with
+ | Some ".cmo" | Some ".cma" -> true, name
+ | Some ".cmxs" -> false, Filename.chop_suffix name ".cmxs"
+ | _ -> false, name
+ in
+ if full then
+ if is_in_path !coq_mlpath_copy base then base else fail base
+ else
+ let name = base ^ ".cmo" in
+ if is_in_path !coq_mlpath_copy name then name else
+ let name = base ^ ".cma" in
+ if is_in_path !coq_mlpath_copy name then name else
+ fail (base ^ ".cm[oa]")
(* TODO: supprimer ce hack, si possible *)
(* Initialisation of ML modules that need the state (ex: tactics like
@@ -242,7 +268,7 @@ let unfreeze_ml_modules x =
(fun name ->
let mname = mod_of_name name in
if not (module_is_known mname) then
- if enable_load() then
+ if has_dynlink then
let fname = file_of_name mname in
load_object mname fname
else
@@ -272,9 +298,9 @@ let cache_ml_module_object (_,{mnames=mnames}) =
if_verbose
msg (str"[Loading ML file " ++ str fname ++ str" ...");
load_object mname fname;
- if_verbose msgnl (str"done]")
+ if_verbose msgnl (str" done]")
with e ->
- if_verbose msgnl (str"failed]");
+ if_verbose msgnl (str" failed]");
raise e
end;
add_loaded_module mname)
@@ -286,7 +312,9 @@ let (inMLModule,outMLModule) =
declare_object {(default_object "ML-MODULE") with
load_function = (fun _ -> cache_ml_module_object);
cache_function = cache_ml_module_object;
- export_function = export_ml_module_object }
+ export_function = export_ml_module_object;
+ subst_function = (fun (_,_,o) -> o);
+ classify_function = (fun (_,o) -> Substitute o) }
let declare_ml_modules l =
Lib.add_anonymous_leaf (inMLModule {mnames=l})
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index b869f70b..875fb423 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mltop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: mltop.mli 11528 2008-10-31 08:40:42Z glondu $ i*)
(* If there is a toplevel under Coq, it is described by the following
record. *)
@@ -16,25 +16,20 @@ type toplevel = {
add_dir : string -> unit;
ml_loop : unit -> unit }
-(* Determines the behaviour of Coq with respect to ML files (compiled
- or not) *)
-type kind_load=
- | WithTop of toplevel
- | WithoutTop
- | Native
+(* Sets and initializes a toplevel (if any) *)
+val set_top : toplevel -> unit
-(* Sets and initializes the kind of loading *)
-val set : kind_load -> unit
-val get : unit -> kind_load
+(* Are we in a native version of Coq? *)
+val is_native : bool
-(* Resets the kind of loading *)
+(* Removes the toplevel (if any) *)
val remove : unit -> unit
(* Tests if an Ocaml toplevel runs under Coq *)
val is_ocaml_top : unit -> bool
(* Tests if we can load ML files *)
-val enable_load : unit -> bool
+val has_dynlink : bool
(* Starts the Ocaml toplevel loop *)
val ocaml_toploop : unit -> unit
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index a9ff3326..caf32305 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: protectedtoplevel.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: protectedtoplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Line_oriented_parser
open Vernac
+open Vernacexpr
(* The toplevel parsing loop we propose here is more robust to printing
errors. The philosophy is that all commands should be individually wrapped
@@ -130,7 +131,8 @@ let rec parse_one_command_group input_channel =
!global_request_id !count None)
| Some(rank, e) ->
(match e with
- DuringCommandInterp(a,e1) ->
+ | DuringCommandInterp(a,e1)
+ | Stdpp.Exc_located (a,DuringSyntaxChecking e1) ->
output_results_nl
(acknowledge_command
!global_request_id rank (Some e1))
@@ -164,7 +166,8 @@ let protected_loop input_chan =
| End_of_file -> exit 0
| DuringCommandInterp(loc, Vernacexpr.Quit) -> raise Vernacexpr.Quit
| DuringCommandInterp(loc, Vernacexpr.Drop) -> raise Vernacexpr.Drop
- | DuringCommandInterp(loc, e) ->
+ | DuringCommandInterp(loc, e)
+ | Stdpp.Exc_located (loc,DuringSyntaxChecking e) ->
explain_and_restart e
| e -> explain_and_restart e in
begin
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 306ab047..4a2ef7db 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: record.ml 11809 2009-01-20 11:39:55Z aspiwack $ *)
open Pp
open Util
@@ -38,17 +38,23 @@ let interp_evars evdref env ?(impls=([],[])) k typ =
let mk_interning_data env na impls typ =
let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
- in (out_name na, ([], impl, Notation.compute_arguments_scope typ))
+ in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
-let interp_fields_evars isevars env l =
- List.fold_left
- (fun (env, uimpls, params, impls) ((loc, i), b, t) ->
+let interp_fields_evars isevars env nots l =
+ List.fold_left2
+ (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
- let data = mk_interning_data env i impl t' in
+ let impls =
+ match i with
+ | Anonymous -> impls
+ | Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls)
+ in
let d = (i,b',t') in
- (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
- (env, [], [], ([], [])) l
+ (* Temporary declaration of notations and scopes *)
+ Option.iter (declare_interning_data impls) no;
+ (push_rel d env, impl :: uimpls, d::params, impls))
+ (env, [], [], ([], [])) nots l
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -56,18 +62,21 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields id t ps fs =
+let typecheck_params_and_fields id t ps nots fs =
let env0 = Global.env () in
- let (env1,newps), imps = interp_context Evd.empty env0 ps in
- let fullarity = it_mkProd_or_LetIn t newps in
- let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
+ let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
+ let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
- interp_fields_evars evars env_ar (binders_of_decls fs)
+ interp_fields_evars evars env_ar nots (binders_of_decls fs)
in
- let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in
- let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in
- let ce t = Evarutil.check_evars env0 Evd.empty !evars t in
+ let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
+ let evars = Typeclasses.resolve_typeclasses env_ar evars in
+ let sigma = Evd.evars_of evars in
+ let newps = Evarutil.nf_rel_context_evar sigma newps in
+ let newfs = Evarutil.nf_rel_context_evar sigma newfs in
+ let ce t = Evarutil.check_evars env0 Evd.empty evars t in
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps;
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs;
imps, newps, impls, newfs
@@ -198,8 +207,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
let constr_fi = mkConst kn in
- Impargs.maybe_declare_manual_implicits
- false refi (Impargs.is_implicit_args()) impls;
+ Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
@@ -210,11 +218,11 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
with NotDefinable why ->
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
- (nfi-1,(optci=None)::kinds,sp_projs,subst))
+ (nfi-1,(fi, optci=None)::kinds,sp_projs,subst))
(List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
-let declare_structure id idbuild paramimpls params arity fieldimpls fields
+let declare_structure finite id idbuild paramimpls params arity fieldimpls fields
?(kind=StructureComponent) ?name is_coe coers =
let nparams = List.length params and nfields = List.length fields in
let args = extended_rel_list nfields params in
@@ -224,26 +232,130 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_consnames = [idbuild];
- mind_entry_lc = [type_constructor] } in
- let declare_as_coind =
- (* CoInd if recursive; otherwise Ind to have compat on _ind schemes *)
- dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) in
+ mind_entry_lc = [type_constructor] }
+ in
+ (* spiwack: raises an error if the structure is supposed to be non-recursive,
+ but isn't *)
+ (* there is probably a way to push this to "declare_mutual" *)
+ begin match finite with
+ | BiFinite ->
+ if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+ error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record."
+ | _ -> ()
+ end;
let mie =
{ mind_entry_params = List.map degenerate_decl params;
mind_entry_record = true;
- mind_entry_finite = not declare_as_coind;
+ mind_entry_finite = recursivity_flag_of_kind finite;
mind_entry_inds = [mie_ind] } in
let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
let build = ConstructRef (rsp,1) in
if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
- kn
+ Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
+ kn,0
+
+let implicits_of_context ctx =
+ list_map_i (fun i name ->
+ let explname =
+ match name with
+ | Name n -> Some n
+ | Anonymous -> None
+ in ExplByPos (i, explname), (true, true))
+ 1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+
+open Typeclasses
+
+let typeclasses_db = "typeclass_instances"
+
+let qualid_of_con c =
+ Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
+
+let set_rigid c =
+ Auto.add_hints false [typeclasses_db]
+ (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
+
+let declare_instance_cst glob con =
+ let instance = Typeops.type_of_constant (Global.env ()) con in
+ let _, r = Sign.decompose_prod_assum instance in
+ match class_of_constr r with
+ | Some tc -> add_instance (new_instance tc None glob con)
+ | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
+
+let declare_class finite def id idbuild paramimpls params arity fieldimpls fields
+ ?(kind=StructureComponent) ?name is_coe coers =
+ let fieldimpls =
+ (* Make the class and all params implicits in the projections *)
+ let ctx_impls = implicits_of_context params in
+ let len = succ (List.length params) in
+ List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) fieldimpls
+ in
+ let impl, projs =
+ match fields with
+ | [(Name proj_name, _, field)] when def ->
+ let class_body = it_mkLambda_or_LetIn field params in
+ let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in
+ let class_entry =
+ { const_entry_body = class_body;
+ const_entry_type = class_type;
+ const_entry_opaque = false;
+ const_entry_boxed = false }
+ in
+ let cst = Declare.declare_constant (snd id)
+ (DefinitionEntry class_entry, IsDefinition Definition)
+ in
+ let inst_type = appvectc (mkConst cst) (rel_vect 0 (List.length params)) in
+ let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in
+ let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in
+ let proj_entry =
+ { const_entry_body = proj_body;
+ const_entry_type = Some proj_type;
+ const_entry_opaque = false;
+ const_entry_boxed = false }
+ in
+ let proj_cst = Declare.declare_constant proj_name
+ (DefinitionEntry proj_entry, IsDefinition Definition)
+ in
+ let cref = ConstRef cst in
+ Impargs.declare_manual_implicits false cref paramimpls;
+ Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+ set_rigid cst; (* set_rigid proj_cst; *)
+ cref, [proj_name, Some proj_cst]
+ | _ ->
+ let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+ let ind = declare_structure BiFinite (snd id) idbuild paramimpls
+ params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
+ ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+ in
+ (* List.iter (Option.iter (declare_interning_data ((),[]))) notations; *)
+ IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
+ (List.rev fields) (Recordops.lookup_projections ind))
+ in
+ let ctx_context =
+ List.map (fun (na, b, t) ->
+ match Typeclasses.class_of_constr t with
+ | Some cl -> Some (cl.cl_impl, true) (*List.exists (fun (_, n) -> n = na) supnames)*)
+ | None -> None)
+ params, params
+ in
+ let k =
+ { cl_impl = impl;
+ cl_context = ctx_context;
+ cl_props = fields;
+ cl_projs = projs }
+ in
+ List.iter2 (fun p sub ->
+ if sub then match snd p with Some p -> declare_instance_cst true p | None -> ())
+ k.cl_projs coers;
+ add_class k; impl
+
+open Vernacexpr
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean
list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (kind,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
+ let cfs,notations = List.split cfs in
let coers,fs = List.split cfs in
let extract_name acc = function
Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
@@ -252,8 +364,16 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
let allnames = idstruc::(List.fold_left extract_name [] fs) in
if not (list_distinct allnames) then error "Two objects have the same name";
(* Now, younger decl in params and fields is on top *)
- let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
- let implfs = List.map
- (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
- declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
-
+ let sc = Option.map mkSort s in
+ let implpars, params, implfs, fields =
+ States.with_heavy_rollback (fun () ->
+ typecheck_params_and_fields idstruc sc ps notations fs) ()
+ in
+ match kind with
+ | Class b ->
+ declare_class finite b (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers
+ | _ ->
+ let arity = Option.cata (fun x -> x) (new_Type ()) sc in
+ let implfs = List.map
+ (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
+ in IndRef (declare_structure finite idstruc idbuild implpars params arity implfs fields is_coe coers)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 48181437..b49c26bc 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: record.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: record.mli 11809 2009-01-20 11:39:55Z aspiwack $ i*)
(*i*)
open Names
@@ -15,6 +15,7 @@ open Sign
open Vernacexpr
open Topconstr
open Impargs
+open Libnames
(*i*)
(* [declare_projections ref name coers params fields] declare projections of
@@ -24,17 +25,17 @@ open Impargs
val declare_projections :
inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
bool list -> manual_explicitation list list -> rel_context ->
- bool list * constant option list
+ (name * bool) list * constant option list
-val declare_structure : identifier -> identifier ->
- manual_explicitation list -> rel_context -> (* params *)
- Term.constr -> (* arity *)
+val declare_structure : Decl_kinds.recursivity_kind ->
+ identifier -> identifier ->
+ manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
bool -> (* coercion? *)
bool list -> (* field coercions *)
- mutual_inductive
+ inductive
val definition_structure :
- lident with_coercion * local_binder list *
- (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name
+ inductive_kind*Decl_kinds.recursivity_kind *lident with_coercion * local_binder list *
+ (local_decl_expr with_coercion with_notation) list * identifier * sorts option -> global_reference
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 8a9ef501..a1acd1d6 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 11317 2008-08-07 15:52:38Z barras $ *)
+(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Pp
open Util
open Flags
open Cerrors
open Vernac
+open Vernacexpr
open Pcoq
open Protectedtoplevel
@@ -262,6 +263,7 @@ let rec is_pervasive_exn = function
| Error_in_file (_,_,e) -> is_pervasive_exn e
| Stdpp.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
+ | DuringSyntaxChecking e -> is_pervasive_exn e
| _ -> false
(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -270,7 +272,8 @@ let rec is_pervasive_exn = function
let print_toplevel_error exc =
let (dloc,exc) =
match exc with
- | DuringCommandInterp (loc,ie) ->
+ | DuringCommandInterp (loc,ie)
+ | Stdpp.Exc_located (loc, DuringSyntaxChecking ie) ->
if loc = dummy_loc then (None,ie) else (Some loc, ie)
| _ -> (None, exc)
in
@@ -321,7 +324,8 @@ let rec discard_to_dot () =
* in encountered. *)
let process_error = function
- | DuringCommandInterp _ as e -> e
+ | DuringCommandInterp _
+ | Stdpp.Exc_located (_,DuringSyntaxChecking _) as e -> e
| e ->
if is_pervasive_exn e then
e
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index b0b0f826..96ff8cbc 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,12 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: usage.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
+(* $Id: usage.ml 11858 2009-01-26 13:27:23Z notin $ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
Coq_config.version Coq_config.date;
- Printf.printf "compiled on %s\n" Coq_config.compile_date;
+ Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version;
exit 0
(* print the usage of coqtop (or coqc) on channel co *)
@@ -57,6 +57,7 @@ let print_usage_channel co command =
-batch batch mode (exits just after arguments parsing)
-boot boot mode (implies -q and -batch)
-emacs tells Coq it is executed under Emacs
+ -noglob f do not dump globalizations
-dump-glob f dump globalizations in file f (to be used by coqdoc)
-with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
-impredicative-set set sort Set impredicative
@@ -80,6 +81,18 @@ let print_usage_coqc () =
print_usage "Usage: coqc <options> <Coq options> file...\n
options are:
-verbose compile verbosely
- -bindir override the default directory where coqc looks for coqtop
-image f specify an alternative executable for Coq
-t keep temporary files\n\n"
+
+(* Print the configuration information *)
+
+let print_config () =
+ if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
+ Printf.printf "COQLIB=%s/\n" Coq_config.coqlib;
+ Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc;
+ Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin;
+ Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib;
+ Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
+ Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin;
+ Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib
+
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 97814fd2..0ee58f4d 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -6,15 +6,18 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: usage.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: usage.mli 11830 2009-01-22 06:45:13Z notin $ i*)
(*s Prints the version number on the standard output and exits (with 0). *)
val version : unit -> 'a
-(*s Prints the usage on the error output, preceeded by a user-provided message. *)
+(*s Prints the usage on the error output, preceded by a user-provided message. *)
val print_usage : string -> unit
(*s Prints the usage on the error output. *)
val print_usage_coqtop : unit -> unit
val print_usage_coqc : unit -> unit
+
+(*s Prints the configuration information. *)
+val print_config : unit -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c331c13b..c5549503 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernac.ml 10836 2008-04-23 11:43:58Z courtieu $ *)
+(* $Id: vernac.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
(* Parsing of vernacular. *)
@@ -32,7 +32,8 @@ exception DuringCommandInterp of Util.loc * exn
let raise_with_file file exc =
let (cmdloc,re) =
match exc with
- | DuringCommandInterp(loc,e) -> (loc,e)
+ | DuringCommandInterp(loc,e)
+ | Stdpp.Exc_located (loc,DuringSyntaxChecking e) -> (loc,e)
| e -> (dummy_loc,e)
in
let (inner,inex) =
@@ -56,7 +57,9 @@ let real_error = function
the file we parse seems a bit risky to me. B.B. *)
let open_file_twice_if verbosely fname =
- let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
+ let paths = Library.get_load_paths () in
+ let _,longfname =
+ find_file_in_path ~warn:(Flags.is_verbose()) paths fname in
let in_chan = open_in longfname in
let verb_ch = if verbosely then Some (open_in longfname) else None in
let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -93,23 +96,24 @@ let parse_phrase (po, verbch) =
* parses, and is verbose on "primitives" commands if verbosely is true *)
let just_parsing = ref false
-let chan_translate = ref stdout
+let chan_beautify = ref stdout
+let beautify_suffix = ".beautified"
let set_formatter_translator() =
- let ch = !chan_translate in
+ let ch = !chan_beautify in
let out s b e = output ch s b e in
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
let pr_new_syntax loc ocom =
let loc = unloc loc in
- if !translate_file then set_formatter_translator();
+ if !beautify_file then set_formatter_translator();
let fs = States.freeze () in
let com = match ocom with
| Some VernacNop -> mt()
| Some com -> pr_vernac com
| None -> mt() in
- if !translate_file then
+ if !beautify_file then
msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
else
msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
@@ -121,33 +125,34 @@ let rec vernac_com interpfun (loc,com) =
| VernacLoad (verbosely, fname) ->
let fname = expand_path_macros fname in
(* translator state *)
- let ch = !chan_translate in
+ let ch = !chan_beautify in
let cs = Lexer.com_state() in
let cl = !Pp.comments in
(* end translator state *)
(* coqdoc state *)
- let cds = Constrintern.coqdoc_freeze() in
- if !Flags.translate_file then
+ let cds = Dumpglob.coqdoc_freeze() in
+ if !Flags.beautify_file then
begin
- let _,f = find_file_in_path (Library.get_load_paths ())
+ let _,f = find_file_in_path ~warn:(Flags.is_verbose())
+ (Library.get_load_paths ())
(make_suffix fname ".v") in
- chan_translate := open_out (f^"8");
+ chan_beautify := open_out (f^beautify_suffix);
Pp.comments := []
end;
begin
try
read_vernac_file verbosely (make_suffix fname ".v");
- if !Flags.translate_file then close_out !chan_translate;
- chan_translate := ch;
+ if !Flags.beautify_file then close_out !chan_beautify;
+ chan_beautify := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds
+ Dumpglob.coqdoc_unfreeze cds
with e ->
- if !Flags.translate_file then close_out !chan_translate;
- chan_translate := ch;
+ if !Flags.beautify_file then close_out !chan_beautify;
+ chan_beautify := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds;
+ Dumpglob.coqdoc_unfreeze cds;
raise e
end
@@ -164,7 +169,7 @@ let rec vernac_com interpfun (loc,com) =
in
try
- if do_translate () then pr_new_syntax loc (Some com);
+ if do_beautify () then pr_new_syntax loc (Some com);
interp com
with e ->
Format.set_formatter_out_channel stdout;
@@ -191,7 +196,7 @@ and read_vernac_file verbosely s =
close_input in_chan input; (* we must close the file first *)
match real_error e with
| End_of_input ->
- if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None
+ if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
| _ -> raise_with_file fname e
(* raw_do_vernac : char Stream.t -> unit
@@ -214,23 +219,26 @@ let set_xml_end_library f = xml_end_library := f
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
- chan_translate :=
- if !Flags.translate_file then open_out (file^"8") else stdout;
+ chan_beautify :=
+ if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
try
read_vernac_file verb file;
- if !Flags.translate_file then close_out !chan_translate;
+ if !Flags.beautify_file then close_out !chan_beautify;
with e ->
- if !Flags.translate_file then close_out !chan_translate;
+ if !Flags.beautify_file then close_out !chan_beautify;
raise_with_file file e
(* Compile a vernac file (f is assumed without .v suffix) *)
let compile verbosely f =
- let ldir,long_f_dot_v = Library.start_library f in
- if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
- if !Flags.xml_export then !xml_start_library ();
- let _ = load_vernac verbosely long_f_dot_v in
- if Pfedit.get_all_proof_names () <> [] then
- (message "Error: There are pending proofs"; exit 1);
- if !Flags.xml_export then !xml_end_library ();
- Library.save_library_to ldir (long_f_dot_v ^ "o")
+ let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+ if Dumpglob.multi_dump () then
+ Dumpglob.open_glob_file (f ^ ".glob");
+ Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+ if !Flags.xml_export then !xml_start_library ();
+ let _ = load_vernac verbosely long_f_dot_v in
+ if Pfedit.get_all_proof_names () <> [] then
+ (message "Error: There are pending proofs"; exit 1);
+ if !Flags.xml_export then !xml_end_library ();
+ if Dumpglob.multi_dump () then Dumpglob.close_glob_file ();
+ Library.save_library_to ldir (long_f_dot_v ^ "o")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3f474239..c95c89d3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 11313 2008-08-07 11:15:03Z barras $ i*)
+(*i $Id: vernacentries.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -182,8 +182,11 @@ let show_match id =
let print_path_entry (s,l) =
(str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
-let print_loadpath () =
+let print_loadpath dir =
let l = Library.get_full_load_paths () in
+ let l = match dir with
+ | None -> l
+ | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
msgnl (Pp.t (str "Logical Path: " ++
tab () ++ str "Physical path:" ++ fnl () ++
prlist_with_sep pr_fnl print_path_entry l))
@@ -232,7 +235,7 @@ let dump_universes s =
let locate_file f =
try
- let _,file = System.where_in_path false (Library.get_load_paths ()) f in
+ let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
msgnl (str file)
with Not_found ->
msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -277,7 +280,7 @@ let print_located_module r =
let global_with_alias r =
let gr = global_with_alias r in
- if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+ Dumpglob.add_glob (loc_of_reference r) gr;
gr
(**********)
@@ -307,49 +310,31 @@ let start_proof_and_print k l hook =
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
-let current_dirpath sec =
- drop_dirpath_prefix (Lib.library_dp ())
- (if sec then Lib.cwd ()
- else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()))
-
-let dump_definition (loc, id) sec s =
- Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc))
- (string_of_dirpath (current_dirpath sec)) (string_of_id id))
-
-let dump_reference loc modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty)
-
-let dump_constraint ((loc, n), _, _) sec ty =
- match n with
- | Name id -> dump_definition (loc, id) sec ty
- | Anonymous -> ()
-
-let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
- if !Flags.dump then dump_definition lid false "def";
- match def with
- | ProveBody (bl,t) -> (* local binders, typ *)
- if Lib.is_modtype () then
- errorlabstrm "Vernacentries.VernacDefinition"
- (str "Proof editing mode not supported in module types.")
- else
- let hook _ _ = () in
- start_proof_and_print (local,DefinitionBody Definition)
- [Some lid,(bl,t)] hook
- | DefineBody (bl,red_option,c,typ_opt) ->
- let red_option = match red_option with
- | None -> None
- | Some r ->
- let (evc,env)= Command.get_current_context () in
- Some (interp_redexp env evc r) in
- declare_definition id k bl red_option c typ_opt hook
-
+let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+ Dumpglob.dump_definition lid false "def";
+ (match def with
+ | ProveBody (bl,t) -> (* local binders, typ *)
+ if Lib.is_modtype () then
+ errorlabstrm "Vernacentries.VernacDefinition"
+ (str "Proof editing mode not supported in module types")
+ else
+ let hook _ _ = () in
+ start_proof_and_print (local,DefinitionBody Definition)
+ [Some lid, (bl,t)] hook
+ | DefineBody (bl,red_option,c,typ_opt) ->
+ let red_option = match red_option with
+ | None -> None
+ | Some r ->
+ let (evc,env)= Command.get_current_context () in
+ Some (interp_redexp env evc r) in
+ declare_definition id k bl red_option c typ_opt hook)
+
let vernac_start_proof kind l lettop hook =
- if !Flags.dump then
+ if Dumpglob.dump () then
List.iter (fun (id, _) ->
match id with
- | Some lid -> dump_definition lid false "prf"
- | None -> ()) l;
+ | Some lid -> Dumpglob.dump_definition lid false "prf"
+ | None -> ()) l;
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
@@ -383,28 +368,75 @@ let vernac_exact_proof c =
let vernac_assumption kind l nl=
let global = fst kind = Global in
- List.iter (fun (is_coe,(idl,c)) ->
- if !dump then
- List.iter (fun lid ->
- if global then dump_definition lid false "ax"
- else dump_definition lid true "var") idl;
- declare_assumption idl is_coe kind [] c false false nl) l
-
-let vernac_inductive f indl =
- if !dump then
- List.iter (fun ((lid, _, _, cstrs), _) ->
- dump_definition lid false"ind";
- List.iter (fun (_, (lid, _)) ->
- dump_definition lid false "constr") cstrs)
- indl;
- build_mutual indl f
+ List.iter (fun (is_coe,(idl,c)) ->
+ if Dumpglob.dump () then
+ List.iter (fun lid ->
+ if global then Dumpglob.dump_definition lid false "ax"
+ else Dumpglob.dump_definition lid true "var") idl;
+ declare_assumption idl is_coe kind [] c false false nl) l
+
+let vernac_record k finite struc binders sort nameopt cfs =
+ let const = match nameopt with
+ | None -> add_prefix "Build_" (snd (snd struc))
+ | Some (_,id as lid) ->
+ Dumpglob.dump_definition lid false "constr"; id in
+ let sigma = Evd.empty in
+ let env = Global.env() in
+ let s = Option.map (fun x ->
+ let s = Reductionops.whd_betadeltaiota env sigma (interp_constr sigma env x) in
+ match kind_of_term s with
+ | Sort s -> s
+ | _ -> user_err_loc
+ (constr_loc x,"definition_structure", str "Sort expected.")) sort
+ in
+ if Dumpglob.dump () then (
+ Dumpglob.dump_definition (snd struc) false "rec";
+ List.iter (fun ((_, x), _) ->
+ match x with
+ | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
+ | _ -> ()) cfs);
+ ignore(Record.definition_structure (k,finite,struc,binders,cfs,const,s))
+
+let vernac_inductive finite indl =
+ if Dumpglob.dump () then
+ List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+ match cstrs with
+ | Constructors cstrs ->
+ Dumpglob.dump_definition lid false "ind";
+ List.iter (fun (_, (lid, _)) ->
+ Dumpglob.dump_definition lid false "constr") cstrs
+ | _ -> () (* dumping is done by vernac_record (called below) *) )
+ indl;
+ match indl with
+ | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] ->
+ vernac_record (match b with Class true -> Class false | _ -> b)
+ finite id bl c oc fs
+ | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
+ let f =
+ let (coe, ((loc, id), ce)) = l in
+ ((coe, AssumExpr ((loc, Name id), ce)), None)
+ in vernac_record (Class true) finite id bl c None [f]
+ | [ ( id , bl , c , Class true, _), _ ] ->
+ Util.error "Definitional classes must have a single method"
+ | [ ( id , bl , c , Class false, Constructors _), _ ] ->
+ Util.error "Inductive classes not supported"
+ | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
+ Util.error "where clause not supported for (co)inductive records"
+ | _ -> let unpack = function
+ | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn
+ | _ -> Util.error "Cannot handle mutually (co)inductive records."
+ in
+ let indl = List.map unpack indl in
+ Command.build_mutual indl (recursivity_flag_of_kind finite)
let vernac_fixpoint l b =
- List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
+ if Dumpglob.dump () then
+ List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_recursive l b
let vernac_cofixpoint l b =
- List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
+ if Dumpglob.dump () then
+ List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_corecursive l b
let vernac_scheme = build_scheme
@@ -415,9 +447,11 @@ let vernac_combined_scheme = build_combined_scheme
(* Modules *)
let vernac_import export refl =
- let import ref = Library.import_module export (qualid_of_reference ref) in
- List.iter import refl;
- Lib.add_frozen_state ()
+ let import ref =
+ Library.import_module export (qualid_of_reference ref)
+ in
+ List.iter import refl;
+ Lib.add_frozen_state ()
let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
(* We check the state of the system (in section, in module type)
@@ -435,9 +469,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast (Some mty_ast_o) None
in
- Modintern.dump_moddef loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is declared");
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_moddef loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is declared");
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
(* We check the state of the system (in section, in module type)
@@ -455,7 +489,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let mp = Declaremods.start_module Modintern.interp_modtype export
id binders_ast mty_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Interactive Module "^ string_of_id id ^" started") ;
List.iter
@@ -475,7 +509,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast mty_ast_o mexpr_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Module "^ string_of_id id ^" is defined");
Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -483,9 +517,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let vernac_end_module export (loc,id) =
let mp = Declaremods.end_module id in
- Modintern.dump_modref loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is defined") ;
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_modref loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
@@ -501,7 +535,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
(idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
([],[]) in
let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
- Modintern.dump_moddef loc mp "modtype";
+ Dumpglob.dump_moddef loc mp "modtype";
if_verbose message
("Interactive Module Type "^ string_of_id id ^" started");
List.iter
@@ -511,25 +545,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
) argsexport
| Some base_mty ->
- let binders_ast = List.map
- (fun (export,idl,ty) ->
- if export <> None then
- error ("Arguments of a functor definition can be imported only if" ^
- " the definition is interactive. Remove the \"Export\" " ^
- "and \"Import\" keywords from every functor argument.")
- else (idl,ty)) binders_ast in
- let mp = Declaremods.declare_modtype Modintern.interp_modtype
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor definition can be imported only if" ^
+ " the definition is interactive. Remove the \"Export\" " ^
+ "and \"Import\" keywords from every functor argument.")
+ else (idl,ty)) binders_ast in
+ let mp = Declaremods.declare_modtype Modintern.interp_modtype
id binders_ast base_mty in
- Modintern.dump_moddef loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_moddef loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype id in
- Modintern.dump_modref loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_modref loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_include = function
| CIMTE mty_ast ->
@@ -541,39 +575,18 @@ let vernac_include = function
(**********************)
(* Gallina extensions *)
-
-let vernac_record struc binders sort nameopt cfs =
- let const = match nameopt with
- | None -> add_prefix "Build_" (snd (snd struc))
- | Some (_,id as lid) ->
- if !dump then dump_definition lid false "constr"; id in
- let sigma = Evd.empty in
- let env = Global.env() in
- let s = interp_constr sigma env sort in
- let s = Reductionops.whd_betadeltaiota env sigma s in
- let s = match kind_of_term s with
- | Sort s -> s
- | _ -> user_err_loc
- (constr_loc sort,"definition_structure", str "Sort expected.") in
- if !dump then (
- dump_definition (snd struc) false "rec";
- List.iter (fun (_, x) ->
- match x with
- | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
- | _ -> ()) cfs);
- ignore(Record.definition_structure (struc,binders,cfs,const,s))
(* Sections *)
let vernac_begin_section (_, id as lid) =
check_no_pending_proofs ();
- if !Flags.dump then dump_definition lid true "sec";
+ Dumpglob.dump_definition lid true "sec";
Lib.open_section id
let vernac_end_section (loc, id) =
- if !Flags.dump then
- dump_reference loc
- (string_of_dirpath (current_dirpath true)) "<>" "sec";
+
+ Dumpglob.dump_reference loc
+ (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section id
let vernac_end_segment lid =
@@ -588,6 +601,10 @@ let vernac_end_segment lid =
let vernac_require import _ qidl =
let qidl = List.map qualid_of_reference qidl in
+ if Dumpglob.dump () then begin
+ let modrefl = Flags.silently (List.map Library.try_locate_qualified_library) qidl in
+ List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl)
+ end;
Library.require_library qidl import
let vernac_canonical r =
@@ -606,21 +623,17 @@ let vernac_identity_coercion stre id qids qidt =
Class.try_add_new_identity_coercion id stre source target
(* Type classes *)
-let vernac_class id par ar sup props =
- if !dump then (
- dump_definition id false "class";
- List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props);
- Classes.new_class id par ar sup props
let vernac_instance glob sup inst props pri =
- if !dump then dump_constraint inst false "inst";
+ Dumpglob.dump_constraint inst false "inst";
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
+ List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
Classes.context l
let vernac_declare_instance id =
- if !dump then dump_definition id false "inst";
+ Dumpglob.dump_definition id false "inst";
Classes.declare_instance false id
(***********)
@@ -752,15 +765,18 @@ let vernac_backto n = Lib.reset_label n
let vernac_declare_tactic_definition = Tacinterp.add_tacdef
+let vernac_create_hintdb local id b =
+ Auto.create_hint_db local id full_transparent_state b
+
let vernac_hints = Auto.add_hints
let vernac_syntactic_definition lid =
- dump_definition lid false "syndef";
+ Dumpglob.dump_definition lid false "syndef";
Command.syntax_definition (snd lid)
let vernac_declare_implicits local r = function
| Some imps ->
- Impargs.declare_manual_implicits local (global_with_alias r) false
+ Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
| None ->
Impargs.declare_implicits local (global_with_alias r)
@@ -1059,7 +1075,7 @@ let vernac_print = function
| PrintSectionContext qid -> msg (print_sec_context_typ qid)
| PrintInspect n -> msg (inspect n)
| PrintGrammar ent -> Metasyntax.print_grammar ent
- | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
+ | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
| PrintModules -> msg (print_modules ())
| PrintModule qid -> print_module qid
| PrintModuleType qid -> print_modtype qid
@@ -1085,7 +1101,6 @@ let vernac_print = function
| PrintHintDbName s -> Auto.print_hint_db_by_name s
| PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
| PrintHintDb -> Auto.print_searchtable ()
- | PrintSetoids -> Setoid_replace.print_setoids()
| PrintScopes ->
pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
| PrintScope s ->
@@ -1113,24 +1128,38 @@ let interp_search_restriction = function
open Search
+let is_ident s = try ignore (check_ident s); true with UserError _ -> false
+
let interp_search_about_item = function
- | SearchRef r -> GlobSearchRef (global_with_alias r)
- | SearchString s -> GlobSearchString s
+ | SearchSubPattern pat ->
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) pat in
+ GlobSearchSubPattern pat
+ | SearchString (s,None) when is_ident s ->
+ GlobSearchString s
+ | SearchString (s,sc) ->
+ try
+ let ref =
+ Notation.interp_notation_as_global_reference dummy_loc
+ (fun _ -> true) s sc in
+ GlobSearchSubPattern (Pattern.PRef ref)
+ with UserError _ ->
+ error ("Unable to interp \""^s^"\" either as a reference or
+ as an identifier component")
let vernac_search s r =
let r = interp_search_restriction r in
if !pcoq <> None then (Option.get !pcoq).search s r else
match s with
| SearchPattern c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
Search.search_pattern pat r
| SearchRewrite c ->
- let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
+ let _,pat = intern_constr_pattern Evd.empty (Global.env()) c in
Search.search_rewrite pat r
| SearchHead ref ->
Search.search_by_head (global_with_alias ref) r
| SearchAbout sl ->
- Search.search_about (List.map interp_search_about_item sl) r
+ Search.search_about (List.map (on_snd interp_search_about_item) sl) r
let vernac_locate = function
| LocateTerm qid -> msgnl (print_located_qualid qid)
@@ -1309,7 +1338,6 @@ let interp c = match c with
| VernacEndSegment lid -> vernac_end_segment lid
- | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
| VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
@@ -1317,8 +1345,6 @@ let interp c = match c with
| VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
(* Type classes *)
- | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
-
| VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstance id -> vernac_declare_instance id
@@ -1356,6 +1382,7 @@ let interp c = match c with
(* Commands *)
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
+ | VernacCreateHintDb (local,dbname,b) -> vernac_create_hintdb local dbname b
| VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
| VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
| VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 663e2e3c..3e9dfb25 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacexpr.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: vernacexpr.ml 11809 2009-01-20 11:39:55Z aspiwack $ i*)
open Util
open Names
@@ -38,7 +38,7 @@ type printable =
| PrintSectionContext of reference
| PrintInspect of int
| PrintGrammar of string
- | PrintLoadPath
+ | PrintLoadPath of dir_path option
| PrintModules
| PrintModule of reference
| PrintModuleType of reference
@@ -60,7 +60,6 @@ type printable =
| PrintHintDbName of string
| PrintRewriteHintDbName of string
| PrintHintDb
- | PrintSetoids
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
@@ -69,14 +68,14 @@ type printable =
| PrintAssumptions of reference
type search_about_item =
- | SearchRef of reference
- | SearchString of string
+ | SearchSubPattern of constr_pattern_expr
+ | SearchString of string * scope_name option
type searchable =
- | SearchPattern of pattern_expr
- | SearchRewrite of pattern_expr
+ | SearchPattern of constr_pattern_expr
+ | SearchRewrite of constr_pattern_expr
| SearchHead of reference
- | SearchAbout of search_about_item list
+ | SearchAbout of (bool * search_about_item) list
type locatable =
| LocateTerm of reference
@@ -112,11 +111,12 @@ type comment =
| CommentInt of int
type hints =
- | HintsResolve of (int option * constr_expr) list
+ | HintsResolve of (int option * bool * constr_expr) list
| HintsImmediate of constr_expr list
| HintsUnfold of reference list
+ | HintsTransparency of reference list * bool
| HintsConstructors of reference list
- | HintsExtern of int * constr_expr * raw_tactic_expr
+ | HintsExtern of int * constr_expr option * raw_tactic_expr
| HintsDestruct of identifier *
int * (bool,unit) location * constr_expr * raw_tactic_expr
@@ -140,19 +140,11 @@ type locality_flag = bool (* true = Local; false = Global *)
type coercion_flag = bool (* true = AddCoercion; false = NoCoercion *)
type export_flag = bool (* true = Export; false = Import *)
type specif_flag = bool (* true = Specification; false = Implementation *)
-type inductive_flag = bool (* true = Inductive; false = CoInductive *)
+type inductive_flag = Decl_kinds.recursivity_kind
type onlyparsing_flag = bool (* true = Parse only; false = Print also *)
type sort_expr = Rawterm.rawsort
-type decl_notation = (string * constr_expr * scope_name option) option
-type simple_binder = lident list * constr_expr
-type class_binder = lident * constr_expr list
-type 'a with_coercion = coercion_flag * 'a
-type constructor_expr = (lident * constr_expr) with_coercion
-type inductive_expr =
- lident * local_binder list * constr_expr * constructor_expr list
-
type definition_expr =
| ProveBody of local_binder list * constr_expr
| DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -162,6 +154,20 @@ type local_decl_expr =
| AssumExpr of lname * constr_expr
| DefExpr of lname * constr_expr * constr_expr option
+type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
+type decl_notation = (string * constr_expr * scope_name option) option
+type simple_binder = lident list * constr_expr
+type class_binder = lident * constr_expr list
+type 'a with_coercion = coercion_flag * 'a
+type 'a with_notation = 'a * decl_notation
+type constructor_expr = (lident * constr_expr) with_coercion
+type constructor_list_or_record_decl_expr =
+ | Constructors of constructor_expr list
+ | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
+type inductive_expr =
+ lident with_coercion * local_binder list * constr_expr option * inductive_kind *
+ constructor_list_or_record_decl_expr
+
type module_binder = bool option * lident list * module_type_ast
type grammar_production =
@@ -211,9 +217,6 @@ type vernac_expr =
| VernacCombinedScheme of lident * lident list
(* Gallina extensions *)
- | VernacRecord of bool (* = Record or Structure *)
- * lident with_coercion * local_binder list
- * constr_expr * lident option * local_decl_expr with_coercion list
| VernacBeginSection of lident
| VernacEndSegment of lident
| VernacRequire of
@@ -225,18 +228,18 @@ type vernac_expr =
class_rawexpr * class_rawexpr
(* Type classes *)
- | VernacClass of
- lident * (* name *)
- local_binder list * (* params *)
- sort_expr located option * (* arity *)
- local_binder list * (* constraints *)
- (lident * bool * constr_expr) list (* props, with substructure hints *)
+(* | VernacClass of *)
+(* lident * (\* name *\) *)
+(* local_binder list * (\* params *\) *)
+(* sort_expr located option * (\* arity *\) *)
+(* local_binder list * (\* constraints *\) *)
+(* (lident * bool * constr_expr) list (\* props, with substructure hints *\) *)
| VernacInstance of
bool * (* global *)
local_binder list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
- (lident * lident list * constr_expr) list * (* props *)
+ constr_expr * (* props *)
int option (* Priority *)
| VernacContext of local_binder list
@@ -287,6 +290,7 @@ type vernac_expr =
(* Commands *)
| VernacDeclareTacticDefinition of
rec_flag * (reference * bool * raw_tactic_expr) list
+ | VernacCreateHintDb of locality_flag * lstring * bool
| VernacHints of locality_flag * lstring list * hints
| VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
locality_flag * onlyparsing_flag
@@ -332,3 +336,72 @@ type vernac_expr =
| VernacExtend of string * raw_generic_argument list
and located_vernac_expr = loc * vernac_expr
+
+(* Locating errors raised just after the dot is parsed but before the
+ interpretation phase *)
+
+exception DuringSyntaxChecking of exn
+
+let syntax_checking_error s =
+ raise (DuringSyntaxChecking (UserError ("",Pp.str s)))
+
+(* Managing locality *)
+
+let locality_flag = ref None
+
+let local_of_bool = function true -> Local | false -> Global
+
+let check_locality () =
+ if !locality_flag = Some true then
+ syntax_checking_error "This command does not support the \"Local\" prefix.";
+ if !locality_flag = Some false then
+ syntax_checking_error "This command does not support the \"Global\" prefix."
+
+let use_locality () =
+ let local = match !locality_flag with Some true -> true | _ -> false in
+ locality_flag := None;
+ local
+
+let use_locality_exp () = local_of_bool (use_locality ())
+
+let use_section_locality () =
+ let local =
+ match !locality_flag with Some b -> b | None -> Lib.sections_are_opened ()
+ in
+ locality_flag := None;
+ local
+
+let use_non_locality () =
+ let local = match !locality_flag with Some false -> false | _ -> true in
+ locality_flag := None;
+ local
+
+let enforce_locality () =
+ let local =
+ match !locality_flag with
+ | Some false ->
+ error "Cannot be simultaneously Local and Global."
+ | _ ->
+ Flags.if_verbose
+ Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
+ true in
+ locality_flag := None;
+ local
+
+let enforce_locality_exp () = local_of_bool (enforce_locality ())
+
+let enforce_locality_of local =
+ let local =
+ match !locality_flag with
+ | Some false when local ->
+ error "Cannot be simultaneously Local and Global."
+ | Some true when local ->
+ error "Use only prefix \"Local\"."
+ | None ->
+ if local then
+ Flags.if_verbose
+ Pp.warning "Obsolete syntax: use \"Local\" as a prefix.";
+ local
+ | Some b -> b in
+ locality_flag := None;
+ local
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 21:51:38 +0000