...

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index 6d70c22c98ef09e80f5bb52e685fea06f4eef762..4bd2f93ed2c633a8e0bb902d83e9bf50189301d6 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -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))
@@ -263,6 +267,7 @@ let pp_params pp_term = function
       
 let pp_flavour = function
   | `Definition -> "definition"
+  | `MutualDefinition -> assert false
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -301,6 +306,8 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Ast.Theorem (`MutualDefinition, name, typ, body) ->
+    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body) ->
     sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)