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 c4ecc87d50232da0527b1fe67dcfef4f1658e037..df598a6ecb517d2bf4aa1075418c182072227542 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -124,8 +124,6 @@ let rec size_of_term =
     | Skip t -> size_of_term t
     | UnsafeCoerce t -> 1 + size_of_term t
 ;;
-let unitty =
- NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
 
 type obj_kind =
    TypeDeclaration of typ_former_decl
@@ -142,6 +140,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,15 +169,23 @@ 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 *)
+     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 =
@@ -207,8 +229,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 _ ->
@@ -382,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 ::
@@ -390,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 =
@@ -548,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!*)
@@ -590,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???*)
@@ -606,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 *)
 ;;
 
@@ -822,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
@@ -858,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 ^ " -> " ^