From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Aug 2012 08:44:25 +0000 (+0000)
Subject: Top used also for fixes.
X-Git-Tag: make_still_working~1522
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b089671a552882bb0666fe6291b339fd5684d523;p=helm.git

Top used also for fixes.
---

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index c2d51b0bf..df598a6ec 100644
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -180,9 +180,12 @@ let rec classify_not_term status context t =
      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 *)
+     assert false (* IMPOSSIBLE *)
   | NCic.Meta _ -> assert false (* TODO *)
+  | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)->
+     let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
+     let _,_,_,_,bo = List.nth l i in
+      classify_not_term status [] bo
   | NCic.Appl (he::_) -> classify_not_term status context he
   | NCic.Rel n ->
      let rec find_sort typ =
@@ -399,6 +402,9 @@ let rec typ_of status ~metasenv context k =
   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
   | NCic.Rel n -> Var n
   | NCic.Const ref -> TConst ref
+  | NCic.Match (_,_,_,_)
+  | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) ->
+     Top
   | NCic.Appl (he::args) ->
      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
      TAppl (typ_of status ~metasenv context he ::
@@ -407,8 +413,7 @@ let rec typ_of status ~metasenv context k =
        (skip_args status ~metasenv context (rev_he_context,args)))
   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
                                    otherwise NOT A TYPE *)
-  | NCic.Meta _
-  | NCic.Match (_,_,_,_) -> Top
+  | NCic.Meta _ -> assert false (*TODO*)
 ;;
 
 let rec fomega_lift_type_from n k =
@@ -621,7 +626,8 @@ and eat_args status metasenv acc context tyhe =
            | `Term `TypeFormerOrTerm
            | `Term `Term -> term_of status ~metasenv context arg
          in
-          eat_args status metasenv (UnsafeCoerce (mk_appl acc arg))
+          eat_args status metasenv
+           (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
            context Top tl
       | Forall (_,_,t) ->
          (match classify status ~metasenv context arg with
@@ -854,8 +860,8 @@ let classify_reference status ref =
   if ReferenceMap.mem ref status#extraction_db then
     `TypeName
   else
-   let NReference.Ref (_,ref) = ref in
-    match ref with
+   let NReference.Ref (_,r) = ref in
+    match r with
        NReference.Con _ -> `Constructor
      | NReference.Ind _ -> assert false
      | _ -> `FunctionName