Last known bug unrelated to names fixed: a fixpoint that creates a type used

to be extracted in the wrong way.

diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml
index c186aef3c96d5b94e321db0f295a433b575936e8..7fa80b5bbc46852f604f7a547f1b064dbfdf16e2 100644 (file)
--- a/matita/components/ng_extraction/extraction.ml
+++ b/matita/components/ng_extraction/extraction.ml
@@ -1151,22 +1151,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 _ ->
+         (*let n = type_scheme_nb_args status [] typ in*)
+         (*let ids = iterate (fun l -> anonymous_name::l) n [] in*)
+         let ids = [] 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
@@ -1277,17 +1289,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) =

diff --git a/matita/components/ng_extraction/extraction.mli b/matita/components/ng_extraction/extraction.mli
index efb2c63da01c3b964e274cd2f625feb4eecbc5c9..a5ab1b05545d4464171e1f455e99b98eb2bf7292 100644 (file)
--- a/matita/components/ng_extraction/extraction.mli
+++ b/matita/components/ng_extraction/extraction.mli
@@ -16,4 +16,4 @@ open OcamlExtractionTable
 
 val extract:
  #OcamlExtractionTable.status as 'status -> NCic.obj ->
-  'status * ml_decl option * ml_spec list
+  'status * ml_decl list * ml_spec list

diff --git a/matita/components/ng_extraction/ocamlExtraction.ml b/matita/components/ng_extraction/ocamlExtraction.ml
index 1d672c49d80409b050ef958e722f6ce54333b4d5..0022599a8dd4c503508a7f6ddceeaa025faf9fd0 100644 (file)
--- a/matita/components/ng_extraction/ocamlExtraction.ml
+++ b/matita/components/ng_extraction/ocamlExtraction.ml
@@ -10,15 +10,13 @@ let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) =
       let status,cmds = Ocaml.pp_spec status ml in
       print_ppcmds ~in_ml:false status (cmds ++ fnl () ++ fnl ());
       status,()) resl in
-  match res with
-     None ->
-(*    print_ppcmds status
-       (str("(* " ^ NUri.string_of_uri uri ^ " non informative *)\n")++ fnl ());*)
-      status
-   | Some ml ->
-      let status,std_ppcmds = Ocaml.pp_decl status ml in
-      print_ppcmds status ~in_ml:true (std_ppcmds ++ fnl ());
-      status
+  let status,_ =
+   map_status status
+    (fun status ml ->
+      let status,cmds = Ocaml.pp_decl status ml in
+      print_ppcmds ~in_ml:true status (cmds ++ fnl ());
+      status,()) res in
+  status
  with
   HExtlib.Localized (_,exn) ->
    prerr_endline (Printexc.to_string exn); assert false