No pattern matching over empty types in Haskell

[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 cbcc24c244f7cfda08f5880ce1516e6e47600ba7..32f5bc35e6fd28cfcf6a4318268cd922c3607d59 100644 (file)
--- a/matita/components/ng_kernel/nCicExtraction.ml
+++ b/matita/components/ng_kernel/nCicExtraction.ml
@@ -122,7 +122,7 @@ 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) list
+ | Algebraic of (string * typ_context * (string * typ) list) list
 
 type obj = NUri.uri * obj_kind
 
@@ -534,23 +534,37 @@ 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
-           Some (name,ctx,[])
-   ) il
+          let ctx,_ = split_kind_prods [] arity 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) ->
+              let ctx,ty =
+               NCicReduction.split_prods status ~subst:[] [] leftno ty in
+              let ty = typ_of status ~metasenv ctx ty in
+               name,ty
+            ) cl
+          in
+           status,i+1,(name,ctx,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) =
@@ -584,10 +598,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 *************************)
 
@@ -697,15 +708,17 @@ let name_of_uri classification uri =
  capitalize classification (NUri.name_of_uri uri)
 
 (* cons avoid duplicates *)
-let rec (@::) name l =
+let rec (@:::) name l =
  if name <> "" (* propositional things *) && name.[0] = '_' then
   let name = String.sub name 1 (String.length name - 1) in
   let name = if name = "" then "a" else name in
-   name @:: l
- else if List.mem name l then (name ^ "'") @:: l
- else name::l
+   name @::: l
+ else if List.mem name l then (name ^ "'") @::: l
+ else name,l
 ;;
 
+let (@::) x l = let x,l = x @::: l in x::l;;
+
 let rec pretty_print_type status ctxt =
   function
     | Var n -> List.nth ctxt (n-1)
@@ -735,6 +748,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
@@ -781,8 +797,14 @@ type term_former_decl = term_context * typ
 let rec pp_obj status (uri,obj_kind) =
   let pretty_print_context ctx =
     String.concat " " (List.rev
-      (List.fold_right (fun (x,kind) l -> x @:: l)
-        (HExtlib.filter_map (fun x -> x) ctx) []))
+      (List.fold_right
+       (fun (x,kind) l ->
+         let x,l = x @:::l in
+         if size_of_kind kind > 1 then
+          ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
+         else
+          x::l)
+       (HExtlib.filter_map (fun x -> x) ctx) []))
   in
  let namectx_of_ctx ctx =
   List.fold_right (@::)
@@ -819,20 +841,21 @@ let rec pp_obj status (uri,obj_kind) =
      (List.map
       (fun _name,ctx,cl ->
         (*CSC: BUG always uses the name of the URI *)
-        "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^
-        String.concat " | " (List.map
+        "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " where\n  " ^
+        String.concat "\n  " (List.map
          (fun name,tys ->
-          capitalize `Constructor name ^
-           String.concat " " (List.map (pretty_print_type status []) tys)
+           let namectx = namectx_of_ctx ctx in
+            capitalize `Constructor name ^ " :: " ^
+             pretty_print_type status namectx tys
          ) cl
       )) il)
  (* inductive and records missing *)
 
-let haskell_of_obj status obj =
+let haskell_of_obj status (uri,_,_,_,_ as obj) =
  let status, obj = object_of status obj in
   status,
    match obj with
-      Erased -> "-- [?] Erased due to term being propositionally irrelevant.\n"
-    | OutsideTheory -> "-- [?] Erased due to image of term under extraction residing outside Fω.\n"
-    | Failure msg -> "-- [!] FAILURE: " ^ msg ^ "\n"
+      Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
+    | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
+    | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
     | Success o -> pp_obj status o ^ "\n"