]> matita.cs.unibo.it Git - helm.git/blobdiff - components/acic_content/cicNotationPp.ml
Wildcard patterns implemented in case analysis. The following term is now
[helm.git] / components / acic_content / cicNotationPp.ml
index 2873912c0129d51b9b17e9a6f2f3aae80c144797..4bd2f93ed2c633a8e0bb902d83e9bf50189301d6 100644 (file)
@@ -176,20 +176,24 @@ let rec pp_term ?(pp_parens = true) t =
 and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term)
 and pp_substs substs = String.concat "; " (List.map pp_subst substs)
 
-and pp_pattern ((head, href, vars), term) =
-  let head_pp =
-    head ^
-    (match debug_printing, href with
-    | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-    | _ -> "")
-  in
-  sprintf "%s \\Rightarrow %s"
-    (match vars with
-    | [] -> head_pp
-    | _ ->
-        sprintf "(%s %s)" head_pp
-          (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
-    (pp_term term)
+and pp_pattern =
+ function
+    Ast.Pattern (head, href, vars), term ->
+     let head_pp =
+       head ^
+       (match debug_printing, href with
+       | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+       | _ -> "")
+     in
+     sprintf "%s \\Rightarrow %s"
+       (match vars with
+       | [] -> head_pp
+       | _ ->
+           sprintf "(%s %s)" head_pp
+             (String.concat " " (List.map (pp_capture_variable pp_term) vars)))
+       (pp_term term)
+  | Ast.Wildcard, term ->
+     sprintf "_ \\Rightarrow %s" (pp_term term)
 
 and pp_patterns patterns =
   sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns))