From d737336c89a9942ebe97a834ff87861c8907d6ab Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Aug 2012 16:11:37 +0000
Subject: [PATCH] Match in classification of non-terms taken in account. We
 take the sup of the classification of all branches according to the order

`Proposition < `PropKind < `Type < `Kind < `KindOrType
---
 matita/components/ng_kernel/nCicExtraction.ml | 27 ++++++++++++++++---
 1 file changed, 23 insertions(+), 4 deletions(-)

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index c4ecc87d5..4336d800f 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -142,6 +142,22 @@ type obj = NReference.reference * obj_kind
 let dummyref =
  NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
 
+type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
+
+let max_not_term t1 t2 =
+ match t1,t2 with
+    `KindOrType,_
+  | _,`KindOrType -> `KindOrType
+  | `Kind,_
+  | _,`Kind -> `Kind
+  | `Type,_
+  | _,`Type -> `Type
+  | `PropKind,_
+  | _,`PropKind -> `PropKind
+  | `Proposition,`Proposition -> `Proposition
+
+let sup = List.fold_left max_not_term `Proposition
+
 let rec classify_not_term status context t =
  match NCicReduction.whd status ~subst:[] context t with
   | NCic.Sort s ->
@@ -155,11 +171,16 @@ let rec classify_not_term status context t =
      classify_not_term status ((b,NCic.Decl s)::context) t
   | NCic.Implicit _
   | NCic.LetIn _
-  | NCic.Lambda _
   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
   | NCic.Appl [] ->
      assert false (* NOT POSSIBLE *)
-  | NCic.Match _
+  | NCic.Lambda (n,s,t) ->
+     (* Lambdas can me met in branches of matches, expecially when the
+        output type is a product *)
+     classify_not_term status ((n,NCic.Decl s)::context) t
+  | NCic.Match (r,_,_,pl) ->
+     let classified_pl = List.map (classify_not_term status context) pl in
+      sup classified_pl
   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
      (* be aware: we can be the head of an application *)
      assert false (* TODO *)
@@ -207,8 +228,6 @@ let rec classify_not_term status context t =
      assert false (* IMPOSSIBLE *)
 ;;
 
-type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
-
 let classify status ~metasenv context t =
  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
   | NCic.Sort _ ->
-- 
2.39.2