matita/components/ng_extraction/extraction.ml

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (*i $Id: extraction.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
  10
  11 open Coq
  12 open Miniml
  13 open OcamlExtractionTable
  14 open Mlutil
  15 open Common
  16
  17 (* A set of all fixpoint functions currently being extracted *)
  18 (*CSC: very imperative, fix/check?*)
  19 let current_fixpoints = ref (None : NUri.uri option)
  20
  21 let whd_betadeltaiota status context t =
  22  NCicReduction.whd status ~subst:[] context t
  23
  24 let whd_betaiotazeta status context t =
  25  NCicReduction.whd status ~delta:max_int ~subst:[] context t
  26
  27 let isRel = function NCic.Rel _ -> true | _ -> false
  28
  29 let rec split_all_prods status ~subst context te =
  30   match NCicReduction.whd status ~subst context te with
  31    | NCic.Prod (name,so,ta) ->
  32        split_all_prods status ~subst ((name,(NCic.Decl so))::context) ta
  33    | _ -> context,te
  34 ;;
  35
  36 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  37  * gives n *)
  38 let nb_lam =
  39   let rec nbrec n =
  40    function
  41     | NCic.Lambda (_,_,c) -> nbrec (n+1) c
  42     | _ -> n
  43   in
  44   nbrec 0
  45
  46 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
  47    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
  48 let decompose_lam_n n =
  49   if n < 0 then assert false else
  50   let rec lamdec_rec l n c =
  51     if n=0 then l,c
  52     else match c with
  53       | NCic.Lambda (x,t,c) -> lamdec_rec ((x,NCic.Decl t)::l) (n-1) c
  54       | _ -> assert false
  55   in
  56   lamdec_rec [] n
  57
  58 let decompose_lam =
  59   let rec lamdec_rec l =
  60    function
  61     | NCic.Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
  62     | c                -> l,c
  63   in
  64   lamdec_rec []
  65
  66 let splay_prod_n status context n =
  67   let rec decrec context m ln c = if m = 0 then (ln,c) else
  68     match whd_betadeltaiota status context c with
  69       | NCic.Prod (n,a,c0) ->
  70           decrec ((n,NCic.Decl a)::context)
  71             (m-1) ((n,NCic.Decl a)::ln) c0
  72       | _                      -> invalid_arg "splay_prod_n"
  73   in
  74   decrec context n []
  75
  76 let splay_prod status context =
  77   let rec decrec context m c =
  78     let t = whd_betadeltaiota status context c in
  79     match t with
  80       | NCic.Prod (n,a,c0) ->
  81           decrec ((n,NCic.Decl a)::context) ((n,NCic.Decl a)::m) c0
  82       | _ -> m,t
  83   in
  84   decrec context []
  85
  86 let type_of status context t =
  87  NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
  88
  89 type sorts_family = InProp | InType
  90
  91 let classify_sort =
  92  function
  93     NCic.Prop -> InProp
  94   | NCic.Type u ->
  95      match NCicEnvironment.family_of u with
  96         `CProp -> InProp
  97       | `Type -> InType
  98
  99 let sort_of status context t =
 100  match
 101   NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
 102  with
 103     NCic.Sort s -> classify_sort s
 104   | _ -> assert false
 105
 106 (*S Generation of flags and signatures. *)
 107
 108 (* The type [flag] gives us information about any Coq term:
 109    \begin{itemize}
 110    \item [TypeScheme] denotes a type scheme, that is
 111      something that will become a type after enough applications.
 112      More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
 113      [s = Set], [Prop] or [Type]
 114    \item [Default] denotes the other cases. It may be inexact after
 115      instanciation. For example [(X:Type)X] is [Default] and may give [Set]
 116      after instanciation, which is rather [TypeScheme]
 117    \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
 118    \item [Info] is the opposite. The same example [(X:Type)X] shows
 119      that an [Info] term might in fact be [Logic] later on.
 120    \end{itemize} *)
 121
 122 type info = Logic | Info
 123
 124 type scheme = TypeScheme | Default
 125
 126 type flag = info * scheme
 127
 128 (*s [flag_of_type] transforms a type [t] into a [flag].
 129   Really important function. *)
 130
 131 let rec flag_of_type status context t =
 132   let t = whd_betadeltaiota status context t in
 133   match t with
 134     | NCic.Prod (x,t,c) -> flag_of_type status ((x,NCic.Decl t)::context) c
 135     | NCic.Sort s ->
 136        (match classify_sort s with
 137            InProp -> (Logic,TypeScheme)
 138          | InType -> (Info,TypeScheme))
 139     | _ ->
 140       if (sort_of status context t) = InProp then (Logic,Default)
 141       else (Info,Default)
 142
 143 (*s Two particular cases of [flag_of_type]. *)
 144
 145 let is_default status context t=(flag_of_type status context t= (Info, Default))
 146
 147 exception NotDefault of kill_reason
 148
 149 let check_default status context t =
 150   match flag_of_type status context t with
 151     | _,TypeScheme -> raise (NotDefault Ktype)
 152     | Logic,_ -> raise (NotDefault Kother)
 153     | _ -> ()
 154
 155 let is_info_scheme status context t =
 156  (flag_of_type status context t = (Info, TypeScheme))
 157
 158 (*s [type_sign] generates a signature aimed at treating a type application. *)
 159
 160 let rec type_sign status context c =
 161   match whd_betadeltaiota status context c with
 162     | NCic.Prod (n,t,d) ->
 163         (if is_info_scheme status context t then Keep else Kill Kother)
 164         :: (type_sign status ((n,NCic.Decl t)::context) d)
 165     | _ -> []
 166
 167 let rec type_scheme_nb_args status context c =
 168   match whd_betadeltaiota status context c with
 169     | NCic.Prod (n,t,d) ->
 170         let n = type_scheme_nb_args status ((n,NCic.Decl t)::context) d in
 171         if is_info_scheme status context t then n+1 else n
 172     | _ -> 0
 173
 174 (*CSC: only useful for inline extraction
 175 let _ = register_type_scheme_nb_args type_scheme_nb_args
 176 *)
 177
 178 (*s [type_sign_vl] does the same, plus a type var list. *)
 179
 180 let rec type_sign_vl status context c =
 181   match whd_betadeltaiota status context c with
 182     | NCic.Prod (n,t,d) ->
 183         let s,vl = type_sign_vl status ((n,NCic.Decl t)::context) d in
 184         if not (is_info_scheme status context t) then Kill Kother::s, vl
 185         else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
 186     | _ -> [],[]
 187
 188 let rec nb_default_params status context c =
 189   match whd_betadeltaiota status context c with
 190     | NCic.Prod (n,t,d) ->
 191         let n = nb_default_params status ((n,NCic.Decl t)::context) d in
 192         if is_default status context t then n+1 else n
 193     | _ -> 0
 194
 195 (* Enriching a signature with implicit information *)
 196
 197 let sign_with_implicits _r s =
 198   let implicits = [](*CSC: implicits_of_global r*) in
 199   let rec add_impl i = function
 200     | [] -> []
 201     | sign::s ->
 202         let sign' =
 203           if sign = Keep && List.mem i implicits then Kill Kother else sign
 204         in sign' :: add_impl (succ i) s
 205   in
 206   add_impl 1 s
 207
 208 (* Enriching a exception message *)
 209
 210 let handle_exn _r _n _fn_name = function x -> x
 211 (*CSC: only for pretty printing
 212   | MLexn s ->
 213       (try Scanf.sscanf s "UNBOUND %d"
 214          (fun i ->
 215             assert ((0 < i) && (i <= n));
 216             MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
 217        with _ -> MLexn s)
 218   | a -> ast_map (handle_exn r n fn_name) a*)
 219
 220 (*S Management of type variable contexts. *)
 221
 222 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
 223    into ML type [Tvar]. *)
 224
 225 (*s From a type signature toward a type variable context (db). *)
 226
 227 let db_from_sign s =
 228   let rec make i acc = function
 229     | [] -> acc
 230     | Keep :: l -> make (i+1) (i::acc) l
 231     | Kill _ :: l -> make i (0::acc) l
 232   in make 1 [] s
 233
 234 (*s Create a type variable context from indications taken from
 235   an inductive type (see just below). *)
 236
 237 let rec db_from_ind dbmap i =
 238   if i = 0 then []
 239   else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 240
 241 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
 242   of a constructor corresponds to the j-th type var of the ML inductive. *)
 243
 244 (* \begin{itemize}
 245    \item [si] : signature of the inductive
 246    \item [i] :  counter of Coq args for [(I args)]
 247    \item [j] : counter of ML type vars
 248    \item [relmax] : total args number of the constructor
 249    \end{itemize} *)
 250
 251 let parse_ind_args si args relmax =
 252   let rec parse i j = function
 253     | [] -> Intmap.empty
 254     | Kill _ :: s -> parse (i+1) j s
 255     | Keep :: s ->
 256       (match args.(i-1) with
 257          | NCic.Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
 258          | _ -> parse (i+1) (j+1) s)
 259   in parse 1 1 si
 260
 261 (*S Extraction of a type. *)
 262
 263 (* [extract_type env db c args] is used to produce an ML type from the
 264    coq term [(c args)], which is supposed to be a Coq type. *)
 265
 266 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 267
 268 (* [j] stands for the next ML type var. [j=0] means we do not
 269    generate ML type var anymore (in subterms for example). *)
 270
 271
 272 let rec extract_type status context db j c args =
 273   match whd_betaiotazeta status context c with
 274     | NCic.Appl (d::args') ->
 275         (* We just accumulate the arguments. *)
 276         extract_type status context db j d (args' @ args)
 277     | NCic.Lambda (_,_,d) ->
 278         (match args with
 279            | [] -> assert false (* otherwise the lambda would be reductible. *)
 280            | a :: args -> extract_type status context db j (NCicSubstitution.subst status a d) args)
 281     | NCic.Prod (n,t,d) ->
 282         assert (args = []);
 283         let context' = (n,NCic.Decl t)::context in
 284         (match flag_of_type status context t with
 285            | (Info, Default) ->
 286                (* Standard case: two [extract_type] ... *)
 287                let status,mld = extract_type status context' (0::db) j d [] in
 288                let status,res = expand status mld in
 289                (match res with
 290                   | Tdummy d -> status,Tdummy d
 291                   | _ ->
 292                     let status,res=extract_type status context db 0 t []  in
 293                      status,Tarr (res, mld))
 294            | (Info, TypeScheme) when j > 0 ->
 295                (* A new type var. *)
 296                let status,mld=extract_type status context' (j::db) (j+1) d [] in
 297                let status,res = expand status mld in
 298                status,
 299                (match res with
 300                   | Tdummy d -> Tdummy d
 301                   | _ -> Tarr (Tdummy Ktype, mld))
 302            | _,lvl ->
 303                let status,mld = extract_type status context' (0::db) j d [] in
 304                let status,res = expand status mld in
 305                status,
 306                (match res with
 307                   | Tdummy d -> Tdummy d
 308                   | _ ->
 309                       let reason = if lvl=TypeScheme then Ktype else Kother in
 310                       Tarr (Tdummy reason, mld)))
 311     | NCic.Sort _ -> status,Tdummy Ktype (* The two logical cases. *)
 312     | _ when sort_of status context (NCicUntrusted.mk_appl c args) = InProp ->
 313        status,Tdummy Kother
 314     | NCic.Rel n ->
 315         (match List.nth context (n-1) with
 316            | (_,NCic.Def (t,_)) -> extract_type status context db j (NCicSubstitution.lift status n t) args
 317            | _ ->
 318                (* Asks [db] a translation for [n]. *)
 319                if n > List.length db then status,Tunknown
 320                else let n' = List.nth db (n-1) in
 321                status,if n' = 0 then Tunknown else Tvar n')
 322     | NCic.Const (NReference.Ref (uri,spec) as r) ->
 323        (match spec with
 324            NReference.Decl ->
 325             let _,_,typ,_,_ = NCicEnvironment.get_checked_decl status r in
 326             (match flag_of_type status [] typ with
 327                | (Info, TypeScheme) ->
 328                   extract_type_app status context db
 329                    (r, type_sign status [] typ) args
 330                | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
 331                    status,Tunknown (* Brutal approximation ... *))
 332          | NReference.Def _ ->
 333             let _,_,bo,typ,_,_ = NCicEnvironment.get_checked_def status r in
 334             (match flag_of_type status [] typ with
 335                | (Info, TypeScheme) ->
 336                    let status,mlt =
 337                     extract_type_app status context db
 338                      (r, type_sign status [] typ) args in
 339                    (*CSC: if is_custom r then mlt else*)
 340                    let newc = NCicUntrusted.mk_appl bo args in
 341                    let status,mlt' = extract_type status context db j newc [] in
 342                    (* ML type abbreviations interact badly with Coq *)
 343                    (* reduction, so [mlt] and [mlt'] might be different: *)
 344                    (* The more precise is [mlt'], extracted after reduction *)
 345                    (* The shortest is [mlt], which use abbreviations *)
 346                    (* If possible, we take [mlt], otherwise [mlt']. *)
 347                    let status,res1 = expand status mlt in
 348                    let status,res2 = expand status mlt' in
 349                    if res1=res2 then status,mlt else status,mlt'
 350                | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
 351                       (* We try to reduce. *)
 352                       let newc = NCicUntrusted.mk_appl bo args in
 353                       extract_type status context db j newc [])
 354          | NReference.Fix _ -> status,Tunknown
 355          | NReference.Con _
 356          | NReference.CoFix _ -> assert false
 357          | NReference.Ind (_,i,_) ->
 358             let status,ind = extract_ind status uri in
 359             let s = ind.ind_packets.(i).ip_sign in
 360              extract_type_app status context db (r,s) args)
 361     | NCic.Match _ -> status,Tunknown
 362     | _ -> assert false
 363
 364 (*s Auxiliary function dealing with type application.
 365   Precondition: [r] is a type scheme represented by the signature [s],
 366   and is completely applied: [List.length args = List.length s]. *)
 367
 368 and extract_type_app status context db (r,s) args =
 369   let status,ml_args =
 370     List.fold_right
 371       (fun (b,c) (status,a) ->
 372         if b=Keep then
 373          let p =
 374           List.length
 375            (fst (splay_prod status context (type_of status context c))) in
 376          let db = iterate (fun l -> 0 :: l) p db in
 377          let status,res = extract_type_scheme status context db c p in
 378           status,res::a
 379         else status,a)
 380       (List.combine s args) (status,[])
 381   in status, Tglob (r,  ml_args)
 382
 383 (*S Extraction of a type scheme. *)
 384
 385 (* [extract_type_scheme env db c p] works on a Coq term [c] which is
 386   an informative type scheme. It means that [c] is not a Coq type, but will
 387   be when applied to sufficiently many arguments ([p] in fact).
 388   This function decomposes p lambdas, with eta-expansion if needed. *)
 389
 390 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 391
 392 and extract_type_scheme status context db c p =
 393   if p=0 then extract_type status context db 0 c []
 394   else
 395     let c = whd_betaiotazeta status context c in
 396     match c with
 397       | NCic.Lambda (n,t,d) ->
 398           extract_type_scheme status((n,NCic.Decl t)::context) db d (p-1)
 399       | _ ->
 400           let rels=fst (splay_prod status context (type_of status context c)) in
 401           let context = rels@context in
 402           let eta_args = List.rev_map (fun x -> NCic.Rel x) (interval 1 p) in
 403           extract_type status context db 0 (NCicSubstitution.lift status p c)
 404            eta_args
 405
 406
 407 (*S Extraction of an inductive type. *)
 408
 409 and extract_ind status uri =
 410  try
 411   status,lookup_ind status uri
 412  with Not_found ->
 413   let _,_,_,_,obj = NCicEnvironment.get_checked_obj status uri in
 414   match obj with
 415      NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
 416       extract_ind0 status uri inductive ind_pragma leftno types
 417    | _ -> assert false
 418
 419 and extract_ind0 status uri inductive ind_pragma leftno types =
 420     (* First, if this inductive is aliased via a Module, *)
 421     (* we process the original inductive. *)
 422     (* Everything concerning parameters. *)
 423     (* We do that first, since they are common to all the [mib]. *)
 424     let _,_,mipty0,_ = List.hd types in
 425     let mipcontext,_=NCicReduction.split_prods status ~subst:[] [] ~-1 mipty0 in
 426     let epar_rev,_= HExtlib.split_nth leftno (List.rev mipcontext) in
 427     let epar = List.rev epar_rev in
 428     (* First pass: we store inductive signatures together with *)
 429     (* their type var list. *)
 430     let packets =
 431       Array.mapi
 432         (fun tyno (_,name,arity,kl) ->
 433            let _,sort=NCicReduction.split_prods status ~subst:[] [] ~-1 arity in
 434            let sort=match sort with NCic.Sort sort -> sort | _ ->assert false in
 435            let b = classify_sort sort <> InProp in
 436            let s,v = if b then type_sign_vl status [] arity else [],[] in
 437            let t = Array.make (List.length kl) [] in
 438            let kl = Array.of_list kl in
 439            let spec = NReference.Ind (inductive,tyno,leftno) in
 440            let ref = NReference.reference_of_spec uri spec in
 441            { ip_reference = ref;
 442              ip_consreferences =
 443               Array.mapi
 444                (fun i _ ->
 445                  NReference.reference_of_spec uri
 446                   (NReference.Con (tyno,i+1,leftno))
 447                ) kl;
 448              ip_typename = name;
 449              ip_consnames= Array.map (fun (_,name,_) -> name) kl;
 450              ip_logical = (not b);
 451              ip_sign = s;
 452              ip_vars = v;
 453              ip_types = t
 454            })
 455         (Array.of_list types)
 456     in
 457     let status = add_ind ~dummy:true status uri
 458       {ind_kind = Standard;
 459        ind_nparams = leftno;
 460        ind_packets = packets
 461       } in
 462     (* Second pass: we extract constructors *)
 463     let rec aux1 i status =
 464      if i = List.length types then status
 465      else begin
 466       let p = packets.(i) in
 467       let _,_,_,cl = List.nth types i in
 468       if not p.ip_logical then
 469         let ktypes = Array.of_list (List.map (fun (_,_,arity) -> arity) cl) in
 470         let rec aux2 j status =
 471          if j = Array.length ktypes then status
 472          else begin
 473           let tctx,t =
 474            NCicReduction.split_prods status ~subst:[] [] leftno ktypes.(j) in
 475           let prods,head = split_all_prods status ~subst:[] tctx t in
 476           let nprods = List.length prods in
 477           let args = match head with
 478             | NCic.Appl (_f::args) -> Array.of_list args (* [f = Ind ip] *)
 479             | _ -> [||]
 480           in
 481           let dbmap = parse_ind_args p.ip_sign args nprods in
 482           let db = db_from_ind dbmap leftno in
 483           let status,res = extract_type_cons status epar db dbmap t (leftno+1)in
 484           p.ip_types.(j) <- res;
 485           aux2 (j+1) status
 486          end
 487         in
 488          let status = aux2 0 status in
 489          aux1 (i+1) status
 490       else begin
 491        aux1 (i+1) status
 492       end
 493      end in
 494     let status = aux1 0 status in
 495     (* Third pass: we determine special cases. *)
 496     let status,ind_info =
 497      (*CSC: let ip = (kn, 0) in
 498      let r = IndRef ip in
 499      if is_custom r then raise_I status Standard;*)
 500      if not inductive then status,Coinductive else
 501      if List.length types <> 1 then status,Standard else
 502      let p = packets.(0) in
 503      if p.ip_logical then status,Standard else
 504      if Array.length p.ip_types <> 1 then status,Standard else
 505      let typ = p.ip_types.(0) in
 506      let status,l =
 507       List.fold_right
 508        (fun x (status,res) ->
 509          let status,y = expand status x in
 510           status,y::res
 511        ) typ (status,[]) in
 512      let l = List.filter (fun t -> not (isDummy t)) l in
 513      if List.length l = 1 && not (type_mem_kn uri (List.hd l))
 514      then status,Singleton else
 515      if l = [] then status,Standard else
 516      (match ind_pragma with
 517          `Regular -> status,Standard
 518        | `Record fields ->
 519            let baseuri = NUri.baseuri_of_uri uri in
 520            let field_names = List.map (fun (n,_,_) -> n) fields in
 521            assert (List.length field_names = List.length typ);
 522            let rec select_fields status l typs = match l,typs with
 523              | [],[] -> status,[]
 524              | id::l, typ::typs ->
 525                 let status,res = expand status typ in
 526                 if isDummy res then
 527                  select_fields status l typs
 528                 else
 529                  (* Is it safe to use [id] for projections [foo.id] ? *)
 530                  let status,res = type2signature status typ in
 531                  let fielduri =
 532                   NUri.uri_of_string (baseuri ^ "/" ^ id ^ ".con") in
 533                  let fieldfakeref =
 534                   NReference.reference_of_spec fielduri fake_spec in
 535 (*
 536                  let ref =
 537                   try
 538                    let fieldspec =
 539                     let (_,height,_,_,obj) =
 540                      NCicEnvironment.get_checked_obj status fielduri
 541                     in
 542                      match obj with
 543                         NCic.Fixpoint (_,fs,(_,_,`Projection)) ->
 544                          let _,_,recparamno,_,_ = List.nth fs 0 in
 545                          NReference.Fix (0,recparamno,height)
 546                       | _ -> assert false
 547                    in
 548                     NReference.reference_of_spec fielduri fieldspec
 549                   with NCicEnvironment.ObjectNotFound _ ->
 550                     assert false
 551                  in *)
 552                  let status =
 553                   if List.for_all ((=) Keep) res
 554                   then
 555                    let n = nb_default_params status [] mipty0 in
 556                     guess_projection status fielduri n
 557                   else status in
 558                  let status,res = select_fields status l typs in
 559                  status, fieldfakeref::res
 560              | _ -> assert false
 561            in
 562            let status,field_glob = select_fields status field_names typ in
 563            (* Is this record officially declared with its projections ? *)
 564            (* If so, we use this information. *)
 565            status, Record field_glob)
 566     in
 567     let i = {ind_kind = ind_info;
 568              ind_nparams = leftno;
 569              ind_packets = packets
 570             } in
 571     let status = add_ind status uri i in
 572      status,i
 573
 574 (*s [extract_type_cons] extracts the type of an inductive
 575   constructor toward the corresponding list of ML types.
 576
 577    - [db] is a context for translating Coq [Rel] into ML type [Tvar]
 578    - [dbmap] is a translation map (produced by a call to [parse_in_args])
 579    - [i] is the rank of the current product (initially [params_nb+1])
 580 *)
 581
 582 and extract_type_cons status context db dbmap c i =
 583   match whd_betadeltaiota status context c with
 584     | NCic.Prod (n,t,d) ->
 585         let context' = (n,NCic.Decl t)::context in
 586         let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
 587         let status,l = extract_type_cons status context' db' dbmap d (i+1) in
 588         let status, res = extract_type status context db 0 t [] in
 589         status, res::l
 590     | _ -> status,[]
 591
 592 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 593
 594 and mlt_env status r =
 595  try
 596   if false (*CSC:XXX not (visible_con kn)*) then raise Not_found;
 597   match lookup_term status r with
 598    | Dtype (_,_vl,mlt) -> Some (status,mlt)
 599    | _ -> None
 600  with Not_found ->
 601   match r with
 602      NReference.Ref (_,NReference.Def _) ->
 603       let _,_,body,typ,_,_ = NCicEnvironment.get_checked_def status r in
 604        (match flag_of_type status [] typ with
 605           | Info,TypeScheme ->
 606               let s,vl = type_sign_vl status [] typ in
 607               let db = db_from_sign s in
 608               let status,t =
 609                extract_type_scheme status [] db body (List.length s) in
 610               let status = add_term status r (Dtype (r, vl, t)) in
 611                Some (status,t)
 612           | _ -> None)
 613    | NReference.Ref (_,NReference.Decl) -> None
 614    | NReference.Ref (_,NReference.Fix _)
 615    | NReference.Ref (_,NReference.CoFix _) -> assert false
 616    | NReference.Ref (_,NReference.Ind _)
 617    | NReference.Ref (_,NReference.Con _) -> None
 618
 619 and expand status = type_expand status mlt_env
 620 and type2signature status = type_to_signature status mlt_env
 621 let type2sign status = type_to_sign status mlt_env
 622 let type_expunge status = type_expunge status mlt_env
 623 let type_expunge_from_sign status = type_expunge_from_sign status mlt_env
 624
 625 (*s Extraction of the type of a constant. *)
 626
 627 let type_of_constant status (NReference.Ref (uri,spec)) =
 628  let (_,_,_,_,obj) = NCicEnvironment.get_checked_obj status uri in
 629  match obj,spec with
 630     NCic.Constant (_,_,_,typ,_),_ -> typ
 631   | NCic.Fixpoint (_,fs,_), (NReference.Fix (n,_,_) | NReference.CoFix n) ->
 632      let _,_,_,typ,_ = List.nth fs n in
 633       typ
 634   | _ -> assert false
 635
 636 let record_constant_type status r opt_typ =
 637   try
 638 (*CSC:XXX to be implemented?    if not (visible_con kn) then raise Not_found;*)
 639     status,lookup_type status r
 640   with Not_found ->
 641     let typ = match opt_typ with
 642       | None -> type_of_constant status r
 643       | Some typ -> typ in
 644     let status,mlt = extract_type status [] [] 1 typ [] in
 645     let schema = (type_maxvar mlt, mlt) in
 646     let status = add_type status r schema in
 647      status,schema
 648
 649 (*S Extraction of a term. *)
 650
 651 (* Precondition: [(c args)] is not a type scheme, and is informative. *)
 652
 653 (* [mle] is a ML environment [Mlenv.t]. *)
 654 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 655
 656 let rec extract_term status context mle mlt c args =
 657   match c with
 658       NCic.Appl [] -> assert false
 659     | NCic.Appl (f::a) ->
 660         extract_term status context mle mlt f (a@args)
 661     | NCic.Lambda (n, t, d) ->
 662         let id = n in
 663         (match args with
 664            | a :: l ->
 665                (* We make as many [LetIn] as possible. *)
 666                 let d' = NCic.LetIn (id,t,a,NCic.Appl (d::(List.map (NCicSubstitution.lift status 1) l)))
 667                in extract_term status context mle mlt d' []
 668            | [] ->
 669                let context' = (id, NCic.Decl t)::context in
 670                let id, a =
 671                  try check_default status context t; Id id, new_meta()
 672                  with NotDefault d -> Dummy, Tdummy d
 673                in
 674                let b = new_meta () in
 675                (* If [mlt] cannot be unified with an arrow type, then magic! *)
 676                let magic = needs_magic (mlt, Tarr (a, b)) in
 677                let status,d' =
 678                 extract_term status context' (Mlenv.push_type mle a) b d [] in
 679                status,put_magic_if magic (MLlam (id, d')))
 680     | NCic.LetIn (n, t1, c1, c2) ->
 681         let id = n in
 682         let context' = (id, NCic.Def (c1, t1))::context in
 683         let args' = List.map (NCicSubstitution.lift status 1) args in
 684         (try
 685           check_default status context t1;
 686           let a = new_meta () in
 687           let status,c1' = extract_term status context mle a c1 [] in
 688           (* The type of [c1'] is generalized and stored in [mle]. *)
 689           let mle' =
 690             if generalizable c1'
 691             then Mlenv.push_gen mle a
 692             else Mlenv.push_type mle a
 693           in
 694           let status,res = extract_term status context' mle' mlt c2 args' in
 695           status,MLletin (Id id, c1', res)
 696         with NotDefault d ->
 697           let mle' = Mlenv.push_std_type mle (Tdummy d) in
 698           let status,res = extract_term status context' mle' mlt c2 args' in
 699           status,ast_pop res)
 700     | NCic.Const ((NReference.Ref (uri,
 701        ( NReference.Decl
 702        | NReference.Def _
 703        | NReference.Fix _
 704        | NReference.CoFix _ ))) as ref) ->
 705         extract_cst_app status context mle mlt uri ref args
 706     | NCic.Const ((NReference.Ref (_,(NReference.Con _))) as ref) ->
 707         extract_cons_app status context mle mlt ref args
 708     | NCic.Rel n ->
 709         (* As soon as the expected [mlt] for the head is known, *)
 710         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
 711         let extract_rel status mlt =
 712          status,put_magic (mlt, Mlenv.get mle n) (MLrel n)
 713         in extract_app status context mle mlt extract_rel args
 714     | NCic.Match (ref,_,c0,br) ->
 715          extract_app status context mle mlt
 716          (extract_case context mle (ref,c0,Array.of_list br)) args
 717     | NCic.Const (NReference.Ref (_,NReference.Ind _))
 718     | NCic.Prod _
 719     | NCic.Sort _
 720     | NCic.Implicit _
 721     | NCic.Meta _ -> assert false
 722
 723 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
 724
 725 and extract_maybe_term status context mle mlt c =
 726   try check_default status context (type_of status context c);
 727     extract_term status context mle mlt c []
 728   with NotDefault d ->
 729     status,put_magic (mlt, Tdummy d) MLdummy
 730
 731 (*s Generic way to deal with an application. *)
 732
 733 (* We first type all arguments starting with unknown meta types.
 734    This gives us the expected type of the head. Then we use the
 735    [mk_head] to produce the ML head from this type. *)
 736
 737 and extract_app status context mle mlt mk_head args =
 738   let metas = List.map new_meta args in
 739   let type_head = type_recomp (metas, mlt) in
 740   let status,mlargs =
 741    List.fold_right2
 742     (fun x y (status,res) ->
 743       let status,z = extract_maybe_term status context mle x y in
 744        status,z::res
 745     ) metas args (status,[]) in
 746   let status,res = mk_head status type_head in
 747   status,mlapp res mlargs
 748
 749 (*s Auxiliary function used to extract arguments of constant or constructor. *)
 750
 751 and make_mlargs status context e s args typs =
 752   let rec f status = function
 753     | [], [], _ -> status,[]
 754     | a::la, t::lt, [] ->
 755        let status,res = extract_maybe_term status context e t a in
 756        let status,res2 = f status (la,lt,[]) in
 757        status, res :: res2
 758     | a::la, t::lt, Keep::s ->
 759        let status,res = extract_maybe_term status context e t a in
 760        let status,res2 = f status (la,lt,s) in
 761         status, res :: res2
 762     | _::la, _::lt, _::s -> f status (la,lt,s)
 763     | _ -> assert false
 764   in f status (args,typs,s)
 765
 766 (*s Extraction of a constant applied to arguments. *)
 767
 768 and extract_cst_app status context mle mlt uri ref args =
 769   (* First, the [ml_schema] of the constant, in expanded version. *)
 770   let status,(nb,t) = record_constant_type status ref None in
 771   let status,res = expand status t in
 772   let schema = nb, res in
 773   (* Can we instantiate types variables for this constant ? *)
 774   (* In Ocaml, inside the definition of this constant, the answer is no. *)
 775   let instantiated =
 776     if
 777      match !current_fixpoints with None -> false | Some uri' -> NUri.eq uri uri'
 778     then var2var' (snd schema)
 779     else instantiation schema
 780   in
 781   (* Then the expected type of this constant. *)
 782   let a = new_meta () in
 783   (* We compare stored and expected types in two steps. *)
 784   (* First, can [kn] be applied to all args ? *)
 785   let metas = List.map new_meta args in
 786   let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
 787   (* Second, is the resulting type compatible with the expected type [mlt] ? *)
 788   let magic2 = needs_magic (a, mlt) in
 789   (* The internal head receives a magic if [magic1] *)
 790   let head = put_magic_if magic1 (MLglob ref) in
 791   (* Now, the extraction of the arguments. *)
 792   let status,s_full = type2signature status (snd schema) in
 793   let s_full = sign_with_implicits ref s_full in
 794   let s = sign_no_final_keeps s_full in
 795   let ls = List.length s in
 796   let la = List.length args in
 797   (* The ml arguments, already expunged from known logical ones *)
 798   let status,mla = make_mlargs status context mle s args metas in
 799   let mla =
 800     if not magic1 then
 801       try
 802         let l,l' = list_chop (projection_arity status ref) mla in
 803         if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 804         else mla
 805       with _ -> mla
 806     else mla
 807   in
 808   (* For strict languages, purely logical signatures with at least
 809      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
 810      accordingly. *)
 811   let optdummy = match sign_kind s_full with
 812     | UnsafeLogicalSig -> [MLdummy]
 813     | _ -> []
 814   in
 815   (* Different situations depending of the number of arguments: *)
 816   if la >= ls
 817   then
 818     (* Enough args, cleanup already done in [mla], we only add the
 819        additionnal dummy if needed. *)
 820     status,put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
 821   else
 822     (* Partially applied function with some logical arg missing.
 823        We complete via eta and expunge logical args. *)
 824     let ls' = ls-la in
 825     let s' = list_skipn la s in
 826     let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
 827     let e = anonym_or_dummy_lams (mlapp head mla) s' in
 828     status,put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
 829
 830 (*s Extraction of an inductive constructor applied to arguments. *)
 831
 832 (* \begin{itemize}
 833    \item In ML, contructor arguments are uncurryfied.
 834    \item We managed to suppress logical parts inside inductive definitions,
 835    but they must appears outside (for partial applications for instance)
 836    \item We also suppressed all Coq parameters to the inductives, since
 837    they are fixed, and thus are not used for the computation.
 838    \end{itemize} *)
 839
 840 and extract_cons_app status context mle mlt ref (*(((kn,i) as ip,j) as cp)*) args =
 841   let uri,i,j =
 842    match ref with
 843       NReference.Ref (uri,NReference.Con(i,j,_)) -> uri,i,j
 844     | _ -> assert false in
 845   let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
 846   let tyref = NReference.mk_indty b ref in
 847   (* First, we build the type of the constructor, stored in small pieces. *)
 848   let status,mi = extract_ind status uri in
 849   let params_nb = mi.ind_nparams in
 850   let oi = mi.ind_packets.(i) in
 851   let nb_tvars = List.length oi.ip_vars in
 852   let status,types =
 853    List.fold_right
 854     (fun x (status,res) ->
 855       let status,y = expand status x in
 856        status,y::res
 857     ) oi.ip_types.(j-1) (status,[]) in
 858   let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
 859   let type_cons = type_recomp (types, Tglob (tyref, list_tvar)) in
 860   let type_cons = instantiation (nb_tvars, type_cons) in
 861   (* Then, the usual variables [s], [ls], [la], ... *)
 862   let status,s =
 863    List.fold_right
 864     (fun x (status,res) ->
 865       let status,y = type2sign status x in
 866        status,y::res)
 867     types (status,[]) in
 868   let s = sign_with_implicits ref s in
 869   let ls = List.length s in
 870   let la = List.length args in
 871   assert (la <= ls + params_nb);
 872   let la' = max 0 (la - params_nb) in
 873   let args' = list_lastn la' args in
 874   (* Now, we build the expected type of the constructor *)
 875   let metas = List.map new_meta args' in
 876   (* If stored and expected types differ, then magic! *)
 877   let a = new_meta () in
 878   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
 879   let magic2 = needs_magic (a, mlt) in
 880   let head status mla =
 881     if mi.ind_kind = Singleton then
 882       status, put_magic_if magic1 (List.hd mla)
 883     else
 884       let status,typeargs = match snd (type_decomp type_cons) with
 885         | Tglob (_,l) ->
 886            List.fold_right
 887             (fun x (status,res) ->
 888               let status,y = type_simpl status x in
 889                status,y::res)
 890             l (status,[])
 891         | _ -> assert false
 892       in
 893       let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
 894       status, put_magic_if magic1 (MLcons (info, ref, mla))
 895   in
 896   (* Different situations depending of the number of arguments: *)
 897   if la < params_nb then
 898     let status,head' = head status (eta_args_sign ls s) in
 899     status,
 900     put_magic_if magic2
 901       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
 902   else
 903     let status,mla = make_mlargs status context mle s args' metas in
 904     if la = ls + params_nb
 905     then
 906      let status,res = head status mla in
 907       status,put_magic_if (magic2 && not magic1) res
 908     else (* [ params_nb <= la <= ls + params_nb ] *)
 909       let ls' = params_nb + ls - la in
 910       let s' = list_lastn ls' s in
 911       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
 912       let status,res = head status mla in
 913        status,put_magic_if magic2 (anonym_or_dummy_lams res s')
 914
 915 (*S Extraction of a case. *)
 916
 917 and extract_case context mle (ip,c,br) status mlt =
 918   (* [br]: bodies of each branch (in functional form) *)
 919   (* [ni]: number of arguments without parameters in each branch *)
 920   let uri,i =
 921    match ip with
 922       NReference.Ref (uri,NReference.Ind (_,i,_)) -> uri,i
 923     | _ -> assert false
 924   in
 925   let br_size = Array.length br in
 926   if br_size = 0 then begin
 927     (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
 928     status,MLexn "absurd case"
 929   end else
 930     (* [c] has an inductive type, and is not a type scheme type. *)
 931     let t = type_of status context c in
 932     (* The only non-informative case: [c] is of sort [Prop] *)
 933     if (sort_of status context t) = InProp then
 934       begin
 935         (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
 936         (* Logical singleton case: *)
 937         (* [match c with C i j k -> t] becomes [t'] *)
 938         assert (br_size = 1);
 939         let ni =
 940          let _,leftno,tys,_,_ = NCicEnvironment.get_checked_indtys status ip in
 941          let _,_,_,cl = List.hd tys in
 942          let _,_,cty = List.hd cl in
 943          let prods,_ = split_all_prods status ~subst:[] [] cty in
 944          List.length prods - leftno
 945         in
 946         let s = iterate (fun l -> Kill Kother :: l) ni [] in
 947         let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni mlt in
 948         let status,e = extract_maybe_term status context mle mlt br.(0) in
 949         status, snd (case_expunge s e)
 950       end
 951     else
 952       let status,mi = extract_ind status uri in
 953       let oi = mi.ind_packets.(i) in
 954       let metas = Array.init (List.length oi.ip_vars) new_meta in
 955       (* The extraction of the head. *)
 956       let type_head = Tglob (ip, Array.to_list metas) in
 957       let status,a = extract_term status context mle type_head c [] in
 958       (* The extraction of each branch. *)
 959       let extract_branch status i =
 960         let r = NReference.mk_constructor (i+1) ip in
 961         (* The types of the arguments of the corresponding constructor. *)
 962         let f status t =
 963          let status,res = expand status t in
 964          status,type_subst_vect metas res in
 965         let status,l =
 966          List.fold_right
 967           (fun x (status,res) ->
 968             let status,y = f status x in
 969              status,y::res)
 970           oi.ip_types.(i) (status,[]) in
 971         (* the corresponding signature *)
 972         let status,s =
 973          List.fold_right
 974           (fun x (status,res) ->
 975             let status,y = type2sign status x in
 976              status,y::res)
 977           oi.ip_types.(i) (status,[]) in
 978         let s = sign_with_implicits r s in
 979         (* Extraction of the branch (in functional form). *)
 980         let status,e =
 981          extract_maybe_term status context mle (type_recomp (l,mlt)) br.(i) in
 982         (* We suppress dummy arguments according to signature. *)
 983         let ids,e = case_expunge s e in
 984         let e' = handle_exn r (List.length s) (fun _ -> "_") e in
 985         status,(r, List.rev ids, e')
 986       in
 987       if mi.ind_kind = Singleton then
 988         begin
 989           (* Informative singleton case: *)
 990           (* [match c with C i -> t] becomes [let i = c' in t'] *)
 991           assert (br_size = 1);
 992           let status,(_,ids,e') = extract_branch status 0 in
 993           assert (List.length ids = 1);
 994           status,MLletin (tmp_id (List.hd ids),a,e')
 995         end
 996       else
 997         (* Standard case: we apply [extract_branch]. *)
 998         let status,typs = List.fold_right
 999          (fun x (status,res) ->
1000            let status,y = type_simpl status x in
1001             status,y::res)
1002          (Array.to_list metas) (status,[]) in
1003         let info={ m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone } in
1004         let status,res =
1005          array_fold_right_i
1006           (fun i _ (status,res) ->
1007             let status,y = extract_branch status i in
1008              status,y::res) br (status,[])
1009         in
1010          status,MLcase (info, a, Array.of_list res)
1011
1012 (*S ML declarations. *)
1013
1014 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
1015    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
1016
1017 let decomp_lams_eta_n n m status context c t =
1018   let rels = fst (splay_prod_n status context n t) in
1019   let rels',c = decompose_lam c in
1020   let d = n - m in
1021   (* we'd better keep rels' as long as possible. *)
1022   let rels=(list_firstn d rels)@(List.map (fun (n,t) -> n, NCic.Decl t) rels')in
1023   let eta_args = List.rev_map (fun n -> NCic.Rel n) (interval 1 d) in
1024   rels, NCic.Appl ((NCicSubstitution.lift status d c)::eta_args)
1025
1026 (* Let's try to identify some situation where extracted code
1027    will allow generalisation of type variables *)
1028
1029 let rec gentypvar_ok c =
1030  match c with
1031   | NCic.Lambda _ -> true
1032   | NCic.Const (NReference.Ref (_,
1033      (NReference.Decl
1034      |NReference.Def _
1035      |NReference.Fix _
1036      |NReference.CoFix _))) -> true
1037   | NCic.Appl (c::v) ->
1038       (* if all arguments are variables, these variables will
1039          disappear after extraction (see [empty_s] below) *)
1040       List.for_all isRel v && gentypvar_ok c
1041   | _ -> false
1042
1043 (*s From a constant to a ML declaration. *)
1044
1045 let extract_std_constant status uri body typ =
1046   reset_meta_count ();
1047   (* The short type [t] (i.e. possibly with abbreviations). *)
1048   let status,res = record_constant_type status uri (Some typ) in
1049   let t = snd res in
1050   (* The real type [t']: without head products, expanded, *)
1051   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
1052   let status,res = expand status (var2var' t) in
1053   let l,t' = type_decomp res in
1054   let status,s =
1055    List.fold_right
1056     (fun x (status,res) ->
1057       let status,y = type2sign status x in
1058        status,y::res)
1059     l (status,[]) in
1060   (* Check for user-declared implicit information *)
1061   let s = sign_with_implicits uri(*CSC: (ConstRef uri)*) s in
1062   (* Decomposing the top level lambdas of [body].
1063      If there isn't enough, it's ok, as long as remaining args
1064      aren't to be pruned (and initial lambdas aren't to be all
1065      removed if the target language is strict). In other situations,
1066      eta-expansions create artificially enough lams (but that may
1067      break user's clever let-ins and partial applications). *)
1068   let rels, c =
1069     let n = List.length s
1070     and m = nb_lam body in
1071     if n <= m then decompose_lam_n n body
1072     else
1073       let s,s' = list_split_at m s in
1074       if List.for_all ((=) Keep) s' && sign_kind s <> UnsafeLogicalSig
1075       then decompose_lam_n m body
1076       else decomp_lams_eta_n n m status [] body typ
1077   in
1078   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
1079   let rels, c =
1080     let n = List.length rels in
1081     let s,s' = list_split_at n s in
1082     let k = sign_kind s in
1083     let empty_s = (k = EmptySig || k = SafeLogicalSig) in
1084     if empty_s && not (gentypvar_ok c) && s' <> [] && type_maxvar t <> 0
1085     then decomp_lams_eta_n (n+1) n status [] body typ
1086     else rels,c
1087   in
1088   let n = List.length rels in
1089   let s = list_firstn n s in
1090   let l,l' = list_split_at n l in
1091   let t' = type_recomp (l',t') in
1092   (* The initial ML environment. *)
1093   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
1094   (* The lambdas names. *)
1095   let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in
1096   (* The according Coq environment. *)
1097   let context = rels in
1098   (* The real extraction: *)
1099   let status,e = extract_term status context mle t' c [] in
1100   (* Expunging term and type from dummy lambdas. *)
1101   let trm = term_expunge s (ids,e) in
1102   let trm = handle_exn uri n (fun i -> fst (List.nth rels (i-1))) trm in
1103   let status,res = type_expunge_from_sign status s t in
1104   status,trm,res
1105
1106 let extract_constant_spec status r bo typ =
1107   match flag_of_type status [] typ with
1108     | (Logic, TypeScheme) ->
1109        status,Stype (r, [], Some (Tdummy Ktype))
1110     | (Logic, Default) -> status,Sval (r, Tdummy Kother)
1111     | (Info, TypeScheme) ->
1112         let s,vl = type_sign_vl status [] typ in
1113         (match bo with
1114           | None -> status,Stype (r, vl, None)
1115           | Some body ->
1116               let db = db_from_sign s in
1117               let status,t =
1118                extract_type_scheme status [] db body (List.length s) in
1119               status,Stype (r, vl, Some t))
1120     | (Info, Default) ->
1121         let status,(_,t) = record_constant_type status r (Some typ) in
1122         let status,res = type_expunge status t in
1123         status,Sval (r,res)
1124
1125
1126 let extract_fixpoint_common uri height fix_or_cofix ifl =
1127   let recparamnoi,ti,ci =
1128    List.fold_right
1129     (fun (_,_,recparamno,ty,bo) (recparamnos,tys,bos) ->
1130       recparamno::recparamnos,ty::tys,bo::bos) ifl ([],[],[]) in
1131   let recparamnoi = Array.of_list recparamnoi in
1132   let ti = Array.of_list ti in
1133   let ci = Array.of_list ci in
1134   let n = Array.length ti in
1135   let vkn =
1136    Array.init n
1137     (fun i ->
1138       if fix_or_cofix then
1139        NReference.reference_of_spec uri
1140         (NReference.Fix (i,recparamnoi.(i),height))
1141       else
1142        NReference.reference_of_spec uri (NReference.CoFix i)) in
1143   ti,ci,n,vkn
1144
1145 (*s Is a [ml_spec] logical ? *)
1146 let logical_spec = function
1147   | Stype (_, [], Some (Tdummy _)) -> true
1148   | Sval (_,Tdummy _) -> true
1149   | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
1150   | _ -> false
1151
1152 let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
1153   let status =
1154    if is_projection then
1155     let _,_,recparamno,_,_ = List.nth ifl 0 in
1156     let fieldspec = NReference.Fix (0,recparamno,height) in
1157     let ref = NReference.reference_of_spec uri fieldspec in
1158      confirm_projection status ref
1159    else
1160     status in
1161   let ti,ci,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
1162   current_fixpoints := Some uri;
1163   let status,res = array_mapi_status status
1164    (fun status i _ ->
1165      let _,head = split_all_prods status ~subst:[] [] ti.(i) in
1166      match head with
1167         NCic.Sort s when classify_sort s = InProp -> status,`None
1168       | NCic.Sort _ ->
1169          let n = type_scheme_nb_args status [] ti.(i) in
1170          let ids = iterate (fun l -> anonymous_name::l) n [] in
1171          status,`Type (Dtype (vkn.(i), ids, Tunknown))
1172       | _ ->
1173         if sort_of status [] ti.(i) <> InProp then
1174          let status,e,t = extract_std_constant status vkn.(i) ci.(i) ti.(i) in
1175           status,`Some (e,t)
1176         else
1177           status,`None
1178    ) ti in
1179   let axioms,terms,types =
1180    Array.fold_right
1181     (fun x ((axioms,terms,types) as res) ->
1182       match x with
1183          `None -> res
1184        | `Some (t,ty) -> axioms,t::terms,ty::types
1185        | `Type decl -> decl::axioms,terms,types
1186     ) res ([],[],[]) in
1187   current_fixpoints := None;
1188   status,axioms @ [Dfix (vkn, Array.of_list terms, Array.of_list types)]
1189
1190 let extract_fixpoint_spec status uri height fix_or_cofix ifl =
1191   let ti,_,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
1192   let status,specs =
1193    array_mapi_status status
1194     (fun status i vkn ->
1195       if sort_of status [] ti.(i) <> InProp then begin
1196        let status,spec = extract_constant_spec status vkn None ti.(i) in
1197        status, if logical_spec spec then None else Some spec
1198       end
1199      else status,None
1200     ) vkn in
1201   status,HExtlib.filter_map (fun x -> x) (Array.to_list specs)
1202
1203 let extract_constant status r bo typ =
1204   match bo with
1205     | None -> (* A logical axiom is risky, an informative one is fatal. *)
1206         (match flag_of_type status [] typ with
1207            | (Info,TypeScheme) ->
1208                if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
1209                let n = type_scheme_nb_args status [] typ in
1210                let ids = iterate (fun l -> anonymous_name::l) n [] in
1211                status,Dtype (r, ids, Taxiom)
1212            | (Info,Default) ->
1213                if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
1214                let status,(_,t) = record_constant_type status r (Some typ) in
1215                let status,res = type_expunge status t in
1216                status, Dterm (r, MLaxiom, res)
1217            | (Logic,TypeScheme) ->
1218                (*CSC: only for warnings add_log_axiom r;*)
1219                status,Dtype (r, [], Tdummy Ktype)
1220            | (Logic,Default) ->
1221                (*CSC: only for warnings add_log_axiom r;*)
1222                status,Dterm (r, MLdummy, Tdummy Kother))
1223     | Some body ->
1224         (match flag_of_type status [] typ with
1225            | (Logic, Default) ->
1226               status,Dterm (r, MLdummy, Tdummy Kother)
1227            | (Logic, TypeScheme) ->
1228               status,Dtype (r, [], Tdummy Ktype)
1229            | (Info, Default) ->
1230                let status,e,t = extract_std_constant status r body typ in
1231                status,Dterm (r,e,t)
1232            | (Info, TypeScheme) ->
1233                let s,vl = type_sign_vl status [] typ in
1234                let db = db_from_sign s in
1235                let status,t =
1236                 extract_type_scheme status [] db body (List.length s)
1237                in status,Dtype (r, vl, t))
1238
1239 let extract_inductive status uri inductive ind_pragma leftno types =
1240   let status,ind = extract_ind0 status uri inductive ind_pragma leftno types in
1241   (*CSC: add_recursors status kn;*)
1242   let f status _i _j l =
1243     let implicits = [] (*CSC:implicits_of_global (ConstructRef ((kn,i),j+1))*) in
1244     let rec filter status i = function
1245       | [] -> status,[]
1246       | t::l ->
1247           let status,l' = filter status (succ i) l in
1248           let status,res = expand status t in
1249           if isDummy res || List.mem i implicits then status,l'
1250           else status,t::l'
1251     in filter status 1 l
1252   in
1253   let status,packets =
1254     array_fold_right_i
1255      (fun i p (status,res) ->
1256        let status,types =
1257         array_fold_right_i
1258         (fun j x (status,res) ->
1259           let status,y = f status i j x in
1260            status,y::res
1261         ) p.ip_types (status,[])
1262        in
1263         status, { p with ip_types = Array.of_list types }::res
1264      ) ind.ind_packets (status,[])
1265   in status,{ ind with ind_packets = Array.of_list packets }
1266
1267 (*s Is a [ml_decl] logical ? *)
1268
1269 let logical_decl = function
1270   | Dterm (_,MLdummy,Tdummy _) -> true
1271   | Dtype (_,[],Tdummy _) -> true
1272   | Dfix (_,av,tv) ->
1273       (array_for_all ((=) MLdummy) av) &&
1274       (array_for_all isDummy tv)
1275   | Dind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
1276   | _ -> false
1277
1278 let extract_impl status (uri,height,metasenv,subst,obj_kind) =
1279  assert (metasenv=[]);
1280  assert (subst=[]);
1281  let status,decl =
1282   match obj_kind with
1283      NCic.Constant (_,_,bo,typ,_) ->
1284       let r =
1285        let spec =
1286         match bo with
1287            None -> NReference.Decl
1288          | Some _ -> NReference.Def height
1289        in NReference.reference_of_spec uri spec
1290       in
1291       let status,res = extract_constant status r bo typ in
1292        status,[res]
1293    | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
1294       let status,res =
1295        extract_inductive status uri inductive ind_pragma leftno types
1296       in
1297        status,[Dind res]
1298    | NCic.Fixpoint (fix_or_cofix,ifl,(_,_,def_pragma)) ->
1299       extract_fixpoint status uri height fix_or_cofix
1300        (def_pragma = `Projection) ifl
1301  in
1302   status, List.filter (fun decl -> not (logical_decl decl)) decl
1303 ;;
1304
1305 let extract_spec status (uri,height,metasenv,subst,obj_kind) =
1306  assert (metasenv=[]);
1307  assert (subst=[]);
1308  match obj_kind with
1309     NCic.Constant (_,_,bo,typ,_) ->
1310      let r =
1311       let spec =
1312        match bo with
1313           None -> NReference.Decl
1314         | Some _ -> NReference.Def height
1315       in NReference.reference_of_spec uri spec
1316      in
1317      let status,spec = extract_constant_spec status r bo typ in
1318      status,if logical_spec spec then [] else [spec]
1319   | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
1320      let status,res =
1321       extract_inductive status uri inductive ind_pragma leftno types in
1322      let spec = Sind res in
1323      status,if logical_spec spec then [] else [spec]
1324   | NCic.Fixpoint (fix_or_cofix,ifl,_) ->
1325      extract_fixpoint_spec status uri height fix_or_cofix ifl
1326
1327 let extract status obj =
1328  let status,res = extract_impl status obj in
1329  let status,resl = extract_spec status obj in
1330   status,res,resl