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