Basics/logic.ma no longer raises exception.

[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 7b24f74c0c741b799f29dd6d95f7318bd1eac82f..53498362ec48caa582f1ab87c4793861963ce264 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -157,7 +157,8 @@ let rec classify_not_term status context t =
   | NCic.LetIn _
   | NCic.Lambda _
   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
-  | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
+  | NCic.Appl [] ->
+     assert false (* NOT POSSIBLE *)
   | NCic.Match _
   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
      (* be aware: we can be the head of an application *)
@@ -328,17 +329,21 @@ let rec split_typ_lambdas status n ~metasenv context typ =
 ;;
 
 
-let context_of_typformer status ~metasenv context =
+let rev_context_of_typformer status ~metasenv context =
  function
     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
-     (try fst (ReferenceMap.find ref status#extraction_db)
+     (try List.rev (fst (ReferenceMap.find ref status#extraction_db))
       with
        Not_found ->
-        prerr_endline ("REF NOT FOUND: " ^ NReference.string_of_reference ref);
-        assert false (* IMPOSSIBLE *))
+        (* This can happen only when we are processing the type of
+           the constructor of a small singleton type. In this case
+           we are not interested in all the type, but only in its
+           backbone. That is why we can safely return the dummy context here *)
+        let rec dummy = None::dummy in
+        dummy)
   | NCic.Match _ -> assert false (* TODO ???? *)
   | NCic.Rel n ->
      let typ =
@@ -347,7 +352,7 @@ let context_of_typformer status ~metasenv context =
        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
      let typ_ctx = snd (HExtlib.split_nth n context) in
      let typ = kind_of status ~metasenv typ_ctx typ in
-      fst (split_kind_prods [] typ)
+      List.rev (fst (split_kind_prods [] typ))
   | NCic.Meta _ -> assert false (* TODO *)
   | NCic.Const (NReference.Ref (_,NReference.Con _))
   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
@@ -378,11 +383,11 @@ let rec typ_of status ~metasenv context k =
   | NCic.Rel n -> Var n
   | NCic.Const ref -> TConst ref
   | NCic.Appl (he::args) ->
-     let he_context = context_of_typformer status ~metasenv context he in
+     let rev_he_context= rev_context_of_typformer status ~metasenv context he in
      TAppl (typ_of status ~metasenv context he ::
       List.map
        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
-       (skip_args status ~metasenv context (List.rev he_context,args)))
+       (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 _
@@ -534,8 +539,19 @@ and eat_args status metasenv acc context tyhe =
            | _ -> term_of status ~metasenv context arg in
          eat_args status metasenv (mk_appl acc arg) context t tl
       | Forall (_,_,t) ->
-         eat_args status metasenv (Inst acc)
-          context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
+         (match classify status ~metasenv context arg with
+           | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
+           | `Proposition
+           | `Term `TypeFormer
+           | `Kind ->
+               eat_args status metasenv (UnsafeCoerce (Inst acc))
+                context (fomega_subst 1 Unit t) tl
+           | `Term _ -> assert false (*TODO: ????*)
+           | `KindOrType
+           | `Type ->
+               eat_args status metasenv (Inst acc)
+                context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
+                 tl)
       | TSkip t ->
          eat_args status metasenv acc context t tl
       | Top -> assert false (*TODO: HOW??*)