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 (_,_,_,_) -> assert false (* TODO *)
 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 (*TODO: HOW??*)
 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       | Forall (_,_,t) ->
 611          (match classify status ~metasenv context arg with
 612            | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
 613            | `Proposition
 614            | `Term `TypeFormer
 615            | `Kind ->
 616                eat_args status metasenv (UnsafeCoerce (Inst acc))
 617                 context (fomega_subst 1 Unit t) tl
 618            | `Term _ -> assert false (*TODO: ????*)
 619            | `KindOrType
 620            | `Type ->
 621                eat_args status metasenv (Inst acc)
 622                 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
 623                  tl)
 624       | TSkip t ->
 625          eat_args status metasenv acc context t tl
 626       | Top -> assert false (*TODO: HOW??*)
 627       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 628 ;;
 629
 630 type 'a result =
 631   | Erased
 632   | OutsideTheory
 633   | Failure of string
 634   | Success of 'a
 635 ;;
 636
 637 let object_of_constant status ~metasenv ref bo ty =
 638   match classify status ~metasenv [] ty with
 639     | `Kind ->
 640         let ty = kind_of status ~metasenv [] ty in
 641         let ctx0,res = split_kind_prods [] ty in
 642         let ctx,bo =
 643          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 644         (match classify status ~metasenv ctx bo with
 645           | `Type
 646           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 647               let nicectx =
 648                List.map2
 649                 (fun p1 n ->
 650                   HExtlib.map_option (fun (_,k) ->
 651                    (*CSC: BUG here, clashes*)
 652                    String.uncapitalize (fst n),k) p1)
 653                 ctx0 ctx
 654               in
 655               let bo = typ_of status ~metasenv ctx bo in
 656                status#set_extraction_db
 657                 (ReferenceMap.add ref (nicectx,Some bo)
 658                   status#extraction_db),
 659                Success (ref,TypeDefinition((nicectx,res),bo))
 660           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 661           | `PropKind
 662           | `Proposition -> status, Erased
 663           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 664     | `PropKind
 665     | `Proposition -> status, Erased
 666     | `KindOrType (* ??? *)
 667     | `Type ->
 668        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 669        let ty = typ_of status ~metasenv [] ty in
 670         status,
 671         Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 672     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 673 ;;
 674
 675 let object_of_inductive status ~metasenv uri ind leftno il =
 676  let status,_,rev_tyl =
 677   List.fold_left
 678    (fun (status,i,res) (_,_,arity,cl) ->
 679      match classify_not_term status [] arity with
 680       | `Proposition
 681       | `KindOrType
 682       | `Type -> assert false (* IMPOSSIBLE *)
 683       | `PropKind -> status,i+1,res
 684       | `Kind ->
 685           let arity = kind_of status ~metasenv [] arity in
 686           let ctx,_ = split_kind_prods [] arity in
 687           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 688           let ref =
 689            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 690           let status =
 691            status#set_extraction_db
 692             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 693           let cl =
 694            HExtlib.list_mapi
 695             (fun (_,_,ty) j ->
 696               let ctx,ty =
 697                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 698               let ty = typ_of status ~metasenv ctx ty in
 699                NReference.mk_constructor (j+1) ref,ty
 700             ) cl
 701           in
 702            status,i+1,(ref,left,right,cl)::res
 703    ) (status,0,[]) il
 704  in
 705   match rev_tyl with
 706      [] -> status,Erased
 707    | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
 708 ;;
 709
 710 let object_of status (uri,height,metasenv,subst,obj_kind) =
 711   let obj_kind = apply_subst subst obj_kind in
 712       match obj_kind with
 713         | NCic.Constant (_,_,None,ty,_) ->
 714           let ref = NReference.reference_of_spec uri NReference.Decl in
 715           (match classify status ~metasenv [] ty with
 716             | `Kind ->
 717               let ty = kind_of status ~metasenv [] ty in
 718               let ctx,_ as res = split_kind_prods [] ty in
 719                 status#set_extraction_db
 720                   (ReferenceMap.add ref (ctx,None) status#extraction_db),
 721                     Success (ref, TypeDeclaration res)
 722             | `PropKind
 723             | `Proposition -> status, Erased
 724             | `Type
 725             | `KindOrType (*???*) ->
 726               let ty = typ_of status ~metasenv [] ty in
 727                 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
 728             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 729         | NCic.Constant (_,_,Some bo,ty,_) ->
 730            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 731             object_of_constant status ~metasenv ref bo ty
 732         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 733           let _,status,objs =
 734             List.fold_right
 735             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 736               let ref =
 737                if fix_or_cofix then
 738                 NReference.reference_of_spec
 739                  uri (NReference.Fix (i,recno,height))
 740                else
 741                 NReference.reference_of_spec uri (NReference.CoFix i)
 742               in
 743               let status,obj = object_of_constant ~metasenv status ref bo ty in
 744                 match obj with
 745                   | Success (ref,obj) -> i+1,status, (ref,obj)::res
 746                   | _ -> i+1,status, res) fs (0,status,[])
 747           in
 748             status, Success (dummyref,LetRec objs)
 749         | NCic.Inductive (ind,leftno,il,_) ->
 750            object_of_inductive status ~metasenv uri ind leftno il
 751
 752 (************************ HASKELL *************************)
 753
 754 (* -----------------------------------------------------------------------------
 755  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 756  * -----------------------------------------------------------------------------
 757  *)
 758 let (|>) f g =
 759   fun x -> g (f x)
 760 ;;
 761
 762 let curry f x y =
 763   f (x, y)
 764 ;;
 765
 766 let uncurry f (x, y) =
 767   f x y
 768 ;;
 769
 770 let rec char_list_of_string s =
 771   let l = String.length s in
 772   let rec aux buffer s =
 773     function
 774       | 0 -> buffer
 775       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 776   in
 777     aux [] s l
 778 ;;
 779
 780 let string_of_char_list s =
 781   let rec aux buffer =
 782     function
 783       | []    -> buffer
 784       | x::xs -> aux (String.make 1 x ^ buffer) xs
 785   in
 786     aux "" s
 787 ;;
 788
 789 (* ----------------------------------------------------------------------------
 790  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 791  * and type variable names.
 792  * ----------------------------------------------------------------------------
 793  *)
 794
 795 let remove_underscores_and_mark =
 796   let rec aux char_list_buffer positions_buffer position =
 797     function
 798       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 799       | x::xs ->
 800         if x == '_' then
 801           aux char_list_buffer (position::positions_buffer) position xs
 802         else
 803           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 804   in
 805     aux [] [] 0
 806 ;;
 807
 808 let rec capitalize_marked_positions s =
 809   function
 810     | []    -> s
 811     | x::xs ->
 812       if x < String.length s then
 813         let c = Char.uppercase (String.get s x) in
 814         let _ = String.set s x c in
 815           capitalize_marked_positions s xs
 816       else
 817         capitalize_marked_positions s xs
 818 ;;
 819
 820 let contract_underscores_and_capitalise =
 821   char_list_of_string |>
 822   remove_underscores_and_mark |>
 823   uncurry capitalize_marked_positions
 824 ;;
 825
 826 let idiomatic_haskell_type_name_of_string =
 827   contract_underscores_and_capitalise |>
 828   String.capitalize
 829 ;;
 830
 831 let idiomatic_haskell_term_name_of_string =
 832   contract_underscores_and_capitalise |>
 833   String.uncapitalize
 834 ;;
 835
 836 (*CSC: code to be changed soon when we implement constructors and
 837   we fix the code for term application *)
 838 let classify_reference status ref =
 839   if ReferenceMap.mem ref status#extraction_db then
 840     `TypeName
 841   else
 842    let NReference.Ref (_,ref) = ref in
 843     match ref with
 844        NReference.Con _ -> `Constructor
 845      | NReference.Ind _ -> assert false
 846      | _ -> `FunctionName
 847 ;;
 848
 849 let capitalize classification name =
 850   match classification with
 851     | `Constructor
 852     | `TypeName -> idiomatic_haskell_type_name_of_string name
 853     | `TypeVariable
 854     | `BoundVariable
 855     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 856 ;;
 857
 858 let pp_ref status ref =
 859  capitalize (classify_reference status ref)
 860   (NCicPp.r2s status true ref)
 861
 862 (* cons avoid duplicates *)
 863 let rec (@:::) name l =
 864  if name <> "" (* propositional things *) && name.[0] = '_' then
 865   let name = String.sub name 1 (String.length name - 1) in
 866   let name = if name = "" then "a" else name in
 867    name @::: l
 868  else if List.mem name l then (name ^ "'") @::: l
 869  else name,l
 870 ;;
 871
 872 let (@::) x l = let x,l = x @::: l in x::l;;
 873
 874 let rec pretty_print_type status ctxt =
 875   function
 876     | Var n -> List.nth ctxt (n-1)
 877     | Unit -> "()"
 878     | Top -> assert false (* ??? *)
 879     | TConst ref -> pp_ref status ref
 880     | Arrow (t1,t2) ->
 881         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 882          pretty_print_type status ("_"::ctxt) t2
 883     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 884     | Forall (name, kind, t) ->
 885       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 886       let name = capitalize `TypeVariable name in
 887       let name,ctxt = name@:::ctxt in
 888         if size_of_kind kind > 1 then
 889           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 890         else
 891           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 892    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 893
 894 let pretty_print_term_context status ctx1 ctx2 =
 895  let name_context, rev_res =
 896   List.fold_right
 897     (fun el (ctx1,rev_res) ->
 898       match el with
 899          None -> ""@::ctx1,rev_res
 900        | Some (name,`OfKind _) -> name@::ctx1,rev_res
 901        | Some (name,`OfType typ) ->
 902           let name,ctx1 = name@:::ctx1 in
 903            name::ctx1,
 904             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 905     ) ctx2 (ctx1,[]) in
 906   name_context, String.concat " " (List.rev rev_res)
 907
 908 let rec pretty_print_term status ctxt =
 909   function
 910     | Rel n -> List.nth ctxt (n-1)
 911     | UnitTerm -> "()"
 912     | Const ref -> pp_ref status ref
 913     | Lambda (name,t) ->
 914        let name = capitalize `BoundVariable name in
 915        let name,ctxt = name@:::ctxt in
 916         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 917     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 918     | LetIn (name,s,t) ->
 919        let name = capitalize `BoundVariable name in
 920        let name,ctxt = name@:::ctxt in
 921         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 922          pretty_print_term status (name::ctxt) t
 923     | BottomElim ->
 924        "error \"Unreachable code\""
 925     | UnsafeCoerce t ->
 926        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 927     | Match (r,matched,pl) ->
 928       if pl = [] then
 929        "error \"Case analysis over empty type\""
 930       else
 931        "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 932          String.concat "\n"
 933            (HExtlib.list_mapi
 934              (fun (bound_names,rhs) i ->
 935                let ref = NReference.mk_constructor (i+1) r in
 936                let name = pp_ref status ref in
 937                let ctxt,bound_names =
 938                 pretty_print_term_context status ctxt bound_names in
 939                let body =
 940                 pretty_print_term status ctxt rhs
 941                in
 942                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
 943              ) pl)
 944     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
 945     | TLambda (name,t) ->
 946        let name = capitalize `TypeVariable name in
 947         pretty_print_term status (name@::ctxt) t
 948     | Inst t -> pretty_print_term status ctxt t
 949 ;;
 950
 951 let rec pp_obj status (ref,obj_kind) =
 952   let pretty_print_context ctx =
 953     String.concat " " (List.rev (snd
 954       (List.fold_right
 955        (fun (x,kind) (l,res) ->
 956          let x,l = x @:::l in
 957          if size_of_kind kind > 1 then
 958           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 959          else
 960           x::l,x::res)
 961        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 962   in
 963  let namectx_of_ctx ctx =
 964   List.fold_right (@::)
 965    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 966  match obj_kind with
 967    TypeDeclaration (ctx,_) ->
 968     (* data?? unsure semantics: inductive type without constructor, but
 969        not matchable apparently *)
 970     if List.length ctx = 0 then
 971       "data " ^ pp_ref status ref
 972     else
 973       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
 974  | TypeDefinition ((ctx, _),ty) ->
 975     let namectx = namectx_of_ctx ctx in
 976     if List.length ctx = 0 then
 977       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
 978     else
 979       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 980  | TermDeclaration (ctx,ty) ->
 981     let name = pp_ref status ref in
 982       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 983       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 984  | TermDefinition ((ctx,ty),bo) ->
 985     let name = pp_ref status ref in
 986     let namectx = namectx_of_ctx ctx in
 987     (*CSC: BUG here *)
 988     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 989     name ^ " = " ^ pretty_print_term status namectx bo
 990  | LetRec l ->
 991     String.concat "\n" (List.map (pp_obj status) l)
 992  | Algebraic il ->
 993     String.concat "\n"
 994      (List.map
 995       (fun ref,left,right,cl ->
 996         "data " ^ pp_ref status ref ^ " " ^
 997         pretty_print_context (right@left) ^ " where\n  " ^
 998         String.concat "\n  " (List.map
 999          (fun ref,tys ->
1000            let namectx = namectx_of_ctx left in
1001             pp_ref status ref ^ " :: " ^
1002              pretty_print_type status namectx tys
1003          ) cl
1004       )) il)
1005  (* inductive and records missing *)
1006
1007 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1008  let status, obj = object_of status obj in
1009   status,
1010    match obj with
1011       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
1012     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
1013     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
1014     | Success o -> pp_obj status o ^ "\n"