diff options
| author | glondu | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /parsing | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
33 files changed, 912 insertions, 912 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 539b203d01..89edbb1230 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -40,7 +40,7 @@ let rec make_rawwit loc = function | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >> - | PairArgType (t1,t2) -> + | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> @@ -65,7 +65,7 @@ let rec make_globwit loc = function | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >> - | PairArgType (t1,t2) -> + | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >> | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >> @@ -90,7 +90,7 @@ let rec make_wit loc = function | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> + | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >> @@ -100,7 +100,7 @@ let make_act loc act pil = | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.string_of_id p in <:expr< - Gramext.action + Gramext.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) >> @@ -131,14 +131,14 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let interp = match f with - | None -> + | None -> <:expr< fun ist gl x -> out_gen $make_wit loc typ$ (Tacinterp.interp_genarg ist gl (Genarg.in_gen $make_globwit loc globtyp$ x)) >> | Some f -> <:expr< $lid:f$>> in let substitute = match h with - | None -> + | None -> <:expr< fun s x -> out_gen $make_globwit loc globtyp$ (Tacinterp.subst_genarg s @@ -163,7 +163,7 @@ let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl = (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), (fun subst x -> (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); - Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None + Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; Pptactic.declare_extra_genarg_pprule ($rawwit$, $lid:rawpr$) @@ -189,7 +189,7 @@ let declare_vernac_argument loc s pr cl = ($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 + Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) @@ -213,10 +213,10 @@ EXTEND h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; rawtyppr = (* Necessary if the globalized type is different from the final type *) - OPT [ "RAW_TYPED"; "AS"; t = argtype; + OPT [ "RAW_TYPED"; "AS"; t = argtype; "RAW_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; globtyppr = - OPT [ "GLOB_TYPED"; "AS"; t = argtype; + OPT [ "GLOB_TYPED"; "AS"; t = argtype; "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> @@ -232,7 +232,7 @@ EXTEND declare_vernac_argument loc s pr l ] ] ; argtype: - [ "2" + [ "2" [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ] | "1" [ e = argtype; LIDENT "list" -> List0ArgType e diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 87e8e1deb2..8d90499dc2 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -22,9 +22,9 @@ open Names open Vernacexpr (**************************************************************************) -(* +(* * --- Note on the mapping of grammar productions to camlp4 actions --- - * + * * Translation of environments: a production * [ nt1(x1) ... nti(xi) ] -> act(x1..xi) * is written (with camlp4 conventions): @@ -34,9 +34,9 @@ open Vernacexpr * the make_*_action family build the following closure: * * ((fun env -> - * (fun vi -> + * (fun vi -> * (fun env -> ... - * + * * (fun v1 -> * (fun env -> gram_action .. env act) * ((x1,v1)::env)) @@ -81,7 +81,7 @@ let make_constr_action make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl) | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:constr_expr list) -> make (env, v::envlist) tl) - | Some (p, ETPattern) :: tl -> + | Some (p, ETPattern) :: tl -> failwith "Unexpected entry of type cases pattern" in make ([],[]) (List.rev pil) @@ -106,7 +106,7 @@ let make_cases_pattern_action | Some (p, ETConstrList _) :: tl -> Gramext.action (fun (v:cases_pattern_expr list) -> make (env, v :: envlist) tl) - | Some (p, (ETPattern | ETOther _)) :: tl -> + | Some (p, (ETPattern | ETOther _)) :: tl -> failwith "Unexpected entry of type cases pattern or other" in make ([],[]) (List.rev pil) @@ -153,7 +153,7 @@ let extend_constr_notation (n,assoc,ntn,rule) = let make_generic_action (f:loc -> ('b * raw_generic_argument) list -> 'a) pil = let rec make env = function - | [] -> + | [] -> Gramext.action (fun loc -> f loc env) | None :: tl -> (* parse a non-binding item *) Gramext.action (fun _ -> make env tl) @@ -167,7 +167,7 @@ let make_rule univ f g pt = (symbs, act) (**********************************************************************) -(** Grammar extensions declared at ML level *) +(** Grammar extensions declared at ML level *) type grammar_prod_item = | GramTerminal of string @@ -200,7 +200,7 @@ let extend_vernac_command_grammar s gl = Gram.extend Vernac_.command None [(None, None, List.rev rules)] (**********************************************************************) -(** Grammar declaration for Tactic Notation (Coq level) *) +(** Grammar declaration for Tactic Notation (Coq level) *) let get_tactic_entry n = if n = 0 then @@ -209,7 +209,7 @@ let get_tactic_entry n = weaken_entry Tactic.binder_tactic, None else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) - else + else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") (* Declaration of the tactic grammar rule *) @@ -219,7 +219,7 @@ let head_is_ident = function GramTerminal _::_ -> true | _ -> false let add_tactic_entry (key,lev,prods,tac) = let univ = get_univ "tactic" in let entry, pos = get_tactic_entry lev in - let rules = + let rules = if lev = 0 then begin if not (head_is_ident prods) then error "Notation for simple tactic must start with an identifier."; @@ -228,7 +228,7 @@ let add_tactic_entry (key,lev,prods,tac) = make_rule univ (mkact key tac) make_prod_item prods end else - let mkact s tac loc l = + let mkact s tac loc l = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in make_rule univ (mkact key tac) make_prod_item prods in synchronize_level_positions (); @@ -237,7 +237,7 @@ let add_tactic_entry (key,lev,prods,tac) = (**********************************************************************) (** State of the grammar extensions *) -type notation_grammar = +type notation_grammar = int * Gramext.g_assoc option * notation * grammar_constr_prod_item list type all_grammar_command = @@ -268,7 +268,7 @@ type frozen_t = all_grammar_command list * Lexer.frozen_t let freeze () = (!grammar_state, Lexer.freeze ()) -(* We compare the current state of the grammar and the state to unfreeze, +(* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) let factorize_grams l1 l2 = if l1 == l2 then ([], [], l1) else list_share_tails l1 l2 @@ -288,7 +288,7 @@ let unfreeze (grams, lex) = grammar_state := common; Lexer.unfreeze lex; List.iter extend_grammar (List.rev redo) - + let init_grammar () = remove_grammars (number_of_entries !grammar_state); grammar_state := [] @@ -298,7 +298,7 @@ let init () = open Summary -let _ = +let _ = declare_summary "GRAMMAR_LEXER" { freeze_function = freeze; unfreeze_function = unfreeze; diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e632e5bb81..14e4cfd37e 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -22,7 +22,7 @@ open Mod_subst (*i*) (** Mapping of grammar productions to camlp4 actions - Used for Coq-level Notation and Tactic Notation, + Used for Coq-level Notation and Tactic Notation, and for ML-level tactic and vernac extensions *) @@ -32,14 +32,14 @@ type grammar_constr_prod_item = | GramConstrTerminal of Token.pattern | GramConstrNonTerminal of constr_prod_entry_key * identifier option -type notation_grammar = +type notation_grammar = int * Gramext.g_assoc option * notation * grammar_constr_prod_item list (* For tactic and vernac notations *) type grammar_prod_item = | GramTerminal of string - | GramNonTerminal of loc * argument_type * + | GramNonTerminal of loc * argument_type * Gram.te prod_entry_key * identifier option (* Adding notations *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f91f0170c7..7e2b41926c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -22,7 +22,7 @@ open Topconstr open Util let constr_kw = - [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; "Prop"; "Set"; "Type"; ".("; "_"; ".."; "`{"; "`("; "{|"; "|}" ] @@ -39,10 +39,10 @@ let loc_of_binder_let = function | _ -> dummy_loc let binders_of_lidents l = - List.map (fun (loc, id) -> - LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + 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 @@ -70,7 +70,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = - if kw then + if kw then let fb = List.map mk_fixb dcls in CFix(loc,id,fb) else @@ -101,16 +101,16 @@ let impl_ident = Gram.Entry.of_parser "impl_ident" (fun strm -> match Stream.npeek 1 strm with - | [(_,"{")] -> + | [(_,"{")] -> (match Stream.npeek 2 strm with | [_;("IDENT",("wf"|"struct"|"measure"))] -> raise Stream.Failure - | [_;("IDENT",s)] -> + | [_;("IDENT",s)] -> Stream.junk strm; Stream.junk strm; Names.id_of_string s | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) - + let ident_colon = Gram.Entry.of_parser "ident_colon" (fun strm -> @@ -134,7 +134,7 @@ let ident_with = Names.id_of_string s | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) - + let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None GEXTEND Gram @@ -169,21 +169,21 @@ GEXTEND Gram [ [ c = operconstr LEVEL "200" -> c ] ] ; constr: - [ [ c = operconstr LEVEL "8" -> c + [ [ c = operconstr LEVEL "8" -> c | "@"; f=global -> CAppExpl(loc,(None,f),[]) ] ] ; operconstr: [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> + [ c1 = operconstr; "<:"; c2 = binder_constr -> CCast(loc,c1, CastConv (VMcast,c2)) - | c1 = operconstr; "<:"; c2 = SELF -> + | c1 = operconstr; "<:"; c2 = SELF -> CCast(loc,c1, CastConv (VMcast,c2)) - | c1 = operconstr; ":";c2 = binder_constr -> + | c1 = operconstr; ":";c2 = binder_constr -> + CCast(loc,c1, CastConv (DEFAULTcast,c2)) + | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1, CastConv (DEFAULTcast,c2)) - | c1 = operconstr; ":"; c2 = SELF -> - CCast(loc,c1, CastConv (DEFAULTcast,c2)) | c1 = operconstr; ":>" -> CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] @@ -205,7 +205,7 @@ GEXTEND Gram CApp(loc,(Some (List.length args+1),CRef f),args@[c,None]) | c=operconstr; ".("; "@"; f=global; args=LIST0 (operconstr LEVEL "9"); ")" -> - CAppExpl(loc,(Some (List.length args+1),f),args@[c]) + CAppExpl(loc,(Some (List.length args+1),f),args@[c]) | c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] | "0" [ c=atomic_constr -> c @@ -222,13 +222,13 @@ GEXTEND Gram CGeneralization (loc, Explicit, None, c) ] ] ; - forall: - [ [ "forall" -> () + forall: + [ [ "forall" -> () | IDENT "Π" -> () ] ] ; - lambda: - [ [ "fun" -> () + lambda: + [ [ "fun" -> () | IDENT "λ" -> () ] ] ; @@ -239,7 +239,7 @@ GEXTEND Gram ] ] ; record_field_declaration: - [ [ id = identref; params = LIST0 identref; ":="; c = lconstr -> + [ [ id = identref; params = LIST0 identref; ":="; c = lconstr -> (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: @@ -266,10 +266,10 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)]) - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)]) - | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; + | "let"; "'"; p=pattern; "in"; t = operconstr LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)]) @@ -326,8 +326,8 @@ GEXTEND Gram ; return_type: [ [ a = OPT [ na = OPT["as"; id=name -> snd id]; - ty = case_type -> (na,ty) ] -> - match a with + ty = case_type -> (na,ty) ] -> + match a with | None -> None, None | Some (na,t) -> (na, Some t) ] ] @@ -351,7 +351,7 @@ GEXTEND Gram [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) - | _ -> Util.user_err_loc + | _ -> Util.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", Pp.str "Constructor expected.")) | p = pattern; "as"; id = ident -> @@ -370,9 +370,9 @@ GEXTEND Gram | s = string -> CPatPrim (loc, String s) ] ] ; binder_list: - [ [ idl=LIST1 name; bl=binders_let -> + [ [ idl=LIST1 name; bl=binders_let -> LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl - | idl=LIST1 name; ":"; c=lconstr -> + | idl=LIST1 name; ":"; c=lconstr -> [LocalRawAssum (idl,Default Explicit,c)] | cl = binders_let -> cl ] ] @@ -390,15 +390,15 @@ GEXTEND Gram fixannot: [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec) | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel) - | "{"; IDENT "measure"; m=constr; id=OPT identref; + | "{"; IDENT "measure"; m=constr; id=OPT identref; rel=OPT constr; "}" -> (id, CMeasureRec (m,rel)) ] ] ; binders_let_fixannot: - [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot -> + [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot -> (assum (loc, Name id) :: fst bl), snd bl | f = fixannot -> [], f - | b = binder_let; bl = binders_let_fixannot -> + | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl | -> [], (None, CStructRec) ] ] @@ -410,21 +410,21 @@ GEXTEND Gram binder_let: [ [ id=name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))] - | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> [LocalRawAssum (id::idl,Default Explicit,c)] - | "("; id=name; ":"; c=lconstr; ")" -> + | "("; id=name; ":"; c=lconstr; ")" -> [LocalRawAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> [LocalRawDef (id,c)] - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] | "{"; id=name; "}" -> [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> [LocalRawAssum (id::idl,Default Implicit,c)] - | "{"; id=name; ":"; c=lconstr; "}" -> + | "{"; id=name; ":"; c=lconstr; "}" -> [LocalRawAssum ([id],Default Implicit,c)] - | "{"; id=name; idl=LIST1 name; "}" -> + | "{"; 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], Generalized (Implicit, Explicit, b), t)) tc @@ -434,8 +434,8 @@ GEXTEND Gram ; binder: [ [ id=name -> ([id],Default Explicit,CHole (loc, None)) - | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) - | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) + | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c) + | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) ] ] ; typeclass_constraint: @@ -448,7 +448,7 @@ GEXTEND Gram (loc, Anonymous), false, c ] ] ; - + type_cstr: [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ] ; diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 91433b8a63..e812faeaca 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -29,7 +29,7 @@ let none_is_empty = function GEXTEND Gram GLOBAL: proof_instr; thesis : - [[ "thesis" -> Plain + [[ "thesis" -> Plain | "thesis"; "for"; i=ident -> (For i) ]]; statement : @@ -42,9 +42,9 @@ GLOBAL: proof_instr; [[ t=thesis -> Thesis t ] | [ c=constr -> This c ]]; - statement_or_thesis : + statement_or_thesis : [ - [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] + [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; @@ -52,25 +52,25 @@ GLOBAL: proof_instr; | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; - justification_items : - [[ -> Some [] + justification_items : + [[ -> Some [] | IDENT "by"; l=LIST1 constr SEP "," -> Some l | IDENT "by"; "*" -> None ]] ; - justification_method : - [[ -> None + justification_method : + [[ -> None | "using"; tac = tactic -> Some tac ]] ; simple_cut_or_thesis : [[ ls = statement_or_thesis; j = justification_items; - taco = justification_method + taco = justification_method -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; simple_cut : [[ ls = statement; j = justification_items; - taco = justification_method + taco = justification_method -> {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; elim_type: @@ -82,40 +82,40 @@ GLOBAL: proof_instr; | IDENT "focus" -> B_focus | IDENT "proof" -> B_proof | et=elim_type -> B_elim et ]] - ; + ; elim_obj: [[ IDENT "on"; c=constr -> Real c | IDENT "of"; c=simple_cut -> Virtual c ]] - ; + ; elim_step: - [[ IDENT "consider" ; + [[ IDENT "consider" ; h=consider_vars ; IDENT "from" ; c=constr -> Pconsider (c,h) | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj) | IDENT "suffices"; ls=suff_clause; j = justification_items; - taco = justification_method - -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] + taco = justification_method + -> Psuffices {cut_stat=ls;cut_by=j;cut_using=taco} ]] ; rew_step : - [[ "~=" ; c=simple_cut -> (Rhs,c) + [[ "~=" ; c=simple_cut -> (Rhs,c) | "=~" ; c=simple_cut -> (Lhs,c)]] ; cut_step: [[ "then"; tt=elim_step -> Pthen tt | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) - | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) + | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) | tt=elim_step -> tt - | tt=rew_step -> let s,c=tt in Prew (s,c); + | tt=rew_step -> let s,c=tt in Prew (s,c); | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; | IDENT "claim"; c=statement -> Pclaim c; - | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; + | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; | "end"; bt = block_type -> Pend bt; | IDENT "escape" -> Pescape ]] ; (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) - loc_id: + loc_id: [[ id=ident -> fun x -> (loc,(id,x)) ]]; hyp: [[ id=loc_id -> id None ; @@ -124,27 +124,27 @@ GLOBAL: proof_instr; consider_vars: [[ name=hyp -> [Hvar name] | name=hyp; ","; v=consider_vars -> (Hvar name) :: v - | name=hyp; + | name=hyp; IDENT "such"; IDENT "that"; h=consider_hyps -> (Hvar name)::h ]] ; - consider_hyps: + consider_hyps: [[ st=statement; IDENT "and"; h=consider_hyps -> Hprop st::h - | st=statement; IDENT "and"; + | st=statement; IDENT "and"; IDENT "consider" ; v=consider_vars -> Hprop st::v | st=statement -> [Hprop st] ]] - ; + ; assume_vars: [[ name=hyp -> [Hvar name] | name=hyp; ","; v=assume_vars -> (Hvar name) :: v - | name=hyp; + | name=hyp; IDENT "such"; IDENT "that"; h=assume_hyps -> (Hvar name)::h ]] ; - assume_hyps: + assume_hyps: [[ st=statement; IDENT "and"; h=assume_hyps -> Hprop st::h - | st=statement; IDENT "and"; + | st=statement; IDENT "and"; IDENT "we"; IDENT "have" ; v=assume_vars -> Hprop st::v | st=statement -> [Hprop st] ]] @@ -152,38 +152,38 @@ GLOBAL: proof_instr; assume_clause: [[ IDENT "we" ; IDENT "have" ; v=assume_vars -> v | h=assume_hyps -> h ]] - ; + ; suff_vars: [[ name=hyp; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> [Hvar name],c - | name=hyp; ","; v=suff_vars -> + | name=hyp; ","; v=suff_vars -> let (q,c) = v in ((Hvar name) :: q),c - | name=hyp; - IDENT "such"; IDENT "that"; h=suff_hyps -> + | name=hyp; + IDENT "such"; IDENT "that"; h=suff_hyps -> let (q,c) = h in ((Hvar name) :: q),c ]]; - suff_hyps: - [[ st=statement; IDENT "and"; h=suff_hyps -> + suff_hyps: + [[ st=statement; IDENT "and"; h=suff_hyps -> let (q,c) = h in (Hprop st::q),c - | st=statement; IDENT "and"; - IDENT "to" ; IDENT "have" ; v=suff_vars -> + | st=statement; IDENT "and"; + IDENT "to" ; IDENT "have" ; v=suff_vars -> let (q,c) = v in (Hprop st::q),c - | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> + | st=statement; IDENT "to"; IDENT "show" ; c = constr_or_thesis -> [Hprop st],c ]] ; suff_clause: [[ IDENT "to" ; IDENT "have" ; v=suff_vars -> v | h=suff_hyps -> h ]] - ; + ; let_vars: [[ name=hyp -> [Hvar name] | name=hyp; ","; v=let_vars -> (Hvar name) :: v - | name=hyp; IDENT "be"; + | name=hyp; IDENT "be"; IDENT "such"; IDENT "that"; h=let_hyps -> (Hvar name)::h ]] ; - let_hyps: + let_hyps: [[ st=statement; IDENT "and"; h=let_hyps -> Hprop st::h | st=statement; IDENT "and"; "let"; v=let_vars -> Hprop st::v | st=statement -> [Hprop st] @@ -194,19 +194,19 @@ GLOBAL: proof_instr; | name=hyp; IDENT "such"; IDENT "that"; h=given_hyps -> (Hvar name)::h ]] ; - given_hyps: + given_hyps: [[ st=statement; IDENT "and"; h=given_hyps -> Hprop st::h | st=statement; IDENT "and"; IDENT "given"; v=given_vars -> Hprop st::v | st=statement -> [Hprop st] ]]; suppose_vars: - [[name=hyp -> [Hvar name] + [[name=hyp -> [Hvar name] |name=hyp; ","; v=suppose_vars -> (Hvar name) :: v - |name=hyp; OPT[IDENT "be"]; + |name=hyp; OPT[IDENT "be"]; IDENT "such"; IDENT "that"; h=suppose_hyps -> (Hvar name)::h ]] ; - suppose_hyps: + suppose_hyps: [[ st=statement_or_thesis; IDENT "and"; h=suppose_hyps -> Hprop st::h | st=statement_or_thesis; IDENT "and"; IDENT "we"; IDENT "have"; v=suppose_vars -> Hprop st::v @@ -220,20 +220,20 @@ GLOBAL: proof_instr; intro_step: [[ IDENT "suppose" ; h=assume_clause -> Psuppose h | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; - po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; - ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> + po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; + ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> Pcase (none_is_empty po,c,none_is_empty ho) - | "let" ; v=let_vars -> Plet v + | "let" ; v=let_vars -> Plet v | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses | IDENT "assume"; h=assume_clause -> Passume h | IDENT "given"; h=given_vars -> Pgiven h - | IDENT "define"; id=ident; args=LIST0 hyp; + | IDENT "define"; id=ident; args=LIST0 hyp; "as"; body=constr -> Pdefine(id,args,body) | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) ]] ; - emphasis : + emphasis : [[ -> 0 | "*" -> 1 | "**" -> 2 @@ -249,4 +249,4 @@ GLOBAL: proof_instr; ; END;; - + diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index f869dc8e8d..7f63428c83 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -35,7 +35,7 @@ GEXTEND Gram tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) - | -> [||] + | -> [||] ] ] ; tactic_then_gen: @@ -54,7 +54,7 @@ GEXTEND Gram [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, [||], ta1, [||]) | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, [||], ta1, [||]) | ta0 = tactic_expr; ";"; "["; (first,tail) = tactic_then_gen; "]" -> - match tail with + match tail with | Some (t,last) -> TacThen (ta0, Array.of_list first, t, last) | None -> TacThens (ta0,first) ] | "3" RIGHTA @@ -94,7 +94,7 @@ GEXTEND Gram TacArg(MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> TacArg(ConstrMayEval(ConstrTerm c)) - | IDENT "ipattern"; ":"; ipat = simple_intropattern -> + | IDENT "ipattern"; ":"; ipat = simple_intropattern -> TacArg(IntroPattern ipat) | r = reference; la = LIST0 tactic_arg -> TacArg(TacCall (loc,r,la)) ] @@ -107,7 +107,7 @@ GEXTEND Gram [ RIGHTA [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> TacFun (it,body) - | "let"; isrec = [IDENT "rec" -> true | -> false]; + | "let"; isrec = [IDENT "rec" -> true | -> false]; llc = LIST1 let_clause SEP "with"; "in"; body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] @@ -153,7 +153,7 @@ GEXTEND Gram [ [ "match" -> false | "lazymatch" -> true ] ] ; input_fun: - [ [ "_" -> None + [ [ "_" -> None | l = ident -> Some l ] ] ; let_clause: @@ -172,11 +172,11 @@ GEXTEND Gram | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: - [ [ 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 -> + [ [ 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 + match mpv with | Term t -> (match t with | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty) | _ -> mpv, None) @@ -213,7 +213,7 @@ GEXTEND Gram [ [ ":=" -> false | "::=" -> true ] ] ; - + (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> @@ -224,7 +224,7 @@ GEXTEND Gram tactic: [ [ tac = tactic_expr -> tac ] ] ; - Vernac_.command: + Vernac_.command: [ [ IDENT "Ltac"; l = LIST1 tacdef_body SEP "with" -> VernacDeclareTacticDefinition (true, l) ] ] diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 168e532a81..8446bf50ca 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -34,7 +34,7 @@ let my_int_of_string loc s = Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") GEXTEND Gram - GLOBAL: + GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_string string pattern_ident pattern_identref by_notation smart_global; @@ -95,7 +95,7 @@ GEXTEND Gram [ [ qid = basequalid -> loc, qid ] ] ; ne_string: - [ [ s = STRING -> + [ [ s = STRING -> if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index d4232eb959..90245fa454 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -53,7 +53,7 @@ GEXTEND Gram | IDENT "Save"; id = identref -> VernacEndProof (Proved (true,Some (id,None))) | IDENT "Defined" -> VernacEndProof (Proved (false,None)) - | IDENT "Defined"; id=identref -> + | IDENT "Defined"; id=identref -> VernacEndProof (Proved (false,Some (id,None))) | IDENT "Suspend" -> VernacSuspend | IDENT "Resume" -> VernacResume None @@ -82,7 +82,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> VernacShow (ExplainProof l) - | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> + | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> VernacShow (ExplainTree l) | IDENT "Go"; n = natural -> VernacGo (GoTo n) | IDENT "Go"; IDENT "top" -> VernacGo GoTop @@ -90,22 +90,22 @@ GEXTEND Gram | IDENT "Go"; IDENT "next" -> VernacGo GoNext | IDENT "Guarded" -> VernacCheckGuard (* Hints for Auto and EAuto *) - | IDENT "Create"; IDENT "HintDb" ; + | IDENT "Create"; IDENT "HintDb" ; id = IDENT ; b = [ "discriminated" -> true | -> false ] -> VernacCreateHintDb (use_locality (), id, b) - | IDENT "Hint"; local = obsolete_locality; h = hint; + | IDENT "Hint"; local = obsolete_locality; h = hint; dbnames = opt_hintbases -> VernacHints (enforce_locality_of local,dbnames, h) -(* Declare "Resolve" directly so as to be able to later extend with +(* Declare "Resolve" directly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; + | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 constr; n = OPT natural; dbnames = opt_hintbases -> VernacHints (enforce_locality_of false,dbnames, HintsResolve (List.map (fun x -> (n, true, x)) lc)) (*This entry is not commented, only for debug*) - | IDENT "PrintConstr"; c = constr -> + | IDENT "PrintConstr"; c = constr -> VernacExtend ("PrintConstr", [Genarg.in_gen Genarg.rawwit_constr c]) ] ]; @@ -114,7 +114,7 @@ GEXTEND Gram [ [ IDENT "Local" -> true | -> false ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural -> + [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT natural -> HintsResolve (List.map (fun x -> (n, true, x)) lc) | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) @@ -124,7 +124,7 @@ GEXTEND Gram | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>"; tac = tactic -> HintsExtern (n,c,tac) - | IDENT "Destruct"; + | IDENT "Destruct"; id = ident; ":="; pri = natural; dloc = destruct_location; diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 846246ed06..c61bff02d7 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -149,7 +149,7 @@ let induction_arg_of_constr (c,lbind as clbind) = let rec mkCLambdaN_simple_loc loc bll c = match bll with - | ((loc1,_)::_ as idl,bk,t) :: bll -> + | ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (join_loc loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c | [] -> c @@ -170,7 +170,7 @@ let map_int_or_var f = function GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var open_constr casted_open_constr + bindings red_expr int_or_var open_constr casted_open_constr simple_intropattern; int_or_var: @@ -183,7 +183,7 @@ GEXTEND Gram ; (* An identifier or a quotation meta-variable *) id_or_meta: - [ [ id = identref -> AI id + [ [ id = identref -> AI id (* This is used in quotations *) | id = METAIDENT -> MetaId (loc,id) ] ] @@ -220,7 +220,7 @@ GEXTEND Gram | "-"; n = nat_or_var; nl = LIST0 int_or_var -> (* have used int_or_var instead of nat_or_var for compatibility *) all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ] - ; + ; occs: [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr_but [] ] ] ; @@ -237,13 +237,13 @@ GEXTEND Gram [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc | "()" -> loc,IntroOrAndPattern [[]] | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]] - | "("; si = simple_intropattern; ","; - tc = LIST1 simple_intropattern SEP "," ; ")" -> + | "("; si = simple_intropattern; ","; + tc = LIST1 simple_intropattern SEP "," ; ")" -> loc,IntroOrAndPattern [si::tc] - | "("; si = simple_intropattern; "&"; - tc = LIST1 simple_intropattern SEP "&" ; ")" -> + | "("; si = simple_intropattern; "&"; + tc = LIST1 simple_intropattern SEP "&" ; ")" -> (* (A & B & C) is translated into (A,(B,C)) *) - let rec pairify = function + let rec pairify = function | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]] in loc,pairify (si::tc) ] ] @@ -256,7 +256,7 @@ GEXTEND Gram | "**" -> loc, IntroForthcoming false ] ] ; intropattern_modifier: - [ [ IDENT "_eqn"; + [ [ IDENT "_eqn"; id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ] -> id ] ] ; @@ -375,14 +375,14 @@ GEXTEND Gram [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) | -> None ] ] ; - orient: - [ [ "->" -> true + orient: + [ [ "->" -> true | "<-" -> false | -> true ]] ; simple_binder: [ [ na=name -> ([na],Default Explicit,CHole (loc, None)) - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; fixdecl: @@ -398,7 +398,7 @@ GEXTEND Gram (loc,id,bl,None,ty) ] ] ; bindings_with_parameters: - [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; + [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ] ; hintbases: @@ -437,10 +437,10 @@ GEXTEND Gram [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> Some tac | -> None ] ] ; - rename : + rename : [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ] ; - rewriter : + rewriter : [ [ "!"; c = constr_with_bindings -> (RepeatPlus,c) | ["?"| LEFTQMARK]; c = constr_with_bindings -> (RepeatStar,c) | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c) @@ -449,11 +449,11 @@ GEXTEND Gram | c = constr_with_bindings -> (Precisely 1, c) ] ] ; - oriented_rewriter : + oriented_rewriter : [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] - ; + ; induction_clause: - [ [ lc = LIST1 induction_arg; ipats = with_induction_names; + [ [ lc = LIST1 induction_arg; ipats = with_induction_names; el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ] ; move_location: @@ -463,9 +463,9 @@ GEXTEND Gram | "at"; IDENT "top" -> MoveToEnd false ] ] ; simple_tactic: - [ [ + [ [ (* Basic tactics *) - IDENT "intros"; IDENT "until"; id = quantified_hypothesis -> + IDENT "intros"; IDENT "until"; id = quantified_hypothesis -> TacIntrosUntil id | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl | IDENT "intro"; id = ident; hto = move_location -> @@ -479,7 +479,7 @@ 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 ","; + | 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) @@ -516,11 +516,11 @@ GEXTEND Gram TacLetTac (na,c,p,false) (* Begin compatibility *) - | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; - c = lconstr; ")" -> + | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + c = lconstr; ")" -> TacAssert (None,Some (loc,IntroIdentifier id),c) - | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; - c = lconstr; ")"; tac=by_tactic -> + | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> TacAssert (Some tac,Some (loc,IntroIdentifier id),c) (* End compatibility *) @@ -535,8 +535,8 @@ GEXTEND Gram | IDENT "generalize"; c = constr; l = LIST1 constr -> let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in TacGeneralize (List.map gen_everywhere (c::l)) - | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; - na = as_name; + | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs; + na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacGeneralize (((nl,c),na)::l) | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c @@ -616,30 +616,30 @@ GEXTEND Gram | IDENT "etransitivity" -> TacTransitivity None (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (false,l,cl,t) - | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause_dft_concl; t=opt_by_tactic -> TacRewrite (true,l,cl,t) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion | IDENT "inversion_clear" -> FullInversionClear ]; - hyp = quantified_hypothesis; + hyp = quantified_hypothesis; ids = with_inversion_names; co = OPT ["with"; c = constr -> c] -> TacInversion (DepInversion (k,co,ids),hyp) | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; cl = in_hyp_list -> TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) - | IDENT "inversion"; + | IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) - | IDENT "inversion_clear"; - hyp = quantified_hypothesis; ids = with_inversion_names; + | IDENT "inversion_clear"; + hyp = quantified_hypothesis; ids = with_inversion_names; cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) - | IDENT "inversion"; hyp = quantified_hypothesis; + | IDENT "inversion"; hyp = quantified_hypothesis; "using"; c = constr; cl = in_hyp_list -> TacInversion (InversionUsing (c,cl), hyp) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0ebbaba924..4cd798e3e1 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -58,28 +58,28 @@ let get_command_entry () = | Mode_none -> noedit_mode let default_command_entry = - Gram.Entry.of_parser "command_entry" + Gram.Entry.of_parser "command_entry" (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm) let no_hook _ _ = () GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode; vernac: FIRST - [ [ IDENT "Time"; v = vernac -> VernacTime v + [ [ IDENT "Time"; v = vernac -> VernacTime v | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | locality; v = vernac_aux -> 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 + [ [ g = gallina; "." -> g | g = gallina_ext; "." -> g - | c = command; "." -> c + | c = command; "." -> c | c = syntax; "." -> c | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l ] ] ; - vernac_aux: LAST + vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; locality: @@ -103,11 +103,11 @@ GEXTEND Gram VernacSolve(g,tac,use_dft_tac)) ] ] ; proof_mode: - [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] + [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] ; proof_mode: LAST [ [ c=subgoal_command -> c (Some 1) ] ] - ; + ; located_vernac: [ [ v = vernac -> loc, v ] ] ; @@ -127,20 +127,20 @@ GEXTEND Gram gallina: (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr; - l = LIST0 + l = LIST0 [ "with"; id = identref; bl = binders_let; ":"; c = lconstr -> (Some id,(bl,c)) ] -> VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook) - | stre = assumption_token; nl = inline; bl = assum_list -> + | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) | stre = assumptions_token; nl = inline; bl = assum_list -> test_plurial_form bl; VernacAssumption (stre, nl, bl) - | IDENT "Boxed";"Definition";id = identref; b = def_body -> + | IDENT "Boxed";"Definition";id = identref; b = def_body -> VernacDefinition ((Global,true,Definition), id, b, no_hook) - | IDENT "Unboxed";"Definition";id = identref; b = def_body -> + | IDENT "Unboxed";"Definition";id = identref; b = def_body -> VernacDefinition ((Global,false,Definition), id, b, no_hook) - | (f,d) = def_token; id = identref; b = def_body -> + | (f,d) = def_token; id = identref; b = def_body -> VernacDefinition (d, id, b, f) (* Gallina inductive declarations *) | f = finite_token; @@ -157,12 +157,12 @@ GEXTEND Gram | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,false) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l - | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; + | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ] ; gallina_ext: [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref; - ps = binders_let; + ps = binders_let; s = OPT [ ":"; s = lconstr -> s ]; cfs = [ ":="; l = constructor_list_or_record_decl -> l | -> RecordDecl (None, []) ] -> @@ -171,7 +171,7 @@ GEXTEND Gram ] ] ; typeclass_context: - [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l + [ [ "["; l=LIST1 typeclass_constraint SEP ","; "]" -> l | -> [] ] ] ; thm_token: @@ -184,14 +184,14 @@ GEXTEND Gram | IDENT "Property" -> Property ] ] ; def_token: - [ [ "Definition" -> + [ [ "Definition" -> no_hook, (Global, Flags.boxed_definitions(), Definition) - | IDENT "Let" -> + | IDENT "Let" -> no_hook, (Local, Flags.boxed_definitions(), Definition) - | IDENT "Example" -> + | IDENT "Example" -> no_hook, (Global, Flags.boxed_definitions(), Example) | IDENT "SubClass" -> - Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] + Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) @@ -218,7 +218,7 @@ GEXTEND Gram ; record_token: [ [ IDENT "Record" -> (Record,BiFinite) - | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; (* Simple definitions *) @@ -237,24 +237,24 @@ GEXTEND Gram | -> None ] ] ; decl_notation: - [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr; + [ [ OPT [ "where"; ntn = ne_string; ":="; c = constr; scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] ] ; (* Inductives and records *) inductive_definition: - [ [ id = identref; oc = opt_coercion; indpar = binders_let; + [ [ 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 "|" -> + | 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) + | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + RecordDecl (Some cstr,fs) + | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) | -> Constructors [] ] ] ; (* @@ -268,9 +268,9 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = identref; + [ [ id = identref; bl = binders_let_fixannot; - ty = type_cstr; + ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> let bl, annot = bl in let names = names_of_local_assums bl in @@ -282,13 +282,13 @@ GEXTEND Gram else Util.user_err_loc (loc,"Fixpoint", str "No argument named " ++ Nameops.pr_id id ++ str".")) - | None -> - (* If there is only one argument, it is the recursive one, + | None -> + (* If there is only one argument, it is the recursive one, otherwise, we search the recursive index later *) match names with | [(loc, Name na)] -> Some (loc, na) - | _ -> None - in + | _ -> None + in ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; corec_definition: @@ -297,7 +297,7 @@ GEXTEND Gram ((id,bl,ty,def),ntn) ] ] ; type_cstr: - [ [ ":"; c=lconstr -> c + [ [ ":"; c=lconstr -> c | -> CHole (loc, None) ] ] ; (* Inductive schemes *) @@ -329,7 +329,7 @@ GEXTEND Gram [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ] ; record_binder_body: - [ [ l = binders_let; oc = of_type_with_opt_coercion; + [ [ l = binders_let; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t)) | l = binders_let; oc = of_type_with_opt_coercion; t = lconstr; ":="; b = lconstr -> fun id -> @@ -352,12 +352,12 @@ GEXTEND Gram [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: - [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> + [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> (oc,(idl,c)) ] ] ; constructor_type: - [[ l = binders_let; + [[ l = binders_let; t= [ coe = of_type_with_opt_coercion; c = lconstr -> fun l id -> (coe,(id,mkCProdN loc l c)) | -> @@ -383,16 +383,16 @@ GEXTEND Gram gallina_ext: [ [ (* Interactive module declaration *) - IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; mty_o = OPT of_module_type; + IDENT "Module"; export = export_token; id = identref; + bl = LIST0 module_binder; mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr -> VernacDefineModule (export, id, bl, mty_o, mexpr_o) - - | IDENT "Module"; "Type"; id = identref; + + | IDENT "Module"; "Type"; id = identref; bl = LIST0 module_binder; mty_o = OPT is_module_type -> VernacDeclareModuleType (id, bl, mty_o) - - | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; + + | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; ":"; mty = module_type -> VernacDeclareModule (export, id, bl, (mty,true)) (* Section beginning *) @@ -405,10 +405,10 @@ GEXTEND Gram (* Requiring an already compiled module *) | IDENT "Require"; export = export_token; qidl = LIST1 global -> VernacRequire (export, None, qidl) - | IDENT "Require"; export = export_token; filename = ne_string -> + | IDENT "Require"; export = export_token; filename = ne_string -> VernacRequireFrom (export, None, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) - | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) + | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr)) | IDENT "Include"; "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ] ; @@ -418,7 +418,7 @@ GEXTEND Gram | -> None ] ] ; of_module_type: - [ [ ":"; mty = module_type -> (mty, true) + [ [ ":"; mty = module_type -> (mty, true) | "<:"; mty = module_type -> (mty, false) ] ] ; is_module_type: @@ -453,13 +453,13 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMTEident qid (* ... *) - | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) + | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) ] ] ; END -(* Extensions: implicits, coercions, etc. *) +(* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext; @@ -480,7 +480,7 @@ GEXTEND Gram | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition + VernacDefinition ((Global,false,CanonicalStructure),(dummy_loc,s),d, (fun _ -> Recordops.declare_canonical_structure)) @@ -492,16 +492,16 @@ GEXTEND Gram let s = coerce_reference_to_id qid in 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 -> + ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (enforce_locality_exp (), f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> + s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (use_locality_exp (), f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> + s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (enforce_locality_exp (), AN qid, s, t) | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> + s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (enforce_locality_exp (), ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> @@ -509,29 +509,29 @@ GEXTEND Gram | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) - - | IDENT "Context"; c = binders_let -> + + | IDENT "Context"; c = binders_let -> VernacContext c - + | IDENT "Instance"; ":"; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> r | + pri = OPT [ "|"; i = natural -> i ] ; + props = [ ":="; "{"; r = record_declaration; "}" -> r | ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri) | IDENT "Instance"; name = identref; sup = OPT binders_let; ":"; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; - props = [ ":="; "{"; r = record_declaration; "}" -> r | + pri = OPT [ "|"; i = natural -> i ] ; + props = [ ":="; "{"; r = record_declaration; "}" -> r | ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] -> let sup = match sup with None -> [] | Some l -> l in - let n = - let (loc, id) = name in + let n = + let (loc, id) = name in (loc, Name id) in VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri) @@ -539,8 +539,8 @@ GEXTEND Gram | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = OPT [ "["; l = LIST0 implicit_name; "]" -> + | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; + pos = OPT [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> VernacDeclareImplicits (use_section_locality (),qid,pos) @@ -550,7 +550,7 @@ GEXTEND Gram implicit_name: [ [ "!"; id = ident -> (id, false, true) | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) + | "["; "!"; id = ident; "]" -> (id,true,true) | "["; id = ident; "]" -> (id,true, false) ] ] ; strategy_level: @@ -592,7 +592,7 @@ GEXTEND Gram (* Managing load paths *) | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> VernacAddLoadPath (false, dir, alias) - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; + | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> VernacRemoveLoadPath dir @@ -611,23 +611,23 @@ GEXTEND Gram (* Printing (careful factorization of entries) *) | IDENT "Print"; p = printable -> VernacPrint p | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid) - | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> + | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> VernacPrint (PrintModuleType qid) - | IDENT "Print"; IDENT "Module"; qid = global -> + | IDENT "Print"; IDENT "Module"; qid = global -> VernacPrint (PrintModule qid) | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid) (* Searching the environment *) - | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "Search"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchHead c, l) | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchPattern c, l) | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> VernacSearch (SearchRewrite c, l) - | IDENT "SearchAbout"; + | IDENT "SearchAbout"; sl = [ "["; - l = LIST1 [ + l = LIST1 [ b = positive_search_mark; s = ne_string; sc = OPT scope -> b, SearchString (s,sc) | b = positive_search_mark; p = constr_pattern @@ -635,7 +635,7 @@ GEXTEND Gram ]; "]" -> l | p = constr_pattern -> [true,SearchSubPattern p] | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ]; - l = in_or_out_modules -> + l = in_or_out_modules -> VernacSearch (SearchAbout sl, l) | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> @@ -671,7 +671,7 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption ([table;field], v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption ([table], v) + VernacRemoveOption ([table], v) | IDENT "proof" -> VernacDeclProof | "return" -> VernacReturn ]] @@ -690,7 +690,7 @@ GEXTEND Gram (* This should be in "syntax" section but is here for factorization*) PrintGrammar ent | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir - | IDENT "Modules" -> + | IDENT "Modules" -> error "Print Modules is obsolete; use Print Libraries instead" | IDENT "Libraries" -> PrintModules @@ -764,7 +764,7 @@ END; GEXTEND Gram command: - [ [ + [ [ (* State management *) IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s @@ -778,11 +778,11 @@ GEXTEND Gram | IDENT "Back" -> VernacBack 1 | IDENT "Back"; n = natural -> VernacBack n | IDENT "BackTo"; n = natural -> VernacBackTo n - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> + | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> VernacBacktrack (n,m,p) (* Tactic Debugger *) - | IDENT "Debug"; IDENT "On" -> + | IDENT "Debug"; IDENT "On" -> VernacSetOption (None,["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> @@ -798,38 +798,38 @@ GEXTEND Gram GLOBAL: syntax; syntax: - [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> + [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> VernacOpenCloseScope (enforce_locality_of local,true,sc) - | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> + | 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) - | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; + | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 opt_scope; "]" -> + "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (use_non_locality (),qid,scl) | IDENT "Infix"; local = obsolete_locality; - op = ne_string; ":="; p = constr; + op = ne_string; ":="; p = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacInfix (enforce_locality_of local,(op,modl),p,sc) - | IDENT "Notation"; local = obsolete_locality; id = identref; + | IDENT "Notation"; local = obsolete_locality; id = identref; idl = LIST0 ident; ":="; c = constr; b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] -> VernacSyntacticDefinition (id,(idl,c),enforce_locality_of local,b) - | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":="; + | IDENT "Notation"; local = obsolete_locality; s = ne_string; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (enforce_locality_of local,c,(s,modl),sc) - | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; + | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; pil = LIST1 production_item; ":="; t = Tactic.tactic -> VernacTacticNotation (n,pil,t) @@ -838,12 +838,12 @@ GEXTEND Gram Metasyntax.check_infix_modifiers l; VernacSyntaxExtension (use_locality (),("x '"^s^"' y",l)) - | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; - s = ne_string; + | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; + s = ne_string; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> VernacSyntaxExtension (enforce_locality_of local,(s,l)) - (* "Print" "Grammar" should be here but is in "command" entry in order + (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; @@ -859,7 +859,7 @@ GEXTEND Gram ; syntax_modifier: [ [ x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; + | x = IDENT; ","; l = LIST1 IDENT SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA @@ -871,7 +871,7 @@ GEXTEND Gram ; syntax_extension_type: [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference - | IDENT "bigint" -> ETBigint + | IDENT "bigint" -> ETBigint ] ] ; opt_scope: @@ -879,8 +879,8 @@ GEXTEND Gram ; production_item: [ [ s = ne_string -> TacTerm s - | nt = IDENT; - po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; + | nt = IDENT; + po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ]; ")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ] ; END diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 8142368358..0f70290419 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -30,7 +30,7 @@ type xml = XmlTag of loc * string * attribute list * xml list let check_tags loc otag ctag = if otag <> ctag then - user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ + user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ str "does not match open xml tag " ++ str otag ++ str ".") let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) @@ -72,7 +72,7 @@ let nmtoken (loc,a) = try int_of_string a with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") -let get_xml_attr s al = +let get_xml_attr s al = try List.assoc s al with Not_found -> error ("No attribute "^s) @@ -143,7 +143,7 @@ let compute_inductive_nargs ind = let rec interp_xml_constr = function | XmlTag (loc,"REL",al,[]) -> RVar (loc, get_xml_ident al) - | XmlTag (loc,"VAR",al,[]) -> + | XmlTag (loc,"VAR",al,[]) -> error "XML parser: unable to interp free variables" | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) -> let body,decls = list_sep_last xl in @@ -200,7 +200,7 @@ let rec interp_xml_constr = function and interp_xml_tag s = function | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl) - | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", + | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".") and interp_xml_constr_alias s x = @@ -231,14 +231,14 @@ and interp_xml_recursionOrder x = let (loc, al, l) = interp_xml_tag "RecursionOrder" x in let (locs, s) = get_xml_attr "type" al in match s with - "Structural" -> + "Structural" -> (match l with [] -> RStructRec | _ -> error_expect_no_argument loc) - | "WellFounded" -> + | "WellFounded" -> (match l with [c] -> RWfRec (interp_xml_type c) | _ -> error_expect_one_argument loc) - | "Measure" -> + | "Measure" -> (match l with [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r)) | _ -> error_expect_two_arguments loc) @@ -261,7 +261,7 @@ and interp_xml_CoFixFunction x = match interp_xml_tag "CoFixFunction" x with | (loc,al,[x1;x2]) -> (get_xml_name al, interp_xml_type x1, interp_xml_body x2) - | (loc,_,_) -> + | (loc,_,_) -> error_expect_one_argument loc (* Interpreting tactic argument *) diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 4356db844e..0c815d2623 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -1,7 +1,7 @@ Coq_config Profile -Pp_control +Pp_control Pp Compat Flags @@ -49,7 +49,7 @@ Nametab Libobject Lib Goptions -Decl_kinds +Decl_kinds Global Termops Evd @@ -68,7 +68,7 @@ Vernacexpr Extrawit Pcoq Q_util -Q_coqast +Q_coqast Egrammar Argextend diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 4b40102eed..4edfbc748d 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pr_o.cmo pa_macro.cmo" i*) +(*i camlp4use: "pr_o.cmo pa_macro.cmo" i*) (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with * ast-based camlp4 *) @@ -21,7 +21,7 @@ open Token module CharMap = Map.Make (struct type t = char let compare = compare end) -type ttree = { +type ttree = { node : string option; branch : ttree CharMap.t } @@ -29,7 +29,7 @@ let empty_ttree = { node = None; branch = CharMap.empty } let ttree_add ttree str = let rec insert tt i = - if i == String.length str then + if i == String.length str then {node = Some str; branch = tt.branch} else let c = str.[i] in @@ -42,7 +42,7 @@ let ttree_add ttree str = CharMap.add c (insert tt' (i + 1)) tt.branch in { node = tt.node; branch = br } - in + in insert ttree 0 (* Search a string in a dictionary: raises [Not_found] @@ -52,14 +52,14 @@ let ttree_find ttree str = let rec proc_rec tt i = if i == String.length str then tt else proc_rec (CharMap.find str.[i] tt.branch) (i+1) - in + in proc_rec ttree 0 (* Removes a string from a dictionary: returns an equal dictionary if the word not present. *) let ttree_remove ttree str = let rec remove tt i = - if i == String.length str then + if i == String.length str then {node = None; branch = tt.branch} else let c = str.[i] in @@ -70,7 +70,7 @@ let ttree_remove ttree str = | None -> tt.branch in { node = tt.node; branch = br } - in + in remove ttree 0 @@ -114,7 +114,7 @@ let check_utf8_trailing_byte cs c = (* but don't certify full utf8 compliance (e.g. no emptyness check) *) let lookup_utf8_tail c cs = let c1 = Char.code c in - if c1 land 0x40 = 0 or c1 land 0x38 = 0x38 then error_utf8 cs + if c1 land 0x40 = 0 or c1 land 0x38 = 0x38 then error_utf8 cs else let n, unicode = if c1 land 0x20 = 0 then @@ -127,20 +127,20 @@ let lookup_utf8_tail c cs = match Stream.npeek 3 cs with | [_;c2;c3] -> check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + + 3, (c1 land 0x0F) lsl 12 + (Char.code c2 land 0x3F) lsl 6 + (Char.code c3 land 0x3F) | _ -> error_utf8 cs else match Stream.npeek 4 cs with | [_;c2;c3;c4] -> check_utf8_trailing_byte cs c2; check_utf8_trailing_byte cs c3; - check_utf8_trailing_byte cs c4; + check_utf8_trailing_byte cs c4; 4, (c1 land 0x07) lsl 18 + (Char.code c2 land 0x3F) lsl 12 + (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) | _ -> error_utf8 cs in try classify_unicode unicode, n with UnsupportedUtf8 -> error_unsupported_unicode_character n cs - + let lookup_utf8 cs = match Stream.peek cs with | Some ('\x00'..'\x7F') -> AsciiChar @@ -177,15 +177,15 @@ let check_keyword str = (* Keyword and symbol dictionary *) let token_tree = ref empty_ttree -let is_keyword s = - try match (ttree_find !token_tree s).node with None -> false | Some _ -> true +let is_keyword s = + try match (ttree_find !token_tree s).node with None -> false | Some _ -> true with Not_found -> false let add_keyword str = check_keyword str; token_tree := ttree_add !token_tree str -let remove_keyword str = +let remove_keyword str = token_tree := ttree_remove !token_tree str (* Adding a new token (keyword or special token). *) @@ -248,13 +248,13 @@ let rec string in_comments bp len = parser if esc then string in_comments bp (store len '"') s else len | [< ''*'; s >] -> (parser - | [< '')'; s >] -> + | [< '')'; s >] -> if in_comments then warning "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment."; - string in_comments bp (store (store len '*') ')') s + string in_comments bp (store (store len '*') ')') s | [< >] -> string in_comments bp (store len '*') s) s - | [< 'c; s >] -> string in_comments bp (store len c) s + | [< 'c; s >] -> string in_comments bp (store len c) s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string (* Hook for exporting comment into xml theory files *) @@ -270,8 +270,8 @@ let between_com = ref true type com_state = int option * string * bool let restore_com_state (o,s,b) = - comment_begin := o; - Buffer.clear current; Buffer.add_string current s; + comment_begin := o; + Buffer.clear current; Buffer.add_string current s; between_com := b let dflt_com = (None,"",true) let com_state () = @@ -326,13 +326,13 @@ let rec comm_string bp = parser | [< >] -> real_push_char '\\'); s >] -> comm_string bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string - | [< 'c; s >] -> real_push_char c; comm_string bp s + | [< 'c; s >] -> real_push_char c; comm_string bp s let rec comment bp = parser bp2 | [< ''('; _ = (parser | [< ''*'; s >] -> push_string "(*"; comment bp s - | [< >] -> push_string "(" ); + | [< >] -> push_string "(" ); s >] -> comment bp s | [< ''*'; _ = parser @@ -356,7 +356,7 @@ let rec progress_further last nj tt cs = and update_longest_valid_token last nj tt cs = match tt.node with | Some _ as last' -> - for i=1 to nj do Stream.junk cs done; + for i=1 to nj do Stream.junk cs done; progress_further last' 0 tt cs | None -> progress_further last nj tt cs @@ -374,7 +374,7 @@ and progress_utf8 last nj n c tt cs = List.iter (check_utf8_trailing_byte cs) l; let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in update_longest_valid_token last (nj+n) tt cs - | _ -> + | _ -> error_utf8 cs with Not_found -> last @@ -404,7 +404,7 @@ let process_chars bp c cs = let parse_after_dollar bp = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> ("METAIDENT", get_buff len) | [< s >] -> match lookup_utf8 s with @@ -419,9 +419,9 @@ let parse_after_dot bp c = ("FIELD", get_buff len) | [< s >] -> match lookup_utf8 s with - | Utf8Token (UnicodeLetter, n) -> + | Utf8Token (UnicodeLetter, n) -> ("FIELD", get_buff (ident_tail (nstore n 0 s) s)) - | AsciiChar | Utf8Token _ | EmptyStream -> + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp c s) (* Parse what follows a question mark *) @@ -449,7 +449,7 @@ let rec next_token = parser bp 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); s >] ep -> - let id = get_buff len in + let id = get_buff len in comment_stop bp; (try ("", find_keyword id s) with Not_found -> ("IDENT", id)), (bp, ep) | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> @@ -475,7 +475,7 @@ let rec next_token = parser bp let ep = Stream.count s in comment_stop bp; (try ("",find_keyword id s) with Not_found -> ("IDENT",id)), (bp, ep) - | AsciiChar | Utf8Token ((UnicodeSymbol | UnicodeIdentPart), _) -> + | AsciiChar | Utf8Token ((UnicodeSymbol | UnicodeIdentPart), _) -> let t = process_chars bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> @@ -540,7 +540,7 @@ let token_text = function | ("STRING", "") -> "string" | ("EOI", "") -> "end of input" | (con, "") -> con - | (con, prm) -> con ^ " \"" ^ prm ^ "\"" + | (con, prm) -> con ^ " \"" ^ prm ^ "\"" (* The lexer of Coq *) @@ -552,7 +552,7 @@ let token_text = function we unfreeze the state of the lexer. This restores the behaviour of the lexer. B.B. *) -IFDEF CAMLP5 THEN +IFDEF CAMLP5 THEN let lexer = { Token.tok_func = func; @@ -562,7 +562,7 @@ let lexer = { Token.tok_comm = None; Token.tok_text = token_text } -ELSE +ELSE let lexer = { Token.func = func; @@ -582,7 +582,7 @@ let is_ident_not_keyword s = let is_number s = let rec aux i = - String.length s = i or + String.length s = i or match s.[i] with '0'..'9' -> aux (i+1) | _ -> false in aux 0 diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6b5d03d912..1b53772f42 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -24,7 +24,7 @@ open Ppextend (* The parser of Coq *) -IFDEF CAMLP5 THEN +IFDEF CAMLP5 THEN module L = struct @@ -34,7 +34,7 @@ module L = module G = Grammar.GMake(L) -ELSE +ELSE module L = struct @@ -55,7 +55,7 @@ let grammar_delete e pos reinit rls = 99 and 200. We didn't find a good solution to this problem (e.g. using G.extend to know if the level exists results in a printed error message as side effect). As a consequence an - extension at 99 or 8 (and for pattern 200 too) inside a section + extension at 99 or 8 (and for pattern 200 too) inside a section corrupts the parser. *) List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) @@ -63,7 +63,7 @@ let grammar_delete e pos reinit rls = if reinit <> None then let lev = match pos with Some (Gramext.Level n) -> n | _ -> assert false in let pos = - if lev = "200" then Gramext.First + if lev = "200" then Gramext.First else Gramext.After (string_of_int (int_of_string lev + 1)) in G.extend e (Some pos) [Some lev,reinit,[]]; @@ -116,7 +116,7 @@ type camlp4_entry_rules = type ext_kind = | ByGrammar of - grammar_object G.Entry.e * Gramext.position option * + grammar_object G.Entry.e * Gramext.position option * camlp4_entry_rules list * Gramext.g_assoc option | ByGEXTEND of (unit -> unit) * (unit -> unit) @@ -215,16 +215,16 @@ let uconstr = create_univ "constr" let utactic = create_univ "tactic" let uvernac = create_univ "vernac" -let get_univ s = +let get_univ s = try Hashtbl.find univ_tab s with Not_found -> anomaly ("Unknown grammar universe: "^s) -let get_entry (u, utab) s = Hashtbl.find utab s +let get_entry (u, utab) s = Hashtbl.find utab s let get_entry_type (u, utab) s = - try + try type_of_typed_entry (get_entry (u, utab) s) with Not_found -> errorlabstrm "Pcoq.get_entry" @@ -263,7 +263,7 @@ let make_gen_entry (u,univ) rawwit s = module Prim = struct let gec_gen x = make_gen_entry uprim x - + (* Entries that can be refered via the string -> Gram.Entry.e table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen rawwit_pre_ident "preident" @@ -334,7 +334,7 @@ module Tactic = (* Entries that can be refered via the string -> Gram.Entry.e table *) (* Typically for tactic user extensions *) - let open_constr = + let open_constr = make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr" let casted_open_constr = make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr" @@ -347,7 +347,7 @@ module Tactic = make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis" let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var" let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr" - let simple_intropattern = + let simple_intropattern = make_gen_entry utactic rawwit_intro_pattern "simple_intropattern" (* Main entries for ltac *) @@ -395,7 +395,7 @@ let main_entry = Vernac_.main_entry left border and into "constr LEVEL n" elsewhere), to the level below (to be translated into "NEXT") or to an below wrt associativity (to be translated in camlp4 into "constr" without level) or to another level - (to be translated into "constr LEVEL n") + (to be translated into "constr LEVEL n") The boolean is true if the entry was existing _and_ empty; this to circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the @@ -422,7 +422,7 @@ let default_pattern_levels = 1,Gramext.LeftA,false; 0,Gramext.RightA,false] -let level_stack = +let level_stack = ref [(default_levels, default_pattern_levels)] (* At a same level, LeftA takes precedence over RightA and NoneA *) @@ -442,7 +442,7 @@ let create_assoc = function let error_level_assoc p current expected = let pr_assoc = function | Gramext.LeftA -> str "left" - | Gramext.RightA -> str "right" + | Gramext.RightA -> str "right" | Gramext.NonA -> str "non" in errorlabstrm "" (str "Level " ++ int p ++ str " is already declared " ++ @@ -508,7 +508,7 @@ let register_empty_levels forpat levels = let find_position forpat assoc level = find_position_gen forpat false assoc level -(* Synchronise the stack of level updates *) +(* Synchronise the stack of level updates *) let synchronize_level_positions () = let _ = find_position true None None in () @@ -517,7 +517,7 @@ let synchronize_level_positions () = (* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) let camlp4_assoc = function - | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA + | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA | None | Some Gramext.LeftA -> Gramext.LeftA (* [adjust_level assoc from prod] where [assoc] and [from] are the name @@ -628,7 +628,7 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = match interp_constr_prod_entry_key assoc from forpat typ with | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) | (eobj,Some None,_) -> Gramext.Snext - | (eobj,Some (Some (lev,cur)),_) -> + | (eobj,Some (Some (lev,cur)),_) -> Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev) (**********************************************************************) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cfd05f4f7e..b625480863 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -55,7 +55,7 @@ module Gram : Grammar.S with type te = Compat.token [GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Left,LeftA)), Some "x"); GramConstrTerminal ("","+"); - GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)), + GramConstrNonTerminal (ETConstr (NextLevel,(BorderProd Right,LeftA)), Some "y")] : grammar_constr_prod_item list | @@ -75,7 +75,7 @@ module Gram : Grammar.S with type te = Compat.token | | Metasyntax.interp_prod_item V - [GramTerminal "f"; + [GramTerminal "f"; GramNonTerminal (ConstrArgType, Aentry ("constr","constr"), Some "x")] : grammar_prod_item list | @@ -110,7 +110,7 @@ type camlp4_entry_rules = (* Add one extension at some camlp4 position of some camlp4 entry *) val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> + grammar_object Gram.Entry.e -> Gramext.position option -> (* for reinitialization if ever needed: *) Gramext.g_assoc option -> camlp4_entry_rules list -> unit @@ -211,7 +211,7 @@ module Constr : val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end -module Module : +module Module : sig val module_expr : module_ast Gram.Entry.e val module_type : module_type_ast Gram.Entry.e @@ -257,16 +257,16 @@ val main_entry : (loc * vernac_expr) option Gram.Entry.e (* Binding constr entry keys to entries and symbols *) -val interp_constr_entry_key : bool (* true for cases_pattern *) -> +val interp_constr_entry_key : bool (* true for cases_pattern *) -> constr_entry_key -> grammar_object Gram.Entry.e * int option -val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> - constr_entry_key -> bool -> constr_prod_entry_key -> +val symbol_of_constr_prod_entry_key : Gramext.g_assoc option -> + constr_entry_key -> bool -> constr_prod_entry_key -> Compat.token Gramext.g_symbol (* Binding general entry keys to symbols *) -val symbol_of_prod_entry_key : +val symbol_of_prod_entry_key : Gram.te prod_entry_key -> Gram.te Gramext.g_symbol (**********************************************************************) @@ -278,10 +278,10 @@ val interp_entry_name : bool (* true to fail on unknown entry *) -> (**********************************************************************) (* Registering/resetting the level of a constr entry *) -val find_position : +val find_position : bool (* true if for creation in pattern entry; false if in constr entry *) -> Gramext.g_assoc option -> int option -> - Gramext.position option * Gramext.g_assoc option * string option * + Gramext.position option * Gramext.g_assoc option * string option * (* for reinitialization: *) Gramext.g_assoc option val synchronize_level_positions : unit -> unit @@ -290,4 +290,4 @@ val register_empty_levels : bool -> int list -> (Gramext.position option * Gramext.g_assoc option * string option * Gramext.g_assoc option) list -val remove_levels : int -> unit +val remove_levels : int -> unit diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 74a4d5e5dc..80e1eb144d 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id$ *) (*i*) open Util @@ -94,14 +94,14 @@ let pr_delimiters key strm = let pr_generalization bk ak c = let hd, tl = - match bk with + match bk with | Implicit -> "{", "}" | Explicit -> "(", ")" - in (* TODO: syntax Abstraction Kind *) + in (* TODO: syntax Abstraction Kind *) str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if Flags.do_beautify() && 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) @@ -114,7 +114,7 @@ let pr_optc pr = function let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" -let pr_universe = Univ.pr_uni +let pr_universe = Univ.pr_uni let pr_rawsort = function | RProp Term.Null -> str "Prop" @@ -130,7 +130,7 @@ let pr_expl_args pr (a,expl) = | None -> pr (lapp,L) a | Some (_,ExplByPos (n,_id)) -> anomaly("Explicitation by position not implemented") - | Some (_,ExplByName id) -> + | Some (_,ExplByName id) -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type pr = function @@ -164,7 +164,7 @@ let pr_evar pr n l = (match l with | Some l -> spc () ++ pr_in_comment - (fun l -> + (fun l -> str"[" ++ hov 0 (prlist_with_sep pr_coma (pr ltop) l) ++ str"]") (List.rev l) | None -> mt())) @@ -200,7 +200,7 @@ let pr_eqn pr (loc,pl,rhs) = spc() ++ hov 4 (pr_with_comments loc (str "| " ++ - hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) @@ -213,22 +213,22 @@ let begin_of_binders = function | b::_ -> begin_of_binder b | _ -> 0 -let surround_impl k p = +let surround_impl k p = match k with | Explicit -> str"(" ++ p ++ str")" | Implicit -> str"{" ++ p ++ str"}" -let surround_binder k p = +let surround_binder k p = match k with | Default b -> hov 1 (surround_impl b p) - | Generalized (b, b', t) -> + | 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) -> + | Generalized (b, b', t) -> surround_impl b' (surround_impl b p) let pr_binder many pr (nal,k,t) = @@ -281,7 +281,7 @@ let rec extract_lam_binders = function let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in LocalRawAssum (nal,bk,t) :: bl, c | c -> [], c - + let split_lambda = function | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c) | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) @@ -293,7 +293,7 @@ let rename na na' t c = | (_,Name id), (_,Name id') -> (na',t,replace_vars_constr_expr [id,id'] c) | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) - + let split_product na' = function | CArrow (loc,t,c) -> (na',t,c) | CProdN (loc,[[na],bk,t],c) -> rename na na' t c @@ -324,7 +324,7 @@ let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom = Constrextern.check_same_type ty1 ty2; ty2 in (LocalRawAssum ([na],bk1,ty), codom) - + let rec strip_domain bvar cofun c = match c with | CArrow(loc,a,b) -> @@ -401,13 +401,13 @@ 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 + if List.length bl > 1 && n <> None then spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}" - else mt() + 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)) ++ + 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 pr_recursive_decl pr prd dangling_with_for id bl annot t c @@ -428,11 +428,11 @@ let is_var id = function | _ -> false let tm_clash = function - | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) + | (CRef (Ident (_,id)), Some (CApp (_,_,nal))) when List.exists (function CRef (Ident (_,id')),_ -> id=id' | _ -> false) nal -> Some id - | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) + | (CRef (Ident (_,id)), Some (CAppExpl (_,_,nal))) when List.exists (function CRef (Ident (_,id')) -> id=id' | _ -> false) nal -> Some id @@ -445,7 +445,7 @@ let pr_asin pr (na,indnalopt) = (match indnalopt with | None -> mt () | Some t -> spc () ++ str "in " ++ pr lsimple t) - + let pr_case_item pr (tm,asin) = hov 0 (pr (lcast,E) tm ++ pr_asin pr asin) @@ -474,7 +474,7 @@ let pr_appexpl pr f l = let pr_app pr a l = hov 2 ( - pr (lapp,L) a ++ + pr (lapp,L) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) let pr_forall () = @@ -554,28 +554,28 @@ let pr pr sep inherited a = let c,l1 = list_sep_last l1 in assert (snd c = None); let p = pr_proj (pr mt) pr_app (fst c) f l1 in - if l2<>[] then + if l2<>[] then p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp else p, lproj | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp | CRecord (_,w,l) -> - let beg = + let beg = match w with - | None -> spc () + | None -> spc () | Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc () in - hv 0 (str"{" ++ beg ++ + 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 '" ++ - hov 0 (pr_patt ltop p ++ + str "let '" ++ + hov 0 (pr_patt ltop p ++ pr_asin (pr_dangling_with_for mt pr) asin ++ - str " :=" ++ pr spc ltop c ++ + str " :=" ++ pr spc ltop c ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ str " in" ++ pr spc ltop b)), lletpattern @@ -608,7 +608,7 @@ let pr pr sep inherited a = hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++ hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)), lif - + | CHole _ -> str "_", latom | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom @@ -645,7 +645,7 @@ let rec strip_context n iscast t = else let bl', c = strip_context (n-n') iscast (if bll=[] then c else CLambdaN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c + LocalRawAssum (nal,bk,t) :: bl', c | CProdN (loc,(nal,bk,t)::bll,c) -> let n' = List.length nal in if n' > n then @@ -654,12 +654,12 @@ let rec strip_context n iscast t = else let bl', c = strip_context (n-n') iscast (if bll=[] then c else CProdN (loc,bll,c)) in - LocalRawAssum (nal,bk,t) :: bl', c + LocalRawAssum (nal,bk,t) :: bl', c | CArrow (loc,t,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawAssum ([loc,Anonymous],default_binder_kind,t) :: bl', c | CCast (_,c,_) -> strip_context n false c - | CLetIn (_,na,b,c) -> + | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c | _ -> anomaly "strip_context" @@ -704,7 +704,7 @@ let pr_with_occurrences_with_trailer pr occs trailer = (if nowhere_except_in then mt() else str "- ") ++ hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer) -let pr_with_occurrences pr occs = +let pr_with_occurrences pr occs = pr_with_occurrences_with_trailer pr occs (mt()) let pr_red_flag pr r = @@ -725,13 +725,13 @@ let pr_metaid id = str"?" ++ pr_id id let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | Red false -> str "red" | Hnf -> str "hnf" - | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o + | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o | Cbv f -> if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then str "compute" else hov 1 (str "cbv" ++ pr_red_flag pr_ref f) - | Lazy f -> + | Lazy f -> hov 1 (str "lazy" ++ pr_red_flag pr_ref f) | Unfold l -> hov 1 (str "unfold" ++ spc() ++ @@ -740,7 +740,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function | Pattern l -> hov 1 (str "pattern" ++ pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l) - + | Red true -> error "Shouldn't be accessible from user." | ExtraRedExpr s -> str s | CbvVm -> str "vm_compute" diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index ad2afa97d2..5767c9955c 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - + (*i $Id$ i*) open Pp @@ -28,11 +28,11 @@ val extract_def_binders : constr_expr -> constr_expr -> local_binder list * constr_expr * constr_expr val split_fix : - int -> constr_expr -> constr_expr -> + int -> constr_expr -> constr_expr -> local_binder list * constr_expr * constr_expr val prec_less : int -> int * Ppextend.parenRelation -> bool - + val pr_tight_coma : unit -> std_ppcmds val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds @@ -60,7 +60,7 @@ val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> ('a,'b) red_expr_gen -> std_ppcmds val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval -> std_ppcmds val pr_rawsort : rawsort -> std_ppcmds @@ -82,9 +82,9 @@ type term_pr = { val set_term_pr : term_pr -> unit val default_term_pr : term_pr -(* The modular constr printer. +(* The modular constr printer. [modular_constr_pr pr s p t] prints the head of the term [t] and calls - [pr] on its subterms. + [pr] on its subterms. [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop] for "lconstr" printers (spiwack: we might need more specification here). We can make a new modular constr printer by overriding certain branches, @@ -92,13 +92,13 @@ val default_term_pr : term_pr instead we can proceed as follows: let my_modular_constr_pr pr s p = function | CSort (_,RProp Null) -> str "Omega" - | t -> modular_constr_pr pr s p t + | t -> modular_constr_pr pr s p t Which has the same type. We can turn a modular printer into a printer by taking its fixpoint. *) type precedence val lsimple : precedence val ltop : precedence -val modular_constr_pr : - ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> +val modular_constr_pr : + ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml index 31fd4561e6..40c712cdff 100644 --- a/parsing/ppdecl_proof.ml +++ b/parsing/ppdecl_proof.ml @@ -8,43 +8,43 @@ (* $Id$ *) -open Util +open Util open Pp open Decl_expr -open Names +open Names open Nameops let pr_constr = Printer.pr_constr_env let pr_tac = Pptactic.pr_glob_tactic -let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr +let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr let pr_label = function Anonymous -> mt () - | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () + | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () let pr_justification_items env = function Some [] -> mt () - | Some (_::_ as l) -> - spc () ++ str "by" ++ spc () ++ + | Some (_::_ as l) -> + spc () ++ str "by" ++ spc () ++ prlist_with_sep (fun () -> str ",") (pr_constr env) l | None -> spc () ++ str "by *" let pr_justification_method env = function None -> mt () - | Some tac -> + | Some tac -> spc () ++ str "using" ++ spc () ++ pr_tac env tac -let pr_statement pr_it env st = +let pr_statement pr_it env st = pr_label st.st_label ++ pr_it env st.st_it let pr_or_thesis pr_this env = function Thesis Plain -> str "thesis" - | Thesis (For id) -> - str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id + | Thesis (For id) -> + str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id | This c -> pr_this env c -let pr_cut pr_it env c = - hov 1 (pr_it env c.cut_stat) ++ +let pr_cut pr_it env c = + hov 1 (pr_it env c.cut_stat) ++ pr_justification_items env c.cut_by ++ pr_justification_method env c.cut_using @@ -54,28 +54,28 @@ let type_or_thesis = function let _I x = x -let rec print_hyps pconstr gtyp env sep _be _have hyps = +let rec print_hyps pconstr gtyp env sep _be _have hyps = let pr_sep = if sep then str "and" ++ spc () else mt () in - match hyps with - (Hvar _ ::_) as rest -> - spc () ++ pr_sep ++ str _have ++ + match hyps with + (Hvar _ ::_) as rest -> + spc () ++ pr_sep ++ str _have ++ print_vars pconstr gtyp env false _be _have rest - | Hprop st :: rest -> + | Hprop st :: rest -> begin let nenv = match st.st_label with Anonymous -> env | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in - spc() ++ pr_sep ++ pr_statement pconstr env st ++ + spc() ++ pr_sep ++ pr_statement pconstr env st ++ print_hyps pconstr gtyp nenv true _be _have rest end | [] -> mt () and print_vars pconstr gtyp env sep _be _have vars = match vars with - Hvar st :: rest -> + Hvar st :: rest -> begin - let nenv = + let nenv = match st.st_label with Anonymous -> anomaly "anonymous variable" | Name id -> Environ.push_named (id,None,st.st_it) env in @@ -85,14 +85,14 @@ and print_vars pconstr gtyp env sep _be _have vars = print_vars pconstr gtyp nenv true _be _have rest end | (Hprop _ :: _) as rest -> - let _st = if _be then - str "be such that" - else + let _st = if _be then + str "be such that" + else str "such that" in spc() ++ _st ++ print_hyps pconstr gtyp env false _be _have rest | [] -> mt () -let pr_suffices_clause env (hyps,c) = +let pr_suffices_clause env (hyps,c) = print_hyps pr_constr _I env false false "to have" hyps ++ spc () ++ str "to show" ++ spc () ++ pr_or_thesis pr_constr env c @@ -110,68 +110,68 @@ let pr_side = function let rec pr_bare_proof_instr _then _thus env = function | Pescape -> str "escape" - | Pthen i -> pr_bare_proof_instr true _thus env i - | Pthus i -> pr_bare_proof_instr _then true env i + | Pthen i -> pr_bare_proof_instr true _thus env i + | Pthus i -> pr_bare_proof_instr _then true env i | Phence i -> pr_bare_proof_instr true true env i - | Pcut c -> + | Pcut c -> begin match _then,_thus with - false,false -> str "have" ++ spc () ++ + false,false -> str "have" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c - | false,true -> str "thus" ++ spc () ++ + | false,true -> str "thus" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c | true,false -> str "then" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c - | true,true -> str "hence" ++ spc () ++ + | true,true -> str "hence" ++ spc () ++ pr_cut (pr_statement (pr_or_thesis pr_constr)) env c end | Psuffices c -> - str "suffices" ++ pr_cut pr_suffices_clause env c + str "suffices" ++ pr_cut pr_suffices_clause env c | Prew (sid,c) -> (if _thus then str "thus" else str " ") ++ spc () ++ pr_side sid ++ spc () ++ pr_cut (pr_statement pr_constr) env c - | Passume hyps -> + | Passume hyps -> str "assume" ++ print_hyps pr_constr _I env false false "we have" hyps - | Plet hyps -> + | Plet hyps -> str "let" ++ print_vars pr_constr _I env false true "let" hyps | Pclaim st -> str "claim" ++ spc () ++ pr_statement pr_constr env st | Pfocus st -> str "focus on" ++ spc () ++ pr_statement pr_constr env st | Pconsider (id,hyps) -> - str "consider" ++ print_vars pr_constr _I env false false "consider" hyps - ++ spc () ++ str "from " ++ pr_constr env id + str "consider" ++ print_vars pr_constr _I env false false "consider" hyps + ++ spc () ++ str "from " ++ pr_constr env id | Pgiven hyps -> str "given" ++ print_vars pr_constr _I env false false "given" hyps - | Ptake witl -> - str "take" ++ spc () ++ + | Ptake witl -> + str "take" ++ spc () ++ prlist_with_sep pr_coma (pr_constr env) witl | Pdefine (id,args,body) -> - str "define" ++ spc () ++ pr_id id ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") args ++ spc () ++ - str "as" ++ (pr_constr env body) - | Pcast (id,typ) -> - str "reconsider" ++ spc () ++ - pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ - str "as" ++ spc () ++ (pr_constr env typ) - | Psuppose hyps -> - str "suppose" ++ + str "define" ++ spc () ++ pr_id id ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr env body) + | Pcast (id,typ) -> + str "reconsider" ++ spc () ++ + pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ + str "as" ++ spc () ++ (pr_constr env typ) + | Psuppose hyps -> + str "suppose" ++ print_hyps pr_constr _I env false false "we have" hyps | Pcase (params,pat,hyps) -> str "suppose it is" ++ spc () ++ pr_pat pat ++ - (if params = [] then mt () else - (spc () ++ str "with" ++ spc () ++ - prlist_with_sep spc - (fun st -> str "(" ++ - pr_statement pr_constr env st ++ str ")") params ++ spc ())) + (if params = [] then mt () else + (spc () ++ str "with" ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") params ++ spc ())) ++ - (if hyps = [] then mt () else - (spc () ++ str "and" ++ + (if hyps = [] then mt () else + (spc () ++ str "and" ++ print_hyps (pr_or_thesis pr_constr) type_or_thesis env false false "we have" hyps)) - | Pper (et,c) -> + | Pper (et,c) -> str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et @@ -184,7 +184,7 @@ let pr_emph = function | 3 -> str "*** " | _ -> anomaly "unknown emphasis" -let pr_proof_instr env instr = - pr_emph instr.emph ++ spc () ++ +let pr_proof_instr env instr = + pr_emph instr.emph ++ spc () ++ pr_bare_proof_instr false false env instr.instr diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli index b0f0e110ce..fd6fb66376 100644 --- a/parsing/ppdecl_proof.mli +++ b/parsing/ppdecl_proof.mli @@ -1,2 +1,2 @@ -val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds +val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index bed5e1b286..f113908f89 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -36,8 +36,8 @@ let declare_extra_tactic_pprule (s,tags,prods) = let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags) type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -48,8 +48,8 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -57,7 +57,7 @@ let genarg_pprule = ref Stringmap.empty let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) = let s = match unquote wit with - | ExtraArgType s -> s + | ExtraArgType s -> s | _ -> error "Can declare a pretty-printing rule only for extra argument types." in @@ -84,13 +84,13 @@ let pr_or_by_notation f = function let pr_located pr (loc,x) = pr x -let pr_evaluable_reference = function +let pr_evaluable_reference = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n - | NamedHyp id -> pr_id id + | NamedHyp id -> pr_id id let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h @@ -103,7 +103,7 @@ let pr_bindings prc prlc = function brk (1,1) ++ str "with" ++ brk (1,1) ++ prlist_with_sep spc prc l | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ + brk (1,1) ++ str "with" ++ brk (1,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | NoBindings -> mt () @@ -112,7 +112,7 @@ let pr_bindings_no_with prc prlc = function brk (1,1) ++ prlist_with_sep spc prc l | ExplicitBindings l -> - brk (1,1) ++ + brk (1,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l | NoBindings -> mt () @@ -160,11 +160,11 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu pr_red_expr (prc,prlc,pr_or_by_notation prref) (out_gen rawwit_red_expr x) | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x)) - | ConstrWithBindingsArgType -> + | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x) - | BindingsArgType -> + | BindingsArgType -> pr_bindings_no_with prc prlc (out_gen rawwit_bindings x) - | List0ArgType _ -> + | List0ArgType _ -> hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref) (fold_list0 (fun a l -> a::l) x [])) | List1ArgType _ -> @@ -176,7 +176,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu (fold_pair (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prref) [a;b]) x) - | ExtraArgType s -> + | ExtraArgType s -> try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" @@ -201,15 +201,15 @@ let rec pr_glob_generic prc prlc prtac x = | QuantHypArgType -> pr_quantified_hypothesis (out_gen globwit_quant_hyp x) | RedExprArgType -> - pr_red_expr + pr_red_expr (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)) (out_gen globwit_red_expr x) | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x)) - | ConstrWithBindingsArgType -> + | ConstrWithBindingsArgType -> pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x) - | BindingsArgType -> + | BindingsArgType -> pr_bindings_no_with prc prlc (out_gen globwit_bindings x) - | List0ArgType _ -> + | List0ArgType _ -> hov 0 (pr_sequence (pr_glob_generic prc prlc prtac) (fold_list0 (fun a l -> a::l) x [])) | List1ArgType _ -> @@ -221,7 +221,7 @@ let rec pr_glob_generic prc prlc prtac x = (fold_pair (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac) [a;b]) x) - | ExtraArgType s -> + | ExtraArgType s -> try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" @@ -248,7 +248,7 @@ let rec pr_generic prc prlc prtac x = | ConstrWithBindingsArgType -> let (c,b) = out_gen wit_constr_with_bindings x in pr_with_bindings prc prlc (c,out_bindings b) - | BindingsArgType -> + | BindingsArgType -> pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x)) | List0ArgType _ -> hov 0 (pr_sequence (pr_generic prc prlc prtac) @@ -261,7 +261,7 @@ let rec pr_generic prc prlc prtac x = hov 0 (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac) [a;b]) x) - | ExtraArgType s -> + | ExtraArgType s -> try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" @@ -275,7 +275,7 @@ let pr_tacarg_using_rule pr_gen l= pr_sequence (fun x -> x) (tacarg_using_rule_token pr_gen l) let pr_extend_gen pr_gen lev s l = - try + try let tags = List.map genarg_tag l in let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in let p = pr_tacarg_using_rule pr_gen (pl,l) in @@ -283,7 +283,7 @@ let pr_extend_gen pr_gen lev s l = with Not_found -> str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" -let pr_raw_extend prc prlc prtac = +let pr_raw_extend prc prlc prtac = pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference) let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) @@ -320,14 +320,14 @@ let pr_arg pr x = spc () ++ pr x let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) -let pr_evaluable_reference_env env = function +let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id - | EvalConstRef sp -> + | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Libnames.ConstRef sp) let pr_quantified_hypothesis = function | AnonHyp n -> int n - | NamedHyp id -> pr_id id + | NamedHyp id -> pr_id id let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h @@ -362,7 +362,7 @@ let pr_with_constr prc = function let pr_with_induction_names = function | None, None -> mt () | eqpat, ipat -> - spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++ + spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++ pr_opt pr_intro_pattern ipat) let pr_as_intro_pattern ipat = @@ -410,10 +410,10 @@ let pr_by_tactic prt = function let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs | occs, InHypTypeOnly -> - spc () ++ + spc () ++ pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs | occs, InHypValueOnly -> - spc () ++ + spc () ++ pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) @@ -441,13 +441,13 @@ let pr_clause_pattern pr_id = function | (glopt,l) -> str " in" ++ prlist - (fun (id,nl) -> prlist (pr_arg int) nl + (fun (id,nl) -> prlist (pr_arg int) nl ++ spc () ++ pr_id id) l ++ pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt let pr_orient b = if b then mt () else str " <-" -let pr_multi = function +let pr_multi = function | Precisely 1 -> mt () | Precisely n -> pr_int n ++ str "!" | UpTo n -> pr_int n ++ str "?" @@ -486,14 +486,14 @@ let pr_match_rule m pr pr_pat = function (* | Pat (rl,mp,t) -> hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl ++ - (if rl <> [] then spc () else mt ()) ++ + (if rl <> [] then spc () else mt ()) ++ hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t)) *) | Pat (rl,mp,t) -> hov 0 ( hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl) ++ - (if rl <> [] then spc () else mt ()) ++ + (if rl <> [] then spc () else mt ()) ++ hov 0 ( str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t)) @@ -504,7 +504,7 @@ let pr_funvar = function | Some id -> spc () ++ pr_id id let pr_let_clause k pr (id,(bl,t)) = - hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++ + hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr (TacArg t)) let pr_let_clauses recflag pr = function @@ -538,7 +538,7 @@ let pr_hintbases = function let pr_auto_using prc = function | [] -> mt () - | l -> spc () ++ + | l -> spc () ++ hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_coma prc l) let pr_autoarg_adding = function @@ -581,7 +581,7 @@ open Closure used only at the glob and typed level: it is used to feed the constr printers *) -let make_pr_tac +let make_pr_tac (pr_tac_level,pr_constr,pr_lconstr,pr_pat, pr_cst,pr_ind,pr_ref,pr_ident, pr_extend,strip_prod_binders) env = @@ -644,7 +644,7 @@ let pr_fix_tac (id,n,c) = let annot = if List.length names = 1 then mt() else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in - hov 1 (str"(" ++ pr_id id ++ + hov 1 (str"(" ++ pr_id id ++ prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in (* spc() ++ @@ -681,7 +681,7 @@ and pr_atom1 = function (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t - | TacIntroPattern (_::_ as p) -> + | TacIntroPattern (_::_ as p) -> hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) | TacIntrosUntil h -> hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h) @@ -695,11 +695,11 @@ and pr_atom1 = function | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) | TacApply (a,ev,cb,inhyp) -> hov 1 ((if a then mt() else str "simple ") ++ - str (with_evars ev "apply") ++ spc () ++ + str (with_evars ev "apply") ++ spc () ++ 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 ++ + hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c) | TacCase (ev,cb) -> @@ -716,16 +716,16 @@ and pr_atom1 = function hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc pr_cofix_tac l) | TacCut c -> hov 1 (str "cut" ++ pr_constrarg c) - | TacAssert (Some tac,ipat,c) -> - hov 1 (str "assert" ++ - pr_assumption pr_lconstr pr_constr ipat c ++ + | TacAssert (Some tac,ipat,c) -> + hov 1 (str "assert" ++ + pr_assumption pr_lconstr pr_constr ipat c ++ pr_by_tactic (pr_tac_level ltop) tac) - | TacAssert (None,ipat,c) -> + | TacAssert (None,ipat,c) -> hov 1 (str "pose proof" ++ pr_assertion pr_lconstr pr_constr ipat c) | TacGeneralize l -> hov 1 (str "generalize" ++ spc () ++ - prlist_with_sep pr_coma (fun (cl,na) -> + prlist_with_sep pr_coma (fun (cl,na) -> pr_with_occurrences pr_constr cl ++ pr_as_name na) l) | TacGeneralizeDep c -> @@ -745,7 +745,7 @@ and pr_atom1 = function | TacInstantiate (n,c,HypLocation (id,hloc)) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg c ++ str ")" ) + pr_lconstrarg c ++ str ")" ) ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None))) *) (* Derived basic tactics *) @@ -762,7 +762,7 @@ and pr_atom1 = function pr_opt_no_spc (pr_clauses pr_ident) cl) l) | TacDoubleInduction (h1,h2) -> hov 1 - (str "double induction" ++ + (str "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ pr_arg pr_quantified_hypothesis h2) | TacDecomposeAnd c -> @@ -774,22 +774,22 @@ and pr_atom1 = function hov 0 (str "[" ++ prlist_with_sep spc pr_ind l ++ str "]" ++ pr_constrarg c)) | TacSpecialize (n,c) -> - hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ + hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ pr_with_bindings c) - | TacLApply c -> + | TacLApply c -> hov 1 (str "lapply" ++ pr_constrarg c) (* Automation tactics *) | TacTrivial ([],Some []) as x -> pr_atom0 x | TacTrivial (lems,db) -> - hov 0 (str "trivial" ++ + hov 0 (str "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 ++ + hov 0 (str "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" ++ + 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 *) @@ -803,18 +803,18 @@ and pr_atom1 = function (* Rem: only b = true is available for users *) assert b; hov 1 - (str "move" ++ brk (1,1) ++ pr_ident id1 ++ + (str "move" ++ brk (1,1) ++ pr_ident id1 ++ pr_move_location pr_ident id2) | TacRename l -> hov 1 (str "rename" ++ brk (1,1) ++ - prlist_with_sep + prlist_with_sep (fun () -> str "," ++ brk (1,1)) - (fun (i1,i2) -> + (fun (i1,i2) -> pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2) l) - | TacRevert l -> - hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) + | TacRevert l -> + hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) (* Constructors *) | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l) @@ -825,10 +825,10 @@ and pr_atom1 = function hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t) | TacAnyConstructor (ev,None) as t -> pr_atom0 t | TacConstructor (ev,n,l) -> - hov 1 (str (with_evars ev "constructor") ++ + hov 1 (str (with_evars ev "constructor") ++ pr_or_metaid pr_intarg n ++ pr_bindings l) - (* Conversion *) + (* Conversion *) | TacReduce (r,h) -> hov 1 (pr_red_expr r ++ pr_clauses pr_ident h) @@ -837,7 +837,7 @@ and pr_atom1 = function (match occ with None -> mt() | Some occlc -> - pr_with_occurrences_with_trailer pr_constr occlc + pr_with_occurrences_with_trailer pr_constr occlc (spc () ++ str "with ")) ++ pr_constr c ++ pr_clauses pr_ident h) @@ -848,15 +848,15 @@ and pr_atom1 = function | TacTransitivity None -> str "etransitivity" (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> - hov 1 (str (with_evars ev "rewrite") ++ + | TacRewrite (ev,l,cl,by) -> + hov 1 (str (with_evars ev "rewrite") ++ prlist_with_sep (fun () -> str ","++spc()) - (fun (b,m,c) -> + (fun (b,m,c) -> pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) l ++ pr_clauses pr_ident cl - ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) + ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ @@ -866,8 +866,8 @@ and pr_atom1 = function pr_quantified_hypothesis hyp ++ pr_with_inversion_names ids ++ pr_simple_hyp_clause pr_ident cl) | TacInversion (InversionUsing (c,cl),hyp) -> - hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ - spc () ++ str "using" ++ spc () ++ pr_constr c ++ + hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ + spc () ++ str "using" ++ spc () ++ pr_constr c ++ pr_simple_hyp_clause pr_ident cl) in @@ -876,7 +876,7 @@ let rec pr_tac inherited tac = let (strm,prec) = match tac with | TacAbstract (t,None) -> str "abstract " ++ pr_tac (labstract,L) t, labstract - | TacAbstract (t,Some s) -> + | TacAbstract (t,Some s) -> hov 0 (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++ str "using " ++ pr_id s), @@ -896,7 +896,7 @@ let rec pr_tac inherited tac = ++ fnl() ++ str "end"), lmatch | TacMatchGoal (lz,lr,lrul) -> - hov 0 (pr_lazy lz ++ + hov 0 (pr_lazy lz ++ str (if lr then "match reverse goal with" else "match goal with") ++ prlist (fun r -> fnl () ++ str "| " ++ @@ -909,7 +909,7 @@ let rec pr_tac inherited tac = prlist pr_funvar lvar ++ str " =>" ++ spc () ++ pr_tac (lfun,E) body), lfun - | TacThens (t,tl) -> + | TacThens (t,tl) -> hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_tac ltop) tl), lseq @@ -925,7 +925,7 @@ let rec pr_tac inherited tac = hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacDo (n,t) -> - hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ + hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacRepeat t -> @@ -941,7 +941,7 @@ let rec pr_tac inherited tac = hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), lorelse - | TacFail (n,l) -> + | TacFail (n,l) -> str "fail" ++ (if n=ArgArg 0 then mt () else pr_arg (pr_or_var int) n) ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom | TacFirst tl -> @@ -988,7 +988,7 @@ and pr_tacarg = function pr_may_eval pr_constr pr_lconstr pr_cst c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacExternal (_,com,req,la) -> - str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ + str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la | (TacCall _|Tacexp _|Integer _) as a -> str "ltac:" ++ pr_tac (latom,E) (TacArg a) @@ -1016,7 +1016,7 @@ let strip_prod_binders_constr n (sigma,ty) = let drop_env f _env = f let rec raw_printers = - (pr_raw_tactic_level, + (pr_raw_tactic_level, drop_env pr_constr_expr, drop_env pr_lconstr_expr, pr_lconstr_pattern_expr, @@ -1036,7 +1036,7 @@ and pr_raw_match_rule env t = let pr_and_constr_expr pr (c,_) = pr c let rec glob_printers = - (pr_glob_tactic_level, + (pr_glob_tactic_level, (fun env -> pr_and_constr_expr (pr_rawconstr_env env)), (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)), (fun c -> pr_lconstr_pattern_env (Global.env()) c), diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index b672e9c23e..081d5fd3be 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -25,8 +25,8 @@ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -37,13 +37,13 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_genarg_pprule : +val declare_extra_genarg_pprule : ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit @@ -51,12 +51,12 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : +val declare_extra_tactic_pprule : string * argument_type list * (int * grammar_terminals) -> unit val exists_extra_tactic_pprule : string -> argument_type list -> bool -val pr_raw_generic : +val pr_raw_generic : (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> @@ -83,7 +83,7 @@ val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds - + val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 26fa535506..95e921a24b 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id$ *) open Pp open Names open Nameops -open Nametab +open Nametab open Util open Extend open Vernacexpr @@ -62,11 +62,11 @@ let sep_end () = str"." (* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *) -let pr_raw_tactic_env l env t = +let pr_raw_tactic_env l env t = pr_glob_tactic env (Tacinterp.glob_tactic_env l env t) let pr_gen env t = - pr_raw_generic + pr_raw_generic pr_constr_expr pr_lconstr_expr (pr_raw_tactic_level env) pr_reference t @@ -137,7 +137,7 @@ 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 (b,c) = +let pr_search_about (b,c) = (if b then str "-" else mt()) ++ match c with | SearchSubPattern p -> pr_constr_pattern_expr p @@ -176,8 +176,8 @@ let pr_printoption table b = prlist_with_sep spc str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b -let pr_set_option a b = - let pr_opt_value = function +let pr_set_option a b = + let pr_opt_value = function | IntValue n -> spc() ++ int n | StringValue s -> spc() ++ str s | BoolValue b -> mt() @@ -193,13 +193,13 @@ let pr_opt_hintbases l = match l with | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z -let pr_hints local db h pr_c pr_pat = +let pr_hints local db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = match h with | HintsResolve l -> - str "Resolve " ++ prlist_with_sep sep - (fun (pri, _, c) -> pr_c c ++ + str "Resolve " ++ prlist_with_sep sep + (fun (pri, _, c) -> pr_c c ++ match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) l | HintsImmediate l -> @@ -207,11 +207,11 @@ let pr_hints local db h pr_c pr_pat = | 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 + 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) -> + | 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 @@ -239,8 +239,8 @@ let rec pr_module_type pr_c = function | CMTEapply (fexpr,mexpr)-> let f = pr_module_type pr_c fexpr in let m = pr_module_expr mexpr in - f ++ spc () ++ m - + f ++ spc () ++ m + and pr_module_expr = function | CMEident qid -> pr_located pr_qualid qid | CMEapply (me1,(CMEident _ as me2)) -> @@ -271,7 +271,7 @@ let pr_module_vardecls pr_c (export,idl,mty) = hov 1 (str"(" ++ pr_require_token export ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")") -let pr_module_binders l pr_c = +let pr_module_binders l pr_c = (* Effet de bord complexe pour garantir la declaration des noms des modules parametres dans la Nametab des l'appel de pr_module_binders malgre l'aspect paresseux des streams *) @@ -299,16 +299,16 @@ let pr_and_type_binders_arg bl = pr_binders_arg bl let pr_onescheme (idop,schem) = - match schem with + match schem with | InductionScheme (dep,ind,s) -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() | None -> spc () ) ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") - ++ spc() ++ pr_smart_global ind) ++ spc() ++ + ++ spc() ++ pr_smart_global ind) ++ spc() ++ hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) - | EqualityScheme ind -> + | EqualityScheme ind -> (match idop with | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc() | None -> spc() @@ -332,10 +332,10 @@ let pr_assumption_token many = function str (if many then "Variables" else "Variable") | (Global,Logical) -> str (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> + | (Global,Definitional) -> str (if many then "Parameters" else "Parameter") | (Global,Conjectural) -> str"Conjecture" - | (Local,Conjectural) -> + | (Local,Conjectural) -> anomaly "Don't know how to beautify a local conjecture" let pr_params pr_c (xl,(c,t)) = @@ -379,14 +379,14 @@ let pr_syntax_modifier = function let pr_syntax_modifiers = function | [] -> mt() - | l -> spc() ++ + | l -> spc() ++ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")") let print_level n = if n <> 0 then str " (at level " ++ int n ++ str ")" else mt () let pr_grammar_tactic_rule n (_,pil,t) = - hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ + hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ hov 0 (prlist_with_sep sep pr_production_item pil ++ spc() ++ str":=" ++ spc() ++ pr_raw_tactic t)) @@ -397,7 +397,7 @@ let pr_box b = let pr_boxkind = function | PpHOVB n -> str"hov" ++ spc() ++ int n | PpTB -> str"t" in str"<" ++ pr_boxkind b ++ str">" - + let pr_paren_reln_or_extern = function | None,L -> str"L" | None,E -> str"E" @@ -414,7 +414,7 @@ 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_record_field (x, ntn) = +let pr_record_field (x, ntn) = let prx = match x with | (oc,AssumExpr (id,t)) -> hov 1 (pr_lname id ++ @@ -430,13 +430,13 @@ let pr_record_field (x, ntn) = pr_lconstr b)) in prx ++ pr_decl_notation pr_constr ntn in -let pr_record_decl b c fs = +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 - + (* Proof management *) | VernacAbortAll -> str "Abort All" | VernacRestart -> str"Restart" @@ -447,17 +447,17 @@ let rec pr_vernac = function | 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) -> + | VernacBacktrack (i,j,k) -> str "Backtrack" ++ spc() ++ prlist_with_sep sep int [i;j;k] | VernacFocus i -> str"Focus" ++ pr_opt int i - | VernacGo g -> + | VernacGo g -> let pr_goable = function | GoTo i -> int i | GoTop -> str"top" | GoNext -> str"next" - | GoPrev -> str"prev" + | GoPrev -> str"prev" in str"Go" ++ spc() ++ pr_goable g - | VernacShow s -> + | VernacShow s -> let pr_showable = function | ShowGoal n -> str"Show" ++ pr_opt int n | ShowGoalImplicitly n -> str"Show Implicit Arguments" ++ pr_opt int n @@ -471,7 +471,7 @@ let rec pr_vernac = function | ShowMatch id -> str"Show Match " ++ pr_lident id | ShowThesis -> str "Show Thesis" | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l - | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l + | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s | VernacCheckGuard -> str"Guarded" @@ -490,13 +490,13 @@ let rec pr_vernac = function | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l - ++ spc() ++ str"]") + ++ spc() ++ str"]") | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose" ++ spc()) else spc() ++ qs s | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v | VernacTimeout(n,v) -> str"Timeout " ++ int n ++ spc() ++ pr_vernac v - - (* Syntax *) + + (* Syntax *) | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e) | VernacOpenCloseScope (local,opening,sc) -> str (if opening then "Open " else "Close ") ++ pr_locality local ++ @@ -507,11 +507,11 @@ let rec pr_vernac = function | VernacBindScope (sc,cll) -> str"Bind Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ prlist_with_sep spc pr_class_rawexpr cll - | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function + | VernacArgumentsScope (local,q,scl) -> let pr_opt_scope = function | None -> str"_" - | Some sc -> str sc in - str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ - pr_smart_global q + | Some sc -> str sc in + str"Arguments Scope" ++ spc() ++ pr_non_locality local ++ + pr_smart_global 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 @@ -523,7 +523,7 @@ let rec pr_vernac = function | VernacNotation (local,c,(s,l),opt) -> let ps = let n = String.length s in - if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' + if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then let s' = String.sub s 1 (n-2) in if String.contains s' '\'' then qs s else str s' @@ -575,13 +575,13 @@ let rec pr_vernac = function | None -> if opac then str"Qed" else str"Defined" | Some (id,th) -> (match th with | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id - | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) + | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)) | VernacExactProof c -> hov 2 (str"Proof" ++ pr_lconstrarg c) | VernacAssumption (stre,_,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in hov 2 - (pr_assumption_token (n > 1) stre ++ spc() ++ + (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) | VernacInductive (f,i,l) -> @@ -595,13 +595,13 @@ let rec pr_vernac = function 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 - | RecordDecl (c,fs) -> + 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" + str (match k with Record -> "Record" | Structure -> "Structure" | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" | Class b -> if b then "Definitional Class" else "Class") in @@ -609,13 +609,13 @@ let rec pr_vernac = function kw ++ spc() ++ (if i then str"Infer" else str"") ++ (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 + 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)) @@ -631,25 +631,25 @@ let rec pr_vernac = function let bl = bl @ bl' in let ids = List.flatten (List.map name_of_binder bl) in let annot = - match n with - | None -> mt () - | Some (loc, id) -> + match n with + | None -> mt () + | Some (loc, id) -> match (ro : Topconstr.recursion_order_expr) with - CStructRec -> - if List.length ids > 1 then + CStructRec -> + 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() ++ + | 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 " ++ + | 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"}" in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ - ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ + ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ pr_decl_notation pr_constr ntn in let start = if b then "Boxed Fixpoint" else "Fixpoint" in @@ -664,12 +664,12 @@ let rec pr_vernac = function let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ spc() ++ pr_lconstr_expr c ++ - str" :=" ++ brk(1,1) ++ pr_lconstr def ++ + str" :=" ++ brk(1,1) ++ pr_lconstr def ++ pr_decl_notation pr_constr ntn in let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in hov 1 (str start ++ spc() ++ - prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) + prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs) | VernacScheme l -> hov 2 (str"Scheme" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onescheme l) @@ -677,7 +677,7 @@ let rec pr_vernac = function hov 2 (str"Combined Scheme" ++ spc() ++ pr_lident id ++ spc() ++ str"from" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - + (* Gallina extensions *) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) @@ -703,7 +703,7 @@ let rec pr_vernac = function | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 ( str"Identity Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ + str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) @@ -717,13 +717,13 @@ let rec pr_vernac = function (* 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 (glob, sup, (instid, bk, cl), props, pri) -> + + | VernacInstance (glob, sup, (instid, bk, cl), props, pri) -> hov 1 ( pr_non_locality (not glob) ++ - str"Instance" ++ spc () ++ + str"Instance" ++ spc () ++ pr_and_type_binders_arg sup ++ - str"=>" ++ spc () ++ + 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":=" ++ spc () ++ @@ -733,35 +733,35 @@ let rec pr_vernac = function hov 1 ( str"Context" ++ spc () ++ str"[" ++ spc () ++ pr_and_type_binders_arg l ++ spc () ++ str "]") - + | VernacDeclareInstance id -> hov 1 (str"Instance" ++ spc () ++ pr_lident id) - + (* Modules and Module Types *) | VernacDefineModule (export,m,bl,ty,bd) -> - let b = pr_module_binders_list bl pr_lconstr in + let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Module" ++ spc() ++ pr_require_token export ++ pr_lident m ++ b ++ pr_opt (pr_of_module_type pr_lconstr) ty ++ pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) | VernacDeclareModule (export,id,bl,m1) -> - let b = pr_module_binders_list bl pr_lconstr in + let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ pr_lident id ++ b ++ pr_of_module_type pr_lconstr m1) | VernacDeclareModuleType (id,bl,m) -> - let b = pr_module_binders_list bl pr_lconstr in + let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Module Type " ++ pr_lident id ++ b ++ pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) | VernacInclude (in_ast) -> begin match in_ast with | CIMTE mty -> - hov 2 (str"Include" ++ + hov 2 (str"Include" ++ (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty) | CIME mexpr -> - hov 2 (str"Include" ++ + hov 2 (str"Include" ++ (fun me -> str " " ++ pr_module_expr me) mexpr) end (* Solving *) @@ -775,12 +775,12 @@ let rec pr_vernac = function str"Existential " ++ int i ++ pr_lconstrarg c (* MMode *) - + | VernacProofInstr instr -> anomaly "Not implemented" - | VernacDeclProof -> str "proof" + | VernacDeclProof -> str "proof" | VernacReturn -> str "return" - (* /MMode *) + (* /MMode *) (* Auxiliary file and library management *) | VernacRequireFrom (exp,spe,f) -> hov 2 @@ -794,9 +794,9 @@ let rec pr_vernac = function (str"Add" ++ (if fl then str" Rec " else spc()) ++ str"LoadPath" ++ spc() ++ qs s ++ - (match d with + (match d with | None -> mt() - | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) + | Some dir -> spc() ++ str"as" ++ spc() ++ pr_dirpath dir)) | VernacRemoveLoadPath s -> str"Remove LoadPath" ++ qs s | VernacAddMLPath (fl,s) -> str"Add" ++ (if fl then str" Rec " else spc()) ++ str"ML Path" ++ qs s @@ -811,13 +811,13 @@ let rec pr_vernac = function match body with | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in - pr_ltac_id id ++ + pr_ltac_id id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in - pr_raw_tactic_env - (idl @ List.map coerce_reference_to_id + pr_raw_tactic_env + (idl @ List.map coerce_reference_to_id (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l))) (Global.env()) body in @@ -830,7 +830,7 @@ let rec pr_vernac = function 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 ++ + (str"Notation " ++ pr_locality local ++ pr_lident id ++ prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) | VernacDeclareImplicits (local,q,None) -> @@ -863,24 +863,24 @@ let rec pr_vernac = function hv 0 (prlist_with_sep sep pr_line l)) | VernacUnsetOption (l,na) -> hov 1 (pr_locality_full l ++ str"Unset" ++ spc() ++ pr_printoption na None) - | VernacSetOption (l,na,v) -> + | VernacSetOption (l,na,v) -> hov 2 (pr_locality_full l ++ str"Set" ++ spc() ++ pr_set_option na v) | VernacAddOption (na,l) -> hov 2 (str"Add" ++ spc() ++ pr_printoption na (Some l)) | VernacRemoveOption (na,l) -> hov 2 (str"Remove" ++ spc() ++ pr_printoption na (Some l)) | VernacMemOption (na,l) -> hov 2 (str"Test" ++ spc() ++ pr_printoption na (Some l)) | VernacPrintOption na -> hov 2 (str"Test" ++ spc() ++ pr_printoption na None) - | VernacCheckMayEval (r,io,c) -> - let pr_mayeval r c = match r with + | VernacCheckMayEval (r,io,c) -> + let pr_mayeval r c = match r with | Some r0 -> hov 2 (str"Eval" ++ spc() ++ pr_red_expr (pr_constr,pr_lconstr,pr_smart_global) r0 ++ spc() ++ str"in" ++ spc () ++ pr_constr c) - | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) - in - (if io = None then mt() else int (Option.get io) ++ str ": ") ++ + | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) + in + (if io = None then mt() else int (Option.get io) ++ str ": ") ++ pr_mayeval r c | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) - | VernacPrint p -> + | VernacPrint p -> let pr_printable = function | PrintFullContext -> str"Print All" | PrintSectionContext s -> @@ -911,17 +911,17 @@ let rec pr_vernac = function | PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid | PrintInspect n -> str"Inspect" ++ spc() ++ int n | PrintScopes -> str"Print Scopes" - | PrintScope s -> str"Print Scope" ++ spc() ++ str s - | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s + | PrintScope s -> str"Print Scope" ++ spc() ++ str s + | PrintVisibility s -> str"Print Visibility" ++ pr_opt str s | PrintAbout qid -> str"About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_smart_global qid -(* spiwack: command printing all the axioms and section variables used in a +(* spiwack: command printing all the axioms and section variables used in a term *) | PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies") ++ spc() ++ pr_smart_global qid in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr - | VernacLocate loc -> + | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_smart_global qid | LocateFile f -> str"File" ++ spc() ++ qs f @@ -932,14 +932,14 @@ let rec pr_vernac = function hov 2 (str"Comments" ++ spc() ++ prlist_with_sep sep (pr_comment pr_constr) l) | VernacNop -> mt() - + (* Toplevel control *) | VernacToplevelControl exn -> pr_topcmd exn (* For extension *) | VernacExtend (s,c) -> pr_extend s c | VernacProof (Tacexpr.TacId _) -> str "Proof" - | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te + | VernacProof te -> str "Proof with" ++ spc() ++ pr_raw_tactic te and pr_extend s cl = let pr_arg a = @@ -951,7 +951,7 @@ and pr_extend s cl = let start,rl,cl = match rl with | Egrammar.GramTerminal s :: rl -> str s, rl, cl - | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl + | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 48e3698d43..c24744f300 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - + (*i $Id$ i*) open Pp diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 0518da327b..12a3bb572e 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -62,20 +62,20 @@ let with_line_skip p = if ismt p then mt() else (fnl () ++ p) (********************************) (** Printing implicit arguments *) - + let conjugate_to_be = function [_] -> "is" | _ -> "are" let pr_implicit imp = pr_id (name_of_implicit imp) let print_impl_args_by_name max = function | [] -> mt () - | impls -> - hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ - prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ + | impls -> + hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ str (conjugate_to_be impls) ++ str" implicit" ++ (if max then strbrk " and maximally inserted" else mt())) ++ fnl() -let print_impl_args l = +let print_impl_args l = let imps = List.filter is_status_implicit l in let maximps = List.filter Impargs.maximal_insertion_of imps in let nonmaximps = list_subtract imps maximps in @@ -87,23 +87,23 @@ let print_impl_args l = let print_ref reduce ref = let typ = Global.type_of_global ref in - let typ = + let typ = if reduce then let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ - in it_mkProd_or_LetIn ccl ctx + in it_mkProd_or_LetIn ccl ctx else typ in hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl () let print_argument_scopes = function | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl() | l when not (List.for_all ((=) None) l) -> - hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ + hov 2 (str"Argument scopes are" ++ spc() ++ + str "[" ++ prlist_with_sep spc (function Some sc -> str sc | None -> str "_") l ++ str "]") ++ fnl() | _ -> mt() -let need_expansion impl ref = +let need_expansion impl ref = let typ = Global.type_of_global ref in let ctx = (prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in @@ -116,7 +116,7 @@ type opacity = | TransparentMaybeOpacified of Conv_oracle.level let opacity env = function - | VarRef v when pi2 (Environ.lookup_named v env) <> None -> + | VarRef v when pi2 (Environ.lookup_named v env) <> None -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in @@ -129,7 +129,7 @@ let opacity env = function let print_opacity ref = match opacity (Global.env()) ref with | None -> mt () - | Some s -> pr_global ref ++ str " is " ++ + | Some s -> pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> @@ -140,14 +140,14 @@ let print_opacity ref = "transparent (with expansion weight "^string_of_int n^")" | TransparentMaybeOpacified Conv_oracle.Expand -> "transparent (with minimal expansion weight)") ++ fnl() - + let print_name_infos ref = let impl = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in - let type_for_implicit = + let type_for_implicit = if need_expansion impl ref then (* Need to reduce since implicits are computed with products flattened *) - str "Expanded type for implicit arguments" ++ fnl () ++ + str "Expanded type for implicit arguments" ++ fnl () ++ print_ref true ref ++ fnl() else mt() in type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes @@ -155,14 +155,14 @@ let print_name_infos ref = let print_id_args_data test pr id l = if List.exists test l then str"For " ++ pr_id id ++ str": " ++ pr l - else + else mt() let print_args_data_of_inductive_ids get test pr sp mipv = prvecti - (fun i mip -> + (fun i mip -> print_id_args_data test pr mip.mind_typename (get (IndRef (sp,i))) ++ - prvecti + prvecti (fun j idc -> print_id_args_data test pr idc (get (ConstructRef ((sp,i),j+1)))) mip.mind_consnames) @@ -173,7 +173,7 @@ let print_inductive_implicit_args = implicits_of_global is_status_implicit print_impl_args let print_inductive_argument_scopes = - print_args_data_of_inductive_ids + print_args_data_of_inductive_ids Notation.find_arguments_scope ((<>) None) print_argument_scopes (*********************) @@ -190,7 +190,7 @@ let locate_any_name ref = let module N = Nametab in let (loc,qid) = qualid_of_reference ref in try Term (N.locate qid) - with Not_found -> + with Not_found -> try Syntactic (N.locate_syndef qid) with Not_found -> try Dir (N.locate_dir qid) @@ -219,7 +219,7 @@ let pr_located_qualid = function str s ++ spc () ++ pr_dirpath dir | ModuleType (qid,_) -> str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid) - | Undefined qid -> + | Undefined qid -> pr_qualid qid ++ spc () ++ str "not a defined object." let print_located_qualid ref = @@ -231,7 +231,7 @@ let print_located_qualid ref = | SynDef kn -> Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in match List.map expand (N.locate_extended_all qid) with - | [] -> + | [] -> let (dir,id) = repr_qualid qid in if dir = empty_dirpath then str "No object of basename " ++ pr_id id @@ -291,7 +291,7 @@ let print_constructors envpar names types = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c) (Array.to_list (array_map2 (fun n t -> (n,t)) names types)) - in + in hv 0 (str " " ++ pc) let build_inductive sp tyi = @@ -300,7 +300,7 @@ let build_inductive sp tyi = let args = extended_rel_list 0 params in let env = Global.env() in let fullarity = match mip.mind_arity with - | Monomorphic ar -> ar.mind_user_arity + | Monomorphic ar -> ar.mind_user_arity | Polymorphic ar -> it_mkProd_or_LetIn (mkSort (Type ar.poly_level)) mip.mind_arity_ctxt in let arity = hnf_prod_applist env fullarity args in @@ -335,7 +335,7 @@ let get_fields = let id = match na with Name id -> id | Anonymous -> id_of_string "_" in prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c | _ -> List.rev l - in + in prodec_rec [] [] let pr_record (sp,tyi) = @@ -345,15 +345,15 @@ let pr_record (sp,tyi) = let fields = get_fields cstrtypes.(0) in hov 0 ( hov 0 ( - str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ + str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++ - str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ - str ":= " ++ pr_id cstrnames.(0)) ++ + 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(2,0)) - (fun (id,b,c) -> - pr_id id ++ str (if b then " : " else " := ") ++ + (fun (id,b,c) -> + pr_id id ++ str (if b then " : " else " := ") ++ pr_lconstr_env envpar c) fields) ++ str" }") let gallina_print_inductive sp = @@ -364,11 +364,11 @@ let gallina_print_inductive sp = pr_record (List.hd names) else pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ - with_line_skip + with_line_skip (print_inductive_implicit_args sp mipv ++ print_inductive_argument_scopes sp mipv) -let print_named_decl id = +let print_named_decl id = gallina_print_named_decl (Global.lookup_named id) ++ fnl () let gallina_print_section_variable id = @@ -391,26 +391,26 @@ let print_constant with_values sep sp = let val_0 = cb.const_body in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( - match val_0 with - | None -> - str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ + match val_0 with + | None -> + str"*** [ " ++ + print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" - | _ -> + | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)) ++ fnl () let gallina_print_constant_with_infos sp = - print_constant true " = " sp ++ + print_constant true " = " sp ++ with_line_skip (print_name_infos (ConstRef sp)) let gallina_print_syntactic_def kn = let sep = " := " and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn - and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in + and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in let c = Topconstr.rawconstr_of_aconstr dummy_loc a in - str "Notation " ++ pr_qualid qid ++ + str "Notation " ++ pr_qualid qid ++ prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ Constrextern.without_symbols pr_lrawconstr c ++ fnl () @@ -419,7 +419,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = and tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes + (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> @@ -427,34 +427,34 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = | (_,"INDUCTIVE") -> Some (gallina_print_inductive kn) | (_,"MODULE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) | (_,s) -> None -let gallina_print_library_entry with_values ent = +let gallina_print_library_entry with_values ent = let pr_name (sp,_) = pr_id (basename sp) in match ent with - | (oname,Lib.Leaf lobj) -> + | (oname,Lib.Leaf lobj) -> gallina_print_leaf_entry with_values (oname,lobj) - | (oname,Lib.OpenedSection (dir,_)) -> + | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> + | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> Some (str " >>>>>>> Library " ++ pr_dirpath dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> + | (oname,Lib.ClosedModule _) -> Some (str " >>>>>>> Closed Module " ++ pr_name oname) | (oname,Lib.OpenedModtype _) -> Some (str " >>>>>>> Module Type " ++ pr_name oname) - | (oname,Lib.ClosedModtype _) -> + | (oname,Lib.ClosedModtype _) -> Some (str " >>>>>>> Closed Module Type " ++ pr_name oname) | (_,Lib.FrozenState _) -> None @@ -464,14 +464,14 @@ let gallina_print_leaf_entry with_values c = | None -> mt () | Some pp -> pp ++ fnl() -let gallina_print_context with_values = +let gallina_print_context with_values = let rec prec n = function - | h::rest when n = None or Option.get n > 0 -> + | h::rest when n = None or Option.get n > 0 -> (match gallina_print_library_entry with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () - in + in prec let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} = @@ -520,16 +520,16 @@ let print_typed_value x = print_typed_value_in_env (Global.env ()) x let print_judgment env {uj_val=trm;uj_type=typ} = print_typed_value_in_env env (trm, typ) - + let print_safe_judgment env j = let trm = Safe_typing.j_val j in let typ = Safe_typing.j_type j in print_typed_value_in_env env (trm, typ) - + (*********************) (* *) -let print_full_context () = +let print_full_context () = print_context true None (Lib.contents_after None) let print_full_context_typ () = @@ -545,28 +545,28 @@ let print_full_pure_context () = let val_0 = cb.const_body in let typ = ungeneralized_type_of_constant_type cb.const_type in hov 0 ( - match val_0 with + match val_0 with | None -> str (if cb.const_opaque then "Axiom " else "Parameter ") ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype typ | Some v -> if cb.const_opaque then - str "Theorem " ++ print_basename con ++ cut () ++ + str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ str "Proof " ++ print_body val_0 else - str "Definition " ++ print_basename con ++ cut () ++ + str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ print_body val_0) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> let (mib,mip) = Global.lookup_inductive (kn,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names ++ str "." ++ + pr_mutual_inductive mib.mind_finite names ++ str "." ++ fnl () ++ fnl () | "MODULE" -> (* TODO: make it reparsable *) - let (mp,_,l) = repr_kn kn in + let (mp,_,l) = repr_kn kn in print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) @@ -576,7 +576,7 @@ let print_full_pure_context () = | _ -> mt () in prec rest ++ pp | _::rest -> prec rest - | _ -> mt () in + | _ -> mt () in prec (Lib.contents_after None) (* For printing an inductive definition with @@ -584,14 +584,14 @@ let print_full_pure_context () = assume that the declaration of constructors and eliminations follows the definition of the inductive type *) -let list_filter_vec f vec = - let rec frec n lf = - if n < 0 then lf - else if f vec.(n) then +let list_filter_vec f vec = + let rec frec n lf = + if n < 0 then lf + else if f vec.(n) then frec (n-1) (vec.(n)::lf) - else + else frec (n-1) lf - in + in frec (Array.length vec -1) [] (* This is designed to print the contents of an opened section *) @@ -608,12 +608,12 @@ let read_sec_context r = error "Cannot print the contents of a closed section." (* LEM: Actually, we could if we wanted to. *) | [] -> [] - | hd::rest -> get_cxt (hd::in_cxt) rest + | hd::rest -> get_cxt (hd::in_cxt) rest in let cxt = (Lib.contents_after None) in List.rev (get_cxt [] cxt) -let print_sec_context sec = +let print_sec_context sec = print_context true None (read_sec_context sec) let print_sec_context_typ sec = @@ -630,9 +630,9 @@ let print_any_name = function | ModuleType (_,kn) -> print_modtype kn | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) - let dir,str = repr_qualid qid in + let dir,str = repr_qualid qid in if (repr_dirpath dir) <> [] then raise Not_found; - let (_,c,typ) = Global.lookup_named str in + let (_,c,typ) = Global.lookup_named str in (print_named_decl (str,c,typ)) with Not_found -> errorlabstrm @@ -641,33 +641,33 @@ let print_any_name = function let print_name = function | Genarg.ByNotation (loc,ntn,sc) -> print_any_name - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) | Genarg.AN ref -> print_any_name (locate_any_name ref) -let print_opaque_name qid = +let print_opaque_name qid = let env = Global.env () in match global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if cb.const_body <> None then print_constant_with_infos cst - else + else error "Not a defined constant." | IndRef (sp,_) -> print_inductive sp - | ConstructRef cstr -> + | ConstructRef cstr -> let ty = Inductiveops.type_of_constructor env cstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in + let (_,c,ty) = lookup_named id env in print_named_decl (id,c,ty) let print_about_any k = begin match k with | Term ref -> - print_ref false ref ++ fnl () ++ print_name_infos ref ++ + print_ref false ref ++ fnl () ++ print_name_infos ref ++ print_opacity ref | Syntactic kn -> print_syntactic_def kn @@ -679,7 +679,7 @@ let print_about_any k = let print_about = function | Genarg.ByNotation (loc,ntn,sc) -> print_about_any - (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc)) | Genarg.AN ref -> print_about_any (locate_any_name ref) @@ -690,20 +690,20 @@ let print_impargs ref = let has_impl = List.filter is_status_implicit impl <> [] in (* Need to reduce since implicits are computed with products flattened *) print_ref (need_expansion impl ref) ref ++ fnl() ++ - (if has_impl then print_impl_args impl + (if has_impl then print_impl_args impl else (str "No implicit arguments" ++ fnl ())) -let unfold_head_fconst = +let unfold_head_fconst = let rec unfrec k = match kind_of_term k with - | Const cst -> constant_value (Global.env ()) cst + | Const cst -> constant_value (Global.env ()) cst | Lambda (na,t,b) -> mkLambda (na,t,unfrec b) | App (f,v) -> appvect (unfrec f,v) | _ -> k - in + in unfrec (* for debug *) -let inspect depth = +let inspect depth = print_context false (Some depth) (Lib.contents_after None) @@ -717,8 +717,8 @@ let print_coercion_value v = pr_lconstr (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in pr_class cl - -let print_path ((i,j),p) = + +let print_path ((i,j),p) = hov 2 ( str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ @@ -726,45 +726,45 @@ let print_path ((i,j),p) = let _ = Classops.install_path_printer print_path -let print_graph () = +let print_graph () = prlist_with_sep pr_fnl print_path (inheritance_graph()) -let print_classes () = +let print_classes () = prlist_with_sep pr_spc pr_class (classes()) -let print_coercions () = +let print_coercions () = prlist_with_sep pr_spc print_coercion_value (coercions()) - + let index_of_class cl = - try + try fst (class_info cl) - with _ -> + with _ -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between cls clt = +let print_path_between cls clt = let i = index_of_class cls in let j = index_of_class clt in - let p = - try - lookup_path_between_class (i,j) - with _ -> + let p = + try + lookup_path_between_class (i,j) + with _ -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in print_path ((i,j),p) -let pr_cs_pattern = function +let pr_cs_pattern = function Const_cs c -> pr_global c | Prod_cs -> str "_ -> _" | Default_cs -> str "_" | Sort_cs s -> pr_sort_family s let print_canonical_projections () = - prlist_with_sep pr_fnl - (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ - str " <- " ++ + prlist_with_sep pr_fnl + (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") (canonical_projections ()) @@ -775,25 +775,25 @@ let print_canonical_projections () = open Typeclasses -let pr_typeclass env t = +let pr_typeclass env t = print_ref false t.cl_impl let print_typeclasses () = let env = Global.env () in prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) - -let pr_instance env i = + +let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) print_ref false (ConstRef (instance_impl i)) - + let print_all_instances () = let env = Global.env () in - let inst = all_instances () 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 + let inst = instances r in prlist_with_sep fnl (pr_instance env) inst - + diff --git a/parsing/printer.ml b/parsing/printer.ml index b23f94a70f..eacad74c4c 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -29,11 +29,11 @@ open Ppconstr open Constrextern open Tacexpr -let emacs_str s alts = +let emacs_str s alts = match !Flags.print_emacs, !Flags.print_emacs_safechar with | true, true -> alts | true , false -> s - | false,_ -> "" + | false,_ -> "" (**********************************************************************) (** Terms *) @@ -77,7 +77,7 @@ let pr_ljudge j = pr_ljudge_env (Global.env()) j let pr_lrawconstr_env env c = pr_lconstr_expr (extern_rawconstr (vars_of_env env) c) -let pr_rawconstr_env env c = +let pr_rawconstr_env env c = pr_constr_expr (extern_rawconstr (vars_of_env env) c) let pr_lrawconstr c = @@ -130,7 +130,7 @@ let pr_var_decl env (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = pr_lconstr_env env c in let pb = if isCast c then surround pb else pb in (str" := " ++ pb ++ cut () ) in @@ -142,7 +142,7 @@ let pr_rel_decl env (na,c,typ) = let pbody = match c with | None -> mt () | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = pr_lconstr_env env c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in @@ -162,7 +162,7 @@ let pr_named_context_of env = 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 = +let pr_named_context env ne_context = hv 0 (Sign.fold_named_context (fun d pps -> pps ++ ws 2 ++ pr_var_decl env d) ne_context ~init:(mt ())) @@ -179,14 +179,14 @@ let pr_context_unlimited env = fold_named_context (fun env d pps -> let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt)) - env ~init:(mt ()) + env ~init:(mt ()) in let db_env = fold_rel_context (fun env d pps -> let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) env ~init:(mt ()) - in + in (sign_env ++ db_env) let pr_ne_context_of header env = @@ -197,21 +197,21 @@ let pr_ne_context_of header env = let pr_context_limit n env = let named_context = Environ.named_context env in let lgsign = List.length named_context in - if n >= lgsign then + if n >= lgsign then pr_context_unlimited env else let k = lgsign-n in let _,sign_env = fold_named_context (fun env d (i,pps) -> - if i < k then + if i < k then (i+1, (pps ++str ".")) else let pidt = pr_var_decl env d in (i+1, (pps ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pidt))) - env ~init:(0,(mt ())) + env ~init:(0,(mt ())) in let db_env = fold_rel_context @@ -221,10 +221,10 @@ let pr_context_limit n env = str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pnat)) env ~init:(mt ()) - in + in (sign_env ++ db_env) -let pr_context_of env = match Flags.print_hyps_limit () with +let pr_context_of env = match Flags.print_hyps_limit () with | None -> hv 0 (pr_context_unlimited env) | Some n -> hv 0 (pr_context_limit n env) @@ -234,33 +234,33 @@ let pr_restricted_named_context among env = hv 0 (fold_named_context (fun env ((id,_,_) as d) pps -> if true || Idset.mem id among then - pps ++ + pps ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pr_var_decl env d - else + else pps) env ~init:(mt ())) -let pr_predicate pr_elt (b, elts) = +let pr_predicate pr_elt (b, elts) = let pr_elts = prlist_with_sep spc pr_elt elts in if b then - str"all" ++ + str"all" ++ (if elts = [] then mt () else str" except: " ++ pr_elts) else if elts = [] then str"none" else pr_elts - + let pr_cpred p = pr_predicate pr_con (Cpred.elements p) let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p) -let pr_transparent_state (ids, csts) = +let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) let pr_subgoal_metas metas env= - let pr_one (meta,typ) = - str "?" ++ int meta ++ str " : " ++ - hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ + let pr_one (meta,typ) = + str "?" ++ int meta ++ str " : " ++ + hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") in hv 0 (prlist_with_sep mt pr_one metas) @@ -272,7 +272,7 @@ let default_pr_goal g = mt (), mt (), pr_context_of env, pr_ltype_env_at_top env g.evar_concl - else + else (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), pr_context_of env, @@ -283,7 +283,7 @@ let default_pr_goal g = str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () - + (* display the conclusion of a goal *) let pr_concl n g = let env = evar_env g in @@ -292,7 +292,7 @@ let pr_concl n g = str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) -let pr_evgl_sign gl = +let pr_evgl_sign gl = let ps = pr_named_context_of (evar_unfiltered_env gl) in let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in let ids = List.rev (List.map pi1 l) in @@ -307,10 +307,10 @@ let pr_evgl_sign gl = let rec pr_evars_int i = function | [] -> (mt ()) | (ev,evd)::rest -> - let pegl = pr_evgl_sign evd in + let pegl = pr_evgl_sign evd in let pei = pr_evars_int (i+1) rest in (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - str (string_of_existential ev) ++ str " : " ++ pegl)) ++ + str (string_of_existential ev) ++ str " : " ++ pegl)) ++ fnl () ++ pei let default_pr_subgoal n = @@ -320,22 +320,22 @@ let default_pr_subgoal n = if p = 1 then let pg = default_pr_goal g in v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) - else + else prrec (p-1) rest - in + in prrec n (* Print open subgoals. Checks for uninstantiated existential variables *) -let default_pr_subgoals close_cmd sigma = function - | [] -> +let default_pr_subgoals close_cmd sigma = function + | [] -> begin match close_cmd with Some cmd -> - (str "Subproof completed, now type " ++ str cmd ++ + (str "Subproof completed, now type " ++ str cmd ++ str "." ++ fnl ()) | None -> - let exl = Evarutil.non_instantiated sigma in - if exl = [] then + let exl = Evarutil.non_instantiated sigma in + if exl = [] then (str"Proof completed." ++ fnl ()) else let pei = pr_evars_int 1 exl in @@ -351,11 +351,11 @@ let default_pr_subgoals close_cmd sigma = function | g::rest -> let pc = pr_concl n g in let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) + (cut () ++ pc ++ prest) in let pg1 = default_pr_goal g1 in let prest = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () + v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ prest ++ fnl ()) @@ -388,17 +388,17 @@ let pr_goal x = !printer_pr.pr_goal x let pr_open_subgoals () = let pfts = get_pftreestate () in - let gls = fst (frontier (proof_of_pftreestate pfts)) in + let gls = fst (frontier (proof_of_pftreestate pfts)) in match focus() with - | 0 -> + | 0 -> let sigma = (top_goal_of_pftreestate pfts).sigma in let close_cmd = Decl_mode.get_end_command pfts in pr_subgoals close_cmd sigma gls - | n -> + | n -> assert (n > List.length gls); - if List.length gls < 2 then + if List.length gls < 2 then pr_subgoal n gls - else + else (* LEM TODO: this way of saying how many subgoals has to be abstracted out*) v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ pr_subgoal n gls) @@ -410,25 +410,25 @@ let pr_nth_open_subgoal n = (* Elementary tactics *) let pr_prim_rule = function - | Intro id -> + | Intro id -> str"intro " ++ pr_id id - + | Cut (b,replace,id,t) -> if b then (* TODO: express "replace" *) (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") else let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ + (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - + | FixRule (f,n,[],_) -> (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> + + | FixRule (f,n,others,j) -> if j<>0 then warning "Unsupported printing of \"fix\""; let rec print_mut = function - | (f,n,ar)::oth -> + | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth | [] -> mt () in (str"fix " ++ pr_id f ++ str"/" ++ int n ++ @@ -444,26 +444,26 @@ let pr_prim_rule = function (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) | [] -> mt () in (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - | Refine c -> + | Refine c -> str(if occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - + | Convert_concl (c,_) -> (str"change " ++ pr_constr c) - + | Convert_hyp (id,None,t) -> (str"change " ++ pr_constr t ++ spc () ++ str"in " ++ pr_id id) | Convert_hyp (id,Some c,t) -> (str"change " ++ pr_constr c ++ spc () ++ str"in " ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") - + | Thin ids -> (str"clear " ++ prlist_with_sep pr_spc pr_id ids) - + | ThinBody ids -> (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) - + | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) @@ -488,7 +488,7 @@ let prterm = pr_lconstr (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -let pr_assumptionset env s = +let pr_assumptionset env s = if (Environ.ContextObjectMap.is_empty s) then str "Closed under the global context" else @@ -497,7 +497,7 @@ let pr_assumptionset env s = let (v,a,o) = r in match t with | Variable id -> ( Some ( - Option.default (fnl ()) v + Option.default (fnl ()) v ++ str (string_of_id id) ++ str " : " ++ pr_ltype typ @@ -527,7 +527,7 @@ let pr_assumptionset env s = ) s (None,None,None) in - let (vars,axioms,opaque) = + let (vars,axioms,opaque) = ( Option.map (fun p -> str "Section Variables:" ++ p) vars , Option.map (fun p -> str "Axioms:" ++ p) axioms , Option.map (fun p -> str "Opaque constants:" ++ p) opaque @@ -540,9 +540,9 @@ let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m [] open Typeclasses -let pr_instance i = +let pr_instance i = pr_global (ConstRef (instance_impl i)) - + let pr_instance_gmap insts = prlist_with_sep fnl (fun (gr, insts) -> prlist_with_sep fnl pr_instance (cmap_to_list insts)) diff --git a/parsing/printer.mli b/parsing/printer.mli index 32f0519480..1797eaf22b 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -112,8 +112,8 @@ val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds (* Emacs/proof general support *) -(* (emacs_str s alts) outputs - - s if emacs mode & unicode allowed, +(* (emacs_str s alts) outputs + - s if emacs mode & unicode allowed, - alts if emacs mode and & unicode not allowed - nothing otherwise *) val emacs_str : string -> string -> string diff --git a/parsing/printmod.ml b/parsing/printmod.ml index 2ec914d6cd..a5470a8924 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -13,8 +13,8 @@ open Declarations open Nameops open Libnames -let get_new_id locals id = - let rec get_id l id = +let get_new_id locals id = + let rec get_id l id = let dir = make_dirpath [id] in if not (Nametab.exists_module dir) then id @@ -29,19 +29,19 @@ let rec print_local_modpath locals = function print_local_modpath locals mp ++ str "." ++ pr_lab l | MPself _ | MPfile _ -> raise Not_found -let print_modpath locals mp = +let print_modpath locals mp = try (* must be with let because streams are lazy! *) - let qid = Nametab.shortest_qualid_of_module mp in + let qid = Nametab.shortest_qualid_of_module mp in pr_qualid qid with | Not_found -> print_local_modpath locals mp -let print_kn locals kn = +let print_kn locals kn = try - let qid = Nametab.shortest_qualid_of_modtype kn in + let qid = Nametab.shortest_qualid_of_modtype kn in pr_qualid qid with - Not_found -> + Not_found -> try print_local_modpath locals kn with @@ -52,50 +52,50 @@ let rec flatten_app mexpr l = match mexpr with | mexpr -> mexpr::l let rec print_module name locals with_body mb = - let body = match with_body, mb.mod_expr with - | false, _ + let body = match with_body, mb.mod_expr with + | false, _ | true, None -> mt() - | true, Some mexpr -> + | true, Some mexpr -> spc () ++ str ":= " ++ print_modexpr locals mexpr in let modtype = match mb.mod_type with None -> str "" - | Some t -> spc () ++ str": " ++ + | Some t -> spc () ++ str": " ++ print_modtype locals t in hv 2 (str "Module " ++ name ++ modtype ++ body) -and print_modtype locals mty = +and print_modtype locals mty = match mty with | SEBident kn -> print_kn locals kn | SEBfunctor (mbid,mtb1,mtb2) -> - (* let env' = Modops.add_module (MPbid mbid) - (Modops.body_of_type mtb) env - in *) + (* let env' = Modops.add_module (MPbid mbid) + (Modops.body_of_type mtb) env + in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid)) ::locals in - hov 2 (str "Funsig" ++ spc () ++ str "(" ++ - pr_id (id_of_mbid mbid) ++ str " : " ++ - print_modtype locals mtb1.typ_expr ++ + hov 2 (str "Funsig" ++ spc () ++ str "(" ++ + pr_id (id_of_mbid mbid) ++ str " : " ++ + print_modtype locals mtb1.typ_expr ++ str ")" ++ spc() ++ print_modtype locals' mtb2) - | SEBstruct (msid,sign) -> + | SEBstruct (msid,sign) -> hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End") - | SEBapply (mexpr,marg,_) -> + | SEBapply (mexpr,marg,_) -> let lapp = flatten_app mexpr [marg] in let fapp = List.hd lapp in let mapp = List.tl lapp in - hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++ + hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++ prlist_with_sep spc (print_modexpr locals) mapp ++ str")") | SEBwith(seb,With_definition_body(idl,cb))-> let s = (String.concat "." (List.map string_of_id idl)) in - hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ + 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,_,_))-> let s =(String.concat "." (List.map string_of_id idl)) in - hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ + hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) -and print_sig locals msid sign = +and print_sig locals msid sign = let print_spec (l,spec) = (match spec with | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " | SFBconst {const_body=None} @@ -107,7 +107,7 @@ and print_sig locals msid sign = in prlist_with_sep spc print_spec sign -and print_struct locals msid struc = +and print_struct locals msid struc = let print_body (l,body) = (match body with | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem " @@ -119,41 +119,41 @@ and print_struct locals msid struc = in prlist_with_sep spc print_body struc -and print_modexpr locals mexpr = match mexpr with +and print_modexpr locals mexpr = match mexpr with | SEBident mp -> print_modpath locals mp | SEBfunctor (mbid,mty,mexpr) -> -(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env +(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ - str ":" ++ print_modtype locals mty.typ_expr ++ + hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++ + str ":" ++ print_modtype locals mty.typ_expr ++ str ")" ++ spc () ++ print_modexpr locals' mexpr) - | SEBstruct (msid, struc) -> + | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") - | SEBapply (mexpr,marg,_) -> + | SEBapply (mexpr,marg,_) -> let lapp = flatten_app mexpr [marg] in hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")") | SEBwith (_,_)-> anomaly "Not avaible yet" -let rec printable_body dir = +let rec printable_body dir = let dir = pop_dirpath dir in - dir = empty_dirpath || - try + dir = empty_dirpath || + try match Nametab.locate_dir (qualid_of_dirpath dir) with DirOpenModtype _ -> false | DirModule _ | DirOpenModule _ -> printable_body dir | _ -> true - with + with Not_found -> true -let print_module with_body mp = +let print_module with_body mp = let name = print_modpath [] mp in print_module name [] with_body (Global.lookup_module mp) ++ fnl () -let print_modtype kn = +let print_modtype kn = let mtb = Global.lookup_modtype kn in let name = print_kn [] kn in - str "Module Type " ++ name ++ str " = " ++ + str "Module Type " ++ name ++ str " = " ++ print_modtype [] mtb.typ_expr ++ fnl () diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index a796cef822..093910b4d4 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -21,8 +21,8 @@ open Pcaml let loc = dummy_loc let dloc = <:expr< Util.dummy_loc >> -let apply_ref f l = - <:expr< +let apply_ref f l = + <:expr< Rawterm.RApp ($dloc$, Rawterm.RRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) >> @@ -57,13 +57,13 @@ EXTEND (* fix todo *) ] | "100" RIGHTA - [ c1 = constr; ":"; c2 = SELF -> + [ c1 = constr; ":"; c2 = SELF -> <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] | "90" RIGHTA - [ c1 = constr; "->"; c2 = SELF -> + [ c1 = constr; "->"; c2 = SELF -> <:expr< Rawterm.RProd ($dloc$,Anonymous,Rawterm.Explicit,$c1$,$c2$) >> ] | "75" RIGHTA - [ "~"; c = constr -> + [ "~"; c = constr -> apply_ref <:expr< coq_not_ref >> [c] ] | "70" RIGHTA [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> @@ -85,26 +85,26 @@ EXTEND ; match_constr: [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; - "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> + "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> let br = mlexpr_of_list (fun x -> x) br in - <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> + <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> ] ] ; match_type: - [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; - "return"; ty = constr LEVEL "100" -> + [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; + "return"; ty = constr LEVEL "100" -> let nal = mlexpr_of_list (fun x -> x) nal in - <:expr< Some $ty$ >>, - <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> + <:expr< Some $ty$ >>, + <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] ; eqn: - [ [ (lid,pl) = pattern; "=>"; rhs = constr -> + [ [ (lid,pl) = pattern; "=>"; rhs = constr -> let lid = mlexpr_of_list (fun x -> x) lid in - <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> + <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> ] ] ; - pattern: + pattern: [ [ "%"; e = string; lip = LIST0 patvar -> let lp = mlexpr_of_list (fun (_,x) -> x) lip in let lid = List.flatten (List.map fst lip) in @@ -113,13 +113,13 @@ EXTEND | "("; p = pattern; ")" -> p ] ] ; patvar: - [ [ "_" -> [], <:expr< Rawterm.PatVar ($dloc$,Anonymous) >> - | id = ident -> [id], <:expr< Rawterm.PatVar ($dloc$,Name $id$) >> + [ [ "_" -> [], <:expr< Rawterm.PatVar ($dloc$,Anonymous) >> + | id = ident -> [id], <:expr< Rawterm.PatVar ($dloc$,Name $id$) >> ] ] ; END;; -(* Example +(* Example open Coqlib let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 91cb681a5d..cd3e7d2a83 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -28,11 +28,11 @@ IFDEF CAMLP5 THEN DEFINE NOP END let anti loc x = let e = let loc = - IFDEF NOP THEN + IFDEF NOP THEN loc - ELSE + ELSE (1, snd loc - fst loc) - END + END in <:expr< $lid:purge_str x$ >> in <:expr< $anti:e$ >> @@ -47,7 +47,7 @@ let mlexpr_of_ident id = let mlexpr_of_name = function | Names.Anonymous -> <:expr< Names.Anonymous >> - | Names.Name id -> + | Names.Name id -> <:expr< Names.Name (Names.id_of_string $str:Names.string_of_id id$) >> let mlexpr_of_dirpath dir = @@ -68,7 +68,7 @@ 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,sco) -> + | Genarg.ByNotation (loc,s,sco) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >> let mlexpr_of_intro_pattern = function @@ -134,14 +134,14 @@ let mlexpr_of_red_flags { let mlexpr_of_explicitation = function | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >> | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >> - + let mlexpr_of_binding_kind = function | Rawterm.Implicit -> <:expr< Rawterm.Implicit >> | Rawterm.Explicit -> <:expr< Rawterm.Explicit >> let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.Generalized (b,b',b'') -> + | Topconstr.Generalized (b,b',b'') -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ $mlexpr_of_binding_kind b'$ $mlexpr_of_bool b''$ >> @@ -153,7 +153,7 @@ let rec mlexpr_of_constr = function | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CArrow (loc,a,b) -> <:expr< Topconstr.CArrow $dloc$ $mlexpr_of_constr a$ $mlexpr_of_constr b$ >> - | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list + | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" @@ -164,10 +164,10 @@ let rec mlexpr_of_constr = function | Topconstr.CHole (loc, Some _) -> failwith "mlexpr_of_constr: TODO CHole (Some _)" | Topconstr.CNotation(_,ntn,subst) -> <:expr< Topconstr.CNotation $dloc$ $mlexpr_of_string ntn$ - $mlexpr_of_pair + $mlexpr_of_pair (mlexpr_of_list mlexpr_of_constr) (mlexpr_of_list (mlexpr_of_list mlexpr_of_constr)) subst$ >> - | Topconstr.CPatVar (loc,n) -> + | Topconstr.CPatVar (loc,n) -> <:expr< Topconstr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >> | _ -> failwith "mlexpr_of_constr: TODO" @@ -216,7 +216,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.List0ArgType t -> <:expr< Genarg.List0ArgType $mlexpr_of_argtype loc t$ >> | Genarg.List1ArgType t -> <:expr< Genarg.List1ArgType $mlexpr_of_argtype loc t$ >> | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> - | Genarg.PairArgType (t1,t2) -> + | Genarg.PairArgType (t1,t2) -> let t1 = mlexpr_of_argtype loc t1 in let t2 = mlexpr_of_argtype loc t2 in <:expr< Genarg.PairArgType $t1$ $t2$ >> @@ -237,10 +237,10 @@ let mlexpr_of_binding_kind = function | Rawterm.ExplicitBindings l -> let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in <:expr< Rawterm.ExplicitBindings $l$ >> - | Rawterm.ImplicitBindings l -> + | Rawterm.ImplicitBindings l -> let l = mlexpr_of_list mlexpr_of_constr l in <:expr< Rawterm.ImplicitBindings $l$ >> - | Rawterm.NoBindings -> + | Rawterm.NoBindings -> <:expr< Rawterm.NoBindings >> let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr @@ -256,7 +256,7 @@ let mlexpr_of_move_location f = function let mlexpr_of_induction_arg = function | Tacexpr.ElimOnConstr c -> <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> - | Tacexpr.ElimOnIdent (_,id) -> + | Tacexpr.ElimOnIdent (_,id) -> <:expr< Tacexpr.ElimOnIdent $dloc$ $mlexpr_of_ident id$ >> | Tacexpr.ElimOnAnonHyp n -> <:expr< Tacexpr.ElimOnAnonHyp $mlexpr_of_int n$ >> @@ -347,11 +347,11 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> 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$ + <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> <:expr< Tacexpr.TacGeneralize - $mlexpr_of_list + $mlexpr_of_list (mlexpr_of_pair mlexpr_of_occ_constr mlexpr_of_name) cl$ >> | Tacexpr.TacGeneralizeDep c -> <:expr< Tacexpr.TacGeneralizeDep $mlexpr_of_constr c$ >> @@ -366,8 +366,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacInductionDestruct (isrec,ev,l) -> - <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_list (mlexpr_of_quadruple + <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ + $mlexpr_of_list (mlexpr_of_quadruple (mlexpr_of_list mlexpr_of_induction_arg) (mlexpr_of_option mlexpr_of_constr_with_binding) (mlexpr_of_pair @@ -437,7 +437,7 @@ let rec mlexpr_of_atomic_tactic = function and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function | Tacexpr.TacAtom (loc,t) -> <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >> - | Tacexpr.TacThen (t1,[||],t2,[||]) -> + | Tacexpr.TacThen (t1,[||],t2,[||]) -> <:expr< Tacexpr.TacThen $mlexpr_of_tactic t1$ [||] $mlexpr_of_tactic t2$ [||]>> | Tacexpr.TacThens (t,tl) -> <:expr< Tacexpr.TacThens $mlexpr_of_tactic t$ $mlexpr_of_list mlexpr_of_tactic tl$>> @@ -455,7 +455,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> | Tacexpr.TacProgress t -> <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> - | Tacexpr.TacId l -> + | Tacexpr.TacId l -> <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> | Tacexpr.TacFail (n,l) -> <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >> @@ -477,7 +477,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> | Tacexpr.TacMatchGoal (lz,lr,l) -> - <:expr< Tacexpr.TacMatchGoal + <:expr< Tacexpr.TacMatchGoal $mlexpr_of_bool lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> @@ -495,7 +495,7 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function and mlexpr_of_tactic_arg = function | Tacexpr.MetaIdArg (loc,true,id) -> anti loc id - | Tacexpr.MetaIdArg (loc,false,id) -> + | Tacexpr.MetaIdArg (loc,false,id) -> <:expr< Tacexpr.ConstrMayEval (Rawterm.ConstrTerm $anti loc id$) >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> @@ -523,7 +523,7 @@ let ftac e = let ep s = patt_of_expr (ee s) in Quotation.ExAst (ee, ep) -let _ = +let _ = Quotation.add "constr" (fconstr Pcoq.Constr.constr_eoi); Quotation.add "tactic" (ftac Pcoq.Tactic.tactic_eoi); Quotation.default := "constr" diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 4694497491..7b9037d92d 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -20,7 +20,7 @@ let not_impl name x = let desc = if Obj.is_block (Obj.repr x) then "tag = " ^ string_of_int (Obj.tag (Obj.repr x)) - else + else "int_val = " ^ string_of_int (Obj.magic x) in failwith ("<Q_util." ^ name ^ ", not impl: " ^ desc) diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index d52ab8dd73..517e34aa2c 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -43,7 +43,7 @@ let rec make_let e = function let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in - let v = + let v = (* Special case for tactics which must be stored in algebraic form to avoid marshalling closures and to be reprinted *) if is_tactic_genarg t then @@ -95,7 +95,7 @@ let rec make_eval_tactic e = function let rec make_fun e = function | [] -> e - | GramNonTerminal(loc,_,_,Some p)::l -> + | GramNonTerminal(loc,_,_,Some p)::l -> let p = Names.string_of_id p in <:expr< fun $lid:p$ -> $make_fun e l$ >> | _::l -> make_fun e l @@ -138,7 +138,7 @@ let rec contains_epsilon = function | ExtraArgType("hintbases") -> true | _ -> false let is_atomic = function - | GramTerminal s :: l when + | GramTerminal s :: l when List.for_all (function GramTerminal _ -> false | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l @@ -152,7 +152,7 @@ let declare_tactic loc s cl = let hide_tac (p,e) = (* reste a definir les fonctions cachees avec des noms frais *) let stac = "h_"^s in - let e = + let e = make_fun <:expr< Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ @@ -194,7 +194,7 @@ EXTEND ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> + -> if match List.hd l with GramNonTerminal _ -> true | _ -> false then (* En attendant la syntaxe de tacticielles *) failwith "Tactic syntax must start with an identifier"; diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 49cec626f4..c09b3431e5 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -23,30 +23,30 @@ let pr_tactic = function | TacArg (Tacexp t) -> (*top tactic from tacinterp*) Pptactic.pr_glob_tactic (Global.env()) t - | t -> + | t -> Pptactic.pr_tactic (Global.env()) t -let pr_proof_instr instr = +let pr_proof_instr instr = Ppdecl_proof.pr_proof_instr (Global.env()) instr let pr_rule = function | Prim r -> hov 0 (pr_prim_rule r) | Nested(cmpd,_) -> begin - match cmpd with + match cmpd with | Tactic (texp,_) -> hov 0 (pr_tactic texp) | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) end | Daimon -> str "<Daimon>" - | Decl_proof _ -> str "proof" + | Decl_proof _ -> str "proof" let uses_default_tac = function | Nested(Tactic(_,dflt),_) -> dflt | _ -> false (* Does not print change of evars *) -let pr_rule_dot = function - | Prim Change_evars ->str "PC: ch_evars" ++ mt () +let pr_rule_dot = function + | Prim Change_evars ->str "PC: ch_evars" ++ mt () (* PC: this might be redundant *) | r -> pr_rule r ++ if uses_default_tac r then str "..." else str"." @@ -66,7 +66,7 @@ exception Different let thin_sign osign sign = Sign.fold_named_context (fun (id,c,ty as d) sign -> - try + try if Sign.lookup_named id osign = (id,c,ty) then sign else raise Different with Not_found | Different -> Environ.push_named_context_val d sign) @@ -76,17 +76,17 @@ let rec print_proof _sigma osign pf = let hyps = Environ.named_context_of_val pf.goal.evar_hyps in let hyps' = thin_sign osign hyps in match pf.ref with - | None -> + | None -> hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) | Some(r,spfl) -> - hov 0 + hov 0 (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++ spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ hov 0 (prlist_with_sep pr_fnl (print_proof _sigma hyps) spfl)) - -let pr_change gl = + +let pr_change gl = str"change " ++ pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." @@ -94,9 +94,9 @@ let print_decl_script tac_printer ?(nochange=true) sigma pf = let rec print_prf pf = match pf.ref with | None -> - (if nochange then + (if nochange then (str"<Your Proof Text here>") - else + else pr_change pf.goal) ++ fnl () | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)" @@ -114,17 +114,17 @@ let print_decl_script tac_printer ?(nochange=true) sigma pf = (if opened then mt () else str "end claim." ++ fnl ()) ++ print_prf cont | Pfocus _,[body;cont] -> - hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ + hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++ (if opened then mt () else str "end focus." ++ fnl ()) ++ print_prf cont | (Psuppose _ |Pcase (_,_,_)),[body;cont] -> hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++ - print_prf cont + print_prf cont | _,[next] -> pr_rule_dot_fnl rule ++ print_prf next | _,[] -> - pr_rule_dot rule + pr_rule_dot rule | _,_ -> anomaly "unknown branching instruction" end | _ -> anomaly "Not Applicable" in @@ -134,19 +134,19 @@ let print_script ?(nochange=true) sigma pf = let rec print_prf pf = match pf.ref with | None -> - (if nochange then - (str"<Your Tactic Text here>") - else + (if nochange then + (str"<Your Tactic Text here>") + else pr_change pf.goal) ++ fnl () | Some(Decl_proof opened,script) -> assert (List.length script = 1); begin - if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) end ++ begin - hov 0 (str "proof." ++ fnl () ++ - print_decl_script print_prf + hov 0 (str "proof." ++ fnl () ++ + print_decl_script print_prf ~nochange sigma (List.hd script)) end ++ fnl () ++ begin @@ -167,7 +167,7 @@ let print_treescript ?(nochange=true) sigma pf = let rec print_prf pf = match pf.ref with | None -> - if nochange then + if nochange then if pf.goal.evar_extra=None then str"<Your Tactic Text here>" else str"<Your Proof Text here>" else pr_change pf.goal @@ -176,10 +176,10 @@ let print_treescript ?(nochange=true) sigma pf = begin if nochange then mt () else pr_change pf.goal ++ fnl () end ++ - hov 0 + hov 0 begin str "proof." ++ fnl () ++ - print_decl_script print_prf ~nochange sigma (List.hd script) - end ++ fnl () ++ + print_decl_script print_prf ~nochange sigma (List.hd script) + end ++ fnl () ++ begin if opened then mt () else (str "end proof." ++ fnl ()) end @@ -197,27 +197,27 @@ let rec print_info_script sigma osign pf = match pf.ref with | None -> (mt ()) | Some(r,spfl) -> - (pr_rule r ++ + (pr_rule r ++ match spfl with | [pf1] -> - if pf1.ref = None then + if pf1.ref = None then (str "." ++ fnl ()) - else + else (str";" ++ brk(1,3) ++ - print_info_script sigma + print_info_script sigma (Environ.named_context_of_val sign) pf1) | _ -> (str"." ++ fnl () ++ prlist_with_sep pr_fnl - (print_info_script sigma + (print_info_script sigma (Environ.named_context_of_val sign)) spfl)) -let format_print_info_script sigma osign pf = +let format_print_info_script sigma osign pf = hov 0 (print_info_script sigma osign pf) - -let print_subscript sigma sign pf = - if is_tactic_proof pf then + +let print_subscript sigma sign pf = + if is_tactic_proof pf then format_print_info_script sigma sign (subproof_of_proof pf) - else + else format_print_info_script sigma sign pf let _ = Refiner.set_info_printer print_subscript diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index dd05d5cd76..e8a3094b9a 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -75,7 +75,7 @@ EXTEND ; rule: [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]" - -> + -> if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty."); (s,l,<:expr< fun () -> $e$ >>) ] ] |