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   | TSkip 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 _ -> 2
  77     | TSkip t -> size_of_type t
  78     | Forall _ -> 2
  79     | TAppl l -> 1
  80 ;;
  81
  82 (* None = dropped abstraction *)
  83 type typ_context = (string * kind) option list
  84 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
  85
  86 type typ_former_decl = typ_context * kind
  87 type typ_former_def = typ_former_decl * typ
  88
  89 type term =
  90   | Rel of int
  91   | UnitTerm
  92   | Const of reference
  93   | Lambda of string * (* typ **) term
  94   | Appl of term list
  95   | LetIn of string * (* typ **) term * term
  96   | Match of reference * term * (term_context * term) list
  97   | BottomElim
  98   | TLambda of string * term
  99   | Inst of (*typ_former **) term
 100   | Skip of term
 101   | UnsafeCoerce of term
 102 ;;
 103
 104 type term_former_decl = term_context * typ
 105 type term_former_def = term_former_decl * term
 106
 107 let mk_appl f x =
 108  match f with
 109     Appl args -> Appl (args@[x])
 110   | _ -> Appl [f;x]
 111
 112 let rec size_of_term =
 113   function
 114     | Rel r -> 1
 115     | UnitTerm -> 1
 116     | Const c -> 1
 117     | Lambda (_, body) -> 1 + size_of_term body
 118     | Appl l -> List.length l
 119     | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
 120     | Match (_, case, pats) -> 1 + size_of_term case + List.length pats
 121     | BottomElim -> 1
 122     | TLambda (_,t) -> size_of_term t
 123     | Inst t -> size_of_term t
 124     | Skip t -> size_of_term t
 125     | UnsafeCoerce t -> 1 + size_of_term t
 126 ;;
 127
 128 type obj_kind =
 129    TypeDeclaration of typ_former_decl
 130  | TypeDefinition of typ_former_def
 131  | TermDeclaration of term_former_decl
 132  | TermDefinition of term_former_def
 133  | LetRec of (NReference.reference * obj_kind) list
 134    (* reference, left, right, constructors *)
 135  | Algebraic of (NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
 136
 137 type obj = NReference.reference * obj_kind
 138
 139 (* For LetRec and Algebraic blocks *)
 140 let dummyref =
 141  NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
 142
 143 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 144
 145 let max_not_term t1 t2 =
 146  match t1,t2 with
 147     `KindOrType,_
 148   | _,`KindOrType -> `KindOrType
 149   | `Kind,_
 150   | _,`Kind -> `Kind
 151   | `Type,_
 152   | _,`Type -> `Type
 153   | `PropKind,_
 154   | _,`PropKind -> `PropKind
 155   | `Proposition,`Proposition -> `Proposition
 156
 157 let sup = List.fold_left max_not_term `Proposition
 158
 159 let rec classify_not_term status context t =
 160  match NCicReduction.whd status ~subst:[] context t with
 161   | NCic.Sort s ->
 162      (match s with
 163          NCic.Prop
 164        | NCic.Type [`CProp,_] -> `PropKind
 165        | NCic.Type [`Type,_] -> `Kind
 166        | NCic.Type _ -> assert false)
 167   | NCic.Prod (b,s,t) ->
 168      (*CSC: using invariant on "_" *)
 169      classify_not_term status ((b,NCic.Decl s)::context) t
 170   | NCic.Implicit _
 171   | NCic.LetIn _
 172   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 173   | NCic.Appl [] ->
 174      assert false (* NOT POSSIBLE *)
 175   | NCic.Lambda (n,s,t) ->
 176      (* Lambdas can me met in branches of matches, expecially when the
 177         output type is a product *)
 178      classify_not_term status ((n,NCic.Decl s)::context) t
 179   | NCic.Match (r,_,_,pl) ->
 180      let classified_pl = List.map (classify_not_term status context) pl in
 181       sup classified_pl
 182   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 183      (* be aware: we can be the head of an application *)
 184      assert false (* TODO *)
 185   | NCic.Meta _ -> assert false (* TODO *)
 186   | NCic.Appl (he::_) -> classify_not_term status context he
 187   | NCic.Rel n ->
 188      let rec find_sort typ =
 189       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 190         NCic.Sort NCic.Prop -> `Proposition
 191       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 192       | NCic.Sort (NCic.Type [`Type,_]) ->
 193          (*CSC: we could be more precise distinguishing the user provided
 194                 minimal elements of the hierarchies and classify these
 195                 as `Kind *)
 196          `KindOrType
 197       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 198       | NCic.Prod (_,_,t) ->
 199          (* we skipped arguments of applications, so here we need to skip
 200             products *)
 201          find_sort t
 202       | _ -> assert false (* NOT A SORT *)
 203      in
 204       (match List.nth context (n-1) with
 205           _,NCic.Decl typ -> find_sort typ
 206         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 207   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 208      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 209       (match classify_not_term status [] ty with
 210         | `Proposition
 211         | `Type -> assert false (* IMPOSSIBLE *)
 212         | `Kind
 213         | `KindOrType -> `Type
 214         | `PropKind -> `Proposition)
 215   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 216      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 217      let _,_,arity,_ = List.nth ityl i in
 218       (match classify_not_term status [] arity with
 219         | `Proposition
 220         | `Type
 221         | `KindOrType -> assert false (* IMPOSSIBLE *)
 222         | `Kind -> `Type
 223         | `PropKind -> `Proposition)
 224   | NCic.Const (NReference.Ref (_,NReference.Con _))
 225   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 226      assert false (* IMPOSSIBLE *)
 227 ;;
 228
 229 let classify status ~metasenv context t =
 230  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 231   | NCic.Sort _ ->
 232      (classify_not_term status context t : not_term :> [> not_term])
 233   | ty ->
 234      let ty = fix_sorts ty in
 235       `Term
 236         (match classify_not_term status context ty with
 237           | `Proposition -> `Proof
 238           | `Type -> `Term
 239           | `KindOrType -> `TypeFormerOrTerm
 240           | `Kind -> `TypeFormer
 241           | `PropKind -> `PropFormer)
 242 ;;
 243
 244
 245 let rec kind_of status ~metasenv context k =
 246  match NCicReduction.whd status ~subst:[] context k with
 247   | NCic.Sort NCic.Type _ -> Type
 248   | NCic.Sort _ -> assert false (* NOT A KIND *)
 249   | NCic.Prod (b,s,t) ->
 250      (match classify status ~metasenv context s with
 251        | `Kind ->
 252            KArrow (kind_of status ~metasenv context s,
 253             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 254        | `Type
 255        | `KindOrType
 256        | `Proposition
 257        | `PropKind ->
 258            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 259        | `Term _ -> assert false (* IMPOSSIBLE *))
 260   | NCic.Implicit _
 261   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 262   | NCic.Lambda _
 263   | NCic.Rel _
 264   | NCic.Const _ -> assert false (* NOT A KIND *)
 265   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 266                                    otherwise NOT A KIND *)
 267   | NCic.Meta _
 268   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 269 ;;
 270
 271 let rec skip_args status ~metasenv context =
 272  function
 273   | _,[] -> []
 274   | [],_ -> assert false (* IMPOSSIBLE *)
 275   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 276   | _::tl1,arg::tl2 ->
 277      match classify status ~metasenv context arg with
 278       | `KindOrType
 279       | `Type
 280       | `Term `TypeFormer ->
 281          Some arg::skip_args status ~metasenv context (tl1,tl2)
 282       | `Kind
 283       | `Proposition
 284       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 285       | `Term _ -> assert false (* IMPOSSIBLE *)
 286 ;;
 287
 288 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 289
 290 type db = (typ_context * typ option) ReferenceMap.t
 291
 292 class type g_status =
 293  object
 294   method extraction_db: db
 295  end
 296
 297 class virtual status =
 298  object
 299   inherit NCic.status
 300   val extraction_db = ReferenceMap.empty
 301   method extraction_db = extraction_db
 302   method set_extraction_db v = {< extraction_db = v >}
 303   method set_extraction_status
 304    : 'status. #g_status as 'status -> 'self
 305    = fun o -> {< extraction_db = o#extraction_db >}
 306  end
 307
 308 let rec split_kind_prods context =
 309  function
 310   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 311   | KSkip ta -> split_kind_prods (None::context) ta
 312   | Type -> context,Type
 313 ;;
 314
 315 let rec split_typ_prods context =
 316  function
 317   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 318   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 319   | TSkip ta -> split_typ_prods (None::context) ta
 320   | _ as t -> context,t
 321 ;;
 322
 323 let rec glue_ctx_typ ctx typ =
 324  match ctx with
 325   | [] -> typ
 326   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 327   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 328   | None::ctx -> glue_ctx_typ ctx (TSkip typ)
 329 ;;
 330
 331 let rec split_typ_lambdas status n ~metasenv context typ =
 332  if n = 0 then context,typ
 333  else
 334   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 335    | NCic.Lambda (name,s,t) ->
 336       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 337    | t ->
 338       (* eta-expansion required *)
 339       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 340       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 341        | NCic.Prod (name,typ,_) ->
 342           split_typ_lambdas status (n-1) ~metasenv
 343            ((name,NCic.Decl typ)::context)
 344            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 345        | _ -> assert false (* IMPOSSIBLE *)
 346 ;;
 347
 348
 349 let rev_context_of_typformer status ~metasenv context =
 350  function
 351     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 352   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 353   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 354   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 355      (try List.rev (fst (ReferenceMap.find ref status#extraction_db))
 356       with
 357        Not_found ->
 358         (* This can happen only when we are processing the type of
 359            the constructor of a small singleton type. In this case
 360            we are not interested in all the type, but only in its
 361            backbone. That is why we can safely return the dummy context here *)
 362         let rec dummy = None::dummy in
 363         dummy)
 364   | NCic.Match _ -> assert false (* TODO ???? *)
 365   | NCic.Rel n ->
 366      let typ =
 367       match List.nth context (n-1) with
 368          _,NCic.Decl typ -> typ
 369        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 370      let typ_ctx = snd (HExtlib.split_nth n context) in
 371      let typ = kind_of status ~metasenv typ_ctx typ in
 372       List.rev (fst (split_kind_prods [] typ))
 373   | NCic.Meta _ -> assert false (* TODO *)
 374   | NCic.Const (NReference.Ref (_,NReference.Con _))
 375   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 376   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 377   | NCic.Appl _ | NCic.Prod _ ->
 378      assert false (* IMPOSSIBLE *)
 379
 380 let rec typ_of status ~metasenv context k =
 381  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 382   | NCic.Prod (b,s,t) ->
 383      (* CSC: non-invariant assumed here about "_" *)
 384      (match classify status ~metasenv context s with
 385        | `Kind ->
 386            Forall (b, kind_of status ~metasenv context s,
 387             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 388        | `Type
 389        | `KindOrType -> (* ??? *)
 390            Arrow (typ_of status ~metasenv context s,
 391             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 392        | `PropKind
 393        | `Proposition ->
 394            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 395        | `Term _ -> assert false (* IMPOSSIBLE *))
 396   | NCic.Sort _
 397   | NCic.Implicit _
 398   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 399   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 400   | NCic.Rel n -> Var n
 401   | NCic.Const ref -> TConst ref
 402   | NCic.Appl (he::args) ->
 403      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
 404      TAppl (typ_of status ~metasenv context he ::
 405       List.map
 406        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 407        (skip_args status ~metasenv context (rev_he_context,args)))
 408   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 409                                    otherwise NOT A TYPE *)
 410   | NCic.Meta _
 411   | NCic.Match (_,_,_,_) -> Top
 412 ;;
 413
 414 let rec fomega_lift_type_from n k =
 415  function
 416   | Var m as t -> if m < k then t else Var (m + n)
 417   | Top -> Top
 418   | TConst _ as t -> t
 419   | Unit -> Unit
 420   | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
 421   | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
 422   | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
 423   | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
 424
 425 let fomega_lift_type n t =
 426  if n = 0 then t else fomega_lift_type_from n 0 t
 427
 428 let fomega_lift_term n t =
 429  let rec fomega_lift_term n k =
 430   function
 431    | Rel m as t -> if m < k then t else Rel (m + n)
 432    | BottomElim
 433    | UnitTerm
 434    | Const _ as t -> t
 435    | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
 436    | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
 437    | Appl args -> Appl (List.map (fomega_lift_term n k) args)
 438    | LetIn (name,m,bo) ->
 439       LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
 440    | Match (ref,t,pl) ->
 441       let lift_p (ctx,t) =
 442        let lift_context ctx =
 443         let len = List.length ctx in
 444          HExtlib.list_mapi
 445           (fun el i ->
 446             let j = len - i - 1 in
 447             match el with
 448                None
 449              | Some (_,`OfKind  _) as el -> el
 450              | Some (name,`OfType t) ->
 451                 Some (name,`OfType (fomega_lift_type_from n (k+j) t))
 452           ) ctx
 453        in
 454         lift_context ctx, fomega_lift_term n (k + List.length ctx) t
 455       in
 456       Match (ref,fomega_lift_term n k t,List.map lift_p pl)
 457    | Inst t -> Inst (fomega_lift_term n k t)
 458    | Skip t -> Skip (fomega_lift_term n (k+1) t)
 459    | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
 460  in
 461   if n = 0 then t else fomega_lift_term n 0 t
 462 ;;
 463
 464 let rec fomega_subst k t1 =
 465  function
 466   | Var n ->
 467      if k=n then fomega_lift_type k t1
 468      else if n < k then Var n
 469      else Var (n-1)
 470   | Top -> Top
 471   | TConst ref -> TConst ref
 472   | Unit -> Unit
 473   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 474   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 475   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 476   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 477
 478 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 479
 480 let rec fomega_whd status ty =
 481  match ty with
 482  | TConst r ->
 483     (match fomega_lookup status r with
 484         None -> ty
 485       | Some ty -> fomega_whd status ty)
 486  | TAppl (TConst r::args) ->
 487     (match fomega_lookup status r with
 488         None -> ty
 489       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 490  | _ -> ty
 491
 492 let rec term_of status ~metasenv context =
 493  function
 494   | NCic.Implicit _
 495   | NCic.Sort _
 496   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 497   | NCic.Lambda (b,ty,bo) ->
 498      (* CSC: non-invariant assumed here about "_" *)
 499      (match classify status ~metasenv context ty with
 500        | `Kind ->
 501            TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 502        | `KindOrType (* ??? *)
 503        | `Type ->
 504            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 505        | `PropKind
 506        | `Proposition ->
 507            (* CSC: LAZY ??? *)
 508            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 509        | `Term _ -> assert false (* IMPOSSIBLE *))
 510   | NCic.LetIn (b,ty,t,bo) ->
 511      (match classify status ~metasenv context t with
 512        | `Term `TypeFormerOrTerm (* ???? *)
 513        | `Term `Term ->
 514           LetIn (b,term_of status ~metasenv context t,
 515            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 516        | `Kind
 517        | `Type
 518        | `KindOrType
 519        | `PropKind
 520        | `Proposition
 521        | `Term `PropFormer
 522        | `Term `TypeFormer
 523        | `Term `Proof ->
 524          (* not in programming languages, we expand it *)
 525          term_of status ~metasenv context
 526           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 527   | NCic.Rel n -> Rel n
 528   | NCic.Const ref -> Const ref
 529   | NCic.Appl (he::args) ->
 530      eat_args status metasenv
 531       (term_of status ~metasenv context he) context
 532       (*BUG: recomputing every time the type of the head*)
 533       (typ_of status ~metasenv context
 534         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 535       args
 536   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 537                                    otherwise NOT A TYPE *)
 538   | NCic.Meta _ -> assert false (* TODO *)
 539   | NCic.Match (ref,_,t,pl) ->
 540      let patterns_of pl =
 541       let constructors, leftno =
 542        let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
 543        let _,_,_,cl  = List.nth tys n in
 544          cl,leftno
 545       in
 546        let rec eat_branch n ty context ctx pat =
 547          match (ty, pat) with
 548          | TSkip t,_
 549          | Forall (_,_,t),_
 550          | Arrow (_, t), _ when n > 0 ->
 551             eat_branch (pred n) t context ctx pat
 552          | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
 553          (*CSC: unify the three cases below? *)
 554          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
 555            let ctx =
 556             (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
 557            let context = (name,NCic.Decl ty)::context in
 558             eat_branch 0 t context ctx t'
 559          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
 560            let ctx =
 561             (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
 562            let context = (name,NCic.Decl ty)::context in
 563             eat_branch 0 t context ctx t'
 564          | TSkip t,NCic.Lambda (name, ty, t') ->
 565             let ctx = None::ctx in
 566             let context = (name,NCic.Decl ty)::context in
 567              eat_branch 0 t context ctx t'
 568          | Top,_ -> assert false (* IMPOSSIBLE *)
 569          | TSkip _, _
 570          | Forall _,_
 571          | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
 572          | _, _ -> context,ctx, pat
 573        in
 574         try
 575          List.map2
 576           (fun (_, name, ty) pat ->
 577             (*BUG: recomputing every time the type of the constructor*)
 578             let ty = typ_of status ~metasenv context ty in
 579             let context,lhs,rhs = eat_branch leftno ty context [] pat in
 580             let rhs =
 581              (* UnsafeCoerce not always required *)
 582              UnsafeCoerce (term_of status ~metasenv context rhs)
 583             in
 584              lhs,rhs
 585           ) constructors pl
 586         with Invalid_argument _ -> assert false
 587      in
 588      (match classify_not_term status [] (NCic.Const ref) with
 589       | `PropKind
 590       | `KindOrType
 591       | `Kind -> assert false (* IMPOSSIBLE *)
 592       | `Proposition ->
 593           (match patterns_of pl with
 594               [] -> BottomElim
 595             | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
 596             | _ -> assert false)
 597       | `Type ->
 598           Match (ref,term_of status ~metasenv context t, patterns_of pl))
 599 and eat_args status metasenv acc context tyhe =
 600  function
 601     [] -> acc
 602   | arg::tl ->
 603      match fomega_whd status tyhe with
 604         Arrow (s,t) ->
 605          let arg =
 606           match s with
 607              Unit -> UnitTerm
 608            | _ -> term_of status ~metasenv context arg in
 609          eat_args status metasenv (mk_appl acc arg) context t tl
 610       | Top ->
 611          let arg =
 612           match classify status ~metasenv context arg with
 613            | `PropKind
 614            | `Proposition
 615            | `Term `TypeFormer
 616            | `Term `PropFormer
 617            | `Term `Proof
 618            | `Type
 619            | `KindOrType
 620            | `Kind -> UnitTerm
 621            | `Term `TypeFormerOrTerm
 622            | `Term `Term -> term_of status ~metasenv context arg
 623          in
 624           eat_args status metasenv (UnsafeCoerce (mk_appl acc arg))
 625            context Top tl
 626       | Forall (_,_,t) ->
 627          (match classify status ~metasenv context arg with
 628            | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
 629            | `Proposition
 630            | `Term `TypeFormer
 631            | `Kind ->
 632                eat_args status metasenv (UnsafeCoerce (Inst acc))
 633                 context (fomega_subst 1 Unit t) tl
 634            | `Term _ -> assert false (*TODO: ????*)
 635            | `KindOrType
 636            | `Type ->
 637                eat_args status metasenv (Inst acc)
 638                 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
 639                  tl)
 640       | TSkip t ->
 641          eat_args status metasenv acc context t tl
 642       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 643 ;;
 644
 645 type 'a result =
 646   | Erased
 647   | OutsideTheory
 648   | Failure of string
 649   | Success of 'a
 650 ;;
 651
 652 let object_of_constant status ~metasenv ref bo ty =
 653   match classify status ~metasenv [] ty with
 654     | `Kind ->
 655         let ty = kind_of status ~metasenv [] ty in
 656         let ctx0,res = split_kind_prods [] ty in
 657         let ctx,bo =
 658          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 659         (match classify status ~metasenv ctx bo with
 660           | `Type
 661           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 662               let nicectx =
 663                List.map2
 664                 (fun p1 n ->
 665                   HExtlib.map_option (fun (_,k) ->
 666                    (*CSC: BUG here, clashes*)
 667                    String.uncapitalize (fst n),k) p1)
 668                 ctx0 ctx
 669               in
 670               let bo = typ_of status ~metasenv ctx bo in
 671                status#set_extraction_db
 672                 (ReferenceMap.add ref (nicectx,Some bo)
 673                   status#extraction_db),
 674                Success (ref,TypeDefinition((nicectx,res),bo))
 675           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 676           | `PropKind
 677           | `Proposition -> status, Erased
 678           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 679     | `PropKind
 680     | `Proposition -> status, Erased
 681     | `KindOrType (* ??? *)
 682     | `Type ->
 683        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 684        let ty = typ_of status ~metasenv [] ty in
 685         status,
 686         Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 687     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 688 ;;
 689
 690 let object_of_inductive status ~metasenv uri ind leftno il =
 691  let status,_,rev_tyl =
 692   List.fold_left
 693    (fun (status,i,res) (_,_,arity,cl) ->
 694      match classify_not_term status [] arity with
 695       | `Proposition
 696       | `KindOrType
 697       | `Type -> assert false (* IMPOSSIBLE *)
 698       | `PropKind -> status,i+1,res
 699       | `Kind ->
 700           let arity = kind_of status ~metasenv [] arity in
 701           let ctx,_ = split_kind_prods [] arity in
 702           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 703           let ref =
 704            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 705           let status =
 706            status#set_extraction_db
 707             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 708           let cl =
 709            HExtlib.list_mapi
 710             (fun (_,_,ty) j ->
 711               let ctx,ty =
 712                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 713               let ty = typ_of status ~metasenv ctx ty in
 714                NReference.mk_constructor (j+1) ref,ty
 715             ) cl
 716           in
 717            status,i+1,(ref,left,right,cl)::res
 718    ) (status,0,[]) il
 719  in
 720   match rev_tyl with
 721      [] -> status,Erased
 722    | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
 723 ;;
 724
 725 let object_of status (uri,height,metasenv,subst,obj_kind) =
 726   let obj_kind = apply_subst subst obj_kind in
 727       match obj_kind with
 728         | NCic.Constant (_,_,None,ty,_) ->
 729           let ref = NReference.reference_of_spec uri NReference.Decl in
 730           (match classify status ~metasenv [] ty with
 731             | `Kind ->
 732               let ty = kind_of status ~metasenv [] ty in
 733               let ctx,_ as res = split_kind_prods [] ty in
 734                 status#set_extraction_db
 735                   (ReferenceMap.add ref (ctx,None) status#extraction_db),
 736                     Success (ref, TypeDeclaration res)
 737             | `PropKind
 738             | `Proposition -> status, Erased
 739             | `Type
 740             | `KindOrType (*???*) ->
 741               let ty = typ_of status ~metasenv [] ty in
 742                 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
 743             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 744         | NCic.Constant (_,_,Some bo,ty,_) ->
 745            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 746             object_of_constant status ~metasenv ref bo ty
 747         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 748           let _,status,objs =
 749             List.fold_right
 750             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 751               let ref =
 752                if fix_or_cofix then
 753                 NReference.reference_of_spec
 754                  uri (NReference.Fix (i,recno,height))
 755                else
 756                 NReference.reference_of_spec uri (NReference.CoFix i)
 757               in
 758               let status,obj = object_of_constant ~metasenv status ref bo ty in
 759                 match obj with
 760                   | Success (ref,obj) -> i+1,status, (ref,obj)::res
 761                   | _ -> i+1,status, res) fs (0,status,[])
 762           in
 763             status, Success (dummyref,LetRec objs)
 764         | NCic.Inductive (ind,leftno,il,_) ->
 765            object_of_inductive status ~metasenv uri ind leftno il
 766
 767 (************************ HASKELL *************************)
 768
 769 (* -----------------------------------------------------------------------------
 770  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 771  * -----------------------------------------------------------------------------
 772  *)
 773 let (|>) f g =
 774   fun x -> g (f x)
 775 ;;
 776
 777 let curry f x y =
 778   f (x, y)
 779 ;;
 780
 781 let uncurry f (x, y) =
 782   f x y
 783 ;;
 784
 785 let rec char_list_of_string s =
 786   let l = String.length s in
 787   let rec aux buffer s =
 788     function
 789       | 0 -> buffer
 790       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 791   in
 792     aux [] s l
 793 ;;
 794
 795 let string_of_char_list s =
 796   let rec aux buffer =
 797     function
 798       | []    -> buffer
 799       | x::xs -> aux (String.make 1 x ^ buffer) xs
 800   in
 801     aux "" s
 802 ;;
 803
 804 (* ----------------------------------------------------------------------------
 805  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 806  * and type variable names.
 807  * ----------------------------------------------------------------------------
 808  *)
 809
 810 let remove_underscores_and_mark =
 811   let rec aux char_list_buffer positions_buffer position =
 812     function
 813       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 814       | x::xs ->
 815         if x == '_' then
 816           aux char_list_buffer (position::positions_buffer) position xs
 817         else
 818           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 819   in
 820     aux [] [] 0
 821 ;;
 822
 823 let rec capitalize_marked_positions s =
 824   function
 825     | []    -> s
 826     | x::xs ->
 827       if x < String.length s then
 828         let c = Char.uppercase (String.get s x) in
 829         let _ = String.set s x c in
 830           capitalize_marked_positions s xs
 831       else
 832         capitalize_marked_positions s xs
 833 ;;
 834
 835 let contract_underscores_and_capitalise =
 836   char_list_of_string |>
 837   remove_underscores_and_mark |>
 838   uncurry capitalize_marked_positions
 839 ;;
 840
 841 let idiomatic_haskell_type_name_of_string =
 842   contract_underscores_and_capitalise |>
 843   String.capitalize
 844 ;;
 845
 846 let idiomatic_haskell_term_name_of_string =
 847   contract_underscores_and_capitalise |>
 848   String.uncapitalize
 849 ;;
 850
 851 (*CSC: code to be changed soon when we implement constructors and
 852   we fix the code for term application *)
 853 let classify_reference status ref =
 854   if ReferenceMap.mem ref status#extraction_db then
 855     `TypeName
 856   else
 857    let NReference.Ref (_,ref) = ref in
 858     match ref with
 859        NReference.Con _ -> `Constructor
 860      | NReference.Ind _ -> assert false
 861      | _ -> `FunctionName
 862 ;;
 863
 864 let capitalize classification name =
 865   match classification with
 866     | `Constructor
 867     | `TypeName -> idiomatic_haskell_type_name_of_string name
 868     | `TypeVariable
 869     | `BoundVariable
 870     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 871 ;;
 872
 873 let pp_ref status ref =
 874  capitalize (classify_reference status ref)
 875   (NCicPp.r2s status true ref)
 876
 877 (* cons avoid duplicates *)
 878 let rec (@:::) name l =
 879  if name <> "" (* propositional things *) && name.[0] = '_' then
 880   let name = String.sub name 1 (String.length name - 1) in
 881   let name = if name = "" then "a" else name in
 882    name @::: l
 883  else if List.mem name l then (name ^ "'") @::: l
 884  else name,l
 885 ;;
 886
 887 let (@::) x l = let x,l = x @::: l in x::l;;
 888
 889 let rec pretty_print_type status ctxt =
 890   function
 891     | Var n -> List.nth ctxt (n-1)
 892     | Unit -> "()"
 893     | Top -> "Top"
 894     | TConst ref -> pp_ref status ref
 895     | Arrow (t1,t2) ->
 896         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 897          pretty_print_type status ("_"::ctxt) t2
 898     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 899     | Forall (name, kind, t) ->
 900       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 901       let name = capitalize `TypeVariable name in
 902       let name,ctxt = name@:::ctxt in
 903         if size_of_kind kind > 1 then
 904           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 905         else
 906           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 907    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 908
 909 let pretty_print_term_context status ctx1 ctx2 =
 910  let name_context, rev_res =
 911   List.fold_right
 912     (fun el (ctx1,rev_res) ->
 913       match el with
 914          None -> ""@::ctx1,rev_res
 915        | Some (name,`OfKind _) -> name@::ctx1,rev_res
 916        | Some (name,`OfType typ) ->
 917           let name,ctx1 = name@:::ctx1 in
 918            name::ctx1,
 919             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 920     ) ctx2 (ctx1,[]) in
 921   name_context, String.concat " " (List.rev rev_res)
 922
 923 let rec pretty_print_term status ctxt =
 924   function
 925     | Rel n -> List.nth ctxt (n-1)
 926     | UnitTerm -> "()"
 927     | Const ref -> pp_ref status ref
 928     | Lambda (name,t) ->
 929        let name = capitalize `BoundVariable name in
 930        let name,ctxt = name@:::ctxt in
 931         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 932     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 933     | LetIn (name,s,t) ->
 934        let name = capitalize `BoundVariable name in
 935        let name,ctxt = name@:::ctxt in
 936         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 937          pretty_print_term status (name::ctxt) t
 938     | BottomElim ->
 939        "error \"Unreachable code\""
 940     | UnsafeCoerce t ->
 941        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 942     | Match (r,matched,pl) ->
 943       if pl = [] then
 944        "error \"Case analysis over empty type\""
 945       else
 946        "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 947          String.concat "\n"
 948            (HExtlib.list_mapi
 949              (fun (bound_names,rhs) i ->
 950                let ref = NReference.mk_constructor (i+1) r in
 951                let name = pp_ref status ref in
 952                let ctxt,bound_names =
 953                 pretty_print_term_context status ctxt bound_names in
 954                let body =
 955                 pretty_print_term status ctxt rhs
 956                in
 957                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
 958              ) pl)
 959     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
 960     | TLambda (name,t) ->
 961        let name = capitalize `TypeVariable name in
 962         pretty_print_term status (name@::ctxt) t
 963     | Inst t -> pretty_print_term status ctxt t
 964 ;;
 965
 966 let rec pp_obj status (ref,obj_kind) =
 967   let pretty_print_context ctx =
 968     String.concat " " (List.rev (snd
 969       (List.fold_right
 970        (fun (x,kind) (l,res) ->
 971          let x,l = x @:::l in
 972          if size_of_kind kind > 1 then
 973           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 974          else
 975           x::l,x::res)
 976        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 977   in
 978  let namectx_of_ctx ctx =
 979   List.fold_right (@::)
 980    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 981  match obj_kind with
 982    TypeDeclaration (ctx,_) ->
 983     (* data?? unsure semantics: inductive type without constructor, but
 984        not matchable apparently *)
 985     if List.length ctx = 0 then
 986       "data " ^ pp_ref status ref
 987     else
 988       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
 989  | TypeDefinition ((ctx, _),ty) ->
 990     let namectx = namectx_of_ctx ctx in
 991     if List.length ctx = 0 then
 992       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
 993     else
 994       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 995  | TermDeclaration (ctx,ty) ->
 996     let name = pp_ref status ref in
 997       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 998       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 999  | TermDefinition ((ctx,ty),bo) ->
1000     let name = pp_ref status ref in
1001     let namectx = namectx_of_ctx ctx in
1002     (*CSC: BUG here *)
1003     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1004     name ^ " = " ^ pretty_print_term status namectx bo
1005  | LetRec l ->
1006     String.concat "\n" (List.map (pp_obj status) l)
1007  | Algebraic il ->
1008     String.concat "\n"
1009      (List.map
1010       (fun ref,left,right,cl ->
1011         "data " ^ pp_ref status ref ^ " " ^
1012         pretty_print_context (right@left) ^ " where\n  " ^
1013         String.concat "\n  " (List.map
1014          (fun ref,tys ->
1015            let namectx = namectx_of_ctx left in
1016             pp_ref status ref ^ " :: " ^
1017              pretty_print_type status namectx tys
1018          ) cl
1019       )) il)
1020  (* inductive and records missing *)
1021
1022 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1023  let status, obj = object_of status obj in
1024   status,
1025    match obj with
1026       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
1027     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
1028     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
1029     | Success o -> pp_obj status o ^ "\n"