summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch)
treee1542c8adb83ff297284eefc23a2703461713d9b /toplevel
parent514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff)
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml13
-rw-r--r--toplevel/cerrors.mli2
-rw-r--r--toplevel/class.ml181
-rw-r--r--toplevel/class.mli19
-rw-r--r--toplevel/command.ml255
-rw-r--r--toplevel/command.mli13
-rw-r--r--toplevel/coqinit.ml20
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqtop.ml45
-rw-r--r--toplevel/coqtop.mli2
-rw-r--r--toplevel/discharge.ml364
-rw-r--r--toplevel/discharge.mli15
-rw-r--r--toplevel/fhimsg.ml13
-rw-r--r--toplevel/fhimsg.mli2
-rw-r--r--toplevel/himsg.ml294
-rw-r--r--toplevel/himsg.mli8
-rw-r--r--toplevel/line_oriented_parser.ml2
-rw-r--r--toplevel/line_oriented_parser.mli2
-rw-r--r--toplevel/metasyntax.ml1100
-rw-r--r--toplevel/metasyntax.mli55
-rw-r--r--toplevel/minicoq.ml2
-rw-r--r--toplevel/mltop.ml48
-rw-r--r--toplevel/mltop.mli2
-rw-r--r--toplevel/protectedtoplevel.ml2
-rw-r--r--toplevel/protectedtoplevel.mli2
-rw-r--r--toplevel/record.ml73
-rw-r--r--toplevel/record.mli4
-rwxr-xr-xtoplevel/recordobj.ml77
-rw-r--r--toplevel/searchisos.mli2
-rw-r--r--toplevel/toplevel.ml39
-rw-r--r--toplevel/toplevel.mli2
-rw-r--r--toplevel/usage.ml2
-rw-r--r--toplevel/usage.mli2
-rw-r--r--toplevel/vernac.ml86
-rw-r--r--toplevel/vernac.mli2
-rw-r--r--toplevel/vernacentries.ml586
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacexpr.ml59
-rw-r--r--toplevel/vernacinterp.ml5
-rw-r--r--toplevel/vernacinterp.mli2
-rw-r--r--toplevel/whelp.ml4209
-rw-r--r--[-rwxr-xr-x]toplevel/whelp.mli (renamed from toplevel/recordobj.mli)18
42 files changed, 1388 insertions, 2205 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 21098a57..ab9c4c63 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,14 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cerrors.ml,v 1.12.2.2 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: cerrors.ml 8003 2006-02-07 22:11:50Z herbelin $ *)
open Pp
open Util
-open Ast
open Indtypes
open Type_errors
open Pretype_errors
+open Indrec
open Lexer
let print_loc loc =
@@ -47,8 +47,6 @@ let rec explain_exn_default = function
hov 0 (str "Out of memory")
| Stack_overflow ->
hov 0 (str "Stack overflow")
- | Ast.No_match s ->
- hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ())
| Anomaly (s,pps) ->
hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ())
| Match_failure(filename,pos1,pos2) ->
@@ -76,9 +74,13 @@ let rec explain_exn_default = function
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
| InductiveError e ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
+ | RecursionSchemeError e ->
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
| Cases.PatternMatchingError (env,e) ->
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
+ | Tacred.ReductionTacticError e ->
+ hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
| Logic.RefinerError e ->
hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
@@ -90,8 +92,7 @@ let rec explain_exn_default = function
hov 0 (str "Error:" ++ spc () ++
str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
| Refiner.FailError (i,s) ->
- let s = if s="" then "" else " \""^s^"\"" in
- hov 0 (str "Error: Tactic failure" ++ str s ++
+ hov 0 (str "Error: Tactic failure" ++ s ++
if i=0 then mt () else str " (level " ++ int i ++ str").")
| Stdpp.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 09d79cec..1236ecf5 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cerrors.mli,v 1.2.6.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: cerrors.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f5493929..5f385934 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: class.ml,v 1.44.2.3 2004/11/26 18:06:54 herbelin Exp $ *)
+(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
open Util
open Pp
@@ -92,42 +92,16 @@ let explain_coercion_error g = function
(* Verifications pour l'ajout d'une classe *)
-let rec arity_sort (ctx,a) = match kind_of_term a with
- | Sort (Prop _ | Type _) -> List.length ctx
- | _ -> raise Not_found
-
let check_reference_arity ref =
- let t = Global.type_of_global ref in
- try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
- with Not_found -> raise (CoercionError (NotAClass ref))
+ if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+ raise (CoercionError (NotAClass ref))
let check_arity = function
- | CL_FUN | CL_SORT -> 0
+ | CL_FUN | CL_SORT -> ()
| CL_CONST sp -> check_reference_arity (ConstRef sp)
| CL_SECVAR sp -> check_reference_arity (VarRef sp)
| CL_IND sp -> check_reference_arity (IndRef sp)
-(* try_add_class : cl_typ -> strength option -> bool -> unit *)
-
-let strength_of_cl = function
- | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
- | CL_SECVAR sp -> variable_strength sp
- | _ -> Global
-
-let try_add_class cl streopt fail_if_exists =
- if not (class_exists cl) then
- let p = check_arity cl in
- let stre' = strength_of_cl cl in
- let stre = match streopt with
- | Some stre -> strength_min (stre,stre')
- | None -> stre'
- in
- declare_class (cl,stre,p)
- else
- if fail_if_exists then errorlabstrm "try_add_new_class"
- (pr_class cl ++ str " is already a class")
-
-
(* Coercions *)
(* check that the computed target is the provided one *)
@@ -148,18 +122,18 @@ let uniform_cond nargs lt =
let id_of_cl = function
| CL_FUN -> id_of_string "FUNCLASS"
| CL_SORT -> id_of_string "SORTCLASS"
- | CL_CONST kn -> id_of_label (label kn)
+ | CL_CONST kn -> id_of_label (con_label kn)
| CL_IND ind ->
let (_,mip) = Global.lookup_inductive ind in
mip.mind_typename
| CL_SECVAR id -> id
-let class_of_ref = function
+let class_of_global = function
| ConstRef sp -> CL_CONST sp
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
- errorlabstrm "class_of_ref"
+ errorlabstrm "class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str " cannot be used as class")
@@ -204,14 +178,19 @@ let get_target t ind =
let prods_of t =
let rec aux acc d = match kind_of_term d with
| Prod (_,c1,c2) -> aux (c1::acc) c2
- | Cast (c,_) -> aux acc c
+ | Cast (c,_,_) -> aux acc c
| _ -> (d,acc)
in
aux [] t
+let strength_of_cl = function
+ | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
+ | CL_SECVAR sp -> variable_strength sp
+ | _ -> Global
+
let get_strength stre ref cls clt =
- let stres = (snd (class_info cls)).cl_strength in
- let stret = (snd (class_info clt)).cl_strength in
+ let stres = strength_of_cl cls in
+ let stret = strength_of_cl clt in
let stref = strength_of_global ref in
(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
let streunif = stre_unif_cond (s_vardep,f_vardep) in
@@ -265,10 +244,11 @@ let build_id_coercion idf_opt source =
in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
- { const_entry_body = mkCast (val_f, typ_f);
+ { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
const_entry_type = Some typ_f;
- const_entry_opaque = false } in
- let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions()} in
+ let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
ConstRef kn
let check_source = function
@@ -288,11 +268,9 @@ lorque source est None alors target est None aussi.
let add_new_coercion_core coef stre source target isid =
check_source source;
- let env = Global.env () in
- let v = constr_of_reference coef in
- let vj = Retyping.get_judgment_of env Evd.empty v in
+ let t = Global.type_of_global coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
- let tg,lp = prods_of (vj.uj_type) in
+ let tg,lp = prods_of t in
let llp = List.length lp in
if llp = 0 then raise (CoercionError NotAFunction);
let (cls,lvs,ind) =
@@ -311,10 +289,10 @@ let add_new_coercion_core coef stre source target isid =
raise (CoercionError NoTarget)
in
check_target clt target;
- try_add_class cls None false;
- try_add_class clt None false;
+ check_arity cls;
+ check_arity clt;
let stre' = get_strength stre coef cls clt in
- declare_coercion coef vj stre' isid cls clt (List.length lvs)
+ declare_coercion coef stre' isid cls clt (List.length lvs)
let try_add_new_coercion_core ref b c d e =
try add_new_coercion_core ref b c d e
@@ -345,114 +323,5 @@ let add_coercion_hook stre ref =
^ " is now a coercion")
let add_subclass_hook stre ref =
- let cl = class_of_ref ref in
+ let cl = class_of_global ref in
try_add_new_coercion_subclass cl stre
-
-(* try_add_new_class : global_reference -> strength -> unit *)
-
-let class_of_global = function
- | VarRef sp -> CL_SECVAR sp
- | ConstRef sp -> CL_CONST sp
- | IndRef sp -> CL_IND sp
- | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref))
-
-let try_add_new_class ref stre =
- try try_add_class (class_of_global ref) (Some stre) true
- with CoercionError e ->
- errorlabstrm "try_add_new_class" (explain_coercion_error ref e)
-
-(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *)
-
-type coercion_entry =
- global_reference * strength * bool * cl_typ * cl_typ * int
-
-let add_new_coercion (ref,stre,isid,cls,clt,n) =
- (* Un peu lourd, tout cela pour trouver l'instance *)
- let env = Global.env () in
- let v = constr_of_reference ref in
- let vj = Retyping.get_judgment_of env Evd.empty v in
- declare_coercion ref vj stre isid cls clt n
-
-let count_extra_abstractions hyps ids_to_discard =
- let _,n =
- List.fold_left
- (fun (hyps,n as sofar) id ->
- match hyps with
- | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
- | _ -> sofar)
- (hyps,0) ids_to_discard
- in n
-
-let defined_in_sec kn olddir =
- let _,dir,_ = repr_kn kn in
- dir = olddir
-
-(* This moves the global path one step below *)
-let process_global olddir = function
- | VarRef _ ->
- anomaly "process_global only processes global surviving the section"
- | ConstRef kn as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- ConstRef newkn
- else x
- | IndRef (kn,i) as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- IndRef (newkn,i)
- else x
- | ConstructRef ((kn,i),j) as x ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- ConstructRef ((newkn,i),j)
- else x
-
-let process_class olddir ids_to_discard x =
- let (cl,{cl_strength=stre; cl_param=p}) = x in
-(* let env = Global.env () in*)
- match cl with
- | CL_SECVAR _ -> x
- | CL_CONST kn ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- let hyps = (Global.lookup_constant kn).const_hyps in
- let n = count_extra_abstractions hyps ids_to_discard in
- (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
- else
- x
- | CL_IND (kn,i) ->
- if defined_in_sec kn olddir then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- let hyps = (Global.lookup_mind kn).mind_hyps in
- let n = count_extra_abstractions hyps ids_to_discard in
- (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n})
- else
- x
- | _ -> anomaly "process_class"
-
-let process_cl sec_sp cl =
- match cl with
- | CL_SECVAR id -> cl
- | CL_CONST kn ->
- if defined_in_sec kn sec_sp then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- CL_CONST newkn
- else
- cl
- | CL_IND (kn,i) ->
- if defined_in_sec kn sec_sp then
- let newkn = Lib.make_kn (id_of_label (label kn)) in
- CL_IND (newkn,i)
- else
- cl
- | _ -> cl
-
-let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) =
- let hyps = context_of_global_reference coe in
- let nargs = count_extra_abstractions hyps ids_to_discard in
- (process_global olddir coe,
- coercion_strength coeinfo,
- coercion_identity coeinfo,
- process_cl olddir cls,
- process_cl olddir clt,
- nargs + coercion_params coeinfo)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index b0350985..7717d754 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: class.mli,v 1.17.6.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: class.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
(*i*)
open Names
@@ -50,19 +50,4 @@ val add_coercion_hook : Tacexpr.declaration_hook
val add_subclass_hook : Tacexpr.declaration_hook
-(* [try_add_new_class ref] declares [ref] as a new class; usually,
- this is done implicitely by [try_add_new_coercion]'s functions *)
-val try_add_new_class : global_reference -> strength -> unit
-
-(*s This is used for the discharge *)
-type coercion_entry
-
-val add_new_coercion : coercion_entry -> unit
-
-val process_class :
- dir_path -> identifier list ->
- (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
-val process_coercion :
- dir_path -> identifier list -> coercion -> coercion_entry
-
-val class_of_ref : global_reference -> cl_typ
+val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 10d6a620..7ff1b1b5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: command.ml,v 1.116.2.4 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *)
open Pp
open Util
@@ -18,7 +18,7 @@ open Entries
open Inductive
open Environ
open Reduction
-open Tacred
+open Redexpr
open Declare
open Nametab
open Names
@@ -37,31 +37,45 @@ open Indtypes
open Vernacexpr
open Decl_kinds
open Pretyping
-open Symbols
+open Notation
let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
-let rec abstract_rawconstr c = function
+let rec abstract_constr_expr c = function
| [] -> c
- | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
| LocalRawAssum (idl,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
- (abstract_rawconstr c bl)
+ (abstract_constr_expr c bl)
-let rec generalize_rawconstr c = function
+let rec generalize_constr_expr c = function
| [] -> c
- | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_rawconstr c bl)
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
| LocalRawAssum (idl,t)::bl ->
List.fold_right (fun x b -> mkProdC([x],t,b)) idl
- (generalize_rawconstr c bl)
+ (generalize_constr_expr c bl)
+
+let rec length_of_raw_binders = function
+ | [] -> 0
+ | LocalRawDef _::bl -> 1 + length_of_raw_binders bl
+ | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl
+
+let rec under_binders env f n c =
+ if n = 0 then f env Evd.empty c else
+ match kind_of_term c with
+ | Lambda (x,t,c) ->
+ mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
+ | LetIn (x,b,t,c) ->
+ mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
+ | _ -> assert false
let rec destSubCast c = match kind_of_term c with
| Lambda (x,t,c) ->
let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
| LetIn (x,b,t,c) ->
let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
- | Cast (b,u) -> (b,u)
+ | Cast (b,_, u) -> (b,u)
| _ -> assert false
let rec adjust_conclusion a cs = function
@@ -84,63 +98,51 @@ let rec adjust_conclusion a cs = function
let definition_message id =
if_verbose message ((string_of_id id) ^ " is defined")
-let constant_entry_of_com (bl,com,comtypopt,opacity) =
+let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
let sigma = Evd.empty in
let env = Global.env() in
match comtypopt with
None ->
- let b = abstract_rawconstr com bl in
- let j = judgment_of_rawconstr sigma env b in
+ let b = abstract_constr_expr com bl in
+ let j = interp_constr_judgment sigma env b in
{ const_entry_body = j.uj_val;
- const_entry_type = Some (Evarutil.refresh_universes j.uj_type);
- const_entry_opaque = opacity }
+ const_entry_type = Some (refresh_universes j.uj_type);
+ const_entry_opaque = opacity;
+ const_entry_boxed = boxed }
| Some comtyp ->
(* We use a cast to avoid troubles with evars in comtyp *)
(* that can only be resolved knowing com *)
- let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in
+ let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
let (body,typ) = destSubCast (interp_constr sigma env b) in
{ const_entry_body = body;
const_entry_type = Some typ;
- const_entry_opaque = opacity }
-
-let rec length_of_raw_binders = function
- | [] -> 0
- | LocalRawDef _::bl -> 1 + length_of_raw_binders bl
- | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl
-
-let rec under_binders env f n c =
- if n = 0 then f env Evd.empty c else
- match kind_of_term c with
- | Lambda (x,t,c) ->
- mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
- | LetIn (x,b,t,c) ->
- mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
- | _ -> assert false
+ const_entry_opaque = opacity;
+ const_entry_boxed = boxed }
let red_constant_entry bl ce = function
| None -> ce
| Some red ->
let body = ce.const_entry_body in
{ ce with const_entry_body =
- under_binders (Global.env()) (reduction_of_redexp red)
- (length_of_raw_binders bl)
- body }
+ under_binders (Global.env()) (fst (reduction_of_red_expr red))
+ (length_of_raw_binders bl)
+ body }
let declare_global_definition ident ce local =
- let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
- if local = Local then
+ let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
+ if local = Local && Options.is_verbose() then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
ConstRef kn
-let declare_definition ident (local,_) bl red_option c typopt hook =
- let ce = constant_entry_of_com (bl,c,typopt,false) in
+let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
+ let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
let ce' = red_constant_entry bl ce red_option in
let r = match local with
| Local when Lib.sections_are_opened () ->
let c =
SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
- let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in
+ let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
definition_message ident;
if Pfedit.refining () then
msgerrnl (str"Warning: Local definition " ++ pr_id ident ++
@@ -152,7 +154,6 @@ let declare_definition ident (local,_) bl red_option c typopt hook =
let syntax_definition ident c local onlyparse =
let c = snd (interp_aconstr [] [] c) in
- let onlyparse = !Options.v7_only or onlyparse in
Syntax_def.declare_syntactic_definition local ident onlyparse c
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -163,7 +164,7 @@ let assumption_message id =
let declare_one_assumption is_coe (local,kind) c (_,ident) =
let r = match local with
| Local when Lib.sections_are_opened () ->
- let r =
+ let _ =
declare_variable ident
(Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
assumption_message ident;
@@ -172,7 +173,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
str" is not visible from current goals");
VarRef ident
| (Global|Local) ->
- let (_,kn) =
+ let kn =
declare_constant ident (ParameterEntry c, IsAssumption kind) in
assumption_message ident;
if local=Local & Options.is_verbose () then
@@ -182,9 +183,13 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
if is_coe then Class.try_add_new_coercion r local
let declare_assumption idl is_coe k bl c =
- let c = generalize_rawconstr c bl in
- let c = interp_type Evd.empty (Global.env()) c in
- List.iter (declare_one_assumption is_coe k c) idl
+ if not (Pfedit.refining ()) then
+ let c = generalize_constr_expr c bl in
+ let c = interp_type Evd.empty (Global.env()) c in
+ List.iter (declare_one_assumption is_coe k c) idl
+ else
+ errorlabstrm "Command.Assumption"
+ (str "Cannot declare an assumption while in proof editing mode.")
(* 3a| Elimination schemes for mutual inductive definitions *)
@@ -203,16 +208,17 @@ let declare_one_elimination ind =
(DefinitionEntry
{ const_entry_body = c;
const_entry_type = t;
- const_entry_opaque = false },
- Decl_kinds.IsDefinition) in
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions() },
+ Decl_kinds.IsDefinition Definition) in
definition_message id;
kn
in
let env = Global.env () in
let sigma = Evd.empty in
let elim_scheme = Indrec.build_indrec env sigma ind in
- let npars = mip.mind_nparams in
- let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in
+ let npars = mib.mind_nparams_rec in
+ let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in
let kelim = mip.mind_kelim in
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
@@ -220,10 +226,10 @@ let declare_one_elimination ind =
if List.mem InType kelim then
let elim = make_elim (new_sort_in_family InType) in
let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in
- let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in
+ let c = mkConst cte and t = constant_type (Global.env()) cte in
List.iter (fun (sort,suff) ->
let (t',c') =
- Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort)
+ Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort)
npars c t in
let _ = declare (mindstr^suff) c' (Some t') in ())
non_type_eliminations
@@ -270,27 +276,9 @@ let interp_mutual lparams lnamearconstrs finite =
[] lnamearconstrs in
if not (list_distinct allnames) then
error "Two inductive objects have the same name";
- let nparams = local_binders_length lparams
- and sigma = Evd.empty
- and env0 = Global.env() in
- let env_params, params =
- List.fold_left
- (fun (env, params) d -> match d with
- | LocalRawAssum ([_,na],(CHole _ as t)) ->
- let t = interp_binder sigma env na t in
- let d = (na,None,t) in
- (push_rel d env, d::params)
- | LocalRawAssum (nal,t) ->
- let t = interp_type sigma env t in
- let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
- let ctx = List.rev ctx in
- (push_rel_context ctx env, ctx@params)
- | LocalRawDef ((_,na),c) ->
- let c = judgment_of_rawconstr sigma env c in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env0,[]) lparams
- in
+ let sigma = Evd.empty and env0 = Global.env() in
+ let env_params, params = interp_context sigma env0 lparams in
+
(* Builds the params of the inductive entry *)
let params' =
List.map (fun (na,b,t) ->
@@ -304,8 +292,6 @@ let interp_mutual lparams lnamearconstrs finite =
let paramassums =
List.fold_right (fun d l -> match d with
(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
- let indnames =
- List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
let nparamassums = List.length paramassums in
let (ind_env,ind_impls,arityl) =
List.fold_left
@@ -316,7 +302,7 @@ let interp_mutual lparams lnamearconstrs finite =
let argsc = compute_arguments_scope fullarity in
let ind_impls' =
if Impargs.is_implicit_args() then
- let impl = Impargs.compute_implicits false env_params fullarity in
+ let impl = Impargs.compute_implicits env_params fullarity in
let paramimpl,_ = list_chop nparamassums impl in
let l = List.fold_right
(fun imp l -> if Impargs.is_status_implicit imp then
@@ -337,8 +323,9 @@ let interp_mutual lparams lnamearconstrs finite =
let fs = States.freeze() in
(* Declare the notations for the inductive types pushed in local context*)
try
- List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
- Metasyntax.add_notation_interpretation df ind_impls c None) notations;
+ List.iter (fun (df,c,scope) ->
+ silently (Metasyntax.add_notation_interpretation df ind_impls c) scope)
+ notations;
let ind_env_params = push_rel_context params ind_env in
let mispecvec =
@@ -358,21 +345,20 @@ let interp_mutual lparams lnamearconstrs finite =
(* Interpret the constructor types *)
let constrs =
List.map
- (interp_type_with_implicits sigma ind_env_params
- (paramassums,ind_impls))
+ (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls))
bodies
in
(* Build the inductive entry *)
- { mind_entry_params = params';
- mind_entry_typename = name;
+ { mind_entry_typename = name;
mind_entry_arity = ar;
mind_entry_consnames = constrnames;
mind_entry_lc = constrs })
(List.rev arityl) lnamearconstrs
in
States.unfreeze fs;
- notations, { mind_entry_record = false;
+ notations, { mind_entry_params = params';
+ mind_entry_record = false;
mind_entry_finite = finite;
mind_entry_inds = mispecvec }
with e -> States.unfreeze fs; raise e
@@ -388,6 +374,7 @@ let declare_mutual_with_eliminations isrecord mie =
(* Very syntactical equality *)
let eq_la d1 d2 = match d1,d2 with
| LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') ->
+ (List.length nal = List.length nal') &&
List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal'
& (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
| LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') ->
@@ -422,7 +409,7 @@ let extract_coe_la_lc = function
let build_mutual lind finite =
let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
let notations,mie = interp_mutual lparams lnamearconstructs finite in
- let kn = declare_mutual_with_eliminations false mie in
+ let _ = declare_mutual_with_eliminations false mie in
(* Declare the notations now bound to the inductive types *)
List.iter (fun (df,c,scope) ->
Metasyntax.add_notation_interpretation df [] c scope) notations;
@@ -465,7 +452,8 @@ let collect_non_rec env =
in
searchrec []
-let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
+let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
+ boxed =
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and sigma = Evd.empty
and env0 = Global.env()
@@ -474,11 +462,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
let (rec_sign,rec_impls,arityl) =
List.fold_left
(fun (env,impls,arl) ((recname,_,bl,arityc,_),_) ->
- let arityc = generalize_rawconstr arityc bl in
+ let arityc = generalize_constr_expr arityc bl in
let arity = interp_type sigma env0 arityc in
let impl =
if Impargs.is_implicit_args()
- then Impargs.compute_implicits false env0 arity
+ then Impargs.compute_implicits env0 arity
else [] in
let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
(Environ.push_named (recname,None,arity) env, impls', arity::arl))
@@ -494,13 +482,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
let fs = States.freeze() in
let def =
try
- List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
- Metasyntax.add_notation_interpretation df rec_impls c None) notations;
+ List.iter (fun (df,c,scope) ->
+ silently
+ (Metasyntax.add_notation_interpretation df rec_impls c) scope)
+ notations;
List.map2
(fun ((_,_,bl,_,def),_) arity ->
- let def = abstract_rawconstr def bl in
- interp_casted_constr_with_implicits
- sigma rec_sign rec_impls def arity)
+ let def = abstract_constr_expr def bl in
+ interp_casted_constr sigma rec_sign ~impls:([],rec_impls)
+ def arity)
lnameargsardef arityl
with e ->
States.unfreeze fs; raise e in
@@ -514,11 +504,12 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
let rec declare i fi =
let ce =
- { const_entry_body = mkFix ((nvrec,i),recdecls);
+ { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
const_entry_type = Some arrec.(i);
- const_entry_opaque = false } in
- let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in
- (ConstRef kn)
+ const_entry_opaque = false;
+ const_entry_boxed = boxed} in
+ let kn = declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+ in (ConstRef kn)
in
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
@@ -530,8 +521,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
(fun subst (f,def,t) ->
let ce = { const_entry_body = replace_vars subst def;
const_entry_type = Some t;
- const_entry_opaque = false } in
- let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in
+ const_entry_opaque = false;
+ const_entry_boxed = boxed } in
+ let _ =
+ declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+ in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -540,7 +534,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
List.iter (fun (df,c,scope) ->
Metasyntax.add_notation_interpretation df [] c scope) notations
-let build_corecursive lnameardef =
+let build_corecursive lnameardef boxed =
let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef
and sigma = Evd.empty
and env0 = Global.env() in
@@ -549,11 +543,10 @@ let build_corecursive lnameardef =
try
List.fold_left
(fun (env,arl) (recname,bl,arityc,_) ->
- let arityc = generalize_rawconstr arityc bl in
- let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
- let arity = arj.utj_val in
+ let arityc = generalize_constr_expr arityc bl in
+ let arity = interp_type Evd.empty env0 arityc in
let _ = declare_variable recname
- (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in
+ (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in
(Environ.push_named (recname,None,arity) env, (arity::arl)))
(env0,[]) lnameardef
with e ->
@@ -562,10 +555,10 @@ let build_corecursive lnameardef =
let recdef =
try
List.map (fun (_,bl,arityc,def) ->
- let arityc = generalize_rawconstr arityc bl in
- let def = abstract_rawconstr def bl in
+ let arityc = generalize_constr_expr arityc bl in
+ let def = abstract_constr_expr def bl in
let arity = interp_constr sigma rec_sign arityc in
- interp_casted_constr sigma rec_sign def arity)
+ interp_casted_constr sigma rec_sign def arity)
lnameardef
with e ->
States.unfreeze fs; raise e
@@ -580,10 +573,11 @@ let build_corecursive lnameardef =
let ce =
{ const_entry_body = mkCoFix (i, recdecls);
const_entry_type = Some (arrec.(i));
- const_entry_opaque = false }
+ const_entry_opaque = false;
+ const_entry_boxed = boxed }
in
- let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
- (ConstRef kn)
+ let kn = declare_constant fi (DefinitionEntry ce,IsDefinition CoFixpoint)
+ in (ConstRef kn)
in
let lrefrec = Array.mapi declare namerec in
if_verbose ppnl (corecursive_message lrefrec);
@@ -593,8 +587,10 @@ let build_corecursive lnameardef =
(fun subst (f,def,t) ->
let ce = { const_entry_body = replace_vars subst def;
const_entry_type = Some t;
- const_entry_opaque = false } in
- let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in
+ const_entry_opaque = false;
+ const_entry_boxed = boxed } in
+ let _ =
+ declare_constant f (DefinitionEntry ce,IsDefinition Definition) in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -616,11 +612,12 @@ let build_scheme lnamedepindsort =
let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in
let rec declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 Evd.empty decl in
- let decltype = Evarutil.refresh_universes decltype in
+ let decltype = refresh_universes decltype in
let ce = { const_entry_body = decl;
const_entry_type = Some decltype;
- const_entry_opaque = false } in
- let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions() } in
+ let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in
ConstRef kn :: lrecref
in
let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -643,29 +640,30 @@ let start_proof_com sopt kind (bl,t) hook =
(Pfedit.get_all_proof_names ())
in
let env = Global.env () in
- let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
+ let c = interp_type Evd.empty env (generalize_constr_expr t bl) in
let _ = Typeops.infer_type env c in
start_proof id kind c hook
-let save id const kind hook =
+let save id const (locality,kind) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
- let l,r = match kind with
- | IsLocal when Lib.sections_are_opened () ->
+ let l,r = match locality with
+ | Local when Lib.sections_are_opened () ->
+ let k = logical_kind_of_goal_kind kind in
let c = SectionLocalDef (pft, tpo, opacity) in
- let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in
+ let _ = declare_variable id (Lib.cwd(), c, k) in
(Local, VarRef id)
- | IsLocal ->
- let k = IsDefinition in
- let _,kn = declare_constant id (DefinitionEntry const, k) in
+ | Local ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn)
- | IsGlobal k ->
- let k = theorem_kind_of_goal_kind k in
- let _,kn = declare_constant id (DefinitionEntry const, k) in
+ | Global ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn) in
- hook l r;
Pfedit.delete_current_proof ();
+ hook l r;
definition_message id
let save_named opacity =
@@ -691,7 +689,7 @@ let save_anonymous_with_strength kind opacity save_ident =
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save save_ident const (IsGlobal (Proof kind)) hook
+ save save_ident const (Global, Proof kind) hook
let admit () =
let (id,k,typ,hook) = Pfedit.current_proof_statement () in
@@ -699,9 +697,10 @@ let admit () =
if k <> IsGlobal (Proof Conjecture) then
error "Only statements declared as conjecture can be admitted";
*)
- let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in
- hook Global (ConstRef kn);
+ let kn =
+ declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
Pfedit.delete_current_proof ();
+ hook Global (ConstRef kn);
assumption_message id
let get_current_context () =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7997288c..c93f69be 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,v 1.38.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: command.mli 7682 2005-12-21 15:06:11Z herbelin $ i*)
(*i*)
open Util
@@ -22,6 +22,7 @@ open Vernacexpr
open Rawterm
open Topconstr
open Decl_kinds
+open Redexpr
(*i*)
(*s Declaration functions. The following functions take ASTs,
@@ -30,7 +31,7 @@ open Decl_kinds
defined object *)
val declare_definition : identifier -> definition_kind ->
- local_binder list -> Tacred.red_expr option -> constr_expr ->
+ local_binder list -> red_expr option -> constr_expr ->
constr_expr option -> declaration_hook -> unit
val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
@@ -43,13 +44,13 @@ val build_mutual : inductive_expr list -> bool -> unit
val declare_mutual_with_eliminations :
bool -> Entries.mutual_inductive_entry -> mutual_inductive
-val build_recursive : (fixpoint_expr * decl_notation) list -> unit
+val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
-val build_corecursive : cofixpoint_expr list -> unit
+val build_corecursive : cofixpoint_expr list -> bool -> unit
val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
-val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
+val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
val start_proof : identifier -> goal_kind -> constr ->
declaration_hook -> unit
@@ -83,3 +84,5 @@ val admit : unit -> unit
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
+
+
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 4ba8f6c2..44b2e231 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqinit.ml,v 1.30.2.4 2006/01/11 23:18:06 barras Exp $ *)
+(* $Id: coqinit.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
open Pp
open System
@@ -73,23 +73,19 @@ let init_load_path () =
(* developper specific directories to open *)
let dev = if Coq_config.local then [ "dev" ] else [] in
let coqlib =
- if !Options.boot then Coq_config.coqtop
- (* variable COQLIB overrides the default library *)
- else getenv_else "COQLIB" Coq_config.coqlib in
- let coqlib = canonical_path_name coqlib in
+ (* variable COQLIB overrides the default library *)
+ getenv_else "COQLIB"
+ (if Coq_config.local || !Options.boot then Coq_config.coqtop
+ else Coq_config.coqlib) in
(* first user-contrib *)
let user_contrib = coqlib/"user-contrib" in
if Sys.file_exists user_contrib then
- Mltop.add_path user_contrib Nameops.default_root_prefix;
+ Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
(* then standard library *)
- let vdirs =
- if !Options.v7 then [ "theories7"; "contrib7" ]
- else [ "theories"; "contrib" ] in
- let dirs =
- (if !Options.v7 then "states7" else "states") :: dev @ vdirs in
+ let vdirs = [ "theories"; "contrib" ] in
+ let dirs = "states" :: dev @ vdirs in
List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
- let camlp4 = canonical_path_name camlp4 in
add_ml_include camlp4;
(* then current directory *)
Mltop.add_path "." Nameops.default_root_prefix;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index e029d8ac..d7856170 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqinit.mli,v 1.7.16.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: coqinit.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* Initialization. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index af787460..c3f79e0a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqtop.ml,v 1.72.2.5 2005/11/23 14:46:09 barras Exp $ *)
+(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
open Pp
open Util
@@ -29,9 +29,8 @@ let get_version_date () =
with _ -> Coq_config.date
let print_header () =
- Printf.printf "Welcome to Coq %s%s (%s)\n"
+ Printf.printf "Welcome to Coq %s (%s)\n"
Coq_config.version
- (if !Options.v7 then " (V7 syntax)" else "")
(get_version_date ());
flush stdout
@@ -50,8 +49,10 @@ let engage () =
let set_batch_mode () = batch_mode := true
-let toplevel_name = ref (make_dirpath [id_of_string "Top"])
-let set_toplevel_name dir = toplevel_name := dir
+let toplevel_default_name = make_dirpath [id_of_string "Top"]
+let toplevel_name = ref (Some toplevel_default_name)
+let set_toplevel_name dir = toplevel_name := Some dir
+let unset_toplevel_name () = toplevel_name := None
let remove_top_ml () = Mltop.remove ()
@@ -91,12 +92,13 @@ let load_vernacular () =
let load_vernacular_obj = ref ([] : string list)
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
let load_vernac_obj () =
- List.iter Library.read_library_from_file (List.rev !load_vernacular_obj)
+ List.iter (fun f -> Library.require_library_from_file None f None)
+ (List.rev !load_vernacular_obj)
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- List.iter (fun s -> Library.require_library_from_file None None s false)
+ List.iter (fun s -> Library.require_library_from_file None s (Some false))
(List.rev !require_list)
let compile_list = ref ([] : (bool * string) list)
@@ -128,7 +130,6 @@ let re_exec is_ide =
let s = !re_exec_version in
let is_native = (Mltop.get()) = Mltop.Native in
let prog = Sys.argv.(0) in
- let coq = Filename.basename prog in
if (is_native && s = "byte") || ((not is_native) && s = "opt")
then begin
let s = if s = "" then if is_native then "opt" else "byte" else s in
@@ -142,6 +143,17 @@ let re_exec is_ide =
Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
end
+(*s options for the virtual machine *)
+
+let boxed_val = ref false
+let boxed_def = ref false
+let use_vm = ref false
+
+let set_vm_opt () =
+ Vm.set_transp_values (not !boxed_val);
+ Options.set_boxed_definitions !boxed_def;
+ Vconv.set_use_vm !use_vm
+
(*s Parsing of the command line.
We no longer use [Arg.parse], in order to use share [Usage.print_usage]
between coqtop and coqc. *)
@@ -162,7 +174,7 @@ let parse_args is_ide =
| [] -> ()
| "-impredicative-set" :: rem ->
- set_engagement Environ.ImpredicativeSet; parse rem
+ set_engagement Declarations.ImpredicativeSet; parse rem
| ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
| ("-I"|"-include") :: [] -> usage ()
@@ -173,6 +185,7 @@ let parse_args is_ide =
| "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
| "-top" :: [] -> usage ()
+ | "-notop" :: rem -> unset_toplevel_name (); parse rem
| "-q" :: rem -> no_load_rc (); parse rem
| "-opt" :: rem -> set_opt(); parse rem
@@ -228,6 +241,7 @@ let parse_args is_ide =
| "-debug" :: rem -> set_debug (); parse rem
+ | "-vm" :: rem -> use_vm := true; parse rem
| "-emacs" :: rem -> Options.print_emacs := true; parse rem
| "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
@@ -253,12 +267,10 @@ let parse_args is_ide =
| "-xml" :: rem -> Options.xml_export := true; parse rem
(* Scanned in Options! *)
- | "-v7" :: rem -> (* Options.v7 := true; *) parse rem
- | "-v8" :: rem -> (* Options.v7 := false; *) parse rem
+ | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
+ | "-v8" :: rem -> parse rem
- (* Translator options *)
- | "-strict-implicit" :: rem ->
- Options.translate_strict_impargs := false; parse rem
+ | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem
| s :: rem ->
if is_ide then begin
@@ -294,9 +306,10 @@ let init is_ide =
if_verbose print_header ();
init_load_path ();
inputstate ();
+ set_vm_opt ();
engage ();
- if not !batch_mode && Global.env_is_empty() then
- Declaremods.start_library !toplevel_name;
+ if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
+ option_iter Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ef8b4b37..b5a1106c 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqtop.mli,v 1.5.4.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: coqtop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* The Coq main module. The following function [start] will parse the
command line, print the banner, initialize the load path, load the input
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 281ff1b6..6c543079 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,325 +6,83 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *)
-open Pp
-open Util
open Names
-open Nameops
+open Util
open Sign
open Term
-open Declarations
open Entries
-open Inductive
-open Instantiate
-open Reduction
+open Declarations
open Cooking
-open Typeops
-open Libnames
-open Libobject
-open Lib
-open Nametab
-open Declare
-open Impargs
-open Classops
-open Class
-open Recordops
-open Library
-open Indtypes
-open Nametab
-open Decl_kinds
-let recalc_sp dir sp =
- let (_,spid) = repr_path sp in Libnames.make_path dir spid
+(********************************)
+(* Discharging mutual inductive *)
-let recalc_kn dir kn =
- let (mp,_,l) = Names.repr_kn kn in
- Names.make_kn mp dir l
+let detype_param = function
+ | (Name id,None,p) -> id, Entries.LocalAssum p
+ | (Name id,Some p,_) -> id, Entries.LocalDef p
+ | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable"
-let rec find_var id = function
- | [] -> false
- | (x,b,_)::l -> if x = id then b=None else find_var id l
+(* Replace
-let build_abstract_list sec_sp hyps ids_to_discard =
- let l1,l2 =
- List.split
- (List.fold_left
- (fun vars id ->
- if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars
- else vars)
- [] ids_to_discard) in
- Array.of_list l1, l2
+ Var(y1)..Var(yq):C1..Cq |- Ij:Bj
+ Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-(* Discharge of inductives is done here (while discharge of constants
- is done by the kernel for efficiency). *)
+ by
-let abstract_inductive sec_sp ids_to_abs hyps inds =
- let abstract_one_assum id t inds =
- let ntyp = List.length inds in
- let new_refs =
- list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
- let inds' =
- List.map
- (function (np,tname,arity,cnames,lc) ->
- let arity' = mkNamedProd id t arity in
- let lc' =
- List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
- in
- (np,tname,arity',cnames,lc'))
- inds
- in
- inds' in
- let abstract_one_def id c inds =
- List.map
- (function (np,tname,arity,cnames,lc) ->
- let arity' = replace_vars [id, c] arity in
- let lc' = List.map (replace_vars [id, c]) lc in
- (np,tname,arity',cnames,lc'))
- inds in
- let abstract_once ((hyps,inds,vars) as sofar) id =
- match hyps with
- | (hyp,None,t as d)::rest when id = hyp ->
- let inds' = abstract_one_assum hyp t inds in
- (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars)
- | (hyp,Some b,t as d)::rest when id = hyp ->
- let inds' = abstract_one_def hyp b inds in
- (rest, inds', vars)
- | _ -> sofar in
- let (_,inds',vars) =
- List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
- let inds'' =
- List.map
- (fun (nparams,a,arity,c,lc) ->
- let nparams' = nparams + (List.length vars) in
- let params, short_arity = decompose_prod_n_assum nparams' arity in
- let shortlc =
- List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
- let params' =
- List.map
- (function
- | (Name id,None,p) -> id, Entries.LocalAssum p
- | (Name id,Some p,_) -> id, Entries.LocalDef p
- | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
- params in
- { mind_entry_params = params';
- mind_entry_typename = a;
- mind_entry_arity = short_arity;
- mind_entry_consnames = c;
- mind_entry_lc = shortlc })
- inds' in
- let l1,l2 = List.split vars in
- (inds'', Array.of_list l1, l2)
+ |- Ij: (y1..yq:C1..Cq)Bj
+ I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
+*)
-let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
- assert (Array.length mib.mind_packets > 0);
- let record = mib.mind_record in
- let finite = mib.mind_finite in
+let abstract_inductive hyps nparams inds =
+ let ntyp = List.length inds in
+ let nhyp = named_context_length hyps in
+ let args = instance_from_named_context (List.rev hyps) in
+ let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
+ let inds' =
+ List.map
+ (function (tname,arity,cnames,lc) ->
+ let lc' = List.map (substl subs) lc in
+ let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
+ let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
+ (tname,arity',cnames,lc''))
+ inds in
+ let nparams' = nparams + Array.length args in
+(* To be sure to be the same as before, should probably be moved to process_inductive *)
+ let params' = let (_,arity,_,_) = List.hd inds' in
+ let (params,_) = decompose_prod_n_assum nparams' arity in
+ List.map detype_param params
+ in
+ let ind'' =
+ List.map
+ (fun (a,arity,c,lc) ->
+ let _, short_arity = decompose_prod_n_assum nparams' arity in
+ let shortlc =
+ List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+ { mind_entry_typename = a;
+ mind_entry_arity = short_arity;
+ mind_entry_consnames = c;
+ mind_entry_lc = shortlc })
+ inds'
+ in (params',ind'')
+
+
+let process_inductive sechyps modlist mib =
+ let nparams = mib.mind_nparams in
let inds =
array_map_to_list
(fun mip ->
- let nparams = mip.mind_nparams in
- let arity = expmod_type modlist mip.mind_user_arity in
- let lc = Array.map (expmod_type modlist) mip.mind_user_lc in
- (nparams,
- mip.mind_typename,
+ let arity = expmod_constr modlist mip.mind_user_arity in
+ let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
+ (mip.mind_typename,
arity,
Array.to_list mip.mind_consnames,
Array.to_list lc))
- mib.mind_packets
- in
- let hyps = mib.mind_hyps in
- let hyps' =
- Sign.fold_named_context
- (fun (x,b,t) sgn ->
- Sign.add_named_decl
- (x, option_app (expmod_constr modlist) b,expmod_constr modlist t)
- sgn)
- mib.mind_hyps ~init:empty_named_context in
- let (inds',abs_vars,discharged_hyps ) =
- abstract_inductive sec_sp ids_to_discard hyps' inds in
- let lmodif_one_mind i =
- let nbc = Array.length mib.mind_packets.(i).mind_consnames in
- (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)),
- list_tabulate
- (function j ->
- let j' = j + 1 in
- (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars)))
- nbc)
- in
- let indmodifs,cstrmodifs =
- List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in
- ({ mind_entry_record = record;
- mind_entry_finite = finite;
- mind_entry_inds = inds' },
- indmodifs,
- List.flatten cstrmodifs,
- discharged_hyps)
-
-(* Discharge messages. *)
-
-let constant_message id =
- Options.if_verbose ppnl (pr_id id ++ str " is discharged.")
-
-let inductive_message inds =
- Options.if_verbose
- ppnl
- (hov 0
- (match inds with
- | [] -> assert false
- | [ind] ->
- (pr_id ind.mind_entry_typename ++ str " is discharged.")
- | l ->
- (prlist_with_sep pr_coma
- (fun ind -> pr_id ind.mind_entry_typename) l ++
- spc () ++ str "are discharged.")))
-
-(* Discharge operations for the various objects of the environment. *)
-
-type opacity = bool
-
-type discharge_operation =
- | Variable of identifier * section_variable_entry * local_kind *
- implicits_flags * Dischargedhypsmap.discharged_hyps
- | Constant of identifier * recipe * global_kind * constant *
- implicits_flags * Dischargedhypsmap.discharged_hyps
- | Inductive of mutual_inductive_entry * implicits_flags *
- Dischargedhypsmap.discharged_hyps
- | Class of cl_typ * cl_info_typ
- | Struc of inductive * (unit -> struc_typ)
- | Objdef of constant
- | Coercion of coercion_entry
- | Require of library_reference
- | Constraints of Univ.constraints
-
-(* Main function to traverse the library segment and compute the various
- discharge operations. *)
-
-let process_object oldenv olddir full_olddir newdir
-(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *)
- (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) =
- let tag = object_tag lobj in
- match tag with
- | "VARIABLE" ->
- let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in
- (* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
- (* always discharged *)
- (Constraints cst :: ops, id :: ids_to_discard, work_alist)
-
- | "CONSTANT" ->
- (* CONSTANT means never discharge (though visibility may vary) *)
- let kind = constant_kind sp in
- let kn = Nametab.locate_constant (qualid_of_sp sp) in
- let lab = label kn in
- let cb = Environ.lookup_constant kn oldenv in
- let imp = is_implicit_constant kn in
- let newkn = recalc_kn newdir kn in
- let abs_vars,discharged_hyps0 =
- build_abstract_list full_olddir cb.const_hyps ids_to_discard in
- (* let's add the new discharged hypothesis to those already discharged*)
- let discharged_hyps =
- discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
- let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ]
- in
- let r = { d_from = cb;
- d_modlist = work_alist;
- d_abstract = ids_to_discard } in
- let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in
- (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
-
- | "INDUCTIVE" ->
- let kn = Nametab.locate_mind (qualid_of_sp sp) in
- let mib = Environ.lookup_mind kn oldenv in
- let newkn = recalc_kn newdir kn in
- let imp = is_implicit_inductive_definition kn in
-(* let imp = is_implicit_args (* CHANGE *) in*)
- let (mie,indmods,cstrmods,discharged_hyps0) =
- process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in
- (* let's add the new discharged hypothesis to those already discharged*)
- let discharged_hyps =
- discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
- ((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard,
- (constl,indmods@indl,cstrmods@cstrl))
-
- | "CLASS" ->
- let ((cl,clinfo) as x) = outClass lobj in
- if clinfo.cl_strength = Local then
- (ops,ids_to_discard,work_alist)
- else
- let (y1,y2) = process_class olddir ids_to_discard x in
- ((Class (y1,y2))::ops, ids_to_discard, work_alist)
-
- | "COERCION" ->
- let (_,coeinfo,_,_ as x) = outCoercion lobj in
- if coercion_strength coeinfo = Local then
- (ops,ids_to_discard,work_alist)
- else
- let y = process_coercion olddir ids_to_discard x in
- ((Coercion y)::ops, ids_to_discard, work_alist)
-
- | "STRUCTURE" ->
- let ((kn,i),info) = outStruc lobj in
- let newkn = recalc_kn newdir kn in
- let strobj () =
- let mib = Environ.lookup_mind newkn (Global.env ()) in
- { s_CONST = info.s_CONST;
- s_PARAM = mib.mind_packets.(0).mind_nparams;
- s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
- ((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
-
- | "OBJDEF1" ->
- let kn = outObjDef1 lobj in
- let new_kn = recalc_kn newdir kn in
- ((Objdef new_kn)::ops, ids_to_discard, work_alist)
-
- | "REQUIRE" ->
- let c = out_require lobj in
- ((Require c)::ops, ids_to_discard, work_alist)
-
- | _ -> (ops,ids_to_discard,work_alist)
-
-let process_item oldenv olddir full_olddir newdir acc = function
- | (sp,Leaf lobj) ->
- process_object oldenv olddir full_olddir newdir acc (sp,lobj)
- | (_,_) -> acc
-
-let process_operation = function
- | Variable (id,expmod_a,stre,imp,discharged_hyps) ->
- (* Warning:parentheses needed to get a side-effect from with_implicits *)
- with_implicits imp (redeclare_variable id discharged_hyps)
- (Lib.cwd(),expmod_a,stre)
- | Constant (id,r,stre,kn,imp,discharged_hyps) ->
- with_implicits imp (redeclare_constant id discharged_hyps) (r,stre);
- constant_message id
- | Inductive (mie,imp,discharged_hyps) ->
- let _ = with_implicits imp (redeclare_inductive discharged_hyps) mie in
- inductive_message mie.mind_entry_inds
- | Class (y1,y2) ->
- Lib.add_anonymous_leaf (inClass (y1,y2))
- | Struc (newsp,strobj) ->
- Lib.add_anonymous_leaf (inStruc (newsp,strobj ()))
- | Objdef newsp ->
- begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
- | Coercion y -> add_new_coercion y
- | Require y -> reload_library y
- | Constraints y -> Global.add_constraints y
-
-let catch_not_found f x =
- try f x
- with Not_found ->
- error ("Something is missing; perhaps a reference to a"^
- " module required inside the section")
-
-let close_section _ s =
- let oldenv = Global.env() in
- let prefix,decls,fs = close_section false s in
- let full_olddir, (_,olddir) = prefix in
- let newdir = fst (split_dirpath olddir) in
- let (ops,ids,_) =
- List.fold_left
- (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls
- in
- let ids = last_section_hyps olddir in
- Summary.section_unfreeze_summaries fs;
- catch_not_found (List.iter process_operation) (List.rev ops);
- Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)
+ mib.mind_packets in
+ let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+ let (params',inds') = abstract_inductive sechyps' nparams inds in
+ { mind_entry_record = mib.mind_record;
+ mind_entry_finite = mib.mind_finite;
+ mind_entry_params = params';
+ mind_entry_inds = inds' }
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index c80b93ce..dcf88f31 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,13 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: discharge.mli,v 1.6.16.1 2004/07/16 19:31:48 herbelin Exp $ i*)
+(*i $Id: discharge.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
-open Names
+open Sign
+open Cooking
+open Declarations
+open Entries
-(* This module implements the discharge mechanism. It provides a function to
- close the last opened section. That function calls [Lib.close_section] and
- then re-introduce all the discharged versions of the objects that were
- defined in the section. *)
-
-val close_section : bool -> identifier -> unit
+val process_inductive :
+ named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index b5185cd3..4ef5d5fd 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: fhimsg.ml,v 1.19.2.1 2004/07/16 19:31:48 herbelin Exp $ *)
+(* $Id: fhimsg.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
open Pp
open Util
@@ -231,7 +231,7 @@ let explain_ill_formed_rec_body k ctx err names i vdefs =
| RecCallInCasePred c ->
(str "Not allowed recursive call in the type of cases in")
| NotGuardedForm c ->
- str "Sub-expression " ++ prterm_env ctx c ++ spc() ++
+ 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
@@ -278,14 +278,7 @@ let explain_ml_case k ctx mes c ct br brt =
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_cant_find_case_type loc k ctx c =
- let pe = P.pr_term k ctx c in
- Ast.user_err_loc
- (loc,"pretype",
- hov 3 (str "Cannot infer type of whole Case expression on" ++
- ws 1 ++ pe))
-*)
+
let explain_type_error k ctx = function
| UnboundRel n ->
explain_unbound_rel k ctx n
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 10175e2a..1ab786d1 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: fhimsg.mli,v 1.8.16.1 2004/07/16 19:31:48 herbelin Exp $ i*)
+(*i $Id: fhimsg.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index beb80d03..3fe51b5a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml,v 1.86.2.4 2004/12/03 18:45:53 herbelin Exp $ *)
+(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *)
open Pp
open Util
@@ -21,18 +21,20 @@ open Sign
open Environ
open Pretype_errors
open Type_errors
+open Indrec
open Reduction
open Cases
open Logic
open Printer
-open Ast
open Rawterm
+open Evd
-let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"")
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
-let prterm c = quote (prterm c)
-let prterm_env e c = quote (prterm_env e c)
-let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t)
+let pr_lconstr c = quote (pr_lconstr c)
+let pr_lconstr_env e c = quote (pr_lconstr_env e c)
+let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
+let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
let nth i =
let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
@@ -56,20 +58,20 @@ let explain_unbound_var ctx v =
let explain_not_type ctx j =
let pe = pr_ne_context_of (str"In environment") ctx in
- let pc,pt = prjudge_env ctx j in
+ let pc,pt = pr_ljudge_env ctx j in
pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
str"has type" ++ spc () ++ pt ++ spc () ++
str"which should be Set, Prop or Type."
let explain_bad_assumption ctx j =
let pe = pr_ne_context_of (str"In environment") ctx in
- let pc,pt = prjudge_env ctx j in
+ let pc,pt = pr_ljudge_env ctx j in
pe ++ str "cannot declare a variable or hypothesis over the term" ++
brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++
str "because this term is not a type."
let explain_reference_variables c =
- let pc = prterm c in
+ let pc = pr_lconstr c in
str "the constant" ++ spc () ++ pc ++ spc () ++
str "refers to variables which are not in the context"
@@ -82,12 +84,11 @@ let rec pr_disjunction pr = function
let explain_elim_arity ctx ind aritylst c pj okinds =
let ctx = make_all_name_different ctx in
let pi = pr_inductive ctx ind in
- let pc = prterm_env ctx c in
- let ppt = prterm_env ctx pj.uj_type in
+ let pc = pr_lconstr_env ctx c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
- let pki = prterm_env ctx ki in
- let pkp = prterm_env ctx kp in
+ let pki = pr_lconstr_env ctx ki in
+ let pkp = pr_lconstr_env ctx kp in
let explanation = match explanation with
| NonInformativeToInformative ->
"proofs can be eliminated only to build proofs"
@@ -106,29 +107,19 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
hov 0 (
str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
str "in the inductive type " ++ spc() ++ quote pi ++
- (if !Options.v7 then
- let pp = prterm_env ctx pj.uj_val in
- let ppar = pr_disjunction (prterm_env ctx) aritylst in
- let ppt = prterm_env ctx pj.uj_type in
- fnl () ++
- str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
- str "has arity" ++ brk(1,1) ++ ppt ++ fnl () ++
- str "It should be " ++ brk(1,1) ++ ppar
- else
- let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
+ (let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
(list_uniquize (List.map (fun ar ->
family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in
- let ppar = pr_disjunction (prterm_env ctx) sorts in
- let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in
+ let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in
+ let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in
str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++
spc () ++ str "while it should be " ++ ppar))
++ fnl () ++ msg
-
-
+
let explain_case_not_inductive ctx cj =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx cj.uj_val in
- let pct = prterm_env ctx cj.uj_type in
+ let pc = pr_lconstr_env ctx cj.uj_val in
+ let pct = pr_lconstr_env ctx cj.uj_type in
match kind_of_term cj.uj_type with
| Evar _ ->
str "Cannot infer a type for this expression"
@@ -139,26 +130,30 @@ let explain_case_not_inductive ctx cj =
let explain_number_branches ctx cj expn =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx cj.uj_val in
- let pct = prterm_env ctx cj.uj_type in
+ let pc = pr_lconstr_env ctx cj.uj_val in
+ let pct = pr_lconstr_env ctx cj.uj_type in
str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
str "of type" ++ brk(1,1) ++ pct ++ spc () ++
str "expects " ++ int expn ++ str " branches"
+let ordinal n =
+ let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+ string_of_int n ^ s
+
let explain_ill_formed_branch ctx c i actty expty =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx c in
- let pa = prterm_env ctx actty in
- let pe = prterm_env ctx expty in
+ let pc = pr_lconstr_env ctx c in
+ let pa = pr_lconstr_env ctx actty in
+ let pe = pr_lconstr_env ctx expty in
str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
- spc () ++ str "the branch " ++ int (i+1) ++
- str " has type" ++ brk(1,1) ++ pa ++ spc () ++
+ spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++
+ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe
let explain_generalization ctx (name,var) j =
let pe = pr_ne_context_of (str "In environment") ctx in
- let pv = prtype_env ctx var in
- let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
+ let pv = pr_ltype_env ctx var in
+ let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in
str"Illegal generalization: " ++ pe ++
str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++
@@ -167,17 +162,18 @@ let explain_generalization ctx (name,var) j =
let explain_actual_type ctx j pt =
let pe = pr_ne_context_of (str "In environment") ctx in
- let (pc,pct) = prjudge_env ctx j in
- let pt = prterm_env ctx pt in
+ let (pc,pct) = pr_ljudge_env ctx j in
+ let pt = pr_lconstr_env ctx pt in
pe ++
str "The term" ++ brk(1,1) ++ pc ++ spc () ++
str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
str "while it is expected to have type" ++ brk(1,1) ++ pt
let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
+ let ctx = make_all_name_different ctx in
let randl = Array.to_list randl in
(* let pe = pr_ne_context_of (str"in environment") ctx in*)
- let pr,prt = prjudge_env ctx rator in
+ let pr,prt = pr_ljudge_env ctx rator in
let term_string1,term_string2 =
if List.length randl > 1 then
str "terms", (str"The "++nth n++str" term")
@@ -185,7 +181,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
str "term", str "This term" in
let appl = prlist_with_sep pr_fnl
(fun c ->
- let pc,pct = prjudge_env ctx c in
+ let pc,pct = pr_ljudge_env ctx c in
hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
@@ -193,19 +189,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
str"of type" ++ brk(1,1) ++ prt ++ spc () ++
str"cannot be applied to the " ++ term_string1 ++ fnl () ++
str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++
- brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++
- str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
+ brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++
+ str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp
let explain_cant_apply_not_functional ctx rator randl =
+ let ctx = make_all_name_different ctx in
let randl = Array.to_list randl in
(* let pe = pr_ne_context_of (str"in environment") ctx in*)
- let pr = prterm_env ctx rator.uj_val in
- let prt = prterm_env ctx rator.uj_type in
+ let pr = pr_lconstr_env ctx rator.uj_val in
+ let prt = pr_lconstr_env 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 = prterm_env ctx c.uj_val in
- let pct = prterm_env ctx c.uj_type in
+ let pc = pr_lconstr_env ctx c.uj_val in
+ let pct = pr_lconstr_env ctx c.uj_type in
hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
str"Illegal application (Non-functional construction): " ++
@@ -216,14 +213,14 @@ let explain_cant_apply_not_functional ctx rator randl =
str" " ++ v 0 appl
let explain_unexpected_type ctx actual_type expected_type =
- let pract = prterm_env ctx actual_type in
- let prexp = prterm_env ctx expected_type in
+ let pract = pr_lconstr_env ctx actual_type in
+ let prexp = pr_lconstr_env ctx expected_type in
str"This type is" ++ spc () ++ pract ++ spc () ++
str "but is expected to be" ++
spc () ++ prexp
let explain_not_product ctx c =
- let pr = prterm_env ctx c in
+ let pr = pr_lconstr_env ctx c in
str"The type of this term is a product," ++ spc () ++
str"but it is casted with type" ++
brk(1,1) ++ pr
@@ -241,8 +238,9 @@ let explain_ill_formed_rec_body ctx err names i =
(* Fixpoint guard errors *)
| NotEnoughAbstractionInFixBody ->
str "Not enough abstractions in the definition"
- | RecursionNotOnInductiveType ->
- str "Recursive definition on a non inductive type"
+ | RecursionNotOnInductiveType c ->
+ str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++
+ str "which should be an inductive type"
| RecursionOnIllegalTerm(j,arg,le,lt) ->
let called =
match names.(j) with
@@ -262,7 +260,7 @@ let explain_ill_formed_rec_body ctx err names i =
prlist_with_sep pr_spc (pr_db ctx) lt in
str "Recursive call to " ++ called ++ spc() ++
str "has principal argument equal to" ++ spc() ++
- prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars
+ pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars
| NotEnoughArgumentsForFixCall j ->
let called =
@@ -273,31 +271,31 @@ let explain_ill_formed_rec_body ctx err names i =
(* CoFixpoint guard errors *)
| CodomainNotInductiveType c ->
- str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++
+ str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++
str "which should be a coinductive type"
| NestedRecursiveOccurrences ->
str "nested recursive occurrences"
| UnguardedRecursiveCall c ->
- str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c
+ str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c
| RecCallInTypeOfAbstraction c ->
str "recursive call forbidden in the domain of an abstraction:" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInNonRecArgOfConstructor c ->
str "recursive call on a non-recursive argument of constructor" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInTypeOfDef c ->
str "recursive call forbidden in the type of a recursive definition" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInCaseFun c ->
- str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c
+ str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c
| RecCallInCaseArg c ->
str "recursive call in the argument of cases in" ++ spc() ++
- prterm_env ctx c
+ pr_lconstr_env ctx c
| RecCallInCasePred c ->
str "recursive call in the type of cases in" ++ spc() ++
- prterm_env ctx c
+ pr_lconstr_env ctx c
| NotGuardedForm c ->
- str "sub-expression " ++ prterm_env ctx c ++ spc() ++
+ str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
str "not in guarded form" ++ spc()++
str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)"
in
@@ -307,8 +305,8 @@ let explain_ill_formed_rec_body ctx err names i =
let explain_ill_typed_rec_body ctx i names vdefj vargs =
let ctx = make_all_name_different ctx in
- let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
- let pv = prterm_env ctx vargs.(i) in
+ let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in
+ let pv = pr_lconstr_env 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 () ++
@@ -317,19 +315,19 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs =
(*
let explain_not_inductive ctx c =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx c in
+ let pc = pr_lconstr_env ctx c in
str"The term" ++ brk(1,1) ++ pc ++ spc () ++
str "is not an inductive definition"
*)
let explain_cant_find_case_type ctx c =
let ctx = make_all_name_different ctx in
- let pe = prterm_env ctx c in
+ let pe = pr_lconstr_env ctx c in
hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe)
let explain_occur_check ctx ev rhs =
let ctx = make_all_name_different ctx in
let id = Evd.string_of_existential ev in
- let pt = prterm_env ctx rhs in
+ let pt = pr_lconstr_env ctx rhs in
str"Occur check failed: tried to define " ++ str id ++
str" with term" ++ brk(1,1) ++ pt
@@ -342,14 +340,10 @@ let explain_hole_kind env = function
| BinderType Anonymous ->
str "a type for this anonymous binder"
| ImplicitArg (c,(n,ido)) ->
- if !Options.v7 then
- str "the " ++ pr_ord n ++
- str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
- else
- let id = out_some ido in
- str "an instance for the implicit parameter " ++
- pr_id id ++ spc () ++ str "of" ++
- spc () ++ Nametab.pr_global_env Idset.empty c
+ let id = out_some ido in
+ str "an instance for the implicit parameter " ++
+ pr_id id ++ spc () ++ str "of" ++
+ spc () ++ Nametab.pr_global_env Idset.empty c
| InternalHole ->
str "a term for an internal placeholder"
| TomatchTypeParameter (tyi,n) ->
@@ -361,7 +355,7 @@ let explain_not_clean ctx ev t k =
let ctx = make_all_name_different ctx in
let c = mkRel (Intset.choose (free_rels t)) in
let id = Evd.string_of_existential ev in
- let var = prterm_env ctx c in
+ let var = pr_lconstr_env ctx c in
str"Tried to define " ++ explain_hole_kind ctx k ++
str" (" ++ str id ++ str ")" ++ spc() ++
str"with a term using variable " ++ var ++ spc () ++
@@ -377,18 +371,36 @@ let explain_var_not_found ctx id =
spc () ++ str "in the current" ++ spc () ++ str "environment"
let explain_wrong_case_info ctx ind ci =
- let ctx = make_all_name_different ctx in
- let pi = prterm (mkInd ind) in
+ let pi = pr_lconstr (mkInd ind) in
if ci.ci_ind = ind then
str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++
spc () ++ str"has invalid information"
else
- let pc = prterm (mkInd ci.ci_ind) in
+ let pc = pr_lconstr (mkInd ci.ci_ind) in
str"A term of inductive type" ++ spc () ++ pi ++ spc () ++
str"was given to a pattern-matching expression on the inductive type" ++
spc () ++ pc
+let explain_cannot_unify m n =
+ let pm = pr_lconstr m in
+ let pn = pr_lconstr n in
+ str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
+ str"with" ++ brk(1,1) ++ pn
+
+let explain_refiner_cannot_generalize ty =
+ str "Cannot find a well-typed generalisation of the goal with type : " ++
+ pr_lconstr ty
+
+let explain_no_occurrence_found c =
+ str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal"
+
+let explain_cannot_unify_binding_type m n =
+ let pm = pr_lconstr m in
+ let pn = pr_lconstr n in
+ str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
+ str "which should be unifiable with" ++ brk(1,1) ++ pn
+
let explain_type_error ctx err =
let ctx = make_all_name_different ctx in
match err with
@@ -445,93 +457,74 @@ let explain_pretype_error ctx err =
explain_unexpected_type ctx actual expected
| NotProduct c ->
explain_not_product ctx c
+ | CannotUnify (m,n) -> explain_cannot_unify m n
+ | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+ | NoOccurrenceFound c -> explain_no_occurrence_found c
+ | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
(* Refiner errors *)
let explain_refiner_bad_type arg ty conclty =
str"refiner was given an argument" ++ brk(1,1) ++
- prterm arg ++ spc () ++
- str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++
- str"instead of" ++ brk(1,1) ++ prterm conclty
+ pr_lconstr arg ++ spc () ++
+ str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
+ str"instead of" ++ brk(1,1) ++ pr_lconstr conclty
let explain_refiner_occur_meta t =
- str"cannot refine with term" ++ brk(1,1) ++ prterm t ++
+ str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++
spc () ++ str"because there are metavariables, and it is" ++
spc () ++ str"neither an application nor a Case"
let explain_refiner_occur_meta_goal t =
- str"generated subgoal" ++ brk(1,1) ++ prterm t ++
+ str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++
spc () ++ str"has metavariables in it"
-let explain_refiner_cannot_applt t harg =
+let explain_refiner_cannot_apply t harg =
str"in refiner, a term of type " ++ brk(1,1) ++
- prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
- prterm harg
-
-let explain_cannot_unify m n =
- let pm = prterm m in
- let pn = prterm n in
- str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
- str"with" ++ brk(1,1) ++ pn
-
-let explain_cannot_unify_binding_type m n =
- let pm = prterm m in
- let pn = prterm n in
- str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
- str "which should be unifiable with" ++ brk(1,1) ++ pn
-
-let explain_refiner_cannot_generalize ty =
- str "Cannot find a well-typed generalisation of the goal with type : " ++
- prterm ty
+ pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
+ pr_lconstr harg
let explain_refiner_not_well_typed c =
- str"The term " ++ prterm 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"
let explain_does_not_occur_in c hyp =
- str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++
+ str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++
spc () ++ pr_id hyp
let explain_non_linear_proof c =
- str "cannot refine with term" ++ brk(1,1) ++ prterm c ++
+ str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
spc () ++ str"because a metavariable has several occurrences"
-let explain_no_occurrence_found c =
- str "Found no subterm matching " ++ prterm c ++ str " in the current goal"
-
let explain_refiner_error = function
| BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
| OccurMeta t -> explain_refiner_occur_meta t
| OccurMetaGoal t -> explain_refiner_occur_meta_goal t
- | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
- | CannotUnify (m,n) -> explain_cannot_unify m n
- | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
- | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+ | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
| NotWellTyped c -> explain_refiner_not_well_typed c
| IntroNeedsProduct -> explain_intro_needs_product ()
| DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
| NonLinearProof c -> explain_non_linear_proof c
- | NoOccurrenceFound c -> explain_no_occurrence_found c
(* Inductive errors *)
let error_non_strictly_positive env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
brk(1,1) ++ pc
let error_ill_formed_inductive env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "Not enough arguments applied to the " ++ pv ++
str " in" ++ brk(1,1) ++ pc
let error_ill_formed_constructor env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++
str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv
@@ -544,9 +537,9 @@ let str_of_nth n =
| _ -> "th")
let error_bad_ind_parameters env c n v1 v2 =
- let pc = prterm_env_at_top env c in
- let pv1 = prterm_env env v1 in
- let pv2 = prterm_env env v2 in
+ let pc = pr_lconstr_env_at_top env c in
+ let pv1 = pr_lconstr_env env v1 in
+ let pv2 = pr_lconstr_env env v2 in
str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++
str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc
@@ -583,10 +576,11 @@ let error_bad_induction dep indid kind =
str "is not allowed"
let error_not_mutual_in_scheme () =
- str "Induction schemes is concerned only with mutually inductive types"
+ str "Induction schemes are concerned only with distinct mutually inductive types"
+
+(* Inductive constructions errors *)
let explain_inductive_error = function
- (* These are errors related to inductive constructions *)
| NonPos (env,c,v) -> error_non_strictly_positive env c v
| NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v
| NotConstructor (env,c,v) -> error_ill_formed_constructor env c v
@@ -596,7 +590,10 @@ let explain_inductive_error = function
| SameNamesOverlap idl -> error_same_names_overlap idl
| NotAnArity id -> error_not_an_arity id
| BadEntry -> error_bad_entry ()
- (* These are errors related to recursors *)
+
+(* Recursion schemes errors *)
+
+let explain_recursion_scheme_error = function
| NotAllowedCaseAnalysis (dep,k,i) ->
error_not_allowed_case_analysis dep k i
| BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
@@ -606,7 +603,7 @@ let explain_inductive_error = function
let explain_bad_pattern ctx cstr ty =
let ctx = make_all_name_different ctx in
- let pt = prterm_env ctx ty in
+ let pt = pr_lconstr_env ctx ty in
let pc = pr_constructor ctx cstr in
str "Found the constructor " ++ pc ++ brk(1,1) ++
str "while matching a term of type " ++ pt ++ brk(1,1) ++
@@ -620,31 +617,38 @@ let explain_bad_constructor ctx cstr ind =
str "while a constructor of " ++ pi ++ brk(1,1) ++
str "is expected"
-let explain_wrong_numarg_of_constructor ctx cstr n =
- let pc = pr_constructor ctx cstr in
- str "The constructor " ++ pc ++ str " expects " ++
- (if n = 0 then str "no argument." else if n = 1 then str "1 argument."
- else (int n ++ str " arguments."))
+let decline_string n s =
+ if n = 0 then "no "^s
+ else if n = 1 then "1 "^s
+ else (string_of_int n^" "^s^"s")
+
+let explain_wrong_numarg_constructor ctx cstr n =
+ str "The constructor " ++ pr_constructor ctx cstr ++
+ str " expects " ++ str (decline_string n "argument")
+
+let explain_wrong_numarg_inductive ctx ind n =
+ str "The inductive type " ++ pr_inductive ctx ind ++
+ str " expects " ++ str (decline_string n "argument")
let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity=
let ctx = make_all_name_different ctx in
- let pp = prterm_env ctx pred in
+ let pp = pr_lconstr_env ctx pred in
str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
str "should be of arity" ++ spc () ++
- prterm_env ctx nondep_arity ++ spc () ++
+ pr_lconstr_env ctx nondep_arity ++ spc () ++
str "(for non dependent case) or" ++
- spc () ++ prterm_env ctx dep_arity ++ spc () ++ str "(for dependent case)."
+ spc () ++ pr_lconstr_env ctx dep_arity ++ spc () ++ str "(for dependent case)."
let explain_needs_inversion ctx x t =
let ctx = make_all_name_different ctx in
- let px = prterm_env ctx x in
- let pt = prterm_env ctx t in
+ let px = pr_lconstr_env ctx x in
+ let pt = pr_lconstr_env ctx t in
str "Sorry, I need inversion to compile pattern matching of term " ++
px ++ str " of type: " ++ pt
let explain_unused_clause env pats =
- let s = if List.length pats > 1 then "s" else "" in
(* Without localisation
+ let s = if List.length pats > 1 then "s" else "" in
(str ("Unused clause with pattern"^s) ++ spc () ++
hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
*)
@@ -659,7 +663,7 @@ let explain_cannot_infer_predicate ctx typs =
let ctx = make_all_name_different ctx in
let pr_branch (cstr,typ) =
let cstr,_ = decompose_app cstr in
- str "For " ++ prterm_env ctx cstr ++ str " : " ++ prterm_env ctx typ
+ str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ
in
str "Unable to unify the types found in the branches:" ++
spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
@@ -670,7 +674,9 @@ let explain_pattern_matching_error env = function
| BadConstructor (c,ind) ->
explain_bad_constructor env c ind
| WrongNumargConstructor (c,n) ->
- explain_wrong_numarg_of_constructor env c n
+ explain_wrong_numarg_constructor env c n
+ | WrongNumargInductive (c,n) ->
+ explain_wrong_numarg_inductive env c n
| WrongPredicateArity (pred,n,dep) ->
explain_wrong_predicate_arity env pred n dep
| NeedsInversion (x,t) ->
@@ -681,3 +687,9 @@ let explain_pattern_matching_error env = function
explain_non_exhaustive env tms
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env typs
+
+let explain_reduction_tactic_error = function
+ | Tacred.InvalidAbstraction (env,c,(env',e)) ->
+ str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++
+ spc() ++ str "is not well typed." ++ fnl () ++
+ explain_type_error env' e
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3e7ba575..92fcafb7 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,v 1.13.14.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: himsg.mli 8003 2006-02-07 22:11:50Z herbelin $ i*)
(*i*)
open Pp
@@ -15,6 +15,7 @@ open Indtypes
open Environ
open Type_errors
open Pretype_errors
+open Indrec
open Cases
open Logic
(*i*)
@@ -27,7 +28,12 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds
val explain_inductive_error : inductive_error -> std_ppcmds
+val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
+
val explain_refiner_error : refiner_error -> std_ppcmds
val explain_pattern_matching_error :
env -> pattern_matching_error -> std_ppcmds
+
+val explain_reduction_tactic_error :
+ Tacred.reduction_tactic_error -> std_ppcmds
diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml
index 81221196..77f5198a 100644
--- a/toplevel/line_oriented_parser.ml
+++ b/toplevel/line_oriented_parser.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: line_oriented_parser.ml,v 1.2.16.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: line_oriented_parser.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
let line_oriented_channel_to_option stop_string input_channel =
let count = ref 0 in
diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli
index 13af0e06..f37472c0 100644
--- a/toplevel/line_oriented_parser.mli
+++ b/toplevel/line_oriented_parser.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: line_oriented_parser.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: line_oriented_parser.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
val line_oriented_channel_to_option: string -> in_channel -> int -> char option
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4c554209..92ce6e36 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,120 +6,27 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *)
+(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *)
open Pp
open Util
open Names
open Topconstr
-open Coqast
-open Ast
open Ppextend
open Extend
-open Esyntax
open Libobject
-open Library
open Summary
open Constrintern
open Vernacexpr
open Pcoq
open Rawterm
open Libnames
-
-let interp_global_rawconstr_with_vars vars c =
- interp_rawconstr_gen false Evd.empty (Global.env()) false (vars,[]) c
-
-(**********************************************************************)
-(* Parsing via ast (used in Zsyntax) *)
-
-(* This updates default parsers for Grammar actions and Syntax *)
-(* patterns by inserting globalization *)
-(* Done here to get parsing/g_*.ml4 non dependent from kernel *)
-let constr_to_ast a =
- Termast.ast_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a)
-
-(* This installs default quotations parsers to escape the ast parser *)
-(* "constr" is used by default in quotations found in the ast parser *)
-let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
-
-let _ = define_ast_quotation true "constr" constr_parser_with_glob
+open Lexer
+open Egrammar
+open Notation
(**********************************************************************)
-(* Globalisation for constr_expr *)
-
-let globalize_ref vars ref =
- match Constrintern.interp_reference (vars,[]) ref with
- | RRef (loc,VarRef a) -> Ident (loc,a)
- | RRef (loc,a) -> Qualid (loc,qualid_of_sp (Nametab.sp_of_global a))
- | RVar (loc,x) -> Ident (loc,x)
- | _ -> anomaly "globalize_ref: not a reference"
-
-let globalize_ref_term vars ref =
- match Constrintern.interp_reference (vars,[]) ref with
- | RRef (loc,VarRef a) -> CRef (Ident (loc,a))
- | RRef (loc,a) -> CRef (Qualid (loc,qualid_of_sp (Nametab.sp_of_global a)))
- | RVar (loc,x) -> CRef (Ident (loc,x))
- | c -> Constrextern.extern_rawconstr Idset.empty c
-
-let rec globalize_constr_expr vars = function
- | CRef ref -> globalize_ref_term vars ref
- | CAppExpl (_,(p,ref),l) ->
- let f =
- map_constr_expr_with_binders globalize_constr_expr
- (fun x e -> e) vars
- in
- CAppExpl (dummy_loc,(p,globalize_ref vars ref), List.map f l)
- | c ->
- map_constr_expr_with_binders globalize_constr_expr (fun id e -> id::e)
- vars c
-
-let without_translation f x =
- let old = Options.do_translate () in
- let oldv7 = !Options.v7 in
- Options.make_translate false;
- try let r = f x in Options.make_translate old; Options.v7:=oldv7; r
- with e -> Options.make_translate old; Options.v7:=oldv7; raise e
-
-let _ = set_constr_globalizer
- (fun vars e -> for_grammar (without_translation (globalize_constr_expr vars)) e)
-
-(**********************************************************************)
-(** For old ast printer *)
-
-(* Pretty-printer state summary *)
-let _ =
- declare_summary "syntax"
- { freeze_function = Esyntax.freeze;
- unfreeze_function = Esyntax.unfreeze;
- init_function = Esyntax.init;
- survive_module = false;
- survive_section = false }
-
-(* Pretty-printing objects = syntax_entry *)
-let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj
-
-let subst_syntax (_,subst,ppobj) =
- Extend.subst_syntax_command Ast.subst_astpat subst ppobj
-
-let (inPPSyntax,outPPSyntax) =
- declare_object {(default_object "PPSYNTAX") with
- open_function = (fun i o -> if i=1 then cache_syntax o);
- cache_function = cache_syntax;
- subst_function = subst_syntax;
- classify_function = (fun (_,o) -> Substitute o);
- export_function = (fun x -> Some x) }
-
-(* Syntax extension functions (registered in the environnement) *)
-
-(* Checking the pretty-printing rules against free meta-variables.
- * Note that object are checked before they are added in the environment.
- * Syntax objects in compiled modules are not re-checked. *)
-
-let add_syntax_obj whatfor sel =
-(* if not !Options.v7_only then*)
- Lib.add_anonymous_leaf (inPPSyntax (interp_syntax_entry whatfor sel))
-
-(* Tokens *)
+(* Tokens *)
let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
@@ -134,69 +41,40 @@ let (inToken, outToken) =
let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
(**********************************************************************)
-(* Grammars (especially Tactic Notation) *)
+(* Tactic Notation *)
let make_terminal_status = function
| VTerm s -> Some s
| VNonTerm _ -> None
-let qualified_nterm current_univ = function
- | NtQual (univ, en) -> (univ, en)
- | NtShort en -> (current_univ, en)
-
-let rec make_tags = function
- | VTerm s :: l -> make_tags l
+let rec make_tags lev = function
+ | VTerm s :: l -> make_tags lev l
| VNonTerm (loc, nt, po) :: l ->
- let (u,nt) = qualified_nterm "tactic" nt in
- let (etyp, _) = Egrammar.interp_entry_name u nt in
- etyp :: make_tags l
+ let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in
+ etyp :: make_tags lev l
| [] -> []
-let declare_pprule = function
- (* Pretty-printing rules only for Grammar (Tactic Notation) *)
- | Egrammar.TacticGrammar (_,pp) ->
- let f (s,t,p) =
- Pptactic.declare_extra_tactic_pprule true s (t,p);
- Pptactic.declare_extra_tactic_pprule false s (t,p) in
- List.iter f pp
- | _ -> ()
+let cache_tactic_notation (_,(pa,pp)) =
+ Egrammar.extend_grammar (Egrammar.TacticGrammar pa);
+ Pptactic.declare_extra_tactic_pprule pp
-let cache_grammar (_,a) =
- Egrammar.extend_grammar a;
- declare_pprule a
+let subst_tactic_parule subst (key,n,p,(d,tac)) =
+ (key,n,p,(d,Tacinterp.subst_tactic subst tac))
-let subst_grammar (_,subst,a) =
- Egrammar.subst_all_grammar_command subst a
+let subst_tactic_notation (_,subst,(pa,pp)) =
+ (subst_tactic_parule subst pa,pp)
-let (inGrammar, outGrammar) =
- declare_object {(default_object "GRAMMAR") with
- open_function = (fun i o -> if i=1 then cache_grammar o);
- cache_function = cache_grammar;
- subst_function = subst_grammar;
+let (inTacticGrammar, outTacticGrammar) =
+ declare_object {(default_object "TacticGrammar") with
+ open_function = (fun i o -> if i=1 then cache_tactic_notation o);
+ cache_function = cache_tactic_notation;
+ subst_function = subst_tactic_notation;
classify_function = (fun (_,o) -> Substitute o);
export_function = (fun x -> Some x)}
-(**********************************************************************)
-(* V7 Grammar *)
-
-open Genarg
-
-let check_entry_type (u,n) =
- if u = "tactic" or u = "vernac" then error "tactic and vernac not supported";
- match entry_type (get_univ u) n with
- | None -> Pcoq.create_entry_if_new (get_univ u) n ConstrArgType
- | Some (ConstrArgType | IdentArgType | RefArgType) -> ()
- | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
-
-let add_grammar_obj univ entryl =
- let u = create_univ_if_new univ in
- let g = interp_grammar_command univ check_entry_type entryl in
- Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
-
-(**********************************************************************)
-(* V8 Grammar *)
-
-(* Tactic notations *)
+let cons_production_parameter l = function
+ | VTerm _ -> l
+ | VNonTerm (_,_,ido) -> option_cons ido l
let rec tactic_notation_key = function
| VTerm id :: _ -> id
@@ -207,41 +85,49 @@ let rec next_key_away key t =
if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
else key
-let locate_tactic_body dir (s,(s',prods as x),e) =
- let tags = make_tags prods in
- let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
- (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods))
-
-let add_tactic_grammar g =
- let dir = Lib.cwd () in
- let pa,pp = List.split (List.map (locate_tactic_body dir) g) in
- Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp)))
-
-(* Printing grammar entries *)
+let add_tactic_notation (n,prods,e) =
+ let tags = make_tags n prods in
+ let key = next_key_away (tactic_notation_key prods) tags in
+ let pprule = (key,tags,(n,List.map make_terminal_status prods)) in
+ let ids = List.fold_left cons_production_parameter [] prods in
+ let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
+ let parule = (key,n,prods,(Lib.cwd(),tac)) in
+ Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule))
-let print_grammar univ entry =
- if !Options.v7 then
- let u = get_univ univ in
- let typ = explicitize_entry (fst u) entry in
- let te,_,_ = get_constr_entry false typ in
- Gram.Entry.print te
- else
- match entry with
- | "constr" | "operconstr" | "binder_constr" ->
- msgnl (str "Entry constr is");
- Gram.Entry.print Pcoq.Constr.constr;
- msgnl (str "and lconstr is");
- Gram.Entry.print Pcoq.Constr.lconstr;
- msgnl (str "where binder_constr is");
- Gram.Entry.print Pcoq.Constr.binder_constr;
- msgnl (str "and operconstr is");
- Gram.Entry.print Pcoq.Constr.operconstr;
- | "pattern" ->
- Gram.Entry.print Pcoq.Constr.pattern
- | "tactic" ->
- Gram.Entry.print Pcoq.Tactic.simple_tactic
- | _ -> error "Unknown or unprintable grammar entry"
+(**********************************************************************)
+(* Printing grammar entries *)
+
+let print_grammar univ = function
+ | "constr" | "operconstr" | "binder_constr" ->
+ msgnl (str "Entry constr is");
+ Gram.Entry.print Pcoq.Constr.constr;
+ msgnl (str "and lconstr is");
+ Gram.Entry.print Pcoq.Constr.lconstr;
+ msgnl (str "where binder_constr is");
+ Gram.Entry.print Pcoq.Constr.binder_constr;
+ msgnl (str "and operconstr is");
+ Gram.Entry.print Pcoq.Constr.operconstr;
+ | "pattern" ->
+ Gram.Entry.print Pcoq.Constr.pattern
+ | "tactic" ->
+ msgnl (str "Entry tactic_expr is");
+ Gram.Entry.print Pcoq.Tactic.tactic_expr;
+ msgnl (str "Entry simple_tactic is");
+ Gram.Entry.print Pcoq.Tactic.simple_tactic;
+ | "vernac" ->
+ msgnl (str "Entry vernac is");
+ Gram.Entry.print Pcoq.Vernac_.vernac;
+ msgnl (str "Entry command is");
+ Gram.Entry.print Pcoq.Vernac_.command;
+ msgnl (str "Entry syntax is");
+ Gram.Entry.print Pcoq.Vernac_.syntax;
+ msgnl (str "Entry gallina is");
+ 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"
+(**********************************************************************)
(* Parse a format (every terminal starting with a letter or a single
quote (except a single quote alone) must be quoted) *)
@@ -342,12 +228,12 @@ let parse_format (loc,str) =
Stdpp.raise_with_loc loc e
(***********************)
-(* Analysing notations *)
-
-open Symbols
+(* Analyzing notations *)
type symbol_token = WhiteSpace of int | String of string
+(* Decompose the notation string into tokens *)
+
let split_notation_string str =
let push_token beg i l =
if beg = i then l else
@@ -376,6 +262,43 @@ let split_notation_string str =
in
loop 0 0
+(* Interpret notations with a recursive component *)
+
+let rec find_pattern xl = function
+ | Break n as x :: l, Break n' :: l' when n=n' ->
+ find_pattern (x::xl) (l,l')
+ | Terminal s as x :: l, Terminal s' :: l' when s = s' ->
+ find_pattern (x::xl) (l,l')
+ | [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")
+ | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+ 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\"")
+
+let rec interp_list_parser hd = function
+ | [] -> [], List.rev hd
+ | NonTerminal id :: tl when id = ldots_var ->
+ let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+ let yl,tl'' = interp_list_parser [] tl' in
+ (* We remember the second copy of each recursive part variable to *)
+ (* remove it afterwards *)
+ y::yl, SProdList (x,sl) :: tl''
+ | (Terminal _ | Break _) as s :: tl ->
+ if hd = [] then
+ let yl,tl' = interp_list_parser [] tl in
+ yl, s :: tl'
+ else
+ interp_list_parser (s::hd) tl
+ | NonTerminal _ as x :: tl ->
+ let yl,tl' = interp_list_parser [x] tl in
+ yl, List.rev_append hd tl'
+ | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+
+(* Find non-terminal tokens of notation *)
+
let unquote_notation_token s =
let n = String.length s in
if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
@@ -410,38 +333,12 @@ let rec raw_analyse_notation_tokens = function
let (vars,l) = raw_analyse_notation_tokens sl in
(vars, Break n :: l)
-let rec find_pattern xl = function
- | Break n as x :: l, Break n' :: l' when n=n' ->
- find_pattern (x::xl) (l,l')
- | Terminal s as x :: l, Terminal s' :: l' when s = s' ->
- find_pattern (x::xl) (l,l')
- | [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")
- | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
- 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\"")
-
-let rec interp_list_parser hd = function
- | [] -> [], List.rev hd
- | NonTerminal id :: tl when id = ldots_var ->
- let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
- let yl,tl'' = interp_list_parser [] tl' in
- (* We remember the second copy of each recursive part variable to *)
- (* remove it afterwards *)
- y::yl, SProdList (x,sl) :: tl''
- | (Terminal _ | Break _) as s :: tl ->
- if hd = [] then
- let yl,tl' = interp_list_parser [] tl in
- yl, s :: tl'
- else
- interp_list_parser (s::hd) tl
- | NonTerminal _ as x :: tl ->
- let yl,tl' = interp_list_parser [x] tl in
- yl, List.rev_append hd tl'
- | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+let is_numeral symbs =
+ match List.filter (function Break _ -> false | _ -> true) symbs with
+ | ([Terminal "-"; Terminal x] | [Terminal x]) ->
+ (try let _ = Bigint.of_string x in true with _ -> false)
+ | _ ->
+ false
let analyse_notation_tokens l =
let vars,l = raw_analyse_notation_tokens l in
@@ -450,7 +347,8 @@ let analyse_notation_tokens l =
let remove_vars = List.fold_right List.remove_assoc
-(* Build the syntax and grammar rules *)
+(**********************************************************************)
+(* Build pretty-printing rules *)
type printing_precedence = int * parenRelation
type parsing_precedence = int option
@@ -460,15 +358,10 @@ let prec_assoc = function
| Gramext.LeftA -> (E,L)
| Gramext.NonA -> (L,L)
-(* For old ast printer *)
-let meta_pattern m = Pmeta(m,Tany)
-
-type white_status = Juxtapose | Separate of int | NextIsTerminal
-
let precedence_of_entry_type from = function
| ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n
- | ETConstr (NumLevel n,BorderProd (left,Some a)) ->
- n, let (lp,rp) = prec_assoc a in if left then lp else rp
+ | ETConstr (NumLevel n,BorderProd (b,Some a)) ->
+ n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp
| ETConstr (NumLevel n,InternalProd) -> n, Prec n
| ETConstr (NextLevel,_) -> from, L
| ETOther ("constr","annot") -> 10, Prec 10
@@ -506,57 +399,15 @@ let is_operator s =
s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~')
-type previous_prod_status = NoBreak | CanBreak
-
let rec is_non_terminal = function
| NonTerminal _ | SProdList _ -> true
| _ -> false
-let add_break n l = UNP_BRK (n,1) :: l
-
-(* For old ast printer *)
-let make_hunks_ast symbols etyps from =
- let rec make ws = function
- | NonTerminal m :: prods ->
- let _,lp = precedence_of_entry_type from (List.assoc m etyps) in
- let u = PH (meta_pattern (string_of_id m), None, lp) in
- if prods <> [] && is_non_terminal (List.hd prods) then
- u :: add_break 1 (make CanBreak prods)
- else
- u :: make CanBreak prods
-
- | Terminal s :: prods when List.exists is_non_terminal prods ->
- let protect =
- is_letter s.[0] ||
- (is_non_terminal (List.hd prods) &&
- (is_letter (s.[String.length s -1])) ||
- (is_digit (s.[String.length s -1]))) in
- if is_comma s || is_right_bracket s then
- RO s :: add_break 0 (make NoBreak prods)
- else if (is_operator s || is_left_bracket s) && ws = CanBreak then
- add_break (if protect then 1 else 0)
- (RO (if protect then s^" " else s) :: make CanBreak prods)
- else
- if protect then
- (if ws = CanBreak then add_break 1 else (fun x -> x))
- (RO (s^" ") :: make CanBreak prods)
- else
- RO s :: make CanBreak prods
-
- | Terminal s :: prods ->
- RO s :: make NoBreak prods
-
- | Break n :: prods ->
- add_break n (make NoBreak prods)
-
- | SProdList _ :: _ ->
- anomaly "Recursive notations not supported in old syntax"
-
- | [] -> []
+let add_break n l = UnpCut (PpBrk(n,0)) :: l
- in make NoBreak symbols
+(* Heuristics for building default printing rules *)
-let add_break n l = UnpCut (PpBrk(n,0)) :: l
+type previous_prod_status = NoBreak | CanBreak
let make_hunks etyps symbols from =
let vars,typs = List.split etyps in
@@ -621,6 +472,8 @@ let make_hunks etyps symbols from =
in make NoBreak symbols
+(* Build default printing rules from explicit format *)
+
let error_format () = error "The format does not match the notation"
let rec split_format_at_ldots hd = function
@@ -656,12 +509,12 @@ let read_recursive_format sl fmt =
let slfmt, fmt = get_head fmt in
slfmt, get_tail (slfmt, fmt)
-let hunks_of_format (from,(vars,typs) as vt) symfmt =
+let hunks_of_format (from,(vars,typs)) symfmt =
let rec aux = function
| symbs, (UnpTerminal s' as u) :: fmt
when s' = String.make (String.length s') ' ' ->
let symbs, l = aux (symbs,fmt) in symbs, u :: l
- | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt
+ | Terminal s :: symbs, (UnpTerminal s') :: fmt
when s = unquote_notation_token s' ->
let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
| NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
@@ -689,36 +542,31 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
| [], l -> l
| _ -> error_format ()
-let string_of_prec (n,p) =
- (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
+(**********************************************************************)
+(* Build parsing rules *)
let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
-let string_of_assoc = function
- | Some(Gramext.RightA) -> "RIGHTA"
- | Some(Gramext.LeftA) | None -> "LEFTA"
- | Some(Gramext.NonA) -> "NONA"
-
let is_not_small_constr = function
ETConstr _ -> true
| ETOther("constr","binder_constr") -> true
| _ -> false
-let rec define_keywords = function
+let rec define_keywords_aux = function
NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l
- when not !Options.v7 && is_not_small_constr e ->
+ when is_not_small_constr e ->
prerr_endline ("Defining '"^k^"' as keyword");
Lexer.add_token("",k);
- n1 :: Term("",k) :: define_keywords l
- | n :: l -> n :: define_keywords l
+ n1 :: Term("",k) :: define_keywords_aux l
+ | n :: l -> n :: define_keywords_aux l
| [] -> []
let define_keywords = function
- Term("IDENT",k)::l when not !Options.v7 ->
+ Term("IDENT",k)::l ->
prerr_endline ("Defining '"^k^"' as keyword");
Lexer.add_token("",k);
- Term("",k) :: define_keywords l
- | l -> define_keywords l
+ Term("",k) :: define_keywords_aux l
+ | l -> define_keywords_aux l
let make_production etyps symbols =
let prod =
@@ -728,12 +576,12 @@ let make_production etyps symbols =
let typ = List.assoc m etyps in
NonTerm (typ, Some (m,typ)) :: l
| Terminal s ->
- Term (Extend.terminal s) :: l
+ Term (terminal s) :: l
| Break _ ->
l
| SProdList (x,sl) ->
let sl = List.flatten
- (List.map (function Terminal s -> [Extend.terminal s]
+ (List.map (function Terminal s -> [terminal s]
| Break _ -> []
| _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
let y = match List.assoc x etyps with
@@ -766,44 +614,8 @@ let recompute_assoc typs =
| _, Some Gramext.RightA -> Some Gramext.RightA
| _ -> None
-let make_grammar_rule n typs symbols ntn perm =
- let assoc = recompute_assoc typs in
- let prod = make_production typs symbols in
- (n,assoc,ntn,prod, perm)
-
-(* For old ast printer *)
-let metas_of sl =
- List.fold_right
- (fun it metatl -> match it with
- | NonTerminal m -> m::metatl
- | _ -> metatl)
- sl []
-
-(* For old ast printer *)
-let make_pattern symbols ast =
- let env = List.map (fun m -> (string_of_id m,ETast)) (metas_of symbols) in
- fst (to_pat env ast)
-
-(* For old ast printer *)
-let make_syntax_rule n name symbols typs ast ntn sc =
- [{syn_id = name;
- syn_prec = n;
- syn_astpat = make_pattern symbols ast;
- syn_hunks =
- [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
-
-let make_pp_rule (n,typs,symbols,fmt) =
- match fmt with
- | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
- | Some fmt ->
- [UnpBox (PpHOVB 0,
- hunks_of_format (n,List.split typs) (symbols,parse_format fmt))]
-
(**************************************************************************)
-(* Syntax extenstion: common parsing/printing rules and no interpretation *)
-
-(* v7 and translator : prec is for v7 (None if V8Notation), prec8 is for v8 *)
-(* v8 : prec is for v8, prec8 is the same *)
+(* Registration of syntax extensions (parsing/printing, no interpretation)*)
let pr_arg_level from = function
| (n,L) when n=from -> str "at next level"
@@ -813,66 +625,38 @@ let pr_arg_level from = function
| (n,_) -> str "Unknown level"
let pr_level ntn (from,args) =
- let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in
-(*
- let ppassoc, args = match args with
- | [] -> mt (), []
- | (nl,lpr)::l when nl=from & fst (list_last l)=from ->
- let (_,rpr),l = list_sep_last l in
- match lpr, snd (list_last l) with
- | L,E -> Gramext.RightA, l
- | E,L -> Gramext.LeftA, l
- | L,L -> Gramext.NoneA, l
- | _ -> args
-*)
str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
prlist_with_sep pr_coma (pr_arg_level from) args
-(* In v8: prec = Some prec8 is for both parsing and printing *)
-(* In v7 and translator:
- prec is for parsing (None if V8Notation),
- prec8 for v8 printing (v7 printing is via ast) *)
-let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) =
+let error_incompatible_level ntn oldprec prec =
+ errorlabstrm ""
+ (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)
+
+let cache_one_syntax_extension (prec,ntn,gr,pp) =
try
- let oldprec, oldprec8 = Symbols.level_of_notation ntn in
- if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then
- errorlabstrm ""
- (str ((if Options.do_translate () then "For new syntax, notation "
- else "Notation ")
- ^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++
- spc() ++ str "while it is now required to be" ++ spc() ++
- pr_level ntn prec8)
- else
- (* Inconsistent v8 notations but not while translating; forget... *)
- ();
- (* V8 notations are consistent (from both translator or v8) *)
- if prec <> None & !Options.v7 then begin
- (* Update the V7 parsing rule *)
- if oldprec <> None & out_some oldprec <> out_some prec then
- (* None of them is V8Notation and they are different: warn *)
- Options.if_verbose
- warning ("Notation "^ntn^
- " was already assigned a different level or sublevels");
- if oldprec = None or out_some oldprec <> out_some prec then
- Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr))
- end
+ let oldprec = Notation.level_of_notation ntn in
+ if prec <> oldprec then error_incompatible_level ntn oldprec prec
with Not_found ->
(* Reserve the notation level *)
- Symbols.declare_notation_level ntn (prec,prec8);
+ Notation.declare_notation_level ntn prec;
(* Declare the parsing rule *)
- option_iter (fun gr ->
- Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr;
+ Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
(* Declare the printing rule *)
- Symbols.declare_notation_printing_rule ntn (se,fst prec8)
+ Notation.declare_notation_printing_rule ntn (pp,fst prec)
+
+let cache_syntax_extension (_,(_,sy_rules)) =
+ List.iter cache_one_syntax_extension sy_rules
-let subst_notation_grammar subst x = x
+let subst_parsing_rule subst x = x
let subst_printing_rule subst x = x
-let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) =
- (local,(prec,ntn,
- option_app (subst_notation_grammar subst) gr,
- subst_printing_rule subst se))
+let subst_syntax_extension (_,subst,(local,sy)) =
+ (local, List.map (fun (prec,ntn,gr,pp) ->
+ (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy)
let classify_syntax_definition (_,(local,_ as o)) =
if local then Dispose else Substitute o
@@ -888,6 +672,11 @@ let (inSyntaxExtension, outSyntaxExtension) =
classify_function = classify_syntax_definition;
export_function = export_syntax_definition}
+(**************************************************************************)
+(* Precedences *)
+
+(* Interpreting user-provided modifiers *)
+
let interp_modifiers modl =
let onlyparsing = ref false in
let rec interp assoc level etyps format = function
@@ -896,23 +685,22 @@ 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")
- else interp assoc level ((id,typ)::etyps) format l
+ 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")
- else
- let typ = ETConstr (n,()) in
- interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
+ 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"
- else interp assoc (Some n) etyps format l
+ 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"
- else interp (Some a) level etyps format l
+ 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
@@ -921,21 +709,15 @@ let interp_modifiers modl =
interp assoc level etyps (Some s) l
in interp None None [] None modl
-let merge_modifiers a n l =
- (match a with None -> [] | Some a -> [SetAssoc a]) @
- (match n with None -> [] | Some n -> [SetLevel n]) @ l
-
-let interp_infix_modifiers modl =
- let (assoc,level,t,b,fmt) = interp_modifiers modl in
+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";
- (assoc,level,b,fmt)
+ error "explicit entry level or type unexpected in infix notation"
+
+let no_syntax_modifiers modifiers =
+ modifiers = [] or modifiers = [SetOnlyParsing]
-(* 2nd list of types has priority *)
-let rec merge_entry_types etyps' = function
- | [] -> etyps'
- | (x,_ as e)::etyps ->
- e :: merge_entry_types (List.remove_assoc x etyps') etyps
+(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type etyps (x,typ) =
let typ = try
@@ -948,7 +730,7 @@ let set_entry_type etyps (x,typ) =
with Not_found -> ETConstr typ
in (x,typ)
-let check_rule_reversibility l =
+let check_rule_productivity l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
error "A notation must include at least one symbol"
@@ -956,17 +738,6 @@ let is_not_printable = function
| AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
| _ -> false
-let find_precedence_v7 lev etyps symbols =
- (match symbols with
- | NonTerminal x :: _ ->
- (try match List.assoc x etyps with
- | ETConstr _ ->
- error "The level of the leftmost non-terminal cannot be changed"
- | _ -> ()
- with Not_found -> ())
- | _ -> ());
- if lev = None then 1 else out_some lev
-
let find_precedence lev etyps symbols =
match symbols with
| NonTerminal x :: _ ->
@@ -1000,7 +771,7 @@ let find_precedence lev etyps symbols =
out_some lev
let check_curly_brackets_notation_exists () =
- try let _ = Symbols.level_of_notation "{ _ }" in ()
+ 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"
@@ -1028,95 +799,59 @@ let remove_curly_brackets l =
| x :: l -> x :: aux false l
in aux true l
-let compute_syntax_data forv7 (df,modifiers) =
+let compute_syntax_data (df,modifiers) =
let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
(* Notation defaults to NONA *)
let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
let toks = split_notation_string df in
let (recvars,vars,symbols) = analyse_notation_tokens toks in
let ntn_for_interp = make_notation_key symbols in
- let symbols = remove_curly_brackets symbols in
- let notation = make_notation_key symbols in
- check_rule_reversibility symbols;
- let n =
- if !Options.v7 then find_precedence_v7 n etyps symbols
- else find_precedence n etyps symbols in
- let innerlevel = NumLevel (if forv7 then 10 else 200) in
+ let symbols' = remove_curly_brackets symbols in
+ let need_squash = (symbols <> symbols') in
+ let ntn_for_grammar = make_notation_key symbols' in
+ check_rule_productivity symbols';
+ let n = find_precedence n etyps symbols' in
+ let innerlevel = NumLevel 200 in
let typs =
find_symbols
- (NumLevel n,BorderProd(true,assoc))
+ (NumLevel n,BorderProd(Left,assoc))
(innerlevel,InternalProd)
- (NumLevel n,BorderProd(false,assoc))
- symbols in
+ (NumLevel n,BorderProd(Right,assoc))
+ symbols' in
(* To globalize... *)
let typs = List.map (set_entry_type etyps) typs in
- let ppdata = (n,typs,symbols,fmt) in
let prec = (n,List.map (assoc_of_type n) typs) in
- ((onlyparse,recvars,vars,
- ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df))
-
-(* Uninterpreted (reserved) notations *)
-let add_syntax_extension local mv mv8 =
- (* from v7:
- if mv8 <> None: tells the translator how to print in v8
- if mv <> None: tells how to parse and, how to print in v7
- mv = None = mv8 does not occur
- from v8 (mv8 is always None and mv is always Some)
- mv tells how to parse and print in v8
- *)
- let data8 = option_app (compute_syntax_data false) mv8 in
- let data = option_app (compute_syntax_data !Options.v7) mv in
- let prec,gram_rule = match data with
- | None -> None, None (* Case of V8Notation from v7 *)
- | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) ->
- Some prec, Some (make_grammar_rule n typs symbols notation None) in
- match data, data8 with
- | None, None -> (* Nothing to do: V8Notation while not translating *) ()
- | _, Some d | Some d, None ->
- let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *)
- let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
- let pp_rule = make_pp_rule ppdata in
- Lib.add_anonymous_leaf
- (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule)))
+ let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
+ let df' = (Lib.library_dp(),df) in
+ let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in
+ (i_data,sy_data)
(**********************************************************************)
-(* Distfix, Infix, Symbols *)
-
-(* A notation comes with a grammar rule, a pretty-printing rule, an
- identifiying pattern called notation and an associated scope *)
-let load_notation _ (_,(_,_,ntn,scope,pat,onlyparse,_,_)) =
- option_iter Symbols.declare_scope scope
-
-let open_notation i (_,(_,oldse,ntn,scope,pat,onlyparse,pp8only,df)) =
- if i=1 then begin
- let b,oldpp8only = Symbols.exists_notation_in_scope scope ntn pat in
- (* Declare the old printer rule and its interpretation *)
- if (not b or oldpp8only) & oldse <> None then
- Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse};
+(* Registration of notations interpretation *)
+
+let load_notation _ (_,(_,scope,pat,onlyparse,_)) =
+ option_iter Notation.declare_scope scope
+
+let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) =
+ if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin
(* Declare the interpretation *)
- if not b then
- Symbols.declare_notation_interpretation ntn scope pat df pp8only;
- if oldpp8only & not pp8only then
- Options.silently
- (Symbols.declare_notation_interpretation ntn scope pat df) pp8only;
- if not b & not onlyparse then
- Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat
+ Notation.declare_notation_interpretation ntn scope pat df;
+ (* Declare the uninterpretation *)
+ if not onlyparse then
+ Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat
end
let cache_notation o =
load_notation 1 o;
open_notation 1 o
-let subst_notation (_,subst,(lc,oldse,ntn,scope,(metas,pat),b,b',df)) =
- (lc,option_app
- (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse,
- ntn,scope,
- (metas,subst_aconstr subst pat), b, b', df)
+let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) =
+ (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf)
-let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) =
+let classify_notation (_,(local,_,_,_,_ as o)) =
if local then Dispose else Substitute o
-let export_notation (local,_,_,_,_,_,_,_ as o) =
+let export_notation (local,_,_,_,_ as o) =
if local then None else Some o
let (inNotation, outNotation) =
@@ -1128,37 +863,8 @@ let (inNotation, outNotation) =
classify_function = classify_notation;
export_function = export_notation}
-(* For old ast printer *)
-let rec reify_meta_ast vars = function
- | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast vars body)
-(* | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)*)
- | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_")
- | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast vars) args)
- | Slam(loc,Some id,body) when List.mem id vars ->
- Smetalam (loc,string_of_id id,reify_meta_ast vars body)
- | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body)
- | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id)
- | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
- | Dynamic _ as a -> (* Hum... what to do here *) a
-
-(* For old ast syntax *)
-let make_old_pp_rule n symbols typs r ntn scope vars =
- let ast = Termast.ast_of_rawconstr r in
- let ast = reify_meta_ast vars ast in
- let scope_name = match scope with Some s -> s | None -> "core_scope" in
- let rule_name = ntn^"_"^scope_name^"_notation" in
- make_syntax_rule n rule_name symbols typs ast ntn scope
-
-(* maps positions in v8-notation into positions in v7-notation (used
- for parsing).
- For instance Notation "x < y < z" := .. V8only "y < z < x"
- yields [1; 2; 0] (y is the second arg in v7; z is 3rd; x is fst) *)
-let mk_permut vars7 vars8 =
- if vars7=vars8 then None else
- Some
- (List.fold_right
- (fun v8 subs -> list_index v8 vars7 - 1 :: subs)
- vars8 [])
+(**********************************************************************)
+(* Recovering existing syntax *)
let contract_notation ntn =
if ntn = "{ _ }" then ntn else
@@ -1173,304 +879,120 @@ let contract_notation ntn =
else ntn in
aux ntn 0
-let add_notation_in_scope local df c mods omodv8 scope =
- let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')=
- compute_syntax_data !Options.v7 (df,mods) in
- (* Declare the parsing and printing rules if not already done *)
- (* For both v7 and translate: parsing is as described for v7 in v7 file *)
- (* For v8: parsing is as described in v8 file *)
- (* For v7: printing is by the old printer - see below *)
- (* For translate: printing is as described for v8 in v7 file *)
- (* For v8: printing is as described in v8 file *)
- (* In short: parsing does not depend on omodv8 *)
- (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *)
- (* if in v7, or of mods without scaling if in v8 *)
- let intnot,ntn,pprecvars,ppvars,ppprec,pp_rule =
- match omodv8 with
- | Some mv8 ->
- let (_,recs8,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in
- intnot8,ntn8,recs8,vars8,p,make_pp_rule d
- | None when not !Options.v7 ->
- intnot,notation,recs,vars,prec,make_pp_rule ppdata
- | None ->
- (* means the rule already exists: recover it *)
- (* occurs only with V8only flag alone *)
- try
- let ntn = contract_notation notation in
- let _, oldprec8 = Symbols.level_of_notation ntn in
- let rule,_ = Symbols.find_notation_printing_rule ntn in
- notation,ntn,recs,vars,oldprec8,rule
- with Not_found -> error "No known parsing rule for this notation in V8"
- in
- let permut = mk_permut vars ppvars in
- let gram_rule = make_grammar_rule n typs symbols ntn permut in
- Lib.add_anonymous_leaf
- (inSyntaxExtension
- (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule)));
-
- (* Declare interpretation *)
- let (acvars,ac) = interp_aconstr [] ppvars c in
- let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in
- let old_pp_rule =
- (* Used only by v7; disable if contains a recursive pattern *)
- if onlyparse or pprecvars <> [] or not (!Options.v7) then None
- else
- let r = interp_global_rawconstr_with_vars vars c in
- Some (make_old_pp_rule n symbols typs r intnot scope vars) in
- let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in
- Lib.add_anonymous_leaf
- (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df'))
-
-let level_rule (n,p) = if p = E then n else max (n-1) 0
+exception NoSyntaxRule
-let recover_syntax ntn =
+let recover_syntax ntn =
try
- match Symbols.level_of_notation ntn with
- | (Some prec,_ as pprec) ->
- let rule,_ = Symbols.find_notation_printing_rule ntn in
- let gr = Egrammar.recover_notation_grammar ntn prec in
- Some (pprec,ntn,Some gr,rule)
- | None,_ -> None
- with Not_found -> None
+ let prec = Notation.level_of_notation ntn in
+ let pprule,_ = Notation.find_notation_printing_rule ntn in
+ let gr = Egrammar.recover_notation_grammar ntn prec in
+ (prec,ntn,gr,pprule)
+ with Not_found ->
+ raise NoSyntaxRule
+
+let recover_squash_syntax () = recover_syntax "{ _ }"
let recover_notation_syntax rawntn =
let ntn = contract_notation rawntn in
- match recover_syntax ntn with
- | None -> None
- | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }")
-
-let set_data_for_v7_pp recs a vars =
- if not !Options.v7 then None else
- if recs=[] then Some (a,vars)
- else (warning "No recursive notation in v7 syntax";None)
-
-let build_old_pp_rule notation scope symbs (r,vars) =
- let prec =
- try
- let a,_ = Symbols.level_of_notation (contract_notation notation) in
- if a = None then raise Not_found else out_some a
- with Not_found ->
- error "Parsing rule for this notation has to be previously declared" in
- let typs = List.map2
- (fun id n ->
- id,ETConstr (NumLevel (level_rule n),InternalProd)) vars (snd prec) in
- make_old_pp_rule (fst prec) symbs typs r notation scope vars
-
-let add_notation_interpretation_core local symbs for_old df a scope onlyparse
- onlypp gram_data =
- let notation = make_notation_key symbs in
- let old_pp_rule =
- if !Options.v7 then
- option_app (build_old_pp_rule notation scope symbs) for_old
- else None in
- option_iter
- (fun (x,y) ->
- Lib.add_anonymous_leaf (inSyntaxExtension (local,x));
- option_iter
- (fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y)
- gram_data;
- Lib.add_anonymous_leaf
- (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,
- (Lib.library_dp(),df)))
+ let sy_rule = recover_syntax ntn in
+ let need_squash = ntn<>rawntn in
+ if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
-let add_notation_interpretation df names c sc =
+(**********************************************************************)
+(* Main entry point for building parsing and printing rules *)
+
+let make_pa_rule (n,typs,symbols,_) ntn =
+ let assoc = recompute_assoc typs in
+ let prod = make_production typs symbols in
+ (n,assoc,ntn,prod)
+
+let make_pp_rule (n,typs,symbols,fmt) =
+ match fmt with
+ | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
+ | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt)
+
+let make_syntax_rules (ntn,prec,need_squash,sy_data) =
+ let pa_rule = make_pa_rule sy_data ntn in
+ let pp_rule = make_pp_rule sy_data in
+ let sy_rule = (prec,ntn,pa_rule,pp_rule) in
+ (* By construction, the rule for "{ _ }" is declared, but we need to
+ redeclare it because the file where it is declared needs not be open
+ when the current file opens (especially in presence of -nois) *)
+ if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
+
+(**********************************************************************)
+(* Main functions about notations *)
+
+let add_notation_in_scope local df c mods scope =
+ let (i_data,sy_data) = compute_syntax_data (df,mods) in
+ (* Declare the parsing and printing rules *)
+ let sy_rules = make_syntax_rules sy_data in
+ Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
+ (* Declare interpretation *)
+ let (onlyparse,recvars,vars,df') = i_data in
+ let (acvars,ac) = interp_aconstr [] vars c in
+ let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in
+ let onlyparse = onlyparse or is_not_printable ac in
+ Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+
+let add_notation_interpretation_core local df names c scope onlyparse =
let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
- let gram_data = recover_notation_syntax (make_notation_key symbs) in
- if gram_data = None then
- error "Parsing rule for this notation has to be previously declared";
+ (* Redeclare pa/pp rules *)
+ if not (is_numeral symbs) then begin
+ let sy_rules = recover_notation_syntax (make_notation_key symbs) in
+ Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
+ end;
+ (* Declare interpretation *)
+ let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
let (acvars,ac) = interp_aconstr names vars c in
let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
- let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in
- let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
- let onlyparse = is_not_printable ac in
- add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse
- false gram_data
-
-let add_notation_in_scope_v8only local df c mv8 scope =
- let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
- let pp_rule = make_pp_rule ppdata in
- Lib.add_anonymous_leaf
- (inSyntaxExtension(local,((None,prec),notation,None,pp_rule)));
- (* Declare the interpretation *)
- let (acvars,ac) = interp_aconstr [] vars c in
- let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
- let onlyparse = is_not_printable ac in
- Lib.add_anonymous_leaf
- (inNotation(local,None,intnot,scope,a,onlyparse,true,df'))
+ let onlyparse = onlyparse or is_not_printable ac in
+ Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
-let add_notation_v8only local c (df,modifiers) sc =
- let toks = split_notation_string df in
- match toks with
- | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
- (* This is a ident to be declared as a rule *)
- add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc
- | _ ->
- let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in
- match lev with
- | None->
- if modifiers <> [] & modifiers <> [SetOnlyParsing] then
- error "Parsing rule for this notation includes no level"
- else
- (* Declare only interpretation *)
- let (recs,vars,symbs) = analyse_notation_tokens toks in
- let (acvars,ac) = interp_aconstr [] vars c in
- let onlyparse = modifiers = [SetOnlyParsing]
- or is_not_printable ac in
- let a = (remove_vars recs acvars,ac) in
- add_notation_interpretation_core local symbs None df a sc
- onlyparse true None
- | Some n ->
- (* Declare both syntax and interpretation *)
- let mods =
- if List.for_all (function SetAssoc _ -> false | _ -> true)
- modifiers
- then SetAssoc Gramext.NonA :: modifiers else modifiers in
- add_notation_in_scope_v8only local df c mods sc
-
-let is_quoted_ident x =
- let x' = unquote_notation_token x in
- x <> x' & try Lexer.check_ident x'; true with _ -> false
-
-(* v7: dfmod=None; mv8=Some: add only v8 printing rule *)
-(* dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *)
-(* dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *)
-(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *)
-let add_notation local c dfmod mv8 sc =
- match dfmod with
- | None -> add_notation_v8only local c (out_some mv8) sc
- | Some (df,modifiers) ->
- let toks = split_notation_string df in
- match toks with
- | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
- (* This is a ident to be declared as a rule *)
- add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc
- | _ ->
- let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers in
- match lev with
- | None->
- if modifiers <> [] & modifiers <> [SetOnlyParsing] then
- error "Parsing rule for this notation includes no level"
- else
- (* Declare only interpretation *)
- let (recs,vars,symbs) = analyse_notation_tokens toks in
- let gram_data =
- recover_notation_syntax (make_notation_key symbs) in
- if gram_data <> None then
- let (acvars,ac) = interp_aconstr [] vars c in
- let a = (remove_vars recs acvars,ac) in
- let onlyparse = modifiers = [SetOnlyParsing]
- or is_not_printable ac in
- let a_for_old = interp_global_rawconstr_with_vars vars c in
- let for_old = set_data_for_v7_pp recs a_for_old vars in
- add_notation_interpretation_core local symbs for_old df a
- sc onlyparse false gram_data
- else
- add_notation_in_scope local df c modifiers mv8 sc
- | Some n ->
- (* Declare both syntax and interpretation *)
- let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
- add_notation_in_scope local df c modifiers mv8 sc
-
-(* TODO add boxes information in the expression *)
+(* Notations without interpretation (Reserved Notation) *)
+
+let add_syntax_extension local mv =
+ let (_,sy_data) = compute_syntax_data mv in
+ let sy_rules = make_syntax_rules sy_data in
+ Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
+
+(* Notations with only interpretation *)
+
+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"
+
+(* Main entry point *)
+
+let add_notation local c (df,modifiers) sc =
+ if no_syntax_modifiers modifiers then
+ (* No syntax data: try to rely on a previously declared rule *)
+ let onlyparse = modifiers=[SetOnlyParsing] in
+ try add_notation_interpretation_core local df [] c sc onlyparse
+ with NoSyntaxRule ->
+ (* Try to determine a default syntax rule *)
+ add_notation_in_scope local df c modifiers sc
+ else
+ (* Declare both syntax and interpretation *)
+ add_notation_in_scope local df c modifiers sc
+
+(* Infix notations *)
let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
-let rec rename x vars n = function
- | [] ->
- (vars,[])
- | String "_"::l ->
- let (vars,l) = rename x vars (n+1) l in
- let xn = x^(string_of_int n) in
- ((inject_var xn)::vars,xn::l)
- | String y::l ->
- let (vars,l) = rename x vars n l in (vars,(quote_notation_token y)::l)
- | WhiteSpace _::l ->
- rename x vars n l
-
-let translate_distfix assoc df r =
- let (vars,l) = rename "x" [] 1 (split_notation_string df) in
- let df = String.concat " " l in
- let a = mkAppC (mkRefC r, vars) in
- let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
- (assoc,df,a)
-
-let add_distfix local assoc n df r sc =
- (* "x" cannot clash since r is globalized (included section vars) *)
- let (vars,l) = rename "x" [] 1 (split_notation_string df) in
- let df = String.concat " " l in
- let a = mkAppC (mkRefC r, vars) in
- let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
- add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc
-
-let make_infix_data n assoc modl mv8 =
- (* Infix defaults to LEFTA in V7 (cf doc) *)
- let mv = match n with None when !Options.v7 -> SetLevel 1 :: modl | _ -> modl in
- let mv = match assoc with None when !Options.v7 -> SetAssoc Gramext.LeftA :: mv | _ -> mv in
- let mv8 = match mv8 with
- None -> None
- | Some(s8,mv8) ->
- if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then
- error "Needs a level"
- else Some (("x "^quote_notation_token s8^" y"),mv8) in
- mv,mv8
-
-let add_infix local (inf,modl) pr mv8 sc =
- if inf="" (* Code for V8Infix only *) then
- let (p8,mv8) = out_some mv8 in
- let (a8,n8,onlyparse,fmt) = interp_infix_modifiers mv8 in
- let metas = [inject_var "x"; inject_var "y"] in
- let a = mkAppC (mkRefC pr,metas) in
- let df = "x "^(quote_notation_token p8)^" y" in
- let toks = split_notation_string df in
- if a8=None & n8=None & fmt=None then
- (* Declare only interpretation *)
- let (recs,vars,symbs) = analyse_notation_tokens toks in
- let (acvars,ac) = interp_aconstr [] vars a in
- let a' = (remove_vars recs acvars,ac) in
- let a_for_old = interp_global_rawconstr_with_vars vars a in
- add_notation_interpretation_core local symbs None df a' sc
- onlyparse true None
- else
- if n8 = None then error "Needs a level" else
- let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in
- add_notation_in_scope_v8only local df a mv8 sc
- else begin
- let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in
+let add_infix local (inf,modifiers) pr sc =
+ check_infix_modifiers modifiers;
(* check the precedence *)
- if !Options.v7 & (n<> None & (out_some n < 1 or out_some n > 10)) then
- errorlabstrm "Metasyntax.infix_grammar_entry"
- (str"Precedence must be between 1 and 10.");
- (*
- if (assoc<>None) & (n<6 or n>9) then
- errorlabstrm "Vernacentries.infix_grammar_entry"
- (str"Associativity Precedence must be 6,7,8 or 9.");
- *)
let metas = [inject_var "x"; inject_var "y"] in
- let a = mkAppC (mkRefC pr,metas) in
+ let c = mkAppC (mkRefC pr,metas) in
let df = "x "^(quote_notation_token inf)^" y" in
- let toks = split_notation_string df in
- if not !Options.v7 & n=None & assoc=None then
- (* En v8, une notation sans information de parsing signifie *)
- (* de ne déclarer que l'interprétation *)
- (* Declare only interpretation *)
- let (recs,vars,symbs) = analyse_notation_tokens toks in
- let gram_data = recover_notation_syntax (make_notation_key symbs) in
- if gram_data <> None then
- let (acvars,ac) = interp_aconstr [] vars a in
- let a' = (remove_vars recs acvars,ac) in
- let a_for_old = interp_global_rawconstr_with_vars vars a in
- let for_old = set_data_for_v7_pp recs a_for_old vars in
- add_notation_interpretation_core local symbs for_old df a' sc
- onlyparse false gram_data
- else
- let mv,mv8 = make_infix_data n assoc modl mv8 in
- add_notation_in_scope local df a mv mv8 sc
- else
- let mv,mv8 = make_infix_data n assoc modl mv8 in
- add_notation_in_scope local df a mv mv8 sc
- end
+ add_notation local c (df,modifiers) sc
+
+(**********************************************************************)
+(* Miscellaneous *)
-let standardise_locatable_notation ntn =
+let standardize_locatable_notation ntn =
let unquote = function
| String s -> [unquote_notation_token s]
| _ -> [] in
@@ -1480,17 +1002,19 @@ let standardise_locatable_notation ntn =
else
unquote_notation_token ntn
-(* Delimiters and classes bound to scopes *)
+(**********************************************************************)
+(* Delimiters and classes bound to scopes *)
+
type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
let load_scope_command _ (_,(scope,dlm)) =
- Symbols.declare_scope scope
+ Notation.declare_scope scope
let open_scope_command i (_,(scope,o)) =
if i=1 then
match o with
- | ScopeDelim dlm -> Symbols.declare_delimiters scope dlm
- | ScopeClasses cl -> Symbols.declare_class_scope scope cl
+ | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+ | ScopeClasses cl -> Notation.declare_class_scope scope cl
let cache_scope_command o =
load_scope_command 1 o;
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index be90cd7a..71522567 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: metasyntax.mli,v 1.26.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
(*i*)
open Util
@@ -15,49 +15,44 @@ open Ppextend
open Extend
open Tacexpr
open Vernacexpr
-open Symbols
+open Notation
open Topconstr
(*i*)
-(* Adding grammar and pretty-printing objects in the environment *)
+val add_token_obj : string -> unit
-val add_syntax_obj : string -> raw_syntax_entry list -> unit
+(* Adding a tactic notation in the environment *)
-val add_grammar_obj : string -> raw_grammar_entry list -> unit
-val add_token_obj : string -> unit
-val add_tactic_grammar :
- (string * (string * grammar_production list) * raw_tactic_expr) list -> unit
+val add_tactic_notation :
+ int * grammar_production list * raw_tactic_expr -> unit
+
+(* Adding a (constr) notation in the environment*)
val add_infix : locality_flag -> (string * syntax_modifier list) ->
- reference -> (string * syntax_modifier list) option ->
- scope_name option -> unit
-val add_distfix : locality_flag ->
- grammar_associativity -> precedence -> string -> reference
- -> scope_name option -> unit
-val translate_distfix : grammar_associativity -> string -> reference ->
- Gramext.g_assoc * string * constr_expr
+ reference -> scope_name option -> unit
+
+val add_notation : locality_flag -> constr_expr ->
+ (string * syntax_modifier list) -> scope_name option -> unit
+
+(* Declaring delimiter keys and default scopes *)
val add_delimiters : scope_name -> string -> unit
val add_class_scope : scope_name -> Classops.cl_typ -> unit
-val add_notation : locality_flag -> constr_expr
- -> (string * syntax_modifier list) option
- -> (string * syntax_modifier list) option
- -> scope_name option -> unit
+(* Add only the interpretation of a notation that already has pa/pp rules *)
-val add_notation_interpretation : string -> Constrintern.implicits_env
- -> constr_expr -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env ->
+ constr_expr -> scope_name option -> unit
-val add_syntax_extension : locality_flag
- -> (string * syntax_modifier list) option
- -> (string * syntax_modifier list) option -> unit
+(* Add only the parsing/printing rule of a notation *)
-val print_grammar : string -> string -> unit
+val add_syntax_extension :
+ locality_flag -> (string * syntax_modifier list) -> unit
-val merge_modifiers : Gramext.g_assoc option -> int option ->
- syntax_modifier list -> syntax_modifier list
+(* Print the Camlp4 state of a grammar *)
+
+val print_grammar : string -> string -> unit
-val interp_infix_modifiers : syntax_modifier list ->
- Gramext.g_assoc option * precedence option * bool * string located option
+(* Removes quotes in a notation *)
-val standardise_locatable_notation : string -> string
+val standardize_locatable_notation : string -> string
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index dcf3e307..490765a4 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: minicoq.ml,v 1.28.14.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4da23d42..a3b7fc14 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: mltop.ml4,v 1.29.2.3 2004/07/17 13:00:15 herbelin Exp $ *)
+(* $Id: mltop.ml4 6692 2005-02-06 13:03:51Z herbelin $ *)
open Util
open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
[Filename.dirname gname]
with | Dynlink.Error a ->
errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
- else ()
+ else ()
| Native ->
errorlabstrm "Mltop.no_load_object"
[< str"Loading of ML object file forbidden in a native Coq" >]
@@ -137,7 +137,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
if exists_dir dir then
begin
add_ml_dir dir;
- Library.add_load_path_entry (dir,coq_dirpath)
+ Library.add_load_path (dir,coq_dirpath)
end
else
msg_warning [< str ("Cannot open " ^ dir) >]
@@ -160,7 +160,7 @@ let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
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_entry dirs
+ List.iter Library.add_load_path dirs
end
else
msg_warning [< str ("Cannot open " ^ dir) >]
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 6ba8cd76..b869f70b 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mltop.mli,v 1.8.14.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: mltop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* If there is a toplevel under Coq, it is described by the following
record. *)
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index c748a12d..a9ff3326 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: protectedtoplevel.ml,v 1.9.10.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: protectedtoplevel.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
open Pp
open Line_oriented_parser
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
index b31afbf6..1d4ba9fc 100644
--- a/toplevel/protectedtoplevel.mli
+++ b/toplevel/protectedtoplevel.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: protectedtoplevel.mli,v 1.5.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: protectedtoplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3a10c7e5..b24e85da 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: record.ml,v 1.52.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: record.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
open Pp
open Util
@@ -20,7 +20,6 @@ open Declarations
open Entries
open Declare
open Nametab
-open Coqast
open Constrintern
open Command
open Inductive
@@ -37,31 +36,14 @@ let interp_decl sigma env = function
| Vernacexpr.DefExpr((_,id),c,t) ->
let c = match t with
| None -> c
- | Some t -> mkCastC (c,t)
+ | Some t -> mkCastC (c,DEFAULTcast,t)
in
- let j = judgment_of_rawconstr Evd.empty env c in
+ let j = interp_constr_judgment Evd.empty env c in
(id,Some j.uj_val, j.uj_type)
let typecheck_params_and_fields ps fs =
let env0 = Global.env () in
- let env1,newps =
- List.fold_left
- (fun (env,newps) d -> match d with
- | LocalRawAssum ([_,na],(CHole _ as t)) ->
- let t = interp_binder Evd.empty env na t in
- let d = (na,None,t) in
- (push_rel d env, d::newps)
- | LocalRawAssum (nal,t) ->
- let t = interp_type Evd.empty env t in
- let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
- let ctx = List.rev ctx in
- (push_rel_context ctx env, ctx@newps)
- | LocalRawDef ((_,na),c) ->
- let c = judgment_of_rawconstr Evd.empty env c in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env, d::newps))
- (env0,[]) ps
- in
+ let env1,newps = interp_context Evd.empty env0 ps in
let env2,newfs =
List.fold_left
(fun (env,newfs) d ->
@@ -146,19 +128,20 @@ let subst_projection fid l c =
let declare_projections indsp coers fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
- let paramdecls = mip.mind_params_ctxt in
+ let paramdecls = mib.mind_params_ctxt in
let r = mkInd indsp in
let rp = applist (r, extended_rel_list 0 paramdecls) in
let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = Termops.named_hd (Global.env()) r Anonymous in
let lifted_fields = lift_rel_context 1 fields in
- let (_,sp_projs,_) =
+ let (_,kinds,sp_projs,_) =
List.fold_left2
- (fun (nfi,sp_projs,subst) coe (fi,optci,ti) ->
- match fi with
- | Anonymous ->
- (nfi-1, None::sp_projs,NoProjection fi::subst)
- | Name fid ->
+ (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+ let (sp_projs,subst) =
+ match fi with
+ | Anonymous ->
+ (None::sp_projs,NoProjection fi::subst)
+ | Name fid ->
try
let ccl = subst_projection fid subst ti in
let body = match optci with
@@ -176,32 +159,34 @@ let declare_projections indsp coers fields =
it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
- let (sp,kn) =
+ let kn =
try
let cie = {
const_entry_body = proj;
const_entry_type = Some projtyp;
- const_entry_opaque = false } in
- let k = (DefinitionEntry cie,IsDefinition) in
- let sp = declare_internal_constant fid k in
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions() } in
+ let k = (DefinitionEntry cie,IsDefinition StructureComponent) in
+ let kn = declare_internal_constant fid k in
Options.if_verbose message (string_of_id fid ^" is defined");
- sp
+ kn
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
let refi = ConstRef kn in
let constr_fi = mkConst kn in
if coe then begin
- let cl = Class.class_of_ref (IndRef indsp) in
+ let cl = Class.class_of_global (IndRef indsp) in
Class.try_add_new_coercion_with_source refi Global cl
end;
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
let constr_fip = applist (constr_fi,proj_args) in
- (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst)
+ (Some kn::sp_projs, Projection constr_fip::subst)
with NotDefinable why ->
warning_or_error coe indsp why;
- (nfi-1, None::sp_projs,NoProjection fi::subst))
- (List.length fields,[],[]) coers (List.rev fields)
- in sp_projs
+ (None::sp_projs,NoProjection fi::subst) in
+ (nfi-1,(optci=None)::kinds,sp_projs,subst))
+ (List.length fields,[],[],[]) coers (List.rev fields)
+ 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 *)
@@ -220,18 +205,18 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
let ind = applist (mkRel (1+List.length params+List.length fields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let mie_ind =
- { mind_entry_params = List.map degenerate_decl params;
- mind_entry_typename = idstruc;
+ { mind_entry_typename = idstruc;
mind_entry_arity = mkSort s;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] } in
let mie =
- { mind_entry_record = true;
+ { mind_entry_params = List.map degenerate_decl params;
+ mind_entry_record = true;
mind_entry_finite = true;
mind_entry_inds = [mie_ind] } in
let sp = declare_mutual_with_eliminations true mie in
let rsp = (sp,0) in (* This is ind path of idstruc *)
- let sp_projs = declare_projections rsp coers fields in
+ 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.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
+ Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 8eff2ed5..66282c20 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,v 1.16.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: record.mli 6743 2005-02-18 22:14:08Z herbelin $ i*)
(*i*)
open Names
@@ -21,7 +21,7 @@ open Topconstr
[coers]; it returns the absolute names of projections *)
val declare_projections :
- inductive -> bool list -> rel_context -> constant option list
+ inductive -> bool list -> rel_context -> bool list * constant option list
val definition_structure :
lident with_coercion * local_binder list *
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
deleted file mode 100755
index d2a1e36e..00000000
--- a/toplevel/recordobj.ml
+++ /dev/null
@@ -1,77 +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: recordobj.ml,v 1.12.2.1 2004/07/16 19:31:49 herbelin Exp $ *)
-
-open Util
-open Pp
-open Names
-open Libnames
-open Nameops
-open Term
-open Instantiate
-open Lib
-open Declare
-open Recordops
-open Classops
-open Nametab
-
-(***** object definition ******)
-
-let typ_lams_of t =
- let rec aux acc c = match kind_of_term c with
- | Lambda (x,c1,c2) -> aux (c1::acc) c2
- | Cast (c,_) -> aux acc c
- | t -> acc,t
- in aux [] t
-
-let objdef_err ref =
- errorlabstrm "object_declare"
- (pr_id (id_of_global ref) ++
- str" is not a structure object")
-
-let objdef_declare ref =
- let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
- let env = Global.env () in
- let v = constr_of_reference ref in
- let vc = match Environ.constant_opt_value env sp with
- | Some vc -> vc
- | None -> objdef_err ref in
- let lt,t = decompose_lam vc in
- let lt = List.rev (List.map snd lt) in
- let f,args = match kind_of_term t with
- | App (f,args) -> f,args
- | _ -> objdef_err ref in
- let { s_PARAM = p; s_PROJ = lpj } =
- try (find_structure
- (match kind_of_term f with
- | Construct (indsp,1) -> indsp
- | _ -> objdef_err ref))
- with Not_found -> objdef_err ref in
- let params, projs =
- try list_chop p (Array.to_list args)
- with _ -> objdef_err ref in
- let lps =
- try List.combine lpj projs
- with _ -> objdef_err ref in
- let comp =
- List.fold_left
- (fun l (spopt,t) -> (* comp=components *)
- match spopt with
- | None -> l
- | Some proji_sp ->
- let c, args = decompose_app t in
- try (ConstRef proji_sp, reference_of_constr c, args) :: l
- with Not_found -> l)
- [] lps in
- add_anonymous_leaf (inObjDef1 sp);
- List.iter
- (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
- comp
-
-let add_object_hook _ = objdef_declare
diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli
index f1ad7d5a..184725b2 100644
--- a/toplevel/searchisos.mli
+++ b/toplevel/searchisos.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: searchisos.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: searchisos.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
val search_in_lib : bool ref
val type_search : Term.constr -> unit
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7fa80bcb..a5c2564c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml,v 1.22.2.2 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *)
open Pp
open Util
@@ -182,11 +182,44 @@ let make_prompt () =
with _ ->
"Coq < "
+(*let build_pending_list l =
+ let pl = ref ">" in
+ let l' = ref l in
+ let res =
+ while List.length !l' > 1 do
+ pl := !pl ^ "|" Names.string_of_id x;
+ l':=List.tl !l'
+ done in
+ let last = try List.hd !l' with _ -> in
+ "<"^l'
+*)
+
+(* the coq prompt added to the default one when in emacs mode
+ The prompt contains the current state label [n] (for global
+ backtracking) and the current proof state [p] (for proof
+ backtracking) plus the list of open (nested) proofs (for proof
+ aborting when backtracking). It looks like:
+
+ "n |lem1|lem2|lem3| p < "
+*)
+let make_emacs_prompt() =
+ let statnum = string_of_int (Lib.current_command_label ()) in
+ let endchar = String.make 1 (Char.chr 249) in
+ let dpth = Pfedit.current_proof_depth() in
+ let pending = Pfedit.get_all_proof_names() in
+ let pendingprompt =
+ List.fold_left
+ (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
+ "" pending in
+ let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
+ statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ endchar
+
(* A buffer to store the current command read on stdin. It is
* initialized when a vernac command is immediately followed by "\n",
* or after a Drop. *)
let top_buffer =
- let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
+ let pr() =
+ make_prompt() ^ Printer.emacs_str (make_emacs_prompt())
in
{ prompt = pr;
str = "";
@@ -197,7 +230,7 @@ let top_buffer =
let set_prompt prompt =
top_buffer.prompt
- <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249))))
+ <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249))))
(* Removes and prints the location of the error. The following exceptions
need not be located. *)
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 1b6b48d4..f4d2e28a 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: toplevel.mli,v 1.6.10.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: toplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index b00cfffc..354aff0b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: usage.ml,v 1.15.2.2 2004/09/03 14:35:26 herbelin Exp $ *)
+(* $Id: usage.ml 6053 2004-09-03 14:33:35Z herbelin $ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 16929d68..97814fd2 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: usage.mli,v 1.5.16.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: usage.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*s Prints the version number on the standard output and exits (with 0). *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a5716619..64d77b74 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernac.ml,v 1.59.2.3 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *)
(* Parsing of vernacular. *)
@@ -15,10 +15,9 @@ open Lexer
open Util
open Options
open System
-open Coqast
open Vernacexpr
open Vernacinterp
-open Ppvernacnew
+open Ppvernac
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
@@ -57,7 +56,7 @@ let real_error = function
the file we parse seems a bit risky to me. B.B. *)
let open_file_twice_if verbosely fname =
- let _,longfname = find_file_in_path (Library.get_load_path ()) fname in
+ let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
let in_chan = open_in longfname in
let verb_ch = if verbosely then Some (open_in longfname) else None in
let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -95,62 +94,18 @@ let parse_phrase (po, verbch) =
let just_parsing = ref false
let chan_translate = ref stdout
-let last_char = ref '\000'
-(* postprocessor to avoid lexical icompatibilities between V7 and V8.
- Ex: auto.(* comment *) or simpl.auto
- *)
let set_formatter_translator() =
let ch = !chan_translate in
- let out s b e =
- let n = e-b in
- if n > 0 then begin
- (match !last_char with
- '.' ->
- (match s.[b] with
- '('|'a'..'z'|'A'..'Z' -> output ch " " 0 1
- | _ -> ())
- | _ -> ());
- last_char := s.[e-1]
- end;
- output ch s b e
- in
+ let out s b e = output ch s b e in
Format.set_formatter_output_functions out (fun () -> flush ch);
Format.set_max_boxes max_int
-let pre_printing = function
- | VernacSolve (i,tac,deftac) when Options.do_translate () ->
- (try
- let (_,env) = Pfedit.get_goal_context i in
- let t = Options.with_option Options.translate_syntax
- (Tacinterp.glob_tactic_env [] env) tac in
- let pfts = Pfedit.get_pftreestate () in
- let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
- Some (env,t,Pfedit.focus(),List.length gls)
- with UserError _|Stdpp.Exc_located _ -> None)
- | _ -> None
-
-let post_printing loc (env,t,f,n) = function
- | VernacSolve (i,_,deftac) ->
- let loc = unloc loc in
- set_formatter_translator();
- let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
- (if !translate_file then begin
- msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1)));
- end
- else
- msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp)));
- Format.set_formatter_out_channel stdout
- | _ -> ()
-
let pr_new_syntax loc ocom =
let loc = unloc loc in
if !translate_file then set_formatter_translator();
let fs = States.freeze () in
let com = match ocom with
- | Some (VernacV7only _) ->
- Options.v7_only := true;
- mt()
| Some VernacNop -> mt()
| Some com -> pr_vernac com
| None -> mt() in
@@ -159,8 +114,6 @@ let pr_new_syntax loc ocom =
else
msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
- Constrintern.set_temporary_implicits_in [];
- Constrextern.set_temporary_implicits_out [];
Format.set_formatter_out_channel stdout
let rec vernac_com interpfun (loc,com) =
@@ -174,7 +127,7 @@ let rec vernac_com interpfun (loc,com) =
(* coqdoc state *)
let cds = Constrintern.coqdoc_freeze() in
if !Options.translate_file then begin
- let _,f = find_file_in_path (Library.get_load_path ())
+ let _,f = find_file_in_path (Library.get_load_paths ())
(make_suffix fname ".v") in
chan_translate := open_out (f^"8");
Pp.comments := []
@@ -203,39 +156,14 @@ let rec vernac_com interpfun (loc,com) =
msgnl (str"Finished transaction in " ++
System.fmt_time_difference tstart tend)
- (* To be interpreted in v7 or translator input only *)
- | VernacV7only v ->
- Options.v7_only := true;
- if !Options.v7 || Options.do_translate() then interp v;
- Options.v7_only := false
-
- (* To be interpreted in translator output only *)
- | VernacV8only v ->
- if not !Options.v7 && not (do_translate()) then
- interp v
-
| v -> if not !just_parsing then interpfun v
in
try
- Options.v7_only := false;
- if do_translate () then
- match pre_printing com with
- None ->
- pr_new_syntax loc (Some com);
- interp com
- | Some state ->
- (try
- interp com;
- post_printing loc state com
- with e ->
- post_printing loc state com;
- raise e)
- else
- interp com
+ if do_translate () then pr_new_syntax loc (Some com);
+ interp com
with e ->
Format.set_formatter_out_channel stdout;
- Options.v7_only := false;
raise (DuringCommandInterp (loc, e))
and vernac interpfun input =
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d8f4b247..4f95376f 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernac.mli,v 1.10.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernac.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1c6ad9a6..7394bd8f 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,v 1.195.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacentries.ml 8700 2006-04-11 23:14:15Z courtieu $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -23,6 +23,7 @@ open Proof_trees
open Constrintern
open Prettyp
open Printer
+open Tactic_printer
open Tacinterp
open Command
open Goptions
@@ -32,6 +33,7 @@ open Vernacexpr
open Decl_kinds
open Topconstr
open Pretyping
+open Redexpr
(* Pcoq hooks *)
@@ -55,14 +57,13 @@ let set_pcoq_hook f = pcoq := Some f
let cl_of_qualid = function
| FunClass -> Classops.CL_FUN
| SortClass -> Classops.CL_SORT
- | RefClass r -> Class.class_of_ref (Nametab.global r)
+ | RefClass r -> Class.class_of_global (Nametab.global r)
(*******************)
(* "Show" commands *)
let show_proof () =
let pts = get_pftreestate () in
- let pf = proof_of_pftreestate pts in
let cursor = cursor_of_pftreestate pts in
let evc = evc_of_pftreestate pts in
let (pfterm,meta_types) = extract_open_pftreestate pts in
@@ -70,41 +71,41 @@ let show_proof () =
prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
str"Subgoals" ++ fnl () ++
prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++
- prtype ty ++ fnl ())
+ pr_ltype ty ++ fnl ())
meta_types
- ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm))
+ ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm))
let show_node () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and cursor = cursor_of_pftreestate pts in
msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
- prgl (goal_of_proof pf) ++ fnl () ++
+ pr_goal (goal_of_proof pf) ++ fnl () ++
(match pf.Proof_type.ref with
| None -> (str"BY <rule>")
| Some(r,spfl) ->
- (str"BY " ++ Refiner.pr_rule r ++ fnl () ++
+ (str"BY " ++ pr_rule r ++ fnl () ++
str" " ++
- hov 0 (prlist_with_sep pr_fnl prgl
+ hov 0 (prlist_with_sep pr_fnl pr_goal
(List.map goal_of_proof spfl)))))
let show_script () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msgnl (Refiner.print_treescript true evc (Global.named_context()) pf)
+ msgnl (print_treescript true evc (Global.named_context()) pf)
let show_top_evars () =
let pfts = get_pftreestate () in
let gls = top_goal_of_pftreestate pfts in
let sigma = project gls in
- msg (pr_evars_int 1 (Evd.non_instantiated sigma))
+ msg (pr_evars_int 1 (Evarutil.non_instantiated sigma))
let show_prooftree () =
let pts = get_pftreestate () in
let pf = proof_of_pftreestate pts
and evc = evc_of_pftreestate pts in
- msg (Refiner.print_proof evc (Global.named_context()) pf)
+ msg (print_proof evc (Global.named_context()) pf)
let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
@@ -112,7 +113,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
let fresh_id_of_name avoid gl = function
Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
- | Name id -> id
+ | Name id -> Tactics.fresh_id avoid id gl
let rec do_renum avoid gl = function
[] -> mt ()
@@ -121,27 +122,83 @@ let rec do_renum avoid gl = function
let id = fresh_id_of_name avoid gl n in
pr_id id ++ spc () ++ do_renum (id :: avoid) gl l
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+ ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *)
+let decompose_prod_letins =
+ let rec prodec_rec l c = match kind_of_term c with
+ | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
+ | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c
+ | Cast (c,_,_) -> prodec_rec l c
+ | _ -> l,c
+ in
+ prodec_rec []
+
let show_intro all =
let pf = get_pftreestate() in
let gl = nth_goal_of_pftreestate 1 pf in
- let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
+ let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in
let nl = List.rev_map fst l in
- if all then
- msgnl (do_renum [] gl nl)
- else
- try
- let n = List.hd nl in
- msgnl (pr_id (fresh_id_of_name [] gl n))
- with Failure "hd" -> message ""
+ if all then msgnl (hov 0 (do_renum [] gl nl))
+ else try
+ let n = List.hd nl in
+ msgnl (pr_id (fresh_id_of_name [] gl n))
+ with Failure "hd" -> message ""
+
+
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
+ | Names.Name x -> x
+
+
+(* Building of match expression *)
+(* From ide/coq.ml *)
+let make_cases s =
+ let qualified_name = Libnames.qualid_of_string s in
+ let glob_ref = Nametab.locate qualified_name in
+ match glob_ref with
+ | Libnames.IndRef i ->
+ let {Declarations.mind_nparams = np}
+ , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr }
+ = Global.lookup_inductive i in
+ Util.array_fold_right2
+ (fun n t l ->
+ let (al,_) = Term.decompose_prod t in
+ let al,_ = Util.list_chop (List.length al - np) al in
+ let rec rename avoid = function
+ | [] -> []
+ | (n,_)::l ->
+ let n' = Termops.next_global_ident_away true (id_of_name n) avoid in
+ string_of_id n' :: rename (n'::avoid) l in
+ let al' = rename [] (List.rev al) in
+ (string_of_id n :: al') :: l)
+ carr tarr []
+ | _ -> raise Not_found
+
+
+let show_match id =
+ try
+ let s = string_of_id (snd id) in
+ let patterns = make_cases s in
+ let cases =
+ List.fold_left
+ (fun acc x ->
+ match x with
+ | [] -> assert false
+ | [x] -> "| "^ x ^ " => \n" ^ acc
+ | x::l ->
+ "| (" ^ List.fold_left (fun acc s -> acc ^ " " ^ s) x l ^ ")"
+ ^ " => \n" ^ acc)
+ "end" patterns in
+ msg (str ("match # with\n" ^ cases))
+ 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))
let print_loadpath () =
- let l = Library.get_full_load_path () in
+ let l = Library.get_full_load_paths () in
msgnl (Pp.t (str "Physical path: " ++
tab () ++ str "Logical Path:" ++ fnl () ++
prlist_with_sep pr_fnl print_path_entry l))
@@ -190,8 +247,7 @@ let dump_universes s =
let locate_file f =
try
- let _,file =
- System.where_in_path (Library.get_load_path()) f in
+ let _,file = System.where_in_path (Library.get_load_paths ()) f in
msgnl (str file)
with Not_found ->
msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -219,13 +275,22 @@ let print_located_library r =
try msg_found_library (Library.locate_qualified_library qid)
with e -> msg_notfound_library loc qid e
+let print_located_module r =
+ let (loc,qid) = qualid_of_reference r in
+ let msg =
+ try
+ let dir = Nametab.full_name_module qid in
+ str "Module " ++ pr_dirpath dir
+ with Not_found ->
+ (if fst (repr_qualid qid) = empty_dirpath then
+ str "No module is referred to by basename "
+ else
+ str "No module is referred to by name ") ++ pr_qualid qid
+ in msgnl msg
+
(**********)
(* Syntax *)
-let vernac_syntax = Metasyntax.add_syntax_obj
-
-let vernac_grammar = Metasyntax.add_grammar_obj
-
let vernac_syntax_extension = Metasyntax.add_syntax_extension
let vernac_delimiters = Metasyntax.add_delimiters
@@ -233,15 +298,13 @@ let vernac_delimiters = Metasyntax.add_delimiters
let vernac_bind_scope sc cll =
List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll
-let vernac_open_close_scope = Symbols.open_close_scope
+let vernac_open_close_scope = Notation.open_close_scope
let vernac_arguments_scope qid scl =
- Symbols.declare_arguments_scope (global qid) scl
+ Notation.declare_arguments_scope (global qid) scl
let vernac_infix = Metasyntax.add_infix
-let vernac_distfix = Metasyntax.add_distfix
-
let vernac_notation = Metasyntax.add_notation
(***********)
@@ -252,7 +315,7 @@ let start_proof_and_print idopt k t hook =
print_subgoals ();
if !pcoq <> None then (out_some !pcoq).start_proof ()
-let vernac_definition (local,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) id def hook =
match def with
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
@@ -260,8 +323,7 @@ let vernac_definition (local,_ as k) id def hook =
(str "Proof editing mode not supported in module types")
else
let hook _ _ = () in
- let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in
- start_proof_and_print (Some id) kind (bl,t) hook
+ start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -278,7 +340,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
if Lib.is_modtype () then
errorlabstrm "Vernacentries.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
+ start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
let vernac_end_proof = function
| Admitted -> admit ()
@@ -293,9 +355,15 @@ let vernac_end_proof = function
the theories [??] *)
let vernac_exact_proof c =
- by (Tactics.exact_proof c);
- save_named true
-
+ let pfs = top_of_tree (get_pftreestate()) in
+ let pf = proof_of_pftreestate pfs in
+ if (is_leaf_proof pf) then begin
+ by (Tactics.exact_proof c);
+ save_named true end
+ else
+ errorlabstrm "Vernacentries.ExactProof"
+ (str "Command 'Proof ...' can only be used at the beginning of the proof")
+
let vernac_assumption kind l =
List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
@@ -310,107 +378,70 @@ let vernac_scheme = build_scheme
(**********************)
(* Modules *)
-let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =
+let vernac_import export refl =
+ let import ref = Library.import_module export (qualid_of_reference ref) in
+ List.iter import refl;
+ Lib.add_frozen_state ()
+
+let vernac_declare_module export 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";
-
- if not (Lib.is_modtype ()) then
- error "Declare Module allowed in module types only";
-
- let constrain_mty = match mty_ast_o with
- Some (_,true) -> true
- | _ -> false
- in
-
- match mty_ast_o, constrain_mty, mexpr_ast_o with
- | _, false, None -> (* no ident, no/soft type *)
- Declaremods.start_module Modintern.interp_modtype
- id binders_ast mty_ast_o;
- if_verbose message
- ("Interactive Declaration of Module "^ string_of_id id ^" started")
-
- | Some _, true, None (* no ident, hard type *)
- | _, false, Some (CMEident _) -> (* ident, no/soft type *)
- Declaremods.declare_module
- Modintern.interp_modtype Modintern.interp_modexpr
- id binders_ast mty_ast_o mexpr_ast_o;
- if_verbose message
- ("Module "^ string_of_id id ^" is declared")
-
- | _, true, Some (CMEident _) -> (* ident, hard type *)
- error "You cannot declare an equality and a type in module declaration"
-
- | _, _, Some _ -> (* not ident *)
- error "Only simple modules allowed in module declarations"
-
- | None,true,None -> assert false (* 1st None ==> false *)
-
-let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o =
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor declaration cannot be exported. " ^
+ "Remove the \"Export\" and \"Import\" keywords from every functor " ^
+ "argument.")
+ else (idl,ty)) binders_ast in
+ Declaremods.declare_module
+ Modintern.interp_modtype Modintern.interp_modexpr
+ id binders_ast (Some mty_ast_o) None;
+ if_verbose message ("Module "^ string_of_id id ^" is declared");
+ option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+
+let vernac_define_module export 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";
-
- if Lib.is_modtype () then
- error "Module definitions not allowed in module types. Use Declare Module instead";
-
match mexpr_ast_o with
| None ->
- Declaremods.start_module Modintern.interp_modtype
+ let binders_ast,argsexport =
+ List.fold_right
+ (fun (export,idl,ty) (args,argsexport) ->
+ (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+ ([],[]) in
+ Declaremods.start_module Modintern.interp_modtype export
id binders_ast mty_ast_o;
if_verbose message
- ("Interactive Module "^ string_of_id id ^" started")
-
+ ("Interactive Module "^ string_of_id id ^" started") ;
+ List.iter
+ (fun (export,id) ->
+ option_iter
+ (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ ) argsexport
| Some _ ->
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor definition can be imported only if" ^
+ " the definition is interactive. Remove the \"Export\" and " ^
+ "\"Import\" keywords from every functor argument.")
+ else (idl,ty)) binders_ast in
Declaremods.declare_module
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast mty_ast_o mexpr_ast_o;
if_verbose message
- ("Module "^ string_of_id id ^" is defined")
-
-(* let vernac_declare_module 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"; *)
-
-(* let constrain_mty = match mty_ast_o with *)
-(* Some (_,true) -> true *)
-(* | _ -> false *)
-(* in *)
-
-(* match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *)
-(* | _, None, _, None *)
-(* | true, Some _, false, None *)
-(* | false, _, _, None -> *)
-(* Declaremods.start_module Modintern.interp_modtype *)
-(* id binders_ast mty_ast_o; *)
-(* if_verbose message *)
-(* ("Interactive Module "^ string_of_id id ^" started") *)
-
-(* | true, Some _, true, None *)
-(* | true, _, false, Some (CMEident _) *)
-(* | false, _, _, Some _ -> *)
-(* Declaremods.declare_module *)
-(* Modintern.interp_modtype Modintern.interp_modexpr *)
-(* id binders_ast mty_ast_o mexpr_ast_o; *)
-(* if_verbose message *)
-(* ("Module "^ string_of_id id ^" is defined") *)
-
-(* | true, _, _, _ -> *)
-(* error "Module definition not allowed in a Module Type" *)
-
-let vernac_end_module id =
- Declaremods.end_module id;
- if_verbose message
- (if Lib.is_modtype () then
- "Module "^ string_of_id id ^" is declared"
- else
- "Module "^ string_of_id id ^" is defined")
+ ("Module "^ string_of_id id ^" is defined");
+ option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+ export
-
+let vernac_end_module export id =
+ Declaremods.end_module id;
+ if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+ option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_declare_module_type id binders_ast mty_ast_o =
@@ -419,11 +450,28 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
match mty_ast_o with
| None ->
+ let binders_ast,argsexport =
+ List.fold_right
+ (fun (export,idl,ty) (args,argsexport) ->
+ (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+ ([],[]) in
Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
if_verbose message
- ("Interactive Module Type "^ string_of_id id ^" started")
+ ("Interactive Module Type "^ string_of_id id ^" started");
+ List.iter
+ (fun (export,id) ->
+ option_iter
+ (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ ) argsexport
| Some base_mty ->
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor definition can be imported only if" ^
+ " the definition is interactive. Remove the \"Export\" " ^
+ "and \"Import\" keywords from every functor argument.")
+ else (idl,ty)) binders_ast in
Declaremods.declare_modtype Modintern.interp_modtype
id binders_ast base_mty;
if_verbose message
@@ -455,86 +503,26 @@ let vernac_record struc binders sort nameopt cfs =
(* Sections *)
-let vernac_begin_section id = let _ = Lib.open_section id in ()
-
-let vernac_end_section id =
- Discharge.close_section (is_verbose ()) id
-
+let vernac_begin_section = Lib.open_section
+let vernac_end_section = Lib.close_section
let vernac_end_segment id =
check_no_pending_proofs ();
- try
- match Lib.what_is_opened () with
- | _,Lib.OpenedModule _ -> vernac_end_module id
- | _,Lib.OpenedModtype _ -> vernac_end_modtype id
- | _,Lib.OpenedSection _ -> vernac_end_section id
- | _ -> anomaly "No more opened things"
- with
- Not_found -> error "There is nothing to end."
-
-let is_obsolete_module (_,qid) =
- match repr_qualid qid with
- | dir, id when dir = empty_dirpath ->
- (match string_of_id id with
- | ("Refine" | "Inv" | "Equality" | "EAuto" | "AutoRewrite"
- | "EqDecide" | "Xml" | "Extraction" | "Tauto" | "Setoid_replace"
- | "Elimdep"
- | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax"
- | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax" | "PolyListSyntax")
- -> true
- | _ -> false)
- | _ -> false
-
-let test_renamed_module (_,qid) =
- match repr_qualid qid with
- | dir, id when dir = empty_dirpath ->
- (match string_of_id id with
- | "List" -> warning "List has been renamed into MonoList"
- | "PolyList" -> warning "PolyList has been renamed into List and old List into MonoList"
- | _ -> ())
- | _ -> ()
-
+ let o =
+ try Lib.what_is_opened ()
+ with Not_found -> error "There is nothing to end." in
+ match o with
+ | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
+ | _,Lib.OpenedModtype _ -> vernac_end_modtype id
+ | _,Lib.OpenedSection _ -> vernac_end_section id
+ | _ -> anomaly "No more opened things"
+
let vernac_require import _ qidl =
let qidl = List.map qualid_of_reference qidl in
- try
- match import with
- | None -> List.iter Library.read_library qidl
- | Some b -> Library.require_library None qidl b
- with e ->
- (* Compatibility message *)
- let qidl' = List.filter is_obsolete_module qidl in
- if qidl' = qidl then
- List.iter
- (fun (_,qid) ->
- warning ("Module "^(string_of_qualid qid)^
- " is now built-in and shouldn't be required")) qidl
- else
- (if not !Options.v7 then List.iter test_renamed_module qidl;
- raise e)
-
-let vernac_import export refl =
- let import_one ref =
- let qid = qualid_of_reference ref in
- Library.import_library export qid
- in
- List.iter import_one refl;
- Lib.add_frozen_state ()
-
-(* else
- let import (loc,qid) =
- try
- let mp = Nametab.locate_module qid in
- Declaremods.import_module mp
- with Not_found ->
- user_err_loc
- (loc,"vernac_import",
- str ((string_of_qualid qid)^" is not a module"))
- in
- List.iter import qidl;
-*)
+ Library.require_library qidl import
let vernac_canonical locqid =
- Recordobj.objdef_declare (Nametab.global locqid)
+ Recordops.declare_canonical_structure (Nametab.global locqid)
let locate_reference ref =
let (loc,qid) = qualid_of_reference ref in
@@ -591,18 +579,14 @@ 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";
- if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
-(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
-
-
+ 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*)
+
(*****************************)
(* Auxiliary file management *)
let vernac_require_from export spec filename =
- match export with
- Some exp ->
- Library.require_library_from_file spec None filename exp
- | None -> Library.read_library_from_file filename
+ Library.require_library_from_file None filename export
let vernac_add_loadpath isrec pdir ldiropt =
let alias = match ldiropt with
@@ -610,7 +594,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
| Some ldir -> ldir in
(if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
-let vernac_remove_loadpath = Library.remove_path
+let vernac_remove_loadpath = Library.remove_load_path
(* Coq syntax for ML or system commands *)
@@ -651,7 +635,9 @@ let vernac_reset_initial () = abort_refine Lib.reset_initial ()
let vernac_back n = Lib.back n
+let vernac_backto n = Lib.reset_label n
+(* see also [vernac_backtrack] which combines undoing and resetting *)
(************)
(* Commands *)
@@ -667,7 +653,7 @@ let vernac_declare_implicits locqid = function
let vernac_reserve idl c =
let t = Constrintern.interp_type Evd.empty (Global.env()) c in
- let t = Detyping.detype (false,Global.env()) [] [] t in
+ let t = Detyping.detype false [] [] t in
List.iter (fun id -> Reserve.declare_reserved_type id t) idl
let make_silent_if_not_pcoq b =
@@ -691,13 +677,11 @@ let _ =
optread = Impargs.is_implicit_args;
optwrite = Impargs.make_implicit_args }
-let impargs = if !Options.v7 then "Implicits" else "Implicit"
-
let _ =
declare_bool_option
- { optsync = false; (* synchronisation is in Impargs *)
+ { optsync = true;
optname = "strict implicit arguments";
- optkey = (SecondaryTable ("Strict",impargs));
+ optkey = (SecondaryTable ("Strict","Implicit"));
optread = Impargs.is_strict_implicit_args;
optwrite = Impargs.make_strict_implicit_args }
@@ -705,7 +689,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "contextual implicit arguments";
- optkey = (SecondaryTable ("Contextual",impargs));
+ optkey = (SecondaryTable ("Contextual","Implicit"));
optread = Impargs.is_contextual_implicit_args;
optwrite = Impargs.make_contextual_implicit_args }
@@ -721,7 +705,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "implicit arguments printing";
- optkey = (SecondaryTable ("Printing",impargs));
+ optkey = (SecondaryTable ("Printing","Implicit"));
optread = (fun () -> !Constrextern.print_implicits);
optwrite = (fun b -> Constrextern.print_implicits := b) }
@@ -737,7 +721,7 @@ let _ =
declare_bool_option
{ optsync = true;
optname = "notations printing";
- optkey = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
+ optkey = (SecondaryTable ("Printing","Notations"));
optread = (fun () -> not !Constrextern.print_no_symbol);
optwrite = (fun b -> Constrextern.print_no_symbol := not b) }
@@ -750,6 +734,30 @@ let _ =
optwrite = (fun b -> Options.raw_print := b) }
let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of virtual machine inside the kernel";
+ optkey = (SecondaryTable ("Virtual","Machine"));
+ optread = (fun () -> Vconv.use_vm ());
+ optwrite = (fun b -> Vconv.set_use_vm b) }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of boxed definitions";
+ optkey = (SecondaryTable ("Boxed","Definitions"));
+ optread = Options.boxed_definitions;
+ optwrite = (fun b -> Options.set_boxed_definitions b) }
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optname = "use of boxed values";
+ optkey = (SecondaryTable ("Boxed","Values"));
+ optread = (fun _ -> not (Vm.transp_values ()));
+ optwrite = (fun b -> Vm.set_transp_values (not b)) }
+
+let _ =
declare_int_option
{ optsync=false;
optkey=PrimaryTable("Undo");
@@ -784,11 +792,11 @@ let _ =
let vernac_set_opacity opaq locqid =
match Nametab.global locqid with
| ConstRef sp ->
- if opaq then Tacred.set_opaque_const sp
- else Tacred.set_transparent_const sp
+ if opaq then set_opaque_const sp
+ else set_transparent_const sp
| VarRef id ->
- if opaq then Tacred.set_opaque_var id
- else Tacred.set_transparent_var id
+ if opaq then set_opaque_var id
+ else set_transparent_var id
| _ -> error "cannot set an inductive type or a constructor as transparent"
let vernac_set_option key = function
@@ -843,7 +851,7 @@ let vernac_check_may_eval redexp glopt rc =
if !pcoq <> None then (out_some !pcoq).print_check j
else msg (print_judgment env j)
| Some r ->
- let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in
+ let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
if !pcoq <> None
then (out_some !pcoq).print_eval (redfun env evmap) env rc j
else msg (print_eval redfun env j)
@@ -859,7 +867,6 @@ let vernac_global_check c =
let vernac_print = function
| PrintTables -> print_tables ()
- | PrintLocalContext -> msg (print_local_context ())
| PrintFullContext -> msg (print_full_context_typ ())
| PrintSectionContext qid -> msg (print_sec_context_typ qid)
| PrintInspect n -> msg (inspect n)
@@ -876,21 +883,25 @@ let vernac_print = function
| PrintOpaqueName qid -> msg (print_opaque_name qid)
| PrintGraph -> ppnl (Prettyp.print_graph())
| PrintClasses -> ppnl (Prettyp.print_classes())
+ | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
| PrintCoercions -> ppnl (Prettyp.print_coercions())
| PrintCoercionPaths (cls,clt) ->
ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+ | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
| PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
| PrintUniverses (Some s) -> dump_universes s
| PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
| PrintHintGoal -> Auto.print_applicable_hint ()
| PrintHintDbName s -> Auto.print_hint_db_by_name s
+ | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
| PrintHintDb -> Auto.print_searchtable ()
+ | PrintSetoids -> Setoid_replace.print_setoids()
| PrintScopes ->
- pp (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm))
+ pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
| PrintScope s ->
- pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
+ pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s)
| PrintVisibility s ->
- pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
+ pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
| PrintAbout qid -> msgnl (print_about qid)
| PrintImplicit qid -> msg (print_impargs qid)
@@ -929,10 +940,11 @@ let vernac_search s r =
let vernac_locate = function
| LocateTerm qid -> msgnl (print_located_qualid qid)
| LocateLibrary qid -> print_located_library qid
+ | LocateModule qid -> print_located_module qid
| LocateFile f -> locate_file f
| LocateNotation ntn ->
- ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm)
- (Metasyntax.standardise_locatable_notation ntn))
+ ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr)
+ (Metasyntax.standardize_locatable_notation ntn))
(********************)
(* Proof management *)
@@ -942,7 +954,7 @@ let vernac_goal = function
| Some c ->
if not (refining()) then begin
let unnamed_kind = Lemma (* Arbitrary *) in
- start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->());
+ start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
print_subgoals ()
end else
error "repeated Goal not permitted in refining mode"
@@ -979,6 +991,17 @@ let vernac_undo n =
undo n;
print_subgoals ()
+(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
+ back-to state number [snum]. This allows to backtrack proofs and
+ state with one command (easier for proofgeneral). *)
+let vernac_backtrack snum pnum naborts =
+ for i = 1 to naborts do vernac_abort None done;
+ undo_todepth pnum;
+ vernac_backto snum;
+ (* there may be no proof in progress, even if no abort *)
+ (try print_subgoals () with UserError _ -> ())
+
+
(* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *)
let vernac_focus = function
| None -> traverse_nth_goal 1; print_subgoals ()
@@ -1005,10 +1028,10 @@ let apply_subproof f occ =
f evc (Global.named_context()) pf
let explain_proof occ =
- msg (apply_subproof (Refiner.print_treescript true) occ)
+ msg (apply_subproof (print_treescript true) occ)
let explain_tree occ =
- msg (apply_subproof Refiner.print_proof occ)
+ msg (apply_subproof print_proof occ)
let vernac_show = function
| ShowGoal nopt ->
@@ -1028,17 +1051,17 @@ let vernac_show = function
| ShowProofNames ->
msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
| ShowIntros all -> show_intro all
+ | ShowMatch id -> show_match id
| ExplainProof occ -> explain_proof occ
| ExplainTree occ -> explain_tree occ
let vernac_check_guard () =
let pts = get_pftreestate () in
- let pf = proof_of_pftreestate pts
- and cursor = cursor_of_pftreestate pts in
+ let pf = proof_of_pftreestate pts in
let (pfterm,_) = extract_open_pftreestate pts in
let message =
try
- Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf))
+ Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf))
pfterm;
(str "The condition holds up to here")
with UserError(_,s) ->
@@ -1049,100 +1072,19 @@ let vernac_check_guard () =
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-
-(**************************)
-(* Not supported commands *)
-(***
-let _ =
- add "ResetSection"
- (function
- | [VARG_IDENTIFIER id] ->
- (fun () -> reset_section (string_of_id id))
- | _ -> bad_vernac_args "ResetSection")
-
-(* Modules *)
-
-let _ =
- vinterp_add "BeginModule"
- (function
- | [VARG_IDENTIFIER id] ->
- let s = string_of_id id in
- let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in
- let dir = extend_dirpath (Library.find_logical_path lpe) id in
- fun () ->
- Lib.start_module dir
- | _ -> bad_vernac_args "BeginModule")
-
-let _ =
- vinterp_add "WriteModule"
- (function
- | [VARG_IDENTIFIER id] ->
- let mid = Lib.end_module id in
- fun () -> let m = string_of_id id in Library.save_module_to mid m
- | [VARG_IDENTIFIER id; VARG_STRING f] ->
- let mid = Lib.end_module id in
- fun () -> Library.save_module_to mid f
- | _ -> bad_vernac_args "WriteModule")
-
-let _ =
- vinterp_add "CLASS"
- (function
- | [VARG_STRING kind; VARG_QUALID qid] ->
- let stre =
- if kind = "LOCAL" then
- make_strength_0()
- else
- Nametab.NeverDischarge
- in
- fun () ->
- let ref = Nametab.global (dummy_loc, qid) in
- Class.try_add_new_class ref stre;
- if_verbose message
- ((string_of_qualid qid) ^ " is now a class")
- | _ -> bad_vernac_args "CLASS")
-
-(* Meta-syntax commands *)
-let _ =
- add "TOKEN"
- (function
- | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s)
- | _ -> bad_vernac_args "TOKEN")
-***)
-
-(* Search commands *)
-
-(***
-let _ =
- add "Searchisos"
- (function
- | [VARG_CONSTR com] ->
- (fun () ->
- let env = Global.env() in
- let c = constr_of_com Evd.empty env com in
- let cc = nf_betaiota env Evd.empty c in
- Searchisos.type_search cc)
- | _ -> bad_vernac_args "Searchisos")
-***)
-
let interp c = match c with
(* Control (done in vernac) *)
| (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false
- | (VernacV7only _ | VernacV8only _) -> assert false
(* Syntax *)
- | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
- | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
- | VernacGrammar (univ,al) -> vernac_grammar univ al
- | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
+ | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+ | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
| VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
| VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
| VernacOpenCloseScope sc -> vernac_open_close_scope sc
| VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
- | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
- | VernacDistfix (local,assoc,n,inf,qid,sc) ->
- vernac_distfix local assoc n inf qid sc
- | VernacNotation (local,c,infpl,mv8,sc) ->
- vernac_notation local c infpl mv8 sc
+ | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
+ | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
(* Gallina *)
| VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
@@ -1152,15 +1094,15 @@ let interp c = match c with
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,l) -> vernac_assumption stre l
| VernacInductive (finite,l) -> vernac_inductive finite l
- | VernacFixpoint l -> vernac_fixpoint l
- | VernacCoFixpoint l -> vernac_cofixpoint l
+ | VernacFixpoint (l,b) -> vernac_fixpoint l b
+ | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
| VernacScheme l -> vernac_scheme l
(* Modules *)
- | VernacDeclareModule ((_,id),bl,mtyo,mexpro) ->
- vernac_declare_module id bl mtyo mexpro
- | VernacDefineModule ((_,id),bl,mtyo,mexpro) ->
- vernac_define_module id bl mtyo mexpro
+ | VernacDeclareModule (export,(_,id),bl,mtyo) ->
+ vernac_declare_module export id bl mtyo
+ | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) ->
+ vernac_define_module export id bl mtyo mexpro
| VernacDeclareModuleType ((_,id),bl,mtyo) ->
vernac_declare_module_type id bl mtyo
@@ -1196,6 +1138,7 @@ let interp c = match c with
| VernacResetName id -> vernac_reset_name id
| VernacResetInitial -> vernac_reset_initial ()
| VernacBack n -> vernac_back n
+ | VernacBackTo n -> vernac_backto n
(* Commands *)
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
@@ -1226,6 +1169,7 @@ let interp c = match c with
| VernacSuspend -> vernac_suspend ()
| VernacResume id -> vernac_resume id
| VernacUndo n -> vernac_undo n
+ | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
| VernacFocus n -> vernac_focus n
| VernacUnfocus -> vernac_unfocus ()
| VernacGo g -> vernac_go g
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 89e0d708..a2bcd990 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.mli,v 1.16.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
+(*i $Id: vernacentries.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 382434dc..a00901a4 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,v 1.55.2.2 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: vernacexpr.ml 7936 2006-01-28 18:36:54Z herbelin $ i*)
open Util
open Names
@@ -34,7 +34,6 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference
type printable =
| PrintTables
- | PrintLocalContext
| PrintFullContext
| PrintSectionContext of reference
| PrintInspect of int
@@ -49,13 +48,17 @@ type printable =
| PrintOpaqueName of reference
| PrintGraph
| PrintClasses
+ | PrintLtac of reference
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
+ | PrintCanonicalConversions
| PrintUniverses of string option
| PrintHint of reference
| PrintHintGoal
| PrintHintDbName of string
+ | PrintRewriteHintDbName of string
| PrintHintDb
+ | PrintSetoids
| PrintScopes
| PrintScope of string
| PrintVisibility of string option
@@ -75,6 +78,7 @@ type searchable =
type locatable =
| LocateTerm of reference
| LocateLibrary of reference
+ | LocateModule of reference
| LocateFile of string
| LocateNotation of notation
@@ -94,6 +98,7 @@ type showable =
| ShowTree
| ShowProofNames
| ShowIntros of bool
+ | ShowMatch of lident
| ExplainProof of int list
| ExplainTree of int list
@@ -103,11 +108,11 @@ type comment =
| CommentInt of int
type hints =
- | HintsResolve of (identifier option * constr_expr) list
- | HintsImmediate of (identifier option * constr_expr) list
- | HintsUnfold of (identifier option * reference) list
- | HintsConstructors of identifier option * reference list
- | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr
+ | HintsResolve of constr_expr list
+ | HintsImmediate of constr_expr list
+ | HintsUnfold of reference list
+ | HintsConstructors of reference list
+ | HintsExtern of int * constr_expr * raw_tactic_expr
| HintsDestruct of identifier *
int * (bool,unit) location * constr_expr * raw_tactic_expr
@@ -152,7 +157,11 @@ type local_decl_expr =
| AssumExpr of lname * constr_expr
| DefExpr of lname * constr_expr * constr_expr option
-type module_binder = lident list * module_type_ast
+type module_binder = bool option * lident list * module_type_ast
+
+type grammar_production =
+ | VTerm of string
+ | VNonTerm of loc * string * Names.identifier option
type proof_end =
| Admitted
@@ -166,25 +175,17 @@ type vernac_expr =
| VernacVar of lident
(* Syntax *)
- | VernacGrammar of lstring * raw_grammar_entry list
- | VernacTacticGrammar of
- (lstring * (lstring * grammar_production list) * raw_tactic_expr) list
- | VernacSyntax of lstring * raw_syntax_entry list
- | VernacSyntaxExtension of locality_flag *
- (lstring * syntax_modifier list) option
- * (lstring * syntax_modifier list) option
- | VernacDistfix of locality_flag *
- grammar_associativity * precedence * lstring * lreference *
- scope_name option
+ | VernacTacticNotation of int * grammar_production list * raw_tactic_expr
+ | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
| VernacOpenCloseScope of (locality_flag * bool * scope_name)
| VernacDelimiters of scope_name * lstring
| VernacBindScope of scope_name * class_rawexpr list
| VernacArgumentsScope of lreference * scope_name option list
| VernacInfix of locality_flag * (lstring * syntax_modifier list) *
- lreference * (lstring * syntax_modifier list) option * scope_name option
+ lreference * scope_name option
| VernacNotation of
- locality_flag * constr_expr * (lstring * syntax_modifier list) option *
- (lstring * syntax_modifier list) option * scope_name option
+ locality_flag * constr_expr * (lstring * syntax_modifier list) *
+ scope_name option
(* Gallina *)
| VernacDefinition of definition_kind * lident * definition_expr *
@@ -195,8 +196,8 @@ type vernac_expr =
| VernacExactProof of constr_expr
| VernacAssumption of assumption_kind * simple_binder with_coercion list
| VernacInductive of inductive_flag * inductive_expr list
- | VernacFixpoint of (fixpoint_expr * decl_notation) list
- | VernacCoFixpoint of cofixpoint_expr list
+ | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
+ | VernacCoFixpoint of cofixpoint_expr list * bool
| VernacScheme of (lident * bool * lreference * sort_expr) list
(* Gallina extensions *)
@@ -214,9 +215,9 @@ type vernac_expr =
class_rawexpr * class_rawexpr
(* Modules and Module Types *)
- | VernacDeclareModule of lident *
- module_binder list * (module_type_ast * bool) option * module_ast option
- | VernacDefineModule of lident *
+ | VernacDeclareModule of bool option * lident *
+ module_binder list * (module_type_ast * bool)
+ | VernacDefineModule of bool option * lident *
module_binder list * (module_type_ast * bool) option * module_ast option
| VernacDeclareModuleType of lident *
module_binder list * module_type_ast option
@@ -241,6 +242,7 @@ type vernac_expr =
| VernacResetName of lident
| VernacResetInitial
| VernacBack of int
+ | VernacBackTo of int
(* Commands *)
| VernacDeclareTacticDefinition of
@@ -273,6 +275,7 @@ type vernac_expr =
| VernacSuspend
| VernacResume of lident option
| VernacUndo of int
+ | VernacBacktrack of int*int*int
| VernacFocus of int option
| VernacUnfocus
| VernacGo of goable
@@ -283,10 +286,6 @@ type vernac_expr =
(* Toplevel control *)
| VernacToplevelControl of exn
- (* For translation from V7 to V8 syntax *)
- | VernacV8only of vernac_expr
- | VernacV7only of vernac_expr
-
(* For extension *)
| VernacExtend of string * raw_generic_argument list
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index c7846d71..98584bac 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: vernacinterp.ml,v 1.17.8.1 2004/07/16 19:31:50 herbelin Exp $ *)
+(* $Id: vernacinterp.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
open Pp
open Util
@@ -15,10 +15,7 @@ open Libnames
open Himsg
open Proof_type
open Tacinterp
-open Coqast
open Vernacexpr
-open Ast
-open Extend
let disable_drop e =
if e <> Drop then e
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 86b80935..e0c34dc9 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacinterp.mli,v 1.11.10.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacinterp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*i*)
open Tacexpr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
new file mode 100644
index 00000000..042ee5c8
--- /dev/null
+++ b/toplevel/whelp.ml4
@@ -0,0 +1,209 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: whelp.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
+
+open Options
+open Pp
+open Util
+open System
+open Names
+open Term
+open Environ
+open Rawterm
+open Libnames
+open Nametab
+open Termops
+open Detyping
+open Constrintern
+open Dischargedhypsmap
+open Command
+open Pfedit
+open Refiner
+open Tacmach
+
+(* Coq interface to the Whelp query engine developed at
+ the University of Bologna *)
+
+let make_whelp_request req c =
+ "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+
+let b = Buffer.create 16
+
+let url_char c =
+ if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or
+ '0' <= c & c <= '9' or c ='.'
+ then Buffer.add_char b c
+ else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
+
+let url_string s = String.iter url_char s
+
+let rec url_list_with_sep sep f = function
+ | [] -> ()
+ | [a] -> f a
+ | a::l -> f a; url_string sep; url_list_with_sep sep f l
+
+let url_id id = url_string (string_of_id id)
+
+let uri_of_dirpath dir =
+ url_string "cic:/"; url_list_with_sep "/" url_id (List.rev 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)
+
+let uri_of_repr_kn ref (mp,dir,l) =
+ match mp with
+ | MPfile sl ->
+ uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl)
+ | _ ->
+ error_whelp_unknown_reference ref
+
+let url_paren f l = url_char '('; f l; url_char ')'
+let url_bracket f l = url_char '['; f l; url_char ']'
+
+let whelp_of_rawsort = function
+ | RProp Null -> "Prop"
+ | RProp Pos -> "Set"
+ | RType _ -> "Type"
+
+let uri_int n = Buffer.add_string b (string_of_int n)
+
+let uri_of_ind_pointer l =
+ url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l
+
+let uri_of_global ref =
+ match ref with
+ | 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) ->
+ uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1]
+ | ConstructRef ((kn,i),j) ->
+ uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j]
+
+let whelm_special = id_of_string "WHELM_ANON_VAR"
+
+let url_of_name = function
+ | Name id -> url_id id
+ | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
+
+let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
+
+let uri_params f = function
+ | [] -> ()
+ | l -> url_string "\\subst";
+ url_bracket (url_list_with_sep ";" (uri_of_binding f)) l
+
+let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
+
+let section_parameters = function
+ | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+ get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
+ | RRef (_,(ConstRef cst as ref)) ->
+ get_discharged_hyp_names (sp_of_global ref)
+ | _ -> []
+
+let merge vl al =
+ let rec aux acc = function
+ | ([],l) | (_,([] as l)) -> List.rev acc, l
+ | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
+ in aux [] (vl,al)
+
+let rec uri_of_constr c =
+ match c with
+ | RVar (_,id) -> url_id id
+ | RRef (_,ref) -> uri_of_global ref
+ | RHole _ | REvar _ -> url_string "?"
+ | RSort (_,s) -> url_string (whelp_of_rawsort s)
+ | _ -> url_paren (fun () -> match c with
+ | RApp (_,f,args) ->
+ let inst,rest = merge (section_parameters f) args in
+ uri_of_constr f; url_char ' '; uri_params uri_of_constr inst;
+ url_list_with_sep " " uri_of_constr rest
+ | RLambda (_,na,ty,c) ->
+ url_string "\\lambda "; url_of_name na; url_string ":";
+ uri_of_constr ty; url_string "."; uri_of_constr c
+ | RProd (_,Anonymous,ty,c) ->
+ uri_of_constr ty; url_string "\\to "; uri_of_constr c
+ | RProd (_,Name id,ty,c) ->
+ url_string "\\forall "; url_id id; url_string ":";
+ uri_of_constr ty; url_string "."; uri_of_constr c
+ | RLetIn (_,na,b,c) ->
+ url_string "let "; url_of_name na; url_string "\\def ";
+ uri_of_constr b; url_string " in "; uri_of_constr c
+ | RCast (_,c,_,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"
+ | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+ anomaly "Written w/o parenthesis"
+ | RPatVar _ | RDynamic _ ->
+ anomaly "Found constructors not supported in constr") ()
+
+let make_string f x = Buffer.reset b; f x; Buffer.contents b
+
+let send_whelp req s =
+ let url = make_whelp_request req s in
+ let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in
+ let _ = run_command (fun x -> x) print_string command in ()
+
+let whelp_constr req c =
+ let c = detype false [whelm_special] [] c in
+ send_whelp req (make_string uri_of_constr c)
+
+let whelp_constr_expr req c =
+ let (sigma,env)= get_current_context () in
+ let _,c = interp_open_constr sigma env c in
+ whelp_constr req c
+
+let whelp_locate s =
+ send_whelp "locate" s
+
+let whelp_elim ind =
+ send_whelp "elim" (make_string uri_of_global (IndRef ind))
+
+let locate_inductive r =
+ let (loc,qid) = qualid_of_reference r in
+ try match Syntax_def.locate_global qid with
+ | IndRef ind -> ind
+ | _ -> user_err_loc (loc,"",str "Inductive type expected")
+ with Not_found -> error_global_not_found_loc loc qid
+
+let on_goal f =
+ let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
+ f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+
+type whelp_request =
+ | Locate of string
+ | Elim of inductive
+ | Constr of string * constr
+
+let whelp = function
+ | Locate s -> whelp_locate s
+ | Elim ind -> whelp_elim ind
+ | Constr (s,c) -> whelp_constr s c
+
+VERNAC ARGUMENT EXTEND whelp_constr_request
+| [ "Match" ] -> [ "match" ]
+| [ "Instance" ] -> [ "instance" ]
+END
+
+VERNAC COMMAND EXTEND Whelp
+| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ]
+| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ]
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ]
+| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
+END
+
+VERNAC COMMAND EXTEND WhelpHint
+| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ]
+| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ]
+END
diff --git a/toplevel/recordobj.mli b/toplevel/whelp.mli
index 91550c34..f3f7408a 100755..100644
--- a/toplevel/recordobj.mli
+++ b/toplevel/whelp.mli
@@ -6,7 +6,19 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: recordobj.mli,v 1.7.6.2 2005/01/21 17:18:33 herbelin Exp $ i*)
+(*i $Id: whelp.mli 7837 2006-01-11 09:47:32Z herbelin $ i*)
-val objdef_declare : Libnames.global_reference -> unit
-val add_object_hook : Tacexpr.declaration_hook
+(* Coq interface to the Whelp query engine developed at
+ the University of Bologna *)
+
+open Names
+open Term
+open Topconstr
+open Environ
+
+type whelp_request =
+ | Locate of string
+ | Elim of inductive
+ | Constr of string * constr
+
+val whelp : whelp_request -> unit