diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r-- | parsing/g_tactic.ml4 | 233 |
1 files changed, 101 insertions, 132 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index be20f891..1609e541 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -1,122 +1,104 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo" i*) - -(* $Id: g_tactic.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Pcoq open Util open Tacexpr -open Rawterm +open Glob_term open Genarg open Topconstr open Libnames open Termops +open Tok +open Compat let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw +let _ = List.iter Lexer.add_keyword tactic_kw + +let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) (* admissible notation "(x t)" *) let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("IDENT",s)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; (("IDENT"|"INT"),_)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":=")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ | INT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x:t) *) let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("IDENT",id)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", ":")] -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> + (match get_tok (stream_nth 2 strm) with + | KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = - match list_last (Stream.npeek n strm) with - | ("","(") -> skip_to_rpar (p+1) (n+1) - | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1) - | ("",".") -> raise Stream.Failure + match get_tok (list_last (Stream.npeek n strm)) with + | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) + | KEYWORD ")" -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1) + | KEYWORD "." -> err () | _ -> skip_to_rpar p (n+1) in let rec skip_names n = - match list_last (Stream.npeek n strm) with - | ("IDENT",_) | ("","_") -> skip_names (n+1) - | ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *) - | _ -> raise Stream.Failure in + match get_tok (list_last (Stream.npeek n strm)) with + | IDENT _ | KEYWORD "_" -> skip_names (n+1) + | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) + | _ -> err () in let rec skip_binders n = - match list_last (Stream.npeek n strm) with - | ("","(") -> skip_binders (skip_names (n+1)) - | ("IDENT",_) | ("","_") -> skip_binders (n+1) - | ("",":=") -> () - | _ -> raise Stream.Failure in - match Stream.npeek 1 strm with - | [("","(")] -> skip_binders 2 - | _ -> raise Stream.Failure) - -let guess_lpar_ipat s strm = - match Stream.npeek 1 strm with - | [("","(")] -> - (match Stream.npeek 2 strm with - | [_; ("",("("|"["))] -> () - | [_; ("IDENT",_)] -> - (match Stream.npeek 3 strm with - | [_; _; ("", s')] when s = s' -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure - -let guess_lpar_coloneq = - Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=") - -let guess_lpar_colon = - Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":") + match get_tok (list_last (Stream.npeek n strm)) with + | KEYWORD "(" -> skip_binders (skip_names (n+1)) + | IDENT _ | KEYWORD "_" -> skip_binders (n+1) + | KEYWORD ":=" -> () + | _ -> err () in + match get_tok (stream_nth 0 strm) with + | KEYWORD "(" -> skip_binders 2 + | _ -> err ()) let lookup_at_as_coma = Gram.Entry.of_parser "lookup_at_as_coma" (fun strm -> - match Stream.npeek 1 strm with - | [("",(","|"at"|"as"))] -> () - | _ -> raise Stream.Failure) + match get_tok (stream_nth 0 strm) with + | KEYWORD (","|"at"|"as") -> () + | _ -> err ()) open Constr open Prim @@ -144,25 +126,23 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let induction_arg_of_constr (c,lbind as clbind) = if lbind = NoBindings then try ElimOnIdent (constr_loc c,snd(coerce_to_id c)) - with _ -> ElimOnConstr clbind + with e when Errors.noncritical e -> ElimOnConstr clbind else ElimOnConstr clbind let mkTacCase with_evar = function - | [([ElimOnConstr cl],None,(None,None))],None -> + | [ElimOnConstr cl,(None,None)],None,None -> TacCase (with_evar,cl) (* Reinterpret numbers as a notation for terms *) - | [([(ElimOnAnonHyp n)],None,(None,None))],None -> + | [ElimOnAnonHyp n,(None,None)],None,None -> TacCase (with_evar, - (CPrim (dummy_loc, Numeral (Bigint.of_string (string_of_int n))), + (CPrim (dummy_loc, Numeral (Bigint.of_int n)), NoBindings)) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) - | [([ElimOnIdent id],None,(None,None))],None -> + | [ElimOnIdent id,(None,None)],None,None -> TacCase (with_evar,(CRef (Ident id),NoBindings)) | ic -> - if List.exists (fun (cl,a,b) -> - List.exists (function ElimOnAnonHyp _ -> true | _ -> false) cl) - (fst ic) + if List.exists (function (ElimOnAnonHyp _,_) -> true | _ -> false) (pi1 ic) then error "Use of numbers as direct arguments of 'case' is not supported."; TacInductionDestruct (false,with_evar,ic) @@ -183,8 +163,8 @@ let mkCLambdaN_simple 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 + | Glob_term.ArgArg x -> Glob_term.ArgArg (f x) + | Glob_term.ArgVar _ as y -> y let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr } @@ -222,12 +202,12 @@ GEXTEND Gram simple_intropattern; int_or_var: - [ [ n = integer -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = integer -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; nat_or_var: - [ [ n = natural -> Rawterm.ArgArg n - | id = identref -> Rawterm.ArgVar id ] ] + [ [ n = natural -> Glob_term.ArgArg n + | id = identref -> Glob_term.ArgVar id ] ] ; (* An identifier or a quotation meta-variable *) id_or_meta: @@ -236,12 +216,6 @@ GEXTEND Gram (* This is used in quotations *) | id = METAIDENT -> MetaId (loc,id) ] ] ; - (* A number or a quotation meta-variable *) - num_or_meta: - [ [ n = integer -> AI n - | id = METAIDENT -> MetaId (loc,id) - ] ] - ; open_constr: [ [ c = constr -> ((),c) ] ] ; @@ -303,11 +277,6 @@ GEXTEND Gram | "*" -> loc, IntroForthcoming true | "**" -> loc, IntroForthcoming false ] ] ; - intropattern_modifier: - [ [ IDENT "_eqn"; - id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ] - -> id ] ] - ; simple_intropattern: [ [ pat = disjunctive_intropattern -> pat | pat = naming_intropattern -> pat @@ -372,7 +341,7 @@ GEXTEND Gram | IDENT "lazy"; s = strategy_flag -> Lazy s | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) | IDENT "vm_compute" -> CbvVm - | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul + | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl | s = IDENT -> ExtraRedExpr s ] ] @@ -451,7 +420,7 @@ GEXTEND Gram ; hintbases: [ [ "with"; "*" -> None - | "with"; l = LIST1 IDENT -> Some l + | "with"; l = LIST1 [ x = IDENT -> x] -> Some l | -> Some [] ] ] ; auto_using: @@ -469,10 +438,15 @@ GEXTEND Gram [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] ; - with_induction_names: - [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier - -> (eq,Some ipat) - | -> (None,None) ] ] + eqn_ipat: + [ [ IDENT "eqn"; ":"; id = naming_intropattern -> Some id + | IDENT "_eqn"; ":"; id = naming_intropattern -> + let msg = "Obsolete syntax \"_eqn:H\" could be replaced by \"eqn:H\"" in + msg_warning (strbrk msg); Some id + | IDENT "_eqn" -> + let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in + msg_warning (strbrk msg); Some (loc, IntroAnonymous) + | -> None ] ] ; as_name: [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] @@ -501,14 +475,11 @@ GEXTEND Gram [ [ 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 -> (lc,el,ipats) ] ] - ; - one_induction_clause: - [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ] + [ [ c = induction_arg; pat = as_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ] ; induction_clause_list: - [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ] + [ [ ic = LIST1 induction_clause SEP ","; + el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ] ; move_location: [ [ IDENT "after"; id = id_or_meta -> MoveAfter id @@ -559,15 +530,16 @@ GEXTEND Gram TacMutualCofix (false,id,List.map mk_cofix_tac fd) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacLetTac (Names.Name id,b,nowhere,true) + TacLetTac (Names.Name id,b,nowhere,true,None) | IDENT "pose"; b = constr; na = as_name -> - TacLetTac (na,b,nowhere,true) + TacLetTac (na,b,nowhere,true,None) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacLetTac (Names.Name id,c,p,true) + TacLetTac (Names.Name id,c,p,true,None) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacLetTac (na,c,p,true) - | IDENT "remember"; c = constr; na = as_name; p = clause_dft_all -> - TacLetTac (na,c,p,false) + TacLetTac (na,c,p,true,None) + | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + TacLetTac (na,c,p,false,e) (* Begin compatibility *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; @@ -602,9 +574,9 @@ GEXTEND Gram (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInductionDestruct (true,h) - | IDENT "induction"; ic = one_induction_clause -> + | IDENT "induction"; ic = induction_clause_list -> TacInductionDestruct (true,false,ic) - | IDENT "einduction"; ic = one_induction_clause -> + | IDENT "einduction"; ic = induction_clause_list -> TacInductionDestruct(true,true,ic) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) @@ -621,21 +593,18 @@ GEXTEND Gram (* Automation tactic *) | IDENT "trivial"; lems = auto_using; db = hintbases -> - TacTrivial (lems,db) + TacTrivial (Off,lems,db) + | IDENT "info_trivial"; lems = auto_using; db = hintbases -> + TacTrivial (Info,lems,db) + | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases -> + TacTrivial (Debug,lems,db) + | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases -> - TacAuto (n,lems,db) - -(* Obsolete since V8.0 - | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n - | IDENT "cdhyp"; id = identref -> TacDestructHyp (true,id) - | IDENT "dhyp"; id = identref -> TacDestructHyp (false,id) - | IDENT "dconcl" -> TacDestructConcl - | IDENT "superauto"; l = autoargs -> TacSuperAuto l -*) - | IDENT "auto"; IDENT "decomp"; p = OPT natural; - lems = auto_using -> TacDAuto (None,p,lems) - | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural; - lems = auto_using -> TacDAuto (n,p,lems) + TacAuto (Off,n,lems,db) + | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; + db = hintbases -> TacAuto (Info,n,lems,db) + | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; + db = hintbases -> TacAuto (Debug,n,lems,db) (* Context management *) | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l) @@ -656,9 +625,9 @@ GEXTEND Gram | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll) | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (true,true,bll) - | IDENT "constructor"; n = num_or_meta; l = with_bindings -> + | IDENT "constructor"; n = nat_or_var; l = with_bindings -> TacConstructor (false,n,l) - | IDENT "econstructor"; n = num_or_meta; l = with_bindings -> + | IDENT "econstructor"; n = nat_or_var; l = with_bindings -> TacConstructor (true,n,l) | IDENT "constructor"; t = OPT tactic -> TacAnyConstructor (false,t) | IDENT "econstructor"; t = OPT tactic -> TacAnyConstructor (true,t) |