1. Some warnings about unused warning fixed (hopefully well)

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

diff --git a/components/acic_content/cicNotationPp.ml b/components/acic_content/cicNotationPp.ml
index 8a2d1de709013b6aa771580d806679c33a80a3a9..49cefaec7db3f7f76652d9e24e9543bd4de9f495 100644 (file)
--- a/components/acic_content/cicNotationPp.ml
+++ b/components/acic_content/cicNotationPp.ml
@@ -99,7 +99,6 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Case (term, indtype, typ, patterns) ->
         sprintf "match %s%s%s with %s"
           (pp_term term)
-         (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (match indtype with
           | None -> ""
           | Some (ty, href_opt) ->
@@ -107,7 +106,8 @@ let rec pp_term ?(pp_parens = true) t =
               (match debug_printing, href_opt with
               | true, Some uri ->
                   sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
-              | _ -> ""))
+              | _ -> ""))        
+         (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
     | Ast.LetIn (var, t1, t2) ->
@@ -120,7 +120,12 @@ let rec pp_term ?(pp_parens = true) t =
              | body                                 -> List.rev l, body
           in 
           aux i [] t
-       in      
+       in
+       let rec get_guard i = function
+          | []                   -> assert false
+          | [term, _] when i = 1 -> term
+          | _ :: tl              -> get_guard (pred i) tl
+       in
        let map (var, body, i) =
            let id, vars, typ, body = match var with
              | term, Some typ ->
@@ -129,9 +134,10 @@ let rec pp_term ?(pp_parens = true) t =
                 term, pvars, pbody, bbody
              | _              -> assert false
           in
-          sprintf "%s %s: %s \\def %s" 
+          sprintf "%s %s on %s: %s \\def %s" 
              (pp_term ~pp_parens:false term)
              (String.concat " " (List.map pp_capture_variable vars))
+             (pp_term ~pp_parens:false (get_guard i vars))
              (pp_term typ) (pp_term body)
        in
        sprintf "let %s %s in %s"
@@ -165,6 +171,7 @@ let rec pp_term ?(pp_parens = true) t =
   in
   match pp_parens, t with
     | false, _ 
+    | true, Ast.Implicit
     | true, Ast.Sort _
     | true, Ast.Ident (_, Some []) 
     | true, Ast.Ident (_, None)    -> t_pp
@@ -282,8 +289,11 @@ let pp_fields fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
     (List.map 
-      (fun (name,ty,coercion) -> 
-        " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
+      (fun (name,ty,coercion,arity) -> 
+        " " ^ name ^ 
+        if coercion then (":" ^ 
+          if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
+        pp_term ty) fields)
         
 let pp_obj = function
  | Ast.Inductive (params, types) ->
@@ -306,13 +316,13 @@ let pp_obj = function
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
  | Ast.Theorem (flavour, name, typ, body) ->
-    sprintf "%s %s: %s %s"
+    sprintf "%s %s:\n %s\n%s"
       (pp_flavour flavour)
       name
       (pp_term typ)
       (match body with
       | None -> ""
-      | Some body -> "\\def " ^ pp_term body)
+      | Some body -> "\\def\n " ^ pp_term body)
  | Ast.Record (params,name,ty,fields) ->
     "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ 
     " \\def {" ^ pp_fields fields ^ "\n}"