From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- parsing/argextend.ml4 | 8 +- parsing/egrammar.ml | 8 +- parsing/g_ascii_syntax.ml | 2 +- parsing/g_constr.ml4 | 19 ++- parsing/g_ltac.ml4 | 4 +- parsing/g_proofs.ml4 | 4 +- parsing/g_tactic.ml4 | 24 ++- parsing/g_vernac.ml4 | 25 ++- parsing/g_xml.ml4 | 91 +++++++---- parsing/lexer.ml4 | 381 ++++++++++++++++++++++++++++------------------ parsing/pcoq.ml4 | 53 ++++++- parsing/pcoq.mli | 41 ++++- parsing/ppconstr.ml | 37 +++-- parsing/ppconstr.mli | 11 +- parsing/pptactic.ml | 350 +++++++++++++++++++++++------------------- parsing/ppvernac.ml | 40 +++-- parsing/prettyp.ml | 8 +- parsing/printer.ml | 9 +- parsing/printer.mli | 7 +- parsing/q_coqast.ml4 | 28 ++-- parsing/tacextend.ml4 | 8 +- 21 files changed, 711 insertions(+), 447 deletions(-) (limited to 'parsing') diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 650afe17..ec3c2c9c 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: argextend.ml4 7739 2005-12-26 17:08:16Z herbelin $ *) +(* $Id: argextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *) open Genarg open Q_util @@ -30,7 +30,6 @@ let rec make_rawwit loc = function | ConstrArgType -> <:expr< Genarg.rawwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> - | TacticArgType n -> <:expr< Genarg.rawwit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> @@ -56,7 +55,6 @@ let rec make_globwit loc = function | SortArgType -> <:expr< Genarg.globwit_sort >> | ConstrArgType -> <:expr< Genarg.globwit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> - | TacticArgType n -> <:expr< Genarg.globwit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> @@ -82,7 +80,6 @@ let rec make_wit loc = function | SortArgType -> <:expr< Genarg.wit_sort >> | ConstrArgType -> <:expr< Genarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | TacticArgType n -> <:expr< Genarg.wit_tactic $mlexpr_of_int n$ >> | RedExprArgType -> <:expr< Genarg.wit_red_expr >> | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >> | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> @@ -193,6 +190,9 @@ let rec interp_entry_name loc s = OptArgType t, <:expr< Gramext.Sopt $g$ >> else let t, se = + if tactic_genarg_level s <> None then + Some (ExtraArgType s), <:expr< Tactic. tactic >> + else match Pcoq.entry_type (Pcoq.get_univ "prim") s with | Some _ as x -> x, <:expr< Prim. $lid:s$ >> | None -> diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index c723175c..9ec7c532 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml 7762 2005-12-30 10:55:33Z herbelin $ *) +(* $Id: egrammar.ml 8926 2006-06-08 20:23:17Z herbelin $ *) open Pp open Util @@ -160,7 +160,7 @@ type grammar_tactic_production = let make_prod_item = function | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None) - | TacNonTerm (_,(nont,t), po) -> (nont, option_app (fun p -> (p,t)) po) + | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po) (* Tactic grammar extensions *) @@ -210,7 +210,7 @@ let rec interp_entry_name up_level u s = else try let i = find_index "tactic" s in - TacticArgType i, + ExtraArgType s, if i=up_level then Gramext.Sself else if i=up_level-1 then Gramext.Snext else Gramext.Snterml(Pcoq.Gram.Entry.obj Tactic.tactic_expr,string_of_int i) @@ -232,7 +232,7 @@ let make_vprod_item n univ = function | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None) | VNonTerm (loc, nt, po) -> let (etyp, e) = interp_entry_name n univ nt in - e, option_app (fun p -> (p,etyp)) po + e, option_map (fun p -> (p,etyp)) po let get_tactic_entry n = if n = 0 then diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml index e6324e00..ac54fc63 100644 --- a/parsing/g_ascii_syntax.ml +++ b/parsing/g_ascii_syntax.ml @@ -72,7 +72,7 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = option_app make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9f7f7304..9ee312ff 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_constr.ml4 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: g_constr.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) open Pcoq open Constr @@ -28,7 +28,7 @@ let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw let mk_cast = function (c,(_,None)) -> c - | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, DEFAULTcast,ty) + | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv DEFAULTcast, ty) let mk_lam = function ([],c) -> c @@ -59,14 +59,13 @@ let rec mkCLambdaN loc bll c = let rec index_and_rec_order_of_annot loc bl ann = match names_of_local_assums bl,ann with - | [_], (None, r) -> 0, r + | [_], (None, r) -> Some 0, r | lids, (Some x, ro) -> let ids = List.map snd lids in - (try list_index (snd x) ids - 1, ro + (try Some (list_index (snd x) ids - 1), ro with Not_found -> user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable")) - | _ -> user_err_loc(loc,"index_of_annot", - Pp.str "cannot guess decreasing argument of fix") + | _, (None, r) -> None, r let mk_fixb (id,bl,ann,body,(loc,tyc)) = let n,ro = index_and_rec_order_of_annot (fst id) bl ann in @@ -76,7 +75,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = (snd id,(n,ro),bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = - let _ = option_app (fun (aloc,_) -> + let _ = option_map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression")) (fst ann) in @@ -156,8 +155,8 @@ GEXTEND Gram [ "200" RIGHTA [ c = binder_constr -> c ] | "100" RIGHTA - [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1,DEFAULTcast,c2) - | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,DEFAULTcast,c2) ] + [ c1 = operconstr; ":"; c2 = binder_constr -> CCast(loc,c1, CastConv DEFAULTcast,c2) + | c1 = operconstr; ":"; c2 = SELF -> CCast(loc,c1,CastConv DEFAULTcast,c2) ] | "99" RIGHTA [ ] | "90" RIGHTA [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) @@ -321,7 +320,7 @@ GEXTEND Gram | "("; id=name; ":="; c=lconstr; ")" -> LocalRawDef (id,c) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,DEFAULTcast,t)) + LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv DEFAULTcast,t)) ] ] ; binder: diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 6ed22c7e..eaa51810 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltac.ml4 8129 2006-03-05 09:05:12Z herbelin $ *) +(* $Id: g_ltac.ml4 8878 2006-05-30 16:44:25Z herbelin $ *) open Pp open Util @@ -23,7 +23,7 @@ type let_clause_kind = | LETCLAUSE of (Names.identifier Util.located * raw_tactic_expr option * raw_tactic_arg) -let fail_default_value = Genarg.ArgArg 0 +let fail_default_value = ArgArg 0 let out_letin_clause loc = function | LETTOPCLAUSE _ -> user_err_loc (loc, "", (str "Syntax Error")) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 886b33e2..94205fa8 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_proofs.ml4 7936 2006-01-28 18:36:54Z herbelin $ *) +(* $Id: g_proofs.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) open Pcoq open Pp @@ -117,6 +117,6 @@ GEXTEND Gram ; constr_body: [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ] + | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Rawterm.CastConv Term.DEFAULTcast,t) ] ] ; END diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 1974d8bc..cba2e7d0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_tactic.ml4 8651 2006-03-21 21:54:43Z jforest $ *) +(* $Id: g_tactic.ml4 8878 2006-05-30 16:44:25Z herbelin $ *) open Pp open Pcoq @@ -102,7 +102,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = option_app (fun (aloc,_) -> + let _ = option_map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", Pp.str"Annotation forbidden in cofix expression")) ann in @@ -121,8 +121,8 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Genarg.ArgArg n - | id = identref -> Genarg.ArgVar id ] ] + [ [ n = integer -> Rawterm.ArgArg n + | id = identref -> Rawterm.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -155,11 +155,11 @@ GEXTEND Gram conversion: [ [ c = constr -> (None, c) | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2) - | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr -> + | c1 = constr; "at"; nl = LIST1 int_or_var; "with"; c2 = constr -> (Some (nl,c1), c2) ] ] ; occurrences: - [ [ "at"; nl = LIST1 integer -> nl + [ [ "at"; nl = LIST1 int_or_var -> nl | -> [] ] ] ; pattern_occ: @@ -240,7 +240,7 @@ GEXTEND Gram ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ] + [ [ (id,l)=hypident; occs=occurrences -> ((occs,id),l) ] ] ; clause: [ [ "in"; "*"; occs=occurrences -> @@ -261,6 +261,11 @@ GEXTEND Gram [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + orient: + [ [ "->" -> true + | "<-" -> false + | -> true ]] + ; fixdecl: [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] @@ -285,7 +290,8 @@ GEXTEND Gram [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ] ; by_tactic: - [ [ IDENT "by"; tac = tactic -> TacComplete tac | -> TacId [] ] ] + [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac + | -> TacId [] ] ] ; simple_tactic: [ [ @@ -411,6 +417,8 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) + | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> + TacRewrite (b,c,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18a424a8..7405ae54 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_vernac.ml4 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: g_vernac.ml4 8929 2006-06-08 22:35:58Z herbelin $ *) (*i camlp4deps: "parsing/grammar.cma" i*) open Pp @@ -218,16 +218,15 @@ GEXTEND Gram let ni = match fst annot with Some id -> - (try list_index (Name id) names - 1 - with Not_found -> Util.user_err_loc - (loc,"Fixpoint", - Pp.str "No argument named " ++ Nameops.pr_id id)) + (try Some (list_index (Name id) names - 1) + with Not_found -> Util.user_err_loc + (loc,"Fixpoint", + Pp.str "No argument named " ++ Nameops.pr_id id)) | None -> - if List.length names > 1 then - Util.user_err_loc - (loc,"Fixpoint", - Pp.str "the recursive argument needs to be specified"); - 0 in + (* If there is only one argument, it is the recursive one, + otherwise, we search the recursive index later *) + if List.length names = 1 then Some 0 else None + in ((id, (ni, snd annot), bl, type_, def),ntn) ] ] ; corec_definition: @@ -320,8 +319,8 @@ GEXTEND Gram VernacDeclareModuleType (id, bl, mty_o) | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; mty_o = of_module_type -> - VernacDeclareModule (export, id, bl, mty_o) + bl = LIST0 module_binder; ":"; mty = module_type -> + VernacDeclareModule (export, id, bl, (mty,true)) (* Section beginning *) | IDENT "Section"; id = identref -> VernacBeginSection id | IDENT "Chapter"; id = identref -> VernacBeginSection id @@ -430,7 +429,7 @@ GEXTEND Gram (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = global; pos = OPT [ "["; l = LIST0 ident; "]" -> l ] -> - let pos = option_app (List.map (fun id -> ExplByName id)) pos in + let pos = option_map (List.map (fun id -> ExplByName id)) pos in VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index b4580750..5ad0193b 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_xml.ml4 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: g_xml.ml4 8875 2006-05-29 19:59:11Z msozeau $ *) open Pp open Util @@ -19,6 +19,7 @@ open Tacexpr open Libnames open Nametab +open Detyping (* Generic xml parser without raw data *) @@ -83,7 +84,7 @@ let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a) let inductive_of_cdata a = match global_of_cdata a with | IndRef (kn,_) -> kn - | _ -> failwith "kn" + | _ -> anomaly "XML parser: not an inductive" let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) @@ -95,7 +96,9 @@ let sort_of_cdata (loc,a) = match a with let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al) -let get_xml_inductive_kn al = inductive_of_cdata (get_xml_attr "uri" al) +let get_xml_inductive_kn al = + inductive_of_cdata (* uriType apparent synonym of uri *) + (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al) let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al) @@ -105,43 +108,66 @@ let get_xml_inductive al = let get_xml_constructor al = (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) -let get_xml_name al = +let get_xml_binder al = try Name (ident_of_cdata (List.assoc "binder" al)) with Not_found -> Anonymous let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) +let get_xml_name al = ident_of_cdata (get_xml_attr "name" al) + let get_xml_noFun al = nmtoken (get_xml_attr "noFun" al) +let get_xml_no al = nmtoken (get_xml_attr "no" al) + +(* A leak in the xml dtd: arities of constructor need to know global env *) + +let compute_branches_lengths ind = + let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + mip.Declarations.mind_consnrealdecls + +let compute_inductive_nargs ind = + Inductiveops.inductive_nargs (Global.env()) ind + (* Interpreting constr as a rawconstr *) let rec interp_xml_constr = function | XmlTag (loc,"REL",al,[]) -> RVar (loc, get_xml_ident al) - | XmlTag (loc,"VAR",al,[]) -> failwith "" - | XmlTag (loc,"LAMBDA",al,[x1;x2]) -> - let na,t = interp_xml_decl x1 in - RLambda (loc, na, t, interp_xml_target x2) - | XmlTag (loc,"PROD",al,[x1;x2]) -> - let na,t = interp_xml_decl x1 in - RProd (loc, na, t, interp_xml_target x2) + | 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 + let ctx = List.map interp_xml_decl decls in + List.fold_right (fun (na,t) b -> RLambda (loc, na, t, b)) + ctx (interp_xml_target body) + | XmlTag (loc,"PROD",al,(_::_ as xl)) -> + let body,decls = list_sep_last xl in + let ctx = List.map interp_xml_decl decls in + List.fold_right (fun (na,t) b -> RProd (loc, na, t, b)) + ctx (interp_xml_target body) | XmlTag (loc,"LETIN",al,[x1;x2]) -> let na,t = interp_xml_def x1 in RLetIn (loc, na, t, interp_xml_target x2) | XmlTag (loc,"APPLY",_,x::xl) -> RApp (loc, interp_xml_constr x, List.map interp_xml_constr xl) + | XmlTag (loc,"instantiate",_, + (XmlTag (_,("CONST"|"MUTIND"|"MUTCONSTRUCT"),_,_) as x)::xl) -> + RApp (loc, interp_xml_constr x, List.map interp_xml_arg xl) | XmlTag (loc,"META",al,xl) -> - failwith "META: TODO" + REvar (loc, get_xml_no al, Some (List.map interp_xml_substitution xl)) | XmlTag (loc,"CONST",al,[]) -> RRef (loc, ConstRef (get_xml_constant al)) - | XmlTag (loc,"MUTCASE",al,x::y::yl) -> (* BUGGE *) - failwith "XML MUTCASE TO DO"; -(* - ROrderedCase (loc,RegularStyle,Some (interp_xml_patternsType x), - interp_xml_inductiveTerm y, - Array.of_list (List.map interp_xml_pattern yl), - ref None) -*) + | XmlTag (loc,"MUTCASE",al,x::y::yl) -> + let ind = get_xml_inductive al in + let p = interp_xml_patternsType x in + let tm = interp_xml_inductiveTerm y in + let brs = List.map interp_xml_pattern yl in + let brns = Array.to_list (compute_branches_lengths ind) in + let mat = simple_cases_matrix_of_branches ind brns brs in + let nparams,n = compute_inductive_nargs ind in + let nal,rtn = return_type_of_predicate ind nparams n p in + RCases (loc,rtn,[tm,nal],mat) | XmlTag (loc,"MUTIND",al,[]) -> RRef (loc, IndRef (get_xml_inductive al)) | XmlTag (loc,"MUTCONSTRUCT",al,[]) -> @@ -149,12 +175,13 @@ let rec interp_xml_constr = function | XmlTag (loc,"FIX",al,xl) -> let li,lnct = List.split (List.map interp_xml_FixFunction xl) in let ln,lc,lt = list_split3 lnct in - RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) + let lctx = List.map (fun _ -> []) ln in + RRec (loc, RFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt) | XmlTag (loc,"COFIX",al,xl) -> let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in RRec (loc, RCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt) | XmlTag (loc,"CAST",al,[x1;x2]) -> - RCast (loc, interp_xml_term x1, DEFAULTcast, interp_xml_type x2) + 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) @@ -177,10 +204,13 @@ and interp_xml_body x = interp_xml_constr_alias "body" x and interp_xml_pattern x = interp_xml_constr_alias "pattern" x and interp_xml_patternsType x = interp_xml_constr_alias "patternsType" x and interp_xml_inductiveTerm x = interp_xml_constr_alias "inductiveTerm" x +and interp_xml_arg x = interp_xml_constr_alias "arg" x +and interp_xml_substitution x = interp_xml_constr_alias "substitution" x + (* no support for empty substitution from official dtd *) and interp_xml_decl_alias s x = match interp_xml_tag s x with - | (_,al,[x]) -> (get_xml_name al, interp_xml_constr x) + | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x) | (loc,_,_) -> user_err_loc (loc,"",str "wrong number of arguments (expect one)") @@ -201,23 +231,22 @@ and interp_xml_recursionOrder x = | _ -> user_err_loc (locs,"",str "invalid recursion order") - and interp_xml_FixFunction x = match interp_xml_tag "FixFunction" x with - | (loc,al,[x1;x2;x3]) -> - ((nmtoken (get_xml_attr "recIndex" al), + | (loc,al,[x1;x2;x3]) -> (* Not in official cic.dtd, not in constr *) + ((Some (nmtoken (get_xml_attr "recIndex" al)), interp_xml_recursionOrder x1), - (get_xml_ident al, interp_xml_type x2, interp_xml_body x3)) - | (loc,al,[x1;x2]) -> (* For backwards compatibility *) - ((nmtoken (get_xml_attr "recIndex" al), RStructRec), - (get_xml_ident al, interp_xml_type x1, interp_xml_body x2)) + (get_xml_name al, interp_xml_type x2, interp_xml_body x3)) + | (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)") and interp_xml_CoFixFunction x = match interp_xml_tag "CoFixFunction" x with | (loc,al,[x1;x2]) -> - (get_xml_ident al, interp_xml_type x1, interp_xml_body 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)") diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 6119b86e..c02dc59b 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 7870 2006-01-15 20:29:09Z herbelin $ i*) +(*i $Id: lexer.ml4 8924 2006-06-08 17:49:01Z notin $ i*) open Pp open Token @@ -54,7 +54,7 @@ let ttree_find ttree str = in proc_rec ttree 0 -(* Lexer conventions on tokens *) +(* Errors occuring while lexing (explained as "Lexer error: ...") *) type error = | Illegal_character @@ -65,8 +65,163 @@ type error = exception Error of error +let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str) + let bad_token str = raise (Error (Bad_token str)) +(* Lexer conventions on tokens *) + +type utf8_token = + Utf8Letter of int | Utf8IdentPart of int | Utf8Symbol | AsciiChar + +let error_unsupported_unicode_character n cs = + let bp = Stream.count cs in + err (bp,bp+n) (Bad_token "Unsupported Unicode character") + +let error_utf8 cs = + let bp = Stream.count cs in + err (bp, bp+1) Illegal_character + +let njunk n = Util.repeat n Stream.junk + +let check_utf8_trailing_byte cs c = + if Char.code c land 0xC0 <> 0x80 then error_utf8 cs + +(* Recognize utf8 blocks (of length less than 4 bytes) *) +(* 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 + else + let n, unicode = + if c1 land 0x20 = 0 then + match Stream.npeek 2 cs with + | [_;c2] -> + check_utf8_trailing_byte cs c2; + 2, (c1 land 0x1F) lsl 6 + (Char.code c2 land 0x3F) + | _ -> error_utf8 cs + else if c1 land 0x10 = 0 then + 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 + + (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; + 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 + match unicode land 0x1F000 with + | 0x0 -> + begin match unicode with + (* utf-8 Latin-1 non breaking space U00A0 *) + | 0x00A0 -> Utf8Letter n + (* utf-8 Latin-1 symbols U00A1-00BF *) + | x when 0x00A0 <= x & x <= 0x00BF -> Utf8Symbol + (* utf-8 Latin-1 letters U00C0-00D6 *) + | x when 0x00C0 <= x & x <= 0x00D6 -> Utf8Letter n + (* utf-8 Latin-1 symbol U00D7 *) + | 0x00D7 -> Utf8Symbol + (* utf-8 Latin-1 letters U00D8-00F6 *) + | x when 0x00D8 <= x & x <= 0x00F6 -> Utf8Letter n + (* utf-8 Latin-1 symbol U00F7 *) + | 0x00F7 -> Utf8Symbol + (* utf-8 Latin-1 letters U00F8-00FF *) + | x when 0x00F8 <= x & x <= 0x00FF -> Utf8Letter n + (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *) + | x when 0x0100 <= x & x <= 0x0241 -> Utf8Letter n + (* utf-8 Phonetic letters U0250-02AF *) + | x when 0x0250 <= x & x <= 0x02AF -> Utf8Letter n + (* utf-8 what do to with diacritics U0300-U036F ? *) + (* utf-8 Greek letters U0380-03FF *) + | x when 0x0380 <= x & x <= 0x03FF -> Utf8Letter n + (* utf-8 Cyrillic letters U0400-0481 *) + | x when 0x0400 <= x & x <= 0x0481 -> Utf8Letter n + (* utf-8 Cyrillic symbol U0482 *) + | 0x0482 -> Utf8Symbol + (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *) + (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *) + | x when 0x048A <= x & x <= 0x04F9 -> Utf8Letter n + (* utf-8 Cyrillic supplements letters U0500-U050F *) + | x when 0x0500 <= x & x <= 0x050F -> Utf8Letter n + (* utf-8 Hebrew letters U05D0-05EA *) + | x when 0x05D0 <= x & x <= 0x05EA -> Utf8Letter n + (* utf-8 Hebrew letters U0621-064A *) + | x when 0x0621 <= x & x <= 0x064A -> Utf8Letter n + | _ -> error_unsupported_unicode_character n cs + end + | 0x1000 -> + begin match unicode with + (* utf-8 Georgian U10A0-10FF (has holes) *) + | x when 0x10A0 <= x & x <= 0x10FF -> Utf8Letter n + (* utf-8 Hangul Jamo U1100-11FF (has holes) *) + | x when 0x1100 <= x & x <= 0x11FF -> Utf8Letter n + (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *) + | x when 0x1E00 <= x & x <= 0x1E9B -> Utf8Letter n + | x when 0x1EA0 <= x & x <= 0x1EF9 -> Utf8Letter n + | _ -> error_unsupported_unicode_character n cs + end + | 0x2000 -> + begin match unicode with + (* utf-8 general punctuation U2080-2089 *) + (* Hyphens *) + | x when 0x2010 <= x & x <= 0x2011 -> Utf8Letter n + (* Dashes and other symbols *) + | x when 0x2012 <= x & x <= 0x2027 -> Utf8Symbol + (* Per mille and per ten thousand signs *) + | x when 0x2030 <= x & x <= 0x2031 -> Utf8Symbol + (* Prime letters *) + | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> Utf8IdentPart n + (* Miscellaneous punctuation *) + | x when 0x2039 <= x & x <= 0x2056 -> Utf8Symbol + | x when 0x2058 <= x & x <= 0x205E -> Utf8Symbol + (* Invisible mathematical operators *) + | x when 0x2061 <= x & x <= 0x2063 -> Utf8Symbol + + (* utf-8 subscript U2080-2089 *) + | x when 0x2080 <= x & x <= 0x2089 -> Utf8IdentPart n + (* utf-8 letter-like U2100-214F *) + | x when 0x2100 <= x & x <= 0x214F -> Utf8Letter n + (* utf-8 number-forms U2153-2183 *) + | x when 0x2153 <= x & x <= 0x2183 -> Utf8Symbol + (* utf-8 arrows A U2190-21FF *) + (* utf-8 mathematical operators U2200-22FF *) + (* utf-8 miscellaneous technical U2300-23FF *) + | x when 0x2190 <= x & x <= 0x23FF -> Utf8Symbol + (* utf-8 box drawing U2500-257F has ceiling, etc. *) + (* utf-8 block elements U2580-259F *) + (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *) + (* utf-8 miscellaneous symbols U2600-26FF *) + | x when 0x2500 <= x & x <= 0x26FF -> Utf8Symbol + (* utf-8 arrows B U2900-297F *) + | x when 0x2900 <= x & x <= 0x297F -> Utf8Symbol + (* utf-8 mathematical operators U2A00-2AFF *) + | x when 0x2A00 <= x & x <= 0x2AFF -> Utf8Symbol + | _ -> error_unsupported_unicode_character n cs + end + | _ -> + begin match unicode with + (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *) + | x when 0x3040 <= x & x <= 0x30FF -> Utf8Letter n + (* utf-8 Unified CJK Ideographs U4E00-9FA5 *) + | x when 0x4E00 <= x & x <= 0x9FA5 -> Utf8Letter n + (* utf-8 Hangul syllables UAC00-D7AF *) + | x when 0xAC00 <= x & x <= 0xD7AF -> Utf8Letter n + (* utf-8 Gothic U10330-1034A *) + | x when 0x10330 <= x & x <= 0x1034A -> Utf8Letter n + | _ -> error_unsupported_unicode_character n cs + end + +let lookup_utf8 cs = + match Stream.peek cs with + | Some ('\x00'..'\x7F') -> Some AsciiChar + | Some ('\x80'..'\xFF' as c) -> Some (lookup_utf8_tail c cs) + | None -> None + let check_special_token str = let rec loop_symb = parser | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str @@ -76,35 +231,19 @@ let check_special_token str = loop_symb (Stream.of_string str) let check_ident str = - let first_letter = function - (''' | '0'..'9') -> false - | _ -> true in - let rec loop_id = parser - | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_'); s >] -> - loop_id s - (* utf-8 Greek letters U0380-03FF *) - | [< ' ('\xCE' | '\xCF'); ' ('\x80'..'\xBF'); s >] -> loop_id s - | [< ''\xE2'; 'c2; 'c3; s >] -> - (match c2, c3 with - (* utf-8 letter-like U2100-214F *) - | ( ('\x84', '\x80'..'\xBF') - | ('\x85', '\x80'..'\x8F') - (* utf-8 subscript U2080-2089 *) - | ('\x82', '\x80'..'\x89')) -> - loop_id s - (* utf-8 symbols (see [parse_226_tail]) *) - | (('\x86'..'\x8F' | '\x94'..'\x9B' - | '\xA4'..'\xA5' | '\xA8'..'\xAB'),_) -> - bad_token str - | _ -> - bad_token str) - | [< _ = Stream.empty >] -> () - | [< >] -> bad_token str + let rec loop_id intail = parser + | [< ' ('$' | 'a'..'z' | 'A'..'Z' | '_'); s >] -> + loop_id true s + | [< ' ('0'..'9' | ''') when intail; s >] -> + loop_id true s + | [< s >] -> + match lookup_utf8 s with + | Some (Utf8Letter n) -> njunk n s; loop_id true s + | Some (Utf8IdentPart n) when intail -> njunk n s; loop_id true s + | Some _ -> bad_token str + | None -> () in - if String.length str > 0 && first_letter str.[0] then - loop_id (Stream.of_string str) - else - bad_token str + loop_id false (Stream.of_string str) let check_keyword str = try check_special_token str @@ -145,9 +284,6 @@ let init () = let _ = init() -(* Errors occuring while lexing (explained as "Lexer error: ...") *) -let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str) - (* The string buffering machinery *) let buff = ref (String.create 80) @@ -158,36 +294,20 @@ let store len x = !buff.[len] <- x; succ len -let mstore len s = - let rec add_rec len i = - if i == String.length s then len else add_rec (store len s.[i]) (succ i) - in - add_rec len 0 +let rec nstore n len cs = + if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len let get_buff len = String.sub !buff 0 len - (* The classical lexer: idents, numbers, quoted strings, comments *) let rec ident_tail len = parser | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> ident_tail (store len c) s - (* utf-8 Greek letters U0380-03FF *) - | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2) ; s >] -> - ident_tail (store (store len c1) c2) s | [< s >] -> - match Stream.peek s with - | Some '\xE2' -> - (match List.tl (Stream.npeek 3 s) with - (* utf-8 subscript U2080-2089 *) - | ['\x82' as c2; ('\x80'..'\x89' as c3)] - (* utf-8 letter-like U2100-214F part 1 *) - | ['\x84' as c2; ('\x80'..'\xBF' as c3)] - (* utf-8 letter-like U2100-214F part 2 *) - | ['\x85' as c2; ('\x80'..'\x8F' as c3)] -> - Stream.junk s; Stream.junk s; Stream.junk s; - ident_tail (store (store (store len '\xE2') c2) c3) s - | _ -> len) + match lookup_utf8 s with + | Some (Utf8IdentPart n | Utf8Letter n) -> + ident_tail (nstore n len s) s | _ -> len let rec number len = parser @@ -292,89 +412,61 @@ let rec comment bp = parser bp2 (* Parse a special token, using the [token_tree] *) -let progress_special c = function - | None -> None - | Some tt -> try Some (CharMap.find c tt.branch) with Not_found -> None - -let rec special tt cs = match tt with - | None -> None - | Some tt -> - match - match Stream.peek cs with - | Some c -> - (try Some (CharMap.find c tt.branch) with Not_found -> None) - | None -> None - with - | Some _ as tt' -> Stream.junk cs; special tt' cs - | None -> tt.node - +(* 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 = + 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 + with Not_found -> + tt.node + +and progress_from_byte nr 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 + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> + error_utf8 cs + +(* Must be a special token *) let process_chars bp c cs = - let t = - try special (Some (CharMap.find c !token_tree.branch)) cs - with Not_found -> !token_tree.node - in + let t = progress_from_byte 1 !token_tree cs c in let ep = Stream.count cs in match t with | Some t -> (("", t), (bp, ep)) | None -> err (bp, ep) Undefined_token -type token_226_tail = - | TokSymbol of string option - | TokIdent of string - -(* 1110xxxx 10yyyyzz 10zztttt utf-8 codes for xxxx=0010 *) -let parse_226_tail tk = parser - | [< ''\x82' as c2; ' ('\x80'..'\x89' as c3); - (* utf-8 subscript U2080-2089 *) - len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] -> - TokIdent (get_buff len) - | [< ''\x84' as c2; ' ('\x80'..'\xBF' as c3); - (* utf-8 letter-like U2100-214F part 1 *) - len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] -> - TokIdent (get_buff len) - | [< ''\x85' as c2; ' ('\x80'..'\x8F' as c3); - (* utf-8 letter-like U2100-214F part 2 *) - len = ident_tail (store (store (store 0 '\xE2') c2) c3) >] -> - TokIdent (get_buff len) - | [< ' ('\x86'..'\x8F' | '\x94'..'\x9B' | '\xA4'..'\xA5' - | '\xA8'..'\xAB' as c2); 'c3; - (* utf-8 arrows A U2190-21FF *) - (* utf-8 mathematical operators U2200-22FF *) - (* utf-8 miscellaneous technical U2300-23FF *) - (* utf-8 box drawing U2500-257F has ceiling, etc. *) - (* utf-8 block elements U2580-259F *) - (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *) - (* utf-8 miscellaneous symbols U2600-26FF *) - (* utf-8 arrows B U2900-297F *) - (* utf-8 mathematical operators U2A00-2AFF *) - t = special (progress_special c3 (progress_special c2 - (progress_special '\xE2' tk))) >] -> - TokSymbol t - | [< '_; '_ >] -> - (* Unsupported utf-8 code *) - TokSymbol None - (* Parse what follows a dot *) let parse_after_dot bp c = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c) >] -> - ("FIELD", get_buff len) - (* utf-8 Greek letters U0380-03FF *) - | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2); - len = ident_tail (store (store 0 c1) c2) >] -> + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> ("FIELD", get_buff len) - (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *) - | [< ''\xE2'; t = parse_226_tail - (progress_special '.' (Some !token_tree)) >] ep -> - (match t with - | TokSymbol (Some t) -> ("", t) - | TokSymbol None -> err (bp, ep) Undefined_token - | TokIdent t -> ("FIELD", t)) - | [< (t,_) = process_chars bp c >] -> t - + | [< s >] -> + match lookup_utf8 s with + | Some (Utf8Letter n) -> + ("FIELD", get_buff (ident_tail (nstore n 0 s) s)) + | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None -> + fst (process_chars bp c s) (* Parse a token in a char stream *) - let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s @@ -383,27 +475,13 @@ let rec next_token = parser bp (("METAIDENT", get_buff len), (bp,ep)) | [< ''.' as c; t = parse_after_dot bp c >] ep -> comment_stop bp; + if Options.do_translate() & t=("",".") then between_com := true; (t, (bp,ep)) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ep -> let id = get_buff len in comment_stop bp; (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) - (* utf-8 Greek letters U0380-03FF [CE80-CEBF and CF80-CFBF] *) - | [< ' ('\xCE' | '\xCF' as c1); ' ('\x80'..'\xBF' as c2); - len = ident_tail (store (store 0 c1) c2) >] ep -> - let id = get_buff len in - comment_stop bp; - (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep) - (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *) - | [< ''\xE2'; t = parse_226_tail (Some !token_tree) >] ep -> - comment_stop bp; - (match t with - | TokSymbol (Some t) -> ("", t), (bp, ep) - | TokSymbol None -> err (bp, ep) Undefined_token - | TokIdent id -> - (try ("", find_keyword id) with Not_found -> ("IDENT", id)), - (bp, ep)) | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep -> comment_stop bp; (("INT", get_buff len), (bp, ep)) @@ -419,8 +497,19 @@ let rec next_token = parser bp next_token s | [< t = process_chars bp c >] -> comment_stop bp; t >] -> t - | [< 'c; t = process_chars bp c >] -> comment_stop bp; t - | [< _ = Stream.empty >] -> comment_stop bp; (("EOI", ""), (bp, bp + 1)) + | [< s >] -> + match lookup_utf8 s with + | Some (Utf8Letter n) -> + let len = ident_tail (nstore n 0 s) s in + let id = get_buff len in + let ep = Stream.count s in + comment_stop bp; + (try ("",find_keyword id) with Not_found -> ("IDENT",id)), (bp, ep) + | Some (Utf8Symbol | AsciiChar | Utf8IdentPart _) -> + let t = process_chars bp (Stream.next s) s in + comment_stop bp; t + | None -> + comment_stop bp; (("EOI", ""), (bp, bp + 1)) (* Location table system for creating tables associating a token count to its location in a char stream (the source) *) @@ -461,10 +550,10 @@ let func cs = Stream.from (fun i -> let (tok, loc) = next_token cs in - loct_add loct i loc; Some tok) + loct_add loct i loc; Some tok) in - current_location_table := loct; - (ts, loct_func loct) + current_location_table := loct; + (ts, loct_func loct) type location_table = (int * int) option array array ref let location_table () = !current_location_table diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d743fffa..127a911f 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.ml4 7826 2006-01-09 22:00:34Z herbelin $ i*) +(*i $Id: pcoq.ml4 8926 2006-06-08 20:23:17Z herbelin $ i*) open Pp open Util @@ -286,6 +286,55 @@ let force_entry_type (u, utab) s etyp = with Not_found -> new_entry etyp (u, utab) s +(* Tactics as arguments *) + +let tactic_main_level = 5 + +let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0" +let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1" +let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2" +let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3" +let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4" +let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5" + +let wit_tactic = function + | 0 -> wit_tactic0 + | 1 -> wit_tactic1 + | 2 -> wit_tactic2 + | 3 -> wit_tactic3 + | 4 -> wit_tactic4 + | 5 -> wit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let globwit_tactic = function + | 0 -> globwit_tactic0 + | 1 -> globwit_tactic1 + | 2 -> globwit_tactic2 + | 3 -> globwit_tactic3 + | 4 -> globwit_tactic4 + | 5 -> globwit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let rawwit_tactic = function + | 0 -> rawwit_tactic0 + | 1 -> rawwit_tactic1 + | 2 -> rawwit_tactic2 + | 3 -> rawwit_tactic3 + | 4 -> rawwit_tactic4 + | 5 -> rawwit_tactic5 + | n -> anomaly ("Unavailable tactic level: "^string_of_int n) + +let tactic_genarg_level s = + if String.length s = 7 && String.sub s 0 6 = "tactic" then + let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) + else None + else None + +let is_tactic_genarg = function +| ExtraArgType s -> tactic_genarg_level s <> None +| _ -> false + + (* [make_gen_entry] builds entries extensible by giving its name (a string) *) (* For entries extensible only via the ML name, Gram.Entry.create is enough *) @@ -382,7 +431,6 @@ module Tactic = let tactic_arg = Gram.Entry.create "tactic:tactic_arg" let tactic_expr = Gram.Entry.create "tactic:tactic_expr" - let tactic_main_level = 5 let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic" (* Main entry for quotations *) @@ -391,6 +439,7 @@ module Tactic = end + module Vernac_ = struct let gec_vernac s = Gram.Entry.create ("vernac:" ^ s) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index fe6fd083..3998d71b 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 7826 2006-01-09 22:00:34Z herbelin $ i*) +(*i $Id: pcoq.mli 8926 2006-06-08 20:23:17Z herbelin $ i*) open Util open Names @@ -77,10 +77,46 @@ val force_entry_type : val create_constr_entry : string * gram_universe -> string -> constr_expr Gram.Entry.e -val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e +val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e val get_generic_entry : string -> grammar_object Gram.Entry.e val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type +(* Tactics as arguments *) + +val tactic_main_level : int + +val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type +val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type +val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type + +val is_tactic_genarg : argument_type -> bool + +val tactic_genarg_level : string -> int option + (* The main entry: reads an optional vernac command *) val main_entry : (loc * vernac_expr) option Gram.Entry.e @@ -148,7 +184,6 @@ module Tactic : val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e val tactic_arg : raw_tactic_arg Gram.Entry.e val tactic_expr : raw_tactic_expr Gram.Entry.e - val tactic_main_level : int val tactic : raw_tactic_expr Gram.Entry.e val tactic_eoi : raw_tactic_expr Gram.Entry.e end diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a43463c6..d55a6c1e 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: ppconstr.ml 8878 2006-05-30 16:44:25Z herbelin $ *) (*i*) open Util @@ -117,7 +117,7 @@ let pr_optc pr = function let pr_universe = Univ.pr_uni -let pr_sort = function +let pr_rawsort = function | RProp Term.Null -> str "Prop" | RProp Term.Pos -> str "Set" | RType u -> str "Type" ++ pr_opt pr_universe u @@ -153,8 +153,8 @@ let pr_lname = function | lna -> pr_located pr_name lna let pr_or_var pr = function - | Genarg.ArgArg x -> pr x - | Genarg.ArgVar (loc,s) -> pr_lident (loc,s) + | ArgArg x -> pr x + | ArgVar (loc,s) -> pr_lident (loc,s) let pr_prim_token = function | Numeral n -> Bigint.pr_bigint n @@ -379,11 +379,11 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = let ids = names_of_local_assums bl in match ro with CStructRec -> - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}" + if List.length ids > 1 && n <> None then + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" else mt() | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}" + spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" in pr_recursive_decl pr prd dangling_with_for id bl annot t c @@ -563,7 +563,7 @@ let rec pr sep inherited a = | CHole _ -> str "_", latom | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom - | CSort (_,s) -> pr_sort s, latom + | CSort (_,s) -> pr_rawsort s, latom | CCast (_,a,_,b) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b), lcast @@ -619,19 +619,16 @@ let rec strip_context n iscast t = let pr_constr_expr c = pr lsimple c let pr_lconstr_expr c = pr ltop c let pr_pattern_expr c = pr lsimple c +let pr_lpattern_expr c = pr ltop c + let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders (pr ltop) -let pr_pattern_occ prc = function - ([],c) -> prc c - | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - -let pr_unfold_occ pr_ref = function - ([],qid) -> pr_ref qid - | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) +let pr_with_occurrences pr = function + ([],c) -> pr c + | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++ + hov 0 (prlist_with_sep spc (pr_or_var int) nl)) let pr_red_flag pr r = (if r.rBeta then pr_arg str "beta" else mt ()) ++ @@ -651,7 +648,7 @@ 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_pattern_occ 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" @@ -661,11 +658,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function hov 1 (str "lazy" ++ pr_red_flag pr_ref f) | Unfold l -> hov 1 (str "unfold" ++ spc() ++ - prlist_with_sep pr_coma (pr_unfold_occ pr_ref) l) + prlist_with_sep pr_coma (pr_with_occurrences pr_ref) l) | Fold l -> hov 1 (str "fold" ++ prlist (pr_arg pr_constr) l) | Pattern l -> hov 1 (str "pattern" ++ - pr_arg (prlist_with_sep pr_coma (pr_pattern_occ pr_constr)) l) + 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 diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 7441f130..8f965d9b 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 7907 2006-01-21 11:03:29Z herbelin $ i*) +(*i $Id: ppconstr.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) open Pp open Environ @@ -53,17 +53,20 @@ val pr_id : identifier -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds +val pr_with_occurrences : + ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> + ('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_sort : rawsort -> std_ppcmds +val pr_rawsort : rawsort -> std_ppcmds val pr_binders : local_binder list -> std_ppcmds val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds +val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds val pr_lconstr_expr : constr_expr -> std_ppcmds val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index e6c12f4f..2113ae89 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 8651 2006-03-21 21:54:43Z jforest $ *) +(* $Id: pptactic.ml 8926 2006-06-08 20:23:17Z herbelin $ *) open Pp open Names @@ -127,7 +127,7 @@ let rec pr_message_token prid = function | MsgInt n -> int n | MsgIdent id -> prid id -let rec pr_raw_generic prc prlc prtac prref x = +let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) 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) @@ -139,16 +139,14 @@ let rec pr_raw_generic prc prlc prtac prref 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_sort (out_gen rawwit_sort x) + | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc prlc prref) - (out_gen rawwit_constr_may_eval x) + pr_arg (pr_may_eval prc prlc prref) (out_gen rawwit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> pr_arg (pr_red_expr (prc,prlc,prref)) (out_gen rawwit_red_expr x) - | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (rawwit_tactic n) x) | OpenConstrArgType b -> pr_arg 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) @@ -182,18 +180,18 @@ let rec pr_glob_generic prc prlc prtac 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_sort (out_gen globwit_sort x) + | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x) | ConstrArgType -> pr_arg prc (out_gen globwit_constr x) | ConstrMayEvalArgType -> pr_arg (pr_may_eval prc prlc - (pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_constr_may_eval x) + (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) | RedExprArgType -> pr_arg (pr_red_expr (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x) - | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (globwit_tactic n) x) | OpenConstrArgType b -> pr_arg 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) @@ -228,7 +226,7 @@ let rec pr_generic prc prlc prtac 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 prc (Term.mkSort (out_gen wit_sort 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) @@ -237,7 +235,6 @@ let rec pr_generic prc prlc prtac x = | RedExprArgType -> pr_arg (pr_red_expr (prc,prlc,pr_evaluable_reference)) (out_gen wit_red_expr x) - | TacticArgType n -> pr_arg (prtac (n,E)) (out_gen (wit_tactic n) x) | OpenConstrArgType b -> pr_arg prc (snd (out_gen (wit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x) @@ -381,17 +378,14 @@ let pr_by_tactic prt = function | TacId [] -> mt () | tac -> spc() ++ str "by " ++ prt tac -let pr_occs pp = function - [] -> pp - | nl -> hov 1 (pp ++ spc() ++ str"at " ++ - hov 0 (prlist_with_sep spc int nl)) - let pr_hyp_location pr_id = function - | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs - | id, occs, InHypTypeOnly -> - spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs - | id, occs, InHypValueOnly -> - spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs + | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, InHypTypeOnly -> + spc () ++ + pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs + | occs, InHypValueOnly -> + spc () ++ + pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) @@ -401,11 +395,11 @@ let pr_simple_clause pr_id = function let pr_clauses pr_id = function { onhyps=None; onconcl=true; concl_occs=nl } -> - pr_in (pr_occs (str " *") nl) + pr_in (pr_with_occurrences (fun () -> str " *") (nl,())) | { onhyps=None; onconcl=false } -> pr_in (str " * |-") | { onhyps=Some l; onconcl=true; concl_occs=nl } -> pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l - ++ pr_occs (str" |- *") nl) + ++ pr_with_occurrences (fun () -> str" |- *") (nl,())) | { onhyps=Some l; onconcl=false } -> pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l) @@ -418,6 +412,8 @@ let pr_clause_pattern pr_id = function ++ 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_induction_arg prc = function | ElimOnConstr c -> prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) @@ -436,17 +432,27 @@ let pr_match_pattern pr_pat = function | Subterm (Some id,a) -> str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" -let pr_match_hyps pr_pat = function - | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp +let pr_match_hyps pr_pat (Hyp (nal,mp)) = + pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp let pr_match_rule m pr pr_pat = function | Pat ([],mp,t) when m -> pr_match_pattern pr_pat mp ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t +(* + | Pat (rl,mp,t) -> + hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl ++ + (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) -> - prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++ - spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ - str "=>" ++ brk (1,4) ++ pr t + hov 0 ( + hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl) ++ + (if rl <> [] then spc () else mt ()) ++ + hov 0 ( + str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ + str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t let pr_funvar = function @@ -532,38 +538,46 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq open Closure +(** A printer for tactics that polymorphically works on the three + "raw", "glob" and "typed" levels; in practice, the environment is + used only at the glob and typed level: it is used to feed the + constr printers *) + 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) = - -let pr_bindings env = - pr_bindings (pr_lconstr env) (pr_constr env) in -let pr_ex_bindings env = - pr_bindings_gen true (pr_lconstr env) (pr_constr env) in -let pr_with_bindings env = - pr_with_bindings (pr_lconstr env) (pr_constr env) in -let pr_eliminator env cb = - str "using" ++ pr_arg (pr_with_bindings env) cb in -let pr_extend env = - pr_extend (pr_constr env) (pr_lconstr env) (pr_tac_level env) in -let pr_red_expr env = - pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) in - -let pr_constrarg env c = spc () ++ pr_constr env c in -let pr_lconstrarg env c = spc () ++ pr_lconstr env c in + pr_extend,strip_prod_binders) env = + +(* The environment is not used by the tactic printer: it is passed to the + constr and cst printers; hence we can make some abbreviations *) +let pr_constr = pr_constr env in +let pr_lconstr = pr_lconstr env in +let pr_cst = pr_cst env in +let pr_ind = pr_ind env in +let pr_tac_level = pr_tac_level env in + +(* Other short cuts *) +let pr_bindings = pr_bindings pr_lconstr pr_constr in +let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in +let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in +let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level in +let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst) in + +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_binder_fix env (nal,t) = +(* Some printing combinators *) +let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in + +let pr_binder_fix (nal,t) = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = - prlist_with_sep spc (pr_lname) nal ++ str ":" ++ - pr_lconstr env t in + let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in -let pr_fix_tac env (id,n,c) = +let pr_fix_tac (id,n,c) = let rec set_nth_name avoid n = function (nal,ty)::bll -> if n <= List.length nal then @@ -589,17 +603,17 @@ let pr_fix_tac env (id,n,c) = if List.length names = 1 then mt() else spc() ++ str"{struct " ++ pr_id idarg ++ str"}" in hov 1 (str"(" ++ pr_id id ++ - prlist (pr_binder_fix env) bll ++ annot ++ str" :" ++ - pr_lconstrarg env ty ++ str")") in + prlist pr_binder_fix bll ++ annot ++ str" :" ++ + pr_lconstrarg ty ++ str")") in (* spc() ++ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg - env c) + c) *) -let pr_cofix_tac env (id,c) = - hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in +let pr_cofix_tac (id,c) = + hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in (* Printing tactics as arguments *) -let rec pr_atom0 env = function +let rec pr_atom0 = function | TacIntroPattern [] -> str "intros" | TacIntroMove (None,None) -> str "intro" | TacAssumption -> str "assumption" @@ -607,77 +621,78 @@ let rec pr_atom0 env = function | TacTrivial ([],Some []) -> str "trivial" | TacAuto (None,[],Some []) -> str "auto" | TacReflexivity -> str "reflexivity" - | t -> str "(" ++ pr_atom1 env t ++ str ")" + | TacClear (true,[]) -> str "clear" + | t -> str "(" ++ pr_atom1 t ++ str ")" (* Main tactic printer *) -and pr_atom1 env = function +and pr_atom1 = function | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl | TacSuperAuto _ | TacExtend (_, ("GTauto"|"GIntuition"|"TSimplif"| "LinearIntuition"),_) -> errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0") | TacExtend (loc,s,l) -> - pr_with_comments loc (pr_extend env 1 s l) + pr_with_comments loc (pr_extend 1 s l) | TacAlias (loc,s,l,_) -> - pr_with_comments loc (pr_extend env 1 s (List.map snd l)) + pr_with_comments loc (pr_extend 1 s (List.map snd l)) (* Basic tactics *) - | TacIntroPattern [] as t -> pr_atom0 env t + | TacIntroPattern [] as t -> pr_atom0 t | 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) - | TacIntroMove (None,None) as t -> pr_atom0 env t + | 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) - | TacAssumption as t -> pr_atom0 env t - | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c) - | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c) - | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb) + | 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) + | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) | TacElim (cb,cbo) -> - hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ - pr_opt (pr_eliminator env) cbo) - | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg env c) - | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings env cb) - | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg env c) + hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ + pr_opt pr_eliminator cbo) + | TacElimType c -> hov 1 (str "elimtype" ++ pr_constrarg c) + | TacCase cb -> hov 1 (str "case" ++ spc () ++ pr_with_bindings cb) + | TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c) | TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ - str"with " ++ prlist_with_sep spc (pr_fix_tac env) l) + str"with " ++ prlist_with_sep spc pr_fix_tac l) | TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ - str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l) - | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c) + 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 env) (pr_constr env) ipat c ++ - pr_by_tactic (pr_tac_level env ltop) tac) + pr_assumption pr_lconstr pr_constr ipat c ++ + pr_by_tactic (pr_tac_level ltop) tac) | TacAssert (None,ipat,c) -> hov 1 (str "pose proof" ++ - pr_assertion (pr_lconstr env) (pr_constr env) ipat c) + pr_assertion pr_lconstr pr_constr ipat c) | TacGeneralize l -> hov 1 (str "generalize" ++ spc () ++ - prlist_with_sep spc (pr_constr env) l) + prlist_with_sep spc pr_constr l) | TacGeneralizeDep c -> hov 1 (str "generalize" ++ spc () ++ str "dependent" ++ - pr_constrarg env c) + pr_constrarg c) | TacLetTac (na,c,cl) when cl = nowhere -> - hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c) + hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c) | TacLetTac (na,c,cl) -> - hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++ + hov 1 (str "set" ++ pr_pose pr_lconstr pr_constr na c ++ pr_clauses pr_ident cl) (* | TacInstantiate (n,c,ConclLocation ()) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg env c ++ str ")" )) + pr_lconstrarg c ++ str ")" )) | TacInstantiate (n,c,HypLocation (id,hloc)) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg env c ++ str ")" ) + pr_lconstrarg c ++ str ")" ) ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None))) *) (* Derived basic tactics *) @@ -685,47 +700,49 @@ and pr_atom1 env = function hov 1 (str "simple induction" ++ pr_arg pr_quantified_hypothesis h) | TacNewInduction (h,e,ids) -> hov 1 (str "induction" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ - pr_opt (pr_eliminator env) e) + prlist_with_sep spc (pr_induction_arg pr_constr) h ++ + pr_with_names ids ++ + pr_opt pr_eliminator e) | TacSimpleDestruct h -> hov 1 (str "simple destruct" ++ pr_arg pr_quantified_hypothesis h) | TacNewDestruct (h,e,ids) -> hov 1 (str "destruct" ++ spc () ++ - prlist_with_sep spc (pr_induction_arg (pr_constr env)) h ++ + prlist_with_sep spc (pr_induction_arg pr_constr) h ++ pr_with_names ids ++ - pr_opt (pr_eliminator env) e) + pr_opt pr_eliminator e) | TacDoubleInduction (h1,h2) -> hov 1 (str "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ pr_arg pr_quantified_hypothesis h2) | TacDecomposeAnd c -> - hov 1 (str "decompose record" ++ pr_constrarg env c) + hov 1 (str "decompose record" ++ pr_constrarg c) | TacDecomposeOr c -> - hov 1 (str "decompose sum" ++ pr_constrarg env c) + hov 1 (str "decompose sum" ++ pr_constrarg c) | TacDecompose (l,c) -> hov 1 (str "decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_ind env) l - ++ str "]" ++ pr_constrarg env c)) + 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 ++ - pr_with_bindings env c) + pr_with_bindings c) | TacLApply c -> - hov 1 (str "lapply" ++ pr_constrarg env c) + hov 1 (str "lapply" ++ pr_constrarg c) (* Automation tactics *) - | TacTrivial ([],Some []) as x -> pr_atom0 env x + | TacTrivial ([],Some []) as x -> pr_atom0 x | TacTrivial (lems,db) -> hov 0 (str "trivial" ++ - pr_auto_using (pr_constr env) lems ++ pr_hintbases db) - | TacAuto (None,[],Some []) as x -> pr_atom0 env x + 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 ++ - pr_auto_using (pr_constr env) lems ++ pr_hintbases db) + pr_auto_using pr_constr lems ++ pr_hintbases db) | TacDAuto (n,p) -> hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p) (* Context management *) + | TacClear (true,[]) as t -> pr_atom0 t | TacClear (keep,l) -> hov 1 (str "clear" ++ spc () ++ (if keep then str "- " else mt ()) ++ prlist_with_sep spc pr_ident l) @@ -743,77 +760,81 @@ and pr_atom1 env = function str "into" ++ brk (1,1) ++ pr_ident id2) (* Constructors *) - | TacLeft l -> hov 1 (str "left" ++ pr_bindings env l) - | TacRight l -> hov 1 (str "right" ++ pr_bindings env l) - | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings env l) - | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings env l) + | TacLeft l -> hov 1 (str "left" ++ pr_bindings l) + | TacRight l -> hov 1 (str "right" ++ pr_bindings l) + | TacSplit (false,l) -> hov 1 (str "split" ++ pr_bindings l) + | TacSplit (true,l) -> hov 1 (str "exists" ++ pr_ex_bindings l) | TacAnyConstructor (Some t) -> - hov 1 (str "constructor" ++ pr_arg (pr_tac_level env (latom,E)) t) - | TacAnyConstructor None as t -> pr_atom0 env t + hov 1 (str "constructor" ++ pr_arg (pr_tac_level (latom,E)) t) + | TacAnyConstructor None as t -> pr_atom0 t | TacConstructor (n,l) -> - hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings env l) + hov 1 (str "constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l) (* Conversion *) | TacReduce (r,h) -> - hov 1 (pr_red_expr env r ++ + hov 1 (pr_red_expr r ++ pr_clauses pr_ident h) | TacChange (occ,c,h) -> hov 1 (str "change" ++ brk (1,1) ++ (match occ with None -> mt() - | Some([],c1) -> hov 1 (pr_constr env c1 ++ spc() ++ str "with ") + | Some([],c1) -> hov 1 (pr_constr c1 ++ spc() ++ str "with ") | Some(ocl,c1) -> - hov 1 (pr_constr env c1 ++ spc() ++ - str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++ + hov 1 (pr_constr c1 ++ spc() ++ + str "at " ++ prlist_with_sep spc (pr_or_var int) ocl) ++ + spc() ++ str "with ") ++ - pr_constr env c ++ pr_clauses pr_ident h) + pr_constr c ++ pr_clauses pr_ident h) (* Equivalence relations *) - | TacReflexivity as x -> pr_atom0 env x + | TacReflexivity as x -> pr_atom0 x | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls - | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c + | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) + | TacRewrite (b,c,cl) -> + hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings c ++ + pr_clauses pr_ident cl) | 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 env) c) + pr_with_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) | TacInversion (InversionUsing (c,cl),hyp) -> hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ - spc () ++ str "using" ++ spc () ++ pr_constr env c ++ + spc () ++ str "using" ++ spc () ++ pr_constr c ++ pr_simple_clause pr_ident cl) in -let rec pr_tac env inherited tac = +let rec pr_tac inherited tac = let (strm,prec) = match tac with | TacAbstract (t,None) -> - str "abstract " ++ pr_tac env (labstract,L) t, labstract + str "abstract " ++ pr_tac (labstract,L) t, labstract | TacAbstract (t,Some s) -> hov 0 - (str "abstract (" ++ pr_tac env (labstract,L) t ++ str")" ++ spc () ++ + (str "abstract (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () ++ str "using " ++ pr_id s), labstract | TacLetRecIn (l,t) -> hv 0 - (str "let rec " ++ pr_rec_clauses (pr_tac env ltop) l ++ str " in" ++ - fnl () ++ pr_tac env (llet,E) t), + (str "let rec " ++ pr_rec_clauses (pr_tac ltop) l ++ str " in" ++ + fnl () ++ pr_tac (llet,E) t), llet | TacLetIn (llc,u) -> v 0 - (hv 0 (pr_let_clauses (pr_tac env ltop) llc + (hv 0 (pr_let_clauses (pr_tac ltop) llc ++ str " in") ++ - fnl () ++ pr_tac env (llet,E) u), + fnl () ++ pr_tac (llet,E) u), llet | TacMatch (lz,t,lrul) -> - hov 0 (pr_lazy lz ++ str "match " ++ pr_tac env ltop t ++ str " with" + hov 0 (pr_lazy lz ++ str "match " ++ pr_tac ltop t ++ str " with" ++ prlist (fun r -> fnl () ++ str "| " ++ - pr_match_rule true (pr_tac env ltop) pr_pat r) + pr_match_rule true (pr_tac ltop) pr_pat r) lrul ++ fnl() ++ str "end"), lmatch @@ -822,79 +843,78 @@ let rec pr_tac env inherited tac = str (if lr then "match reverse goal with" else "match goal with") ++ prlist (fun r -> fnl () ++ str "| " ++ - pr_match_rule false (pr_tac env ltop) pr_pat r) + pr_match_rule false (pr_tac ltop) pr_pat r) lrul ++ fnl() ++ str "end"), lmatch | TacFun (lvar,body) -> -(* let env = List.fold_right (option_fold_right Idset.add) lvar env in*) hov 2 (str "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () ++ - pr_tac env (lfun,E) body), + pr_tac (lfun,E) body), lfun | TacThens (t,tl) -> - hov 1 (pr_tac env (lseq,E) t ++ pr_then () ++ spc () ++ - pr_seq_body (pr_tac env ltop) tl), + hov 1 (pr_tac (lseq,E) t ++ pr_then () ++ spc () ++ + pr_seq_body (pr_tac ltop) tl), lseq | TacThen (t1,t2) -> - hov 1 (pr_tac env (lseq,E) t1 ++ pr_then () ++ spc () ++ - pr_tac env (lseq,L) t2), + hov 1 (pr_tac (lseq,E) t1 ++ pr_then () ++ spc () ++ + pr_tac (lseq,L) t2), lseq | TacTry t -> - hov 1 (str "try" ++ spc () ++ pr_tac env (ltactical,E) t), + hov 1 (str "try" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacDo (n,t) -> hov 1 (str "do " ++ pr_or_var int n ++ spc () ++ - pr_tac env (ltactical,E) t), + pr_tac (ltactical,E) t), ltactical | TacRepeat t -> - hov 1 (str "repeat" ++ spc () ++ pr_tac env (ltactical,E) t), + hov 1 (str "repeat" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacProgress t -> - hov 1 (str "progress" ++ spc () ++ pr_tac env (ltactical,E) t), + hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacInfo t -> - hov 1 (str "info" ++ spc () ++ pr_tac env (ltactical,E) t), + hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacOrelse (t1,t2) -> - hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ - pr_tac env (lorelse,E) t2), + hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ + pr_tac (lorelse,E) t2), lorelse | 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 -> - str "first" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet + str "first" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacSolve tl -> - str "solve" ++ spc () ++ pr_seq_body (pr_tac env ltop) tl, llet + str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - str "complete" ++ spc () ++ pr_tac env (lcomplete,E) t, lcomplete + str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete | TacId l -> str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom | TacAtom (loc,TacAlias (_,s,l,_)) -> pr_with_comments loc - (pr_extend env (level_of inherited) s (List.map snd l)), + (pr_extend (level_of inherited) s (List.map snd l)), latom | TacAtom (loc,t) -> - pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom - | TacArg(Tacexp e) -> pr_tac_level env (latom,E) e, latom + pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom + | TacArg(Tacexp e) -> pr_tac_level (latom,E) e, latom | TacArg(ConstrMayEval (ConstrTerm c)) -> - str "constr:" ++ pr_constr env c, latom + str "constr:" ++ pr_constr c, latom | TacArg(ConstrMayEval c) -> - pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval + pr_may_eval pr_constr pr_lconstr pr_cst c, leval | TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qs sopt, latom | TacArg(Integer n) -> int n, latom | TacArg(TacCall(loc,f,l)) -> pr_with_comments loc (hov 1 (pr_ref f ++ spc () ++ - prlist_with_sep spc (pr_tacarg env) l)), + prlist_with_sep spc pr_tacarg l)), lcall - | TacArg a -> pr_tacarg env a, latom + | TacArg a -> pr_tacarg a, latom in if prec_less prec inherited then strm else str"(" ++ strm ++ str")" -and pr_tacarg env = function +and pr_tacarg = function | TacDynamic (loc,t) -> pr_with_comments loc (str ("")) | MetaIdArg (loc,s) -> pr_with_comments loc (str ("$" ^ s)) @@ -902,13 +922,13 @@ and pr_tacarg env = function | TacVoid -> str "()" | Reference r -> pr_ref r | ConstrMayEval c -> - pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c + pr_may_eval pr_constr pr_lconstr pr_cst c | TacFreshId sopt -> str "fresh" ++ pr_opt qs sopt | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ - spc() ++ prlist_with_sep spc (pr_tacarg env) la + spc() ++ prlist_with_sep spc pr_tacarg la | (TacCall _|Tacexp _|Integer _) as a -> - str "ltac:" ++ pr_tac env (latom,E) (TacArg a) + str "ltac:" ++ pr_tac (latom,E) (TacArg a) in (pr_tac, pr_match_rule) @@ -936,7 +956,7 @@ let rec raw_printers = (pr_raw_tactic_level, drop_env pr_constr_expr, drop_env pr_lconstr_expr, - pr_pattern_expr, + pr_lpattern_expr, drop_env pr_reference, drop_env pr_reference, pr_reference, @@ -945,10 +965,10 @@ let rec raw_printers = strip_prod_binders_expr) and pr_raw_tactic_level env n (t:raw_tactic_expr) = - fst (make_pr_tac raw_printers) env n t + fst (make_pr_tac raw_printers env) n t and pr_raw_match_rule env t = - snd (make_pr_tac raw_printers) env t + snd (make_pr_tac raw_printers env) t let pr_and_constr_expr pr (c,_) = pr c @@ -956,7 +976,7 @@ let rec glob_printers = (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_constr_pattern_env (Global.env()) c), + (fun c -> pr_lconstr_pattern_env (Global.env()) c), (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))), (fun env -> pr_or_var (pr_inductive env)), pr_ltac_or_var (pr_located pr_ltac_constant), @@ -965,17 +985,16 @@ let rec glob_printers = strip_prod_binders_rawterm) and pr_glob_tactic_level env n (t:glob_tactic_expr) = - fst (make_pr_tac glob_printers) env n t + fst (make_pr_tac glob_printers env) n t and pr_glob_match_rule env t = - snd (make_pr_tac glob_printers) env t + snd (make_pr_tac glob_printers env) t -let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) = - make_pr_tac +let typed_printers = (pr_glob_tactic_level, pr_constr_env, pr_lconstr_env, - pr_constr_pattern, + pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, pr_ltac_constant, @@ -983,6 +1002,8 @@ let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> s pr_extend, strip_prod_binders_constr) +let pr_tactic_level env = fst (make_pr_tac typed_printers env) + let pr_raw_tactic env = pr_raw_tactic_level env ltop let pr_glob_tactic env = pr_glob_tactic_level env ltop let pr_tactic env = pr_tactic_level env ltop @@ -996,3 +1017,14 @@ let _ = Tactic_debug.set_match_pattern_printer let _ = Tactic_debug.set_match_rule_printer (fun rl -> pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl) + +open Pcoq + +let pr_tac_polymorphic n _ _ prtac = prtac (n,E) + +let _ = for i=0 to 5 do + declare_extra_genarg_pprule + (rawwit_tactic i, pr_tac_polymorphic i) + (globwit_tactic i, pr_tac_polymorphic i) + (wit_tactic i, pr_tac_polymorphic i) +done diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 0b6e5771..aea44604 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 8624 2006-03-13 17:38:17Z msozeau $ *) +(* $Id: ppvernac.ml 8831 2006-05-19 09:29:54Z herbelin $ *) open Pp open Names @@ -277,7 +277,7 @@ let pr_onescheme (id,dep,ind,s) = hov 0 (pr_lident id ++ str" :=") ++ spc() ++ hov 0 ((if dep then str"Induction for" else str"Minimality for") ++ spc() ++ pr_reference ind) ++ spc() ++ - hov 0 (str"Sort" ++ spc() ++ pr_sort s) + hov 0 (str"Sort" ++ spc() ++ pr_rawsort s) let begin_of_inductive = function [] -> 0 @@ -555,18 +555,23 @@ let rec pr_vernac = function else ([],def,type_) in let bl = bl @ bl' in let ids = List.flatten (List.map name_of_binder bl) in - let name = - try snd (List.nth ids n) - with Failure _ -> - warn (str "non-printable fixpoint \""++pr_id id++str"\""); - Anonymous in let annot = - match (ro : Topconstr.recursion_order_expr) with - CStructRec -> - if List.length ids > 1 then - spc() ++ str "{struct " ++ pr_name name ++ str"}" - else mt() - | CWfRec c -> spc() ++ str "{wf " ++ pr_name name ++ spc() ++ pr_lconstr_expr c ++ str"}" + match n with + | None -> mt () + | Some n -> + let name = + try snd (List.nth ids n) + with Failure _ -> + warn (str "non-printable fixpoint \""++pr_id id++str"\""); + Anonymous in + match (ro : Topconstr.recursion_order_expr) with + CStructRec -> + if List.length ids > 1 then + spc() ++ str "{struct " ++ pr_name name ++ str"}" + else mt() + | CWfRec c -> + spc() ++ str "{wf " ++ pr_name name ++ spc() ++ + pr_lconstr_expr c ++ str"}" in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ @@ -823,6 +828,13 @@ and pr_extend s cl = try let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in + let start,rl,cl = + match rl with + | Egrammar.TacTerm s :: rl -> str s, rl, cl + | Egrammar.TacNonTerm _ :: rl -> + (* Will put an unnecessary extra space in front *) + pr_gen (Global.env()) (List.hd cl), rl, List.tl cl + | [] -> anomaly "Empty entry" in let (pp,_) = List.fold_left (fun (strm,args) pi -> @@ -831,7 +843,7 @@ and pr_extend s cl = (strm ++ pr_gen (Global.env()) (List.hd args), List.tl args) | Egrammar.TacTerm s -> (strm ++ spc() ++ str s, args)) - (mt(),cl) rl in + (start,cl) rl in hov 1 pp with Not_found -> hov 1 (str ("TODO("^s) ++ prlist_with_sep sep pr_arg cl ++ str ")") diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a22f5796..4534369f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml 7938 2006-01-28 22:03:33Z herbelin $ *) +(* $Id: prettyp.ml 8845 2006-05-23 07:41:58Z herbelin $ *) open Pp open Util @@ -278,11 +278,11 @@ let print_constructors envpar names types = hv 0 (str " " ++ pc) let build_inductive sp tyi = - let (mib,mip) = Global.lookup_inductive (sp,tyi) in + let (mib,mip as specif) = Global.lookup_inductive (sp,tyi) in let params = mib.mind_params_ctxt in let args = extended_rel_list 0 params in let env = Global.env() in - let arity = hnf_prod_applist env mip.mind_user_arity args in + let arity = hnf_prod_applist env (Inductive.type_of_inductive specif) args in let cstrtypes = arities_of_constructors env (sp,tyi) in let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in @@ -401,7 +401,7 @@ let print_context with_values = | h::rest when n = None or out_some n > 0 -> (match print_library_entry with_values h with | None -> prec n rest - | Some pp -> prec (option_app ((+) (-1)) n) rest ++ pp ++ fnl ()) + | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec diff --git a/parsing/printer.ml b/parsing/printer.ml index 82676b79..8cb5ac42 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 7855 2006-01-12 08:21:57Z herbelin $ *) +(* $Id: printer.ml 8831 2006-05-19 09:29:54Z herbelin $ *) open Pp open Util @@ -77,11 +77,18 @@ let pr_rawconstr c = let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Idset.empty t) +let pr_lconstr_pattern_env env c = + pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_constr_pattern_env env c = pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c) + +let pr_lconstr_pattern t = + pr_lconstr_expr (extern_constr_pattern empty_names_context t) let pr_constr_pattern t = pr_constr_expr (extern_constr_pattern empty_names_context t) +let pr_sort s = pr_rawsort (extern_sort s) + let _ = Termops.set_print_constr pr_lconstr_env (**********************************************************************) diff --git a/parsing/printer.mli b/parsing/printer.mli index 66471d41..9d59bf75 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 7855 2006-01-12 08:21:57Z herbelin $ i*) +(*i $Id: printer.mli 8831 2006-05-19 09:29:54Z herbelin $ i*) (*i*) open Pp @@ -50,11 +50,16 @@ val pr_lrawconstr : rawconstr -> std_ppcmds val pr_rawconstr_env : env -> rawconstr -> std_ppcmds val pr_rawconstr : rawconstr -> std_ppcmds +val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds +val pr_lconstr_pattern : constr_pattern -> std_ppcmds + val pr_constr_pattern_env : env -> constr_pattern -> std_ppcmds val pr_constr_pattern : constr_pattern -> std_ppcmds val pr_cases_pattern : cases_pattern -> std_ppcmds +val pr_sort : sorts -> std_ppcmds + (* Printing global references using names as short as possible *) val pr_global_env : Idset.t -> global_reference -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 35801f73..b5b07091 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: q_coqast.ml4 8651 2006-03-21 21:54:43Z jforest $ *) +(* $Id: q_coqast.ml4 8926 2006-06-08 20:23:17Z herbelin $ *) open Util open Names @@ -77,20 +77,22 @@ 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 - | Genarg.ArgArg x -> <:expr< Genarg.ArgArg $f x$ >> - | Genarg.ArgVar id -> <:expr< Genarg.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> + | Rawterm.ArgArg x -> <:expr< Rawterm.ArgArg $f x$ >> + | Rawterm.ArgVar id -> <:expr< Rawterm.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) -let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int +let mlexpr_of_occs = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) + +let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f let mlexpr_of_hyp_location = function - | id, occs, Tacexpr.InHyp -> - <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHyp) >> - | id, occs, Tacexpr.InHypTypeOnly -> - <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypTypeOnly) >> - | id, occs, Tacexpr.InHypValueOnly -> - <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, Tacexpr.InHypValueOnly) >> + | occs, Tacexpr.InHyp -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHyp) >> + | occs, Tacexpr.InHypTypeOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypTypeOnly) >> + | occs, Tacexpr.InHypValueOnly -> + <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Tacexpr.InHypValueOnly) >> let mlexpr_of_clause cl = <:expr< {Tacexpr.onhyps= @@ -140,7 +142,8 @@ let rec mlexpr_of_constr = function | _ -> failwith "mlexpr_of_constr: TODO" let mlexpr_of_occ_constr = - mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr + mlexpr_of_pair (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int)) + mlexpr_of_constr let mlexpr_of_red_expr = function | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >> @@ -151,7 +154,7 @@ let mlexpr_of_red_expr = function | Rawterm.Lazy f -> <:expr< Rawterm.Lazy $mlexpr_of_red_flags f$ >> | Rawterm.Unfold l -> - let f1 = mlexpr_of_list mlexpr_of_int in + let f1 = mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) in let f2 = mlexpr_of_reference in let f = mlexpr_of_list (mlexpr_of_pair f1 f2) in <:expr< Rawterm.Unfold $f l$ >> @@ -179,7 +182,6 @@ let rec mlexpr_of_argtype loc = function | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> - | Genarg.TacticArgType n -> <:expr< Genarg.TacticArgType $mlexpr_of_int n$ >> | Genarg.SortArgType -> <:expr< Genarg.SortArgType >> | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 48a124a7..3d41e388 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacextend.ml4 7732 2005-12-26 13:51:24Z herbelin $ *) +(* $Id: tacextend.ml4 8926 2006-06-08 20:23:17Z herbelin $ *) open Genarg open Q_util @@ -36,8 +36,6 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l -let is_tactic_arg = function TacticArgType _ -> true | _ -> false - let rec make_let e = function | [] -> e | TacNonTerm(loc,t,_,Some p)::l -> @@ -47,7 +45,7 @@ let rec make_let e = function let v = (* Special case for tactics which must be stored in algebraic form to avoid marshalling closures and to be reprinted *) - if is_tactic_arg t then + if Pcoq.is_tactic_genarg t then <:expr< ($v$, Tacinterp.eval_tactic $v$) >> else v in <:expr< let $lid:p$ = $v$ in $e$ >> @@ -84,7 +82,7 @@ let rec make_args = function let rec make_eval_tactic e = function | [] -> e - | TacNonTerm(loc,TacticArgType _,_,Some p)::l -> + | TacNonTerm(loc,tag,_,Some p)::l when Pcoq.is_tactic_genarg tag -> let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_eval_tactic e l in (* Special case for tactics which must be stored in algebraic -- cgit v1.2.3