diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-15 10:13:31 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
commit | e61e2dffaac5f5ffbffdbd87c3d3466bd9a2e83b (patch) | |
tree | b257b75eb0c8670b3b653c3b97acca8277cd021c | |
parent | f86e6618b62769b1c3e78175f95f882d3960d54b (diff) | |
download | compcert-e61e2dffaac5f5ffbffdbd87c3d3466bd9a2e83b.tar.gz compcert-e61e2dffaac5f5ffbffdbd87c3d3466bd9a2e83b.zip |
ndfun: add support for guards on patterns
Syntax is "pat ?? bexpr => action".
The whole case is selected only when "pat" matches and then "bexpr"
evaluates to "true".
-rw-r--r-- | tools/ndfun.ml | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/tools/ndfun.ml b/tools/ndfun.ml index 2b8bcb19..b6a87ede 100644 --- a/tools/ndfun.ml +++ b/tools/ndfun.ml @@ -41,7 +41,9 @@ let trim s = let str_match n re s = if not (Str.string_match re s 0) then [||] else begin let res = Array.make (n+1) "" in - for i = 1 to n do res.(i) <- Str.matched_group i s done; + for i = 1 to n do + res.(i) <- (try Str.matched_group i s with Not_found -> "") + done; for i = 1 to n do res.(i) <- trim res.(i) done; res end @@ -87,6 +89,11 @@ let match_temps args = let parenpats p = "(" ^ Str.global_replace re_comma ") (" p ^ ")" +(* "foo, bar, gee" -> "_ _ _" *) + +let underscores_for s = + Str.global_replace re_arg "_" (remove_commas s) + (* Extract the bound variables in a pattern. Heuristic: any identifier that starts with a lowercase letter and is not "nil". *) @@ -123,7 +130,7 @@ let re_nd = Str.regexp( let re_split_cases = Str.regexp "|" -let re_case = Str.regexp "\\(.*\\)=>\\(.*\\)" +let re_case = Str.regexp "\\([^?]*\\)\\(\\?\\?\\(.*\\)\\)?=>\\(.*\\)" let re_default_pat = Str.regexp "[ _,]*$" @@ -165,16 +172,20 @@ let transl_ndfun filename lineno s = (* Adding each case *) let numcase = ref 0 in let transl_case s = - let res = str_match 2 re_case s in + let res = str_match 4 re_case s in if Array.length res = 0 then error filename lineno ("ill-formed case: " ^ s); - let patlist = res.(1) and rhs = res.(2) in + let patlist = res.(1) and guard = res.(3) and rhs = res.(4) in let bv = boundvarspat patlist in if not (Str.string_match re_default_pat patlist 0) then begin incr numcase; bprintf a " | %s_case%d: forall %s, %s_cases %s\n" name !numcase bv name (parenpats patlist); - bprintf b " | %s => %s_case%d %s\n" patlist name !numcase bv; + if guard = "" then + bprintf b " | %s => %s_case%d %s\n" patlist name !numcase bv + else + bprintf b " | %s => if %s then %s_case%d %s else %s_default %s\n" + patlist guard name !numcase bv name (underscores_for args); bprintf c " | %s_case%d %s => (* %s *) \n" name !numcase bv patlist; bprintf c " %s\n" rhs end else begin |