X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPp.ml;h=47bfe2748693c07975996bd6f7662fb91ddc44d4;hb=774c8d18f41e71ae7e26a90d726d10a6f95de1fe;hp=efcc25897b4b0301081a03665670c30e0f05fc1a;hpb=ce6cdbb31ba6a38e72194dd8bcb5107eba13122d;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index efcc25897..47bfe2748 100644
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/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,20 +106,34 @@ 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) ->
         sprintf "let %s \\def %s in %s" (pp_capture_variable var) (pp_term ~pp_parens:true t1)
           (pp_term ~pp_parens:true t2)
     | Ast.LetRec (kind, definitions, term) ->
-        sprintf "let %s %s in %s"
+	let rec get_guard i = function
+	   | []                   -> (*assert false*) Ast.Implicit
+	   | [term, _] when i = 1 -> term
+	   | _ :: tl              -> get_guard (pred i) tl
+	in
+	let map (params, (id,typ), body, i) =
+         let typ =
+          match typ with
+             None -> Ast.Implicit
+           | Some typ -> typ
+         in
+	   sprintf "%s %s on %s: %s \\def %s" 
+	      (pp_term ~pp_parens:false term)
+	      (String.concat " " (List.map pp_capture_variable params))
+	      (pp_term ~pp_parens:false (get_guard i params))
+	      (pp_term typ) (pp_term body)
+	in
+	sprintf "let %s %s in %s"
           (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
-          (String.concat " and "
-            (List.map
-              (fun (var, body, _) ->
-                sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
-              definitions))
+          (String.concat " and " (List.map map definitions))
           (pp_term term)
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
     | Ast.Uri (name, Some []) | Ast.Uri (name, None) ->
@@ -149,6 +162,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
@@ -245,15 +259,10 @@ let set_pp_term f = _pp_term := f
 
 let pp_params = function
   | [] -> ""
-  | params ->
-      " " ^
-      String.concat " "
-        (List.map
-          (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
-          params)
+  | params -> " " ^ String.concat " " (List.map pp_capture_variable params)
       
 let pp_flavour = function
-  | `Definition -> "Definition"
+  | `Definition -> "definition"
   | `Fact -> "fact"
   | `Goal -> "goal"
   | `Lemma -> "lemma"
@@ -266,8 +275,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) ->
@@ -290,16 +302,16 @@ 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 ^ " \\def {" ^
-    pp_fields fields ^ "}"
+    "record " ^ name ^ " " ^ pp_params params ^ ": " ^ pp_term ty ^ 
+    " \\def {" ^ pp_fields fields ^ "\n}"
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)