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