Fixed left/right context distinction in inductive types.

[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 58310dfd31ce73da8d4bac207edf2825eefc05cf..d68ff2c4408582c2610dc23d30471e64a0020895 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -73,10 +73,10 @@ let rec size_of_type =
     | Unit -> 1
     | Top -> 1
     | TConst c -> 1
-    | Arrow (l, r) -> 1 + size_of_type l + size_of_type r
+    | Arrow _ -> 2
     | Skip t -> size_of_type t
-    | Forall (name, kind, typ) -> 1 + size_of_type typ
-    | TAppl l -> List.fold_right (+) (List.map size_of_type l) 0
+    | Forall _ -> 2
+    | TAppl l -> 1
 ;;
 
 type term =
@@ -122,7 +122,8 @@ type obj_kind =
  | TermDeclaration of term_former_decl
  | TermDefinition of term_former_def
  | LetRec of obj_kind list
- | Algebraic of (string * typ_context * (string * typ) list) list
+   (* name, left, right, constructors *)
+ | Algebraic of (string * typ_context * typ_context * (string * typ) list) list
 
 type obj = NUri.uri * obj_kind
 
@@ -534,17 +535,23 @@ let object_of_constant status ~metasenv uri height bo ty =
 ;;
 
 let object_of_inductive status ~metasenv uri ind leftno il =
- let tyl =
-  HExtlib.filter_map
-   (fun _,name,arity,cl ->
+ let status,_,rev_tyl =
+  List.fold_left
+   (fun (status,i,res) (_,name,arity,cl) ->
      match classify_not_term status [] arity with
       | `Proposition
       | `KindOrType
       | `Type -> assert false (* IMPOSSIBLE *)
-      | `PropKind -> None
+      | `PropKind -> status,i+1,res
       | `Kind ->
           let arity = kind_of status ~metasenv [] arity in
-          let ctx,_ as res = split_kind_prods [] arity in
+          let ctx,_ = split_kind_prods [] arity in
+          let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
+          let ref =
+           NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
+          let status =
+           status#set_extraction_db
+            (ReferenceMap.add ref (ctx,None) status#extraction_db) in
           let cl =
            List.map
             (fun (_,name,ty) ->
@@ -554,12 +561,12 @@ let object_of_inductive status ~metasenv uri ind leftno il =
                name,ty
             ) cl
           in
-           Some (name,ctx,cl)
-   ) il
+           status,i+1,(name,left,right,cl)::res
+   ) (status,0,[]) il
  in
-  match tyl with
-     [] -> status,None
-   | _ -> status, Some (uri, Algebraic tyl)
+  match rev_tyl with
+     [] -> status,Erased
+   | _ -> status, Success (uri, Algebraic (List.rev rev_tyl))
 ;;
 
 let object_of status (uri,height,metasenv,subst,obj_kind) =
@@ -593,10 +600,7 @@ let object_of status (uri,height,metasenv,subst,obj_kind) =
           in
             status, Success (uri,LetRec objs)
         | NCic.Inductive (ind,leftno,il,_) ->
-          let status, obj_of_inductive = object_of_inductive status ~metasenv uri ind leftno il in
-            match obj_of_inductive with
-              | None -> status, Failure "Could not extract an inductive type."
-              | Some s -> status, Success s
+           object_of_inductive status ~metasenv uri ind leftno il
 
 (************************ HASKELL *************************)
 
@@ -712,7 +716,7 @@ let rec (@:::) name l =
   let name = if name = "" then "a" else name in
    name @::: l
  else if List.mem name l then (name ^ "'") @::: l
- else name,l
+ else if name="" then "[erased]",l else name,l
 ;;
 
 let (@::) x l = let x,l = x @::: l in x::l;;
@@ -746,6 +750,9 @@ let rec pretty_print_term status ctxt =
     | LetIn (name,s,t) ->
       "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t
     | Match (r,matched,pl) ->
+      if pl = [] then
+       "error \"Case analysis over empty type\""
+      else
       let constructors, leftno =
       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
       let _,_,_,cl  = List.nth tys n in
@@ -791,15 +798,15 @@ type term_former_decl = term_context * typ
 
 let rec pp_obj status (uri,obj_kind) =
   let pretty_print_context ctx =
-    String.concat " " (List.rev
+    String.concat " " (List.rev (snd
       (List.fold_right
-       (fun (x,kind) l ->
+       (fun (x,kind) (l,res) ->
          let x,l = x @:::l in
          if size_of_kind kind > 1 then
-          ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
+          x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
          else
-          x::l)
-       (HExtlib.filter_map (fun x -> x) ctx) []))
+          x::l,x::res)
+       (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
   in
  let namectx_of_ctx ctx =
   List.fold_right (@::)
@@ -834,12 +841,13 @@ let rec pp_obj status (uri,obj_kind) =
  | Algebraic il ->
     String.concat "\n"
      (List.map
-      (fun _name,ctx,cl ->
+      (fun _name,left,right,cl ->
         (*CSC: BUG always uses the name of the URI *)
-        "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " where\n  " ^
+        "data " ^ name_of_uri `TypeName uri ^ " " ^
+        pretty_print_context (right@left) ^ " where\n  " ^
         String.concat "\n  " (List.map
          (fun name,tys ->
-           let namectx = namectx_of_ctx ctx in
+           let namectx = namectx_of_ctx left in
             capitalize `Constructor name ^ " :: " ^
              pretty_print_type status namectx tys
          ) cl