From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Aug 2012 09:48:25 +0000 (+0000)
Subject: Fixed pretty-printing of types of variables bound in patterns.
X-Git-Tag: make_still_working~1532
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=906c022e53d47fc28d1b02728ac12170bee0080c;p=helm.git

Fixed pretty-printing of types of variables bound in patterns.
---

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index a0630fd7b..7b24f74c0 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -95,7 +95,7 @@ type term =
   | LetIn of string * (* typ **) term * term
   | Match of reference * term * (term_context * term) list
   | BottomElim
-  | TLambda of (* string **) term
+  | TLambda of string * term
   | Inst of (*typ_former **) term
   | Skip of term
   | UnsafeCoerce of term
@@ -114,12 +114,12 @@ let rec size_of_term =
     | Rel r -> 1
     | UnitTerm -> 1
     | Const c -> 1
-    | Lambda (name, body) -> 1 + size_of_term body
+    | Lambda (_, body) -> 1 + size_of_term body
     | Appl l -> List.length l
-    | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
-    | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
+    | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
+    | Match (_, case, pats) -> 1 + size_of_term case + List.length pats
     | BottomElim -> 1
-    | TLambda t -> size_of_term t
+    | TLambda (_,t) -> size_of_term t
     | Inst t -> size_of_term t
     | Skip t -> size_of_term t
     | UnsafeCoerce t -> 1 + size_of_term t
@@ -426,7 +426,7 @@ let rec term_of status ~metasenv context =
      (* CSC: non-invariant assumed here about "_" *)
      (match classify status ~metasenv context ty with
        | `Kind ->
-           TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
+           TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
        | `KindOrType (* ??? *)
        | `Type ->
            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
@@ -481,12 +481,12 @@ let rec term_of status ~metasenv context =
          (*CSC: unify the three cases below? *)
          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
            let ctx =
-            (Some (name,`OfType Unit(*(typ_of status ~metasenv context ty)*)))::ctx in
+            (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
            let context = (name,NCic.Decl ty)::context in
             eat_branch 0 t context ctx t'
          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
            let ctx =
-            (Some (name,`OfKind Type(*(kind_of status ~metasenv context ty)*)))::ctx in
+            (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
            let context = (name,NCic.Decl ty)::context in
             eat_branch 0 t context ctx t'
          | TSkip t,NCic.Lambda (name, ty, t') ->
@@ -856,8 +856,10 @@ let rec pretty_print_term status ctxt =
                in
                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
              ) pl)
-    | Skip t
-    | TLambda t -> pretty_print_term status (""@::ctxt) t
+    | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
+    | TLambda (name,t) ->
+       let name = capitalize `TypeVariable name in
+        pretty_print_term status (name@::ctxt) t
     | Inst t -> pretty_print_term status ctxt t
 ;;