From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- parsing/egrammar.ml | 34 ++++--- parsing/g_ascii_syntax.ml | 4 +- parsing/g_constr.ml4 | 32 +++--- parsing/g_intsyntax.ml | 6 +- parsing/g_ltac.ml4 | 6 +- parsing/g_minicoq.ml4 | 177 -------------------------------- parsing/g_prim.ml4 | 20 +++- parsing/g_tactic.ml4 | 151 +++++++++++++++------------ parsing/g_vernac.ml4 | 10 +- parsing/g_xml.ml4 | 44 ++++---- parsing/g_zsyntax.ml | 6 +- parsing/lexer.ml4 | 62 ++++++----- parsing/pcoq.ml4 | 28 ++--- parsing/pcoq.mli | 6 +- parsing/ppconstr.ml | 14 +-- parsing/ppconstr.mli | 3 +- parsing/pptactic.ml | 249 +++++++++++++++++++++++---------------------- parsing/pptactic.mli | 4 +- parsing/ppvernac.ml | 13 +-- parsing/prettyp.ml | 20 ++-- parsing/printer.ml | 34 +++++-- parsing/printer.mli | 5 +- parsing/q_coqast.ml4 | 55 +++++----- parsing/q_util.ml4 | 7 +- parsing/q_util.mli | 6 +- parsing/search.ml | 4 +- parsing/tacextend.ml4 | 4 +- parsing/tactic_printer.ml | 84 +++++++-------- parsing/tactic_printer.mli | 6 +- parsing/vernacextend.ml4 | 4 +- 30 files changed, 497 insertions(+), 601 deletions(-) delete mode 100644 parsing/g_minicoq.ml4 (limited to 'parsing') diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 9416bff2..825d1af0 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml 10987 2008-05-26 12:28:36Z herbelin $ *) +(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -114,27 +114,33 @@ let make_constr_prod_item univ assoc from forpat = function let prepare_empty_levels entry (pos,p4assoc,name,reinit) = grammar_extend entry pos reinit [(name, p4assoc, [])] -let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) = +let pure_sublevels level symbs = + map_succeed (function + | Gramext.Snterml (_,n) when Some (int_of_string n) <> level -> + int_of_string n + | _ -> + failwith "") symbs + +let extend_constr (entry,level) (n,assoc) mkact forpat pt = let univ = get_univ "constr" in let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in let (symbs,ntl) = List.split pil in - let needed_levels = register_empty_levels forpat symbs in + let pure_sublevels = pure_sublevels level symbs in + let needed_levels = register_empty_levels forpat pure_sublevels in + let pos,p4assoc,name,reinit = find_position forpat assoc level in List.iter (prepare_empty_levels entry) needed_levels; grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])] let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,List.map snd env) in - let (e,level) = get_constr_entry false (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position false assoc level in - extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit) - (make_constr_action mkact) (false,rule); + let e = get_constr_entry false (ETConstr (n,())) in + extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule; (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in - let (e,level) = get_constr_entry true (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position true assoc level in - extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit) - (make_cases_pattern_action mkact) (true,rule) + let e = get_constr_entry true (ETConstr (n,())) in + extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) + true rule (**********************************************************************) (** Making generic actions in type generic_argument *) @@ -228,7 +234,7 @@ let rec interp_entry_name up_level s = try get_entry (get_univ "prim") s with _ -> try get_entry (get_univ "constr") s - with _ -> error ("Unknown entry "^s) + with _ -> error ("Unknown entry "^s^".") in let o = object_of_typed_entry e in let t = type_of_typed_entry e in @@ -248,7 +254,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)) + error ("Invalid Tactic Notation level: "^(string_of_int n)^".") (* Declaration of the tactic grammar rule *) @@ -261,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) = let rules = if lev = 0 then begin if not (head_is_ident prods) then - error "Notation for simple tactic must start with an identifier"; + error "Notation for simple tactic must start with an identifier."; let mkact s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in make_rule univ (mkact key tac) mkprod prods diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml index b262b978..944e2338 100644 --- a/parsing/g_ascii_syntax.ml +++ b/parsing/g_ascii_syntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(*i $Id: g_ascii_syntax.ml 10744 2008-04-03 14:09:56Z herbelin $ i*) +(*i $Id: g_ascii_syntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pp open Util @@ -53,7 +53,7 @@ let interp_ascii_string dloc s = then int_of_string s else user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code") in + str "Expects a single character or a three-digits ascii code.") in interp_ascii dloc p let uninterp_ascii r = diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ba61eb61..b93fdadd 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_constr.ml4 11024 2008-05-30 12:41:39Z msozeau $ *) +(* $Id: g_constr.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pcoq open Constr @@ -47,7 +47,7 @@ let rec index_and_rec_order_of_annot loc bl ann = | lids, (Some (loc, n), ro) -> if List.exists (fun (_, x) -> x = Name n) lids then Some (loc, n), ro - else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable") + else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.") | _, (None, r) -> None, r let mk_fixb (id,bl,ann,body,(loc,tyc)) = @@ -61,7 +61,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofixb", - Pp.str"Annotation forbidden in cofix expression")) (fst ann) in + Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in @@ -326,7 +326,7 @@ GEXTEND Gram | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp) | _ -> Util.user_err_loc (cases_pattern_expr_loc p, "compound_pattern", - Pp.str "Constructor expected")) + Pp.str "Constructor expected.")) | p = pattern; "as"; id = ident -> CPatAlias (loc, p, id) ] | "1" LEFTA @@ -398,7 +398,12 @@ GEXTEND Gram [LocalRawAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) - | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc + | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc + | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc + | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> + List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc ] ] ; binder: @@ -407,19 +412,14 @@ GEXTEND Gram | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c) ] ] ; - typeclass_constraint_binder: - [ [ tc = typeclass_constraint -> - let (n,bk,t) = tc in - LocalRawAssum ([n], TypeClass bk, t) - ] ] - ; - typeclass_constraint: [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c - | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> - (loc, Name iid), expl, c - | c = operconstr LEVEL "200" -> - (loc, Anonymous), Implicit, c + | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + id, expl, c + | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" -> + (loc, Name iid), expl, c + | c = operconstr LEVEL "200" -> + (loc, Anonymous), Implicit, c ] ] ; diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index 6ab8f99c..a589ccf1 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: g_intsyntax.ml 11087 2008-06-10 13:29:52Z letouzey $ i*) +(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) @@ -122,7 +122,7 @@ let int31_of_pos_bigint dloc n = RApp (dloc, ref_construct, List.rev (args 31 n)) let error_negative dloc = - Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers") + Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") let interp_int31 dloc n = if is_pos_or_zero n then @@ -212,7 +212,7 @@ let bigN_of_pos_bigint dloc n = result hght (word_of_pos_bigint dloc hght n) let bigN_error_negative dloc = - Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers") + Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") let interp_bigN dloc n = if is_pos_or_zero n then diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 78a9fbc7..dbd81e7f 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_ltac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: g_ltac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -72,10 +72,10 @@ GEXTEND Gram | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchContext (b,false,mrl) + TacMatchGoal (b,false,mrl) | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchContext (b,true,mrl) + TacMatchGoal (b,true,mrl) | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> TacMatch (b,c,mrl) | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 deleted file mode 100644 index a9275cf9..00000000 --- a/parsing/g_minicoq.ml4 +++ /dev/null @@ -1,177 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ()); Token.tparse = Lexer.tparse; - Token.text = Lexer.token_text} -;; - -type command = - | Definition of identifier * constr option * constr - | Parameter of identifier * constr - | Variable of identifier * constr - | Inductive of - (identifier * constr) list * - (identifier * constr * (identifier * constr) list) list - | Check of constr - -let gram = Grammar.create lexer - -let term = Grammar.Entry.create gram "term" -let name = Grammar.Entry.create gram "name" -let nametype = Grammar.Entry.create gram "nametype" -let inductive = Grammar.Entry.create gram "inductive" -let constructor = Grammar.Entry.create gram "constructor" -let command = Grammar.Entry.create gram "command" - -let path_of_string s = make_path [] (id_of_string s) - -EXTEND - name: - [ [ id = IDENT -> Name (id_of_string id) - | "_" -> Anonymous - ] ]; - nametype: - [ [ id = IDENT; ":"; t = term -> (id_of_string id, t) - ] ]; - term: - [ [ id = IDENT -> - mkVar (id_of_string id) - | IDENT "Rel"; n = INT -> - mkRel (int_of_string n) - | "Set" -> - mkSet - | "Prop" -> - mkProp - | "Type" -> - mkType (new_univ()) - | "Const"; id = IDENT -> - mkConst (path_of_string id, [||]) - | "Ind"; id = IDENT; n = INT -> - let n = int_of_string n in - mkMutInd ((path_of_string id, n), [||]) - | "Construct"; id = IDENT; n = INT; i = INT -> - let n = int_of_string n and i = int_of_string i in - mkMutConstruct (((path_of_string id, n), i), [||]) - | "["; na = name; ":"; t = term; "]"; c = term -> - mkLambda (na,t,c) - | "("; na = name; ":"; t = term; ")"; c = term -> - mkProd (na,t,c) - | c1 = term; "->"; c2 = term -> - mkArrow c1 c2 - | "("; id = IDENT; cl = LIST1 term; ")" -> - let c = mkVar (id_of_string id) in - mkApp (c, Array.of_list cl) - | "("; cl = LIST1 term; ")" -> - begin match cl with - | [c] -> c - | c::cl -> mkApp (c, Array.of_list cl) - end - | "("; c = term; "::"; t = term; ")" -> - mkCast (c, t) - | "<"; p = term; ">"; - IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT; - "of"; bl = LIST0 term; "end" -> - let ind = (path_of_string id,int_of_string i) in - let nc = List.length bl in - let dummy_pats = Array.create nc RegularPat in - let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in - mkMutCase (dummy_ci, p, c, Array.of_list bl) - ] ]; - command: - [ [ "Definition"; id = IDENT; ":="; c = term; "." -> - Definition (id_of_string id, None, c) - | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." -> - Definition (id_of_string id, Some t, c) - | "Parameter"; id = IDENT; ":"; t = term; "." -> - Parameter (id_of_string id, t) - | "Variable"; id = IDENT; ":"; t = term; "." -> - Variable (id_of_string id, t) - | "Inductive"; "["; params = LIST0 nametype SEP ";"; "]"; - inds = LIST1 inductive SEP "with" -> - Inductive (params, inds) - | IDENT "Check"; c = term; "." -> - Check c - | EOI -> raise End_of_file - ] ]; - inductive: - [ [ id = IDENT; ":"; ar = term; ":="; constrs = LIST0 constructor SEP "|" -> - (id_of_string id,ar,constrs) - ] ]; - constructor: - [ [ id = IDENT; ":"; c = term -> (id_of_string id,c) ] ]; -END - -(* Pretty-print. *) - -let print_univers = ref false -let print_casts = ref false - -let print_type u = - if !print_univers then (str "Type" ++ pr_uni u) - else (str "Type") - -let print_name = function - | Anonymous -> (str "_") - | Name id -> pr_id id - -let print_rel bv n = print_name (List.nth bv (pred n)) - -let rename bv = function - | Anonymous -> Anonymous - | Name id as na -> - let idl = - List.fold_left - (fun l n -> match n with Name x -> x::l | _ -> l) [] bv - in - if List.mem na bv then Name (next_ident_away id idl) else na - -let rec pp bv t = - match kind_of_term t with - | Sort (Prop Pos) -> (str "Set") - | Sort (Prop Null) -> (str "Prop") - | Sort (Type u) -> print_type u - | Lambda (na, t, c) -> - (str"[" ++ print_name na ++ str":" ++ pp bv t ++ str"]" ++ pp (na::bv) c) - | Prod (Anonymous, t, c) -> - (pp bv t ++ str"->" ++ pp (Anonymous::bv) c) - | Prod (na, t, c) -> - (str"(" ++ print_name na ++ str":" ++ pp bv t ++ str")" ++ pp (na::bv) c) - | Cast (c, t) -> - if !print_casts then - (str"(" ++ pp bv c ++ str"::" ++ pp bv t ++ str")") - else - pp bv c - | App(h, v) -> - (str"(" ++ pp bv h ++ spc () ++ - prvect_with_sep (fun () -> (spc ())) (pp bv) v ++ str")") - | Const (sp, _) -> - (str"Const " ++ pr_id (basename sp)) - | Ind ((sp,i), _) -> - (str"Ind " ++ pr_id (basename sp) ++ str" " ++ int i) - | Construct (((sp,i),j), _) -> - (str"Construct " ++ pr_id (basename sp) ++ str" " ++ int i ++ - str" " ++ int j) - | Var id -> pr_id id - | Rel n -> print_rel bv n - | _ -> (str"") - -let pr_term _ ctx = pp (fold_rel_context (fun _ (n,_,_) l -> n::l) ctx []) - diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index c3792d65..1e738384 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(*i $Id: g_prim.ml4 10155 2007-09-28 22:36:35Z glondu $ i*) +(*i $Id: g_prim.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pcoq open Names @@ -23,6 +23,16 @@ open Nametab let local_make_qualid l id = make_qualid (make_dirpath l) id +let my_int_of_string loc s = + try + let n = int_of_string s in + (* To avoid Array.make errors (that e.g. Undo uses), we set a *) + (* more restricted limit than int_of_string does *) + if n > 1024 * 2048 then raise Exit; + n + with Failure _ | Exit -> + Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.") + GEXTEND Gram GLOBAL: bigint natural integer identref name ident var preident @@ -79,7 +89,7 @@ GEXTEND Gram ; ne_string: [ [ s = STRING -> - if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s + if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s ] ] ; dirpath: @@ -90,11 +100,11 @@ GEXTEND Gram [ [ s = STRING -> s ] ] ; integer: - [ [ i = INT -> int_of_string i - | "-"; i = INT -> - int_of_string i ] ] + [ [ i = INT -> my_int_of_string loc i + | "-"; i = INT -> - my_int_of_string loc i ] ] ; natural: - [ [ i = INT -> int_of_string i ] ] + [ [ i = INT -> my_int_of_string loc i ] ] ; bigint: (* Negative numbers are dealt with specially *) [ [ i = INT -> (Bigint.of_string i) ] ] diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c0a4ba5b..49f00d40 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_tactic.ml4 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: g_tactic.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Pcoq @@ -26,7 +26,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) -let lpar_id_coloneq = +let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> match Stream.npeek 1 strm with @@ -34,9 +34,7 @@ let lpar_id_coloneq = (match Stream.npeek 2 strm with | [_; ("IDENT",s)] -> (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> - Stream.junk strm; Stream.junk strm; Stream.junk strm; - Names.id_of_string s + | [_; _; ("", ":=")] -> () | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) @@ -56,7 +54,7 @@ let test_lpar_idnum_coloneq = | _ -> raise Stream.Failure) (* idem for (x:t) *) -let lpar_id_colon = +let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> match Stream.npeek 1 strm with @@ -64,9 +62,7 @@ let lpar_id_colon = (match Stream.npeek 2 strm with | [_; ("IDENT",id)] -> (match Stream.npeek 3 strm with - | [_; _; ("", ":")] -> - Stream.junk strm; Stream.junk strm; Stream.junk strm; - Names.id_of_string id + | [_; _; ("", ":")] -> () | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) @@ -131,15 +127,15 @@ let mk_fix_tac (loc,id,bl,ann,ty) = | _, Some x -> let ids = List.map snd (List.flatten (List.map pi1 bl)) in (try list_index (snd x) ids - with Not_found -> error "no such fix variable") - | _ -> error "cannot guess decreasing argument of fix" in + with Not_found -> error "No such fix variable.") + | _ -> error "Cannot guess decreasing argument of fix." in (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", - Pp.str"Annotation forbidden in cofix expression")) ann in + Pp.str"Annotation forbidden in cofix expression.")) ann in (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) @@ -162,6 +158,8 @@ let mkCLambdaN_simple bl c = let loc = join_loc (fst (List.hd (pi1 (List.hd bl)))) (constr_loc c) in mkCLambdaN_simple_loc loc bl c +let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l)) + let map_int_or_var f = function | Rawterm.ArgArg x -> Rawterm.ArgArg (f x) | Rawterm.ArgVar _ as y -> y @@ -237,27 +235,32 @@ GEXTEND Gram intropatterns: [ [ l = LIST0 simple_intropattern -> l ]] ; - simple_intropattern: - [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc - | "()" -> IntroOrAndPattern [[]] - | "("; si = simple_intropattern; ")" -> IntroOrAndPattern [[si]] + disjunctive_intropattern: + [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc + | "()" -> loc,IntroOrAndPattern [[]] + | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]] | "("; si = simple_intropattern; ","; tc = LIST1 simple_intropattern SEP "," ; ")" -> - IntroOrAndPattern [si::tc] + loc,IntroOrAndPattern [si::tc] | "("; si = simple_intropattern; "&"; tc = LIST1 simple_intropattern SEP "&" ; ")" -> (* (A & B & C) is translated into (A,(B,C)) *) let rec pairify = function | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l] - | t::q -> IntroOrAndPattern [[t;pairify q]] - in pairify (si::tc) - | "_" -> IntroWildcard - | prefix = pattern_ident -> IntroFresh prefix - | "?" -> IntroAnonymous - | id = ident -> IntroIdentifier id - | "->" -> IntroRewrite true - | "<-" -> IntroRewrite false - ] ] + | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]] + in loc,pairify (si::tc) ] ] + ; + naming_intropattern: + [ [ prefix = pattern_ident -> loc, IntroFresh prefix + | "?" -> loc, IntroAnonymous + | id = ident -> loc, IntroIdentifier id ] ] + ; + simple_intropattern: + [ [ pat = disjunctive_intropattern -> pat + | pat = naming_intropattern -> pat + | "_" -> loc, IntroWildcard + | "->" -> loc, IntroRewrite true + | "<-" -> loc, IntroRewrite false ] ] ; simple_binding: [ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c) @@ -402,7 +405,18 @@ GEXTEND Gram [ [ "using"; el = constr_with_bindings -> el ] ] ; with_names: - [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ] + [ [ "as"; ipat = simple_intropattern -> ipat + | -> dummy_loc,IntroAnonymous ] ] + ; + with_inversion_names: + [ [ "as"; ipat = disjunctive_intropattern -> Some ipat + | -> None ] ] + ; + with_induction_names: + [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern + -> (eq,Some ipat) + | "as"; eq = naming_intropattern -> (Some eq,None) + | -> (None,None) ] ] ; as_name: [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] @@ -439,30 +453,40 @@ GEXTEND Gram oriented_rewriter : [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; + induction_clause: + [ [ lc = LIST1 induction_arg; ipats = with_induction_names; + el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ] + ; + move_location: + [ [ IDENT "after"; id = id_or_meta -> MoveAfter id + | IDENT "before"; id = id_or_meta -> MoveBefore id + | "at"; IDENT "bottom" -> MoveToEnd true + | "at"; IDENT "top" -> MoveToEnd false ] ] + ; simple_tactic: [ [ (* Basic tactics *) IDENT "intros"; IDENT "until"; id = quantified_hypothesis -> TacIntrosUntil id | IDENT "intros"; pl = intropatterns -> TacIntroPattern pl - | IDENT "intro"; id = ident; IDENT "after"; id2 = identref -> - TacIntroMove (Some id, Some id2) - | IDENT "intro"; IDENT "after"; id2 = identref -> - TacIntroMove (None, Some id2) - | IDENT "intro"; id = ident -> TacIntroMove (Some id, None) - | IDENT "intro" -> TacIntroMove (None, None) + | IDENT "intro"; id = ident; hto = move_location -> + TacIntroMove (Some id, hto) + | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto) + | IDENT "intro"; id = ident -> TacIntroMove (Some id, no_move) + | IDENT "intro" -> TacIntroMove (None, no_move) | IDENT "assumption" -> TacAssumption | IDENT "exact"; c = constr -> TacExact c | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = constr_with_bindings -> TacApply (true,false,cl) - | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,true,cl) - | IDENT "simple"; IDENT "apply"; cl = constr_with_bindings -> - TacApply (false,false,cl) - | IDENT "simple"; IDENT "eapply"; cl = constr_with_bindings -> - TacApply (false, true,cl) + | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," -> + TacApply (true,false,cl) + | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> + TacApply (true,true,cl) + | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," + -> TacApply (false,false,cl) + | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> TacApply (false,true,cl) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> @@ -492,10 +516,12 @@ GEXTEND Gram TacLetTac (na,c,p,false) (* Begin compatibility *) - | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> - TacAssert (None,IntroIdentifier id,c) - | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic -> - TacAssert (Some tac,IntroIdentifier id,c) + | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + c = lconstr; ")" -> + TacAssert (None,(loc,IntroIdentifier id),c) + | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAssert (Some tac,(loc,IntroIdentifier id),c) (* End compatibility *) | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic -> @@ -521,23 +547,19 @@ GEXTEND Gram (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> - TacSimpleInduction h - | IDENT "induction"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator; cl = opt_clause -> - TacNewInduction (false,lc,el,ids,cl) - | IDENT "einduction"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator; cl = opt_clause -> - TacNewInduction (true,lc,el,ids,cl) + TacSimpleInductionDestruct (true,h) + | IDENT "induction"; ic = induction_clause -> + TacInductionDestruct (true,false,[ic]) + | IDENT "einduction"; ic = induction_clause -> + TacInductionDestruct(true,true,[ic]) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis -> - TacSimpleDestruct h - | IDENT "destruct"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator; cl = opt_clause -> - TacNewDestruct (false,lc,el,ids,cl) - | IDENT "edestruct"; lc = LIST1 induction_arg; ids = with_names; - el = OPT eliminator; cl = opt_clause -> - TacNewDestruct (true,lc,el,ids,cl) + TacSimpleInductionDestruct (false,h) + | IDENT "destruct"; ic = induction_clause -> + TacInductionDestruct(false,false,[ic]) + | IDENT "edestruct"; ic = induction_clause -> + TacInductionDestruct(false,true,[ic]) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr @@ -565,8 +587,8 @@ GEXTEND Gram | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l) | IDENT "clear"; l = LIST0 id_or_meta -> TacClear (l=[], l) | IDENT "clearbody"; l = LIST1 id_or_meta -> TacClearBody l - | IDENT "move"; id1 = id_or_meta; IDENT "after"; id2 = id_or_meta -> - TacMove (true,id1,id2) + | IDENT "move"; dep = [IDENT "dependent" -> true | -> false]; + hfrom = id_or_meta; hto = move_location -> TacMove (dep,hfrom,hto) | IDENT "rename"; l = LIST1 rename SEP "," -> TacRename l | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l @@ -601,16 +623,19 @@ GEXTEND Gram | IDENT "inversion" -> FullInversion | IDENT "inversion_clear" -> FullInversionClear ]; hyp = quantified_hypothesis; - ids = with_names; co = OPT ["with"; c = constr -> c] -> + 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_names; cl = simple_clause -> + hyp = quantified_hypothesis; ids = with_inversion_names; + cl = simple_clause -> TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) | IDENT "inversion"; - hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + hyp = quantified_hypothesis; ids = with_inversion_names; + cl = simple_clause -> TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) | IDENT "inversion_clear"; - hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + hyp = quantified_hypothesis; ids = with_inversion_names; + cl = simple_clause -> TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) | IDENT "inversion"; hyp = quantified_hypothesis; "using"; c = constr; cl = simple_clause -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 00469ad5..87c11164 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 11083 2008-06-09 22:08:14Z herbelin $ *) +(* $Id: g_vernac.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp @@ -113,7 +113,7 @@ let test_plurial_form = function let no_coercion loc (c,x) = if c then Util.user_err_loc - (loc,"no_coercion",Pp.str"no coercion allowed here"); + (loc,"no_coercion",str"No coercion allowed here."); x (* Gallina declarations *) @@ -271,7 +271,7 @@ GEXTEND Gram Some (loc, id) else Util.user_err_loc (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_id id)) + str "No argument named " ++ Nameops.pr_id id ++ str".")) | None -> (* If there is only one argument, it is the recursive one, otherwise, we search the recursive index later *) @@ -311,7 +311,7 @@ GEXTEND Gram LocalRawAssum(l,ty) -> (l,ty) | LocalRawDef _ -> Util.user_err_loc - (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ] + (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] ; *) (* ... with coercions *) @@ -491,7 +491,7 @@ GEXTEND Gram props = typeclass_field_types -> VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props) - | IDENT "Context"; c = typeclass_context -> + | IDENT "Context"; c = binders_let -> VernacContext c | global = [ IDENT "Global" -> true | -> false ]; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 5b2d8668..72d5d275 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_xml.ml4 10727 2008-03-28 20:22:43Z msozeau $ *) +(* $Id: g_xml.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -31,7 +31,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 ++ - str "does not match open xml tag " ++ str otag) + str "does not match open xml tag " ++ str otag ++ str ".") let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e) @@ -55,11 +55,19 @@ GEXTEND Gram ; END +(* Errors *) + +let error_expect_one_argument loc = + user_err_loc (loc,"",str "wrong number of arguments (expect one).") + +let error_expect_no_argument loc = + user_err_loc (loc,"",str "wrong number of arguments (expect none).") + (* Interpreting attributes *) let nmtoken (loc,a) = try int_of_string a - with Failure _ -> user_err_loc (loc,"",str "nmtoken expected") + with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") let interp_xml_attr_qualid = function | "uri", s -> qualid_of_string s @@ -94,7 +102,7 @@ let sort_of_cdata (loc,a) = match a with | "Prop" -> RProp Null | "Set" -> RProp Pos | "Type" -> RType None - | _ -> user_err_loc (loc,"",str "sort expected") + | _ -> user_err_loc (loc,"",str "sort expected.") let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) @@ -188,18 +196,18 @@ let rec interp_xml_constr = function RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2)) | XmlTag (loc,"SORT",al,[]) -> RSort (loc, get_xml_sort al) - | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") and interp_xml_tag s = function | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl) | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", - str "Expect tag " ++ str s ++ str " but find " ++ str s) + str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".") and interp_xml_constr_alias s x = match interp_xml_tag s x with | (_,_,[x]) -> interp_xml_constr x - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> error_expect_one_argument loc and interp_xml_term x = interp_xml_constr_alias "term" x and interp_xml_type x = interp_xml_constr_alias "type" x @@ -215,8 +223,7 @@ and interp_xml_substitution x = interp_xml_constr_alias "substitution" x and interp_xml_decl_alias s x = match interp_xml_tag s x with | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x) - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> error_expect_one_argument loc and interp_xml_def x = interp_xml_decl_alias "def" x and interp_xml_decl x = interp_xml_decl_alias "decl" x @@ -227,17 +234,17 @@ and interp_xml_recursionOrder x = match s with "Structural" -> (match l with [] -> RStructRec - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)")) + | _ -> error_expect_no_argument loc) | "WellFounded" -> (match l with [c] -> RWfRec (interp_xml_type c) - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> error_expect_one_argument loc) | "Measure" -> (match l with [c] -> RMeasureRec (interp_xml_type c) - | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)")) + | _ -> error_expect_one_argument loc) | _ -> - user_err_loc (locs,"",str "invalid recursion order") + user_err_loc (locs,"",str "Invalid recursion order.") and interp_xml_FixFunction x = match interp_xml_tag "FixFunction" x with @@ -248,15 +255,15 @@ and interp_xml_FixFunction x = | (loc,al,[x1;x2]) -> ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec), (get_xml_name al, interp_xml_type x1, interp_xml_body x2)) - | (loc,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + | (loc,_,_) -> + error_expect_one_argument loc 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,_,_) -> - user_err_loc (loc,"",str "wrong number of arguments (expect one)") + error_expect_one_argument loc (* Interpreting tactic argument *) @@ -266,7 +273,8 @@ let rec interp_xml_tactic_arg = function | XmlTag (loc,"CALL",al,xl) -> let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl) - | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s) + | XmlTag (loc,s,_,_) -> + user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".") let parse_tactic_arg ch = interp_xml_tactic_arg diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index aab266c0..8b9c0d22 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_zsyntax.ml 10806 2008-04-16 23:51:06Z letouzey $ *) +(* $Id: g_zsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pcoq open Pp @@ -57,7 +57,7 @@ let pos_of_bignat dloc x = let error_non_positive dloc = user_err_loc (dloc, "interp_positive", - str "Only strictly positive numbers in type \"positive\"") + str "Only strictly positive numbers in type \"positive\".") let interp_positive dloc n = if is_strictly_pos n then pos_of_bignat dloc n @@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n = RRef (dloc, glob_N0) let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"") + user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") let n_of_int dloc n = if is_pos_or_zero n then n_of_binnat dloc true n diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index c1e4cfc6..1b0c24da 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lexer.ml4 11059 2008-06-06 09:29:20Z herbelin $ i*) +(*i $Id: lexer.ml4 11238 2008-07-19 09:34:03Z herbelin $ i*) (*i camlp4use: "pr_o.cmo" i*) @@ -324,43 +324,49 @@ let rec comment bp = parser bp2 (* Parse a special token, using the [token_tree] *) (* Peek as much utf-8 lexemes as possible *) -(* then look if a special token is obtained *) -let rec special tt cs = - match Stream.peek cs with - | Some c -> progress_from_byte 0 tt cs c - | None -> tt.node - - (* nr is the number of char peeked; n the number of char in utf8 block *) -and progress_utf8 nr n c tt cs = +(* and retain the longest valid special token obtained *) +let rec progress_further last nj tt cs = + try progress_from_byte last nj tt cs (List.nth (Stream.npeek (nj+1) cs) nj) + with Failure _ -> last + +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; + progress_further last' 0 tt cs + | None -> + progress_further last nj tt cs + +(* nr is the number of char peeked since last valid token *) +(* n the number of char in utf8 block *) +and progress_utf8 last nj n c tt cs = try let tt = CharMap.find c tt.branch in - let tt = - if n=1 then tt else - match Stream.npeek (n-nr) cs with - | l when List.length l = n-nr -> - let l = Util.list_skipn (1-nr) l in - List.iter (check_utf8_trailing_byte cs) l; - List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l - | _ -> - error_utf8 cs - in - for i=1 to n-nr do Stream.junk cs done; - special tt cs + if n=1 then + update_longest_valid_token last (nj+n) tt cs + else + match Util.list_skipn (nj+1) (Stream.npeek (nj+n) cs) with + | l when List.length l = n-1 -> + 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 -> - tt.node + last -and progress_from_byte nr tt cs = function +and progress_from_byte last nj tt cs = function (* Utf8 leading byte *) - | '\x00'..'\x7F' as c -> progress_utf8 nr 1 c tt cs - | '\xC0'..'\xDF' as c -> progress_utf8 nr 2 c tt cs - | '\xE0'..'\xEF' as c -> progress_utf8 nr 3 c tt cs - | '\xF0'..'\xF7' as c -> progress_utf8 nr 4 c tt cs + | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs + | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs + | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs + | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs (* Must be a special token *) let process_chars bp c cs = - let t = progress_from_byte 1 !token_tree cs c in + let t = progress_from_byte None (-1) !token_tree cs c in let ep = Stream.count cs in match t with | Some t -> (("", t), (bp, ep)) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 70a41ddc..2e55b656 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id: pcoq.ml4 10987 2008-05-26 12:28:36Z herbelin $ i*) +(*i $Id: pcoq.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pp open Util @@ -247,7 +247,7 @@ let get_entry (u, utab) s = Hashtbl.find utab s with Not_found -> errorlabstrm "Pcoq.get_entry" - (str "unknown grammar entry " ++ str u ++ str ":" ++ str s) + (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".") let new_entry etyp (u, utab) s = let ename = u ^ ":" ^ s in @@ -307,12 +307,12 @@ let get_generic_entry s = try object_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let get_generic_entry_type (u,utab) s = try type_of_typed_entry (Hashtbl.find utab s) with Not_found -> - error ("unknown grammar entry "^u^":"^s) + error ("Unknown grammar entry "^u^":"^s^".") let force_entry_type (u, utab) s etyp = try @@ -578,7 +578,7 @@ let error_level_assoc p current expected = errorlabstrm "" (str "Level " ++ int p ++ str " is already declared " ++ pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative") + pr_assoc expected ++ str " associative.") let find_position_gen forpat ensure assoc lev = let ccurrent,pcurrent as current = List.hd !level_stack in @@ -628,13 +628,13 @@ let rec list_mem_assoc_triple x = function | [] -> false | (a,b,c) :: l -> a = x or list_mem_assoc_triple x l -let register_empty_levels forpat symbs = - map_succeed (function - | Gramext.Snterml (_,n) when - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - not (list_mem_assoc_triple (int_of_string n) levels) -> - find_position_gen forpat true None (Some (int_of_string n)) - | _ -> failwith "") symbs +let register_empty_levels forpat levels = + map_succeed (fun n -> + let levels = (if forpat then snd else fst) (List.hd !level_stack) in + if not (list_mem_assoc_triple n levels) then + find_position_gen forpat true None (Some n) + else + failwith "") levels let find_position forpat assoc level = find_position_gen forpat false assoc level @@ -695,7 +695,7 @@ let compute_entry allow_create adjust forpat = function | ETPattern -> weaken_entry Constr.pattern, None, false | ETOther ("constr","annot") -> weaken_entry Constr.annot, None, false - | ETConstrList _ -> error "List of entries cannot be registered" + | ETConstrList _ -> error "List of entries cannot be registered." | ETOther (u,n) -> let u = get_univ u in let e = @@ -762,6 +762,6 @@ let coerce_reference_to_id = function | Ident (_,id) -> id | Qualid (loc,_) -> user_err_loc (loc, "coerce_reference_to_id", - str "This expression should be a simple identifier") + str "This expression should be a simple identifier.") let coerce_global_to_id = coerce_reference_to_id diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 44a3686e..525727ce 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 10987 2008-05-26 12:28:36Z herbelin $ i*) +(*i $Id: pcoq.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) open Util open Names @@ -188,7 +188,7 @@ module Tactic : val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e - val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e + val simple_intropattern : Genarg.intro_pattern_expr located Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e val tactic_expr : raw_tactic_expr Gram.Entry.e val binder_tactic : raw_tactic_expr Gram.Entry.e @@ -229,7 +229,7 @@ val find_position : val synchronize_level_positions : unit -> unit -val register_empty_levels : bool -> Compat.token Gramext.g_symbol list -> +val register_empty_levels : bool -> int list -> (Gramext.position option * Gramext.g_assoc option * string option * Gramext.g_assoc option) list diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 985396f5..5f6ffe87 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: ppconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (*i*) open Util @@ -96,12 +96,6 @@ let pr_patnotation = pr_notation_gen decode_patlist_value let pr_delimiters key strm = strm ++ str ("%"^key) -let pr_located pr (loc,x) = - if Flags.do_translate() && loc<>dummy_loc then - let (b,e) = unloc loc in - comment b ++ pr x ++ comment e - else pr x - let pr_com_at n = if Flags.do_translate() && n <> 0 then comment n else mt() @@ -219,13 +213,13 @@ let surround_binder k p = match k with Default Explicit -> hov 1 (str"(" ++ p ++ str")") | Default Implicit -> hov 1 (str"{" ++ p ++ str"}") - | TypeClass b -> hov 1 (str"[" ++ p ++ str"]") + | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]") let surround_implicit k p = match k with Default Explicit -> p | Default Implicit -> (str"{" ++ p ++ str"}") - | TypeClass b -> (str"[" ++ p ++ str"]") + | TypeClass _ -> (str"[" ++ p ++ str"]") let pr_binder many pr (nal,k,t) = match t with @@ -719,7 +713,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function 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" + | 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 a0eb4ad9..8047e968 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ppconstr.mli 11094 2008-06-10 19:35:23Z herbelin $ i*) +(*i $Id: ppconstr.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pp open Environ @@ -35,7 +35,6 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool val pr_tight_coma : unit -> std_ppcmds -val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds val pr_metaid : identifier -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index f955d83b..6a7ae9bc 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: pptactic.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Names @@ -58,7 +58,7 @@ let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) = let s = match unquote wit with | ExtraArgType s -> s | _ -> error - "Can declare a pretty-printing rule only for extra argument types" + "Can declare a pretty-printing rule only for extra argument types." in let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in @@ -142,41 +142,40 @@ let out_bindings = function let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with - | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") - | IntArgType -> pr_arg int (out_gen rawwit_int x) - | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen rawwit_int_or_var x) - | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" - | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x) - | IntroPatternArgType -> pr_arg pr_intro_pattern - (out_gen rawwit_intro_pattern x) - | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x) - | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x) - | RefArgType -> pr_arg prref (out_gen rawwit_ref x) - | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x) - | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) + | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false") + | IntArgType -> int (out_gen rawwit_int x) + | IntOrVarArgType -> pr_or_var pr_int (out_gen rawwit_int_or_var x) + | StringArgType -> str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" + | PreIdentArgType -> str (out_gen rawwit_pre_ident x) + | IntroPatternArgType -> pr_intro_pattern (out_gen rawwit_intro_pattern x) + | IdentArgType -> pr_id (out_gen rawwit_ident x) + | VarArgType -> pr_located pr_id (out_gen rawwit_var x) + | RefArgType -> prref (out_gen rawwit_ref x) + | SortArgType -> pr_rawsort (out_gen rawwit_sort x) + | ConstrArgType -> prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc prlc (pr_or_by_notation prref)) + pr_may_eval prc prlc (pr_or_by_notation prref) (out_gen rawwit_constr_may_eval x) - | QuantHypArgType -> - pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) + | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (prc,prlc,pr_or_by_notation prref)) + pr_red_expr (prc,prlc,pr_or_by_notation prref) (out_gen rawwit_red_expr x) - | OpenConstrArgType b -> pr_arg prc (snd (out_gen (rawwit_open_constr_gen b) x)) + | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) + pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) (out_gen rawwit_bindings x) + pr_bindings_no_with prc prlc (out_gen rawwit_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt())) + hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref) + (fold_list0 (fun a l -> a::l) x [])) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt())) + hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref) + (fold_list1 (fun a l -> a::l) x [])) | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prref) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_raw_generic prc prlc prtac prref a ++ spc () ++ - pr_raw_generic prc prlc prtac prref b) + (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prref) [a;b]) x) | ExtraArgType s -> try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x @@ -185,107 +184,105 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu let rec pr_glob_generic prc prlc prtac x = match Genarg.genarg_tag x with - | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false") - | IntArgType -> pr_arg int (out_gen globwit_int x) - | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x) - | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\"" - | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x) - | IntroPatternArgType -> - pr_arg pr_intro_pattern (out_gen globwit_intro_pattern x) - | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x) - | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x) - | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x) - | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x) - | ConstrArgType -> pr_arg prc (out_gen globwit_constr x) + | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false") + | IntArgType -> int (out_gen globwit_int x) + | IntOrVarArgType -> pr_or_var pr_int (out_gen globwit_int_or_var x) + | StringArgType -> str "\"" ++ str (out_gen globwit_string x) ++ str "\"" + | PreIdentArgType -> str (out_gen globwit_pre_ident x) + | IntroPatternArgType -> pr_intro_pattern (out_gen globwit_intro_pattern x) + | IdentArgType -> pr_id (out_gen globwit_ident x) + | VarArgType -> pr_located pr_id (out_gen globwit_var x) + | RefArgType -> pr_or_var (pr_located pr_global) (out_gen globwit_ref x) + | SortArgType -> pr_rawsort (out_gen globwit_sort x) + | ConstrArgType -> prc (out_gen globwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc prlc - (pr_or_var (pr_and_short_name pr_evaluable_reference))) + pr_may_eval prc prlc + (pr_or_var (pr_and_short_name pr_evaluable_reference)) (out_gen globwit_constr_may_eval x) | QuantHypArgType -> - pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x) + pr_quantified_hypothesis (out_gen globwit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference))) + pr_red_expr + (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference)) (out_gen globwit_red_expr x) - | OpenConstrArgType b -> pr_arg prc (snd (out_gen (globwit_open_constr_gen b) x)) + | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) + pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) (out_gen globwit_bindings x) + pr_bindings_no_with prc prlc (out_gen globwit_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt())) + hov 0 (pr_sequence (pr_glob_generic prc prlc prtac) + (fold_list0 (fun a l -> a::l) x [])) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prlc prtac x ++ a) x (mt())) + hov 0 (pr_sequence (pr_glob_generic prc prlc prtac) + (fold_list1 (fun a l -> a::l) x [])) | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_glob_generic prc prlc prtac a ++ spc () ++ - pr_glob_generic prc prlc prtac b) + (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac) [a;b]) x) | ExtraArgType s -> try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str " [no printer for " ++ str s ++ str "] " + with Not_found -> str "[no printer for " ++ str s ++ str "] " open Closure let rec pr_generic prc prlc prtac x = match Genarg.genarg_tag x with - | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") - | IntArgType -> pr_arg int (out_gen wit_int x) - | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen wit_int_or_var x) - | StringArgType -> spc () ++ str "\"" ++ str (out_gen wit_string x) ++ str "\"" - | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) - | IntroPatternArgType -> - pr_arg pr_intro_pattern (out_gen wit_intro_pattern x) - | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) - | VarArgType -> pr_arg pr_id (out_gen wit_var x) - | RefArgType -> pr_arg pr_global (out_gen wit_ref x) - | SortArgType -> pr_arg pr_sort (out_gen wit_sort x) - | ConstrArgType -> pr_arg prc (out_gen wit_constr x) - | ConstrMayEvalArgType -> - pr_arg prc (out_gen wit_constr_may_eval x) - | QuantHypArgType -> - pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) + | BoolArgType -> str (if out_gen wit_bool x then "true" else "false") + | IntArgType -> int (out_gen wit_int x) + | IntOrVarArgType -> pr_or_var pr_int (out_gen wit_int_or_var x) + | StringArgType -> str "\"" ++ str (out_gen wit_string x) ++ str "\"" + | PreIdentArgType -> str (out_gen wit_pre_ident x) + | IntroPatternArgType -> pr_intro_pattern (out_gen wit_intro_pattern x) + | IdentArgType -> pr_id (out_gen wit_ident x) + | VarArgType -> pr_id (out_gen wit_var x) + | RefArgType -> pr_global (out_gen wit_ref x) + | SortArgType -> pr_sort (out_gen wit_sort x) + | ConstrArgType -> prc (out_gen wit_constr x) + | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x) + | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) - (out_gen wit_red_expr x) - | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) + pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x) + | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> let (c,b) = out_gen wit_constr_with_bindings x in - pr_arg (pr_with_bindings prc prlc) (c,out_bindings b) + pr_with_bindings prc prlc (c,out_bindings b) | BindingsArgType -> - pr_arg (pr_bindings_no_with prc prlc) - (out_bindings (out_gen wit_bindings x)) - | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) + pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x)) + | List0ArgType _ -> + hov 0 (pr_sequence (pr_generic prc prlc prtac) + (fold_list0 (fun a l -> a::l) x [])) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_generic prc prlc prtac x ++ a) x (mt())) + hov 0 (pr_sequence (pr_generic prc prlc prtac) + (fold_list1 (fun a l -> a::l) x [])) | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac) (mt()) x) | PairArgType _ -> hov 0 - (fold_pair - (fun a b -> pr_generic prc prlc prtac a ++ spc () ++ - pr_generic prc prlc prtac b) + (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac) [a;b]) x) | ExtraArgType s -> try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str " [no printer for " ++ str s ++ str "]" + with Not_found -> str "[no printer for " ++ str s ++ str "]" -let rec pr_tacarg_using_rule pr_gen = function - | Some s :: l, al -> spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | None :: l, a :: al -> pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () +let rec tacarg_using_rule_token pr_gen = function + | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al) + | None :: l, a :: al -> pr_gen a :: tacarg_using_rule_token pr_gen (l,al) + | [], [] -> [] | _ -> failwith "Inconsistent arguments of extended tactic" -let pr_extend_gen prgen lev s l = +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 let tags = List.map genarg_tag l in let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in - let p = pr_tacarg_using_rule prgen (pl,l) in + let p = pr_tacarg_using_rule pr_gen (pl,l) in if lev' > lev then surround p else p with Not_found -> - str s ++ prlist prgen l ++ str " (* Generic printer *)" + str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" let pr_raw_extend prc prlc prtac = pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference) @@ -366,9 +363,22 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) +let pr_with_induction_names = function + | None, None -> mt () + | eqpat, ipat -> + spc () ++ hov 1 (str "as" ++ pr_opt pr_intro_pattern eqpat ++ + pr_opt pr_intro_pattern ipat) + +let pr_as_intro_pattern ipat = + spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) + +let pr_with_inversion_names = function + | None -> mt () + | Some ipat -> pr_as_intro_pattern ipat + let pr_with_names = function - | IntroAnonymous -> mt () - | ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) + | _,IntroAnonymous -> mt () + | ipat -> pr_as_intro_pattern ipat let pr_as_name = function | Anonymous -> mt () @@ -454,7 +464,7 @@ let pr_induction_kind = function | FullInversion -> str "inversion" | FullInversionClear -> str "inversion_clear" -let pr_lazy lz = if lz then str "lazy " else mt () +let pr_lazy lz = if lz then str "lazy" else mt () let pr_match_pattern pr_pat = function | Term a -> pr_pat a @@ -489,8 +499,9 @@ let pr_funvar = function | None -> spc () ++ str "_" | Some id -> spc () ++ pr_id id -let pr_let_clause k pr (id,t) = - hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++ pr (TacArg t)) +let pr_let_clause k pr (id,(bl,t)) = + 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 | hd::tl -> @@ -599,6 +610,10 @@ let pr_intarg n = spc () ++ int n in (* Some printing combinators *) let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in +let extract_binders = function + | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) + | body -> ([],body) in + let pr_binder_fix (nal,t) = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal @@ -644,7 +659,7 @@ let pr_cofix_tac (id,c) = (* Printing tactics as arguments *) let rec pr_atom0 = function | TacIntroPattern [] -> str "intros" - | TacIntroMove (None,None) -> str "intro" + | TacIntroMove (None,hto) when hto = no_move -> str "intro" | TacAssumption -> str "assumption" | TacAnyConstructor (false,None) -> str "constructor" | TacAnyConstructor (true,None) -> str "econstructor" @@ -672,12 +687,10 @@ and pr_atom1 = function 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) - | TacIntroMove (None,None) as t -> pr_atom0 t - | TacIntroMove (Some id1,None) -> str "intro " ++ pr_id id1 - | TacIntroMove (ido1,Some id2) -> - hov 1 - (str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ - pr_lident id2) + | TacIntroMove (None,hto) as t when hto = no_move -> pr_atom0 t + | TacIntroMove (Some id,hto) when hto = no_move -> str "intro " ++ pr_id id + | TacIntroMove (ido,hto) -> + hov 1 (str"intro" ++ pr_opt pr_id ido ++ pr_move_location pr_ident hto) | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) @@ -685,7 +698,7 @@ and pr_atom1 = function | TacApply (a,ev,cb) -> hov 1 ((if a then mt() else str "simple ") ++ str (with_evars ev "apply") ++ spc () ++ - pr_with_bindings cb) + prlist_with_sep pr_coma pr_with_bindings cb) | TacElim (ev,cb,cbo) -> hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) @@ -737,22 +750,17 @@ and pr_atom1 = function ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None))) *) (* Derived basic tactics *) - | TacSimpleInduction h -> - hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) - | TacNewInduction (ev,h,e,ids,cl) -> - hov 1 (str (with_evars ev "induction") ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ - pr_with_names ids ++ - pr_opt pr_eliminator e ++ - pr_opt_no_spc (pr_clauses pr_ident) cl) - | TacSimpleDestruct h -> - hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) - | TacNewDestruct (ev,h,e,ids,cl) -> - hov 1 (str (with_evars ev "destruct") ++ spc () ++ - prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ - pr_with_names ids ++ - pr_opt pr_eliminator e ++ - pr_opt_no_spc (pr_clauses pr_ident) cl) + | TacSimpleInductionDestruct (isrec,h) -> + hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct") + ++ pr_arg pr_quantified_hypothesis h) + | TacInductionDestruct (isrec,ev,l) -> + hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++ + spc () ++ + prlist_with_sep pr_coma (fun (h,e,ids,cl) -> + prlist_with_sep spc (pr_induction_arg pr_lconstr pr_constr) h ++ + pr_with_induction_names ids ++ + pr_opt pr_eliminator e ++ + pr_opt_no_spc (pr_clauses pr_ident) cl) l) | TacDoubleInduction (h1,h2) -> hov 1 (str "double induction" ++ @@ -796,8 +804,8 @@ and pr_atom1 = function (* Rem: only b = true is available for users *) assert b; hov 1 - (str "move" ++ brk (1,1) ++ pr_ident id1 ++ spc () ++ - str "after" ++ brk (1,1) ++ pr_ident id2) + (str "move" ++ brk (1,1) ++ pr_ident id1 ++ + pr_move_location pr_ident id2) | TacRename l -> hov 1 (str "rename" ++ brk (1,1) ++ @@ -852,11 +860,11 @@ and pr_atom1 = function | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ - pr_with_names ids ++ pr_with_constr pr_constr c) + pr_with_inversion_names ids ++ pr_with_constr pr_constr c) | TacInversion (NonDepInversion (k,cl,ids),hyp) -> hov 1 (pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ - pr_with_names ids ++ pr_simple_clause pr_ident cl) + pr_with_inversion_names ids ++ pr_simple_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 ++ @@ -874,6 +882,7 @@ let rec pr_tac inherited tac = str "using " ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> + let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 (pr_let_clauses recflag (pr_tac ltop) llc ++ str " in") ++ fnl () ++ pr_tac (llet,E) u), @@ -886,7 +895,7 @@ let rec pr_tac inherited tac = lrul ++ fnl() ++ str "end"), lmatch - | TacMatchContext (lz,lr,lrul) -> + | TacMatchGoal (lz,lr,lrul) -> hov 0 (pr_lazy lz ++ str (if lr then "match reverse goal with" else "match goal with") ++ prlist diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index e5162dae..e24f666f 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pptactic.mli 9842 2007-05-20 17:44:23Z herbelin $ i*) +(*i $Id: pptactic.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) open Pp open Genarg @@ -78,6 +78,8 @@ val pr_extend : (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> string -> typed_generic_argument list -> std_ppcmds +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 diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ac2adde2..67cd6f72 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 11059 2008-06-06 09:29:20Z herbelin $ *) +(* $Id: ppvernac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Names @@ -403,9 +403,6 @@ 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_lname_lident_constr (oi,bk,a) = - (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ()) - ++ pr_lconstr a in let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l ++ sep ++ pr_constrarg c in @@ -717,8 +714,7 @@ let rec pr_vernac = function | VernacContext l -> hov 1 ( str"Context" ++ spc () ++ str"[" ++ spc () ++ - prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++ - spc () ++ str "]") + pr_and_type_binders_arg l ++ spc () ++ str "]") | VernacDeclareInstance id -> @@ -808,10 +804,7 @@ let rec pr_vernac = function (Global.env()) body in hov 1 - (((*if !Flags.p1 then - (if rc then str "Recursive " else mt()) ++ - str "Tactic Definition " else*) - (* Rec by default *) str "Ltac ") ++ + ((str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> pr_hints local dbnames h pr_constr pr_pattern_expr diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 401ef7fe..3aa51c53 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,7 +10,7 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id: prettyp.ml 10971 2008-05-22 17:12:11Z barras $ *) +(* $Id: prettyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -219,7 +219,7 @@ let pr_located_qualid = function | ModuleType (qid,_) -> str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid) | Undefined qid -> - pr_qualid qid ++ str " is not a defined object" + pr_qualid qid ++ spc () ++ str "not a defined object." let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in @@ -303,7 +303,7 @@ let build_inductive sp tyi = | 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 - let cstrtypes = arities_of_constructors env (sp,tyi) in + let cstrtypes = type_of_constructors env (sp,tyi) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let cstrnames = mip.mind_consnames in @@ -599,12 +599,12 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err_loc (loc,"read_sec_context", str "Unknown section") in + user_err_loc (loc,"read_sec_context", str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> - error "Cannot print the contents of a closed section" + 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 @@ -648,7 +648,7 @@ let print_name ref = print_leaf_entry true (oname,lobj) with Not_found -> errorlabstrm - "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object") + "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") let print_opaque_name qid = let env = Global.env () in @@ -658,7 +658,7 @@ let print_opaque_name qid = if cb.const_body <> None then print_constant_with_infos cst else - error "not a defined constant" + error "Not a defined constant." | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr -> @@ -736,7 +736,8 @@ let index_of_class cl = try fst (class_info cl) with _ -> - errorlabstrm "index_of_class" (pr_class cl ++ str" is not a defined class") + errorlabstrm "index_of_class" + (pr_class cl ++ spc() ++ str "not a defined class.") let print_path_between cls clt = let i = index_of_class cls in @@ -746,7 +747,8 @@ let print_path_between cls clt = lookup_path_between (i,j) with _ -> errorlabstrm "index_cl_of_id" - (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt) + (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt + ++ str ".") in print_path ((i,j),p) diff --git a/parsing/printer.ml b/parsing/printer.ml index 6a19cb0a..b126cc9c 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 11001 2008-05-27 16:56:07Z aspiwack $ *) +(* $Id: printer.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -28,6 +28,7 @@ open Refiner open Pfedit open Ppconstr open Constrextern +open Tacexpr let emacs_str s alts = match !Flags.print_emacs, !Flags.print_emacs_safechar with @@ -318,7 +319,7 @@ let rec pr_evars_int i = function let default_pr_subgoal n = let rec prrec p = function - | [] -> error "No such goal" + | [] -> error "No such goal." | g::rest -> if p = 1 then let pg = default_pr_goal g in @@ -421,14 +422,14 @@ let pr_prim_rule = function | Intro id -> str"intro " ++ pr_id id - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"assert " ++ pr_constr t) - else - (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") + | 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 ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") | FixRule (f,n,[]) -> (str"fix " ++ pr_id f ++ str"/" ++ int n) @@ -472,7 +473,7 @@ let pr_prim_rule = function | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2) + str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) @@ -527,3 +528,14 @@ let pr_assumptionset env s = in (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms) +let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m [] + +open Typeclasses + +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)) + (Gmap.to_list insts) diff --git a/parsing/printer.mli b/parsing/printer.mli index 935fca12..40bb9122 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: printer.mli 11001 2008-05-27 16:56:07Z aspiwack $ i*) +(*i $Id: printer.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Pp @@ -22,6 +22,7 @@ open Termops open Evd open Proof_type open Rawterm +open Tacexpr (*i*) (* These are the entry points for printing terms, context, tac, ... *) @@ -137,3 +138,5 @@ val set_printer_pr : printer_pr -> unit val default_printer_pr : printer_pr +val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t -> + Pp.std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 24562459..a4cfe27a 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*) -(* $Id: q_coqast.ml4 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: q_coqast.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -62,6 +62,10 @@ let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> +let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> + +let mlexpr_of_loc loc = <:expr< $dloc$ >> + let mlexpr_of_by_notation f = function | Genarg.AN x -> <:expr< Genarg.AN $f x$ >> | Genarg.ByNotation (loc,s) -> <:expr< Genarg.ByNotation $dloc$ $str:s$ >> @@ -85,10 +89,6 @@ let mlexpr_of_quantified_hypothesis = function | Rawterm.AnonHyp n -> <:expr< Rawterm.AnonHyp $mlexpr_of_int n$ >> | Rawterm.NamedHyp id -> <:expr< Rawterm.NamedHyp $mlexpr_of_ident id$ >> -let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >> - -let mlexpr_of_loc loc = <:expr< $dloc$ >> - let mlexpr_of_or_var f = function | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >> | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> @@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function let mlexpr_of_binder_kind = function | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >> - | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >> + | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >> let rec mlexpr_of_constr = function | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) -> @@ -242,6 +242,11 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr let mlexpr_of_constr_with_binding = mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind +let mlexpr_of_move_location f = function + | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >> + | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >> + | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >> + let mlexpr_of_induction_arg = function | Tacexpr.ElimOnConstr c -> <:expr< Tacexpr.ElimOnConstr $mlexpr_of_constr_with_binding c$ >> @@ -279,13 +284,13 @@ let mlexpr_of_message_token = function let rec mlexpr_of_atomic_tactic = function (* Basic tactics *) | Tacexpr.TacIntroPattern pl -> - let pl = mlexpr_of_list mlexpr_of_intro_pattern pl in + let pl = mlexpr_of_list (mlexpr_of_located mlexpr_of_intro_pattern) pl in <:expr< Tacexpr.TacIntroPattern $pl$ >> | Tacexpr.TacIntrosUntil h -> <:expr< Tacexpr.TacIntrosUntil $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacIntroMove (idopt,idopt') -> let idopt = mlexpr_of_ident_option idopt in - let idopt'=mlexpr_of_option (mlexpr_of_located mlexpr_of_ident) idopt' in + let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> | Tacexpr.TacAssumption -> <:expr< Tacexpr.TacAssumption >> @@ -296,7 +301,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply (b,false,cb) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_constr_with_binding cb$ >> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in @@ -332,7 +337,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacCut c -> <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> - let ipat = mlexpr_of_intro_pattern ipat in + let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> @@ -348,18 +353,18 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_bool b$ >> (* Derived basic tactics *) - | Tacexpr.TacSimpleInduction h -> - <:expr< Tacexpr.TacSimpleInduction ($mlexpr_of_quantified_hypothesis h$) >> - | Tacexpr.TacNewInduction (false,cl,cbo,ids,cls) -> - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewInduction False $mlexpr_of_list mlexpr_of_induction_arg cl$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> - | Tacexpr.TacSimpleDestruct h -> - <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >> - | Tacexpr.TacNewDestruct (false,c,cbo,ids,cls) -> - let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in - let ids = mlexpr_of_intro_pattern ids in - <:expr< Tacexpr.TacNewDestruct False $mlexpr_of_list mlexpr_of_induction_arg c$ $cbo$ $ids$ $mlexpr_of_option mlexpr_of_clause cls$ >> + | Tacexpr.TacSimpleInductionDestruct (isrec,h) -> + <: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 + (mlexpr_of_list mlexpr_of_induction_arg) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))) + (mlexpr_of_option mlexpr_of_clause)) l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> @@ -371,7 +376,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacMove (dep,id1,id2) -> <:expr< Tacexpr.TacMove $mlexpr_of_bool dep$ $mlexpr_of_hyp id1$ - $mlexpr_of_hyp id2$ >> + $mlexpr_of_move_location mlexpr_of_hyp id2$ >> (* Constructors *) | Tacexpr.TacLeft (ev,l) -> @@ -462,8 +467,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function $mlexpr_of_bool lz$ $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> - | Tacexpr.TacMatchContext (lz,lr,l) -> - <:expr< Tacexpr.TacMatchContext + | Tacexpr.TacMatchGoal (lz,lr,l) -> + <:expr< Tacexpr.TacMatchGoal $mlexpr_of_bool lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index da78e287..da4329bb 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "q_MLast.cmo" i*) -(* $Id: q_util.ml4 10091 2007-08-24 10:57:37Z herbelin $ *) +(* $Id: q_util.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) (* This file defines standard combinators to build ml expressions *) @@ -53,6 +53,11 @@ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in <:expr< ($e1$, $e2$, $e3$) >> +let mlexpr_of_quadruple m1 m2 m3 m4 (a1,a2,a3,a4)= + let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 and e4 = m4 a4 in + let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e4) in + <:expr< ($e1$, $e2$, $e3$, $e4$) >> + (* We don't give location for tactic quotation! *) let loc = dummy_loc diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 901f9198..b950e68f 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: q_util.mli 9265 2006-10-24 08:35:38Z herbelin $ i*) +(*i $Id: q_util.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) val patt_of_expr : MLast.expr -> MLast.patt @@ -20,6 +20,10 @@ val mlexpr_of_triple : ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr) -> 'a * 'b * 'c -> MLast.expr +val mlexpr_of_quadruple : + ('a -> MLast.expr) -> ('b -> MLast.expr) -> + ('c -> MLast.expr) -> ('d -> MLast.expr) -> 'a * 'b * 'c * 'd -> MLast.expr + val mlexpr_of_bool : bool -> MLast.expr val mlexpr_of_int : int -> MLast.expr diff --git a/parsing/search.ml b/parsing/search.ml index c375826c..c6ff4c04 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: search.ml 10840 2008-04-23 21:29:34Z herbelin $ *) +(* $Id: search.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -150,7 +150,7 @@ let rec id_from_pattern = function | PVar id -> Nametab.locate (make_qualid [] (string_of_id id)) *) | PApp (p,_) -> id_from_pattern p - | _ -> error "the pattern is not simple enough" + | _ -> error "The pattern is not simple enough." let raw_pattern_search extra_filter display_function pat = let name = id_from_pattern pat in diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 3d71af84..695677a3 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: tacextend.ml4 10091 2007-08-24 10:57:37Z herbelin $ *) +(* $Id: tacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Genarg @@ -206,7 +206,7 @@ EXTEND let t, g = Q_util.interp_entry_name loc e sep in TacNonTerm (loc, t, g, Some s) | s = STRING -> - if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal"); + if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal."); TacTerm s ] ] ; diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index c5b77774..e0836984 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactic_printer.ml 11146 2008-06-19 08:26:38Z corbinea $ *) +(* $Id: tactic_printer.ml 11313 2008-08-07 11:15:03Z barras $ *) open Pp open Util @@ -90,7 +90,8 @@ let pr_change gl = str"change " ++ pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." -let rec print_decl_script tac_printer nochange sigma pf = +let print_decl_script tac_printer ?(nochange=true) sigma pf = + let rec print_prf pf = match pf.ref with | None -> (if nochange then @@ -99,46 +100,38 @@ let rec print_decl_script tac_printer nochange sigma pf = pr_change pf.goal) ++ fnl () | Some (Daimon,[]) -> str "(* Some proof has been skipped here *)" - | Some (Prim Change_evars,[subpf]) -> - print_decl_script tac_printer nochange sigma subpf + | Some (Prim Change_evars,[subpf]) -> print_prf subpf | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> begin match instr.instr,subprfs with Pescape,[{ref=Some(_,subsubprfs)}] -> hov 7 (pr_rule_dot_fnl rule ++ - prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++ - if opened then mt () else str "return." + prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++ + if opened then mt () else str "return." | Pclaim _,[body;cont] -> - hov 2 - (pr_rule_dot_fnl rule ++ - print_decl_script tac_printer nochange sigma body) ++ - fnl () ++ - if opened then mt () else str "end claim." ++ fnl () ++ - print_decl_script tac_printer nochange sigma cont + hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++ + (if opened then mt () else str "end claim." ++ fnl ()) ++ + print_prf cont | Pfocus _,[body;cont] -> - hov 2 - (pr_rule_dot_fnl rule ++ - print_decl_script tac_printer nochange sigma body) ++ - fnl () ++ - if opened then mt () else str "end focus." ++ fnl () ++ - print_decl_script tac_printer nochange sigma cont + 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_decl_script tac_printer nochange sigma body) ++ - fnl () ++ - print_decl_script tac_printer nochange sigma cont + hov 2 (pr_rule_dot_fnl rule ++ print_prf body) ++ fnl () ++ + print_prf cont | _,[next] -> - pr_rule_dot_fnl rule ++ - print_decl_script tac_printer nochange sigma next + pr_rule_dot_fnl rule ++ print_prf next | _,[] -> pr_rule_dot rule | _,_ -> anomaly "unknown branching instruction" end - | _ -> anomaly "Not Applicable" + | _ -> anomaly "Not Applicable" in + print_prf pf -let rec print_script nochange sigma pf = +let print_script ?(nochange=true) sigma pf = + let rec print_prf pf = match pf.ref with | None -> (if nochange then @@ -153,26 +146,25 @@ let rec print_script nochange sigma pf = end ++ begin hov 0 (str "proof." ++ fnl () ++ - print_decl_script (print_script nochange sigma) - nochange sigma (List.hd script)) + print_decl_script print_prf + ~nochange sigma (List.hd script)) end ++ fnl () ++ begin if opened then mt () else (str "end proof." ++ fnl ()) end | Some(Daimon,spfl) -> ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - prlist_with_sep pr_fnl - (print_script nochange sigma) spfl ) + prlist_with_sep pr_fnl print_prf spfl ) | Some(rule,spfl) -> ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ pr_rule_dot_fnl rule ++ - prlist_with_sep pr_fnl - (print_script nochange sigma) spfl ) + prlist_with_sep pr_fnl print_prf spfl ) in + print_prf pf (* printed by Show Script command *) -let print_treescript nochange sigma pf = - let rec aux pf = +let print_treescript ?(nochange=true) sigma pf = + let rec print_prf pf = match pf.ref with | None -> if nochange then @@ -184,23 +176,21 @@ let print_treescript nochange 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 aux - nochange sigma (List.hd script) + print_decl_script print_prf ~nochange sigma (List.hd script) end ++ fnl () ++ - begin - if opened then mt () else (str "end proof." ++ fnl ()) - end + begin + if opened then mt () else (str "end proof." ++ fnl ()) + end | Some(Daimon,spfl) -> - ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - prlist_with_sep pr_fnl - (print_script nochange sigma) spfl ) + (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++ + prlist_with_sep pr_fnl (print_script ~nochange sigma) spfl | Some(r,spfl) -> let indent = if List.length spfl >= 2 then 1 else 0 in - (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - hv indent (pr_rule_dot_fnl r ++ prlist_with_sep mt aux spfl) - in hov 0 (aux pf) + (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++ + hv indent (pr_rule_dot_fnl r ++ prlist_with_sep fnl print_prf spfl) + in hov 0 (print_prf pf) let rec print_info_script sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 676dbdf2..affc5ec2 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactic_printer.mli 10580 2008-02-22 13:39:13Z lmamane $ i*) +(*i $Id: tactic_printer.mli 11313 2008-08-07 11:15:03Z barras $ i*) (*i*) open Pp @@ -23,6 +23,6 @@ val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expr -> std_ppcmds val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds val print_script : - bool -> evar_map -> proof_tree -> std_ppcmds + ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds val print_treescript : - bool -> evar_map -> proof_tree -> std_ppcmds + ?nochange:bool -> evar_map -> proof_tree -> std_ppcmds diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index d12ca098..08feb17a 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: vernacextend.ml4 10091 2007-08-24 10:57:37Z herbelin $ *) +(* $Id: vernacextend.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Genarg @@ -110,7 +110,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"); + if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty."); (s,l,<:expr< fun () -> $e$ >>) ] ] ; -- cgit v1.2.3