Merge remote-tracking branch 'origin/ld-0.99.3'

[helm.git] / matita / components / ng_extraction / extraction.ml

diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml
index c186aef3c96d5b94e321db0f295a433b575936e8..be8099598e31eb5e804d482cb0c270518ffae94b 100644 (file)
--- a/matita/components/ng_extraction/extraction.ml
+++ b/matita/components/ng_extraction/extraction.ml
@@ -207,7 +207,7 @@ let sign_with_implicits _r s =
 
 (* Enriching a exception message *)
 
-let rec handle_exn _r _n _fn_name = function x -> x
+let handle_exn _r _n _fn_name = function x -> x
 (*CSC: only for pretty printing
   | MLexn s ->
       (try Scanf.sscanf s "UNBOUND %d"
@@ -1014,7 +1014,7 @@ and extract_case context mle (ip,c,br) status mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n m status context c t =
+let decomp_lams_eta_n n m status context c t =
   let rels = fst (splay_prod_n status context n t) in
   let rels',c = decompose_lam c in
   let d = n - m in
@@ -1142,6 +1142,13 @@ let extract_fixpoint_common uri height fix_or_cofix ifl =
        NReference.reference_of_spec uri (NReference.CoFix i)) in
   ti,ci,n,vkn
 
+(*s Is a [ml_spec] logical ? *)
+let logical_spec = function
+  | Stype (_, [], Some (Tdummy _)) -> true
+  | Sval (_,Tdummy _) -> true
+  | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | _ -> false
+
 let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
   let status =
    if is_projection then
@@ -1151,22 +1158,34 @@ let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
      confirm_projection status ref
    else
     status in
-  let ti,ci,n,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
-  let types = Array.make n (Tdummy Kother)
-  and terms = Array.make n MLdummy in
+  let ti,ci,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
   current_fixpoints := Some uri;
-  let status = ref status in
-  for i = 0 to n-1 do
-    if sort_of !status [] ti.(i) <> InProp then begin
-      let status',e,t = extract_std_constant !status vkn.(i) ci.(i) ti.(i) in
-      status := status';
-      terms.(i) <- e;
-      types.(i) <- t;
-    end
-  done;
-  let status = !status in
+  let status,res = array_mapi_status status
+   (fun status i _ ->
+     let _,head = split_all_prods status ~subst:[] [] ti.(i) in
+     match head with
+        NCic.Sort s when classify_sort s = InProp -> status,`None
+      | NCic.Sort _ ->
+         let n = type_scheme_nb_args status [] ti.(i) in
+         let ids = iterate (fun l -> anonymous_name::l) n [] in
+         status,`Type (Dtype (vkn.(i), ids, Tunknown))
+      | _ ->
+        if sort_of status [] ti.(i) <> InProp then
+         let status,e,t = extract_std_constant status vkn.(i) ci.(i) ti.(i) in
+          status,`Some (e,t)
+        else
+          status,`None
+   ) ti in
+  let axioms,terms,types =
+   Array.fold_right
+    (fun x ((axioms,terms,types) as res) ->
+      match x with
+         `None -> res
+       | `Some (t,ty) -> axioms,t::terms,ty::types
+       | `Type decl -> decl::axioms,terms,types
+    ) res ([],[],[]) in
   current_fixpoints := None;
-  status,Dfix (vkn, terms, types)
+  status,axioms @ [Dfix (vkn, Array.of_list terms, Array.of_list types)]
 
 let extract_fixpoint_spec status uri height fix_or_cofix ifl =
   let ti,_,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
@@ -1175,7 +1194,7 @@ let extract_fixpoint_spec status uri height fix_or_cofix ifl =
     (fun status i vkn ->
       if sort_of status [] ti.(i) <> InProp then begin
        let status,spec = extract_constant_spec status vkn None ti.(i) in
-       status, Some spec
+       status, if logical_spec spec then None else Some spec
       end
      else status,None
     ) vkn in
@@ -1256,14 +1275,6 @@ let logical_decl = function
   | Dind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
-(*s Is a [ml_spec] logical ? *)
-
-let logical_spec = function
-  | Stype (_, [], Some (Tdummy _)) -> true
-  | Sval (_,Tdummy _) -> true
-  | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
-  | _ -> false
-
 let extract_impl status (uri,height,metasenv,subst,obj_kind) =
  assert (metasenv=[]);
  assert (subst=[]);
@@ -1277,17 +1288,18 @@ let extract_impl status (uri,height,metasenv,subst,obj_kind) =
          | Some _ -> NReference.Def height
        in NReference.reference_of_spec uri spec
       in
-       extract_constant status r bo typ
+      let status,res = extract_constant status r bo typ in
+       status,[res]
    | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
       let status,res =
        extract_inductive status uri inductive ind_pragma leftno types
       in
-       status,Dind res
+       status,[Dind res]
    | NCic.Fixpoint (fix_or_cofix,ifl,(_,_,def_pragma)) ->
       extract_fixpoint status uri height fix_or_cofix
        (def_pragma = `Projection) ifl
  in
-  status, if logical_decl decl then None else Some decl
+  status, List.filter (fun decl -> not (logical_decl decl)) decl
 ;;
 
 let extract_spec status (uri,height,metasenv,subst,obj_kind) =