From 0406263287e722c7784bc66225da4ef13118f2da Mon Sep 17 00:00:00 2001 From: delahaye Date: Thu, 17 Aug 2000 16:14:53 +0000 Subject: Pattern matching de sous-termes + exceptions dans le lexer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@578 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/g_constr.ml4 | 6 +++-- parsing/g_tactic.ml4 | 46 ++++++++++++++++++++++---------- parsing/g_vernac.ml4 | 5 +++- parsing/lexer.mll | 21 ++++++++------- parsing/pattern.ml | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++- parsing/pattern.mli | 8 +++++- parsing/pcoq.ml4 | 4 +++ parsing/pcoq.mli | 4 +++ 8 files changed, 140 insertions(+), 29 deletions(-) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e9ed83a54..d685b292a 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -17,8 +17,10 @@ GEXTEND Gram ; constr: [ [ c = constr8 -> c - | IDENT "Eval"; rtc=Tactic.red_tactic; "in"; c=constr8 -> - <:ast<(EVAL $c (REDEXP $rtc))>> ] ] + | IDENT "Context"; id = ident; IDENT "With"; c = constr8 -> + <:ast< (CONTEXT $id $c) >> + | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 -> + <:ast< (EVAL $c (REDEXP $rtc)) >> ] ] ; lconstr: [ [ c = constr10 -> c ] ] diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 37f47b6f0..d0e3a8a76 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -4,8 +4,8 @@ open Pp open Ast open Pcoq - open Tactic +open Util (* Please leave several GEXTEND for modular compilation under PowerPC *) @@ -193,23 +193,42 @@ GEXTEND Gram [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr -> <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ] ; + match_pattern: + [ [ id = constrarg; "["; pc = constrarg; "]" -> + (match id with + | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> + <:ast< (SUBTERM ($VAR $s) $pc) >> + | _ -> + errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">]) + | "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >> + | pc = constrarg -> <:ast< (TERM $pc) >> ] ] + ; match_hyps: - [ [ id = identarg; ":"; pc = constrarg -> - <:ast< (MATCHCONTEXTHYPS $id $pc) >> - | IDENT "_"; ":"; pc = constrarg -> <:ast< (MATCHCONTEXTHYPS $pc) >> ] ] + [ [ id = identarg; ":"; mp = match_pattern -> + <:ast< (MATCHCONTEXTHYPS $id $mp) >> + | IDENT "_"; ":"; mp = match_pattern -> + <:ast< (MATCHCONTEXTHYPS $mp) >> ] ] ; match_context_rule: - [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; pc = constrarg; "]"; "->"; - te = tactic_expr -> - <:ast< (MATCHCONTEXTRULE ($LIST $largs) $pc $te) >> + [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]"; + "->"; te = tactic_expr -> + <:ast< (MATCHCONTEXTRULE ($LIST $largs) $mp $te) >> | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHCONTEXTRULE $te) >> ] ] ; + match_context_list: + [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl + | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] + ; match_rule: - [ [ "["; com = constrarg; "]"; "->"; te = tactic_expr -> - <:ast<(MATCHRULE $com $te)>> + [ [ "["; mp = match_pattern; "]"; "->"; te = tactic_expr -> + <:ast<(MATCHRULE $mp $te)>> | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHRULE $te) >> ] ] ; + match_list: + [ [ mrl = LIST1 match_rule SEP "|" -> mrl + | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] + ; tactic_expr: [ [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> <:ast< (TACTICLIST $ta0 $ta1) >> @@ -229,11 +248,10 @@ GEXTEND Gram <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >> | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In"; u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >> - | IDENT "Match"; IDENT "Context"; IDENT "With"; - mrl = LIST1 match_context_rule SEP "|" -> - <:ast< (MATCHCONTEXT ($LIST $mrl)) >> - | IDENT "Match"; com = constrarg; IDENT "With"; - mrl = LIST1 match_rule SEP "|" -> <:ast< (MATCH $com ($LIST $mrl)) >> + | IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list + -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >> + | IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list -> + <:ast< (MATCH $com ($LIST $mrl)) >> | "'("; te = tactic_expr; ")" -> te | "'("; te = tactic_expr; tel=LIST1 tactic_expr; ")" -> <:ast< (APP $te ($LIST tel)) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 187c75c07..7c91cbf90 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -428,13 +428,16 @@ GEXTEND Gram (* Proof commands *) GEXTEND Gram - GLOBAL: command; + GLOBAL: command ne_constrarg_list; destruct_location : [ [ IDENT "Conclusion" -> <:ast< (CONCL)>> | IDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>> | "Hypothesis" -> <:ast< (PreciousHYP)>> ]] ; + ne_constrarg_list: + [ [ l = LIST1 constrarg -> l ] ] + ; opt_identarg_list: [ [ -> [] | ":"; l = LIST1 identarg -> l ] ] diff --git a/parsing/lexer.mll b/parsing/lexer.mll index 10ed3ab86..54cb8285c 100644 --- a/parsing/lexer.mll +++ b/parsing/lexer.mll @@ -119,8 +119,8 @@ let firstchar = let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] -let symbolchar = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '~' '#'] -let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '='] +let symbolchar = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'] +let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'] let decimal_literal = ['0'-'9']+ let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ let oct_literal = '0' ['o' 'O'] ['0'-'7']+ @@ -137,14 +137,15 @@ rule token = parse | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "()" | "'(" | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | extrachar { ("", Lexing.lexeme lexbuf) } - | ('\\' (symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ | - '/' (symbolchar | '/' | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ | - '-' (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<')+ | - '|' (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<')+ | - '=' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ | - ':' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ | - '<' (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<')+ | - "<-" (symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<')+ | + | ('\\'(symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ | + '/' (symbolchar | '/' | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ | + '-' (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<' | '~')+ | + '|' (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<' | '~')+ | + '=' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' | '~')+ | + '<' (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<' | '~')+ | + "<-"(symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<' | '~')+ | + '~' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ | + ':' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ | '>' | '?') extrachar* | "<-" { ("", Lexing.lexeme lexbuf) } | symbolchar+ extrachar* diff --git a/parsing/pattern.ml b/parsing/pattern.ml index 6d3c362d6..e3fa611ed 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -189,7 +189,7 @@ let matches_core convert pat c = if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma else raise PatternMatchingFailure - | PCase (_,a1,br1), IsMutCase (ci,p2,a2,br2) -> + | PCase (_,a1,br1), IsMutCase (_,_,a2,br2) -> (* On ne teste pas le prédicat *) array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2 @@ -204,6 +204,79 @@ let matches_core convert pat c = let matches = matches_core None +(* To skip to the next occurrence *) +exception NextOccurrence of int + +(* Tells if it is an authorized occurrence *) +let authorized_occ nocc mres = + if nocc = 0 then mres + else raise (NextOccurrence nocc) + +(* Tries matches according to the occurrence *) +let rec try_matches nocc pat = function + | [] -> raise (NextOccurrence nocc) + | c::tl -> + (try authorized_occ nocc (matches pat c) with + | PatternMatchingFailure -> (try_matches nocc pat tl) + | NextOccurrence nocc -> (try_matches (nocc - 1) pat tl)) + +(* Tries to match a subterm of [c] with [pat] *) +let rec sub_match nocc pat c = + match c with + | DOP2 (Cast,c1,c2) -> + (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1] in + (lm,DOP2 (Cast,List.hd lc,c2)) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in + (lm,DOP2 (Cast,List.hd lc,c2))) + | DOP2 (ne,c1,DLAM (x,c2)) -> + (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + | PatternMatchingFailure -> + let (lm,lc) = try_sub_match nocc pat [c1;c2] in + (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1))) + | NextOccurrence nocc -> + let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in + (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1)))) + | DOPN (AppL,a) when Array.length a <> 0 -> + let c1 = a.(0) + and lc = List.tl (Array.to_list a) in + (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + | PatternMatchingFailure -> + let (lm,le) = try_sub_match nocc pat (c1::lc) in + (lm,DOPN (AppL,Array.of_list le)) + | NextOccurrence nocc -> + let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in + (lm,DOPN (AppL,Array.of_list le))) + | DOPN (MutCase ci,v) -> + let hd = v.(0) + and c1 = v.(1) + and lc = Array.to_list (Array.sub v 2 (Array.length v - 2)) in + (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + | PatternMatchingFailure -> + let (lm,le) = try_sub_match nocc pat (c1::lc) in + (lm,DOPN (MutCase ci,Array.of_list (hd::le))) + | NextOccurrence nocc -> + let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in + (lm,DOPN (MutCase ci,Array.of_list (hd::le)))) + | c -> + (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with + | PatternMatchingFailure -> raise (NextOccurrence nocc) + | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) + +(* Tries [sub_match] for all terms in the list *) +and try_sub_match nocc pat lc = + let rec try_sub_match_rec nocc pat lacc = function + | [] -> raise (NextOccurrence nocc) + | c::tl -> + (try + let (lm,ce) = sub_match nocc pat c in + (lm,lacc@(ce::tl)) + with + | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in + try_sub_match_rec nocc pat [] lc + let is_matching pat n = try let _ = matches pat n in true with PatternMatchingFailure -> false diff --git a/parsing/pattern.mli b/parsing/pattern.mli index b725d9044..803e4fffe 100644 --- a/parsing/pattern.mli +++ b/parsing/pattern.mli @@ -69,9 +69,15 @@ val is_matching : val matches_conv : env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list +(* To skip to the next occurrence *) +exception NextOccurrence of int + +(* Tries to match a subterm of [c] with [pat] *) +val sub_match : + int -> constr_pattern -> constr -> ((int * constr) list * constr) + (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] up to conversion for constants in patterns *) val is_matching_conv : env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool - diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index a80952480..9d2b8e931 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -286,7 +286,10 @@ module Tactic = let clausearg = gec "clausearg" let match_context_rule = gec "match_context_rule" let match_hyps = gec "match_hyps" + let match_pattern = gec "match_pattern" + let match_context_list = gec_list "match_context_list" let match_rule = gec "match_rule" + let match_list = gec_list "match_list" let ne_identarg_list = gec_list "ne_identarg_list" let ne_num_list = gec_list "ne_num_list" let ne_pattern_list = gec_list "ne_pattern_list" @@ -343,6 +346,7 @@ module Vernac = let stringarg = gec "stringarg" let ne_stringarg_list = gec_list "ne_stringarg_list" let constrarg = gec "constrarg" + let ne_constrarg_list = gec_list "ne_constrarg_list" let tacarg = gec "tacarg" let sortarg = gec "sortarg" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 2d486e561..e3ccced7d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -113,7 +113,10 @@ module Tactic : val let_clause : Coqast.t Gram.Entry.e val match_context_rule : Coqast.t Gram.Entry.e val match_hyps : Coqast.t Gram.Entry.e + val match_pattern : Coqast.t Gram.Entry.e + val match_context_list : Coqast.t list Gram.Entry.e val match_rule : Coqast.t Gram.Entry.e + val match_list : Coqast.t list Gram.Entry.e val ne_identarg_list : Coqast.t list Gram.Entry.e val ne_intropattern : Coqast.t Gram.Entry.e val ne_num_list : Coqast.t list Gram.Entry.e @@ -152,6 +155,7 @@ module Vernac : val stringarg : Coqast.t Gram.Entry.e val ne_stringarg_list : Coqast.t list Gram.Entry.e val constrarg : Coqast.t Gram.Entry.e + val ne_constrarg_list : Coqast.t list Gram.Entry.e val tacarg : Coqast.t Gram.Entry.e val sortarg : Coqast.t Gram.Entry.e -- cgit v1.2.3