From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- parsing/argextend.ml4 | 74 +++++++++++++++++++++++++++++++++++++++++++++---- parsing/egrammar.ml | 41 +++++++++++++++++++-------- parsing/egrammar.mli | 2 ++ parsing/extrawit.ml | 12 ++++---- parsing/g_constr.ml4 | 24 +++++++++++----- parsing/g_proofs.ml4 | 21 ++------------ parsing/g_tactic.ml4 | 27 ++++++++---------- parsing/g_vernac.ml4 | 4 +-- parsing/ppconstr.ml | 72 +++++++++++++++++++++++++++++------------------- parsing/ppconstr.mli | 6 +++- parsing/pptactic.ml | 30 ++++++++++---------- parsing/ppvernac.ml | 76 +++++++++++++-------------------------------------- parsing/printer.ml | 37 +++++++++++++++---------- parsing/printer.mli | 3 +- parsing/q_coqast.ml4 | 15 +++++++--- parsing/tacextend.ml4 | 61 +++++++++++++++++++++++++++++------------ 16 files changed, 297 insertions(+), 208 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 3266fcf9..f554522a 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -107,6 +107,64 @@ let rec make_wit loc = function value wit = $lid:"wit_"^s$; end in WIT.wit >> +let has_extraarg = + List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) + +let statically_known_possibly_empty s (prods,_) = + List.for_all (function + | GramNonTerminal(_,ExtraArgType s',_,_) -> + (* For ExtraArg we don't know (we'll have to test dynamically) *) + (* unless it is a recursive call *) + s <> s' + | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) -> + (* Opt and List0 parses the empty string *) + true + | _ -> + (* This consumes a token for sure *) false) + prods + +let possibly_empty_subentries loc (prods,act) = + let bind_name p v e = match p with + | None -> e + | Some id -> + let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in + let rec aux = function + | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >> + | GramNonTerminal(_,OptArgType _,_,p) :: tl -> + bind_name p <:expr< None >> (aux tl) + | GramNonTerminal(_,List0ArgType _,_,p) :: tl -> + bind_name p <:expr< [] >> (aux tl) + | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl -> + (* We check at runtime if extraarg s parses "epsilon" *) + let s = match p with None -> "_" | Some id -> Names.string_of_id id in + <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with + [ None -> raise Exit + | Some v -> v ] in $aux tl$ >> + | _ -> assert false (* already filtered out *) in + if has_extraarg prods then + (* Needs a dynamic check; catch all exceptions if ever some rhs raises *) + (* an exception rather than returning a value; *) + (* declares loc because some code can refer to it; *) + (* ensures loc is used to avoid "unused variable" warning *) + (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>) + else + (* Static optimisation *) + (false, aux prods) + +let make_possibly_empty_subentries loc s cl = + let cl = List.filter (statically_known_possibly_empty s) cl in + if cl = [] then + <:expr< None >> + else + let rec aux = function + | (true, e) :: l -> + <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >> + | (false, e) :: _ -> + <:expr< Some $e$ >> + | [] -> + <:expr< None >> in + aux (List.map (possibly_empty_subentries loc) cl) + let make_act loc act pil = let rec make = function | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> @@ -144,9 +202,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let interp = match f with | None -> <:expr< fun ist gl x -> - out_gen $make_wit loc globtyp$ - (Tacinterp.interp_genarg ist gl - (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + let (sigma,a_interp) = + Tacinterp.interp_genarg ist gl + (Genarg.in_gen $make_globwit loc globtyp$ x) + in + (sigma , out_gen $make_wit loc globtyp$ a_interp)>> | Some f -> <:expr< $lid:f$>> in let substitute = match h with | None -> @@ -160,10 +220,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = 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 default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = - Genarg.create_arg $se$ >>; + Genarg.create_arg $default_value$ $se$>>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { @@ -171,7 +232,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = ((fun e x -> (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))), (fun ist gl x -> - (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), + let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in + (sigma , Genarg.in_gen $wit$ a_interp)), (fun subst x -> (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) @@ -195,7 +257,7 @@ let declare_vernac_argument loc s pr cl = [ <:str_item< 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$ >>; + $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>; <:str_item< value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>; <:str_item< do { diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 4418a45f..82f24242 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -106,11 +106,14 @@ let make_constr_action in make ([],[],[]) (List.rev pil) +let check_cases_pattern_env loc (env,envlist,hasbinders) = + if hasbinders then error_invalid_pattern_notation loc else (env,envlist) + let make_cases_pattern_action (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = - let rec make (env,envlist as fullenv) = function + let rec make (env,envlist,hasbinders as fullenv) = function | [] -> - Gram.action (fun loc -> f loc fullenv) + Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv)) | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> (* parse a non-binding item *) Gram.action (fun _ -> make fullenv tl) @@ -118,28 +121,37 @@ let make_cases_pattern_action (* parse a binding non-terminal *) (match typ with | ETConstr _ -> (* pattern non-terminal *) - Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl) + Gram.action (fun (v:cases_pattern_expr) -> + make (v::env, envlist, hasbinders) tl) | ETReference -> Gram.action (fun (v:reference) -> - make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl) + make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl) | ETName -> Gram.action (fun (na:name located) -> - make (cases_pattern_expr_of_name na :: env, envlist) tl) + make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) | ETBigint -> Gram.action (fun (v:Bigint.bigint) -> - make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl) + make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl) | ETConstrList (_,_) -> Gram.action (fun (vl:cases_pattern_expr list) -> - make (env, vl :: envlist) tl) - | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) -> - failwith "Unexpected entry of type cases pattern or other") + make (env, vl :: envlist, hasbinders) tl) + | ETBinder _ | ETBinderList (true,_) -> + Gram.action (fun (v:local_binder list) -> + make (env, envlist, hasbinders) tl) + | ETBinderList (false,_) -> + Gram.action (fun (v:local_binder list list) -> + make (env, envlist, true) tl) + | (ETPattern | ETOther _) -> + anomaly "Unexpected entry of type cases pattern or other") | GramConstrListMark (n,b) :: tl -> (* Rebuild expansions of ConstrList *) let heads,env = list_chop n env in - if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl - else make (env,heads::envlist) tl + if b then + make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl + else + make (env,heads::envlist,hasbinders) tl in - make ([],[]) (List.rev pil) + make ([],[],false) (List.rev pil) let rec make_constr_prod_item assoc from forpat = function | GramConstrTerminal tok :: l -> @@ -349,3 +361,8 @@ let _ = { freeze_function = freeze; unfreeze_function = unfreeze; init_function = init } + +let with_grammar_rule_protection f x = + let fs = freeze () in + try let a = f x in unfreeze fs; a + with e -> unfreeze fs; raise e diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 1d85c74e..0ac46ded 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -71,3 +71,5 @@ val get_extend_vernac_grammars : val recover_notation_grammar : notation -> (precedence * tolerability list) -> notation_var_internalization_type list * notation_grammar + +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index ce734622..0398f0b6 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -15,12 +15,12 @@ open Genarg let tactic_main_level = 5 -let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0" -let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1" -let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2" -let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3" -let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4" -let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5" +let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg None "tactic0" +let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg None "tactic1" +let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg None "tactic2" +let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg None "tactic3" +let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg None "tactic4" +let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg None "tactic5" let wit_tactic = function | 0 -> wit_tactic0 diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 5d5f6e4d..958f59e0 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -31,6 +31,11 @@ let mk_cast = function (c,(_,None)) -> c | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty)) +let binders_of_names l = + List.map (fun (loc, na) -> + LocalRawAssum ([loc, na], Default Explicit, + CHole (loc, Some (Evd.BinderType na)))) l + let binders_of_lidents l = List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Glob_term.Explicit, @@ -95,15 +100,21 @@ let impl_ident_head = | _ -> err ()) | _ -> err ()) -let ident_colon = - Gram.Entry.of_parser "ident_colon" +let name_colon = + Gram.Entry.of_parser "name_colon" (fun strm -> match get_tok (stream_nth 0 strm) with | IDENT s -> (match get_tok (stream_nth 1 strm) with | KEYWORD ":" -> stream_njunk 2 strm; - Names.id_of_string s + Name (Names.id_of_string s) + | _ -> err ()) + | KEYWORD "_" -> + (match get_tok (stream_nth 1 strm) with + | KEYWORD ":" -> + stream_njunk 2 strm; + Anonymous | _ -> err ()) | _ -> err ()) @@ -378,8 +389,7 @@ GEXTEND Gram [LocalRawAssum (id::idl,Default Explicit,c)] (* binders factorized with open binder *) | id = name; idl = LIST0 name; bl = binders -> - let t = CHole (loc, Some (Evd.BinderType (snd id))) in - LocalRawAssum (id::idl,Default Explicit,t)::bl + binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> [LocalRawAssum ([id1;(loc,Name ldots_var);id2], Default Explicit,CHole (loc,None))] @@ -421,8 +431,8 @@ GEXTEND Gram [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> id, expl, c - | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> - (loc, Name iid), expl, c + | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> + (loc, iid), expl, c | c = operconstr LEVEL "200" -> (loc, Anonymous), false, c ] ] diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 9abb8cd1..23e7e31b 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -23,11 +23,6 @@ let thm_token = G_vernac.thm_token GEXTEND Gram GLOBAL: command; - destruct_location : - [ [ IDENT "Conclusion" -> Tacexpr.ConclLocation () - | discard = [ IDENT "Discardable" -> true | -> false ]; "Hypothesis" - -> Tacexpr.HypLocation discard ] ] - ; opt_hintbases: [ [ -> [] | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] @@ -58,9 +53,6 @@ GEXTEND Gram | IDENT "Defined" -> VernacEndProof (Proved (false,None)) | IDENT "Defined"; id=identref -> VernacEndProof (Proved (false,Some (id,None))) - | IDENT "Suspend" -> VernacSuspend - | IDENT "Resume" -> VernacResume None - | IDENT "Resume"; id = identref -> VernacResume (Some id) | IDENT "Restart" -> VernacRestart | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n @@ -68,9 +60,7 @@ GEXTEND Gram | IDENT "Focus" -> VernacFocus None | IDENT "Focus"; n = natural -> VernacFocus (Some n) | IDENT "Unfocus" -> VernacUnfocus - | IDENT "BeginSubproof" -> VernacSubproof None - | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n) - | IDENT "EndSubproof" -> VernacEndSubproof + | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) | IDENT "Show"; IDENT "Goal"; n = string -> @@ -118,14 +108,7 @@ GEXTEND Gram | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> - HintsExtern (n,c,tac) - | IDENT "Destruct"; - id = ident; ":="; - pri = natural; - dloc = destruct_location; - hyptyp = constr_pattern; - "=>"; tac = tactic -> - HintsDestruct(id,pri,dloc,hyptyp,tac) ] ] + HintsExtern (n,c,tac) ] ] ; constr_body: [ [ ":="; c = lconstr -> c diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index f1b3ffed..34590fb1 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -348,7 +348,7 @@ GEXTEND Gram | IDENT "lazy"; s = strategy_flag -> Lazy s | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) | IDENT "vm_compute" -> CbvVm - | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul + | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl | s = IDENT -> ExtraRedExpr s ] ] @@ -597,21 +597,18 @@ GEXTEND Gram (* Automation tactic *) | IDENT "trivial"; lems = auto_using; db = hintbases -> - TacTrivial (lems,db) + TacTrivial (Off,lems,db) + | IDENT "info_trivial"; lems = auto_using; db = hintbases -> + TacTrivial (Info,lems,db) + | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases -> + TacTrivial (Debug,lems,db) + | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases -> - TacAuto (n,lems,db) - -(* Obsolete since V8.0 - | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n - | IDENT "cdhyp"; id = identref -> TacDestructHyp (true,id) - | IDENT "dhyp"; id = identref -> TacDestructHyp (false,id) - | IDENT "dconcl" -> TacDestructConcl - | IDENT "superauto"; l = autoargs -> TacSuperAuto l -*) - | IDENT "auto"; IDENT "decomp"; p = OPT natural; - lems = auto_using -> TacDAuto (None,p,lems) - | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural; - lems = auto_using -> TacDAuto (n,p,lems) + TacAuto (Off,n,lems,db) + | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; + db = hintbases -> TacAuto (Info,n,lems,db) + | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; + db = hintbases -> TacAuto (Debug,n,lems,db) (* Context management *) | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ac81786b..333934be 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -143,7 +143,7 @@ let test_plurial_form_types = function (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - typeclass_constraint record_field decl_notation rec_definition; + record_field decl_notation rec_definition; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -656,6 +656,7 @@ GEXTEND Gram | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] | IDENT "rename" -> [`Rename] + | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> [`ClearImplicits; `ClearScopes] | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> @@ -927,7 +928,6 @@ GEXTEND Gram (* Resetting *) | IDENT "Reset"; id = identref -> VernacResetName id - | IDENT "Delete"; id = identref -> VernacRemoveName id | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 4970ca13..fa075536 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -219,25 +219,33 @@ let surround_impl k p = | 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"}") - | Generalized (b, b', t) -> - surround_impl b' (surround_impl b p) + | Explicit -> p + | Implicit -> (str"{" ++ p ++ str"}") let pr_binder many pr (nal,k,t) = - match t with - | CHole _ -> prlist_with_sep spc pr_lname nal - | _ -> - let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in - hov 1 (if many then surround_binder k s else surround_implicit k s) + match k with + | Generalized (b, b', t') -> + assert (b=Implicit); + begin match nal with + |[loc,Anonymous] -> + hov 1 (str"`" ++ (surround_impl b' + ((if t' then str "!" else mt ()) ++ pr t))) + |[loc,Name id] -> + hov 1 (str "`" ++ (surround_impl b' + (pr_lident (loc,id) ++ str " : " ++ + (if t' then str "!" else mt()) ++ pr t))) + |_ -> anomaly "List of generalized binders have alwais one element." + end + | Default b -> + match t with + | CHole _ -> + let s = prlist_with_sep spc pr_lname nal in + hov 1 (surround_implicit b s) + | _ -> + let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in + hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function | LocalRawAssum (nal,k,t) -> @@ -323,19 +331,27 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c -let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) = - let annot = - match ro with - CStructRec -> - if List.length bl > 1 && n <> None then - spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}" - else mt() - | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}" - | CMeasureRec (m,r) -> - spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++ - (match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}" - in +let pr_guard_annot pr_aux bl (n,ro) = + match n with + | None -> mt () + | Some (loc, id) -> + match (ro : Topconstr.recursion_order_expr) with + | CStructRec -> + let names_of_binder = function + | LocalRawAssum (nal,_,_) -> nal + | LocalRawDef (_,_) -> [] + in let ids = List.flatten (List.map names_of_binder bl) in + if List.length ids > 1 then + spc() ++ str "{struct " ++ pr_id id ++ str"}" + else mt() + | CWfRec c -> + spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}" + | CMeasureRec (m,r) -> + spc() ++ str "{measure " ++ pr_aux m ++ spc() ++ pr_id id++ + (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" + +let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let annot = pr_guard_annot (pr lsimple) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index f9ed3af0..afcdad3e 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -51,12 +51,16 @@ val pr_with_occurrences : ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - ('a,'b,'c) red_expr_gen -> std_ppcmds + ('a,'b,'c) red_expr_gen -> std_ppcmds val pr_may_eval : ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds +val pr_guard_annot : (constr_expr -> std_ppcmds) -> + local_binder list -> + ('a * Names.identifier) option * recursion_order_expr -> + std_ppcmds val pr_binders : local_binder list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3305acb7..6e13d4e9 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -515,6 +515,11 @@ let pr_auto_using prc = function | l -> spc () ++ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l) +let string_of_debug = function + | Off -> "" + | Debug -> "debug " + | Info -> "info_" + let pr_then () = str ";" let ltop = (5,E) @@ -623,19 +628,14 @@ let rec pr_atom0 = function | TacAssumption -> str "assumption" | TacAnyConstructor (false,None) -> str "constructor" | TacAnyConstructor (true,None) -> str "econstructor" - | TacTrivial ([],Some []) -> str "trivial" - | TacAuto (None,[],Some []) -> str "auto" + | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial") + | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto") | TacReflexivity -> str "reflexivity" | TacClear (true,[]) -> str "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" (* Main tactic printer *) and pr_atom1 = function - | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl - | TacSuperAuto _ | TacExtend (_, - ("GTauto"|"GIntuition"|"TSimplif"| - "LinearIntuition"),_) -> - errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0") | TacExtend (loc,s,l) -> pr_with_comments loc (pr_extend 1 s l) | TacAlias (loc,s,l,_) -> @@ -742,17 +742,15 @@ and pr_atom1 = function hov 1 (str "lapply" ++ pr_constrarg c) (* Automation tactics *) - | TacTrivial ([],Some []) as x -> pr_atom0 x - | TacTrivial (lems,db) -> - hov 0 (str "trivial" ++ + | TacTrivial (_,[],Some []) as x -> pr_atom0 x + | TacTrivial (d,lems,db) -> + hov 0 (str (string_of_debug d ^ "trivial") ++ pr_auto_using pr_constr lems ++ pr_hintbases db) - | TacAuto (None,[],Some []) as x -> pr_atom0 x - | TacAuto (n,lems,db) -> - hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ + | TacAuto (_,None,[],Some []) as x -> pr_atom0 x + | TacAuto (d,n,lems,db) -> + hov 0 (str (string_of_debug d ^ "auto") ++ + pr_opt (pr_or_var int) n ++ pr_auto_using pr_constr lems ++ pr_hintbases db) - | TacDAuto (n,p,lems) -> - hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ - pr_opt int p ++ pr_auto_using pr_constr lems) (* Context management *) | TacClear (true,[]) as t -> pr_atom0 t diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index c858439e..cf9d4a53 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -203,11 +203,7 @@ let pr_hints local db h pr_c pr_pat = 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() ++ - pr_c c ++ str " =>") ++ spc() ++ - pr_raw_tactic tac in + in hov 2 (str"Hint "++pr_locality local ++ pph ++ opth) let pr_with_declaration pr_c = function @@ -292,28 +288,6 @@ let pr_binders_arg = let pr_and_type_binders_arg bl = pr_binders_arg bl -let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - -let pr_guard_annot bl (n,ro) = - match n with - | None -> mt () - | Some (loc, id) -> - match (ro : Topconstr.recursion_order_expr) with - | CStructRec -> - let ids = List.flatten (List.map names_of_binder bl) in - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_id id ++ str"}" - else mt() - | CWfRec c -> - spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ - pr_id id ++ str"}" - | CMeasureRec (m,r) -> - spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++ - pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++ - pr_lconstr_expr r) ++ str"}" - let pr_onescheme (idop,schem) = match schem with | InductionScheme (dep,ind,s) -> @@ -419,7 +393,7 @@ let pr_statement head (id,(bl,c,guard)) = hov 1 (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++ (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++ - pr_opt (pr_guard_annot bl) guard ++ + pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) (**************************************) @@ -462,11 +436,10 @@ let rec pr_vernac = function (* Proof management *) | VernacAbortAll -> str "Abort All" | VernacRestart -> str"Restart" - | VernacSuspend -> str"Suspend" | VernacUnfocus -> str"Unfocus" + | VernacUnfocused -> str"Unfocused" | VernacGoal c -> str"Goal" ++ pr_lconstrarg c | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id - | VernacResume id -> str"Resume" ++ pr_opt pr_lident id | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i | VernacBacktrack (i,j,k) -> @@ -493,7 +466,6 @@ let rec pr_vernac = function | VernacCheckGuard -> str"Guarded" (* Resetting *) - | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id | VernacResetInitial -> str"Reset Initial" | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i @@ -627,7 +599,7 @@ let rec pr_vernac = function let (_,_,_,k,_),_ = List.hd l in match k with Record -> "Record" | Structure -> "Structure" | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class b -> if b then "Definitional Class" else "Class" in + | Class _ -> "Class" in hov 1 (pr_oneind key (List.hd l)) ++ (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) @@ -635,10 +607,10 @@ let rec pr_vernac = function | VernacFixpoint recs -> let pr_onerec = function | ((loc,id),ro,bl,type_,def),ntn -> - let annot = pr_guard_annot bl ro in - pr_id id ++ pr_binders_arg bl ++ annot ++ spc() + let annot = pr_guard_annot pr_lconstr_expr bl ro in + pr_id id ++ pr_binders_arg bl ++ annot ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ - ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++ + ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++ prlist (pr_decl_notation pr_constr) ntn in hov 0 (str "Fixpoint" ++ spc() ++ @@ -690,34 +662,23 @@ let rec pr_vernac = function 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_glob_sort (snd ar) | None -> mt()) ++ *) -(* spc () ++ str":=" ++ 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 (abst,glob, sup, (instid, bk, cl), props, pri) -> hov 1 ( pr_non_locality (not glob) ++ (if abst then str"Declare " else mt ()) ++ - 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 () ++ + str"Instance" ++ + (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | + Anonymous -> mt ()) ++ + pr_and_type_binders_arg sup ++ + str":" ++ spc () ++ + pr_constr_expr cl ++ spc () ++ (match props with | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p | None -> mt())) | VernacContext l -> hov 1 ( - str"Context" ++ spc () ++ str"[" ++ spc () ++ - pr_and_type_binders_arg l ++ spc () ++ str "]") + str"Context" ++ spc () ++ pr_and_type_binders_arg l) | VernacDeclareInstances (glob, ids) -> @@ -817,8 +778,8 @@ let rec pr_vernac = function pr_hints local dbnames h pr_constr pr_constr_pattern_expr | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) -> hov 2 - (pr_locality local ++ str"Notation " ++ pr_lident id ++ - prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ + (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++ + prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ @@ -852,6 +813,7 @@ let rec pr_vernac = function | `SimplNeverUnfold -> str "simpl never" | `DefaultImplicits -> str "default implicits" | `Rename -> str "rename" + | `ExtraScopes -> str "extra scopes" | `ClearImplicits -> str "clear implicits" | `ClearScopes -> str "clear scopes") mods) @@ -978,9 +940,9 @@ let rec pr_vernac = function | Star -> str"*" | Plus -> str"+" end ++ spc() - | VernacSubproof None -> str "BeginSubproof" + | VernacSubproof None -> str "{" | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i - | VernacEndSubproof -> str "EndSubproof" + | VernacEndSubproof -> str "}" and pr_extend s cl = let pr_arg a = diff --git a/parsing/printer.ml b/parsing/printer.ml index 0b9ce918..5352e0b7 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -35,13 +35,19 @@ let delayed_emacs_cmd s = (**********************************************************************) (** Terms *) - (* [at_top] means ids of env must be avoided in bound variables *) -let pr_constr_core at_top env t = - pr_constr_expr (extern_constr at_top env t) -let pr_lconstr_core at_top env t = - pr_lconstr_expr (extern_constr at_top env t) +(* [goal_concl_style] means that all names of goal/section variables + and all names of rel variables (if any) in the given env and all short + names of global definitions of the current module must be avoided while + printing bound variables. + Otherwise, short names of global definitions are printed qualified + and only names of goal/section variables and rel names that do + _not_ occur in the scope of the binder to be printed are avoided. *) + +let pr_constr_core goal_concl_style env t = + pr_constr_expr (extern_constr goal_concl_style env t) +let pr_lconstr_core goal_concl_style env t = + pr_lconstr_expr (extern_constr goal_concl_style env t) -let pr_lconstr_env_at_top env = pr_lconstr_core true env let pr_lconstr_env env = pr_lconstr_core false env let pr_constr_env env = pr_constr_core false env @@ -68,12 +74,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c -let pr_type_core at_top env t = - pr_constr_expr (extern_type at_top env t) -let pr_ltype_core at_top env t = - pr_lconstr_expr (extern_type at_top env t) +let pr_type_core goal_concl_style env t = + pr_constr_expr (extern_type goal_concl_style env t) +let pr_ltype_core goal_concl_style env t = + pr_lconstr_expr (extern_type goal_concl_style env t) -let pr_ltype_env_at_top env = pr_ltype_core true env +let pr_goal_concl_style_env env = pr_ltype_core true env let pr_ltype_env env = pr_ltype_core false env let pr_type_env env = pr_type_core false env @@ -262,7 +268,7 @@ let default_pr_goal gs = let preamb,thesis,penv,pc = mt (), mt (), pr_context_of env, - pr_ltype_env_at_top env (Goal.V82.concl sigma g) + pr_goal_concl_style_env env (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ @@ -279,7 +285,7 @@ let pr_goal_tag g = let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in - let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in + let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in str (emacs_str "") ++ str "subgoal " ++ int n ++ pr_goal_tag g ++ str " is:" ++ cut () ++ str" " ++ pc @@ -363,7 +369,8 @@ let default_pr_subgoals close_cmd sigma seeds = function let pei = pr_evars_int 1 exl in (str "No more subgoals but non-instantiated existential " ++ str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end | [g] -> let pg = default_pr_goal { it = g ; sigma = sigma } in @@ -424,7 +431,7 @@ let pr_open_subgoals () = begin match bgoals with | [] -> pr_subgoals None sigma seeds goals | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++ - str"This subproof is complete, but there are still unfocused goals:" + str"This subproof is complete, but there are still unfocused goals." ++ fnl () (* spiwack: to stay compatible with the proof general and coqide, I use print the message after the goal. It would be better to have something like: diff --git a/parsing/printer.mli b/parsing/printer.mli index 2d437c20..bbc3a6ca 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -26,7 +26,6 @@ open Tacexpr (** Terms *) val pr_lconstr_env : env -> constr -> std_ppcmds -val pr_lconstr_env_at_top : env -> constr -> std_ppcmds val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds @@ -44,7 +43,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds -val pr_ltype_env_at_top : env -> types -> std_ppcmds +val pr_goal_concl_style_env : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 7df97a07..6e3b3f35 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -273,6 +273,11 @@ let mlexpr_of_message_token = function | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >> | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >> +let mlexpr_of_debug = function + | Tacexpr.Off -> <:expr< Tacexpr.Off >> + | Tacexpr.Debug -> <:expr< Tacexpr.Debug >> + | Tacexpr.Info -> <:expr< Tacexpr.Info >> + let rec mlexpr_of_atomic_tactic = function (* Basic tactics *) | Tacexpr.TacIntroPattern pl -> @@ -399,15 +404,17 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> (* Automation tactics *) - | Tacexpr.TacAuto (n,lems,l) -> + | Tacexpr.TacAuto (debug,n,lems,l) -> + let d = mlexpr_of_debug debug in let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in let lems = mlexpr_of_list mlexpr_of_constr lems in let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in - <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >> - | Tacexpr.TacTrivial (lems,l) -> + <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >> + | Tacexpr.TacTrivial (debug,lems,l) -> + let d = mlexpr_of_debug debug in let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in let lems = mlexpr_of_list mlexpr_of_constr lems in - <:expr< Tacexpr.TacTrivial $lems$ $l$ >> + <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >> | _ -> failwith "Quotation of atomic tactic expressions: TODO" diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 2fe1fdda..05fdba42 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -119,20 +119,42 @@ let make_one_printing_rule se (pt,e) = let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se) -let rec contains_epsilon = function - | List0ArgType _ -> true - | List1ArgType t -> contains_epsilon t - | OptArgType _ -> true - | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2 - | ExtraArgType("hintbases") -> true - | _ -> false -let is_atomic = function - | GramTerminal s :: l when - List.for_all (function - GramTerminal _ -> false - | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l - -> [s] - | _ -> [] +let rec possibly_empty_subentries loc = function + | [] -> [] + | (s,prodsl) :: l -> + let rec aux = function + | [] -> (false,<:expr< None >>) + | prods :: rest -> + try + let l = List.map (function + | GramNonTerminal(_,(List0ArgType _| + OptArgType _| + ExtraArgType _ as t),_,_)-> + (* This possibly parses epsilon *) + let rawwit = make_rawwit loc t in + <:expr< match Genarg.default_empty_value $rawwit$ with + [ None -> failwith "" + | Some v -> + Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign + (Genarg.in_gen $rawwit$ v) ] >> + | GramTerminal _ | GramNonTerminal(_,_,_,_) -> + (* This does not parse epsilon (this Exit is static time) *) + raise Exit) prods in + if has_extraarg prods then + (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$ + with [ Failure "" -> $snd (aux rest)$ ] >>) + else + (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>) + with Exit -> aux rest in + let (nonempty,v) = aux prodsl in + if nonempty then (s,v) :: possibly_empty_subentries loc l + else possibly_empty_subentries loc l + +let possibly_atomic loc prods = + let l = list_map_filter (function + | GramTerminal s :: l, _ -> Some (s,l) + | _ -> None) prods in + possibly_empty_subentries loc (list_factorize_left l) let declare_tactic loc s cl = let se = mlexpr_of_string s in @@ -151,17 +173,20 @@ let declare_tactic loc s cl = in let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in let atomic_tactics = - mlexpr_of_list mlexpr_of_string - (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in + mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x)) + (possibly_atomic loc cl) in declare_str_items loc (hidden @ [ <:str_item< do { try let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in List.iter - (fun s -> Tacinterp.add_primitive_tactic s + (fun (s,l) -> match l with + [ Some l -> + Tacinterp.add_primitive_tactic s (Tacexpr.TacAtom($default_loc$, - Tacexpr.TacExtend($default_loc$,s,[])))) + Tacexpr.TacExtend($default_loc$,$se$,l))) + | None -> () ]) $atomic_tactics$ with e -> Pp.pp (Errors.print e); Egrammar.extend_tactic_grammar $se$ $gl$; -- cgit v1.2.3