matita/components/ng_kernel/nCicExtraction.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
  27
  28 let fix_sorts t = t;;
  29 let apply_subst subst t = assert (subst=[]); t;;
  30
  31 type typformerreference = NReference.reference
  32 type reference = NReference.reference
  33
  34 type kind =
  35   | Type
  36   | KArrow of kind * kind
  37   | KSkip of kind (* dropped abstraction *)
  38
  39 let rec size_of_kind =
  40   function
  41     | Type -> 1
  42     | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
  43     | KSkip k -> size_of_kind k
  44 ;;
  45
  46 let bracket size_of pp o =
  47   if size_of o > 1 then
  48     "(" ^ pp o ^ ")"
  49   else
  50     pp o
  51 ;;
  52
  53 let rec pretty_print_kind =
  54   function
  55     | Type -> "*"
  56     | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
  57     | KSkip k -> pretty_print_kind k
  58 ;;
  59
  60 type typ =
  61   | Var of int
  62   | Unit
  63   | Top
  64   | TConst of typformerreference
  65   | Arrow of typ * typ
  66   | Skip of typ
  67   | Forall of string * kind * typ
  68   | TAppl of typ list
  69
  70 let rec size_of_type =
  71   function
  72     | Var v -> 1
  73     | Unit -> 1
  74     | Top -> 1
  75     | TConst c -> 1
  76     | Arrow (l, r) -> 1 + size_of_type l + size_of_type r
  77     | Skip t -> size_of_type t
  78     | Forall (name, kind, typ) -> 1 + size_of_type typ
  79     | TAppl l -> List.fold_right (+) (List.map size_of_type l) 0
  80 ;;
  81
  82 type term =
  83   | Rel of int
  84   | UnitTerm
  85   | Const of reference
  86   | Lambda of string * (* typ **) term
  87   | Appl of term list
  88   | LetIn of string * (* typ **) term * term
  89   | Match of reference * term * term list
  90   | TLambda of (* string **) term
  91   | Inst of (*typ_former **) term
  92 ;;
  93
  94 let rec size_of_term =
  95   function
  96     | Rel r -> 1
  97     | UnitTerm -> 1
  98     | Const c -> 1
  99     | Lambda (name, body) -> 1 + size_of_term body
 100     | Appl l -> List.length l
 101     | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
 102     | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
 103     | TLambda t -> size_of_term t
 104     | Inst t -> size_of_term t
 105 ;;
 106 let unitty =
 107  NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
 108
 109 (* None = dropped abstraction *)
 110 type typ_context = (string * kind) option list
 111 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 112
 113 type typ_former_decl = typ_context * kind
 114 type typ_former_def = typ_former_decl * typ
 115
 116 type term_former_decl = term_context * typ
 117 type term_former_def = term_former_decl * term
 118
 119 type obj_kind =
 120    TypeDeclaration of typ_former_decl
 121  | TypeDefinition of typ_former_def
 122  | TermDeclaration of term_former_decl
 123  | TermDefinition of term_former_def
 124  | LetRec of obj_kind list
 125  | Algebraic of (string * typ_context * (string * typ list) list) list
 126
 127 type obj = NUri.uri * obj_kind
 128
 129 let rec classify_not_term status context t =
 130  match NCicReduction.whd status ~subst:[] context t with
 131   | NCic.Sort s ->
 132      (match s with
 133          NCic.Prop
 134        | NCic.Type [`CProp,_] -> `PropKind
 135        | NCic.Type [`Type,_] -> `Kind
 136        | NCic.Type _ -> assert false)
 137   | NCic.Prod (b,s,t) ->
 138      (*CSC: using invariant on "_" *)
 139      classify_not_term status ((b,NCic.Decl s)::context) t
 140   | NCic.Implicit _
 141   | NCic.LetIn _
 142   | NCic.Lambda _
 143   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 144   | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
 145   | NCic.Match _
 146   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 147      (* be aware: we can be the head of an application *)
 148      assert false (* TODO *)
 149   | NCic.Meta _ -> assert false (* TODO *)
 150   | NCic.Appl (he::_) -> classify_not_term status context he
 151   | NCic.Rel n ->
 152      let rec find_sort typ =
 153       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 154         NCic.Sort NCic.Prop -> `Proposition
 155       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 156       | NCic.Sort (NCic.Type [`Type,_]) ->
 157          (*CSC: we could be more precise distinguishing the user provided
 158                 minimal elements of the hierarchies and classify these
 159                 as `Kind *)
 160          `KindOrType
 161       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 162       | NCic.Prod (_,_,t) ->
 163          (* we skipped arguments of applications, so here we need to skip
 164             products *)
 165          find_sort t
 166       | _ -> assert false (* NOT A SORT *)
 167      in
 168       (match List.nth context (n-1) with
 169           _,NCic.Decl typ -> find_sort typ
 170         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 171   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 172      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 173       (match classify_not_term status [] ty with
 174         | `Proposition
 175         | `Type -> assert false (* IMPOSSIBLE *)
 176         | `Kind
 177         | `KindOrType -> `Type
 178         | `PropKind -> `Proposition)
 179   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 180      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 181      let _,_,arity,_ = List.nth ityl i in
 182       (match classify_not_term status [] arity with
 183         | `Proposition
 184         | `Type
 185         | `KindOrType -> assert false (* IMPOSSIBLE *)
 186         | `Kind -> `Type
 187         | `PropKind -> `Proposition)
 188   | NCic.Const (NReference.Ref (_,NReference.Con _))
 189   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 190      assert false (* IMPOSSIBLE *)
 191 ;;
 192
 193 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 194
 195 let classify status ~metasenv context t =
 196  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 197   | NCic.Sort _ ->
 198      (classify_not_term status context t : not_term :> [> not_term])
 199   | ty ->
 200      let ty = fix_sorts ty in
 201       `Term
 202         (match classify_not_term status context ty with
 203           | `Proposition -> `Proof
 204           | `Type -> `Term
 205           | `KindOrType -> `TypeFormerOrTerm
 206           | `Kind -> `TypeFormer
 207           | `PropKind -> `PropFormer)
 208 ;;
 209
 210
 211 let rec kind_of status ~metasenv context k =
 212  match NCicReduction.whd status ~subst:[] context k with
 213   | NCic.Sort NCic.Type _ -> Type
 214   | NCic.Sort _ -> assert false (* NOT A KIND *)
 215   | NCic.Prod (b,s,t) ->
 216      (match classify status ~metasenv context s with
 217        | `Kind ->
 218            KArrow (kind_of status ~metasenv context s,
 219             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 220        | `Type
 221        | `KindOrType
 222        | `Proposition
 223        | `PropKind ->
 224            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 225        | `Term _ -> assert false (* IMPOSSIBLE *))
 226   | NCic.Implicit _
 227   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 228   | NCic.Lambda _
 229   | NCic.Rel _
 230   | NCic.Const _ -> assert false (* NOT A KIND *)
 231   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 232                                    otherwise NOT A KIND *)
 233   | NCic.Meta _
 234   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 235 ;;
 236
 237 let rec skip_args status ~metasenv context =
 238  function
 239   | _,[] -> []
 240   | [],_ -> assert false (* IMPOSSIBLE *)
 241   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 242   | _::tl1,arg::tl2 ->
 243      match classify status ~metasenv context arg with
 244       | `KindOrType
 245       | `Type
 246       | `Term `TypeFormer ->
 247          Some arg::skip_args status ~metasenv context (tl1,tl2)
 248       | `Kind
 249       | `Proposition
 250       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 251       | `Term _ -> assert false (* IMPOSSIBLE *)
 252 ;;
 253
 254 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 255
 256 type db = (typ_context * typ option) ReferenceMap.t
 257
 258 class type g_status =
 259  object
 260   method extraction_db: db
 261  end
 262
 263 class virtual status =
 264  object
 265   inherit NCic.status
 266   val extraction_db = ReferenceMap.empty
 267   method extraction_db = extraction_db
 268   method set_extraction_db v = {< extraction_db = v >}
 269   method set_extraction_status
 270    : 'status. #g_status as 'status -> 'self
 271    = fun o -> {< extraction_db = o#extraction_db >}
 272  end
 273
 274 let rec split_kind_prods context =
 275  function
 276   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 277   | KSkip ta -> split_kind_prods (None::context) ta
 278   | Type -> context,Type
 279 ;;
 280
 281 let rec split_typ_prods context =
 282  function
 283   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 284   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 285   | Skip ta -> split_typ_prods (None::context) ta
 286   | _ as t -> context,t
 287 ;;
 288
 289 let rec glue_ctx_typ ctx typ =
 290  match ctx with
 291   | [] -> typ
 292   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 293   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 294   | None::ctx -> glue_ctx_typ ctx (Skip typ)
 295 ;;
 296
 297 let rec split_typ_lambdas status n ~metasenv context typ =
 298  if n = 0 then context,typ
 299  else
 300   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 301    | NCic.Lambda (name,s,t) ->
 302       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 303    | t ->
 304       (* eta-expansion required *)
 305       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 306       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 307        | NCic.Prod (name,typ,_) ->
 308           split_typ_lambdas status (n-1) ~metasenv
 309            ((name,NCic.Decl typ)::context)
 310            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 311        | _ -> assert false (* IMPOSSIBLE *)
 312 ;;
 313
 314
 315 let context_of_typformer status ~metasenv context =
 316  function
 317     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 318   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 319   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 320   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 321      (try fst (ReferenceMap.find ref status#extraction_db)
 322       with
 323        Not_found -> assert false (* IMPOSSIBLE *))
 324   | NCic.Match _ -> assert false (* TODO ???? *)
 325   | NCic.Rel n ->
 326      let typ =
 327       match List.nth context (n-1) with
 328          _,NCic.Decl typ -> typ
 329        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 330      let typ_ctx = snd (HExtlib.split_nth n context) in
 331      let typ = kind_of status ~metasenv typ_ctx typ in
 332       fst (split_kind_prods [] typ)
 333   | NCic.Meta _ -> assert false (* TODO *)
 334   | NCic.Const (NReference.Ref (_,NReference.Con _))
 335   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 336   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 337   | NCic.Appl _ | NCic.Prod _ ->
 338      assert false (* IMPOSSIBLE *)
 339
 340 let rec typ_of status ~metasenv context k =
 341  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 342   | NCic.Prod (b,s,t) ->
 343      (* CSC: non-invariant assumed here about "_" *)
 344      (match classify status ~metasenv context s with
 345        | `Kind ->
 346            Forall (b, kind_of status ~metasenv context s,
 347             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 348        | `Type
 349        | `KindOrType -> (* ??? *)
 350            Arrow (typ_of status ~metasenv context s,
 351             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 352        | `PropKind
 353        | `Proposition ->
 354            Skip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 355        | `Term _ -> assert false (* IMPOSSIBLE *))
 356   | NCic.Sort _
 357   | NCic.Implicit _
 358   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 359   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 360   | NCic.Rel n -> Var n
 361   | NCic.Const ref -> TConst ref
 362   | NCic.Appl (he::args) ->
 363      let he_context = context_of_typformer status ~metasenv context he in
 364      TAppl (typ_of status ~metasenv context he ::
 365       List.map
 366        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 367        (skip_args status ~metasenv context (List.rev he_context,args)))
 368   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 369                                    otherwise NOT A TYPE *)
 370   | NCic.Meta _
 371   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 372 ;;
 373
 374 let rec fomega_subst k t1 =
 375  function
 376   | Var n ->
 377      if k=n then t1
 378      else if n < k then Var n
 379      else Var (n-1)
 380   | Top -> Top
 381   | TConst ref -> TConst ref
 382   | Unit -> Unit
 383   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 384   | Skip t -> Skip (fomega_subst (k+1) t1 t)
 385   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 386   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 387
 388 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 389
 390 let rec fomega_whd status ty =
 391  match ty with
 392  | TConst r ->
 393     (match fomega_lookup status r with
 394         None -> ty
 395       | Some ty -> fomega_whd status ty)
 396  | TAppl (TConst r::args) ->
 397     (match fomega_lookup status r with
 398         None -> ty
 399       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 400  | _ -> ty
 401
 402 let rec term_of status ~metasenv context =
 403  function
 404   | NCic.Implicit _
 405   | NCic.Sort _
 406   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 407   | NCic.Lambda (b,ty,bo) ->
 408      (* CSC: non-invariant assumed here about "_" *)
 409      (match classify status ~metasenv context ty with
 410        | `Kind ->
 411            TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 412        | `KindOrType (* ??? *)
 413        | `Type ->
 414            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 415        | `PropKind
 416        | `Proposition ->
 417            (* CSC: LAZY ??? *)
 418            term_of status ~metasenv ((b,NCic.Decl ty)::context) bo
 419        | `Term _ -> assert false (* IMPOSSIBLE *))
 420   | NCic.LetIn (b,ty,t,bo) ->
 421      (match classify status ~metasenv context t with
 422        | `Term `TypeFormerOrTerm (* ???? *)
 423        | `Term `Term ->
 424           LetIn (b,term_of status ~metasenv context t,
 425            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 426        | `Kind
 427        | `Type
 428        | `KindOrType
 429        | `PropKind
 430        | `Proposition
 431        | `Term `PropFormer
 432        | `Term `TypeFormer
 433        | `Term `Proof ->
 434          (* not in programming languages, we expand it *)
 435          term_of status ~metasenv context
 436           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 437   | NCic.Rel n -> Rel n
 438   | NCic.Const ref -> Const ref
 439   | NCic.Appl (he::args) ->
 440      eat_args status metasenv
 441       (term_of status ~metasenv context he) context
 442       (typ_of status ~metasenv context
 443         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 444       args
 445 (*
 446      let he_context = context_of_typformer status ~metasenv context he in
 447      let process_args he =
 448       function
 449          `Empty -> he
 450        | `Inst tl -> Inst (process_args he tl)
 451        | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
 452      in
 453      Appl (typ_of status ~metasenv context he ::
 454       process_args (typ_of status ~metasenv context he)
 455        (skip_term_args status ~metasenv context (List.rev he_context,args))
 456 *)
 457   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 458                                    otherwise NOT A TYPE *)
 459   | NCic.Meta _ -> assert false (* TODO *)
 460   | NCic.Match (ref,_,t,pl) ->
 461      Match (ref,term_of status ~metasenv context t,
 462       List.map (term_of status ~metasenv context) pl)
 463 and eat_args status metasenv acc context tyhe =
 464  function
 465     [] -> acc
 466   | arg::tl ->
 467      let mk_appl f x =
 468       match f with
 469          Appl args -> Appl (args@[x])
 470        | _ -> Appl [f;x]
 471      in
 472      match fomega_whd status tyhe with
 473         Arrow (s,t) ->
 474          let arg =
 475           match s with
 476              Unit -> UnitTerm
 477            | _ -> term_of status ~metasenv context arg in
 478          eat_args status metasenv (mk_appl acc arg) context t tl
 479       | Forall (_,_,t) ->
 480          eat_args status metasenv (Inst acc)
 481           context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
 482       | Skip t ->
 483          eat_args status metasenv acc context t tl
 484       | Top -> assert false (*TODO: HOW??*)
 485       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 486 ;;
 487
 488 type 'a result =
 489   | Erased
 490   | OutsideTheory
 491   | Failure of string
 492   | Success of 'a
 493 ;;
 494
 495 let object_of_constant status ~metasenv uri height bo ty =
 496   match classify status ~metasenv [] ty with
 497     | `Kind ->
 498         let ty = kind_of status ~metasenv [] ty in
 499         let ctx0,res = split_kind_prods [] ty in
 500         let ctx,bo =
 501          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 502         (match classify status ~metasenv ctx bo with
 503           | `Type
 504           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 505               let nicectx =
 506                List.map2
 507                 (fun p1 n ->
 508                   HExtlib.map_option (fun (_,k) ->
 509                    (*CSC: BUG here, clashes*)
 510                    String.uncapitalize (fst n),k) p1)
 511                 ctx0 ctx
 512               in
 513               (* BUG here: for mutual type definitions the spec is not good *)
 514               let ref =
 515                NReference.reference_of_spec uri (NReference.Def height) in
 516               let bo = typ_of status ~metasenv ctx bo in
 517                status#set_extraction_db
 518                 (ReferenceMap.add ref (nicectx,Some bo)
 519                   status#extraction_db),
 520                Success (uri,TypeDefinition((nicectx,res),bo))
 521           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 522           | `PropKind
 523           | `Proposition -> status, Erased
 524           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 525     | `PropKind
 526     | `Proposition -> status, Erased
 527     | `KindOrType (* ??? *)
 528     | `Type ->
 529        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 530        let ty = typ_of status ~metasenv [] ty in
 531         status,
 532         Success (uri, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 533     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 534 ;;
 535
 536 let object_of_inductive status ~metasenv uri ind leftno il =
 537  let tyl =
 538   HExtlib.filter_map
 539    (fun _,name,arity,cl ->
 540      match classify_not_term status [] arity with
 541       | `Proposition
 542       | `KindOrType
 543       | `Type -> assert false (* IMPOSSIBLE *)
 544       | `PropKind -> None
 545       | `Kind ->
 546           let arity = kind_of status ~metasenv [] arity in
 547           let ctx,_ as res = split_kind_prods [] arity in
 548            Some (name,ctx,[])
 549    ) il
 550  in
 551   match tyl with
 552      [] -> status,None
 553    | _ -> status, Some (uri, Algebraic tyl)
 554 ;;
 555
 556 let object_of status (uri,height,metasenv,subst,obj_kind) =
 557   let obj_kind = apply_subst subst obj_kind in
 558       match obj_kind with
 559         | NCic.Constant (_,_,None,ty,_) ->
 560           (match classify status ~metasenv [] ty with
 561             | `Kind ->
 562               let ty = kind_of status ~metasenv [] ty in
 563               let ctx,_ as res = split_kind_prods [] ty in
 564               let ref = NReference.reference_of_spec uri NReference.Decl in
 565                 status#set_extraction_db
 566                   (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res)
 567             | `PropKind
 568             | `Proposition -> status, Erased
 569             | `Type
 570             | `KindOrType (*???*) ->
 571               let ty = typ_of status ~metasenv [] ty in
 572                 status, Success (uri, TermDeclaration (split_typ_prods [] ty))
 573             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 574         | NCic.Constant (_,_,Some bo,ty,_) ->
 575           object_of_constant status ~metasenv uri height bo ty
 576         | NCic.Fixpoint (_fix_or_cofix,fs,_) ->
 577           let status,objs =
 578             List.fold_right
 579             (fun (_,_name,_,ty,bo) (status,res) ->
 580               let status,obj = object_of_constant ~metasenv status uri height bo ty in
 581                 match obj with
 582                   | Success (_uri,obj) -> status, obj::res
 583                   | _ -> status, res) fs (status,[])
 584           in
 585             status, Success (uri,LetRec objs)
 586         | NCic.Inductive (ind,leftno,il,_) ->
 587           let status, obj_of_inductive = object_of_inductive status ~metasenv uri ind leftno il in
 588             match obj_of_inductive with
 589               | None -> status, Failure "Could not extract an inductive type."
 590               | Some s -> status, Success s
 591
 592 (************************ HASKELL *************************)
 593
 594 (* -----------------------------------------------------------------------------
 595  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 596  * -----------------------------------------------------------------------------
 597  *)
 598 let (|>) f g =
 599   fun x -> g (f x)
 600 ;;
 601
 602 let curry f x y =
 603   f (x, y)
 604 ;;
 605
 606 let uncurry f (x, y) =
 607   f x y
 608 ;;
 609
 610 let rec char_list_of_string s =
 611   let l = String.length s in
 612   let rec aux buffer s =
 613     function
 614       | 0 -> buffer
 615       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 616   in
 617     aux [] s l
 618 ;;
 619
 620 let string_of_char_list s =
 621   let rec aux buffer =
 622     function
 623       | []    -> buffer
 624       | x::xs -> aux (String.make 1 x ^ buffer) xs
 625   in
 626     aux "" s
 627 ;;
 628
 629 (* ----------------------------------------------------------------------------
 630  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 631  * and type variable names.
 632  * ----------------------------------------------------------------------------
 633  *)
 634
 635 let remove_underscores_and_mark =
 636   let rec aux char_list_buffer positions_buffer position =
 637     function
 638       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 639       | x::xs ->
 640         if x == '_' then
 641           aux char_list_buffer (position::positions_buffer) position xs
 642         else
 643           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 644   in
 645     aux [] [] 0
 646 ;;
 647
 648 let rec capitalize_marked_positions s =
 649   function
 650     | []    -> s
 651     | x::xs ->
 652       if x < String.length s then
 653         let c = Char.uppercase (String.get s x) in
 654         let _ = String.set s x c in
 655           capitalize_marked_positions s xs
 656       else
 657         capitalize_marked_positions s xs
 658 ;;
 659
 660 let contract_underscores_and_capitalise =
 661   char_list_of_string |>
 662   remove_underscores_and_mark |>
 663   uncurry capitalize_marked_positions
 664 ;;
 665
 666 let idiomatic_haskell_type_name_of_string =
 667   contract_underscores_and_capitalise |>
 668   String.capitalize
 669 ;;
 670
 671 let idiomatic_haskell_term_name_of_string =
 672   contract_underscores_and_capitalise |>
 673   String.uncapitalize
 674 ;;
 675
 676 (*CSC: code to be changed soon when we implement constructors and
 677   we fix the code for term application *)
 678 let classify_reference status ref =
 679   if ReferenceMap.mem ref status#extraction_db then
 680     `TypeName
 681   else
 682     `FunctionName
 683 ;;
 684
 685 let capitalize classification name =
 686   match classification with
 687     | `Constructor
 688     | `TypeName -> idiomatic_haskell_type_name_of_string name
 689     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 690 ;;
 691
 692 let pp_ref status ref =
 693  capitalize (classify_reference status ref)
 694   (NCicPp.r2s status false ref)
 695
 696 let name_of_uri classification uri =
 697  capitalize classification (NUri.name_of_uri uri)
 698
 699 (* cons avoid duplicates *)
 700 let rec (@:::) name l =
 701  if name <> "" (* propositional things *) && name.[0] = '_' then
 702   let name = String.sub name 1 (String.length name - 1) in
 703   let name = if name = "" then "a" else name in
 704    name @::: l
 705  else if List.mem name l then (name ^ "'") @::: l
 706  else name,l
 707 ;;
 708
 709 let (@::) x l = let x,l = x @::: l in x::l;;
 710
 711 let rec pretty_print_type status ctxt =
 712   function
 713     | Var n -> List.nth ctxt (n-1)
 714     | Unit -> "()"
 715     | Top -> assert false (* ??? *)
 716     | TConst ref -> pp_ref status ref
 717     | Arrow (t1,t2) ->
 718         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 719          pretty_print_type status ("_"::ctxt) t2
 720     | Skip t -> pretty_print_type status ("_"::ctxt) t
 721     | Forall (name, kind, t) ->
 722       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 723       let name = String.uncapitalize name in
 724         if size_of_kind kind > 1 then
 725           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name@::ctxt) t
 726         else
 727           "forall " ^ name ^ ". " ^ pretty_print_type status (name@::ctxt) t
 728    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 729
 730 let rec pretty_print_term status ctxt =
 731   function
 732     | Rel n -> List.nth ctxt (n-1)
 733     | UnitTerm -> "()"
 734     | Const ref -> pp_ref status ref
 735     | Lambda (name,t) -> "\\" ^ name ^ " -> " ^ pretty_print_term status (name@::ctxt) t
 736     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 737     | LetIn (name,s,t) ->
 738       "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t
 739     | Match (r,matched,pl) ->
 740       let constructors, leftno =
 741       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
 742       let _,_,_,cl  = List.nth tys n in
 743         cl,leftno
 744       in
 745         let rec eat_branch n ty pat =
 746           match (ty, pat) with
 747           | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat
 748           | NCic.Prod (_, _, t), Lambda (name, t') ->
 749             (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
 750             let cv, rhs = eat_branch 0 t t' in
 751               name :: cv, rhs
 752           | _, _ -> [], pat
 753         in
 754           let j = ref 0 in
 755           let patterns =
 756             try
 757               List.map2
 758                 (fun (_, name, ty) pat -> incr j; name, eat_branch leftno ty pat) constructors pl
 759             with Invalid_argument _ -> assert false
 760           in
 761             "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 762               String.concat "\n"
 763                 (List.map
 764                   (fun (name,(bound_names,rhs)) ->
 765                     let pattern,body =
 766                     (*CSC: BUG avoid name clashes *)
 767                     String.concat " " (String.capitalize name::bound_names),
 768                       pretty_print_term status ((List.rev bound_names)@ctxt) rhs
 769                     in
 770                       "  " ^ pattern ^ " -> " ^ body
 771                   ) patterns)
 772     | TLambda t -> pretty_print_term status ctxt t
 773     | Inst t -> pretty_print_term status ctxt t
 774 ;;
 775
 776 (*
 777 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 778
 779 type term_former_def = term_context * term * typ
 780 type term_former_decl = term_context * typ
 781 *)
 782
 783 let rec pp_obj status (uri,obj_kind) =
 784   let pretty_print_context ctx =
 785     String.concat " " (List.rev
 786       (List.fold_right
 787        (fun (x,kind) l ->
 788          let x,l = x @:::l in
 789          if size_of_kind kind > 1 then
 790           ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
 791          else
 792           x::l)
 793        (HExtlib.filter_map (fun x -> x) ctx) []))
 794   in
 795  let namectx_of_ctx ctx =
 796   List.fold_right (@::)
 797    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 798  match obj_kind with
 799    TypeDeclaration (ctx,_) ->
 800     (* data?? unsure semantics: inductive type without constructor, but
 801        not matchable apparently *)
 802     if List.length ctx = 0 then
 803       "data " ^ name_of_uri `TypeName uri
 804     else
 805       "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx
 806  | TypeDefinition ((ctx, _),ty) ->
 807     let namectx = namectx_of_ctx ctx in
 808     if List.length ctx = 0 then
 809       "type " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty
 810     else
 811       "type " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 812  | TermDeclaration (ctx,ty) ->
 813     let name = name_of_uri `FunctionName uri in
 814       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 815       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 816  | TermDefinition ((ctx,ty),bo) ->
 817     let name = name_of_uri `FunctionName uri in
 818     let namectx = namectx_of_ctx ctx in
 819     (*CSC: BUG here *)
 820     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 821     name ^ " = " ^ pretty_print_term status namectx bo
 822  | LetRec l ->
 823     (*CSC: BUG always uses the name of the URI *)
 824     String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
 825  | Algebraic il ->
 826     String.concat "\n"
 827      (List.map
 828       (fun _name,ctx,cl ->
 829         (*CSC: BUG always uses the name of the URI *)
 830         "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^
 831         String.concat " | " (List.map
 832          (fun name,tys ->
 833           capitalize `Constructor name ^
 834            String.concat " " (List.map (pretty_print_type status []) tys)
 835          ) cl
 836       )) il)
 837  (* inductive and records missing *)
 838
 839 let haskell_of_obj status obj =
 840  let status, obj = object_of status obj in
 841   status,
 842    match obj with
 843       Erased -> "-- [?] Erased due to term being propositionally irrelevant.\n"
 844     | OutsideTheory -> "-- [?] Erased due to image of term under extraction residing outside Fω.\n"
 845     | Failure msg -> "-- [!] FAILURE: " ^ msg ^ "\n"
 846     | Success o -> pp_obj status o ^ "\n"