Bug fixed: when extracting pattern matching on singleton types it is possible

[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 a0630fd7bdbdf192ce7b08b99c871a64676edec1..7f76392caf7b4faee2a819b9b466a24b0c0e4ff4 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -95,7 +95,7 @@ type term =
   | LetIn of string * (* typ **) term * term
   | Match of reference * term * (term_context * term) list
   | BottomElim
-  | TLambda of (* string **) term
+  | TLambda of string * term
   | Inst of (*typ_former **) term
   | Skip of term
   | UnsafeCoerce of term
@@ -114,12 +114,12 @@ let rec size_of_term =
     | Rel r -> 1
     | UnitTerm -> 1
     | Const c -> 1
-    | Lambda (name, body) -> 1 + size_of_term body
+    | Lambda (_, body) -> 1 + size_of_term body
     | Appl l -> List.length l
-    | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
-    | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
+    | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
+    | Match (_, case, pats) -> 1 + size_of_term case + List.length pats
     | BottomElim -> 1
-    | TLambda t -> size_of_term t
+    | TLambda (_,t) -> size_of_term t
     | Inst t -> size_of_term t
     | Skip t -> size_of_term t
     | UnsafeCoerce t -> 1 + size_of_term t
@@ -328,17 +328,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 +351,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 +382,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 _
@@ -426,7 +430,7 @@ let rec term_of status ~metasenv context =
      (* CSC: non-invariant assumed here about "_" *)
      (match classify status ~metasenv context ty with
        | `Kind ->
-           TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
+           TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
        | `KindOrType (* ??? *)
        | `Type ->
            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
@@ -481,12 +485,12 @@ let rec term_of status ~metasenv context =
          (*CSC: unify the three cases below? *)
          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
            let ctx =
-            (Some (name,`OfType Unit(*(typ_of status ~metasenv context ty)*)))::ctx in
+            (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
            let context = (name,NCic.Decl ty)::context in
             eat_branch 0 t context ctx t'
          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
            let ctx =
-            (Some (name,`OfKind Type(*(kind_of status ~metasenv context ty)*)))::ctx in
+            (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
            let context = (name,NCic.Decl ty)::context in
             eat_branch 0 t context ctx t'
          | TSkip t,NCic.Lambda (name, ty, t') ->
@@ -856,8 +860,10 @@ let rec pretty_print_term status ctxt =
                in
                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
              ) pl)
-    | Skip t
-    | TLambda t -> pretty_print_term status (""@::ctxt) t
+    | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
+    | TLambda (name,t) ->
+       let name = capitalize `TypeVariable name in
+        pretty_print_term status (name@::ctxt) t
     | Inst t -> pretty_print_term status ctxt t
 ;;