summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /toplevel
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml30
-rw-r--r--toplevel/cerrors.ml33
-rw-r--r--toplevel/class.ml13
-rw-r--r--toplevel/classes.ml437
-rw-r--r--toplevel/classes.mli52
-rw-r--r--toplevel/command.ml53
-rw-r--r--toplevel/command.mli24
-rw-r--r--toplevel/coqtop.ml21
-rw-r--r--toplevel/fhimsg.ml355
-rw-r--r--toplevel/himsg.ml75
-rw-r--r--toplevel/himsg.mli5
-rw-r--r--toplevel/metasyntax.ml77
-rw-r--r--toplevel/minicoq.ml149
-rw-r--r--toplevel/mltop.ml451
-rw-r--r--toplevel/record.ml127
-rw-r--r--toplevel/record.mli16
-rw-r--r--toplevel/toplevel.ml27
-rw-r--r--toplevel/usage.ml10
-rw-r--r--toplevel/vernacentries.ml73
-rw-r--r--toplevel/vernacexpr.ml4
-rw-r--r--toplevel/vernacinterp.ml6
-rw-r--r--toplevel/whelp.ml410
22 files changed, 504 insertions, 1144 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 094a77ff..49b9ce7a 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 11166 2008-06-22 13:23:35Z herbelin $ i*)
+(*i $Id: auto_ind_decl.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Tacmach
open Util
@@ -55,6 +55,8 @@ let subst_in_constr (_,subst,(ind,const)) =
exception EqNotFound of string
exception EqUnknown of string
+let dl = dummy_loc
+
(* Some pre declaration of constant we are going to use *)
let bb = constr_of_global Coqlib.glob_bool
@@ -514,13 +516,13 @@ let compute_bl_tact ind lnamesparrec nparrec =
new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
Rawterm.NoBindings))]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshm;
new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
Rawterm.NoBindings))]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshz;
intros;
@@ -542,9 +544,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
(new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshz,Rawterm.NoBindings))]
None
- ( Genarg.IntroOrAndPattern [[
- Genarg.IntroIdentifier fresht;
- Genarg.IntroIdentifier freshz]]) None) gl
+ (None, Some (dl,Genarg.IntroOrAndPattern [[
+ dl,Genarg.IntroIdentifier fresht;
+ dl,Genarg.IntroIdentifier freshz]])) None) gl
]);
(*
Ci a1 ... an = Ci b1 ... bn
@@ -632,13 +634,13 @@ let compute_lb_tact ind lnamesparrec nparrec =
new_induct false [Tacexpr.ElimOnConstr
((mkVar freshn),Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshm;
new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshm),Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshz;
intros;
@@ -746,7 +748,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
Pfedit.by ( tclTHENSEQ [
intros_using fresh_first_intros;
intros_using [freshn;freshm];
- assert_as true (Genarg.IntroIdentifier freshH) (
+ assert_as true (dl,Genarg.IntroIdentifier freshH) (
mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
) ]);
(*we do this so we don't have to prove the same goal twice *)
@@ -754,7 +756,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
(new_destruct false [Tacexpr.ElimOnConstr
(eqbnm,Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None)
Auto.default_auto
);
@@ -764,9 +766,9 @@ let compute_dec_tact ind lnamesparrec nparrec =
new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshH),Rawterm.NoBindings)]
None
- (Genarg.IntroOrAndPattern [
- [Genarg.IntroAnonymous];
- [Genarg.IntroIdentifier freshH2]]) None
+ (None,Some (dl,Genarg.IntroOrAndPattern [
+ [dl,Genarg.IntroAnonymous];
+ [dl,Genarg.IntroIdentifier freshH2]])) None
);
let arfresh = Array.of_list fresh_first_intros in
let xargs = Array.sub arfresh 0 (2*nparrec) in
@@ -793,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 (Genarg.IntroIdentifier freshH3)
+ assert_as true (dl,Genarg.IntroIdentifier freshH3)
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
]);
Pfedit.by
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 40d74256..0983463a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cerrors.ml 10410 2007-12-31 13:11:55Z msozeau $ *)
+(* $Id: cerrors.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -34,21 +34,21 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
| Stream.Failure ->
hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
| Stream.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt)
+ hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Token.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt)
+ hov 0 (str "Syntax error: " ++ str txt ++ str ".")
| Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
| UserError(s,pps) ->
- hov 1 (str "User error: " ++ where s ++ pps)
+ hov 0 (str "Error: " ++ where s ++ pps)
| Out_of_memory ->
- hov 0 (str "Out of memory")
+ hov 0 (str "Out of memory.")
| Stack_overflow ->
- hov 0 (str "Stack overflow")
+ hov 0 (str "Stack overflow.")
| Anomaly (s,pps) ->
- hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+ hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
| Match_failure(filename,pos1,pos2) ->
- hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
+ hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
if Sys.ocaml_version = "3.06" then
(str " from character " ++ int pos1 ++
str " to " ++ int pos2)
@@ -83,6 +83,11 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
| RecursionSchemeError e ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
+ | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () ->
+ explain_exn_default_aux anomaly_string report_fn exc
+ | Proof_type.LtacLocated (s,exc) ->
+ hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
+ ++ explain_exn_default_aux anomaly_string report_fn exc)
| Cases.PatternMatchingError (env,e) ->
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
@@ -94,13 +99,15 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (str "Error:" ++ spc () ++
str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
spc () ++ str "was not found" ++
- spc () ++ str "in the current" ++ spc () ++ str "environment")
+ spc () ++ str "in the current" ++ spc () ++ str "environment.")
| Nametab.GlobalizationConstantError q ->
hov 0 (str "Error:" ++ spc () ++
- str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
+ str "No constant of this name:" ++ spc () ++
+ Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
- hov 0 (str "Error: Tactic failure" ++ s ++
- if i=0 then mt () else str " (level " ++ int i ++ str").")
+ hov 0 (str "Error: Tactic failure" ++
+ (if s <> mt() then str ":" ++ s else mt ()) ++
+ if i=0 then str "." else str " (level " ++ int i ++ str").")
| Stdpp.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
@@ -145,7 +152,7 @@ let raise_if_debug e =
let _ = Tactic_debug.explain_logic_error := explain_exn_default
let _ = Tactic_debug.explain_logic_error_no_anomaly :=
- explain_exn_default_aux (fun () -> mt()) (fun () -> mt())
+ explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
let explain_exn_function = ref explain_exn_default
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 92fd2d4c..2c6a63b0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: class.ml 11085 2008-06-10 08:54:43Z herbelin $ *)
+(* $Id: class.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Pp
@@ -119,7 +119,7 @@ let class_of_global = function
| ConstructRef _ as c ->
errorlabstrm "class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
- str " cannot be used as class")
+ str ", cannot be used as a class.")
(*
lp est la liste (inverse'e) des arguments de la coercion
@@ -189,7 +189,7 @@ let ident_key_of_class = function
let error_not_transparent source =
errorlabstrm "build_id_coercion"
- (pr_class source ++ str " must be a transparent constant")
+ (pr_class source ++ str " must be a transparent constant.")
let build_id_coercion idf_opt source =
let env = Global.env () in
@@ -218,8 +218,8 @@ let build_id_coercion idf_opt source =
(Reductionops.is_conv_leq env Evd.empty
(Typing.type_of env Evd.empty val_f) typ_f)
then
- error ("cannot be defined as coercion - "^
- "maybe a bad number of arguments")
+ errorlabstrm "" (strbrk
+ "Cannot be defined as coercion (maybe a bad number of arguments).")
in
let idf =
match idf_opt with
@@ -283,7 +283,8 @@ let add_new_coercion_core coef stre source target isid =
let try_add_new_coercion_core ref b c d e =
try add_new_coercion_core ref b c d e
with CoercionError e ->
- errorlabstrm "try_add_new_coercion_core" (explain_coercion_error ref e)
+ errorlabstrm "try_add_new_coercion_core"
+ (explain_coercion_error ref e ++ str ".")
let try_add_new_coercion ref stre =
try_add_new_coercion_core ref stre None None false
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8ed99cbd..511befd8 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 11161 2008-06-21 14:32:47Z msozeau $ i*)
+(*i $Id: classes.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
(*i*)
open Names
@@ -50,22 +50,23 @@ let declare_instance_cst glob con =
let _, r = decompose_prod_assum instance in
match class_of_constr r with
| Some tc -> add_instance (new_instance tc None glob con)
- | None -> error "Constant does not build instances of a declared type class"
+ | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
let declare_instance glob idl =
let con =
try (match global (Ident idl) with
| ConstRef x -> x
| _ -> raise Not_found)
- with _ -> error "Instance definition not found"
+ with _ -> error "Instance definition not found."
in declare_instance_cst glob con
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
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) ->
@@ -87,111 +88,6 @@ let interp_typeclass_context_evars isevars env avoid l =
(push_named d env, i :: ids, d::params))
(env, avoid, []) l
-let interp_constrs_evars isevars env avoid l =
- List.fold_left
- (fun (env, ids, params) t ->
- let t' = interp_binder_evars isevars env Anonymous t in
- let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in
- let d = (id,None,t') in
- (push_named d env, id :: ids, d::params))
- (env, avoid, []) l
-
-let raw_assum_of_binders k =
- List.map (fun ((loc,i),t) -> LocalRawAssum ([(loc, Name i)], k, t))
-
-let raw_assum_of_constrs k =
- List.map2 (fun t (n,_,_) -> LocalRawAssum ([(dummy_loc, Name n)], k, t))
-
-let raw_assum_of_anonymous_constrs k =
- List.map (fun t -> LocalRawAssum ([(dummy_loc, Anonymous)], k, t))
-
-let decl_expr_of_binders =
- List.map (fun ((loc,i),t) -> false, Vernacexpr.AssumExpr ((loc, Name i), t))
-
-let rec unfold n f acc =
- match n with
- | 0 -> f 0 acc
- | n -> unfold (n - 1) f (f n acc)
-
-(* Declare everything in the parameters as implicit, and the class instance as well *)
-open Topconstr
-
-let declare_implicit_proj c proj imps sub =
- let len = List.length c.cl_context in
- let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in
- let expls =
- let rec aux i expls = function
- [] -> expls
- | (Name n, _) :: tl ->
- let impl = ExplByPos (i, Some n), (true, true) in
- aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl
- | (Anonymous,_) :: _ -> assert(false)
- in
- aux 1 [] (List.rev ctx)
- in
- let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
- if sub then
- declare_instance_cst true (snd proj);
- Impargs.declare_manual_implicits false (ConstRef (snd proj)) true expls
-
-let declare_implicits impls subs cl =
- Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
- cl.cl_projs impls subs;
- let len = List.length cl.cl_context in
- let indimps =
- list_fold_left_i
- (fun i acc (is, (na, b, t)) ->
- if len - i <= cl.cl_params then acc
- else
- match is with
- None | Some (_, false) -> (ExplByPos (i, Some na), (false, true)) :: acc
- | _ -> acc)
- 1 [] (List.rev cl.cl_context)
- in
- Impargs.declare_manual_implicits false cl.cl_impl false indimps
-
-let rel_of_named_context subst l =
- List.fold_right
- (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
- l ([], subst)
-
-let ids_of_rel_context subst l =
- List.fold_right
- (fun (id, _, t) acc -> Nameops.out_name id :: acc)
- l subst
-
-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 declare_structure env id idbuild params arity fields =
- let nparams = List.length params and nfields = List.length fields in
- let args = extended_rel_list nfields params in
- let ind = applist (mkRel (1+nparams+nfields), args) in
- let type_constructor = it_mkProd_or_LetIn ind fields in
- let mie_ind =
- { mind_entry_typename = id;
- mind_entry_arity = arity;
- mind_entry_consnames = [idbuild];
- mind_entry_lc = [type_constructor] } in
- let mie =
- { mind_entry_params = List.map degenerate_decl params;
- mind_entry_record = true;
- mind_entry_finite = true;
- mind_entry_inds = [mie_ind] } in
- let kn = Command.declare_mutual_with_eliminations true mie [] in
- let rsp = (kn,0) in (* This is ind path of idstruc *)
- let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
- let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in
- let _build = ConstructRef (rsp,1) in
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
- rsp
-
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
@@ -206,19 +102,31 @@ let interp_fields_evars isevars env avoid l =
(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 = (i,None,t') in
- (push_named d env, impl :: uimpls, Idset.add i ids, d::params, ([], data :: snd impls)))
- (env, [], avoid, [], ([], [])) l
-
-let interp_fields_rel_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 =
@@ -237,33 +145,7 @@ let name_typeclass_binders avoid l =
b' :: binders, avoid)
([], avoid) l
in List.rev l', avoid
-
-let decompose_named_assum =
- let rec prodec_rec subst l c =
- match kind_of_term c with
- | Prod (Name na,t,c) ->
- let decl = (na,None,substl subst t) in
- let subst' = mkVar na :: subst in
- prodec_rec subst' (add_named_decl decl l) (substl subst' c)
- | LetIn (Name na, b, t, c) ->
- let decl = (na,Some (substl subst b),substl subst t) in
- let subst' = mkVar na :: subst in
- prodec_rec subst' (add_named_decl decl l) (substl subst' c)
- | Cast (c,_,_) -> prodec_rec subst l c
- | _ -> l,c
- in prodec_rec [] []
-let push_named_context =
- List.fold_right push_named
-
-let named_of_rel_context (subst, ids, env as init) ctx =
- Sign.fold_rel_context
- (fun (na,c,t) (subst, avoid, env) ->
- let id = Nameops.next_name_away na avoid in
- let d = (id,Option.map (substl subst) c,substl subst t) in
- (mkVar id :: subst, id::avoid, d::env))
- ctx ~init
-
let new_class id par ar sup props =
let env0 = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -294,7 +176,7 @@ let new_class id par ar sup props =
(* Interpret the definitions and propositions *)
let env_props, prop_impls, bound, ctx_props, _ =
- interp_fields_rel_evars isevars env_params bound 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 *)
@@ -305,6 +187,12 @@ let new_class id par ar sup props =
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);
@@ -337,31 +225,34 @@ let new_class id par ar sup props =
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
- ConstRef cst, [proj_name, proj_cst]
+ 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 kn = declare_structure env0 (snd id) idb params arity fields in
- IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
- fields (Recordops.lookup_projections kn))
+ 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 ids = List.map pi1 (named_context env0) in
- let (subst, ids, named_ctx_params) = named_of_rel_context ([], ids, []) ctx_params in
- let (_, _, named_ctx_props) = named_of_rel_context (subst, ids, []) ctx_props 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 = Name na) supnames), d)
+ | Some cl -> (Some (cl.cl_impl, List.exists (fun (_, n) -> n = na) supnames), d)
| None -> (None, d))
- named_ctx_params
+ ctx_params
in
let k =
{ cl_impl = impl;
- cl_params = List.length par;
cl_context = ctx_context;
- cl_props = named_ctx_props;
+ cl_props = ctx_props;
cl_projs = projs }
in
- declare_implicits (List.rev prop_impls) subs k;
+ 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
@@ -369,63 +260,16 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
let binders_of_lidents l =
List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
-let subst_ids_in_named_context subst l =
- let x, _ =
- List.fold_right
- (fun (id, _, t) (ctx, k) -> (id, None, substn_vars k subst t) :: ctx, succ k)
- l ([], 1)
- in x
-
-let subst_one_named inst ids t =
- substnl inst 0 (substn_vars 1 ids t)
-
-let subst_named inst subst ctx =
- let ids = List.map (fun (id, _, _) -> id) subst in
- let ctx' = subst_ids_in_named_context ids ctx in
- let ctx', _ =
- List.fold_right
- (fun (id, _, t) (ctx, k) -> (id, None, substnl inst k t) :: ctx, succ k)
- ctx' ([], 0)
- in ctx'
-(*
-let infer_super_instances env params params_ctx super =
- let super = subst_named params params_ctx super in
- List.fold_right
- (fun (na, _, t) (sups, ids, supctx) ->
- let t = subst_one_named sups ids t in
- let inst =
- try resolve_one_typeclass env t
- with Not_found ->
- let cl, args = destClass t in
- no_instance (push_named_context supctx env) (dummy_loc, cl.cl_name) (Array.to_list args)
- in
- let d = (na, Some inst, t) in
- inst :: sups, na :: ids, d :: supctx)
- super ([], [], [])*)
-
-(* let evars_of_context ctx id n env = *)
-(* List.fold_right (fun (na, _, t) (n, env, nc) -> *)
-(* let b = Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (Ident id, (n * Some na))) t in *)
-(* let d = (na, Some b, t) in *)
-(* (succ n, push_named d env, d :: nc)) *)
-(* ctx (n, env, []) *)
-
let type_ctx_instance isevars env ctx inst subst =
- List.fold_left2
- (fun (subst, instctx) (na, _, t) ce ->
- let t' = replace_vars subst t in
- let c = interp_casted_constr_evars isevars env ce t' in
- let d = na, Some c, t' in
- (na, c) :: subst, d :: instctx)
- (subst, []) (List.rev ctx) inst
-
-let substitution_of_constrs ctx cstrs =
- List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
-
-let destClassApp cl =
- match cl with
- | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
- | _ -> raise Not_found
+ let (s, _) =
+ List.fold_left2
+ (fun (subst, instctx) (na, _, 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)
+ (subst, []) (List.rev ctx) inst
+ in s
let refine_ref = ref (fun _ -> assert(false))
@@ -521,31 +365,31 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
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_named_assum c' in
+ let ctx, c = decompose_prod_assum c' in
let cl, args = Typeclasses.dest_class_app c in
- cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+ cl, ctx, imps, List.rev (Array.to_list args)
in
let id =
match snd instid with
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+ errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
Termops.next_global_ident_away false i (Termops.ids_of_context env)
in
- let env' = push_named_context ctx' env in
+ let env' = push_rel_context ctx' env in
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses env !isevars;
let sigma = Evd.evars_of !isevars in
- let substctx = Typeclasses.nf_substitution sigma subst in
+ let substctx = List.map (Evarutil.nf_evar sigma) subst in
if Lib.is_modtype () then
begin
- let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in
+ let _, ty_constr = instance_constructor k (List.rev subst) in
let termtype =
- let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+ let t = it_mkProd_or_LetIn ty_constr ctx' in
Evarutil.nf_isevar !isevars t
in
Evarutil.check_evars env Evd.empty !isevars termtype;
@@ -555,7 +399,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
end
else
begin
- let subst, _propsctx =
+ let subst =
let props =
List.map (fun (x, l, d) ->
x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
@@ -567,8 +411,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
List.fold_left
(fun (props, rest) (id,_,_) ->
try
- let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
- let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+ 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)
@@ -579,12 +423,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
else
type_ctx_instance isevars env' k.cl_props props substctx
in
- let app, ty_constr = instance_constructor k (List.rev_map snd subst) in
+ let app, ty_constr = instance_constructor k (List.rev subst) in
let termtype =
- let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+ let t = it_mkProd_or_LetIn ty_constr ctx' in
Evarutil.nf_isevar !isevars t
in
- let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
+ let term = Termops.it_mkLambda_or_LetIn app ctx' in
isevars := Evarutil.nf_evar_defs !isevars;
let term = Evarutil.nf_isevar !isevars term in
let evm = Evd.evars_of (undefined_evars !isevars) in
@@ -607,31 +451,26 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
end
end
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
-
-let solve_by_tac env evd evar evi t =
- let goal = {it = evi; sigma = (Evd.evars_of evd) } in
- let (res, valid) = t goal in
- if res.it = [] then
- let prooftree = valid [] in
- let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in
- if obls = [] then
- let evd' = evars_reset_evd res.sigma evd in
- let evd' = evar_define evar proofterm evd' in
- evd', true
- else evd, false
- else evd, false
+let named_of_rel_context l =
+ let acc, ctx =
+ List.fold_right
+ (fun (na, b, t) (subst, ctx) ->
+ let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in
+ let d = (id, Option.map (substl subst) b, substl subst t) in
+ (mkVar id :: subst, d :: ctx))
+ l ([], [])
+ in ctx
let context ?(hook=fun _ -> ()) l =
let env = Global.env() in
- let isevars = ref (Evd.create_evar_defs Evd.empty) in
- let avoid = Termops.ids_of_context env in
- let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in
- let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in
- let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
- isevars := Evarutil.nf_evar_defs !isevars;
- let sigma = Evd.evars_of !isevars in
- let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
+ let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let (env', fullctx), impls = interp_context_evars evars env l in
+ let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in
+ let ce t = Evarutil.check_evars env Evd.empty !evars t in
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
+ let ctx = try named_of_rel_context fullctx with _ ->
+ error "Anonymous variables not allowed in contexts."
+ in
List.iter (function (id,_,t) ->
if Lib.is_modtype () then
let cst = Declare.declare_internal_constant id
@@ -642,96 +481,12 @@ let context ?(hook=fun _ -> ()) l =
add_instance (Typeclasses.new_instance tc None false cst);
hook (ConstRef cst)
| None -> ()
- else
- (Command.declare_one_assumption false (Local (* global *), Definitional) t
- [] true (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
- match class_of_constr t with
- None -> ()
- | Some tc -> hook (VarRef id)))
- (List.rev fullctx)
-
-open Libobject
-
-let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init")
-let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation")
-
-let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid)))
-let tactic = lazy (Tacinterp.interp tactic_expr)
-
-let _ =
- Typeclasses.solve_instanciation_problem :=
- (fun env evd ev evi ->
- Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
- solve_by_tac env evd ev evi (Lazy.force tactic))
-
-(* let prod = lazy_fun Coqlib.build_prod *)
-
-(* let build_conjunction evm = *)
-(* List.fold_left *)
-(* (fun (acc, evs) (ev, evi) -> *)
-(* if class_of_constr evi.evar_concl <> None then *)
-(* mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs *)
-(* else acc, Evd.add evs ev evi) *)
-(* (Coqlib.build_coq_True (), Evd.empty) evm *)
-
-(* let destruct_conjunction evm_list evm evm' term = *)
-(* let _, evm = *)
-(* List.fold_right *)
-(* (fun (ev, evi) (term, evs) -> *)
-(* if class_of_constr evi.evar_concl <> None then *)
-(* match kind_of_term term with *)
-(* | App (x, [| _ ; _ ; proof ; term |]) -> *)
-(* let evs' = Evd.define evs ev proof in *)
-(* (term, evs') *)
-(* | _ -> assert(false) *)
-(* else *)
-(* match (Evd.find evm' ev).evar_body with *)
-(* Evar_empty -> raise Not_found *)
-(* | Evar_defined c -> *)
-(* let evs' = Evd.define evs ev c in *)
-(* (term, evs')) *)
-(* evm_list (term, evm) *)
-(* in evm *)
-
-(* let solve_by_tac env evd evar evi t = *)
-(* let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
-(* let (res, valid) = t goal in *)
-(* if res.it = [] then *)
-(* let prooftree = valid [] in *)
-(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
-(* if obls = [] then *)
-(* let evd' = evars_reset_evd res.sigma evd in *)
-(* let evd' = evar_define evar proofterm evd' in *)
-(* evd', true *)
-(* else evd, false *)
-(* else evd, false *)
-
-(* let resolve_all_typeclasses env evd = *)
-(* let evm = Evd.evars_of evd in *)
-(* let evm_list = Evd.to_list evm in *)
-(* let goal, typesevm = build_conjunction evm_list in *)
-(* let evars = ref (Evd.create_evar_defs typesevm) in *)
-(* let term = resolve_one_typeclass_evd env evars goal in *)
-(* let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in *)
-(* Evd.create_evar_defs evm' *)
-
-(* let _ = *)
-(* Typeclasses.solve_instanciations_problem := *)
-(* (fun env evd -> *)
-(* Library.require_library [(dummy_loc, module_qualid)] None; (\* may be inefficient *\) *)
-(* resolve_all_typeclasses env evd) *)
-
-let solve_evars_by_tac env evd t =
- let ev = make_evar empty_named_context_val mkProp in
- let goal = {it = ev; sigma = (Evd.evars_of evd) } in
- let (res, valid) = t goal in
- let evd' = evars_reset_evd res.sigma evd in
- evd'
-(* Library.require_library [(dummy_loc, module_qualid)] None (a\* may be inefficient *\); *)
-
-(* let _ = *)
-(* Typeclasses.solve_instanciations_problem := *)
-(* (fun env evd -> *)
-(* Eauto.resolve_all_evars false (true, 15) env *)
-(* (fun ev evi -> is_implicit_arg (snd (evar_source ev evd)) *)
-(* && class_of_constr evi.evar_concl <> None) evd) *)
+ else (
+ let impl = List.exists (fun (x,_) -> match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
+ in
+ Command.declare_one_assumption false (Local (* global *), Definitional) t
+ [] impl (* implicit *) true (* always kept *) false (* inline *) (dummy_loc, id);
+ match class_of_constr t with
+ | None -> ()
+ | Some tc -> hook (VarRef id)))
+ (List.rev ctx)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index f3cb0c58..f149ac72 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
(*i*)
open Names
@@ -23,17 +23,21 @@ open Typeclasses
open Implicit_quantifiers
(*i*)
+(* Errors *)
+
+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 declare_implicit_proj : typeclass -> (identifier * constant) ->
- Impargs.manual_explicitation list -> bool -> unit
-(*
-val infer_super_instances : env -> constr list ->
- named_context -> named_context -> types list * identifier list * named_context
-*)
+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 ->
@@ -46,6 +50,10 @@ 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
+
val declare_instance_constant :
typeclass ->
int option -> (* priority *)
@@ -69,35 +77,15 @@ val new_instance :
identifier
(* For generation on names based on classes only *)
-val id_of_class : typeclass -> identifier
-
-val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
-
-val declare_instance : bool -> identifier located -> unit
-val mismatched_params : env -> constr_expr list -> named_context -> 'a
+val id_of_class : typeclass -> identifier
-val mismatched_props : env -> constr_expr list -> named_context -> 'a
+(* Context command *)
-val solve_by_tac : env ->
- Evd.evar_defs ->
- Evd.evar ->
- evar_info ->
- Proof_type.tactic ->
- Evd.evar_defs * bool
+val context : ?hook:(Libnames.global_reference -> unit) ->
+ local_binder list -> unit
-val solve_evars_by_tac : env ->
- Evd.evar_defs ->
- Proof_type.tactic ->
- Evd.evar_defs
+(* Forward ref for refine *)
val refine_ref : (open_constr -> Proof_type.tactic) ref
-val decompose_named_assum : types -> named_context * types
-
-val push_named_context : named_context -> env -> env
-
-val name_typeclass_binders : Idset.t ->
- Topconstr.local_binder list ->
- Topconstr.local_binder list * Idset.t
-
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 531eadb3..3688c347 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml 11169 2008-06-24 14:37:18Z notin $ *)
+(* $Id: command.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -88,8 +88,8 @@ let rec complete_conclusion a cs = function
let (has_no_args,name,params) = a in
if not has_no_args then
user_err_loc (loc,"",
- str "Cannot infer the non constant arguments of the conclusion of "
- ++ pr_id cs);
+ strbrk"Cannot infer the non constant arguments of the conclusion of "
+ ++ pr_id cs ++ str ".");
let args = List.map (fun id -> CRef(Ident(loc,id))) params in
CAppExpl (loc,(None,Ident(loc,name)),List.rev args)
| c -> c
@@ -310,7 +310,7 @@ let declare_eq_scheme sp =
definition_message nam
done
with Not_found ->
- error "Your type contains Parameters without a boolean equality"
+ error "Your type contains Parameters without a boolean equality."
(* decidability of eq *)
@@ -473,7 +473,7 @@ type inductive_expr = {
}
let minductive_message = function
- | [] -> error "no inductive definition"
+ | [] -> error "No inductive definition."
| [x] -> (pr_id x ++ str " is defined")
| l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
spc () ++ str "are defined")
@@ -556,12 +556,18 @@ let interp_mutual paramsl indl notations finite =
mind_entry_consnames = cnames;
mind_entry_lc = ctypes
}) indl arities constructors in
-
+ let impls =
+ let len = List.length ctx_params in
+ List.map (fun (_,_,impls) ->
+ userimpls, List.map (fun impls ->
+ userimpls @ (lift_implicits len impls)) impls) constructors
+ in
(* Build the mutual inductive entry *)
{ mind_entry_params = List.map prepare_param ctx_params;
mind_entry_record = false;
mind_entry_finite = finite;
- mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
+ mind_entry_inds = entries },
+ impls
let eq_constr_expr c1 c2 =
try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -591,7 +597,7 @@ let extract_params indl =
| [] -> anomaly "empty list of inductive types"
| params::paramsl ->
if not (List.for_all (eq_local_binders params) paramsl) then error
- "Parameters should be syntactically the same for each inductive type";
+ "Parameters should be syntactically the same for each inductive type.";
params
let prepare_inductive ntnl indl =
@@ -613,23 +619,17 @@ let _ =
optread = (fun () -> !elim_flag) ;
optwrite = (fun b -> elim_flag := b) }
-
-let lift_implicits n =
- List.map (fun x ->
- match fst x with
- ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
- | _ -> x)
-
let declare_mutual_with_eliminations isrecord mie impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let params = List.length mie.mind_entry_params in
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;
list_iter_i
(fun j impls ->
maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
- (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+ (is_implicit_args()) impls)
constrimpls)
impls;
if_verbose ppnl (minductive_message names);
@@ -672,7 +672,7 @@ let recursive_message indexes = function
| None -> mt ())
let corecursive_message _ = function
- | [] -> error "no corecursive definition"
+ | [] -> error "No corecursive definition."
| [id] -> pr_id id ++ str " is corecursively defined"
| l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
spc () ++ str "are corecursively defined")
@@ -827,6 +827,7 @@ let interp_recursive fixkind l boxed =
List.split (List.map (interp_fix_context evdref env) fixl) in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
+ let fixtypes = List.map (nf_evar (evars_of !evdref)) fixtypes in
let env_rec = push_named_types env fixnames fixtypes in
(* Get interpretation metadatas *)
@@ -1005,7 +1006,7 @@ let build_combined_scheme name schemes =
let qualid = qualid_of_reference refe in
let cst = try
Nametab.locate_constant (snd qualid)
- with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared")
+ with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")
in
let ty = Typeops.type_of_constant env cst in
qualid, cst, ty)
@@ -1051,15 +1052,21 @@ let retrieve_first_recthm = function
(Option.map Declarations.force body,opaq)
| _ -> assert false
+let default_thm_id = id_of_string "Unnamed_thm"
+
let compute_proof_name = function
| Some (loc,id) ->
(* We check existence here: it's a bit late at Qed time *)
if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
- user_err_loc (loc,"",pr_id id ++ str " already exists");
+ user_err_loc (loc,"",pr_id id ++ str " already exists.");
id
| None ->
- next_global_ident_away false (id_of_string "Unnamed_thm")
- (Pfedit.get_all_proof_names ())
+ let rec next avoid id =
+ let id = next_global_ident_away false id avoid in
+ if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id
+ else id
+ in
+ next (Pfedit.get_all_proof_names ()) default_thm_id
let save_remaining_recthms (local,kind) body opaq i (id,(t_i,imps)) =
match body with
@@ -1207,7 +1214,7 @@ let start_proof_com kind thms hook =
let check_anonymity id save_ident =
if atompart_of_id id <> "Unnamed_thm" then
- error "This command can only be used for unnamed theorem"
+ error "This command can only be used for unnamed theorem."
(*
message("Overriding name "^(string_of_id id)^" and using "^save_ident)
*)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 26526a5f..8ac8c234 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: command.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
(*i*)
open Util
@@ -56,18 +56,16 @@ 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 ->
- Term.types list ->
- Impargs.manual_explicitation list list ->
+val compute_interning_datas : Environ.env -> 'a list -> 'b list ->
+ Term.types list ->Impargs.manual_explicitation list list ->
'a list *
- ('b *
- (Names.identifier list * Impargs.implicits_list *
- Topconstr.scope_name option list))
+ ('b * (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 declare_mutual_with_eliminations :
@@ -87,10 +85,10 @@ type fixpoint_expr = {
fix_type : constr_expr
}
-val recursive_message : Decl_kinds.definition_object_kind ->
- int array option -> Names.identifier list -> Pp.std_ppcmds
+val recursive_message : definition_object_kind ->
+ int array option -> identifier list -> Pp.std_ppcmds
-val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier ->
+val declare_fix : bool -> definition_object_kind -> identifier ->
constr -> types -> Impargs.manual_explicitation list -> global_reference
val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e6d2deec..f8c57ad2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml 11062 2008-06-06 14:19:50Z notin $ *)
+(* $Id: coqtop.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
open Pp
open Util
@@ -72,10 +72,12 @@ 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_include d p = push_include (d,p)
-let set_rec_include d p = check_coq_overwriting p; push_rec_include (d,p)
-let set_default_include d = set_include d Nameops.default_root_prefix
-let set_default_rec_include d = set_rec_include d Nameops.default_root_prefix
+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 set_rec_include d p =
+ let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
@@ -187,15 +189,22 @@ let parse_args is_ide =
| "-impredicative-set" :: rem ->
set_engagement Declarations.ImpredicativeSet; parse rem
+ | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
+ | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
| ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
| ("-I"|"-include") :: [] -> usage ()
- | "-R" :: d :: p :: rem ->set_rec_include d (dirpath_of_string p);parse rem
+ | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
+ | "-R" :: d :: "-as" :: [] -> usage ()
+ | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
| "-R" :: ([] | [_]) -> usage ()
| "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
| "-top" :: [] -> usage ()
+ | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
+ | "-exclude-dir" :: [] -> usage ()
+
| "-notop" :: rem -> unset_toplevel_name (); parse rem
| "-q" :: rem -> no_load_rc (); parse rem
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
deleted file mode 100644
index 4ef5d5fd..00000000
--- a/toplevel/fhimsg.ml
+++ /dev/null
@@ -1,355 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: fhimsg.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Environ
-open Type_errors
-open Reduction
-open G_minicoq
-
-module type Printer = sig
- val pr_term : path_kind -> env -> constr -> std_ppcmds
-end
-
-module Make = functor (P : Printer) -> struct
-
- let print_decl k env (s,typ) =
- let ptyp = P.pr_term k env typ in
- (spc () ++ pr_id s ++ str" : " ++ ptyp)
-
- let print_binding k env = function
- | Anonymous,ty ->
- (spc () ++ str"_" ++ str" : " ++ P.pr_term k env ty)
- | Name id,ty ->
- (spc () ++ pr_id id ++ str" : " ++ P.pr_term k env ty)
-
-(****
- let sign_it_with f sign e =
- snd (fold_named_context
- (fun (id,v,t) (sign,e) -> (add_named_decl (id,v,t) sign, f id t sign e))
- sign (empty_named_context,e))
-
- let dbenv_it_with f env e =
- snd (dbenv_it
- (fun na t (env,e) -> (add_rel_decl (na,t) env, f na t env e))
- env (gLOB(get_globals env),e))
-****)
-
- let pr_env k env =
- let sign_env =
- fold_named_context
- (fun env (id,_,t) pps ->
- let pidt = print_decl k env (id,t) in (pps ++ fnl () ++ pidt))
- env (mt ())
- in
- let db_env =
- fold_rel_context
- (fun env (na,_,t) pps ->
- let pnat = print_binding k env (na,t) in (pps ++ fnl () ++ pnat))
- env (mt ())
- in
- (sign_env ++ db_env)
-
- let pr_ne_ctx header k env =
- if rel_context env = [] && named_context env = [] then
- (mt ())
- else
- (header ++ pr_env k env)
-
-
-let explain_unbound_rel k ctx n =
- let pe = pr_ne_ctx (str"in environment") k ctx in
- (str"Unbound reference: " ++ pe ++ fnl () ++
- str"The reference " ++ int n ++ str" is free")
-
-let explain_not_type k ctx c =
- let pe = pr_ne_ctx (str"In environment") k ctx in
- let pc = P.pr_term k ctx c in
- (pe ++ cut () ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
- str"should be typed by Set, Prop or Type.");;
-
-let explain_bad_assumption k ctx c =
- let pc = P.pr_term k ctx c in
- (str "Cannot declare a variable or hypothesis over the term" ++
- brk(1,1) ++ pc ++ spc () ++ str "because this term is not a type.");;
-
-let explain_reference_variables id =
- (str "the constant" ++ spc () ++ pr_id id ++ spc () ++
- str "refers to variables which are not in the context")
-
-let msg_bad_elimination ctx k = function
- | Some(ki,kp,explanation) ->
- let pki = P.pr_term k ctx ki in
- let pkp = P.pr_term k ctx kp in
- (hov 0
- (fnl () ++ str "Elimination of an inductive object of sort : " ++
- pki ++ brk(1,0) ++
- str "is not allowed on a predicate in sort : " ++ pkp ++fnl () ++
- str "because" ++ spc () ++ str explanation))
- | None ->
- (mt ())
-
-let explain_elim_arity k ctx ind aritylst c pj okinds =
- let pi = P.pr_term k ctx ind in
- let ppar = prlist_with_sep pr_coma (P.pr_term k ctx) aritylst in
- let pc = P.pr_term k ctx c in
- let pp = P.pr_term k ctx pj.uj_val in
- let ppt = P.pr_term k ctx pj.uj_type in
- (str "Incorrect elimination of" ++ brk(1,1) ++ pc ++ spc () ++
- str "in the inductive type" ++ brk(1,1) ++ pi ++ fnl () ++
- str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
- str "has type" ++ brk(1,1) ++ ppt ++ fnl () ++
- str "It should be one of :" ++ brk(1,1) ++ hov 0 ppar ++ fnl () ++
- msg_bad_elimination ctx k okinds)
-
-let explain_case_not_inductive k ctx cj =
- let pc = P.pr_term k ctx cj.uj_val in
- let pct = P.pr_term k ctx cj.uj_type in
- (str "In Cases expression" ++ brk(1,1) ++ pc ++ spc () ++
- str "has type" ++ brk(1,1) ++ pct ++ spc () ++
- str "which is not an inductive definition")
-
-let explain_number_branches k ctx cj expn =
- let pc = P.pr_term k ctx cj.uj_val in
- let pct = P.pr_term k ctx cj.uj_val in
- (str "Cases on term" ++ brk(1,1) ++ pc ++ spc () ++
- str "of type" ++ brk(1,1) ++ pct ++ spc () ++
- str "expects " ++ int expn ++ str " branches")
-
-let explain_ill_formed_branch k ctx c i actty expty =
- let pc = P.pr_term k ctx c in
- let pa = P.pr_term k ctx actty in
- let pe = P.pr_term k ctx expty in
- (str "In Cases expression on term" ++ brk(1,1) ++ pc ++
- spc () ++ str "the branch " ++ int (i+1) ++
- str " has type" ++ brk(1,1) ++ pa ++ spc () ++
- str "which should be:" ++ brk(1,1) ++ pe)
-
-let explain_generalization k ctx (name,var) c =
- let pe = pr_ne_ctx (str"in environment") k ctx in
- let pv = P.pr_term k ctx var in
- let pc = P.pr_term k (push_rel (name,None,var) ctx) c in
- (str"Illegal generalization: " ++ pe ++ fnl () ++
- str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
- str"over" ++ brk(1,1) ++ pc ++ spc () ++
- str"which should be typed by Set, Prop or Type.")
-
-let explain_actual_type k ctx c ct pt =
- let pe = pr_ne_ctx (str"In environment") k ctx in
- let pc = P.pr_term k ctx c in
- let pct = P.pr_term k ctx ct in
- let pt = P.pr_term k ctx pt in
- (pe ++ fnl () ++
- str"The term" ++ brk(1,1) ++ pc ++ spc () ++
- str"does not have type" ++ brk(1,1) ++ pt ++ fnl () ++
- str"Actually, it has type" ++ brk(1,1) ++ pct)
-
-let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
- let ctx = make_all_name_different ctx in
- let pe = pr_ne_ctx (str"in environment") k ctx in
- let pr = pr_term k ctx rator.uj_val in
- let prt = pr_term k ctx rator.uj_type in
- let term_string = if List.length randl > 1 then "terms" else "term" in
- let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
- let appl = prlist_with_sep pr_fnl
- (fun c ->
- let pc = pr_term k ctx c.uj_val in
- let pct = pr_term k ctx c.uj_type in
- hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
- in
- (str"Illegal application (Type Error): " ++ pe ++ fnl () ++
- str"The term" ++ brk(1,1) ++ pr ++ spc () ++
- str"of type" ++ brk(1,1) ++ prt ++ spc () ++
- str("cannot be applied to the "^term_string) ++ fnl () ++
- str" " ++ v 0 appl ++ fnl () ++
- str"The " ++int n ++ str (many^" term of type ") ++
- pr_term k ctx actualtyp ++
- str" should be of type " ++ pr_term k ctx exptyp)
-
-let explain_cant_apply_not_functional k ctx rator randl =
- let ctx = make_all_name_different ctx in
- let pe = pr_ne_ctx (str"in environment") k ctx in
- let pr = pr_term k ctx rator.uj_val in
- let prt = pr_term k ctx rator.uj_type in
- let term_string = if List.length randl > 1 then "terms" else "term" in
- let appl = prlist_with_sep pr_fnl
- (fun c ->
- let pc = pr_term k ctx c.uj_val in
- let pct = pr_term k ctx c.uj_type in
- hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
- in
- (str"Illegal application (Non-functional construction): " ++ pe ++ fnl () ++
- str"The term" ++ brk(1,1) ++ pr ++ spc () ++
- str"of type" ++ brk(1,1) ++ prt ++ spc () ++
- str("cannot be applied to the "^term_string) ++ fnl () ++
- str" " ++ v 0 appl ++ fnl ())
-
-(* (co)fixpoints *)
-let explain_ill_formed_rec_body k ctx err names i vdefs =
- let str = match err with
-
- (* Fixpoint guard errors *)
- | NotEnoughAbstractionInFixBody ->
- (str "Not enough abstractions in the definition")
- | RecursionNotOnInductiveType ->
- (str "Recursive definition on a non inductive type")
- | RecursionOnIllegalTerm ->
- (str "Recursive call applied to an illegal term")
- | NotEnoughArgumentsForFixCall ->
- (str "Not enough arguments for the recursive call")
-
- (* CoFixpoint guard errors *)
- (* TODO : récupérer le contexte des termes pour pouvoir les afficher *)
- | CodomainNotInductiveType c ->
- (str "The codomain is" ++ spc () ++ P.pr_term k ctx c ++ spc () ++
- str "which should be a coinductive type")
- | NestedRecursiveOccurrences ->
- (str "Nested recursive occurrences")
- | UnguardedRecursiveCall c ->
- (str "Unguarded recursive call")
- | RecCallInTypeOfAbstraction c ->
- (str "Not allowed recursive call in the domain of an abstraction")
- | RecCallInNonRecArgOfConstructor c ->
- (str "Not allowed recursive call in a non-recursive argument of constructor")
- | RecCallInTypeOfDef c ->
- (str "Not allowed recursive call in the type of a recursive definition")
- | RecCallInCaseFun c ->
- (str "Not allowed recursive call in a branch of cases")
- | RecCallInCaseArg c ->
- (str "Not allowed recursive call in the argument of cases")
- | RecCallInCasePred c ->
- (str "Not allowed recursive call in the type of cases in")
- | NotGuardedForm c ->
- str "Sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
- str "not in guarded form (should be a constructor, Cases or CoFix)"
-in
- let pvd = P.pr_term k ctx vdefs.(i) in
- let s =
- match names.(i) with Name id -> string_of_id id | Anonymous -> "_" in
- (str ++ fnl () ++ str"The " ++
- if Array.length vdefs = 1 then (mt ()) else (int (i+1) ++ str "-th ") ++
- str"recursive definition" ++ spc () ++ str s ++
- spc () ++ str":=" ++ spc () ++ pvd ++ spc () ++
- str "is not well-formed")
-
-let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
- let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
- let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in
- let pv = P.pr_term k ctx vargs.(i) in
- (str"The " ++
- if Array.length vdefj = 1 then (mt ()) else (int (i+1) ++ str "-th") ++
- str"recursive definition" ++ spc () ++ pvd ++ spc () ++
- str "has type" ++ spc () ++ pvdt ++spc () ++ str "it should be" ++ spc () ++ pv)
-
-let explain_not_inductive k ctx c =
- let pc = P.pr_term k ctx c in
- (str"The term" ++ brk(1,1) ++ pc ++ spc () ++
- str "is not an inductive definition")
-
-let explain_ml_case k ctx mes c ct br brt =
- let pc = P.pr_term k ctx c in
- let pct = P.pr_term k ctx ct in
- let expln =
- match mes with
- | "Inductive" -> (pct ++ str "is not an inductive definition")
- | "Predicate" -> (str "ML case not allowed on a predicate")
- | "Absurd" -> (str "Ill-formed case expression on an empty type")
- | "Decomp" ->
- let plf = P.pr_term k ctx br in
- let pft = P.pr_term k ctx brt in
- (str "The branch " ++ plf ++ ws 1 ++ cut () ++ str "has type " ++ pft ++
- ws 1 ++ cut () ++
- str "does not correspond to the inductive definition")
- | "Dependent" ->
- (str "ML case not allowed for a dependent case elimination")
- | _ -> (mt ())
- in
- hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++
- str "of type" ++ ws 1 ++ pct ++ ws 1 ++ cut () ++
- str "which is an inductive predicate." ++ fnl () ++ expln)
-
-let explain_type_error k ctx = function
- | UnboundRel n ->
- explain_unbound_rel k ctx n
- | NotAType c ->
- explain_not_type k ctx c.uj_val
- | BadAssumption c ->
- explain_bad_assumption k ctx c
- | ReferenceVariables id ->
- explain_reference_variables id
- | ElimArity (ind, aritylst, c, pj, okinds) ->
- explain_elim_arity k ctx (mkMutInd ind) aritylst c pj okinds
- | CaseNotInductive cj ->
- explain_case_not_inductive k ctx cj
- | NumberBranches (cj, n) ->
- explain_number_branches k ctx cj n
- | IllFormedBranch (c, i, actty, expty) ->
- explain_ill_formed_branch k ctx c i actty expty
- | Generalization (nvar, c) ->
- explain_generalization k ctx nvar c.uj_val
- | ActualType (c, ct, pt) ->
- explain_actual_type k ctx c ct pt
- | CantApplyBadType (s, rator, randl) ->
- explain_cant_apply_bad_type k ctx s rator randl
- | CantApplyNonFunctional (rator, randl) ->
- explain_cant_apply_not_functional k ctx rator randl
- | IllFormedRecBody (i, lna, vdefj, vargs) ->
- explain_ill_formed_rec_body k ctx i lna vdefj vargs
- | IllTypedRecBody (i, lna, vdefj, vargs) ->
- explain_ill_typed_rec_body k ctx i lna vdefj vargs
-(*
- | NotInductive c ->
- explain_not_inductive k ctx c
- | MLCase (mes,c,ct,br,brt) ->
- explain_ml_case k ctx mes c ct br brt
-*)
- | _ ->
- (str "Unknown type error (TODO)")
-
-let explain_refiner_bad_type k ctx arg ty conclty =
- errorlabstrm "Logic.conv_leq_goal"
- (str"refiner was given an argument" ++ brk(1,1) ++
- P.pr_term k ctx arg ++ spc () ++
- str"of type" ++ brk(1,1) ++ P.pr_term k ctx ty ++ spc () ++
- str"instead of" ++ brk(1,1) ++ P.pr_term k ctx conclty)
-
-let explain_refiner_occur_meta k ctx t =
- errorlabstrm "Logic.mk_refgoals"
- (str"cannot refine with term" ++ brk(1,1) ++ P.pr_term k ctx t ++
- spc () ++ str"because there are metavariables, and it is" ++
- spc () ++ str"neither an application nor a Case")
-
-let explain_refiner_cannot_applt k ctx t harg =
- errorlabstrm "Logic.mkARGGOALS"
- (str"in refiner, a term of type " ++ brk(1,1) ++
- P.pr_term k ctx t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
- P.pr_term k ctx harg)
-
-let explain_occur_check k ctx ev rhs =
- let id = "?" ^ string_of_int ev in
- let pt = P.pr_term k ctx rhs in
- errorlabstrm "Trad.occur_check"
- (str"Occur check failed: tried to define " ++ str id ++
- str" with term" ++ brk(1,1) ++ pt)
-
-let explain_not_clean k ctx sp t =
- let c = mkRel (Intset.choose (free_rels t)) in
- let id = string_of_id (Names.basename sp) in
- let var = P.pr_term k ctx c in
- errorlabstrm "Trad.not_clean"
- (str"Tried to define " ++ str id ++
- str" with a term using variable " ++ var ++ spc () ++
- str"which is not in its scope.")
-
-end
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 579acffa..41783faa 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml 11150 2008-06-19 11:38:27Z msozeau $ *)
+(* $Id: himsg.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -392,7 +392,7 @@ let explain_cannot_unify env m n =
let pm = pr_lconstr_env env m in
let pn = pr_lconstr_env env n in
str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
- str "with" ++ brk(1,1) ++ pn
+ str "with" ++ brk(1,1) ++ pn ++ str "."
let explain_cannot_unify_local env m n subn =
let pm = pr_lconstr_env env m in
@@ -400,34 +400,31 @@ let explain_cannot_unify_local env m n subn =
let psubn = pr_lconstr_env env subn in
str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
- psubn ++ str " contains local variables"
+ psubn ++ str " contains local variables."
let explain_refiner_cannot_generalize env ty =
str "Cannot find a well-typed generalisation of the goal with type: " ++
- pr_lconstr_env env ty
+ pr_lconstr_env env ty ++ str "."
let explain_no_occurrence_found env c id =
str "Found no subterm matching " ++ pr_lconstr_env env c ++
str " in " ++
(match id with
| Some id -> pr_id id
- | None -> str"the current goal")
+ | None -> str"the current goal") ++ str "."
let explain_cannot_unify_binding_type env m n =
let pm = pr_lconstr_env env m in
let pn = pr_lconstr_env env n in
str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
- str "which should be unifiable with" ++ brk(1,1) ++ pn
+ str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
let explain_cannot_find_well_typed_abstraction env p l =
- let la,lc = list_chop (List.length l - 1) l in
str "Abstracting over the " ++
str (plural (List.length l) "term") ++ spc () ++
- hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++
- (if la<>[] then str " and" ++ spc () else mt()) ++
- pr_lconstr_env env (List.hd lc)) ++ spc () ++
+ hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
- str "which is ill-typed"
+ str "which is ill-typed."
let explain_type_error env err =
let env = make_all_name_different env in
@@ -487,11 +484,11 @@ let explain_pretype_error env err =
(* Typeclass errors *)
let explain_not_a_class env c =
- pr_constr_env env c ++ str" is not a declared type class"
+ pr_constr_env env c ++ str" is not a declared type class."
let explain_unbound_method env cid id =
str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++
- pr_global cid
+ pr_global cid ++ str "."
let pr_constr_exprs exprs =
hv 0 (List.fold_right
@@ -532,7 +529,7 @@ let explain_unsatisfiable_constraints env evd constr =
let explain_mismatched_contexts env c i j =
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
- hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++
+ hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ fnl () ++ brk (1,1) ++
hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
let explain_typeclass_error env err =
@@ -549,21 +546,20 @@ let explain_refiner_bad_type arg ty conclty =
str "Refiner was given an argument" ++ brk(1,1) ++
pr_lconstr arg ++ spc () ++
str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
- str "instead of" ++ brk(1,1) ++ pr_lconstr conclty
+ str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "."
let explain_refiner_unresolved_bindings l =
- let l = map_succeed (function Name id -> id | _ -> failwith "") l in
str "Unable to find an instance for the " ++
str (plural (List.length l) "variable") ++ spc () ++
- prlist_with_sep pr_coma pr_id l
+ prlist_with_sep pr_coma pr_name l ++ str"."
let explain_refiner_cannot_apply t harg =
- str "In refiner, a term of type " ++ brk(1,1) ++
+ str "In refiner, a term of type" ++ brk(1,1) ++
pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
- pr_lconstr harg
+ pr_lconstr harg ++ str "."
let explain_refiner_not_well_typed c =
- str "The term " ++ pr_lconstr c ++ str " is not well-typed"
+ str "The term " ++ pr_lconstr c ++ str " is not well-typed."
let explain_intro_needs_product () =
str "Introduction tactics needs products."
@@ -706,7 +702,7 @@ let explain_bad_constructor env cstr ind =
str "is expected."
let decline_string n s =
- if n = 0 then "no "^s
+ if n = 0 then "no "^s^"s"
else if n = 1 then "1 "^s
else (string_of_int n^" "^s^"s")
@@ -781,3 +777,40 @@ let explain_reduction_tactic_error = function
str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' e
+
+let explain_ltac_call_trace (last,trace,loc) =
+ let calls = last :: List.rev (List.map snd trace) in
+ let pr_call = function
+ | Proof_type.LtacNotationCall s -> quote (str s)
+ | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+ | Proof_type.LtacVarCall (id,t) ->
+ quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+ | Proof_type.LtacAtomCall (te,otac) -> quote
+ (Pptactic.pr_glob_tactic (Global.env())
+ (Tacexpr.TacAtom (dummy_loc,te)))
+ ++ (match !otac with
+ | Some te' when (Obj.magic te' <> te) ->
+ strbrk " (expanded to " ++ quote
+ (Pptactic.pr_tactic (Global.env())
+ (Tacexpr.TacAtom (dummy_loc,te')))
+ ++ str ")"
+ | _ -> mt ())
+ | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
+ let filter =
+ function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
+ let unboundvars = list_map_filter filter unboundvars in
+ quote (pr_rawconstr_env (Global.env()) c) ++
+ (if unboundvars <> [] or vars <> [] then
+ strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) ->
+ pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
+ (List.rev vars @ unboundvars)
+ else mt()) ++ str ")" in
+ if calls <> [] then
+ let kind_of_last_call = match list_last calls with
+ | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
+ | _ -> ", last call failed." in
+ hov 0 (str "In nested Ltac calls to " ++
+ pr_enum pr_call calls ++ strbrk kind_of_last_call)
+ else
+ mt ()
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 1b9e38ce..ff5991de 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: himsg.mli 10410 2007-12-31 13:11:55Z msozeau $ i*)
+(*i $Id: himsg.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
(*i*)
open Pp
@@ -40,3 +40,6 @@ val explain_pattern_matching_error :
val explain_reduction_tactic_error :
Tacred.reduction_tactic_error -> std_ppcmds
+
+val explain_ltac_call_trace :
+ Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc -> std_ppcmds
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fbeaea34..89ba6aac 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml 11121 2008-06-12 21:15:49Z herbelin $ *)
+(* $Id: metasyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -127,7 +127,7 @@ let print_grammar = function
Gram.Entry.print Pcoq.Vernac_.gallina;
msgnl (str "Entry gallina_ext is");
Gram.Entry.print Pcoq.Vernac_.gallina_ext;
- | _ -> error "Unknown or unprintable grammar entry"
+ | _ -> error "Unknown or unprintable grammar entry."
(**********************************************************************)
(* Parse a format (every terminal starting with a letter or a single
@@ -143,11 +143,11 @@ let parse_format (loc,str) =
if n = 0 then l else push_token (UnpTerminal (String.make n ' ')) l in
let close_box i b = function
| a::(_::_ as l) -> push_token (UnpBox (b,a)) l
- | _ -> error "Non terminated box in format" in
+ | _ -> error "Non terminated box in format." in
let close_quotation i =
if i < String.length str & str.[i] = '\'' & (i+1 = l or str.[i+1] = ' ')
then i+1
- else error "Incorrectly terminated quoted expression" in
+ else error "Incorrectly terminated quoted expression." in
let rec spaces n i =
if i < String.length str & str.[i] = ' ' then spaces (n+1) (i+1)
else n in
@@ -155,10 +155,10 @@ let parse_format (loc,str) =
if i < String.length str & str.[i] <> ' ' then
if str.[i] = '\'' & quoted &
(i+1 >= String.length str or str.[i+1] = ' ')
- then if n=0 then error "Empty quoted token" else n
+ then if n=0 then error "Empty quoted token." else n
else nonspaces quoted (n+1) (i+1)
else
- if quoted then error "Spaces are not allowed in (quoted) symbols"
+ if quoted then error "Spaces are not allowed in (quoted) symbols."
else n in
let rec parse_non_format i =
let n = nonspaces false 0 i in
@@ -189,8 +189,8 @@ let parse_format (loc,str) =
(* Parse " [ .. ", *)
| ' ' | '\'' ->
parse_box (fun n -> PpHOVB n) (i+1)
- | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format"
- else error "\"v\", \"hv\" or \" \" expected after \"[\" in format"
+ | _ -> error "\"v\", \"hv\", \" \" expected after \"[\" in format."
+ else error "\"v\", \"hv\" or \" \" expected after \"[\" in format."
(* Parse "]" *)
| ']' ->
([] :: parse_token (close_quotation (i+1)))
@@ -201,7 +201,7 @@ let parse_format (loc,str) =
(parse_token (close_quotation (i+n))))
else
if n = 0 then []
- else error "Ending spaces non part of a format annotation"
+ else error "Ending spaces non part of a format annotation."
and parse_box box i =
let n = spaces 0 i in
close_box i (box n) (parse_token (close_quotation (i+n)))
@@ -223,9 +223,9 @@ let parse_format (loc,str) =
try
if str <> "" then match parse_token 0 with
| [l] -> l
- | _ -> error "Box closed without being opened in format"
+ | _ -> error "Box closed without being opened in format."
else
- error "Empty format"
+ error "Empty format."
with e ->
Stdpp.raise_with_loc loc e
@@ -274,11 +274,11 @@ let rec find_pattern xl = function
| [NonTerminal x], NonTerminal x' :: l' ->
(x,x',xl),l'
| [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
- error ("The token "^s^" occurs on one side of \"..\" but not on the other side")
+ error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
| [NonTerminal _], Break s :: _ | Break s :: _, _ ->
- error ("A break occurs on one side of \"..\" but not on the other side")
+ error ("A break occurs on one side of \"..\" but not on the other side.")
| ((SProdList _ | NonTerminal _) :: _ | []), _ ->
- error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"")
+ 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
@@ -320,12 +320,13 @@ let rec raw_analyse_notation_tokens = function
| String ".." :: sl ->
let (vars,l) = raw_analyse_notation_tokens sl in
(list_add_set ldots_var vars, NonTerminal ldots_var :: l)
+ | String "_" :: _ -> error "_ must be quoted."
| String x :: sl when is_normal_token x ->
Lexer.check_ident x;
let id = Names.id_of_string x in
let (vars,l) = raw_analyse_notation_tokens sl in
if List.mem id vars then
- error ("Variable "^x^" occurs more than once");
+ error ("Variable "^x^" occurs more than once.");
(id::vars, NonTerminal id :: l)
| String s :: sl ->
Lexer.check_keyword s;
@@ -481,10 +482,10 @@ let make_hunks etyps symbols from =
(* Build default printing rules from explicit format *)
-let error_format () = error "The format does not match the notation"
+let error_format () = error "The format does not match the notation."
let rec split_format_at_ldots hd = function
- | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt
+ | UnpTerminal s :: fmt when s = string_of_id ldots_var -> List.rev hd, fmt
| u :: fmt ->
check_no_ldots_in_box u;
split_format_at_ldots (u::hd) fmt
@@ -494,7 +495,7 @@ and check_no_ldots_in_box = function
| UnpBox (_,fmt) ->
(try
let _ = split_format_at_ldots [] fmt in
- error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse")
+ error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse.")
with Exit -> ())
| _ -> ()
@@ -512,7 +513,7 @@ let read_recursive_format sl fmt =
let rec get_tail = function
| a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt)
| [], tail -> skip_var_in_recursive_format tail
- | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"" in
+ | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"." in
let slfmt, fmt = get_head fmt in
slfmt, get_tail (slfmt, fmt)
@@ -594,7 +595,7 @@ let make_production etyps symbols =
let y = match List.assoc x etyps with
| ETConstr x -> x
| _ ->
- error "Component of recursive patterns in notation must be constr" in
+ error "Component of recursive patterns in notation must be constr." in
let typ = ETConstrList (y,sl) in
NonTerm (typ, Some (x,typ)) :: l)
symbols [] in
@@ -640,7 +641,7 @@ let error_incompatible_level ntn oldprec prec =
(str ("Notation "^ntn^" is already defined") ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
- pr_level ntn prec)
+ pr_level ntn prec ++ str ".")
let cache_one_syntax_extension (prec,ntn,gr,pp) =
try
@@ -692,34 +693,34 @@ let interp_modifiers modl =
| SetEntryType (s,typ) :: l ->
let id = id_of_string s in
if List.mem_assoc id etyps then
- error (s^" is already assigned to an entry or constr level");
+ error (s^" is already assigned to an entry or constr level.");
interp assoc level ((id,typ)::etyps) format l
| SetItemLevel ([],n) :: l ->
interp assoc level etyps format l
| SetItemLevel (s::idl,n) :: l ->
let id = id_of_string s in
if List.mem_assoc id etyps then
- error (s^" is already assigned to an entry or constr level");
+ error (s^" is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
| SetLevel n :: l ->
- if level <> None then error "A level is given more than once";
+ if level <> None then error "A level is given more than once.";
interp assoc (Some n) etyps format l
| SetAssoc a :: l ->
- if assoc <> None then error "An associativity is given more than once";
+ if assoc <> None then error"An associativity is given more than once.";
interp (Some a) level etyps format l
| SetOnlyParsing :: l ->
onlyparsing := true;
interp assoc level etyps format l
| SetFormat s :: l ->
- if format <> None then error "A format is given more than once";
+ if format <> None then error "A format is given more than once.";
interp assoc level etyps (Some s) l
in interp None None [] None modl
let check_infix_modifiers modifiers =
let (assoc,level,t,b,fmt) = interp_modifiers modifiers in
if t <> [] then
- error "explicit entry level or type unexpected in infix notation"
+ error "explicit entry level or type unexpected in infix notation."
let no_syntax_modifiers modifiers =
modifiers = [] or modifiers = [SetOnlyParsing]
@@ -739,9 +740,9 @@ let set_entry_type etyps (x,typ) =
let check_rule_productivity l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
- error "A notation must include at least one symbol";
+ error "A notation must include at least one symbol.";
if (match l with SProdList _ :: _ -> true | _ -> false) then
- error "A recursive notation must start with at least one symbol"
+ 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
@@ -752,38 +753,38 @@ let find_precedence lev etyps symbols =
| NonTerminal x :: _ ->
(try match List.assoc x etyps with
| ETConstr _ ->
- error "The level of the leftmost non-terminal cannot be changed"
+ error "The level of the leftmost non-terminal cannot be changed."
| ETIdent | ETBigint | ETReference ->
if lev = None then
- Flags.if_verbose msgnl (str "Setting notation at level 0")
+ Flags.if_verbose msgnl (str "Setting notation at level 0.")
else
if lev <> Some 0 then
- error "A notation starting with an atomic expression must be at level 0";
+ error "A notation starting with an atomic expression must be at level 0.";
0
| ETPattern | ETOther _ -> (* Give a default ? *)
if lev = None then
- error "Need an explicit level"
+ error "Need an explicit level."
else Option.get lev
| ETConstrList _ -> assert false (* internally used in grammar only *)
with Not_found ->
if lev = None then
- error "A left-recursive notation must have an explicit level"
+ error "A left-recursive notation must have an explicit level."
else Option.get lev)
| Terminal _ ::l when
(match list_last symbols with Terminal _ -> true |_ -> false)
->
if lev = None then
- (Flags.if_verbose msgnl (str "Setting notation at level 0"); 0)
+ (Flags.if_verbose msgnl (str "Setting notation at level 0."); 0)
else Option.get lev
| _ ->
- if lev = None then error "Cannot determine the level";
+ if lev = None then error "Cannot determine the level.";
Option.get lev
let check_curly_brackets_notation_exists () =
try let _ = Notation.level_of_notation "{ _ }" in ()
with Not_found ->
error "Notations involving patterns of the form \"{ _ }\" are treated \n\
-specially and require that the notation \"{ _ }\" is already reserved"
+specially and require that the notation \"{ _ }\" is already reserved."
(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
let remove_curly_brackets l =
@@ -970,7 +971,7 @@ let add_syntax_extension local mv =
let add_notation_interpretation df names c sc =
try add_notation_interpretation_core false df names c sc false
with NoSyntaxRule ->
- error "Parsing rule for this notation has to be previously declared"
+ error "Parsing rule for this notation has to be previously declared."
(* Main entry point *)
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
deleted file mode 100644
index e688d50e..00000000
--- a/toplevel/minicoq.ml
+++ /dev/null
@@ -1,149 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* $Id: minicoq.ml 10346 2007-12-05 21:11:19Z aspiwack $ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Sign
-open Declarations
-open Inductive
-open Type_errors
-open Safe_typing
-open G_minicoq
-
-let (env : safe_environment ref) = ref empty_environment
-
-let locals () =
- List.map (fun (id,b,t) -> (id, make_path [] id CCI))
- (named_context !env)
-
-let lookup_named id =
- let rec look n = function
- | [] -> mkVar id
- | (Name id')::_ when id = id' -> mkRel n
- | _::r -> look (succ n) r
- in
- look 1
-
-let args sign = Array.of_list (instance_from_section_context sign)
-
-let rec globalize bv c = match kind_of_term c with
- | Var id -> lookup_named id bv
- | Const (sp, _) ->
- let cb = lookup_constant sp !env in mkConst (sp, args cb.const_hyps)
- | Ind (sp,_ as spi, _) ->
- let mib = lookup_mind sp !env in mkMutInd (spi, args mib.mind_hyps)
- | Construct ((sp,_),_ as spc, _) ->
- let mib = lookup_mind sp !env in mkMutConstruct (spc, args mib.mind_hyps)
- | _ -> map_constr_with_named_binders (fun na l -> na::l) globalize bv c
-
-let check c =
- let c = globalize [] c in
- let (j,u) = safe_infer !env c in
- let ty = j_type j in
- let pty = pr_term CCI (env_of_safe_env !env) ty in
- mSGNL (hov 0 (str" :" ++ spc () ++ hov 0 pty ++ fnl ()))
-
-let definition id ty c =
- let c = globalize [] c in
- let ty = Option.map (globalize []) ty in
- let ce = { const_entry_body = c; const_entry_type = ty } in
- let sp = make_path [] id CCI in
- env := add_constant sp ce (locals()) !env;
- mSGNL (hov 0 (pr_id id ++ spc () ++ str"is defined" ++ fnl ()))
-
-let parameter id t =
- let t = globalize [] t in
- let sp = make_path [] id CCI in
- env := add_parameter sp t (locals()) !env;
- mSGNL (hov 0 (str"parameter" ++ spc () ++ pr_id id ++
- spc () ++ str"is declared" ++ fnl ()))
-
-let variable id t =
- let t = globalize [] t in
- env := push_named_assum (id,t) !env;
- mSGNL (hov 0 (str"variable" ++ spc () ++ pr_id id ++
- spc () ++ str"is declared" ++ fnl ()))
-
-let inductive par inds =
- let nparams = List.length par in
- let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in
- let name_inds = List.map (fun (id,_,_) -> Name id) inds in
- let bv = bvpar @ List.rev name_inds in
- let npar = List.map (fun (id,c) -> (Name id, globalize [] c)) par in
- let one_inductive (id,ar,cl) =
- let cv = List.map (fun (_,c) -> prod_it (globalize bv c) npar) cl in
- { mind_entry_nparams = nparams;
- mind_entry_params = List.map (fun (id,c) -> (id, LocalAssum c)) par;
- mind_entry_typename = id;
- mind_entry_arity = prod_it (globalize bvpar ar) npar;
- mind_entry_consnames = List.map fst cl;
- mind_entry_lc = cv }
- in
- let inds = List.map one_inductive inds in
- let mie = {
- mind_entry_finite = true;
- mind_entry_inds = inds }
- in
- let sp =
- let mi1 = List.hd inds in
- make_path [] mi1.mind_entry_typename CCI in
- env := add_mind sp mie (locals()) !env;
- mSGNL (hov 0 (str"inductive type(s) are declared" ++ fnl ()))
-
-
-let execute = function
- | Check c -> check c
- | Definition (id, ty, c) -> definition id ty c
- | Parameter (id, t) -> parameter id t
- | Variable (id, t) -> variable id t
- | Inductive (par,inds) -> inductive par inds
-
-let parse_file f =
- let c = open_in f in
- let cs = Stream.of_channel c in
- try
- while true do
- let c = Grammar.Entry.parse command cs in execute c
- done
- with
- | End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0
- | exn -> close_in c; raise exn
-
-module Explain = Fhimsg.Make(struct let pr_term = pr_term end)
-
-let rec explain_exn = function
- | TypeError (k,ctx,te) ->
- mSGNL (hov 0 (str "type error:" ++ spc () ++
- Explain.explain_type_error k ctx te ++ fnl ()))
- | Stdpp.Exc_located (_,exn) ->
- explain_exn exn
- | exn ->
- mSGNL (hov 0 (str"error: " ++ str (Printexc.to_string exn) ++ fnl ()))
-
-let top () =
- let cs = Stream.of_channel stdin in
- while true do
- try
- let c = Grammar.Entry.parse command cs in execute c
- with
- | End_of_file | Stdpp.Exc_located (_, End_of_file) -> exit 0
- | exn -> explain_exn exn
- done
-
-let main () =
- if Array.length Sys.argv = 1 then
- parse_file "test"
- else
- if Sys.argv.(1) = "-top" then top () else parse_file (Sys.argv.(1))
-
-let _ = Printexc.print main ()
-
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 30cffa34..ac30f890 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 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id: mltop.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Util
open Pp
@@ -99,8 +99,8 @@ let dir_ml_load s =
(try t.load_obj s
with
| (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
- | _ -> errorlabstrm "Mltop.load_object" [< str"Cannot link ml-object ";
- str s; str" to Coq code." >])
+ | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+ str s ++ str" to Coq code."))
(* TO DO: .cma loading without toplevel *)
| WithoutTop ->
IFDEF Byte THEN
@@ -108,7 +108,7 @@ let dir_ml_load s =
* 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 !coq_mlpath_copy s in
+ let _,gname = where_in_path true !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
Dynlink.add_interfaces
@@ -116,11 +116,11 @@ let dir_ml_load s =
(Filename.basename gname) ".cmo"))]
[Filename.dirname gname]
with | Dynlink.Error a ->
- errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message 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" >]
+ (str"Loading of ML object file forbidden in a native Coq.")
(* Dynamic interpretation of .ml *)
let dir_ml_use s =
@@ -145,10 +145,10 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
if exists_dir dir then
begin
add_ml_dir dir;
- Library.add_load_path (dir,coq_dirpath)
+ Library.add_load_path true (dir,coq_dirpath)
end
else
- msg_warning [< str ("Cannot open " ^ dir) >]
+ msg_warning (str ("Cannot open " ^ dir))
let convert_string d =
try Names.id_of_string d
@@ -159,19 +159,18 @@ let convert_string d =
failwith "caught"
let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
- let dirs = all_subdirs dir in
- let prefix = Names.repr_dirpath coq_dirpath in
- if dirs <> [] then
+ if exists_dir dir then
+ let dirs = all_subdirs dir in
+ let prefix = Names.repr_dirpath coq_dirpath in
let convert_dirs (lp,cp) =
- (lp,Names.make_dirpath
- ((List.map convert_string (List.rev cp))@prefix)) in
+ (lp,Names.make_dirpath (List.map convert_string (List.rev cp)@prefix)) in
let dirs = map_succeed convert_dirs dirs in
- begin
- List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
- List.iter Library.add_load_path dirs
- end
+ List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
+ add_ml_dir dir;
+ List.iter (Library.add_load_path false) dirs;
+ Library.add_load_path true (dir,Names.make_dirpath prefix)
else
- msg_warning [< str ("Cannot open " ^ dir) >]
+ msg_warning (str ("Cannot open " ^ dir))
(* convertit un nom quelconque en nom de fichier ou de module *)
let mod_of_name name =
@@ -191,7 +190,7 @@ let file_of_name name =
if (is_in_path !coq_mlpath_copy fname) then fname
else
errorlabstrm "Mltop.load_object"
- [< str"File not found on loadpath : "; str (bname^".cm[oa]") >]
+ (str"File not found on loadpath : " ++ str (bname^".cm[oa]"))
(* TODO: supprimer ce hack, si possible *)
(* Initialisation of ML modules that need the state (ex: tactics like
@@ -248,7 +247,7 @@ let unfreeze_ml_modules x =
load_object mname fname
else
errorlabstrm "Mltop.unfreeze_ml_modules"
- [< str"Loading of ML object file forbidden in a native Coq" >];
+ (str"Loading of ML object file forbidden in a native Coq.");
add_loaded_module mname)
x
@@ -271,11 +270,11 @@ let cache_ml_module_object (_,{mnames=mnames}) =
begin
try
if_verbose
- msg [< str"[Loading ML file "; str fname; str" ..." >];
+ 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)
@@ -294,11 +293,11 @@ let declare_ml_modules l =
let print_ml_path () =
let l = !coq_mlpath_copy in
- ppnl [< str"ML Load Path:"; fnl (); str" ";
- hv 0 (prlist_with_sep pr_fnl pr_str l) >]
+ ppnl (str"ML Load Path:" ++ fnl () ++ str" " ++
+ hv 0 (prlist_with_sep pr_fnl pr_str l))
(* Printing of loaded ML modules *)
let print_ml_modules () =
let l = get_loaded_modules () in
- pp [< str"Loaded ML Modules: " ; pr_vertical_list pr_str l >]
+ pp (str"Loaded ML Modules: " ++ pr_vertical_list pr_str l)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 5629bb71..306ab047 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
+(* $Id: record.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -31,29 +31,46 @@ open Topconstr
(********** definition d'un record (structure) **************)
-let interp_decl sigma env = function
- | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
- | Vernacexpr.DefExpr((_,id),c,t) ->
- let c = match t with
- | None -> c
- | Some t -> mkCastC (c, Rawterm.CastConv (DEFAULTcast,t))
- in
- let j = interp_constr_judgment Evd.empty env c in
- (id,Some j.uj_val, refresh_universes j.uj_type)
+let interp_evars evdref env ?(impls=([],[])) k 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 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))
+
+let interp_fields_evars isevars env l =
+ List.fold_left
+ (fun (env, uimpls, params, impls) ((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 d = (i,b',t') in
+ (push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
+ (env, [], [], ([], [])) l
+
+let binder_of_decl = function
+ | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
+ | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))
+
+let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields id t ps fs =
let env0 = Global.env () in
- let (env1,newps), _ = interp_context Evd.empty env0 ps 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 env2,newfs =
- List.fold_left
- (fun (env,newfs) d ->
- let decl = interp_decl Evd.empty env d in
- (push_rel decl env, decl::newfs))
- (env_ar,[]) fs
+ let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let env2,impls,newfs,data =
+ interp_fields_evars evars env_ar (binders_of_decls fs)
in
- newps, newfs
+ 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
+ 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
let degenerate_decl (na,b,t) =
let id = match na with
@@ -70,24 +87,25 @@ type record_error =
let warning_or_error coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
- let s,have = if List.length projs > 1 then "s","have" else "","has" in
+ let s,have = if List.length projs > 1 then "s","were" else "","was" in
(str(string_of_id fi) ++
- str" cannot be defined because the projection" ++ str s ++ spc () ++
- prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++ str "n't.")
+ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
+ prlist_with_sep pr_coma pr_id projs ++ spc () ++ str have ++
+ strbrk " not defined.")
| BadTypedProj (fi,ctx,te) ->
match te with
| ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
(pr_id fi ++
- str" cannot be defined because it is informative and " ++
+ strbrk" cannot be defined because it is informative and " ++
Printer.pr_inductive (Global.env()) indsp ++
- str " is not.")
+ strbrk " is not.")
| ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
(pr_id fi ++
- str" cannot be defined because it is large and " ++
+ strbrk" cannot be defined because it is large and " ++
Printer.pr_inductive (Global.env()) indsp ++
- str " is not.")
+ strbrk " is not.")
| _ ->
- (pr_id fi ++ str " cannot be defined because it is not typable")
+ (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
if coe then errorlabstrm "structure" st;
Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
@@ -131,7 +149,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
substl_rel_context (subst@[mkInd indsp]) fields
(* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let paramdecls = mib.mind_params_ctxt in
@@ -142,8 +160,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
let lifted_fields = lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
- List.fold_left2
- (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+ list_fold_left3
+ (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
let (sp_projs,subst) =
match fi with
| Anonymous ->
@@ -180,6 +198,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
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;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
@@ -191,28 +211,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
warning_or_error coe indsp why;
(None::sp_projs,NoProjection fi::subst) in
(nfi-1,(optci=None)::kinds,sp_projs,subst))
- (List.length fields,[],[],[]) coers (List.rev fields)
+ (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
-(* [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 coers,fs = List.split cfs in
- let extract_name acc = function
- Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
- | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
- | _ -> acc in
- 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 params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+let declare_structure 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
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let mie_ind =
- { mind_entry_typename = idstruc;
- mind_entry_arity = mkSort s;
+ { mind_entry_typename = id;
+ mind_entry_arity = arity;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] } in
let declare_as_coind =
@@ -223,10 +233,27 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
mind_entry_record = true;
mind_entry_finite = not declare_as_coind;
mind_entry_inds = [mie_ind] } in
- let kn = declare_mutual_with_eliminations true mie [] 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 coers fields in
- let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
- if is_coe then Class.try_add_new_coercion build Global;
- Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
- kn
+ 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
+
+(* [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 coers,fs = List.split cfs in
+ let extract_name acc = function
+ Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+ | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+ | _ -> acc in
+ 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
+
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 9642b351..48181437 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: record.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
(*i*)
open Names
@@ -14,6 +14,7 @@ open Term
open Sign
open Vernacexpr
open Topconstr
+open Impargs
(*i*)
(* [declare_projections ref name coers params fields] declare projections of
@@ -21,7 +22,18 @@ open Topconstr
as coercions accordingly to [coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+ inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+ bool list -> manual_explicitation list list -> rel_context ->
+ bool list * constant option list
+
+val declare_structure : identifier -> identifier ->
+ manual_explicitation list -> rel_context -> (* params *)
+ Term.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
val definition_structure :
lident with_coercion * local_binder list *
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 42f2883a..8a9ef501 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 10916 2008-05-10 15:38:36Z herbelin $ *)
+(* $Id: toplevel.ml 11317 2008-08-07 15:52:38Z barras $ *)
open Pp
open Util
@@ -140,13 +140,15 @@ let print_highlight_location ib loc =
(* Functions to report located errors in a file. *)
let print_location_in_file s inlibrary fname loc =
- let errstrm = (str"Error while reading " ++ str s ++ str":") in
- if loc = dummy_loc then
- (errstrm ++ str", unknown location." ++ fnl ())
+ let errstrm = str"Error while reading " ++ str s in
+ if loc = dummy_loc then
+ hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl ()
else
+ let errstrm =
+ if s = fname then mt() else errstrm ++ str":" ++ fnl() in
if inlibrary then
- (errstrm ++ fnl () ++ str"Module " ++ str ("\""^fname^"\"") ++
- str" characters " ++ Cerrors.print_loc loc ++ fnl ())
+ hov 0 (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ spc() ++
+ str"characters " ++ Cerrors.print_loc loc) ++ fnl ()
else
let (bp,ep) = unloc loc in
let ic = open_in fname in
@@ -160,10 +162,15 @@ let print_location_in_file s inlibrary fname loc =
try
let (line, bol) = line_of_pos 1 0 0 in
close_in ic;
- (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
- str", line " ++ int line ++
- str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ str":" ++ fnl ())
- with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ()))
+ hov 0
+ (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
+ hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
+ str"characters " ++
+ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
+ fnl ()
+ with e ->
+ (close_in ic;
+ hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
let print_command_location ib dloc =
match dloc with
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 782fdc80..b0b0f826 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: usage.ml 8932 2006-06-09 09:29:03Z notin $ *)
+(* $Id: usage.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
@@ -20,10 +20,14 @@ let print_usage_channel co command =
output_string co command;
output_string co "Coq options are:\n";
output_string co
-" -I dir add directory dir in the include path
+" -I dir -as coqdir map physical dir to logical coqdir
+ -I dir map directory dir to the empty logical path
-include dir (idem)
- -R dir coqdir recursively map physical dir to logical coqdir
+ -R dir -as coqdir recursively map physical dir to logical coqdir
+ -R dir coqdir (idem)
-top coqdir set the toplevel name to be coqdir instead of Top
+ -notop r set the toplevel name to be the empty logical path
+ -exclude-dir f exclude subdirectories named f for option -R
-inputstate f read state from file f.coq
-is f (idem)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 402f3b34..3f474239 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 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: vernacentries.ml 11313 2008-08-07 11:15:03Z barras $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -95,7 +95,7 @@ let show_script () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msgnl_with !Pp_control.deep_ft (print_treescript true evc pf)
+ msgnl_with !Pp_control.deep_ft (print_treescript evc pf)
let show_thesis () =
msgnl (anomaly "TODO" )
@@ -175,17 +175,17 @@ let show_match id =
^ " => \n" ^ acc)
"end" patterns in
msg (str ("match # with\n" ^ cases))
- with Not_found -> error "Unknown inductive type"
+ with Not_found -> error "Unknown inductive type."
(* "Print" commands *)
let print_path_entry (s,l) =
- (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l))
+ (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
let print_loadpath () =
let l = Library.get_full_load_paths () in
- msgnl (Pp.t (str "Physical path: " ++
- tab () ++ str "Logical Path:" ++ fnl () ++
+ msgnl (Pp.t (str "Logical Path: " ++
+ tab () ++ str "Physical path:" ++ fnl () ++
prlist_with_sep pr_fnl print_path_entry l))
let print_modules () =
@@ -232,7 +232,7 @@ let dump_universes s =
let locate_file f =
try
- let _,file = System.where_in_path (Library.get_load_paths ()) f in
+ let _,file = System.where_in_path 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 () ++
@@ -240,24 +240,26 @@ let locate_file f =
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->
- msgnl(pr_dirpath fulldir ++ str " has been loaded from file" ++ fnl () ++
- str file)
+ msgnl (hov 0
+ (pr_dirpath fulldir ++ strbrk " has been loaded from file " ++
+ str file))
| Library.LibInPath, fulldir, file ->
- msgnl(pr_dirpath fulldir ++ str " is bound to file " ++ str file)
+ msgnl (hov 0
+ (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
let msg_notfound_library loc qid = function
| Library.LibUnmappedDir ->
let dir = fst (repr_qualid qid) in
user_err_loc (loc,"locate_library",
- str "Cannot find a physical path bound to logical path " ++
- pr_dirpath dir ++ fnl ())
+ strbrk "Cannot find a physical path bound to logical path " ++
+ pr_dirpath dir ++ str".")
| Library.LibNotFound ->
msgnl (hov 0
- (str"Unable to locate library" ++ spc () ++ pr_qualid qid))
+ (strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
| e -> assert false
let print_located_library r =
let (loc,qid) = qualid_of_reference r in
- try msg_found_library (Library.locate_qualified_library qid)
+ try msg_found_library (Library.locate_qualified_library false qid)
with e -> msg_notfound_library loc qid e
let print_located_module r =
@@ -329,7 +331,7 @@ let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
errorlabstrm "Vernacentries.VernacDefinition"
- (str "Proof editing mode not supported in module types")
+ (str "Proof editing mode not supported in module types.")
else
let hook _ _ = () in
start_proof_and_print (local,DefinitionBody Definition)
@@ -351,10 +353,10 @@ let vernac_start_proof kind l lettop hook =
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
- (str "Let declarations can only be used in proof editing mode");
+ (str "Let declarations can only be used in proof editing mode.");
if Lib.is_modtype () then
errorlabstrm "Vernacentries.StartProof"
- (str "Proof editing mode not supported in module types");
+ (str "Proof editing mode not supported in module types.");
start_proof_and_print (Global, Proof kind) l hook
let vernac_end_proof = function
@@ -377,7 +379,7 @@ let vernac_exact_proof c =
save_named true end
else
errorlabstrm "Vernacentries.ExactProof"
- (str "Command 'Proof ...' can only be used at the beginning of the proof")
+ (strbrk "Command 'Proof ...' can only be used at the beginning of the proof.")
let vernac_assumption kind l nl=
let global = fst kind = Global in
@@ -421,7 +423,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
(* We check the state of the system (in section, in module type)
and what module information is supplied *)
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections";
+ error "Modules and Module Types are not allowed inside sections.";
let binders_ast = List.map
(fun (export,idl,ty) ->
if export <> None then
@@ -441,7 +443,7 @@ 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)
and what module information is supplied *)
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections";
+ error "Modules and Module Types are not allowed inside sections.";
match mexpr_ast_o with
| None ->
check_no_pending_proofs ();
@@ -488,7 +490,7 @@ let vernac_end_module export (loc,id) =
let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
if Lib.sections_are_opened () then
- error "Modules and Module Types are not allowed inside sections";
+ error "Modules and Module Types are not allowed inside sections.";
match mty_ast_o with
| None ->
@@ -552,7 +554,7 @@ let vernac_record struc binders sort nameopt cfs =
let s = match kind_of_term s with
| Sort s -> s
| _ -> user_err_loc
- (constr_loc sort,"definition_structure", str "Sort expected") in
+ (constr_loc sort,"definition_structure", str "Sort expected.") in
if !dump then (
dump_definition (snd struc) false "rec";
List.iter (fun (_, x) ->
@@ -615,7 +617,6 @@ let vernac_instance glob sup inst props pri =
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
- if !dump then List.iter (fun x -> dump_constraint x true "var") l;
Classes.context l
let vernac_declare_instance id =
@@ -626,7 +627,7 @@ let vernac_declare_instance id =
(* Solving *)
let vernac_solve n tcom b =
if not (refining ()) then
- error "Unknown command of the non proof-editing mode";
+ error "Unknown command of the non proof-editing mode.";
Decl_mode.check_not_proof_mode "Unknown proof instruction";
begin
if b then
@@ -653,7 +654,7 @@ let vernac_solve_existential = instantiate_nth_evar_com
let vernac_set_end_tac tac =
if not (refining ()) then
- error "Unknown command of the non proof-editing mode";
+ error "Unknown command of the non proof-editing mode.";
if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
@@ -771,7 +772,7 @@ let vernac_reserve idl c =
let make_silent_if_not_pcoq b =
if !pcoq <> None then
- error "Turning on/off silent flag is not supported in Centaur mode"
+ error "Turning on/off silent flag is not supported in Pcoq mode."
else make_silent b
let _ =
@@ -793,6 +794,14 @@ let _ =
let _ =
declare_bool_option
{ optsync = true;
+ optname = "manual implicit arguments";
+ optkey = (TertiaryTable ("Manual","Implicit","Arguments"));
+ optread = Impargs.is_manual_implicit_args;
+ optwrite = Impargs.make_manual_implicit_args }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
optname = "strict implicit arguments";
optkey = (SecondaryTable ("Strict","Implicit"));
optread = Impargs.is_strict_implicit_args;
@@ -825,7 +834,7 @@ let _ =
let _ =
declare_bool_option
{ optsync = true;
- optname = "implicit arguments defensive printing";
+ optname = "implicit status of reversible patterns";
optkey = (TertiaryTable ("Reversible","Pattern","Implicit"));
optread = Impargs.is_reversible_pattern_implicit_args;
optwrite = Impargs.make_reversible_pattern_implicit_args }
@@ -1096,7 +1105,7 @@ let global_module r =
try Nametab.full_name_module qid
with Not_found ->
user_err_loc (loc, "global_module",
- str "Module/section " ++ pr_qualid qid ++ str " not found")
+ str "Module/section " ++ pr_qualid qid ++ str " not found.")
let interp_search_restriction = function
| SearchOutside l -> (List.map global_module l, true)
@@ -1143,7 +1152,7 @@ let vernac_goal = function
start_proof_com (Global, Proof unnamed_kind) [None,c] (fun _ _ ->());
print_subgoals ()
end else
- error "repeated Goal not permitted in refining mode"
+ error "repeated Goal not permitted in refining mode."
let vernac_abort = function
| None ->
@@ -1161,7 +1170,7 @@ let vernac_abort_all () =
delete_all_proofs ();
message "Current goals aborted"
end else
- error "No proof-editing in progress"
+ error "No proof-editing in progress."
let vernac_restart () = restart_proof(); print_subgoals ()
@@ -1217,7 +1226,7 @@ let apply_subproof f occ =
f evc (Global.named_context()) pf
let explain_proof occ =
- msg (apply_subproof (fun evd _ -> print_treescript true evd) occ)
+ msg (apply_subproof (fun evd _ -> print_treescript evd) occ)
let explain_tree occ =
msg (apply_subproof print_proof occ)
@@ -1256,7 +1265,7 @@ let vernac_check_guard () =
pfterm;
(str "The condition holds up to here")
with UserError(_,s) ->
- (str ("Condition violated : ") ++s)
+ (str ("Condition violated: ") ++s)
in
msgnl message
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 744c3a6f..663e2e3c 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: vernacexpr.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
open Util
open Names
@@ -239,7 +239,7 @@ type vernac_expr =
(lident * lident list * constr_expr) list * (* props *)
int option (* Priority *)
- | VernacContext of typeclass_context
+ | VernacContext of local_binder list
| VernacDeclareInstance of
lident (* instance name *)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index f43c0c5e..41669c47 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernacinterp.ml 10348 2007-12-06 17:36:14Z aspiwack $ *)
+(* $Id: vernacinterp.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
open Pp
open Util
@@ -31,7 +31,7 @@ let vinterp_add s f =
Hashtbl.add vernac_tab s f
with Failure _ ->
errorlabstrm "vinterp_add"
- (str"Cannot add the vernac command " ++ str s ++ str" twice")
+ (str"Cannot add the vernac command " ++ str s ++ str" twice.")
let overwriting_vinterp_add s f =
begin
@@ -46,7 +46,7 @@ let vinterp_map s =
Hashtbl.find vernac_tab s
with Not_found ->
errorlabstrm "Vernac Interpreter"
- (str"Cannot find vernac command " ++ str s)
+ (str"Cannot find vernac command " ++ str s ++ str".")
let vinterp_init () = Hashtbl.clear vernac_tab
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 58703c8e..62aaa303 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: whelp.ml4 10904 2008-05-08 16:31:26Z herbelin $ *)
+(* $Id: whelp.ml4 11309 2008-08-06 10:30:35Z herbelin $ *)
open Flags
open Pp
@@ -80,7 +80,9 @@ let uri_of_dirpath dir =
let error_whelp_unknown_reference ref =
let qid = Nametab.shortest_qualid_of_global Idset.empty ref in
- error ("Definitions of the current session not supported in Whelp: " ^ string_of_qualid qid)
+ errorlabstrm ""
+ (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++
+ strbrk ", are not supported in Whelp.")
let uri_of_repr_kn ref (mp,dir,l) =
match mp with
@@ -104,7 +106,7 @@ let uri_of_ind_pointer l =
let uri_of_global ref =
match ref with
- | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id))
+ | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".")
| ConstRef cst ->
uri_of_repr_kn ref (repr_con cst); url_string ".con"
| IndRef (kn,i) ->
@@ -165,7 +167,7 @@ let rec uri_of_constr c =
| RCast (_,c, CastConv (_,t)) ->
uri_of_constr c; url_string ":"; uri_of_constr t
| RRec _ | RIf _ | RLetTuple _ | RCases _ ->
- error "Whelp does not support pattern-matching and (co-)fixpoint"
+ error "Whelp does not support pattern-matching and (co-)fixpoint."
| RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
anomaly "Written w/o parenthesis"
| RPatVar _ | RDynamic _ ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:32:05 +0000