aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/extraction/g_extraction.ml45
-rw-r--r--contrib/interface/showproof.ml2
-rw-r--r--contrib/interface/xlate.ml4
-rw-r--r--interp/constrextern.ml4
-rw-r--r--parsing/egrammar.ml1
-rw-r--r--parsing/g_constrnew.ml4145
-rw-r--r--parsing/g_ltacnew.ml46
-rw-r--r--parsing/g_prim.ml43
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--parsing/g_tacticnew.ml4102
-rw-r--r--parsing/g_vernacnew.ml42
-rw-r--r--parsing/lexer.ml434
-rw-r--r--parsing/pcoq.ml43
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--parsing/pptactic.ml6
-rw-r--r--parsing/q_coqast.ml48
-rw-r--r--proofs/tacexpr.ml4
-rw-r--r--tactics/hiddentac.ml6
-rw-r--r--tactics/hiddentac.mli4
-rw-r--r--tactics/tacinterp.ml17
-rw-r--r--tactics/tactics.ml20
-rw-r--r--tactics/tactics.mli4
-rwxr-xr-xtest-suite/check2
-rw-r--r--theories/Init/LogicSyntax.v47
-rw-r--r--toplevel/metasyntax.ml18
-rw-r--r--toplevel/vernac.ml25
-rw-r--r--translate/ppconstrnew.ml34
-rw-r--r--translate/pptacticnew.ml138
-rw-r--r--translate/ppvernacnew.ml13
29 files changed, 410 insertions, 252 deletions
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index c8ee21c0e..72ad70105 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -15,7 +15,10 @@ open Pcoq
open Genarg
open Pp
-let pr_mlname _ _ s = spc () ++ str"\"" ++ str s ++ str"\""
+let pr_mlname _ _ s =
+ spc () ++
+ (if !Options.v7 && not (Options.do_translate()) then qs s
+ else Pptacticnew.qsnew s)
ARGUMENT EXTEND mlname
TYPED AS string
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index d33a41f98..f2f56caa8 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1285,7 +1285,7 @@ let rec natural_ntree ig ntree =
| TacAssumption -> natural_trivial ig lh g gs ltree
| TacClear _ -> natural_clear ig lh g gs ltree
(* Besoin de l'argument de la tactique *)
- | TacOldInduction (NamedHyp id) ->
+ | TacSimpleInduction (NamedHyp id) ->
natural_induction ig lh g gs ge id ltree false
| TacExtend (_,"InductionIntro",[a]) ->
let id=(out_gen wit_ident a) in
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 244b0543d..2be3e18e6 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -964,8 +964,8 @@ and xlate_tac =
CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
| TacCase (c1,sl) ->
CT_casetac (xlate_formula c1, xlate_bindings sl)
- | TacOldInduction h -> CT_induction (xlate_quantified_hypothesis h)
- | TacOldDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
+ | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
+ | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
| TacCut c -> CT_cut (xlate_formula c)
| TacLApply c -> CT_use (xlate_formula c)
| TacDecompose ([],c) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7a557f858..7ec783e03 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,6 +274,8 @@ let translate_v7_string = function
| "simpl_plus_r" -> "plus_simpl_r"
| "fact_growing" -> "fact_le"
| "lt_mult_left" -> "lt_mult_S_left"
+ | "exists" -> "exists_between"
+ | "IHexists" -> "IHexists_between"
(* Lists *)
| "idempot_rev" -> "involutive_rev"
| "forall" -> "HereAndFurther"
@@ -310,6 +312,8 @@ let translate_v7_string = function
(s' = "unicite" or s' = "unicity") ->
"uniqueness"^(String.sub s 7 (String.length s - 7))
(* Default *)
+ | s when String.length s > 1 && s.[0]='_' ->
+ String.sub s 1 (String.length s - 1)
| "_" ->
msgerrnl (str
"Warning: '_' is no longer an ident; it has been translated to 'x_'");
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 88c821167..6d1d317e6 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -55,7 +55,6 @@ let default_levels_v8 =
[200,Gramext.RightA;
100,Gramext.RightA;
80,Gramext.RightA;
- 40,Gramext.LeftA;
10,Gramext.LeftA;
9,Gramext.RightA;
1,Gramext.LeftA;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index e8f9c38c5..ce45d73b0 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -22,7 +22,7 @@ open Util
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
"end"; "as"; "let"; "if"; "then"; "else"; "return";
- "Prop"; "Set"; "Type"; ".(" ]
+ "Prop"; "Set"; "Type"; ".("; "_" ]
let _ =
if not !Options.v7 then
@@ -46,47 +46,20 @@ let mk_lam = function
([],c) -> c
| (bl,c) -> CLambdaN(constr_loc c, bl,c)
-let coerce_to_id c =
- match c with
- CRef(Ident(loc,id)) -> (loc,Name id)
- | CHole loc -> (loc,Anonymous)
- | _ -> error "ill-formed match type annotation"
-
-let match_bind_of_pat loc (oid,ty) =
- let l2 =
- match oid with
- None -> []
- | Some x -> [([x],CHole loc)] in
- let l1 =
- match ty with
- None -> [] (* No: should lookup inductive arity! *)
- | Some (CApp(_,_,args)) -> (* parameters do not appear *)
- List.map (fun (c,_) -> ([coerce_to_id c],CHole loc)) args
- | _ -> error "ill-formed match type annotation" in
- l1@l2
-
let mk_match (loc,cil,rty,br) =
-(*
- let (lc,pargs) = List.split cil in
- let pr =
- match rty with
- None -> None
- | Some ty ->
- let idargs = (* TODO: not forget the list lengths for PP! *)
- List.flatten (List.map (match_bind_of_pat loc) pargs) in
- Some (CLambdaN(loc,idargs,ty)) in
-*)
CCases(loc,(None,rty),cil,br)
+let index_of_annot bl ann =
+ match bl,ann with
+ [([_],_)], None -> 0
+ | _, Some x ->
+ let ids = List.map snd (List.flatten (List.map fst bl)) in
+ (try list_index (snd x) ids - 1
+ with Not_found -> error "no such fix variable")
+ | _ -> error "cannot guess decreasing argument of fix"
+
let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
- let n =
- match bl,ann with
- [([_],_)], None -> 0
- | _, Some x ->
- let ids = List.map snd (List.flatten (List.map fst bl)) in
- (try list_index (snd x) ids - 1
- with Not_found -> error "no such fix variable")
- | _ -> error "cannot find decreasing arg of fix" in
+ let n = index_of_annot bl ann in
let ty = match tyc with
None -> CHole tloc
| Some t -> CProdN(loc,bl,t) in
@@ -113,7 +86,6 @@ let mk_fix(loc,kw,id,dcls) =
let binder_constr =
create_constr_entry (get_univ "constr") "binder_constr"
-
let rec mkCProdN loc bll c =
match bll with
| LocalRawAssum ((loc1,_)::_ as idl,t) :: bll ->
@@ -132,33 +104,35 @@ let rec mkCLambdaN loc bll c =
| [] -> c
| LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
-(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
-(* admissible notation "(n)" *)
-let test_lpar_id_coloneq =
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let lpar_id_coloneq =
Gram.Entry.of_parser "test_lpar_id_coloneq"
(fun strm ->
- match Stream.npeek 1 strm with
- | [("", "(")] ->
- begin match Stream.npeek 2 strm with
- | [_; ("IDENT", _)] ->
- begin match Stream.npeek 3 strm with
- | [_; _; ("", ":=")] -> ()
- | _ -> raise Stream.Failure
- end
- | _ -> raise Stream.Failure
- end
- | _ -> raise Stream.Failure)
+ match Stream.npeek 3 strm with
+ | [("","("); ("IDENT",s); ("", ":=")] ->
+ Stream.junk strm; Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure);;
+
if not !Options.v7 then
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
- constr_pattern lconstr_pattern Constr.ident binder_let tuple_constr;
+ constr_pattern lconstr_pattern Constr.ident binder binder_let
+ tuple_constr;
Constr.ident:
[ [ id = Prim.ident -> id
(* This is used in quotations and Syntax *)
| id = METAIDENT -> id_of_string id ] ]
;
+ Prim.name:
+ [ [ "_" -> (loc, Anonymous) ] ]
+ ;
+ Prim.ast:
+ [ [ "_" -> Coqast.Nvar(loc,id_of_string"_") ] ]
+ ;
global:
[ [ r = Prim.reference -> r
@@ -177,7 +151,7 @@ GEXTEND Gram
| "Type" -> RType None ] ]
;
lconstr:
- [ [ c = operconstr -> c ] ]
+ [ [ c = operconstr LEVEL "200" -> c ] ]
;
constr:
[ [ c = operconstr LEVEL "9" -> c ] ]
@@ -197,8 +171,6 @@ GEXTEND Gram
| "80" RIGHTA
[ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
| c1 = operconstr; "->"; c2 = operconstr -> CArrow(loc,c1,c2) ]
- | "40L" LEFTA
- [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
| "10L" LEFTA
[ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
| "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
@@ -206,7 +178,8 @@ GEXTEND Gram
| "1L" LEFTA
[ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
- | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT; ")" ->
+ | c=operconstr; ".("; "@"; f=global;
+ args=LIST0 (operconstr LEVEL "9"); ")" ->
CAppExpl(loc,(Some (List.length args+1),f),args@[c])
| c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
| "0"
@@ -217,19 +190,25 @@ GEXTEND Gram
binder_constr:
[ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
mkCProdN loc bl c
- | "fun"; bl = binder_list; ty = type_cstr; "=>";
- c = operconstr LEVEL "200" ->
- mkCLambdaN loc bl (mk_cast(c,ty))
+ | "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" ->
+ mkCLambdaN loc bl c
| "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
- c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+ c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
let loc1 = match bl with
| LocalRawAssum ((loc,_)::_,_)::_ -> loc
| LocalRawDef ((loc,_),_)::_ -> loc
| _ -> dummy_loc in
CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+ | "let"; fx = fix_constr; "in"; c = operconstr LEVEL "200" ->
+ let (li,id) = match fx with
+ CFix(_,id,_) -> id
+ | CCoFix(_,id,_) -> id
+ | _ -> assert false in
+ CLetIn(loc,(li,Name id),fx,c)
| "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
po = return_type;
- ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+ ":="; c1 = operconstr LEVEL "200"; "in";
+ c2 = operconstr LEVEL "200" ->
CLetTuple (loc,List.map snd lb,po,c1,c2)
| "if"; c=operconstr; po = return_type;
"then"; b1=operconstr LEVEL "200";
@@ -238,21 +217,15 @@ GEXTEND Gram
| c=fix_constr -> c ] ]
;
appl_arg:
- [ [ _ = test_lpar_id_coloneq; "("; id = ident; ":="; c=lconstr; ")" ->
+ [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
(c,Some (loc,ExplByName id))
-(*
- | "@"; n=INT; ":="; c=constr -> (c,Some(loc,ExplByPos (int_of_string n)))
-*)
| c=constr -> (c,None) ] ]
;
atomic_constr:
[ [ g=global -> CRef g
| s=sort -> CSort(loc,s)
| n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
- | IDENT "_" -> CHole loc
-(*
- | "?"; n=Prim.natural -> CPatVar(loc,(false,Pattern.patvar_of_int n)) ] ]
-*)
+ | "_" -> CHole loc
| "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
;
fix_constr:
@@ -282,12 +255,13 @@ GEXTEND Gram
case_item:
[ [ c=operconstr LEVEL "100"; p=pred_pattern ->
match c,p with
- | CRef (Ident (_,id)), (Names.Anonymous,x) -> (c,(Name id,x))
- | _ -> (c,p) ] ]
+ | CRef (Ident (_,id)), (None,indp) -> (c,(Name id,indp))
+ | _, (None,indp) -> (c,(Anonymous,indp))
+ | _, (Some na,indp) -> (c,(na,indp)) ] ]
;
pred_pattern:
- [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
- ty = OPT ["in"; t=lconstr -> t] -> (oid,ty) ] ]
+ [ [ ona = OPT ["as"; id=name -> snd id];
+ ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ]
;
case_type:
[ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]
@@ -302,24 +276,23 @@ GEXTEND Gram
eqn:
[ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
;
- simple_pattern:
- [ [ r = Prim.reference -> CPatAtom (loc,Some r)
- | IDENT "_" -> CPatAtom (loc,None)
- | "("; p = lpattern; ")" -> p
- | n = bigint -> CPatNumeral (loc,n)
- ] ]
- ;
pattern:
- [ [ p = pattern ; lp = LIST1 simple_pattern ->
+ [ "1" LEFTA
+ [ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
(match p with
| CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
| _ -> Util.user_err_loc
- (loc, "compound_pattern", Pp.str "Constructor expected"))
+ (cases_pattern_loc p, "compound_pattern",
+ Pp.str "Constructor expected"))
| p = pattern; "as"; id = base_ident ->
CPatAlias (loc, p, id)
| c = pattern; "%"; key=IDENT ->
- CPatDelimiters (loc,key,c)
- | p = simple_pattern -> p ] ]
+ CPatDelimiters (loc,key,c) ]
+ | "0"
+ [ r = Prim.reference -> CPatAtom (loc,Some r)
+ | "_" -> CPatAtom (loc,None)
+ | "("; p = lpattern; ")" -> p
+ | n = bigint -> CPatNumeral (loc,n) ] ]
;
lpattern:
[ [ c = pattern -> c
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 672aeb3b6..9d8dea149 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -142,7 +142,7 @@ GEXTEND Gram
| "()" -> TacVoid ] ]
;
input_fun:
- [ [ IDENT "_" -> None
+ [ [ "_" -> None
| l = base_ident -> Some l ] ]
;
let_clause:
@@ -171,7 +171,7 @@ GEXTEND Gram
match_context_rule:
[ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
"=>"; te = tactic_expr -> Pat (largs, mp, te)
- | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+ | "_"; "=>"; te = tactic_expr -> All te ] ]
;
match_context_list:
[ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
@@ -179,7 +179,7 @@ GEXTEND Gram
;
match_rule:
[ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te)
- | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+ | "_"; "=>"; te = tactic_expr -> All te ] ]
;
match_list:
[ [ mrl = LIST1 match_rule SEP "|" -> mrl
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 39a7687f1..7a1b910c6 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -88,7 +88,8 @@ GEXTEND Gram
[ [ s = IDENT -> local_id_of_string s ] ]
;
name:
- [ [ IDENT "_" -> (loc, Anonymous) | id = base_ident -> (loc, Name id) ] ]
+ [ [ IDENT "_" -> (loc, Anonymous)
+ | id = base_ident -> (loc, Name id) ] ]
;
identref:
[ [ id = base_ident -> (loc,id) ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 18422b460..6c8ad0c1b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -295,12 +295,12 @@ GEXTEND Gram
| IDENT "LApply"; c = constr -> TacLApply c
(* Derived basic tactics *)
- | IDENT "Induction"; h = quantified_hypothesis -> TacOldInduction h
+ | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction h
| IDENT "NewInduction"; c = induction_arg; el = OPT eliminator;
ids = with_names -> TacNewInduction (c,el,ids)
| IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
- | IDENT "Destruct"; h = quantified_hypothesis -> TacOldDestruct h
+ | IDENT "Destruct"; h = quantified_hypothesis -> TacSimpleDestruct h
| IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator;
ids = with_names -> TacNewDestruct (c,el,ids)
| IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 414311b0f..b17907844 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -22,17 +22,33 @@ let _ =
if not !Options.v7 then
List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
-(* Hack to parse "with n := c ..." as a binder without conflicts with the *)
-(* admissible notation "with c1 c2..." *)
-let test_lparcoloneq2 =
- Gram.Entry.of_parser "test_lparcoloneq2"
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let lpar_id_coloneq =
+ Gram.Entry.of_parser "lpar_id_coloneq"
(fun strm ->
- match Stream.npeek 1 strm with
- | [("", "(")] ->
- begin match Stream.npeek 3 strm with
- | [_; _; ("", ":=")] -> ()
- | _ -> raise Stream.Failure
- end
+ match Stream.npeek 3 strm with
+ | [("","("); ("IDENT",s); ("", ":=")] ->
+ Stream.junk strm; Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
+
+(* idem for (x:=t) and (1:=t) *)
+let test_lpar_idnum_coloneq =
+ Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+ (fun strm ->
+ match Stream.npeek 3 strm with
+ | [("","("); (("IDENT"|"INT"),_); ("", ":=")] -> ()
+ | _ -> raise Stream.Failure)
+
+(* idem for (x:t) *)
+let lpar_id_colon =
+ Gram.Entry.of_parser "test_lpar_id_colon"
+ (fun strm ->
+ match Stream.npeek 3 strm with
+ | [("","("); ("IDENT",id); ("", ":")] ->
+ Stream.junk strm; Stream.junk strm; Stream.junk strm;
+ Names.id_of_string id
| _ -> raise Stream.Failure)
(* open grammar entries, possibly in quotified form *)
@@ -42,10 +58,28 @@ open Constr
open Prim
open Tactic
-(* Functions overloaded by quotifier *)
+let mk_fix_tac (loc,id,bl,ann,ty) =
+ let n =
+ match bl,ann with
+ [([_],_)], None -> 0
+ | _, Some x ->
+ let ids = List.map snd (List.flatten (List.map fst bl)) in
+ (try list_index (snd x) ids
+ with Not_found -> error "no such fix variable")
+ | _ -> error "cannot guess decreasing argument of fix" in
+ (id,n,Topconstr.CProdN(loc,bl,ty))
+let mk_cofix_tac (loc,id,bl,ann,ty) =
+ let _ = option_app (fun (aloc,_) ->
+ Util.user_err_loc
+ (aloc,"Constr:mk_cofix_tac",
+ Pp.str"Annotation forbidden in cofix expression")) ann in
+ (id,Topconstr.CProdN(loc,bl,ty))
+
+(* Functions overloaded by quotifier *)
let induction_arg_of_constr c =
- try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c
+ try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c)
+ with _ -> ElimOnConstr c
let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
@@ -160,7 +194,7 @@ GEXTEND Gram
simple_intropattern:
[ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
| "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
- | IDENT "_" -> IntroWildcard
+ | "_" -> IntroWildcard
| id = base_ident -> IntroIdentifier id
] ]
;
@@ -169,7 +203,8 @@ GEXTEND Gram
| "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ]
;
binding_list:
- [ [ test_lparcoloneq2; bl = LIST1 simple_binding -> ExplicitBindings bl
+ [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
+ ExplicitBindings bl
| bl = LIST1 constr -> ImplicitBindings bl ] ]
;
constr_with_bindings:
@@ -223,10 +258,12 @@ GEXTEND Gram
| -> [] ] ]
;
fixdecl:
- [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
+ [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot;
+ ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ]
;
- cofixdecl:
- [ [ id = base_ident; ":"; c = constr -> (id,c) ] ]
+ fixannot:
+ [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
+ | -> None ] ]
;
hintbases:
[ [ "with"; "*" -> None
@@ -265,39 +302,42 @@ GEXTEND Gram
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = base_ident; n = natural -> TacFix (Some id,n)
| "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl ->
- TacMutualFix (id,n,fd)
+ TacMutualFix (id,n,List.map mk_fix_tac fd)
| "cofix" -> TacCofix None
| "cofix"; id = base_ident -> TacCofix (Some id)
- | "cofix"; id = base_ident; "with"; fd = LIST0 cofixdecl ->
- TacMutualCofix (id,fd)
+ | "cofix"; id = base_ident; "with"; fd = LIST0 fixdecl ->
+ TacMutualCofix (id,List.map mk_cofix_tac fd)
| IDENT "cut"; c = constr -> TacCut c
+ | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
+ TacTrueCut (Some id,t)
+ | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
+ TacForward (false,Names.Name id,b)
| IDENT "assert"; c = constr -> TacTrueCut (None,c)
- | IDENT "assert"; c = constr; ":"; t = lconstr ->
- TacTrueCut (Some (coerce_to_id c),t)
- | IDENT "assert"; c = constr; ":="; b = lconstr ->
- TacForward (false,Names.Name (coerce_to_id c),b)
- | IDENT "pose"; c = constr; ":="; b = lconstr ->
- TacForward (true,Names.Name (coerce_to_id c),b)
+ | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
+ TacForward (true,Names.Name id,b)
| IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
| IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
| IDENT "generalize"; IDENT "dependent"; c = constr ->
TacGeneralizeDep c
- | IDENT "lettac"; id = base_ident; ":="; c = lconstr; p = clause_pattern
- -> TacLetTac (id,c,p)
- | IDENT "instantiate"; n = natural; c = constr -> TacInstantiate (n,c)
+ | IDENT "lettac"; "("; id = base_ident; ":="; c = lconstr; ")";
+ p = clause_pattern -> TacLetTac (id,c,p)
+ | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" ->
+ TacInstantiate (n,c)
| IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
| IDENT "lapply"; c = constr -> TacLApply c
(* Derived basic tactics *)
- | IDENT "oldinduction"; h = quantified_hypothesis -> TacOldInduction h
+ | IDENT "simple_induction"; h = quantified_hypothesis ->
+ TacSimpleInduction h
| IDENT "induction"; c = induction_arg; el = OPT eliminator;
ids = with_names -> TacNewInduction (c,el,ids)
| IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
- | IDENT "olddestruct"; h = quantified_hypothesis -> TacOldDestruct h
+ | IDENT "simple_destruct"; h = quantified_hypothesis ->
+ TacSimpleDestruct h
| IDENT "destruct"; c = induction_arg; el = OPT eliminator;
ids = with_names -> TacNewDestruct (c,el,ids)
| IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8e0088890..28c0f5fd4 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -759,7 +759,7 @@ GEXTEND Gram
] ]
;
opt_scope:
- [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ]
+ [ [ "_" -> None | sc = IDENT -> Some sc ] ]
;
(* Syntax entries for Grammar. Only grammar_entry is exported *)
grammar_entry:
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 843bd068f..a96237e5b 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -110,7 +110,8 @@ let is_normal_token str =
if String.length str > 0 then
match str.[0] with
| ' ' | '\n' | '\r' | '\t' | '"' -> bad_token str
- | '_' | '$' | 'a'..'z' | 'A'..'Z' -> true
+ | '$' | 'a'..'z' | 'A'..'Z' -> true
+ | '_' -> !Options.v7
(* utf-8 symbols of the form "E2 xx xx" [E2=226] *)
| '\226' when String.length str > 2 ->
(match str.[1], str.[2] with
@@ -122,9 +123,9 @@ let is_normal_token str =
false
| _ ->
(* default to iso 8859-1 "â" *)
- true)
+ !Options.v7)
(* iso 8859-1 accentuated letters *)
- | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' -> true
+ | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' -> !Options.v7
| _ -> false
else
bad_token str
@@ -347,7 +348,7 @@ let parse_226_tail tk = parser
(* Parse what follows a dot *)
let parse_after_dot bp c strm =
- if (* !Options.v7 *) true then
+ if !Options.v7 then
match strm with parser
| [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
("FIELD", get_buff len)
@@ -369,6 +370,19 @@ let parse_after_dot bp c strm =
| [< (t,_) = process_chars bp c >] -> t
else
match strm with parser
+ | [< ' ('a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
+ ("FIELD", get_buff len)
+ (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
+ | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2);
+ len = ident (store (store 0 c1) c2) >] ->
+ ("FIELD", get_buff len)
+ (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
+ | [< ''\226' as c1; t = parse_226_tail
+ (progress_special '.' (Some !token_tree)) >] ep ->
+ (match t with
+ | TokSymbol (Some t) -> ("", t)
+ | TokSymbol None -> err (bp, ep) Undefined_token
+ | TokIdent t -> ("FIELD", t))
| [< (t,_) = process_chars bp c >] -> t
@@ -384,10 +398,20 @@ let rec next_token = parser bp
comment_stop bp;
if !Options.v7 & t=("",".") then between_com := true;
(t, (bp,ep))
- | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
+ | [< ' ('a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
let id = get_buff len in
comment_stop bp;
(try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
+ | [< ''_' as c; s >] ->
+ if !Options.v7 then
+ (match s with parser [< len = ident (store 0 c) >] ep ->
+ let id = get_buff len in
+ comment_stop bp;
+ (try ("", find_keyword id) with Not_found -> ("IDENT", id)),
+ (bp, ep))
+ else
+ (match s with parser [< t = process_chars bp c >] ->
+ comment_stop bp; t)
(* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
| [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2);
len = ident (store (store 0 c1) c2) >] ep ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 9bb2a86b9..1f462b615 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -348,7 +348,8 @@ module Constr =
let annot = Gram.Entry.create "constr:annot"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
- let binder_let = Gram.Entry.create "constr:binder_list"
+ let binder = Gram.Entry.create "constr:binder"
+ let binder_let = Gram.Entry.create "constr:binder_let"
let tuple_constr = gec_constr "tuple_constr"
end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8f393030e..1c7a1932f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -139,6 +139,7 @@ module Constr :
val annot : constr_expr Gram.Entry.e
val constr_pattern : constr_expr Gram.Entry.e
val lconstr_pattern : constr_expr Gram.Entry.e
+ val binder : (name located list * constr_expr) Gram.Entry.e
val binder_let : local_binder Gram.Entry.e
val tuple_constr : constr_expr Gram.Entry.e
end
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d24de5675..166db8675 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -411,7 +411,7 @@ and pr_atom1 = function
| TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
| TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
- hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
+ hov 1 (str "Fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
hov 0 (str "with" ++ brk (1,1) ++
prlist_with_sep spc
(fun (id,n,c) ->
@@ -444,12 +444,12 @@ and pr_atom1 = function
hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c)
(* Derived basic tactics *)
- | TacOldInduction h ->
+ | TacSimpleInduction h ->
hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
| TacNewInduction (h,e,ids) ->
hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
pr_opt pr_eliminator e ++ pr_with_names ids)
- | TacOldDestruct h ->
+ | TacSimpleDestruct h ->
hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
| TacNewDestruct (h,e,ids) ->
hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6b89169b5..44e78462f 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -376,14 +376,14 @@ let rec mlexpr_of_atomic_tactic = function
<:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
(* Derived basic tactics *)
- | Tacexpr.TacOldInduction h ->
- <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
+ | Tacexpr.TacSimpleInduction h ->
+ <:expr< Tacexpr.TacSimpleInduction $mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacNewInduction (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
<:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
- | Tacexpr.TacOldDestruct h ->
- <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
+ | Tacexpr.TacSimpleDestruct h ->
+ <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
| Tacexpr.TacNewDestruct (c,cbo,ids) ->
let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 75ebb2d28..c6453f076 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -109,10 +109,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacInstantiate of int * 'constr
(* Derived basic tactics *)
- | TacOldInduction of quantified_hypothesis
+ | TacSimpleInduction of quantified_hypothesis
| TacNewInduction of 'constr induction_arg * 'constr with_bindings option
* intro_pattern_expr list list
- | TacOldDestruct of quantified_hypothesis
+ | TacSimpleDestruct of quantified_hypothesis
| TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
* intro_pattern_expr list list
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0e8725c6a..046ae4ed1 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -50,8 +50,10 @@ let h_instantiate n c =
abstract_tactic (TacInstantiate (n,c)) (Evar_refiner.instantiate n c)
(* Derived basic tactics *)
-let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h)
-let h_old_destruct h = abstract_tactic (TacOldDestruct h) (old_destruct h)
+let h_simple_induction h =
+ abstract_tactic (TacSimpleInduction h) (simple_induct h)
+let h_simple_destruct h =
+ abstract_tactic (TacSimpleDestruct h) (simple_destruct h)
let h_new_induction c e idl =
abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl)
let h_new_destruct c e idl =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index dba9908a9..82146c01a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -53,8 +53,8 @@ val h_instantiate : int -> constr -> tactic
(* Derived basic tactics *)
-val h_old_induction : quantified_hypothesis -> tactic
-val h_old_destruct : quantified_hypothesis -> tactic
+val h_simple_induction : quantified_hypothesis -> tactic
+val h_simple_destruct : quantified_hypothesis -> tactic
val h_new_induction :
constr induction_arg -> constr with_bindings option ->
intro_pattern_expr list list -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ccd22cc73..7f1a0943a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -587,12 +587,14 @@ let rec intern_atomic lf ist x =
| TacDAuto (n,p) -> TacDAuto (n,p)
(* Derived basic tactics *)
- | TacOldInduction h -> TacOldInduction (intern_quantified_hypothesis ist h)
+ | TacSimpleInduction h ->
+ TacSimpleInduction (intern_quantified_hypothesis ist h)
| TacNewInduction (c,cbo,ids) ->
TacNewInduction (intern_induction_arg ist c,
option_app (intern_constr_with_bindings ist) cbo,
List.map (List.map (intern_intro_pattern lf ist)) ids)
- | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h)
+ | TacSimpleDestruct h ->
+ TacSimpleDestruct (intern_quantified_hypothesis ist h)
| TacNewDestruct (c,cbo,ids) ->
TacNewDestruct (intern_induction_arg ist c,
option_app (intern_constr_with_bindings ist) cbo,
@@ -1602,13 +1604,14 @@ and interp_atomic ist gl = function
| TacDAuto (n,p) -> Auto.h_dauto (n,p)
(* Derived basic tactics *)
- | TacOldInduction h ->
- h_old_induction (interp_quantified_hypothesis ist gl h)
+ | TacSimpleInduction h ->
+ h_simple_induction (interp_quantified_hypothesis ist gl h)
| TacNewInduction (c,cbo,ids) ->
h_new_induction (interp_induction_arg ist gl c)
(option_app (interp_constr_with_bindings ist gl) cbo)
(List.map (List.map (interp_intro_pattern ist)) ids)
- | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist gl h)
+ | TacSimpleDestruct h ->
+ h_simple_destruct (interp_quantified_hypothesis ist gl h)
| TacNewDestruct (c,cbo,ids) ->
h_new_destruct (interp_induction_arg ist gl c)
(option_app (interp_constr_with_bindings ist gl) cbo)
@@ -1831,11 +1834,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacDAuto (n,p) -> TacDAuto (n,p)
(* Derived basic tactics *)
- | TacOldInduction h as x -> x
+ | TacSimpleInduction h as x -> x
| TacNewInduction (c,cbo,ids) ->
TacNewInduction (subst_induction_arg subst c,
option_app (subst_raw_with_bindings subst) cbo, ids)
- | TacOldDestruct h as x -> x
+ | TacSimpleDestruct h as x -> x
| TacNewDestruct (c,cbo,ids) ->
TacNewDestruct (subst_induction_arg subst c,
option_app (subst_raw_with_bindings subst) cbo, ids)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4f9ab4ad1..f38be2f24 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1459,24 +1459,24 @@ let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
(* This was Induction in 6.3 (hybrid form) *)
-let old_induct_id s =
+let simple_induct_id s =
tclORELSE (raw_induct s) (induction_from_context true true None s [])
-let old_induct_nodep = raw_induct_nodep
+let simple_induct_nodep = raw_induct_nodep
-let old_induct = function
- | NamedHyp id -> old_induct_id id
- | AnonHyp n -> old_induct_nodep n
+let simple_induct = function
+ | NamedHyp id -> simple_induct_id id
+ | AnonHyp n -> simple_induct_nodep n
(* Destruction tactics *)
-let old_destruct_id s =
+let simple_destruct_id s =
(tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case))
-let old_destruct_nodep n =
+let simple_destruct_nodep n =
(tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case))
-let old_destruct = function
- | NamedHyp id -> old_destruct_id id
- | AnonHyp n -> old_destruct_nodep n
+let simple_destruct = function
+ | NamedHyp id -> simple_destruct_id id
+ | AnonHyp n -> simple_destruct_nodep n
(*
* Eliminations giving the type instead of the proof.
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 38c31f015..1f4c5b35c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -172,7 +172,7 @@ val elim : constr with_bindings -> constr with_bindings option -> tacti
val general_elim_in : identifier -> constr * constr bindings ->
constr * constr bindings -> tactic
-val old_induct : quantified_hypothesis -> tactic
+val simple_induct : quantified_hypothesis -> tactic
val general_elim_in : identifier -> constr * constr bindings ->
constr * constr bindings -> tactic
@@ -184,7 +184,7 @@ val new_induct : constr induction_arg -> constr with_bindings option ->
val general_case_analysis : constr with_bindings -> tactic
val simplest_case : constr -> tactic
-val old_destruct : quantified_hypothesis -> tactic
+val simple_destruct : quantified_hypothesis -> tactic
val new_destruct : constr induction_arg -> constr with_bindings option ->
intro_pattern_expr list list -> tactic
diff --git a/test-suite/check b/test-suite/check
index aa6bef1eb..3a10d0e16 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -82,7 +82,7 @@ test_parser() {
printf " "$f"..."
tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
foutput=`dirname $f`/`basename $f .v`.out
- echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1
+ echo "parse_file 1 \"$f\"" | ../bin/parser -v7 > $tmpoutput 2>&1
perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \
$tmpoutput | diff - $foutput > /dev/null
if [ $? = 0 ] ; then
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
new file mode 100644
index 000000000..102e67db6
--- /dev/null
+++ b/theories/Init/LogicSyntax.v
@@ -0,0 +1,47 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Notations.
+Require Export Logic.
+
+(** Symbolic notations for things in [Logic.v] *)
+
+(* Order is important to give printing priority to fully typed ALL and
+ exists *)
+
+V7only [ Notation All := (all ?). ].
+Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8)
+ V8only "'ALL' x , p" (at level 200, p at level 200).
+Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
+ V8only "'ALL' x : t , p" (at level 200).
+
+V7only [ Notation Ex := (ex ?). ].
+Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8)
+ V8only "'exists' x , p" (at level 200, x at level 80).
+Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8)
+ V8only "'exists' x : t , p" (at level 200, x at level 80).
+
+V7only [ Notation Ex2 := (ex2 ?). ].
+Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q)
+ (at level 10, p, q at level 8)
+ V8only "'exists2' x , p & q" (at level 200, x at level 80).
+Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q)
+ (at level 10, p, q at level 8)
+ V8only "'exists2' x : t , p & q" (at level 200, x at level 80).
+
+V7only[
+(** Parsing only of things in [Logic.v] *)
+
+Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing).
+Notation "< A > x = y" := (eq A x y)
+ (A annot, at level 1, x at level 0, only parsing).
+Notation "< A > x <> y" := ~(eq A x y)
+ (A annot, at level 1, x at level 0, only parsing).
+].
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1211faba0..45af3a3c5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -616,6 +616,9 @@ let make_syntax_rule n name symbols typs ast ntn sc =
syn_hunks =
[UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
+let make_pp_rule (n,typs,symbols) =
+ [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
+
let make_pp_rule (n,typs,symbols,fmt) =
match fmt with
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
@@ -875,7 +878,6 @@ let make_old_pp_rule n symbols typs r ntn scope vars =
let add_notation_in_scope local df c mods omodv8 scope toks =
let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata)) =
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 *)
@@ -885,21 +887,23 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
(* 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 ppprec,pp_rule =
+ let ppnot,ppprec,pp_rule =
match omodv8 with
- | Some mv8 -> let _,p,d = compute_syntax_data false mv8 in p,make_pp_rule d
+ | Some mv8 ->
+ let (_,_,ntn8),p,d = compute_syntax_data false mv8 in
+ ntn8,p,make_pp_rule d
| _ ->
(* means the rule already exists: recover it *)
try
let _, oldprec8 = Symbols.level_of_notation notation in
let rule,_ = Symbols.find_notation_printing_rule notation in
- oldprec8,rule
+ notation,oldprec8,rule
with Not_found -> error "No known parsing rule for this notation in V8"
in
- let gram_rule = make_grammar_rule n typs symbols notation in
+ let gram_rule = make_grammar_rule n typs symbols ppnot in
Lib.add_anonymous_leaf
(inSyntaxExtension
- (local,(Some prec,ppprec),notation,Some gram_rule,pp_rule));
+ (local,(Some prec,ppprec),ppnot,Some gram_rule,pp_rule));
(* Declare interpretation *)
let a = interp_aconstr vars c in
@@ -912,7 +916,7 @@ let add_notation_in_scope local df c mods omodv8 scope toks =
let onlyparse = onlyparse or !Options.v7_only in
let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
Lib.add_anonymous_leaf
- (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,false,df))
+ (inNotation(local,old_pp_rule,ppnot,scope,a,onlyparse,false,df))
let level_rule (n,p) = if p = E then n else max (n-1) 0
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 853b3f594..00020a85a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,10 +100,11 @@ let parse_phrase (po, verbch) =
let just_parsing = ref false
let chan_translate = ref stdout
-
let pr_new_syntax loc ocom =
- Format.set_formatter_out_channel !chan_translate;
- Format.set_max_boxes max_int;
+ if !translate_file then begin
+ Format.set_formatter_out_channel !chan_translate;
+ Format.set_max_boxes max_int;
+ end;
let fs = States.freeze () in
let com = match ocom with
| Some (VernacV7only _) ->
@@ -117,11 +118,7 @@ let pr_new_syntax loc ocom =
| Some com -> pr_vernac com
| None -> mt() in
if !translate_file then
- msg (hov 0 (
-(*str"{"++int (fst loc)++str"}"++List.fold_right (fun ((b,e),s) strm -> str"("++int b++str","++int
- e++str":"++str s++str")"++strm)
- !Pp.comments (mt()) ++*)
-comment (fst loc) ++ com ++ comment (snd loc - 1)))
+ msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
else
msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com));
States.unfreeze fs;
@@ -135,7 +132,7 @@ let rec vernac_com interpfun (loc,com) =
let ch = !chan_translate in
let cs = Lexer.com_state() in
let cl = !Pp.comments in
- if Options.do_translate() then begin
+ if !Options.translate_file then begin
let _,f = find_file_in_path (Library.get_load_path ())
(make_suffix fname ".v") in
chan_translate := open_out (f^"8");
@@ -143,12 +140,12 @@ let rec vernac_com interpfun (loc,com) =
end;
begin try
read_vernac_file verbosely (make_suffix fname ".v");
- if Options.do_translate () then close_out !chan_translate;
+ if !Options.translate_file then close_out !chan_translate;
chan_translate := ch;
Lexer.restore_com_state cs;
Pp.comments := cl
with e ->
- if Options.do_translate() then close_out !chan_translate;
+ if !Options.translate_file then close_out !chan_translate;
chan_translate := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
@@ -221,12 +218,12 @@ let raw_do_vernac po =
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
chan_translate :=
- if Options.do_translate () then open_out (file^"8") else stdout;
+ if !Options.translate_file then open_out (file^"8") else stdout;
try
read_vernac_file verb file;
- if Options.do_translate () then close_out !chan_translate;
+ if !Options.translate_file then close_out !chan_translate;
with e ->
- if Options.do_translate () then close_out !chan_translate;
+ if !Options.translate_file then close_out !chan_translate;
raise_with_file file e
(* Compile a vernac file (f is assumed without .v suffix) *)
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 03e83caca..27ddc4d1a 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -389,32 +389,6 @@ let pr_app pr a l =
pr (lapp,L) a ++
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
-
-let cs = function
- | CRef(Ident(_,i)) -> "ID"
- | CRef(Qualid(_,q)) -> "Q"
- | CFix(_,x,a) -> "FX"
- | CCoFix(_,x,a) -> "CFX"
- | CArrow(_,a,b) -> "->"
- | CProdN(_,bl,a) -> "Pi"
- | CLambdaN(_,bl,a) -> "L"
- | CLetIn(_,x,a,b) -> "LET"
- | CAppExpl(_,f,a) -> "@E"
- | CApp(_,f,a) -> "@"
- | CCases(_,p,a,br) -> "C"
- | COrderedCase(_,s,p,a,br) -> "OC"
- | CLetTuple(_,ids,p,a,b) -> "LC"
- | CIf(_,e,p,a,b) -> "LI"
- | CHole _ -> "?"
- | CPatVar(_,v) -> "PV"
- | CEvar(_,ev) -> "EV"
- | CSort(_,s) -> "S"
- | CCast(_,a,b) -> "::"
- | CNotation(_,n,l) -> "NOT"
- | CNumeral(_,i) -> "NUM"
- | CDelimiters(_,s,e) -> "DEL"
- | CDynamic(_,d) -> "DYN"
-
let rec pr inherited a =
let (strm,prec) = match a with
| CRef r -> pr_reference r, latom
@@ -441,6 +415,12 @@ let rec pr inherited a =
str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
str " =>" ++ spc() ++ pr ltop a),
llambda
+ | CLetIn (_,(_,Name x),(CFix(_,(_,x'),_)|CCoFix(_,(_,x'),_) as fx), b)
+ when x=x' ->
+ hv 0 (
+ hov 2 (str "let " ++ pr ltop fx ++ str " in") ++
+ spc () ++ pr ltop b),
+ lletin
| CLetIn (_,x,a,b) ->
hv 0 (
hov 2 (str "let " ++ pr_located pr_name x ++ str " :=" ++ spc() ++
@@ -559,7 +539,7 @@ let rec strip_context n iscast t =
let n' = List.length nal in
if n' > n then
let nal1,nal2 = list_chop n nal in
- [LocalRawAssum (nal1,t)], CLambdaN (loc,(nal2,t)::bll,c)
+ [LocalRawAssum (nal1,t)], CProdN (loc,(nal2,t)::bll,c)
else
let bl', c = strip_context (n-n') iscast
(if bll=[] then c else CProdN (loc,bll,c)) in
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 335160f6b..5b04a7c34 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -23,6 +23,21 @@ open Genarg
open Libnames
open Pptactic
+let strip_prod_binders_expr n ty =
+ let rec strip_ty acc n ty =
+ match ty with
+ Topconstr.CProdN(_,bll,a) ->
+ let nb =
+ List.fold_left (fun i (nal,_) -> i + List.length nal) 0 bll in
+ if nb >= n then (List.rev (bll@acc), a)
+ else strip_ty (bll@acc) (n-nb) a
+ | Topconstr.CArrow(_,a,b) ->
+ if n=1 then
+ (List.rev (([(dummy_loc,Anonymous)],a)::acc), b)
+ else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
(* In v8 syntax only double quote char is escaped by repeating it *)
let rec escape_string_v8 s =
let rec escape_at s i =
@@ -281,9 +296,10 @@ let rec pr_tacarg_using_rule pr_gen = function
let pr_then () = str ";"
+
open Closure
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) =
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
@@ -294,6 +310,52 @@ let pr_lconstrarg env c = spc () ++ pr_lconstr env c in
let pr_intarg n = spc () ++ int n in
+let pr_binder_fix env (nal,t) =
+(* match t with
+ | CHole _ -> spc() ++ prlist_with_sep spc (pr_located pr_name) nal
+ | _ ->*)
+ let s =
+ prlist_with_sep spc (pr_located pr_name) nal ++ str ":" ++
+ pr_lconstr env t in
+ spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+let pr_fix_tac env (id,n,c) =
+ let rec set_nth_name avoid n = function
+ (nal,ty)::bll ->
+ if n <= List.length nal then
+ match list_chop (n-1) nal with
+ _, (_,Name id) :: _ -> id, (nal,ty)::bll
+ | bef, (loc,Anonymous) :: aft ->
+ let id = next_ident_away_from (id_of_string"y") avoid in
+ id, ((bef@(loc,Name id)::aft, ty)::bll)
+ | _ -> assert false
+ else
+ let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+ (id,(nal,ty)::bll')
+ | [] -> assert false in
+ let (bll,ty) = strip_prod_binders n c in
+ let names =
+ List.fold_left
+ (fun ln (nal,_) -> List.fold_left
+ (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+ ln nal)
+ [] bll in
+ let idarg,bll = set_nth_name names n bll in
+ let annot =
+ if List.length names = 1 then mt()
+ else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in
+ spc() ++ str"with " ++
+ hov 0 (pr_id id ++
+ prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ spc() ++
+ pr_lconstr env ty) in
+(* spc() ++
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+ env c)
+*)
+let pr_cofix_tac env (id,c) =
+ spc() ++ str"with " ++ hov 0 (pr_id id ++ str":" ++ pr_constrarg env c) in
+
+
(* Printing tactics as arguments *)
let rec pr_atom0 env = function
| TacIntroPattern [] -> str "intros"
@@ -311,7 +373,7 @@ let rec pr_atom0 env = function
(* Main tactic printer *)
and pr_atom1 env = function
| TacExtend (loc,s,l) ->
- pr_with_comments loc
+ pr_with_comments loc
(pr_extend (pr_constr env) (pr_lconstr env) (pr_tac env) s l)
| TacAlias (loc,s,l,_) ->
pr_with_comments loc
@@ -341,36 +403,26 @@ and pr_atom1 env = function
| TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
| TacMutualFix (id,n,l) ->
- hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
- hv 0 (str "with" ++ brk (1,1) ++
- prlist
- (fun (id,n,c) ->
- spc() ++
- hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg env c))
- l))
+ hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++
+ prlist (pr_fix_tac env) l)
| TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
| TacMutualCofix (id,l) ->
hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc () ++
- hv 0 (str "with" ++ brk (1,1) ++
- prlist
- (fun (id,c) ->
- spc() ++
- hov 0 (pr_id id ++ str":" ++ pr_constrarg env c))
- l))
+ prlist (pr_cofix_tac env) l)
| TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
| TacTrueCut (None,c) ->
hov 1 (str "assert" ++ pr_constrarg env c)
| TacTrueCut (Some id,c) ->
- hov 1 (str "assert" ++ spc () ++ pr_id id ++ str ":" ++
- pr_lconstrarg env c)
+ hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_id id ++ str ":" ++
+ pr_lconstrarg env c ++ str")")
| TacForward (false,na,c) ->
- hov 1 (str "assert" ++ pr_arg pr_name na ++ str " :=" ++
- pr_lconstrarg env c)
+ hov 1 (str "assert" ++ spc () ++ str"(" ++ pr_name na ++ str " :=" ++
+ pr_lconstrarg env c ++ str")")
| TacForward (true,Anonymous,c) ->
hov 1 (str "pose" ++ pr_constrarg env c)
| TacForward (true,Name id,c) ->
- hov 1 (str "pose" ++ pr_arg pr_id id ++ str " :=" ++
- pr_lconstrarg env c)
+ hov 1 (str "pose" ++ spc() ++ str"(" ++ pr_id id ++ str " :=" ++
+ pr_lconstrarg env c ++ str")")
| TacGeneralize l ->
hov 1 (str "generalize" ++ spc () ++
prlist_with_sep spc (pr_constr env) l)
@@ -378,20 +430,21 @@ and pr_atom1 env = function
hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
pr_constrarg env c)
| TacLetTac (id,c,cl) ->
- hov 1 (str "lettac" ++ spc () ++ pr_id id ++ str " :=" ++
- pr_constrarg env c ++ pr_clause_pattern pr_ident cl)
+ hov 1 (str "lettac" ++ spc () ++ str"(" ++ pr_id id ++ str " :=" ++
+ pr_lconstrarg env c ++ str")" ++ pr_clause_pattern pr_ident cl)
| TacInstantiate (n,c) ->
- hov 1 (str "instantiate" ++ pr_arg int n ++ pr_constrarg env c)
+ hov 1 (str "instantiate" ++ pr_arg int n ++ str":=" ++
+ pr_lconstrarg env c ++ str")")
(* Derived basic tactics *)
- | TacOldInduction h ->
- hov 1 (str "oldinduction" ++ pr_arg pr_quantified_hypothesis h)
+ | TacSimpleInduction h ->
+ hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h)
| TacNewInduction (h,e,ids) ->
hov 1 (str "induction" ++ spc () ++
pr_induction_arg (pr_constr env) h ++
pr_opt (pr_eliminator env) e ++ pr_with_names ids)
- | TacOldDestruct h ->
- hov 1 (str "olddestruct" ++ pr_arg pr_quantified_hypothesis h)
+ | TacSimpleDestruct h ->
+ hov 1 (str "simple_destruct" ++ pr_arg pr_quantified_hypothesis h)
| TacNewDestruct (h,e,ids) ->
hov 1 (str "destruct" ++ spc () ++
pr_induction_arg (pr_constr env) h ++
@@ -619,6 +672,25 @@ let pi1 (a,_,_) = a
let pi2 (_,a,_) = a
let pi3 (_,_,a) = a
+let strip_prod_binders_rawterm n (ty,_) =
+ let rec strip_ty acc n ty =
+ if n=0 then (List.rev acc, (ty,None)) else
+ match ty with
+ Rawterm.RProd(loc,na,a,b) ->
+ strip_ty (([dummy_loc,na],(a,None))::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+let strip_prod_binders_constr n ty =
+ let rec strip_ty acc n ty =
+ if n=0 then (List.rev acc, ty) else
+ match Term.kind_of_term ty with
+ Term.Prod(na,a,b) ->
+ strip_ty (([dummy_loc,na],a)::acc) (n-1) b
+ | _ -> error "Cannot translate fix tactic: not enough products" in
+ strip_ty [] n ty
+
+
let rec raw_printers =
(pr_raw_tactic,
pr_raw_tactic0,
@@ -629,7 +701,8 @@ let rec raw_printers =
(fun _ -> pr_reference),
pr_reference,
pr_or_metaid (pr_located pr_id),
- Pptactic.pr_raw_extend)
+ Pptactic.pr_raw_extend,
+ strip_prod_binders_expr)
and pr_raw_tactic env (t:raw_tactic_expr) =
pi1 (make_pr_tac raw_printers) env t
@@ -642,6 +715,7 @@ and pr_raw_match_rule env t =
let pr_and_constr_expr pr (c,_) = pr c
+
let rec glob_printers =
(pr_glob_tactic,
pr_glob_tactic0,
@@ -652,7 +726,8 @@ let rec glob_printers =
(fun vars -> pr_or_var (pr_inductive vars)),
pr_ltac_or_var (pr_located pr_ltac_constant),
pr_located pr_id,
- Pptactic.pr_glob_extend)
+ Pptactic.pr_glob_extend,
+ strip_prod_binders_rawterm)
and pr_glob_tactic env (t:glob_tactic_expr) =
pi1 (make_pr_tac glob_printers) env t
@@ -674,4 +749,5 @@ let (pr_tactic,_,_) =
pr_inductive,
pr_ltac_constant,
pr_id,
- Pptactic.pr_extend)
+ Pptactic.pr_extend,
+ strip_prod_binders_constr)
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 1e392b548..ebf6a14d0 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -579,7 +579,9 @@ let rec pr_vernac = function
let ps =
let n = String.length s in
if n > 2 & s.[0] = '\'' & s.[n-1] = '\''
- then str (String.sub s 1 (n-2))
+ then
+ let s' = String.sub s 1 (n-2) in
+ if String.contains s' '\'' then qsnew s else str s'
else qsnew s in
hov 2( str"Notation" ++ spc() ++ pr_locality local ++ ps ++
str " :=" ++ pr_constrarg c ++ pr_syntax_modifiers l ++
@@ -619,10 +621,11 @@ let rec pr_vernac = function
(bl2,body,mt())
| Some ty ->
let bl2,body,ty' = extract_def_binders c ty in
- (bl2,CCast (dummy_loc,body,ty'), spc() ++ str":" ++ spc () ++
- pr_type_env_n (Global.env())
- (local_binders_length bl + local_binders_length bl2)
- (prod_rawconstr ty bl)) in
+ (bl2,CCast (dummy_loc,body,ty'),
+ spc() ++ str":" ++ spc () ++
+ pr_type_env_n (Global.env())
+ (local_binders_length bl + local_binders_length bl2)
+ (prod_rawconstr ty bl)) in
let n = local_binders_length bl + local_binders_length bl2 in
let iscast = d <> None in
let bindings,ppred =
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 06:35:44 +0000