summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml2
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/cerrors.mli2
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/class.mli2
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/command.ml62
-rw-r--r--toplevel/command.mli14
-rw-r--r--toplevel/coqinit.ml2
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/coqtop.mli2
-rw-r--r--toplevel/discharge.ml2
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/himsg.ml4
-rw-r--r--toplevel/himsg.mli2
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml72
-rw-r--r--toplevel/indschemes.mli2
-rw-r--r--toplevel/lemmas.ml2
-rw-r--r--toplevel/lemmas.mli2
-rw-r--r--toplevel/metasyntax.ml265
-rw-r--r--toplevel/metasyntax.mli4
-rw-r--r--toplevel/mltop.ml42
-rw-r--r--toplevel/mltop.mli2
-rw-r--r--toplevel/record.ml10
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/search.ml2
-rw-r--r--toplevel/search.mli2
-rw-r--r--toplevel/toplevel.ml2
-rw-r--r--toplevel/toplevel.mli2
-rw-r--r--toplevel/usage.ml2
-rw-r--r--toplevel/usage.mli2
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--toplevel/vernac.mli2
-rw-r--r--toplevel/vernacentries.ml5
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacexpr.ml3
-rw-r--r--toplevel/vernacinterp.ml2
-rw-r--r--toplevel/vernacinterp.mli2
-rw-r--r--toplevel/whelp.ml42
-rw-r--r--toplevel/whelp.mli2
43 files changed, 303 insertions, 208 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 809af337..6064c3d4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: auto_ind_decl.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* This file is about the automatic generation of schemes about
decidable equality, created by Vincent Siles, Oct 2007 *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 071731ac..5828f12d 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index e2c42d50..00316007 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 49b3399c..0ee9dd19 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: class.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Util
open Pp
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 7410ed32..057d85ac 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: class.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4c334e0b..435ddb4d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Names
@@ -149,7 +149,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
let k, cty, ctx', ctx, len, imps, subst =
let (env', ctx), imps = interp_context_evars evars env ctx in
- let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+ let c', imps' = interp_type_evars_impls ~evdref:evars ~fail_evar:false env' tclass in
let len = List.length ctx in
let imps = imps @ Impargs.lift_implicits len imps' in
let ctx', c = decompose_prod_assum c' in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index a19d5dbb..61670e0d 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1f6e7e83..9b18ef27 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
open Pp
open Util
@@ -69,8 +69,7 @@ let red_constant_entry n ce = function
let interp_definition boxed bl red_option c ctypopt =
let env = Global.env() in
let evdref = ref Evd.empty in
- let (env_bl, ctx), imps1 =
- interp_context_evars ~fail_anonymous:false evdref env bl in
+ let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
let imps,ce =
match ctypopt with
None ->
@@ -227,7 +226,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
let env0 = Global.env() in
let evdref = ref Evd.empty in
let (env_params, ctx_params), userimpls =
- interp_context_evars ~fail_anonymous:false evdref env0 paramsl
+ interp_context_evars evdref env0 paramsl
in
let indnames = List.map (fun ind -> ind.ind_name) indl in
@@ -244,7 +243,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
let arities = List.map fst arities in
- let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in
+ let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
let constructors =
@@ -256,9 +255,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
() in
(* Instantiate evars and check all are resolved *)
- let evd,_ = consider_remaining_unif_problems env_params !evdref in
+ let evd = consider_remaining_unif_problems env_params !evdref in
let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
- let sigma = evd in
+ let sigma = evd in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
let arities = List.map (nf_evar sigma) arities in
@@ -448,14 +447,19 @@ let check_mutuality env isfix fixl =
type structured_fixpoint_expr = {
fix_name : identifier;
+ fix_annot : identifier located option;
fix_binders : local_binder list;
fix_body : constr_expr option;
fix_type : constr_expr
}
-let interp_fix_context evdref env fix =
- interp_context_evars evdref env fix.fix_binders
-
+let interp_fix_context evdref env isfix fix =
+ let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
+ let (env', ctx), imps = interp_context_evars evdref env before in
+ let (env'', ctx'), imps' = interp_context_evars evdref env' after in
+ let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
+ ((env'', ctx' @ ctx), imps @ imps', annot)
+
let interp_fix_ccl evdref (env,_) fix =
interp_type_evars evdref env fix.fix_type
@@ -487,8 +491,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
(* Jump over let-bindings. *)
-let compute_possible_guardness_evidences na fix (ids,_) =
- match index_of_annot fix.fix_binders na with
+let compute_possible_guardness_evidences (ids,_,na) =
+ match na with
| Some i -> [i]
| None ->
(* If recursive argument was not given by user, we try all args.
@@ -507,15 +511,15 @@ let interp_recursive isfix fixl notations =
(* Interp arities allowing for unresolved types *)
let evdref = ref Evd.empty in
- let fixctxs, fiximps =
- List.split (List.map (interp_fix_context evdref env) fixl) in
+ let fixctxs, fiximps, fixannots =
+ list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
let fixtypes = List.map (nf_evar !evdref) fixtypes in
let env_rec = push_named_types env fixnames fixtypes in
(* Get interpretation metadatas *)
- let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in
+ let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in
(* Interp bodies with rollback because temp use of notations/implicit *)
let fixdefs =
@@ -525,7 +529,7 @@ let interp_recursive isfix fixl notations =
() in
(* Instantiate evars and check all are resolved *)
- let evd,_ = consider_remaining_unif_problems env_rec !evdref in
+ let evd = consider_remaining_unif_problems env_rec !evdref in
let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in
let fixtypes = List.map (nf_evar evd) fixtypes in
let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in
@@ -538,7 +542,7 @@ let interp_recursive isfix fixl notations =
end;
(* Build the fix declaration block *)
- (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps
+ (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
let interp_fixpoint = interp_recursive true
let interp_cofixpoint = interp_recursive false
@@ -547,7 +551,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
if List.mem None fixdefs then
(* Some bodies to define by proof *)
let thms =
- list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+ list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
@@ -558,7 +562,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in
- let fiximps = List.map snd fiximps in
+ let fiximps = List.map (fun (n,r,p) -> r) fiximps in
let fixdecls =
list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
@@ -572,7 +576,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
if List.mem None fixdefs then
(* Some bodies to define by proof *)
let thms =
- list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in
+ list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
let init_tac =
Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
fixdefs) in
@@ -583,7 +587,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- let fiximps = List.map snd fiximps in
+ let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
@@ -592,28 +596,28 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
List.iter Metasyntax.add_notation_interpretation ntns
let extract_decreasing_argument = function
- | (_,(na,CStructRec),_,_,_) -> na
+ | (na,CStructRec) -> na
| _ -> error
"Only structural decreasing is supported for a non-Program Fixpoint"
let extract_fixpoint_components l =
let fixl, ntnl = List.split l in
- let wfl = List.map extract_decreasing_argument fixl in
- let fixl = List.map (fun ((_,id),_,bl,typ,def) ->
- {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
- fixl, List.flatten ntnl, wfl
+ let fixl = List.map (fun ((_,id),ann,bl,typ,def) ->
+ let ann = extract_decreasing_argument ann in
+ {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
+ fixl, List.flatten ntnl
let extract_cofixpoint_components l =
let fixl, ntnl = List.split l in
List.map (fun ((_,id),bl,typ,def) ->
- {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
+ {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
List.flatten ntnl
let do_fixpoint l b =
- let fixl,ntns,wfl = extract_fixpoint_components l in
+ let fixl,ntns = extract_fixpoint_components l in
let fix = interp_fixpoint fixl ntns in
let possible_indexes =
- list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in
+ List.map compute_possible_guardness_evidences (snd fix) in
declare_fixpoint b fix possible_indexes ntns
let do_cofixpoint l b =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index ab94e7d2..f5996905 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: command.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
(*i*)
open Util
@@ -102,6 +102,7 @@ val do_mutual_inductive :
type structured_fixpoint_expr = {
fix_name : identifier;
+ fix_annot : identifier located option;
fix_binders : local_binder list;
fix_body : constr_expr option;
fix_type : constr_expr
@@ -112,8 +113,7 @@ type structured_fixpoint_expr = {
val extract_fixpoint_components :
(fixpoint_expr * decl_notation list) list ->
- structured_fixpoint_expr list * decl_notation list *
- (* possible structural arg: *) lident option list
+ structured_fixpoint_expr list * decl_notation list
val extract_cofixpoint_components :
(cofixpoint_expr * decl_notation list) list ->
@@ -126,20 +126,20 @@ type recursive_preentry =
val interp_fixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (name list * manual_implicits) list
+ recursive_preentry * (name list * manual_implicits * int option) list
val interp_cofixpoint :
structured_fixpoint_expr list -> decl_notation list ->
- recursive_preentry * (name list * manual_implicits) list
+ recursive_preentry * (name list * manual_implicits * int option) list
(* Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
- bool -> recursive_preentry * (name list * manual_implicits) list ->
+ bool -> recursive_preentry * (name list * manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
val declare_cofixpoint :
- bool -> recursive_preentry * (name list * manual_implicits) list ->
+ bool -> recursive_preentry * (name list * manual_implicits * int option) list ->
decl_notation list -> unit
(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 5f9f96a9..bce38128 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: coqinit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open System
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 926ecf8f..c2a535dd 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: coqinit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Initialization. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3d3010dd..f05509a4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: coqtop.ml 13358 2010-07-29 23:10:17Z herbelin $ *)
open Pp
open Util
@@ -281,7 +281,7 @@ let parse_args is_ide =
| "-emacs-U" :: rem -> Flags.print_emacs := true;
Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
- | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
+ | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
| "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
| "-coqlib" :: [] -> usage ()
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index f5e3a464..e80b3252 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: coqtop.mli 13323 2010-07-24 15:57:30Z 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 af02253b..6f74c526 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: discharge.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Names
open Util
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index a2cbb6be..dda4c5d7 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: discharge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Sign
open Cooking
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a97bf9bb..a080442c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -543,7 +543,7 @@ let explain_unsatisfiable_constraints env evd constr =
match constr with
| None ->
str"Unable to satisfy the following constraints:" ++ fnl() ++
- pr_constraints true env evm
+ pr_constraints true env undef
| Some (ev, k) ->
explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
if List.length (Evd.to_list undef) > 1 then
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 856583d9..a916e87b 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: himsg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6f692ced..4e28ccac 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* File created by Vincent Siles, Oct 2007, extended into a generic
support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index ef3efa47..29d7a12c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *)
(* Created by Hugo Herbelin from contents related to inductive schemes
initially developed by Christine Paulin (induction schemes), Vincent
@@ -54,7 +54,7 @@ let _ =
optread = (fun () -> !elim_flag) ;
optwrite = (fun b -> elim_flag := b) }
-let case_flag = ref true
+let case_flag = ref false
let _ =
declare_bool_option
{ optsync = true;
@@ -63,7 +63,7 @@ let _ =
optread = (fun () -> !case_flag) ;
optwrite = (fun b -> case_flag := b) }
-let eq_flag = ref true
+let eq_flag = ref false
let _ =
declare_bool_option
{ optsync = true;
@@ -292,6 +292,7 @@ let rec split_scheme l =
| (Some id,t)::q -> let l1,l2 = split_scheme q in
( match t with
| InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
+ | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
| EqualityScheme x -> l1,((Some id,smart_global_inductive x)::l2)
)
(*
@@ -299,38 +300,41 @@ let rec split_scheme l =
requested
*)
| (None,t)::q ->
- let l1,l2 = split_scheme q in
- ( match t with
- | InductionScheme (x,y,z) ->
- let ind = smart_global_inductive y in
- let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
- let z' = family_of_sort (interp_sort z) in
- let suffix = (
- match sort_of_ind with
- | InProp ->
- if x then (match z' with
- | InProp -> "_ind_nodep"
- | InSet -> "_rec_nodep"
- | InType -> "_rect_nodep")
- else ( match z' with
- | InProp -> "_ind"
- | InSet -> "_rec"
- | InType -> "_rect" )
- | _ ->
- if x then (match z' with
- | InProp -> "_ind"
- | InSet -> "_rec"
- | InType -> "_rect" )
- else (match z' with
- | InProp -> "_ind_dep"
- | InSet -> "_rec_dep"
- | InType -> "_rect_dep")
- ) in
- let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
- let newref = (dummy_loc,newid) in
+ let l1,l2 = split_scheme q in
+ let names inds recs x y z =
+ let ind = smart_global_inductive y in
+ let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
+ let z' = family_of_sort (interp_sort z) in
+ let suffix = (
+ match sort_of_ind with
+ | InProp ->
+ if x then (match z' with
+ | InProp -> inds ^ "_nodep"
+ | InSet -> recs ^ "_nodep"
+ | InType -> recs ^ "t_nodep")
+ else ( match z' with
+ | InProp -> inds
+ | InSet -> recs
+ | InType -> recs ^ "t" )
+ | _ ->
+ if x then (match z' with
+ | InProp -> inds
+ | InSet -> recs
+ | InType -> recs ^ "t" )
+ else (match z' with
+ | InProp -> inds ^ "_dep"
+ | InSet -> recs ^ "_dep"
+ | InType -> recs ^ "t_dep")
+ ) in
+ let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+ let newref = (dummy_loc,newid) in
((newref,x,ind,z)::l1),l2
- | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
- )
+ in
+ match t with
+ | CaseScheme (x,y,z) -> names "_case" "_case" x y z
+ | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
+ | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2)
+
let do_mutual_induction_scheme lnamedepindsort =
let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 76a5e4b7..f763e182 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: indschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Util
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 89252e54..7af5d0aa 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: lemmas.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Created by Hugo Herbelin from contents related to lemma proofs in
file command.ml, Aug 2009 *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index e0700341..5327f63f 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: lemmas.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a297d1d7..6ee00f48 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
open Pp
open Flags
@@ -280,7 +280,7 @@ let rec find_pattern nt xl = function
| [], NonTerminal x' :: l' ->
(out_nt nt,x',List.rev xl),l'
| [], Terminal s :: _ | Terminal s :: _, _ ->
- error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
+ error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
| [], Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| _, [] ->
@@ -289,23 +289,23 @@ let rec find_pattern nt xl = function
anomaly "Only Terminal or Break expected on left, non-SProdList on right"
let rec interp_list_parser hd = function
- | [] -> [], [], List.rev hd
+ | [] -> [], List.rev hd
| NonTerminal id :: tl when id = ldots_var ->
let hd = List.rev hd in
let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
- let yl,xl,tl'' = interp_list_parser [] tl' in
+ let xyl,tl'' = interp_list_parser [] tl' in
(* We remember each pair of variable denoting a recursive part to *)
(* remove the second copy of it afterwards *)
- (y,x)::yl, x::xl, SProdList (x,sl) :: tl''
+ (x,y)::xyl, SProdList (x,sl) :: tl''
| (Terminal _ | Break _) as s :: tl ->
if hd = [] then
- let yl,xl,tl' = interp_list_parser [] tl in
- yl, xl, s :: tl'
+ let yl,tl' = interp_list_parser [] tl in
+ yl, s :: tl'
else
interp_list_parser (s::hd) tl
| NonTerminal _ as x :: tl ->
- let yl,xl,tl' = interp_list_parser [x] tl in
- yl, xl, List.rev_append hd tl'
+ let xyl,tl' = interp_list_parser [x] tl in
+ xyl, List.rev_append hd tl'
| SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
@@ -345,33 +345,28 @@ let rec get_notation_vars = function
| [] -> []
| NonTerminal id :: sl ->
let vars = get_notation_vars sl in
- if List.mem id vars then
- if id <> ldots_var then
+ if id = ldots_var then vars else
+ if List.mem id vars then
error ("Variable "^string_of_id id^" occurs more than once.")
- else
- vars
- else
- id::vars
+ else
+ id::vars
| (Terminal _ | Break _) :: sl -> get_notation_vars sl
| SProdList _ :: _ -> assert false
let analyze_notation_tokens l =
let l = raw_analyze_notation_tokens l in
let vars = get_notation_vars l in
- let extrarecvars,recvars,l = interp_list_parser [] l in
- (if extrarecvars = [] then [], [], vars, l
- else extrarecvars, recvars, list_subtract vars recvars, l)
-
-let remove_extravars extrarecvars (vars,recvars) =
- let vars =
- List.fold_right (fun (x,y) l ->
- if List.assoc x l <> List.assoc y recvars then
- error
- "Two end variables of a recursive notation are not in the same scope."
- else
- List.remove_assoc x l)
- extrarecvars (List.remove_assoc ldots_var vars) in
- (vars,recvars)
+ let recvars,l = interp_list_parser [] l in
+ recvars, list_subtract vars (List.map snd recvars), l
+
+let error_not_same_scope x y =
+ error ("Variables "^string_of_id x^" and "^string_of_id y^
+ " must be in the same scope.")
+
+let error_both_bound_and_binding x y =
+ errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++
+ strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder
+ for both terms and binders.")
(**********************************************************************)
(* Build pretty-printing rules *)
@@ -434,6 +429,13 @@ let rec is_non_terminal = function
let add_break n l = UnpCut (PpBrk(n,0)) :: l
+let check_open_binder isopen sl m =
+ if isopen & sl <> [] then
+ errorlabstrm "" (str "as " ++ pr_id m ++
+ str " is a non-closed binder, no such \"" ++
+ prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+ ++ strbrk "\" is allowed to occur.")
+
(* Heuristics for building default printing rules *)
type previous_prod_status = NoBreak | CanBreak
@@ -478,7 +480,7 @@ let make_hunks etyps symbols from =
| Terminal s :: prods ->
if is_right_bracket s then
- UnpTerminal s ::make NoBreak prods
+ UnpTerminal s :: make NoBreak prods
else if ws = CanBreak then
add_break 1 (UnpTerminal s :: make NoBreak prods)
else
@@ -489,14 +491,20 @@ let make_hunks etyps symbols from =
| SProdList (m,sl) :: prods ->
let i = list_index m vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+ let typ = List.nth typs (i-1) in
+ let _,prec = precedence_of_entry_type from typ in
let sl' =
(* If no separator: add a break *)
if sl = [] then add_break 1 []
(* We add NonTerminal for simulation but remove it afterwards *)
- else snd (list_sep_last (make NoBreak (sl@[NonTerminal m])))
- in
- UnpListMetaVar (i,prec,sl') :: make CanBreak prods
+ else snd (list_sep_last (make NoBreak (sl@[NonTerminal m]))) in
+ let hunk = match typ with
+ | ETConstr _ -> UnpListMetaVar (i,prec,sl')
+ | ETBinder isopen ->
+ check_open_binder isopen sl m;
+ UnpBinderListMetaVar (i,isopen,sl')
+ | _ -> assert false in
+ hunk :: make CanBreak prods
| [] -> []
@@ -559,12 +567,19 @@ let hunks_of_format (from,(vars,typs)) symfmt =
let symbs, l = aux (symbs,fmt) in symbs, u :: l
| SProdList (m,sl) :: symbs, fmt ->
let i = list_index m vars in
- let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
+ let typ = List.nth typs (i-1) in
+ let _,prec = precedence_of_entry_type from typ in
let slfmt,fmt = read_recursive_format sl fmt in
let sl, slfmt = aux (sl,slfmt) in
if sl <> [] then error_format ();
let symbs, l = aux (symbs,fmt) in
- symbs, UnpListMetaVar (i,prec,slfmt) :: l
+ let hunk = match typ with
+ | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+ | ETBinder isopen ->
+ check_open_binder isopen sl m;
+ UnpBinderListMetaVar (i,isopen,slfmt)
+ | _ -> assert false in
+ symbs, hunk :: l
| symbs, [] -> symbs, []
| _, _ -> error_format ()
in
@@ -632,11 +647,13 @@ let make_production etyps symbols =
(List.map (function Terminal s -> [terminal s]
| Break _ -> []
| _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
- let typ = match List.assoc x etyps with
- | ETConstr x -> x
- | _ ->
- error "Component of recursive patterns in notation must be constr." in
- expand_list_rule typ tkl x 1 0 [] ll)
+ match List.assoc x etyps with
+ | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll
+ | ETBinder o ->
+ distribute
+ [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll
+ | _ ->
+ error "Components of recursive patterns in notation must be terms or binders.")
symbols [[]] in
List.map define_keywords prod
@@ -682,7 +699,7 @@ let error_incompatible_level ntn oldprec prec =
spc() ++ str "while it is now required to be" ++ spc() ++
pr_level ntn prec ++ str ".")
-let cache_one_syntax_extension (prec,ntn,gr,pp) =
+let cache_one_syntax_extension (typs,prec,ntn,gr,pp) =
try
let oldprec = Notation.level_of_notation ntn in
if prec <> oldprec then error_incompatible_level ntn oldprec prec
@@ -690,7 +707,7 @@ let cache_one_syntax_extension (prec,ntn,gr,pp) =
(* Reserve the notation level *)
Notation.declare_notation_level ntn prec;
(* Declare the parsing rule *)
- Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
+ Egrammar.extend_grammar (Egrammar.Notation (prec,typs,gr));
(* Declare the printing rule *)
Notation.declare_notation_printing_rule ntn (pp,fst prec)
@@ -702,8 +719,9 @@ let subst_parsing_rule subst x = x
let subst_printing_rule subst x = x
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)
+ (local, List.map (fun (typs,prec,ntn,gr,pp) ->
+ (typs,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
@@ -768,11 +786,59 @@ let set_entry_type etyps (x,typ) =
| ETConstr (n,()), (_,BorderProd (left,_)) ->
ETConstr (n,BorderProd (left,None))
| ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
- | (ETPattern | ETName | ETBigint | ETOther _ | ETReference as t), _ -> t
- | (ETConstrList _, _) -> assert false
+ | (ETPattern | ETName | ETBigint | ETOther _ |
+ ETReference | ETBinder _ as t), _ -> t
+ | (ETBinderList _ |ETConstrList _), _ -> assert false
with Not_found -> ETConstr typ
in (x,typ)
+let join_auxiliary_recursive_types recvars etyps =
+ List.fold_right (fun (x,y) typs ->
+ let xtyp = try Some (List.assoc x etyps) with Not_found -> None in
+ let ytyp = try Some (List.assoc y etyps) with Not_found -> None in
+ match xtyp,ytyp with
+ | None, None -> typs
+ | Some _, None -> typs
+ | None, Some ytyp -> (x,ytyp)::typs
+ | Some xtyp, Some ytyp when xtyp = ytyp -> typs
+ | Some xtyp, Some ytyp ->
+ errorlabstrm ""
+ (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
+ strbrk ", both ends have incompatible types."))
+ recvars etyps
+
+let internalization_type_of_entry_type = function
+ | ETConstr _ -> NtnInternTypeConstr
+ | ETBigint | ETReference -> NtnInternTypeConstr
+ | ETBinder _ -> NtnInternTypeBinder
+ | ETName -> NtnInternTypeIdent
+ | ETPattern | ETOther _ -> error "Not supported."
+ | ETBinderList _ | ETConstrList _ -> assert false
+
+let set_internalization_type typs =
+ List.map (down_snd internalization_type_of_entry_type) typs
+
+let make_internalization_vars recvars mainvars typs =
+ let maintyps = List.combine mainvars typs in
+ let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
+ maintyps@extratyps
+
+let make_interpretation_type isrec = function
+ | NtnInternTypeConstr when isrec -> NtnTypeConstrList
+ | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr
+ | NtnInternTypeBinder when isrec -> NtnTypeBinderList
+ | NtnInternTypeBinder -> error "Type not allowed in recursive notation."
+
+let make_interpretation_vars recvars allvars =
+ List.iter (fun (x,y) ->
+ if fst (List.assoc x allvars) <> fst (List.assoc y allvars) then
+ error_not_same_scope x y) recvars;
+ let useless_recvars = List.map snd recvars in
+ let mainvars =
+ List.filter (fun (x,_) -> not (List.mem x useless_recvars)) allvars in
+ List.map (fun (x,(sc,typ)) ->
+ (x,(sc,make_interpretation_type (List.mem_assoc x recvars) typ))) mainvars
+
let check_rule_productivity l =
if List.for_all (function NonTerminal _ -> true | _ -> false) l then
error "A notation must include at least one symbol.";
@@ -791,29 +857,31 @@ let find_precedence lev etyps symbols =
error "The level of the leftmost non-terminal cannot be changed."
| ETName | ETBigint | ETReference ->
if lev = None then
- if_verbose msgnl (str "Setting notation at level 0.")
+ ([msgnl,str "Setting notation at level 0."],0)
else
if lev <> Some 0 then
- error "A notation starting with an atomic expression must be at level 0.";
- 0
- | ETPattern | ETOther _ -> (* Give a default ? *)
+ error "A notation starting with an atomic expression must be at level 0."
+ else
+ ([],0)
+ | ETPattern | ETBinder _ | ETOther _ -> (* Give a default ? *)
if lev = None then
error "Need an explicit level."
- else Option.get lev
- | ETConstrList _ -> assert false (* internally used in grammar only *)
+ else [],Option.get lev
+ | ETConstrList _ | ETBinderList _ ->
+ assert false (* internally used in grammar only *)
with Not_found ->
if lev = None then
error "A left-recursive notation must have an explicit level."
- else Option.get lev)
+ else [],Option.get lev)
| Terminal _ ::l when
(match list_last symbols with Terminal _ -> true |_ -> false)
->
if lev = None then
- (if_verbose msgnl (str "Setting notation at level 0."); 0)
- else Option.get lev
+ ([msgnl,str "Setting notation at level 0."], 0)
+ else [],Option.get lev
| _ ->
if lev = None then error "Cannot determine the level.";
- Option.get lev
+ [],Option.get lev
let check_curly_brackets_notation_exists () =
try let _ = Notation.level_of_notation "{ _ }" in ()
@@ -849,13 +917,13 @@ let compute_syntax_data (df,modifiers) =
(* Notation defaults to NONA *)
let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
let toks = split_notation_string df in
- let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in
+ let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let need_squash = (symbols <> symbols') in
let ntn_for_grammar = make_notation_key symbols' in
check_rule_productivity symbols';
- let n = find_precedence n etyps symbols' in
+ let msgs,n = find_precedence n etyps symbols' in
let innerlevel = NumLevel 200 in
let typs =
find_symbols
@@ -864,12 +932,25 @@ let compute_syntax_data (df,modifiers) =
(NumLevel n,BorderProd(Right,assoc))
symbols' in
(* To globalize... *)
- let typs = List.map (set_entry_type etyps) typs in
- let prec = (n,List.map (assoc_of_type n) typs) in
- let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
+ let etyps = join_auxiliary_recursive_types recvars etyps in
+ let sy_typs = List.map (set_entry_type etyps) typs in
+ let prec = (n,List.map (assoc_of_type n) sy_typs) in
+ let i_typs = set_internalization_type sy_typs in
+ let sy_data = (n,sy_typs,symbols',fmt) in
+ let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
- let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
- (i_data,sy_data)
+ let i_data = (onlyparse,recvars,mainvars,(ntn_for_interp,df')) in
+ (* Return relevant data for interpretation and for parsing/printing *)
+ (msgs,i_data,i_typs,sy_fulldata)
+
+let compute_pure_syntax_data (df,mods) =
+ let (msgs,(onlyparse,_,_,_),_,sy_data) = compute_syntax_data (df,mods) in
+ let msgs =
+ if onlyparse then
+ (msg_warning,
+ str "The only parsing modifier has no effect in Reserved Notation.")::msgs
+ else msgs in
+ msgs, sy_data
(**********************************************************************)
(* Registration of notations interpretation *)
@@ -925,9 +1006,9 @@ exception NoSyntaxRule
let recover_syntax ntn =
try
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)
+ let pp_rule,_ = Notation.find_notation_printing_rule ntn in
+ let typs,pa_rule = Egrammar.recover_notation_grammar ntn prec in
+ (typs,prec,ntn,pa_rule,pp_rule)
with Not_found ->
raise NoSyntaxRule
@@ -935,9 +1016,9 @@ let recover_squash_syntax () = recover_syntax "{ _ }"
let recover_notation_syntax rawntn =
let ntn = contract_notation rawntn in
- let sy_rule = recover_syntax ntn in
+ let (typs,_,_,_,_ as sy_rule) = recover_syntax ntn in
let need_squash = ntn<>rawntn in
- if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
+ typs,if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
(**********************************************************************)
(* Main entry point for building parsing and printing rules *)
@@ -952,10 +1033,10 @@ let make_pp_rule (n,typs,symbols,fmt) =
| 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 make_syntax_rules (i_typs,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
+ let sy_rule = (i_typs,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) *)
@@ -965,31 +1046,35 @@ let make_syntax_rules (ntn,prec,need_squash,sy_data) =
(* 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 (msgs,i_data,i_typs,sy_data) = compute_syntax_data (df,mods) in
+ (* Prepare 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,extrarecvars,recvars,vars,df') = i_data in
- let (acvars,ac) = interp_aconstr (vars,recvars) c in
- let a = (remove_extravars extrarecvars acvars,ac) in
+ (* Prepare the interpretation *)
+ let (onlyparse,recvars,mainvars,df') = i_data in
+ let i_vars = make_internalization_vars recvars mainvars i_typs in
+ let (acvars,ac) = interp_aconstr i_vars recvars c in
+ let a = (make_interpretation_vars recvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
+ (* Ready to change the global state *)
+ Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
+ Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
df'
let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
let dfs = split_notation_string df in
- let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in
- (* Redeclare pa/pp rules *)
- if not (is_numeral symbs) then begin
- let sy_rules = recover_notation_syntax (make_notation_key symbs) in
- Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
- end;
+ let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
+ (* Recover types of variables and pa/pp rules; redeclare them if needed *)
+ let i_typs = if not (is_numeral symbs) then begin
+ let i_typs,sy_rules = recover_notation_syntax (make_notation_key symbs) in
+ Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)); i_typs
+ end else [] in
(* Declare interpretation *)
let path = (Lib.library_dp(),Lib.current_dirpath true) in
let df' = (make_notation_key symbs,(path,df)) in
- let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in
- let a = (remove_extravars extrarecvars acvars,ac) in
+ let i_vars = make_internalization_vars recvars mainvars i_typs in
+ let (acvars,ac) = interp_aconstr ~impls i_vars recvars c in
+ let a = (make_interpretation_vars recvars acvars,ac) in
let onlyparse = onlyparse or is_not_printable ac in
Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
df'
@@ -997,8 +1082,9 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
(* Notations without interpretation (Reserved Notation) *)
let add_syntax_extension local ((loc,df),mods) =
- let (_,sy_data) = compute_syntax_data (df,mods) in
+ let msgs,sy_data = compute_pure_syntax_data (df,mods) in
let sy_rules = make_syntax_rules sy_data in
+ Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
@@ -1090,7 +1176,10 @@ let try_interp_name_alias = function
let add_syntactic_definition ident (vars,c) local onlyparse =
let vars,pat =
try [], ARef (try_interp_name_alias (vars,c))
- with Not_found -> let (vars,_),pat = interp_aconstr (vars,[]) c in vars,pat
+ with Not_found ->
+ let i_vars = List.map (fun id -> (id,NtnInternTypeConstr)) vars in
+ let vars,pat = interp_aconstr i_vars [] c in
+ List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
in
let onlyparse = onlyparse or is_not_printable pat in
Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 2fd7749d..d8dd0d52 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: metasyntax.mli 13328 2010-07-26 11:05:30Z herbelin $ i*)
(*i*)
open Util
@@ -47,7 +47,7 @@ val add_notation_interpretation :
(* Add a notation interpretation for supporting the "where" clause *)
-val set_notation_for_interpretation : Constrintern.full_internalization_env ->
+val set_notation_for_interpretation : Constrintern.internalization_env ->
(lstring * constr_expr * scope_name option) -> unit
(* Add only the parsing/printing rule of a notation *)
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 5cefe263..e8c06d13 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
* camlp4deps will not work for this file unless Makefile system enhanced.
*)
-(* $Id$ *)
+(* $Id: mltop.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
open Util
open Pp
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index c2d65493..12b6f78f 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: mltop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* If there is a toplevel under Coq, it is described by the following
record. *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ae53b0cf..cd569178 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
open Pp
open Util
@@ -32,7 +32,6 @@ open Topconstr
(********** definition d'un record (structure) **************)
let interp_evars evdref env impls k typ =
- let impls = set_internalization_env_params impls [] in
let typ' = intern_gen true ~impls !evdref env typ in
let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
@@ -48,8 +47,7 @@ let interp_fields_evars evars env nots l =
| Name id -> (id, compute_internalization_data env Constrintern.Method t' impl) :: impls
in
let d = (i,b',t') in
- let impls' = set_internalization_env_params impls [] in
- List.iter (Metasyntax.set_notation_for_interpretation impls') no;
+ List.iter (Metasyntax.set_notation_for_interpretation impls) no;
(push_rel d env, impl :: uimpls, d::params, impls))
(env, [], [], []) nots l
@@ -62,13 +60,13 @@ let binders_of_decls = List.map binder_of_decl
let typecheck_params_and_fields id t ps nots fs =
let env0 = Global.env () in
let evars = ref Evd.empty in
- let (env1,newps), imps = interp_context_evars ~fail_anonymous:false evars env0 ps in
+ let (env1,newps), imps = interp_context_evars evars env0 ps in
let fullarity = it_mkProd_or_LetIn (Option.cata (fun x -> x) (new_Type ()) t) newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,impls,newfs,data =
interp_fields_evars evars env_ar nots (binders_of_decls fs)
in
- let evars,_ = Evarconv.consider_remaining_unif_problems env_ar !evars in
+ let evars = Evarconv.consider_remaining_unif_problems env_ar !evars in
let evars = Typeclasses.resolve_typeclasses env_ar evars in
let sigma = evars in
let newps = Evarutil.nf_rel_context_evar sigma newps in
diff --git a/toplevel/record.mli b/toplevel/record.mli
index eae279f3..ea4a3b7e 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: record.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/search.ml b/toplevel/search.ml
index a358f687..0bd552af 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/search.mli b/toplevel/search.mli
index b4b971a7..a73052f2 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: search.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
open Pp
open Names
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 64096152..9594c988 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 92c8ddc4..a614c1da 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: toplevel.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index dcee9921..22588f2c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: usage.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 662f56ad..1167750b 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: usage.mli 13323 2010-07-24 15:57:30Z 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 17792579..7f8bcb9e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d925614c..dc4d9e2f 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: vernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3a5e1da8..254f690c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -626,7 +626,6 @@ let vernac_instance abst glob sup inst props pri =
ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
let vernac_context l =
- List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
Classes.context l
let vernac_declare_instance glob id =
@@ -1079,7 +1078,7 @@ let vernac_global_check c =
let vernac_print = function
| PrintTables -> print_tables ()
- | PrintFullContext -> msg (print_full_context_typ ())
+ | PrintFullContext-> msg (print_full_context_typ ())
| PrintSectionContext qid -> msg (print_sec_context_typ qid)
| PrintInspect n -> msg (inspect n)
| PrintGrammar ent -> Metasyntax.print_grammar ent
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 031864fd..10ed35a7 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: vernacentries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 1f3261e1..5eb220cb 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
open Util
open Names
@@ -197,6 +197,7 @@ type proof_end =
type scheme =
| InductionScheme of bool * reference or_by_notation * sort_expr
+ | CaseScheme of bool * reference or_by_notation * sort_expr
| EqualityScheme of reference or_by_notation
type vernac_expr =
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 90d8d9dd..f3d2e7a5 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: vernacinterp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 8bcbe5f3..ce64188c 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: vernacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i*)
open Tacexpr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 20928cbe..15caaddd 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id$ *)
+(* $Id: whelp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
open Flags
open Pp
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index d6beeca1..27c36239 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: whelp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Coq interface to the Whelp query engine developed at
the University of Bologna *)