Top used also for fixes.

[helm.git] / matita / components / ng_kernel / nCicExtraction.ml

diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml
index 1bfcf832eefb4ac0f558f183f8d272c9129ab110..df598a6ecb517d2bf4aa1075418c182072227542 100644 (file)
--- 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 (_,_,_,_) -> assert false (* TODO *)
+  | NCic.Meta _ -> assert false (*TODO*)
 ;;
 
 let rec fomega_lift_type_from n k =
@@ -565,7 +570,7 @@ let rec term_of status ~metasenv context =
             let ctx = None::ctx in
             let context = (name,NCic.Decl ty)::context in
              eat_branch 0 t context ctx t'
-         | Top,_ -> assert false (*TODO: HOW??*)
+         | Top,_ -> assert false (* IMPOSSIBLE *)
          | TSkip _, _
          | Forall _,_
          | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
@@ -607,6 +612,23 @@ and eat_args status metasenv acc context tyhe =
              Unit -> UnitTerm
            | _ -> term_of status ~metasenv context arg in
          eat_args status metasenv (mk_appl acc arg) context t tl
+      | Top ->
+         let arg =
+          match classify status ~metasenv context arg with
+           | `PropKind
+           | `Proposition
+           | `Term `TypeFormer
+           | `Term `PropFormer
+           | `Term `Proof
+           | `Type
+           | `KindOrType
+           | `Kind -> UnitTerm
+           | `Term `TypeFormerOrTerm
+           | `Term `Term -> term_of status ~metasenv context arg
+         in
+          eat_args status metasenv
+           (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
+           context Top tl
       | Forall (_,_,t) ->
          (match classify status ~metasenv context arg with
            | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
@@ -623,7 +645,6 @@ and eat_args status metasenv acc context tyhe =
                  tl)
       | TSkip t ->
          eat_args status metasenv acc context t tl
-      | Top -> assert false (*TODO: HOW??*)
       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 ;;
 
@@ -839,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
@@ -875,7 +896,7 @@ let rec pretty_print_type status ctxt =
   function
     | Var n -> List.nth ctxt (n-1)
     | Unit -> "()"
-    | Top -> assert false (* ??? *)
+    | Top -> "Top"
     | TConst ref -> pp_ref status ref
     | Arrow (t1,t2) ->
         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^