From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- parsing/argextend.ml4 | 26 ++++-- parsing/egrammar.ml | 48 +++++----- parsing/g_constr.ml4 | 64 +++++++++---- parsing/g_ltac.ml4 | 19 +++- parsing/g_prim.ml4 | 4 +- parsing/g_proofs.ml4 | 17 ++-- parsing/g_tactic.ml4 | 78 ++++++++-------- parsing/g_vernac.ml4 | 227 ++++++++++++++++++++++++----------------------- parsing/lexer.ml4 | 49 ++++++---- parsing/pcoq.ml4 | 5 +- parsing/pcoq.mli | 5 +- parsing/ppconstr.ml | 112 +++++++++++++---------- parsing/ppconstr.mli | 10 +-- parsing/pptactic.ml | 59 ++++++------ parsing/ppvernac.ml | 172 ++++++++++++++++++----------------- parsing/prettyp.ml | 13 ++- parsing/prettyp.mli | 4 +- parsing/printer.ml | 19 ++-- parsing/printmod.ml | 6 +- parsing/q_constr.ml4 | 4 +- parsing/q_coqast.ml4 | 44 +++++---- parsing/search.ml | 17 +--- parsing/search.mli | 9 +- parsing/vernacextend.ml4 | 5 +- 24 files changed, 569 insertions(+), 447 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 57e88133..bd6be424 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: argextend.ml4 10122 2007-09-15 10:35:59Z letouzey $ *) +(* $Id: argextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *) open Genarg open Q_util @@ -25,7 +25,7 @@ let rec make_rawwit loc = function | StringArgType -> <:expr< Genarg.rawwit_string >> | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.rawwit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.rawwit_ident >> + | IdentArgType b -> <:expr< Genarg.rawwit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.rawwit_var >> | RefArgType -> <:expr< Genarg.rawwit_ref >> | SortArgType -> <:expr< Genarg.rawwit_sort >> @@ -50,7 +50,7 @@ let rec make_globwit loc = function | StringArgType -> <:expr< Genarg.globwit_string >> | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.globwit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.globwit_ident >> + | IdentArgType b -> <:expr< Genarg.globwit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.globwit_var >> | RefArgType -> <:expr< Genarg.globwit_ref >> | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> @@ -75,7 +75,7 @@ let rec make_wit loc = function | StringArgType -> <:expr< Genarg.wit_string >> | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >> - | IdentArgType -> <:expr< Genarg.wit_ident >> + | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >> | VarArgType -> <:expr< Genarg.wit_var >> | RefArgType -> <:expr< Genarg.wit_ref >> | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> @@ -163,16 +163,27 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = end >> -let declare_vernac_argument loc s cl = +let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in + let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in + let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in + let pr_rules = match pr with + | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in <:str_item< declare - value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x; + value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel), + ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel), + $lid:"rawwit_"^s$) = Genarg.create_arg $se$; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; + Pptactic.declare_extra_genarg_pprule + ($rawwit$, $pr_rules$) + ($globwit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not globwit printer") + ($wit$, fun _ _ _ _ -> Util.anomaly "vernac argument needs not wit printer"); end >> @@ -202,11 +213,12 @@ EXTEND failwith "Argument entry names must be lowercase"; declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; + pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_vernac_argument loc s l ] ] + declare_vernac_argument loc s pr l ] ] ; argtype: [ "2" diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 825d1af0..43836dbb 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: egrammar.ml 11512 2008-10-27 12:28:36Z herbelin $ *) open Pp open Util @@ -52,58 +52,56 @@ type prod_item = | NonTerm of constr_production_entry * (Names.identifier * constr_production_entry) option -type 'a action_env = (identifier * 'a) list +type 'a action_env = 'a list * 'a list list let make_constr_action (f : loc -> constr_expr action_env -> constr_expr) pil = - let rec make (env : constr_expr action_env) = function + let rec make (env,envlist as fullenv : constr_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc env) + Gramext.action (fun loc -> f loc fullenv) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gramext.action (fun _ -> make fullenv tl) | Some (p, (ETConstr _| ETOther _)) :: tl -> (* constr non-terminal *) - Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl) + Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl) | Some (p, ETReference) :: tl -> (* non-terminal *) - Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl) + Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl) | Some (p, ETIdent) :: tl -> (* non-terminal *) Gramext.action (fun (v:identifier) -> - make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) + make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) Gramext.action (fun (v:Bigint.bigint) -> - make ((p,CPrim (dummy_loc,Numeral v)) :: env) tl) + make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl) | Some (p, ETConstrList _) :: tl -> - Gramext.action (fun (v:constr_expr list) -> - let dummyid = Ident (dummy_loc,id_of_string "_") in - make ((p,CAppExpl (dummy_loc,(None,dummyid),v)) :: env) tl) + Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) | Some (p, ETPattern) :: tl -> failwith "Unexpected entry of type cases pattern" in - make [] (List.rev pil) + make ([],[]) (List.rev pil) let make_cases_pattern_action (f : loc -> cases_pattern_expr action_env -> cases_pattern_expr) pil = - let rec make (env : cases_pattern_expr action_env) = function + let rec make (env,envlist as fullenv : cases_pattern_expr action_env) = function | [] -> - Gramext.action (fun loc -> f loc env) + Gramext.action (fun loc -> f loc fullenv) | None :: tl -> (* parse a non-binding item *) - Gramext.action (fun _ -> make env tl) + Gramext.action (fun _ -> make fullenv tl) | Some (p, ETConstr _) :: tl -> (* pattern non-terminal *) - Gramext.action (fun (v:cases_pattern_expr) -> make ((p,v) :: env) tl) + Gramext.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) | Some (p, ETReference) :: tl -> (* non-terminal *) Gramext.action (fun (v:reference) -> - make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl) + make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) | Some (p, ETIdent) :: tl -> (* non-terminal *) Gramext.action (fun (v:identifier) -> - make ((p,CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))) :: env) tl) + make + (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl) | Some (p, ETBigint) :: tl -> (* non-terminal *) Gramext.action (fun (v:Bigint.bigint) -> - make ((p,CPatPrim (dummy_loc,Numeral v)) :: env) tl) + make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:cases_pattern_expr list) -> - let dummyid = Ident (dummy_loc,id_of_string "_") in - make ((p,CPatCstr (dummy_loc,dummyid,v)) :: env) tl) + make (env, v :: envlist) tl) | Some (p, (ETPattern | ETOther _)) :: tl -> failwith "Unexpected entry of type cases pattern or other" in - make [] (List.rev pil) + make ([],[]) (List.rev pil) let make_constr_prod_item univ assoc from forpat = function | Term tok -> (Gramext.Stoken tok, None) @@ -133,11 +131,11 @@ let extend_constr (entry,level) (n,assoc) mkact forpat pt = let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) - let mkact loc env = CNotation (loc,ntn,List.map snd env) in + let mkact loc env = CNotation (loc,ntn,env) in let e = get_constr_entry false (ETConstr (n,())) in extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule; (* Add the notation in cases_pattern *) - let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in + let mkact loc env = CPatNotation (loc,ntn,env) in let e = get_constr_entry true (ETConstr (n,())) in extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rule diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b93fdadd..cdce13e6 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_constr.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: g_constr.ml4 11709 2008-12-20 11:42:15Z msozeau $ *) open Pcoq open Constr @@ -24,7 +24,8 @@ 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 _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw @@ -41,6 +42,11 @@ let loc_of_binder_let = function | LocalRawDef ((loc,_),_)::_ -> loc | _ -> dummy_loc +let binders_of_lidents l = + List.map (fun (loc, id) -> + LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + CHole (loc, Some (Evd.BinderType (Name id))))) l + let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with | [loc,Name id], (None, r) -> Some (loc, id), r @@ -124,12 +130,24 @@ let ident_colon = | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) +let ident_with = + Gram.Entry.of_parser "ident_with" + (fun strm -> + match Stream.npeek 1 strm with + | [("IDENT",s)] -> + (match Stream.npeek 2 strm with + | [_; ("", "with")] -> + Stream.junk strm; Stream.junk strm; + Names.id_of_string s + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident - binder binder_let binders_let + binder binder_let binders_let record_declaration binders_let_fixannot typeclass_constraint pattern appl_arg; Constr.ident: [ [ id = Prim.ident -> id @@ -202,8 +220,14 @@ GEXTEND Gram | "("; c = operconstr LEVEL "200"; ")" -> (match c with CPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CNotation(loc,"( _ )",[c]) - | _ -> c) ] ] + CNotation(loc,"( _ )",([c],[])) + | _ -> c) + | "{|"; c = record_declaration; "|}" -> c + | "`{"; c = operconstr LEVEL "200"; "}" -> + CGeneralization (loc, Implicit, None, c) + | "`("; c = operconstr LEVEL "200"; ")" -> + CGeneralization (loc, Explicit, None, c) + ] ] ; forall: [ [ "forall" -> () @@ -215,6 +239,16 @@ GEXTEND Gram | IDENT "λ" -> () ] ] ; + record_declaration: + [ [ fs = LIST1 record_field_declaration SEP ";" -> CRecord (loc, None, fs) +(* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) +(* CRecord (loc, Some c, fs) *) + ] ] + ; + record_field_declaration: + [ [ id = identref; params = LIST0 identref; ":="; c = lconstr -> + (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ] + ; binder_constr: [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" -> mkCProdN loc bl c @@ -337,7 +371,7 @@ GEXTEND Gram | "("; p = pattern LEVEL "200"; ")" -> (match p with CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z -> - CPatNotation(loc,"( _ )",[p]) + CPatNotation(loc,"( _ )",([p],[])) | _ -> p) | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n)) | s = string -> CPatPrim (loc, String s) ] ] @@ -398,12 +432,10 @@ GEXTEND Gram [LocalRawAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) - | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc - | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc - | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc + | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc + | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc ] ] ; binder: @@ -413,13 +445,13 @@ GEXTEND Gram ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c - | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c + | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> id, expl, c - | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> (loc, Name iid), expl, c | c = operconstr LEVEL "200" -> - (loc, Anonymous), Implicit, c + (loc, Anonymous), false, c ] ] ; diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index dbd81e7f..316bf8e1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: g_ltac.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) open Pp open Util @@ -165,11 +165,24 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (oid, pc) + Subterm (false,oid, pc) + | IDENT "appcontext"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + Subterm (true,oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] + [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) + | na = name; ":="; mpv = match_pattern -> + let t, ty = + match mpv with + | Term t -> (match t with + | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) + | _ -> mpv, None) + | _ -> mpv, None + in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty) + ] ] ; match_context_rule: [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 1e738384..76225d77 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(*i $Id: g_prim.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: g_prim.ml4 11525 2008-10-30 22:18:54Z amahboub $ i*) open Pcoq open Names @@ -45,7 +45,7 @@ GEXTEND Gram [ [ s = IDENT -> id_of_string s ] ] ; pattern_ident: - [ [ s = PATTERNIDENT -> id_of_string s ] ] + [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: [ [ id = pattern_ident -> (loc, id) ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 05878e97..655bb267 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_proofs.ml4 10628 2008-03-06 14:56:08Z msozeau $ *) +(* $Id: g_proofs.ml4 11784 2009-01-14 11:36:32Z herbelin $ *) open Pcoq @@ -90,9 +90,12 @@ GEXTEND Gram | IDENT "Go"; IDENT "next" -> VernacGo GoNext | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) - | IDENT "Hint"; local = locality; h = hint; + | IDENT "Create"; IDENT "HintDb" ; + id = IDENT ; b = [ "discriminated" -> true | -> false ] -> + VernacCreateHintDb (use_locality (), id, b) + | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> - VernacHints (local,dbnames, h) + VernacHints (enforce_locality_of local,dbnames, h) (*This entry is not commented, only for debug*) @@ -101,16 +104,18 @@ GEXTEND Gram [Genarg.in_gen Genarg.rawwit_constr c]) ] ]; - locality: + obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] ; hint: [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] -> - HintsResolve (List.map (fun x -> (n, x)) lc) + HintsResolve (List.map (fun x -> (n, true, x)) lc) | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc + | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) + | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc - | IDENT "Extern"; n = natural; c = constr_pattern ; "=>"; + | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> HintsExtern (n,c,tac) | IDENT "Destruct"; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 49f00d40..7bebf6db 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_tactic.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: g_tactic.ml4 11741 2009-01-03 14:34:39Z herbelin $ *) open Pp open Pcoq @@ -18,6 +18,7 @@ open Rawterm open Genarg open Topconstr open Libnames +open Termops let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] @@ -215,7 +216,8 @@ GEXTEND Gram ; smart_global: [ [ c = global -> AN c - | s = ne_string -> ByNotation (loc,s) ] ] + | s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> + ByNotation (loc,s,sc) ] ] ; occs_nums: [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl @@ -255,6 +257,11 @@ GEXTEND Gram | "?" -> loc, IntroAnonymous | id = ident -> loc, IntroIdentifier id ] ] ; + intropattern_modifier: + [ [ IDENT "_eqn"; + id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ] + -> id ] ] + ; simple_intropattern: [ [ pat = disjunctive_intropattern -> pat | pat = naming_intropattern -> pat @@ -362,10 +369,14 @@ GEXTEND Gram [ [ "*"; occs = occs -> occs | -> no_occurrences_expr ] ] ; - simple_clause: + in_hyp_list: [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + in_hyp_as: + [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) + | -> None ] ] + ; orient: [ [ "->" -> true | "<-" -> false @@ -404,18 +415,17 @@ GEXTEND Gram eliminator: [ [ "using"; el = constr_with_bindings -> el ] ] ; - with_names: - [ [ "as"; ipat = simple_intropattern -> ipat - | -> dummy_loc,IntroAnonymous ] ] + as_ipat: + [ [ "as"; ipat = simple_intropattern -> Some ipat + | -> None ] ] ; with_inversion_names: - [ [ "as"; ipat = disjunctive_intropattern -> Some ipat + [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; with_induction_names: - [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern + [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier -> (eq,Some ipat) - | "as"; eq = naming_intropattern -> (Some eq,None) | -> (None,None) ] ] ; as_name: @@ -433,19 +443,10 @@ GEXTEND Gram [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; rewriter : - [ [ - (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally - produce a pattern_ident *) - c = pattern_ident -> - let c = (CRef (Ident (loc,c)), NoBindings) in - (RepeatStar, c) - | n = natural; c = pattern_ident -> - let c = (CRef (Ident (loc,c)), NoBindings) in - (UpTo n, c) - | "!"; c = constr_with_bindings -> (RepeatPlus,c) - | "?"; c = constr_with_bindings -> (RepeatStar,c) + [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c) + | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c) | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) - | n = natural; "?"; c = constr_with_bindings -> (UpTo n,c) + | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings -> (UpTo n,c) | n = natural; c = constr_with_bindings -> (Precisely n,c) | c = constr_with_bindings -> (Precisely 1, c) ] ] @@ -480,13 +481,14 @@ GEXTEND Gram | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," -> - TacApply (true,false,cl) - | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> - TacApply (true,true,cl) - | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," - -> TacApply (false,false,cl) - | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> TacApply (false,true,cl) + | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp) + | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp) + | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp) + | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP","; + inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> @@ -518,15 +520,15 @@ GEXTEND Gram (* Begin compatibility *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAssert (None,(loc,IntroIdentifier id),c) + TacAssert (None,Some (loc,IntroIdentifier id),c) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAssert (Some tac,(loc,IntroIdentifier id),c) + TacAssert (Some tac,Some (loc,IntroIdentifier id),c) (* End compatibility *) - | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic -> + | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAssert (Some tac,ipat,c) - | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names -> + | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> TacAssert (None,ipat,c) | IDENT "cut"; c = constr -> TacCut c @@ -587,8 +589,8 @@ GEXTEND Gram | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l) | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l) | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l - | IDENT "move"; dep = [IDENT "dependent" -> true | -> false]; - hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto) + | IDENT "move"; hfrom = id_or_meta; hto = move_location -> + TacMove (true,hfrom,hto) | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l @@ -627,18 +629,18 @@ GEXTEND Gram TacInversion (DepInversion (k,co,ids),hyp) | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) | IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) | IDENT "inversion_clear"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) | IDENT "inversion"; hyp = quantified_hypothesis; - "using"; c = constr; cl = simple_clause -> + "using"; c = constr; cl = in_hyp_list -> TacInversion (InversionUsing (c,cl), hyp) (* Conversion *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 87c11164..f960492e 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: g_vernac.ml4 11809 2009-01-20 11:39:55Z aspiwack $ *) open Pp @@ -46,7 +46,9 @@ let noedit_mode = Gram.Entry.create "vernac:noedit_command" let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" let thm_token = Gram.Entry.create "vernac:thm_token" let def_body = Gram.Entry.create "vernac:def_body" +let decl_notation = Gram.Entry.create "vernac:decl_notation" let typeclass_context = Gram.Entry.create "vernac:typeclass_context" +let record_field = Gram.Entry.create "vernac:record_field" let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion" let get_command_entry () = @@ -62,7 +64,13 @@ let default_command_entry = let no_hook _ _ = () GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode; - vernac: + vernac: FIRST + [ [ IDENT "Time"; locality; v = vernac_aux -> + check_locality (); VernacTime v + | locality; v = vernac_aux -> + check_locality (); v ] ] + ; + vernac_aux: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) [ [ g = gallina; "." -> g @@ -72,12 +80,14 @@ GEXTEND Gram | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l ] ] ; - vernac: FIRST - [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] - ; - vernac: LAST + vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; + locality: + [ [ IDENT "Local" -> locality_flag := Some true + | IDENT "Global" -> locality_flag := Some false + | -> locality_flag := None ] ] + ; noedit_mode: [ [ c = subgoal_command -> c None] ] ; @@ -104,7 +114,6 @@ GEXTEND Gram ; END - let test_plurial_form = function | [(_,([_],_))] -> Flags.if_verbose warning @@ -119,7 +128,7 @@ let no_coercion loc (c,x) = (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - typeclass_context typeclass_constraint; + typeclass_context typeclass_constraint record_field decl_notation; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -142,6 +151,8 @@ GEXTEND Gram (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> + let (k,f) = f in + let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (f,indl) | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,true) @@ -158,16 +169,12 @@ GEXTEND Gram gallina_ext: [ [ b = record_token; oc = opt_coercion; name = identref; ps = binders_let; - s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ]; - ":="; cstr = OPT identref; "{"; - fs = LIST0 record_field SEP ";"; "}" -> - VernacRecord (b,(oc,name),ps,s,cstr,fs) -(* Non port ? - | f = finite_token; s = csort; id = identref; - indpar = LIST0 simple_binder; ":="; lc = constructor_list -> - VernacInductive (f,[id,None,indpar,s,lc]) -*) - ] ] + s = OPT [ ":"; s = lconstr -> s ]; + cfs = [ ":="; l = constructor_list_or_record_decl -> l + | -> RecordDecl (None, []) ] -> + let (recf,indf) = b in + VernacInductive (indf,[((oc,name),ps,s,recf,cfs),None]) + ] ] ; typeclass_context: [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l @@ -189,9 +196,8 @@ GEXTEND Gram no_hook, (Local, Flags.boxed_definitions(), Definition) | IDENT "Example" -> no_hook, (Global, Flags.boxed_definitions(), Example) - | IDENT "SubClass" -> Class.add_subclass_hook, (Global, false, SubClass) - | IDENT "Local"; IDENT "SubClass" -> - Class.add_subclass_hook, (Local, false, SubClass) ] ] + | IDENT "SubClass" -> + Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) @@ -210,11 +216,13 @@ GEXTEND Gram [ ["Inline" -> true | -> false] ] ; finite_token: - [ [ "Inductive" -> true - | "CoInductive" -> false ] ] + [ [ "Inductive" -> (Inductive_kw,Finite) + | "CoInductive" -> (CoInductive,CoFinite) ] ] ; record_token: - [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ] + [ [ IDENT "Record" -> (Record,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Class" -> (Class true,BiFinite) ] ] ; (* Simple definitions *) def_body: @@ -237,15 +245,20 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; indpar = binders_let; - c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ]; - ":="; lc = constructor_list; ntn = decl_notation -> - ((id,indpar,c,lc),ntn) ] ] - ; - constructor_list: - [ [ "|"; l = LIST1 constructor SEP "|" -> l - | l = LIST1 constructor SEP "|" -> l - | -> [] ] ] + [ [ id = identref; oc = opt_coercion; indpar = binders_let; + c = OPT [ ":"; c = lconstr -> c ]; + ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> + (((oc,id),indpar,c,lc),ntn) ] ] + ; + constructor_list_or_record_decl: + [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l + | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> + Constructors ((c id)::l) + | id = identref ; c = constructor_type -> Constructors [ c id ] + | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + RecordDecl (Some cstr,fs) + | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) + | -> Constructors [] ] ] ; (* csort: @@ -316,6 +329,9 @@ GEXTEND Gram *) (* ... with coercions *) record_field: + [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] + ; + record_binder: [ [ id = name -> (false,AssumExpr(id,CHole (loc, None))) | id = name; oc = of_type_with_opt_coercion; t = lconstr -> (oc,AssumExpr (id,t)) @@ -336,12 +352,19 @@ GEXTEND Gram [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> (oc,(idl,c)) ] ] ; + + constructor_type: + [[ l = binders_let; + t= [ coe = of_type_with_opt_coercion; c = lconstr -> + fun l id -> (coe,(id,mkCProdN loc l c)) + | -> + fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] + -> t l + ]] +; + constructor: - [ [ id = identref; l = binders_let; - coe = of_type_with_opt_coercion; c = lconstr -> - (coe,(id,mkCProdN loc l c)) - | id = identref; l = binders_let -> - (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ] + [ [ id = identref; c=constructor_type -> c id ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true @@ -440,15 +463,12 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 global -> - VernacSetOpacity (true,[Conv_oracle.transparent,l]) + VernacSetOpacity (use_non_locality (),[Conv_oracle.transparent,l]) | IDENT "Opaque"; l = LIST1 global -> - VernacSetOpacity (true,[Conv_oracle.Opaque, l]) + VernacSetOpacity (use_non_locality (),[Conv_oracle.Opaque, l]) | IDENT "Strategy"; l = LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> - VernacSetOpacity (false,l) - | IDENT "Local"; IDENT "Strategy"; l = - LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> - VernacSetOpacity (true,l) + VernacSetOpacity (use_locality (),l) (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid @@ -461,43 +481,31 @@ GEXTEND Gram (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_global_to_id qid in - VernacDefinition ((Global,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = coerce_global_to_id qid in - VernacDefinition ((Local,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) + VernacDefinition ((enforce_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (Local, f, s, t) + VernacIdentityCoercion (enforce_locality_exp (), f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (Global, f, s, t) + VernacIdentityCoercion (use_locality_exp (), f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (Local, qid, s, t) + VernacCoercion (enforce_locality_exp (), qid, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (Global, qid, s, t) - - (* Type classes, new syntax without artificial sup. *) - | IDENT "Class"; qid = identref; pars = binders_let; - s = [ ":"; c = sort -> Some (loc, c) | -> None ]; - props = typeclass_field_types -> - VernacClass (qid, pars, s, [], props) - - (* Type classes *) - | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ]; - qid = identref; pars = binders_let; - s = [ ":"; c = sort -> Some (loc, c) | -> None ]; - props = typeclass_field_types -> - VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props) + VernacCoercion (use_locality_exp (), qid, s, t) | IDENT "Context"; c = binders_let -> VernacContext c - | global = [ IDENT "Global" -> true | -> false ]; - IDENT "Instance"; name = identref; sup = OPT binders_let; ":"; + | IDENT "Instance"; name = identref; sup = OPT binders_let; ":"; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs -> + pri = OPT [ "|"; i = natural -> i ] ; + props = [ ":="; "{"; r = record_declaration; "}" -> r | + ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> let sup = match sup with None -> [] @@ -507,17 +515,15 @@ GEXTEND Gram let (loc, id) = name in (loc, Name id) in - VernacInstance (global, sup, (n, expl, t), props, pri) + VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri) | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; - local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; - qid = global; + | IDENT "Implicit"; IDENT "Arguments"; qid = global; pos = OPT [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - VernacDeclareImplicits (local,qid,pos) + VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ] @@ -528,20 +534,6 @@ GEXTEND Gram | "["; "!"; id = ident; "]" -> (id,true,true) | "["; id = ident; "]" -> (id,true, false) ] ] ; - typeclass_field_type: - [ [ id = identref; oc = of_type_with_opt_coercion; t = lconstr -> id, oc, t ] ] - ; - typeclass_field_def: - [ [ id = identref; params = LIST0 identref; ":="; t = lconstr -> id, params, t ] ] - ; - typeclass_field_types: - [ [ ":="; l = LIST1 typeclass_field_type SEP ";" -> l - | -> [] ] ] - ; - typeclass_field_defs: - [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l - | -> [] ] ] - ; strategy_level: [ [ IDENT "expand" -> Conv_oracle.Expand | IDENT "opaque" -> Conv_oracle.Opaque @@ -615,9 +607,15 @@ GEXTEND Gram | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchRewrite c, l) | IDENT "SearchAbout"; - sl = [ "["; l = LIST1 [ r = global -> SearchRef r - | s = ne_string -> SearchString s ]; "]" -> l - | qid = global -> [SearchRef qid] ]; + sl = [ "["; + l = LIST1 [ + b = positive_search_mark; s = ne_string; sc = OPT scope + -> b, SearchString (s,sc) + | b = positive_search_mark; p = constr_pattern + -> b, SearchSubPattern p + ]; "]" -> l + | p = constr_pattern -> [true,SearchSubPattern p] + | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ]; l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) @@ -672,7 +670,7 @@ GEXTEND Gram | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) PrintGrammar ent - | IDENT "LoadPath" -> PrintLoadPath + | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir | IDENT "Modules" -> error "Print Modules is obsolete; use Print Libraries instead" | IDENT "Libraries" -> PrintModules @@ -697,7 +695,6 @@ GEXTEND Gram | IDENT "Hint"; "*" -> PrintHintDb | IDENT "HintDb"; s = IDENT -> PrintHintDbName s | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s - | IDENT "Setoids" -> PrintSetoids | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s @@ -743,6 +740,12 @@ GEXTEND Gram | s = STRING -> CommentString s | n = natural -> CommentInt n ] ] ; + positive_search_mark: + [ [ "-" -> false | -> true ] ] + ; + scope: + [ [ "%"; key = IDENT -> key ] ] + ; END; GEXTEND Gram @@ -776,16 +779,16 @@ GEXTEND Gram ;; (* Grammar extensions *) - + GEXTEND Gram GLOBAL: syntax; syntax: - [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (local,true,sc) + [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (enforce_locality_of local,true,sc) - | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (local,false,sc) + | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (enforce_locality_of local,false,sc) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc,key) @@ -793,44 +796,44 @@ GEXTEND Gram | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - | IDENT "Arguments"; IDENT "Scope"; local = non_globality; qid = global; - "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (local,qid,scl) + | IDENT "Arguments"; IDENT "Scope"; qid = global; + "["; scl = LIST0 opt_scope; "]" -> + VernacArgumentsScope (use_non_locality (),qid,scl) - | IDENT "Infix"; local = locality; + | IDENT "Infix"; local = obsolete_locality; op = ne_string; ":="; p = global; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix (local,(op,modl),p,sc) - | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; - ":="; c = constr; + VernacInfix (enforce_locality_of local,(op,modl),p,sc) + | IDENT "Notation"; local = obsolete_locality; id = identref; + idl = LIST0 ident; ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> - VernacSyntacticDefinition (id,(idl,c),local,b) - | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr; + VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b) + | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":="; + c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (local,c,(s,modl),sc) + VernacNotation (enforce_locality_of local,c,(s,modl),sc) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic -> VernacTacticNotation (n,pil,t) - | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; + | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; + s = ne_string; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (local,(s,l)) + -> VernacSyntaxExtension (enforce_locality_of local,(s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; + obsolete_locality: + [ [ IDENT "Local" -> true | -> false ] ] + ; tactic_level: [ [ "("; "at"; IDENT "level"; n = natural; ")" -> n | -> 0 ] ] ; - locality: - [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> false ] ] - ; - non_globality: - [ [ IDENT "Global" -> false | IDENT "Local" -> true | -> true ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 1b0c24da..2633386f 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lexer.ml4 11238 2008-07-19 09:34:03Z herbelin $ i*) +(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*) (*i camlp4use: "pr_o.cmo" i*) @@ -175,7 +175,7 @@ let add_keyword str = (* Adding a new token (keyword or special token). *) let add_token (con, str) = match con with | "" -> add_keyword str - | "METAIDENT" | "PATTERNIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" + | "METAIDENT" | "LEFTQMARK" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI" -> () | _ -> raise (Token.Error ("\ @@ -237,7 +237,7 @@ let rec string bp len = parser let xml_output_comment = ref (fun _ -> ()) let set_xml_output_comment f = xml_output_comment := f -(* Utilities for comment translation *) +(* Utilities for comments in beautify *) let comment_begin = ref None let comm_loc bp = if !comment_begin=None then comment_begin := Some bp @@ -280,7 +280,7 @@ let comment_stop ep = if !Flags.xml_export && Buffer.length current > 0 && (!between_com || not(null_comment current_s)) then !xml_output_comment current_s; - (if Flags.do_translate() && Buffer.length current > 0 && + (if Flags.do_beautify() && Buffer.length current > 0 && (!between_com || not(null_comment current_s)) then let bp = match !comment_begin with Some bp -> bp @@ -315,7 +315,7 @@ let rec comment bp = parser bp2 | [< '')' >] -> push_string "*)"; | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> - if Flags.do_translate() then (push_string"\"";comm_string bp2 s) + if Flags.do_beautify() then (push_string"\"";comm_string bp2 s) else ignore (string bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment @@ -372,31 +372,50 @@ let process_chars bp c cs = | Some t -> (("", t), (bp, ep)) | None -> err (bp, ep) Undefined_token -(* Parse what follows a dot/question mark *) +let parse_after_dollar bp = + parser + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> + ("METAIDENT", get_buff len) + | [< s >] -> + match lookup_utf8 s with + | Utf8Token (UnicodeLetter, n) -> + ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s) + +(* Parse what follows a dot *) let parse_after_dot bp c = - let constructor = if c = '?' then "PATTERNIDENT" else "FIELD" in parser | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> - (constructor, get_buff len) + ("FIELD", get_buff len) | [< s >] -> match lookup_utf8 s with | Utf8Token (UnicodeLetter, n) -> - (constructor, get_buff (ident_tail (nstore n 0 s) s)) + ("FIELD", get_buff (ident_tail (nstore n 0 s) s)) | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) +(* Parse what follows a question mark *) +let parse_after_qmark bp s = + match Stream.peek s with + |Some ('a'..'z' | 'A'..'Z' | '_') -> ("LEFTQMARK", "") + |None -> ("","?") + | _ -> + match lookup_utf8 s with + | Utf8Token (UnicodeLetter, _) -> ("LEFTQMARK", "") + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '?' s) + (* Parse a token in a char stream *) let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c) >] ep -> - comment_stop bp; - (("METAIDENT", get_buff len), (bp,ep)) - | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep -> + | [< ''$'; t = parse_after_dollar bp >] ep -> + comment_stop bp; (t, (ep, bp)) + | [< ''.' as c; t = parse_after_dot bp c >] ep -> comment_stop bp; - if Flags.do_translate() & t=("",".") then between_com := true; + if Flags.do_beautify() & t=("",".") then between_com := true; (t, (bp,ep)) + | [< ''?'; s >] ep -> + let t = parse_after_qmark bp s in comment_stop bp; (t, (ep, bp)) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ep -> let id = get_buff len in diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 2e55b656..d0a9c3d8 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id: pcoq.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: pcoq.ml4 11784 2009-01-14 11:36:32Z herbelin $ i*) open Pp open Util @@ -407,7 +407,7 @@ module Prim = let name = Gram.Entry.create "Prim.name" let identref = Gram.Entry.create "Prim.identref" - let pattern_ident = Gram.Entry.create "pattern_ident" + let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident" let pattern_identref = Gram.Entry.create "pattern_identref" (* A synonym of ident - maybe ident will be located one day *) @@ -445,6 +445,7 @@ module Constr = let binders_let = Gram.Entry.create "constr:binders_let" let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot" let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint" + let record_declaration = Gram.Entry.create "constr:record_declaration" let appl_arg = Gram.Entry.create "constr:appl_arg" end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 525727ce..0a4b349f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: pcoq.mli 11784 2009-01-14 11:36:32Z herbelin $ i*) open Util open Names @@ -166,7 +166,8 @@ module Constr : val binder_let : local_binder list Gram.Entry.e val binders_let : local_binder list Gram.Entry.e val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e - val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e + val typeclass_constraint : (name located * bool * constr_expr) Gram.Entry.e + val record_declaration : constr_expr Gram.Entry.e val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 5f6ffe87..d5357d86 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: ppconstr.ml 11739 2009-01-02 19:33:19Z herbelin $ *) (*i*) open Util @@ -62,42 +62,46 @@ let prec_of_prim_token = function | Numeral p -> if Bigint.is_pos_or_zero p then lposint else lnegint | String _ -> latom -let env_assoc_value v env = - try List.nth env (v-1) - with Not_found -> anomaly ("Inconsistent environment for pretty-print rule") - -let decode_constrlist_value = function - | CAppExpl (_,_,l) -> l - | CApp (_,_,l) -> List.map fst l - | _ -> anomaly "Ill-formed list argument of notation" - -let decode_patlist_value = function - | CPatCstr (_,_,l) -> l - | _ -> anomaly "Ill-formed list argument of notation" - open Notation -let rec print_hunk n decode pr env = function - | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env) - | UnpListMetaVar (e,prec,sl) -> - prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl) - (pr (n,prec)) (decode (env_assoc_value e env)) - | UnpTerminal s -> str s - | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub) - | UnpCut cut -> ppcmd_of_cut cut - -let pr_notation_gen decode pr s env = +let print_hunks n pr (env,envlist) unp = + let env = ref env and envlist = ref envlist in + let pop r = let a = List.hd !r in r := List.tl !r; a in + let rec aux = function + | [] -> mt () + | UnpMetaVar (_,prec) :: l -> + let c = pop env in pr (n,prec) c ++ aux l + | UnpListMetaVar (_,prec,sl) :: l -> + let cl = pop envlist in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in + let pp2 = aux l in + pp1 ++ pp2 + | UnpTerminal s :: l -> str s ++ aux l + | UnpBox (b,sub) :: l -> + (* Keep order: side-effects *) + let pp1 = ppcmd_of_box b (aux sub) in + let pp2 = aux l in + pp1 ++ pp2 + | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in + aux unp + +let pr_notation pr s env = let unpl, level = find_notation_printing_rule s in - prlist (print_hunk level decode pr env) unpl, level - -let pr_notation = pr_notation_gen decode_constrlist_value -let pr_patnotation = pr_notation_gen decode_patlist_value + print_hunks level pr env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) +let pr_generalization bk ak c = + let hd, tl = + match bk with + | Implicit -> "{", "}" + | Explicit -> "(", ")" + in (* TODO: syntax Abstraction Kind *) + str "`" ++ str hd ++ c ++ str tl + let pr_com_at n = - if Flags.do_translate() && n <> 0 then comment n + if Flags.do_beautify() && n <> 0 then comment n else mt() let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) @@ -179,9 +183,9 @@ let rec pr_patt sep inh p = | CPatAtom (_,Some r) -> pr_reference r, latom | CPatOr (_,pl) -> hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator - | CPatNotation (_,"( _ )",[p]) -> + | CPatNotation (_,"( _ )",([p],[])) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env + | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in @@ -209,17 +213,23 @@ let begin_of_binders = function | b::_ -> begin_of_binder b | _ -> 0 -let surround_binder k p = +let surround_impl k p = match k with - Default Explicit -> hov 1 (str"(" ++ p ++ str")") - | Default Implicit -> hov 1 (str"{" ++ p ++ str"}") - | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]") + | Explicit -> str"(" ++ p ++ str")" + | Implicit -> str"{" ++ p ++ str"}" +let surround_binder k p = + match k with + | Default b -> hov 1 (surround_impl b p) + | Generalized (b, b', t) -> + hov 1 (surround_impl b' (surround_impl b p)) + let surround_implicit k p = match k with - Default Explicit -> p - | Default Implicit -> (str"{" ++ p ++ str"}") - | TypeClass _ -> (str"[" ++ p ++ str"]") + | Default Explicit -> p + | Default Implicit -> (str"{" ++ p ++ str"}") + | Generalized (b, b', t) -> + surround_impl b' (surround_impl b p) let pr_binder many pr (nal,k,t) = match t with @@ -542,6 +552,17 @@ let rec pr sep inherited a = else p, lproj | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp + | CRecord (_,w,l) -> + let beg = + match w with + | None -> spc () + | Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc () + in + hv 0 (str"{" ++ beg ++ + prlist_with_sep (fun () -> spc () ++ str";" ++ spc ()) + (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c) + l), latom + | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> hv 0 ( str "let '" ++ @@ -592,9 +613,10 @@ let rec pr sep inherited a = | CCast (_,a,CastCoerce) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), lcast - | CNotation (_,"( _ )",[t]) -> + | CNotation (_,"( _ )",([t],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom | CNotation (_,s,env) -> pr_notation (pr mt) s env + | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 | CDynamic _ -> str "", latom @@ -644,15 +666,15 @@ let rec strip_context n iscast t = type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds; - pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds } let default_term_pr = { pr_constr_expr = pr lsimple; pr_lconstr_expr = pr ltop; - pr_pattern_expr = pr lsimple; - pr_lpattern_expr = pr ltop + pr_constr_pattern_expr = pr lsimple; + pr_lconstr_pattern_expr = pr ltop } let term_pr = ref default_term_pr @@ -661,8 +683,8 @@ let set_term_pr = (:=) term_pr let pr_constr_expr c = !term_pr.pr_constr_expr c let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c -let pr_pattern_expr c = !term_pr.pr_pattern_expr c -let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c +let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c +let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c let pr_cases_pattern_expr = pr_patt ltop diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 8047e968..0d0c8f56 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ppconstr.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: ppconstr.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) open Pp open Environ @@ -66,8 +66,8 @@ val pr_may_eval : val pr_rawsort : rawsort -> std_ppcmds val pr_binders : local_binder list -> std_ppcmds -val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds -val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds +val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds +val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds val pr_lconstr_expr : constr_expr -> std_ppcmds val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds @@ -75,8 +75,8 @@ val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds type term_pr = { pr_constr_expr : constr_expr -> std_ppcmds; pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds; - pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds + pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; + pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds } val set_term_pr : term_pr -> unit diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 6a7ae9bc..3b433498 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Pp open Names @@ -21,6 +21,7 @@ open Pattern open Ppextend open Ppconstr open Printer +open Termops let pr_global x = Nametab.pr_global_env Idset.empty x @@ -79,7 +80,7 @@ let pr_and_short_name pr (c,_) = pr c let pr_or_by_notation f = function | AN v -> f v - | ByNotation (_,s) -> str s + | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_located pr (loc,x) = pr x @@ -122,10 +123,6 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) -let pr_with_names = function - | None -> mt () - | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) - let rec pr_message_token prid = function | MsgString s -> qs s | MsgInt n -> int n @@ -140,6 +137,8 @@ let out_bindings = function | ExplicitBindings l -> ExplicitBindings (List.map (fun (loc,id,c) -> (loc,id,snd c)) l) | NoBindings -> NoBindings +let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c + let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false") @@ -148,7 +147,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen rawwit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x) - | IdentArgType -> pr_id (out_gen rawwit_ident x) + | IdentArgType b -> if_pattern_ident b pr_id (out_gen rawwit_ident x) | VarArgType -> pr_located pr_id (out_gen rawwit_var x) | RefArgType -> prref (out_gen rawwit_ref x) | SortArgType -> pr_rawsort (out_gen rawwit_sort x) @@ -179,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu x) | ExtraArgType s -> try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str " [no printer for " ++ str s ++ str "] " + with Not_found -> str "[no printer for " ++ str s ++ str "]" let rec pr_glob_generic prc prlc prtac x = @@ -190,7 +189,7 @@ let rec pr_glob_generic prc prlc prtac x = | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen globwit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x) - | IdentArgType -> pr_id (out_gen globwit_ident x) + | IdentArgType b -> if_pattern_ident b pr_id (out_gen globwit_ident x) | VarArgType -> pr_located pr_id (out_gen globwit_var x) | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x) | SortArgType -> pr_rawsort (out_gen globwit_sort x) @@ -224,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac x = x) | ExtraArgType s -> try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str "[no printer for " ++ str s ++ str "] " + with Not_found -> str "[no printer for " ++ str s ++ str "]" open Closure @@ -236,7 +235,7 @@ let rec pr_generic prc prlc prtac x = | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\"" | PreIdentArgType -> str (out_gen wit_pre_ident x) | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x) - | IdentArgType -> pr_id (out_gen wit_ident x) + | IdentArgType b -> if_pattern_ident b pr_id (out_gen wit_ident x) | VarArgType -> pr_id (out_gen wit_var x) | RefArgType -> pr_global (out_gen wit_ref x) | SortArgType -> pr_sort (out_gen wit_sort x) @@ -326,9 +325,6 @@ let pr_evaluable_reference_env env = function | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) -let pr_inductive env ind = - Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.IndRef ind) - let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id @@ -376,9 +372,9 @@ let pr_with_inversion_names = function | None -> mt () | Some ipat -> pr_as_intro_pattern ipat -let pr_with_names = function - | _,IntroAnonymous -> mt () - | ipat -> pr_as_intro_pattern ipat +let pr_as_ipat = function + | None -> mt () + | Some ipat -> pr_as_intro_pattern ipat let pr_as_name = function | Anonymous -> mt () @@ -397,7 +393,7 @@ let pr_assertion _prlc prc ipat c = match ipat with spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) *) | ipat -> - spc() ++ prc c ++ pr_with_names ipat + spc() ++ prc c ++ pr_as_ipat ipat let pr_assumption prlc prc ipat c = match ipat with (* Use this "optimisation" or use only the general case ? @@ -405,7 +401,7 @@ let pr_assumption prlc prc ipat c = match ipat with spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) *) | ipat -> - spc() ++ prc c ++ pr_with_names ipat + spc() ++ prc c ++ pr_as_ipat ipat let pr_by_tactic prt = function | TacId [] -> mt () @@ -426,6 +422,10 @@ let pr_simple_clause pr_id = function | [] -> mt () | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) +let pr_in_hyp_as pr_id = function + | None -> mt () + | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat + let pr_clauses pr_id = function | { onhyps=None; concl_occs=occs } -> if occs = no_occurrences_expr then pr_in (str " * |-") @@ -468,12 +468,16 @@ let pr_lazy lz = if lz then str "lazy" else mt () let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]" - | Subterm (Some id,a) -> - str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" + | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]" + | Subterm (b,Some id,a) -> + (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" -let pr_match_hyps pr_pat (Hyp (nal,mp)) = - pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp +let pr_match_hyps pr_pat = function + | Hyp (nal,mp) -> + pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp + | Def (nal,mv,mp) -> + pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv + ++ str ":" ++ pr_match_pattern pr_pat mp let pr_match_rule m pr pr_pat = function | Pat ([],mp,t) when m -> @@ -695,10 +699,11 @@ and pr_atom1 = function | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) - | TacApply (a,ev,cb) -> + | TacApply (a,ev,cb,inhyp) -> hov 1 ((if a then mt() else str "simple ") ++ str (with_evars ev "apply") ++ spc () ++ - prlist_with_sep pr_coma pr_with_bindings cb) + prlist_with_sep pr_coma pr_with_bindings cb ++ + pr_in_hyp_as pr_ident inhyp) | TacElim (ev,cb,cbo) -> hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) @@ -1019,7 +1024,7 @@ let rec raw_printers = (pr_raw_tactic_level, drop_env pr_constr_expr, drop_env pr_lconstr_expr, - pr_lpattern_expr, + pr_lconstr_pattern_expr, drop_env (pr_or_by_notation pr_reference), drop_env (pr_or_by_notation pr_reference), pr_reference, diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 67cd6f72..78c63ca2 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: ppvernac.ml 11809 2009-01-20 11:39:55Z aspiwack $ *) open Pp open Names @@ -133,9 +133,11 @@ let pr_in_out_modules = function | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ str"outside" ++ spc() ++ prlist_with_sep sep pr_module l -let pr_search_about = function - | SearchRef r -> pr_reference r - | SearchString s -> qs s +let pr_search_about (b,c) = + (if b then str "-" else mt()) ++ + match c with + | SearchSubPattern p -> pr_constr_pattern_expr p + | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a b pr_p = match a with | SearchHead qid -> str"Search" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b @@ -144,7 +146,7 @@ let pr_search a b pr_p = match a with | SearchAbout sl -> str"SearchAbout" ++ spc() ++ str "[" ++ prlist_with_sep spc pr_search_about sl ++ str "]" ++ pr_in_out_modules b let pr_locality local = if local then str "Local " else str "" -let pr_non_globality local = if local then str "" else str "Global " +let pr_non_locality local = if local then str "" else str "Global " let pr_explanation (e,b,f) = let a = match e with @@ -192,18 +194,22 @@ let pr_hints local db h pr_c pr_pat = match h with | HintsResolve l -> str "Resolve " ++ prlist_with_sep sep - (fun (pri, c) -> pr_c c ++ + (fun (pri, _, c) -> pr_c c ++ match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) l | HintsImmediate l -> str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l | HintsUnfold l -> str "Unfold " ++ prlist_with_sep sep pr_reference l + | HintsTransparency (l, b) -> + str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep + pr_reference l | HintsConstructors c -> str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c - | HintsExtern (n,c,tac) -> - str "Extern" ++ spc() ++ int n ++ spc() ++ pr_pat c ++ str" =>" ++ - spc() ++ pr_raw_tactic tac + | HintsExtern (n,c,tac) -> + let pat = match c with None -> mt () | Some pat -> pr_pat pat in + str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ + spc() ++ pr_raw_tactic tac | HintsDestruct(name,i,loc,c,tac) -> str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++ hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++ @@ -325,7 +331,7 @@ let pr_assumption_token many = function str (if many then "Parameters" else "Parameter") | (Global,Conjectural) -> str"Conjecture" | (Local,Conjectural) -> - anomaly "Don't know how to translate a local conjecture" + anomaly "Don't know how to beautify a local conjecture" let pr_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -402,9 +408,27 @@ let make_pr_vernac pr_constr pr_lconstr = let pr_constrarg c = spc () ++ pr_constr c in let pr_lconstrarg c = spc () ++ pr_lconstr c in let pr_intarg n = spc () ++ int n in -let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in -let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l - ++ sep ++ pr_constrarg c in +(* let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in *) +let pr_record_field (x, ntn) = + let prx = match x with + | (oc,AssumExpr (id,t)) -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t) + | (oc,DefExpr(id,b,opt)) -> (match opt with + | Some t -> + hov 1 (pr_lname id ++ + (if oc then str" :>" else str" :") ++ spc() ++ + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) + | None -> + hov 1 (pr_lname id ++ str" :=" ++ spc() ++ + pr_lconstr b)) in + prx ++ pr_decl_notation pr_constr ntn +in +let pr_record_decl b c fs = + pr_opt pr_lident c ++ str"{" ++ + hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}") +in let rec pr_vernac = function @@ -480,7 +504,7 @@ let rec pr_vernac = function | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function | None -> str"_" | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ pr_non_globality local ++ pr_reference q + str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *) hov 0 (hov 0 (str"Infix " ++ pr_locality local @@ -533,11 +557,11 @@ let rec pr_vernac = function | VernacStartTheoremProof (ki,l,_,_) -> let pr_statement head (id,(bl,c)) = hov 0 - (head ++ spc () ++ pr_opt pr_lident id ++ spc() ++ + (head ++ pr_opt pr_lident id ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ str":" ++ pr_spc_lconstr c) in hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ - prlist (pr_statement (str "with ")) (List.tl l)) + prlist (pr_statement (spc () ++ str "with")) (List.tl l)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with @@ -558,22 +582,31 @@ let rec pr_vernac = function hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ pr_spc_lconstr c) in - let pr_constructor_list l = match l with - | [] -> mt() - | _ -> + let pr_constructor_list b l = match l with + | Constructors [] -> mt() + | Constructors l -> pr_com_at (begin_of_inductive l) ++ fnl() ++ str (if List.length l = 1 then " " else " | ") ++ - prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in - let pr_oneind key ((id,indpar,s,lc),ntn) = - hov 0 ( - str key ++ spc() ++ - pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ - spc() ++ pr_lconstr_expr s ++ - str" :=") ++ pr_constructor_list lc ++ - pr_decl_notation pr_constr ntn in - - hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l)) + prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l + | RecordDecl (c,fs) -> + spc() ++ + pr_record_decl b c fs in + let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) = + let kw = + str (match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class b -> if b then "Definitional Class" else "Class") + in + hov 0 ( + kw ++ spc() ++ + (if coe then str" > " else str" ") ++ pr_lident id ++ + pr_and_type_binders_arg indpar ++ spc() ++ + Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ + str" :=") ++ pr_constructor_list k lc ++ + pr_decl_notation pr_constr ntn + in + hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) @@ -585,7 +618,7 @@ let rec pr_vernac = function let pr_onerec = function | ((loc,id),(n,ro),bl,type_,def),ntn -> let (bl',def,type_) = - if Flags.do_translate() then extract_def_binders def type_ + if Flags.do_beautify() then extract_def_binders def type_ else ([],def,type_) in let bl = bl @ bl' in let ids = List.flatten (List.map name_of_binder bl) in @@ -617,7 +650,7 @@ let rec pr_vernac = function | VernacCoFixpoint (corecs,b) -> let pr_onecorec (((loc,id),bl,c,def),ntn) = let (bl',def,c) = - if Flags.do_translate() then extract_def_binders def c + if Flags.do_beautify() then extract_def_binders def c else ([],def,c) in let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ @@ -638,30 +671,6 @@ let rec pr_vernac = function (* Gallina extensions *) - | VernacRecord (b,(oc,name),ps,s,c,fs) -> - let pr_record_field = function - | (oc,AssumExpr (id,t)) -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t) - | (oc,DefExpr(id,b,opt)) -> (match opt with - | Some t -> - hov 1 (pr_lname id ++ - (if oc then str" :>" else str" :") ++ spc() ++ - pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) - | None -> - hov 1 (pr_lname id ++ str" :=" ++ spc() ++ - pr_lconstr b)) in - hov 2 - (str (if b then "Record" else "Structure") ++ - (if oc then str" > " else str" ") ++ pr_lident name ++ - pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ - pr_lconstr_expr s ++ str" := " ++ - (match c with - | None -> mt() - | Some sc -> pr_lident sc) ++ - spc() ++ str"{" ++ - hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id) | VernacRequire (exp,spe,l) -> hov 2 @@ -688,28 +697,17 @@ let rec pr_vernac = function str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) - - - | VernacClass (id, par, ar, sup, props) -> - hov 1 ( - str"Class" ++ spc () ++ pr_lident id ++ -(* prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ *) - pr_and_type_binders_arg par ++ - (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++ - spc () ++ str"where" ++ spc () ++ - prlist_with_sep (fun () -> str";" ++ spc()) - (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) | VernacInstance (glob, sup, (instid, bk, cl), props, pri) -> hov 1 ( - pr_non_globality (not glob) ++ + pr_non_locality (not glob) ++ str"Instance" ++ spc () ++ pr_and_type_binders_arg sup ++ str"=>" ++ spc () ++ (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++ pr_constr_expr cl ++ spc () ++ - spc () ++ str"where" ++ spc () ++ - prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props) + spc () ++ str":=" ++ spc () ++ + pr_constr_expr props) | VernacContext l -> hov 1 ( @@ -806,8 +804,10 @@ let rec pr_vernac = function hov 1 ((str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) + | VernacCreateHintDb (local,dbname,b) -> + hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ())) | VernacHints (local,dbnames,h) -> - pr_hints local dbnames h pr_constr pr_pattern_expr + pr_hints local dbnames h pr_constr pr_constr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> hov 2 (str"Notation " ++ pr_locality local ++ pr_lident id ++ @@ -816,7 +816,7 @@ let rec pr_vernac = function | VernacDeclareImplicits (local,q,None) -> hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q) | VernacDeclareImplicits (local,q,Some imps) -> - hov 1 (str"Implicit Arguments " ++ pr_non_globality local ++ + hov 1 (str"Implicit Arguments " ++ pr_non_locality local ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") | VernacReserve (idl,c) -> @@ -824,11 +824,11 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) - | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent -> - hov 1 (str"Transparent" ++ + | VernacSetOpacity(b,[k,l]) when k=Conv_oracle.transparent -> + hov 1 (str"Transparent" ++ pr_non_locality b ++ spc() ++ prlist_with_sep sep pr_reference l) - | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) -> - hov 1 (str"Opaque" ++ + | VernacSetOpacity(b,[Conv_oracle.Opaque,l]) -> + hov 1 (str"Opaque" ++ pr_non_locality b ++ spc() ++ prlist_with_sep sep pr_reference l) | VernacSetOpacity (local,l) -> let pr_lev = function @@ -866,7 +866,7 @@ let rec pr_vernac = function str"Print Section" ++ spc() ++ Libnames.pr_reference s | PrintGrammar ent -> str"Print Grammar" ++ spc() ++ str ent - | PrintLoadPath -> str"Print LoadPath" + | PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir | PrintModules -> str"Print Modules" | PrintMLLoadPath -> str"Print ML Path" | PrintMLModules -> str"Print ML Modules" @@ -890,7 +890,6 @@ let rec pr_vernac = function | PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n - | PrintSetoids -> str"Print Setoids" | PrintScopes -> str"Print Scopes" | PrintScope s -> str"Print Scope" ++ spc() ++ str s | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s @@ -900,7 +899,7 @@ let rec pr_vernac = function term *) | PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid in pr_printable p - | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr + | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_reference qid @@ -931,19 +930,16 @@ and pr_extend s cl = let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with - | Egrammar.TacTerm s :: rl -> str s, rl, cl - | Egrammar.TacNonTerm _ :: rl -> - (* Will put an unnecessary extra space in front *) - pr_gen (Global.env()) (List.hd cl), rl, List.tl cl - | [] -> anomaly "Empty entry" in + | Egrammar.TacTerm s :: rl -> str s, rl, cl + | Egrammar.TacNonTerm _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl + | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left (fun (strm,args) pi -> - match pi with - Egrammar.TacNonTerm _ -> - (strm ++ pr_gen (Global.env()) (List.hd args), - List.tl args) - | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) + let pp,args = match pi with + | Egrammar.TacNonTerm _ -> (pr_arg (List.hd args), List.tl args) + | Egrammar.TacTerm s -> (str s, args) in + (strm ++ spc() ++ pp), args) (start,cl) rl in hov 1 pp with Not_found -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 4811c443..5543a31c 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 11343 2008-09-01 20:55:13Z herbelin $ *) +(* $Id: prettyp.ml 11622 2008-11-23 08:45:56Z herbelin $ *) open Pp open Util @@ -349,10 +349,10 @@ let pr_record (sp,tyi) = str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ str ":= " ++ pr_id cstrnames.(0)) ++ brk(1,2) ++ - hv 2 (str "{ " ++ - prlist_with_sep (fun () -> str "; " ++ brk(1,0)) + hv 2 (str "{" ++ + prlist_with_sep (fun () -> str ";" ++ brk(1,0)) (fun (id,b,c) -> - pr_id id ++ str (if b then " : " else " := ") ++ + str " " ++ pr_id id ++ str (if b then " : " else " := ") ++ pr_lconstr_env envpar c) fields) ++ str" }") let gallina_print_inductive sp = @@ -784,6 +784,11 @@ let pr_instance env i = (* lighter *) print_ref false (ConstRef (instance_impl i)) +let print_all_instances () = + let env = Global.env () in + let inst = all_instances () in + prlist_with_sep fnl (pr_instance env) inst + let print_instances r = let env = Global.env () in let inst = instances r in diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index a487ef62..ec2228c7 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: prettyp.mli 10697 2008-03-19 17:58:43Z msozeau $ i*) +(*i $Id: prettyp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) (*i*) open Pp @@ -61,7 +61,7 @@ val print_canonical_projections : unit -> std_ppcmds (* Pretty-printing functions for type classes and instances *) val print_typeclasses : unit -> std_ppcmds val print_instances : global_reference -> std_ppcmds - +val print_all_instances : unit -> std_ppcmds val inspect : int -> std_ppcmds diff --git a/parsing/printer.ml b/parsing/printer.ml index b126cc9c..10034dd9 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *) open Pp open Util @@ -90,14 +90,14 @@ let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Idset.empty t) let pr_lconstr_pattern_env env c = - pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_constr_pattern_env env c = - pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_lconstr_pattern t = - pr_lconstr_expr (extern_constr_pattern empty_names_context t) + pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_constr_pattern t = - pr_constr_expr (extern_constr_pattern empty_names_context t) + pr_constr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_sort s = pr_rawsort (extern_sort s) @@ -162,9 +162,9 @@ let pr_rel_decl env (na,c,typ) = (* Prints a signature, all declarations on the same line if possible *) let pr_named_context_of env = - hv 0 (fold_named_context - (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) - env ~init:(mt ())) + let make_decl_list env d pps = pr_var_decl env d :: pps in + let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in + hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env ne_context = hv 0 (Sign.fold_named_context @@ -475,6 +475,9 @@ let pr_prim_rule = function (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) + | Order ord -> + (str"order " ++ prlist_with_sep pr_spc pr_id ord) + | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) diff --git a/parsing/printmod.ml b/parsing/printmod.ml index be73f573..596ce6b2 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -90,7 +90,7 @@ and print_modtype locals mty = let s = (String.concat "." (List.map string_of_id idl)) in hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | SEBwith(seb,With_module_body(idl,mp,_))-> + | SEBwith(seb,With_module_body(idl,mp,_,_))-> let s =(String.concat "." (List.map string_of_id idl)) in hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) @@ -102,7 +102,7 @@ and print_sig locals msid sign = | SFBconst {const_opaque=true} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module " + | SFBalias (mp,_,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign @@ -114,7 +114,7 @@ and print_struct locals msid struc = | SFBconst {const_body=None} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module " + | SFBalias (mp,_,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 72d81051..37817389 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: q_constr.ml4 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: q_constr.ml4 11576 2008-11-10 19:13:15Z msozeau $ *) open Rawterm open Term @@ -75,7 +75,7 @@ EXTEND | "0" [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> - | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >> + | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark (Define False)) >> | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> apply_ref <:expr< coq_sumbool_ref >> [c1;c2] diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a4cfe27a..aeee632c 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*) -(* $Id: q_coqast.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: q_coqast.ml4 11735 2009-01-02 17:22:31Z herbelin $ *) open Util open Names @@ -68,7 +68,8 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >> let mlexpr_of_by_notation f = function | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> - | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> + | Genarg.ByNotation (loc,s,sco) -> + <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> let mlexpr_of_intro_pattern = function | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >> @@ -102,12 +103,12 @@ let mlexpr_of_occs = let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f let mlexpr_of_hyp_location = function - | occs, Tacexpr.InHyp -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >> - | occs, Tacexpr.InHypTypeOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >> - | occs, Tacexpr.InHypValueOnly -> - <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >> + | occs, Termops.InHyp -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >> + | occs, Termops.InHypTypeOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >> + | occs, Termops.InHypValueOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >> let mlexpr_of_clause cl = <:expr< {Tacexpr.onhyps= @@ -139,7 +140,9 @@ let mlexpr_of_binding_kind = function let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >> + | Topconstr.Generalized (b,b',b'') -> + <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ + $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> let rec mlexpr_of_constr = function | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> @@ -158,9 +161,11 @@ let rec mlexpr_of_constr = function | Topconstr.CCases (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole (loc, None) -> <:expr< Topconstr.CHole $dloc$ None >> | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" - | Topconstr.CNotation(_,ntn,l) -> + | Topconstr.CNotation(_,ntn,subst) -> <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$ - $mlexpr_of_list mlexpr_of_constr l$ >> + $mlexpr_of_pair + (mlexpr_of_list mlexpr_of_constr) + (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >> | Topconstr.CPatVar (loc,n) -> <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" @@ -196,7 +201,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.RefArgType -> <:expr< Genarg.RefArgType >> | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >> | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >> - | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >> + | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >> | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> | Genarg.StringArgType -> <:expr< Genarg.StringArgType >> | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> @@ -264,13 +269,16 @@ let mlexpr_of_entry_type = function let mlexpr_of_match_pattern = function | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >> - | Tacexpr.Subterm (ido,t) -> - <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> + | Tacexpr.Subterm (b,ido,t) -> + <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >> let mlexpr_of_match_context_hyps = function | Tacexpr.Hyp (id,l) -> let f = mlexpr_of_located mlexpr_of_name in <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >> + | Tacexpr.Def (id,v,l) -> + let f = mlexpr_of_located mlexpr_of_name in + <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >> let mlexpr_of_match_rule f = function | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >> @@ -300,8 +308,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacApply (b,false,cb) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacApply (b,false,cb,None) -> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in @@ -337,7 +345,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacCut c -> <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> - let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in + let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> @@ -480,6 +488,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id | Tacexpr.TacArg t -> <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >> + | Tacexpr.TacComplete t -> + <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >> | _ -> failwith "Quotation of tactic expressions: TODO" and mlexpr_of_tactic_arg = function diff --git a/parsing/search.ml b/parsing/search.ml index c6ff4c04..8b1551b6 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: search.ml 11739 2009-01-02 19:33:19Z herbelin $ *) open Pp open Util @@ -165,15 +165,6 @@ let raw_search_rewrite extra_filter display_function pattern = (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) && extra_filter s a c) display_function gref_eq -(* - ; - filtered_search - (fun s a c -> - ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) || - (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c)) - && extra_filter s a c) - display_function gref_eqT -*) let text_pattern_search extra_filter = raw_pattern_search extra_filter plain_display @@ -204,17 +195,17 @@ let gen_filtered_search filter_function display_function = let name_of_reference ref = string_of_id (id_of_global ref) type glob_search_about_item = - | GlobSearchRef of global_reference + | GlobSearchSubPattern of constr_pattern | GlobSearchString of string let search_about_item (itemref,typ) = function - | GlobSearchRef ref -> Termops.occur_term (constr_of_global ref) typ + | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ | GlobSearchString s -> string_string_contains (name_of_reference itemref) s let raw_search_about filter_modules display_function l = let filter ref' env typ = filter_modules ref' env typ && - List.for_all (search_about_item (ref',typ)) l && + List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l && not (string_string_contains (name_of_reference ref') "_subproof") in gen_filtered_search filter display_function diff --git a/parsing/search.mli b/parsing/search.mli index 8ee708bc..7d12d26f 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: search.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: search.mli 11739 2009-01-02 19:33:19Z herbelin $ i*) open Pp open Names @@ -19,13 +19,14 @@ open Nametab (*s Search facilities. *) type glob_search_about_item = - | GlobSearchRef of global_reference + | GlobSearchSubPattern of constr_pattern | GlobSearchString of string val search_by_head : global_reference -> dir_path list * bool -> unit val search_rewrite : constr_pattern -> dir_path list * bool -> unit val search_pattern : constr_pattern -> dir_path list * bool -> unit -val search_about : glob_search_about_item list -> dir_path list * bool -> unit +val search_about : + (bool * glob_search_about_item) list -> dir_path list * bool -> unit (* The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. @@ -46,4 +47,4 @@ val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> constr_pattern -> unit val raw_search_about : (global_reference -> env -> constr -> bool) -> (global_reference -> env -> constr -> unit) -> - glob_search_about_item list -> unit + (bool * glob_search_about_item) list -> unit diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index 08feb17a..a7b27e21 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: vernacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: vernacextend.ml4 11622 2008-11-23 08:45:56Z herbelin $ *) open Util open Genarg @@ -118,6 +118,9 @@ EXTEND [ [ e = LIDENT; "("; s = LIDENT; ")" -> let t, g = Q_util.interp_entry_name loc e "" in VernacNonTerm (loc, t, g, Some s) + | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> + let t, g = Q_util.interp_entry_name loc e sep in + VernacNonTerm (loc, t, g, Some s) | s = STRING -> VernacTerm s ] ] -- cgit v1.2.3