X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=038d75d9c7afd1862bfc0909ee002fd019d158b6;hb=7666f9dddfcaca5671dd25d3cd2095481968c7bf;hp=8828a03216bb74c64b71db833276fdd8c500d662;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 8828a0321..038d75d9c 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -110,34 +110,12 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
 	  (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))          
           (pp_patterns status patterns)
     | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2)
-    | Ast.LetIn ((var,t2), t1, t3) ->
+    | Ast.LetIn ((var,_t2), t1, t3) ->
 (*       let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *)
         sprintf "let %s \\def %s in %s" (pp_term var)
 (*           (pp_term ~pp_parens:true t2) *)
           (pp_term ~pp_parens:true t1)
           (pp_term ~pp_parens:true t3)
-    | Ast.LetRec (kind, definitions, term) ->
-	let rec get_guard i = function
-	   | []                   -> (*assert false*) Ast.Implicit `JustOne
-	   | [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 `JustOne
-           | 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 pp_term) 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 map definitions))
-          (pp_term term)
     | Ast.Ident (name, Some []) | Ast.Ident (name, None)
     | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
     | Ast.NRef nref -> NReference.string_of_reference nref
@@ -273,8 +251,8 @@ and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
   | Ast.IdentVar s -> "ident " ^ s
   | Ast.TermVar (s,Ast.Self _) -> s
-  | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l 
-  | Ast.Ascription (t, n) -> assert false
+  | Ast.TermVar (_s,Ast.Level l) -> "term " ^string_of_int l 
+  | Ast.Ascription (_t, _n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
 let _pp_term = ref (pp_term ~pp_parens:false)
@@ -297,8 +275,13 @@ let pp_fields pp_term fields =
       pp_term ty)
     fields)
 
+let string_of_source = function
+   | `Provided  -> ""
+   | `Implied   -> "implied "
+   | `Generated -> "generated "
+
 let pp_obj pp_term = function
- | Ast.Inductive (params, types) ->
+ | Ast.Inductive (params, types, source) ->
     let pp_constructors constructors =
       String.concat "\n"
         (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
@@ -312,22 +295,48 @@ let pp_obj pp_term = function
     | [] -> assert false
     | (name, inductive, typ, constructors) :: tl ->
         let fst_typ_pp =
-          sprintf "%sinductive %s%s: %s \\def\n%s"
+          sprintf "%s%sinductive %s%s: %s \\def\n%s"
+            (string_of_source source)
             (if inductive then "" else "co") name (pp_params pp_term params)
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (flavour, name, typ, body,_) ->
-    sprintf "%s %s:\n %s\n%s"
+ | Ast.Theorem (name, typ, body,(source, flavour, _)) ->
+    sprintf "%s%s %s:\n %s\n%s"
+      (string_of_source source)
       (NCicPp.string_of_flavour flavour)
       name
       (pp_term typ)
       (match body with
       | None -> ""
       | Some body -> "\\def\n " ^ pp_term body)
- | Ast.Record (params,name,ty,fields) ->
+ | Ast.Record (params,name,ty,fields, source) ->
+    string_of_source source ^
     "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ 
     " \\def {" ^ pp_fields pp_term fields ^ "\n}"
+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
+    let rec get_guard i = function
+       | []                   -> assert false (* Ast.Implicit `JustOne *)
+       | [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 -> assert false (* Ast.Implicit `JustOne *)
+       | Some typ -> typ
+     in
+       sprintf "%s %s on %s: %s \\def %s" 
+	  (pp_term id)
+	  (String.concat " " (List.map (pp_capture_variable pp_term) params))
+	  (pp_term (get_guard i params))
+	  (pp_term typ) (pp_term body)
+    in
+    sprintf "%s%s %s %s"
+      (string_of_source source)
+      (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+      (NCicPp.string_of_flavour flavour)
+      (String.concat " and " (List.map map definitions))
 
 let rec pp_value (status: #NCic.status) = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term status t)