matita/components/ng_extraction/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 module Ref = NReference
  29
  30 let fix_sorts t = t;;
  31 let apply_subst subst t = assert (subst=[]); t;;
  32
  33 type typformerreference = Ref.reference
  34 type reference = Ref.reference
  35
  36 type kind =
  37   | Type
  38   | KArrow of kind * kind
  39   | KSkip of kind (* dropped abstraction *)
  40
  41 let rec size_of_kind =
  42   function
  43     | Type -> 1
  44     | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
  45     | KSkip k -> size_of_kind k
  46 ;;
  47
  48 let bracket ?(prec=1) size_of pp o =
  49   if size_of o > prec then
  50     "(" ^ pp o ^ ")"
  51   else
  52     pp o
  53 ;;
  54
  55 let rec pretty_print_kind =
  56   function
  57     | Type -> "*"
  58     | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
  59     | KSkip k -> pretty_print_kind k
  60 ;;
  61
  62 type typ =
  63   | Var of int
  64   | Unit
  65   | Top
  66   | TConst of typformerreference
  67   | Arrow of typ * typ
  68   | TSkip of typ
  69   | Forall of string * kind * typ
  70   | TAppl of typ list
  71
  72 let rec size_of_type =
  73   function
  74     | Var _ -> 0
  75     | Unit -> 0
  76     | Top -> 0
  77     | TConst _ -> 0
  78     | Arrow _ -> 2
  79     | TSkip t -> size_of_type t
  80     | Forall _ -> 2
  81     | TAppl _ -> 1
  82 ;;
  83
  84 (* None = dropped abstraction *)
  85 type typ_context = (string * kind) option list
  86 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
  87
  88 type typ_former_decl = typ_context * kind
  89 type typ_former_def = typ_former_decl * typ
  90
  91 type term =
  92   | Rel of int
  93   | UnitTerm
  94   | Const of reference
  95   | Lambda of string * (* typ **) term
  96   | Appl of term list
  97   | LetIn of string * (* typ **) term * term
  98   | Match of reference * term * (term_context * term) list
  99   | BottomElim
 100   | TLambda of string * term
 101   | Inst of (*typ_former **) term
 102   | Skip of term
 103   | UnsafeCoerce of term
 104 ;;
 105
 106 type term_former_decl = term_context * typ
 107 type term_former_def = term_former_decl * term
 108
 109 let mk_appl f x =
 110  match f with
 111     Appl args -> Appl (args@[x])
 112   | _ -> Appl [f;x]
 113
 114 let mk_tappl f l =
 115  match f with
 116     TAppl args -> TAppl (args@l)
 117   | _ -> TAppl (f::l)
 118
 119 let rec size_of_term =
 120   function
 121     | Rel _ -> 1
 122     | UnitTerm -> 1
 123     | Const _ -> 1
 124     | Lambda (_, body) -> 1 + size_of_term body
 125     | Appl l -> List.length l
 126     | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
 127     | Match (_, case, pats) -> 1 + size_of_term case + List.length pats
 128     | BottomElim -> 1
 129     | TLambda (_,t) -> size_of_term t
 130     | Inst t -> size_of_term t
 131     | Skip t -> size_of_term t
 132     | UnsafeCoerce t -> 1 + size_of_term t
 133 ;;
 134
 135 module ReferenceMap = Map.Make(struct type t = Ref.reference let compare = Ref.compare end)
 136
 137 module GlobalNames = Set.Make(String)
 138
 139 type info_el =
 140  string * [`Type of typ_context * typ option | `Constructor of typ | `Function of typ ]
 141 type info = (Ref.reference * info_el) list
 142 type db = info_el ReferenceMap.t * GlobalNames.t
 143
 144 let empty_info = []
 145
 146 type obj_kind =
 147    TypeDeclaration of typ_former_decl
 148  | TypeDefinition of typ_former_def
 149  | TermDeclaration of term_former_decl
 150  | TermDefinition of term_former_def
 151  | LetRec of (info * Ref.reference * obj_kind) list
 152    (* reference, left, right, constructors *)
 153  | Algebraic of (info * Ref.reference * typ_context * typ_context * (Ref.reference * typ) list) list
 154
 155 type obj = info * Ref.reference * obj_kind
 156
 157 (* For LetRec and Algebraic blocks *)
 158 let dummyref =
 159  let uri = NUri.uri_of_string "cic:/matita/dummy/indty.ind" in
 160  Ref.reference_of_spec uri (Ref.Ind (true,1,1))
 161
 162 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 163
 164 let max_not_term t1 t2 =
 165  match t1,t2 with
 166     `KindOrType,_
 167   | _,`KindOrType -> `KindOrType
 168   | `Kind,_
 169   | _,`Kind -> `Kind
 170   | `Type,_
 171   | _,`Type -> `Type
 172   | `PropKind,_
 173   | _,`PropKind -> `PropKind
 174   | `Proposition,`Proposition -> `Proposition
 175
 176 let sup = List.fold_left max_not_term `Proposition
 177
 178 let rec classify_not_term status context t =
 179  match NCicReduction.whd status ~subst:[] context t with
 180   | NCic.Sort s ->
 181      (match s with
 182          NCic.Prop
 183        | NCic.Type [`CProp,_] -> `PropKind
 184        | NCic.Type [`Type,_] -> `Kind
 185        | NCic.Type _ -> assert false)
 186   | NCic.Prod (b,s,t) ->
 187      (*CSC: using invariant on "_" *)
 188      classify_not_term status ((b,NCic.Decl s)::context) t
 189   | NCic.Implicit _
 190   | NCic.LetIn _
 191   | NCic.Const (Ref.Ref (_,Ref.CoFix _))
 192   | NCic.Appl [] ->
 193      assert false (* NOT POSSIBLE *)
 194   | NCic.Lambda (n,s,t) ->
 195      (* Lambdas can me met in branches of matches, expecially when the
 196         output type is a product *)
 197      classify_not_term status ((n,NCic.Decl s)::context) t
 198   | NCic.Match (_,_,_,pl) ->
 199      let classified_pl = List.map (classify_not_term status context) pl in
 200       sup classified_pl
 201   | NCic.Const (Ref.Ref (_,Ref.Fix _)) ->
 202      assert false (* IMPOSSIBLE *)
 203   | NCic.Meta _ -> assert false (* TODO *)
 204   | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix (i,_,_)) as r)::_)->
 205      let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
 206      let _,_,_,_,bo = List.nth l i in
 207       classify_not_term status [] bo
 208   | NCic.Appl (he::_) -> classify_not_term status context he
 209   | NCic.Rel n ->
 210      let rec find_sort typ =
 211       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 212         NCic.Sort NCic.Prop -> `Proposition
 213       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 214       | NCic.Sort (NCic.Type [`Type,_]) ->
 215          (*CSC: we could be more precise distinguishing the user provided
 216                 minimal elements of the hierarchies and classify these
 217                 as `Kind *)
 218          `KindOrType
 219       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 220       | NCic.Prod (_,_,t) ->
 221          (* we skipped arguments of applications, so here we need to skip
 222             products *)
 223          find_sort t
 224       | _ -> assert false (* NOT A SORT *)
 225      in
 226       (match List.nth context (n-1) with
 227           _,NCic.Decl typ -> find_sort typ
 228         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 229   | NCic.Const (Ref.Ref (_,Ref.Decl) as ref) ->
 230      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 231       (match classify_not_term status [] ty with
 232         | `Proposition
 233         | `Type -> assert false (* IMPOSSIBLE *)
 234         | `Kind
 235         | `KindOrType -> `Type
 236         | `PropKind -> `Proposition)
 237   | NCic.Const (Ref.Ref (_,Ref.Ind _) as ref) ->
 238      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 239      let _,_,arity,_ = List.nth ityl i in
 240       (match classify_not_term status [] arity with
 241         | `Proposition
 242         | `Type
 243         | `KindOrType -> assert false (* IMPOSSIBLE *)
 244         | `Kind -> `Type
 245         | `PropKind -> `Proposition)
 246   | NCic.Const (Ref.Ref (_,Ref.Con _))
 247   | NCic.Const (Ref.Ref (_,Ref.Def _)) ->
 248      assert false (* IMPOSSIBLE *)
 249 ;;
 250
 251 let classify status ~metasenv context t =
 252  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 253   | NCic.Sort _ ->
 254      (classify_not_term status context t : not_term :> [> not_term])
 255   | ty ->
 256      let ty = fix_sorts ty in
 257       `Term
 258         (match classify_not_term status context ty with
 259           | `Proposition -> `Proof
 260           | `Type -> `Term
 261           | `KindOrType -> `TypeFormerOrTerm
 262           | `Kind -> `TypeFormer
 263           | `PropKind -> `PropFormer)
 264 ;;
 265
 266
 267 let rec kind_of status ~metasenv context k =
 268  match NCicReduction.whd status ~subst:[] context k with
 269   | NCic.Sort NCic.Type _ -> Type
 270   | NCic.Sort _ -> assert false (* NOT A KIND *)
 271   | NCic.Prod (b,s,t) ->
 272      (match classify status ~metasenv context s with
 273        | `Kind ->
 274            KArrow (kind_of status ~metasenv context s,
 275             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 276        | `Type
 277        | `KindOrType
 278        | `Proposition
 279        | `PropKind ->
 280            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 281        | `Term _ -> assert false (* IMPOSSIBLE *))
 282   | NCic.Implicit _
 283   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 284   | NCic.Lambda _
 285   | NCic.Rel _
 286   | NCic.Const _ -> assert false (* NOT A KIND *)
 287   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 288                                    otherwise NOT A KIND *)
 289   | NCic.Meta _
 290   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 291 ;;
 292
 293 let rec skip_args status ~metasenv context =
 294  function
 295   | _,[] -> []
 296   | [],_ -> assert false (* IMPOSSIBLE *)
 297   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 298   | _::tl1,arg::tl2 ->
 299      match classify status ~metasenv context arg with
 300       | `KindOrType
 301       | `Type
 302       | `Term `TypeFormer ->
 303          Some arg::skip_args status ~metasenv context (tl1,tl2)
 304       | `Kind
 305       | `Proposition
 306       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 307       | `Term _ -> assert false (* IMPOSSIBLE *)
 308 ;;
 309
 310 class type g_status =
 311  object
 312   method extraction_db: db
 313  end
 314
 315 class virtual status =
 316  object
 317   inherit NCic.status
 318   val extraction_db = ReferenceMap.empty, GlobalNames.empty
 319   method extraction_db = extraction_db
 320   method set_extraction_db v = {< extraction_db = v >}
 321   method set_extraction_status
 322    : 'status. #g_status as 'status -> 'self
 323    = fun o -> {< extraction_db = o#extraction_db >}
 324  end
 325
 326 let xdo_pretty_print_type = ref (fun _ _ -> assert false)
 327 let do_pretty_print_type status ctx t =
 328  !xdo_pretty_print_type (status : #status :> status) ctx t
 329
 330 let xdo_pretty_print_term = ref (fun _ _ -> assert false)
 331 let do_pretty_print_term status ctx t =
 332  !xdo_pretty_print_term (status : #status :> status) ctx t
 333
 334 let term_ctx_of_type_ctx =
 335  List.map
 336   (function
 337       None -> None
 338     | Some (name,k) -> Some (name,`OfKind k))
 339
 340 let rec split_kind_prods context =
 341  function
 342   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 343   | KSkip ta -> split_kind_prods (None::context) ta
 344   | Type -> context,Type
 345 ;;
 346
 347 let rec split_typ_prods context =
 348  function
 349   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 350   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 351   | TSkip ta -> split_typ_prods (None::context) ta
 352   | _ as t -> context,t
 353 ;;
 354
 355 let rec glue_ctx_typ ctx typ =
 356  match ctx with
 357   | [] -> typ
 358   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 359   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 360   | None::ctx -> glue_ctx_typ ctx (TSkip typ)
 361 ;;
 362
 363 let rec split_typ_lambdas status n ~metasenv context typ =
 364  if n = 0 then context,typ
 365  else
 366   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 367    | NCic.Lambda (name,s,t) ->
 368       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 369    | t ->
 370       (* eta-expansion required *)
 371       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 372       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 373        | NCic.Prod (name,typ,_) ->
 374           split_typ_lambdas status (n-1) ~metasenv
 375            ((name,NCic.Decl typ)::context)
 376            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 377        | _ -> assert false (* IMPOSSIBLE *)
 378 ;;
 379
 380
 381 let rev_context_of_typformer status ~metasenv context =
 382  function
 383     NCic.Const (Ref.Ref (_,Ref.Ind _) as ref)
 384   | NCic.Const (Ref.Ref (_,Ref.Def _) as ref)
 385   | NCic.Const (Ref.Ref (_,Ref.Decl) as ref)
 386   | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref) ->
 387      (try
 388        match snd (ReferenceMap.find ref (fst status#extraction_db)) with
 389           `Type (ctx,_) -> List.rev ctx
 390         | `Constructor _
 391         | `Function _ -> assert false
 392       with
 393        Not_found ->
 394         (* This can happen only when we are processing the type of
 395            the constructor of a small singleton type. In this case
 396            we are not interested in all the type, but only in its
 397            backbone. That is why we can safely return the dummy context
 398            here *)
 399         let rec dummy = None::dummy in
 400         dummy)
 401   | NCic.Match _ -> assert false (* TODO ???? *)
 402   | NCic.Rel n ->
 403      let typ =
 404       match List.nth context (n-1) with
 405          _,NCic.Decl typ -> typ
 406        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 407      let typ_ctx = snd (HExtlib.split_nth n context) in
 408      let typ = kind_of status ~metasenv typ_ctx typ in
 409       List.rev (fst (split_kind_prods [] typ))
 410   | NCic.Meta _ -> assert false (* TODO *)
 411   | NCic.Const (Ref.Ref (_,Ref.Con _))
 412   | NCic.Const (Ref.Ref (_,Ref.CoFix _))
 413   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 414   | NCic.Appl _ | NCic.Prod _ ->
 415      assert false (* IMPOSSIBLE *)
 416
 417 let rec typ_of status ~metasenv context k =
 418  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 419   | NCic.Prod (b,s,t) ->
 420      (* CSC: non-invariant assumed here about "_" *)
 421      (match classify status ~metasenv context s with
 422        | `Kind ->
 423            Forall (b, kind_of status ~metasenv context s,
 424             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 425        | `Type
 426        | `KindOrType -> (* ??? *)
 427            Arrow (typ_of status ~metasenv context s,
 428             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 429        | `PropKind
 430        | `Proposition ->
 431            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 432        | `Term _ -> assert false (* IMPOSSIBLE *))
 433   | NCic.Sort _
 434   | NCic.Implicit _
 435   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 436   | NCic.Lambda _ -> Top (*assert false (* LAMBDA-LIFT INNER DECLARATION *)*)
 437   | NCic.Rel n -> Var n
 438   | NCic.Const ref -> TConst ref
 439   | NCic.Match (_,_,_,_)
 440   | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Fix _))::_) ->
 441      Top
 442   | NCic.Appl (he::args) ->
 443      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
 444      TAppl (typ_of status ~metasenv context he ::
 445       List.map
 446        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 447        (skip_args status ~metasenv context (rev_he_context,args)))
 448   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 449                                    otherwise NOT A TYPE *)
 450   | NCic.Meta _ -> assert false (*TODO*)
 451 ;;
 452
 453 let rec fomega_lift_type_from n k =
 454  function
 455   | Var m as t -> if m < k then t else Var (m + n)
 456   | Top -> Top
 457   | TConst _ as t -> t
 458   | Unit -> Unit
 459   | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
 460   | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
 461   | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
 462   | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
 463
 464 let fomega_lift_type n t =
 465  if n = 0 then t else fomega_lift_type_from n 0 t
 466
 467 let fomega_lift_term n t =
 468  let rec fomega_lift_term n k =
 469   function
 470    | Rel m as t -> if m < k then t else Rel (m + n)
 471    | BottomElim
 472    | UnitTerm
 473    | Const _ as t -> t
 474    | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
 475    | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
 476    | Appl args -> Appl (List.map (fomega_lift_term n k) args)
 477    | LetIn (name,m,bo) ->
 478       LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
 479    | Match (ref,t,pl) ->
 480       let lift_p (ctx,t) =
 481        let lift_context ctx =
 482         let len = List.length ctx in
 483          HExtlib.list_mapi
 484           (fun el i ->
 485             let j = len - i - 1 in
 486             match el with
 487                None
 488              | Some (_,`OfKind  _) as el -> el
 489              | Some (name,`OfType t) ->
 490                 Some (name,`OfType (fomega_lift_type_from n (k+j) t))
 491           ) ctx
 492        in
 493         lift_context ctx, fomega_lift_term n (k + List.length ctx) t
 494       in
 495       Match (ref,fomega_lift_term n k t,List.map lift_p pl)
 496    | Inst t -> Inst (fomega_lift_term n k t)
 497    | Skip t -> Skip (fomega_lift_term n (k+1) t)
 498    | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
 499  in
 500   if n = 0 then t else fomega_lift_term n 0 t
 501 ;;
 502
 503 let rec fomega_subst k t1 =
 504  function
 505   | Var n ->
 506      if k=n then fomega_lift_type (k-1) t1
 507      else if n < k then Var n
 508      else Var (n-1)
 509   | Top -> Top
 510   | TConst ref -> TConst ref
 511   | Unit -> Unit
 512   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 513   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 514   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 515   | TAppl (he::args) ->
 516      mk_tappl (fomega_subst k t1 he) (List.map (fomega_subst k t1) args)
 517   | TAppl [] -> assert false
 518
 519 let fomega_lookup status ref =
 520  try
 521   match snd (ReferenceMap.find ref (fst status#extraction_db)) with
 522      `Type (_,bo) -> bo
 523    | `Constructor _
 524    | `Function _ -> assert false
 525  with
 526   Not_found ->
 527 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); None
 528
 529 let rec fomega_whd status ty =
 530  match ty with
 531  | TConst r ->
 532     (match fomega_lookup status r with
 533         None -> ty
 534       | Some ty -> fomega_whd status ty)
 535  | TAppl (TConst r::args) ->
 536     (match fomega_lookup status r with
 537         None -> ty
 538       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 539  | _ -> ty
 540
 541 let rec fomega_conv_kind k1 k2 =
 542  match k1,k2 with
 543     Type,Type -> true
 544   | KArrow (s1,t1), KArrow (s2,t2) ->
 545      fomega_conv_kind s1 s2 && fomega_conv_kind t1 t2
 546   | KSkip k1, KSkip k2 -> fomega_conv_kind k1 k2
 547   | _,_ -> false
 548
 549 let rec fomega_conv status t1 t2 =
 550  match fomega_whd status t1, fomega_whd status t2 with
 551     Var n, Var m -> n=m
 552   | Unit, Unit -> true
 553   | Top, Top -> true
 554   | TConst r1, TConst r2 -> Ref.eq r1 r2
 555   | Arrow (s1,t1), Arrow (s2,t2) ->
 556      fomega_conv status s1 s2 && fomega_conv status t1 t2
 557   | TSkip t1, TSkip t2 -> fomega_conv status t1 t2
 558   | Forall (_,k1,t1), Forall (_,k2,t2) ->
 559      fomega_conv_kind k1 k2 && fomega_conv status t1 t2
 560   | TAppl tl1, TAppl tl2 ->
 561      (try
 562        List.fold_left2 (fun b t1 t2 -> b && fomega_conv status t1 t2)
 563         true tl1 tl2
 564       with
 565        Invalid_argument _ -> false)
 566   | _,_ -> false
 567
 568 exception PatchMe (* BUG: constructor of singleton type :-( *)
 569
 570 let type_of_constructor status ref =
 571  try
 572   match snd (ReferenceMap.find ref (fst status#extraction_db)) with
 573      `Constructor ty -> ty
 574    | _ -> assert false
 575  with
 576   Not_found -> raise PatchMe (* BUG: constructor of singleton type :-( *)
 577
 578 let type_of_appl_he status ~metasenv context =
 579  function
 580     NCic.Const (Ref.Ref (_,Ref.Con _) as ref)
 581   | NCic.Const (Ref.Ref (_,Ref.Def _) as ref)
 582   | NCic.Const (Ref.Ref (_,Ref.Decl) as ref)
 583   | NCic.Const (Ref.Ref (_,Ref.Fix _) as ref)
 584   | NCic.Const (Ref.Ref (_,Ref.CoFix _) as ref) ->
 585      (try
 586        match snd (ReferenceMap.find ref (fst status#extraction_db)) with
 587           `Type _ -> assert false
 588         | `Constructor ty
 589         | `Function ty -> ty
 590       with
 591        Not_found -> assert false)
 592   | NCic.Const (Ref.Ref (_,Ref.Ind _)) ->
 593      assert false (* IMPOSSIBLE *)
 594   | NCic.Rel n ->
 595      (match List.nth context (n-1) with
 596          _,NCic.Decl typ
 597        | _,NCic.Def (_,typ) ->
 598            (* recomputed every time *)
 599            typ_of status ~metasenv context
 600             (NCicSubstitution.lift status n typ))
 601   | (NCic.Lambda _
 602   | NCic.LetIn _
 603   | NCic.Match _) as t ->
 604      (* BUG: here we should implement a real type-checker since we are
 605         trusting the translation of the Cic one that could be wrong
 606         (e.g. pruned abstractions, etc.) *)
 607      (typ_of status ~metasenv context
 608       (NCicTypeChecker.typeof status ~metasenv ~subst:[] context t))
 609   | NCic.Meta _ -> assert false (* TODO *)
 610   | NCic.Sort _ | NCic.Implicit _ | NCic.Appl _ | NCic.Prod _ ->
 611      assert false (* IMPOSSIBLE *)
 612
 613 let rec term_of status ~metasenv context =
 614  function
 615   | NCic.Implicit _
 616   | NCic.Sort _
 617   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 618   | NCic.Lambda (b,ty,bo) ->
 619      (* CSC: non-invariant assumed here about "_" *)
 620      (match classify status ~metasenv context ty with
 621        | `Kind ->
 622            TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 623        | `KindOrType (* ??? *)
 624        | `Type ->
 625            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 626        | `PropKind
 627        | `Proposition ->
 628            (* CSC: LAZY ??? *)
 629            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 630        | `Term _ -> assert false (* IMPOSSIBLE *))
 631   | NCic.LetIn (b,ty,t,bo) ->
 632      (match classify status ~metasenv context t with
 633        | `Term `TypeFormerOrTerm (* ???? *)
 634        | `Term `Term ->
 635           LetIn (b,term_of status ~metasenv context t,
 636            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 637        | `Kind
 638        | `Type
 639        | `KindOrType
 640        | `PropKind
 641        | `Proposition
 642        | `Term `PropFormer
 643        | `Term `TypeFormer
 644        | `Term `Proof ->
 645          (* not in programming languages, we expand it *)
 646          term_of status ~metasenv context
 647           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 648   | NCic.Rel n -> Rel n
 649   | NCic.Const ref -> Const ref
 650   | NCic.Appl (he::args) ->
 651      let hety = type_of_appl_he status ~metasenv context he in
 652       eat_args status metasenv (term_of status ~metasenv context he) context
 653        hety args
 654   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 655                                    otherwise NOT A TYPE *)
 656   | NCic.Meta _ -> assert false (* TODO *)
 657   | NCic.Match (ref,_,t,pl) ->
 658      let patterns_of pl =
 659       let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
 660        let rec eat_branch n ty context ctx pat =
 661          match (ty, pat) with
 662          | TSkip t,_
 663          | Forall (_,_,t),_
 664          | Arrow (_, t), _ when n > 0 ->
 665             eat_branch (pred n) t context ctx pat
 666          | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
 667          (*CSC: unify the three cases below? *)
 668          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
 669            let ctx =
 670             (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
 671            let context = (name,NCic.Decl ty)::context in
 672             eat_branch 0 t context ctx t'
 673          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
 674            let ctx =
 675             (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
 676            let context = (name,NCic.Decl ty)::context in
 677             eat_branch 0 t context ctx t'
 678          | TSkip t,NCic.Lambda (name, ty, t') ->
 679             let ctx = None::ctx in
 680             let context = (name,NCic.Decl ty)::context in
 681              eat_branch 0 t context ctx t'
 682          | Top,_ -> assert false (* IMPOSSIBLE *)
 683          | TSkip _, _
 684          | Forall _,_
 685          | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
 686          | _, _ -> context,ctx, pat
 687        in
 688         try
 689          HExtlib.list_mapi
 690           (fun pat i ->
 691             let ref = Ref.mk_constructor (i+1) ref in
 692             let ty =
 693              (* BUG HERE, QUICK BUG WRONG PATCH IN PLACE *)
 694              try
 695               type_of_constructor status ref
 696              with
 697               PatchMe ->
 698                typ_of status ~metasenv context
 699                 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context
 700                  (NCic.Const ref))
 701             in
 702             let context,lhs,rhs = eat_branch leftno ty context [] pat in
 703             let rhs =
 704              (* UnsafeCoerce not always required *)
 705              UnsafeCoerce (term_of status ~metasenv context rhs)
 706             in
 707              lhs,rhs
 708           ) pl
 709         with Invalid_argument _ -> assert false
 710      in
 711      (match classify_not_term status [] (NCic.Const ref) with
 712       | `PropKind
 713       | `KindOrType
 714       | `Kind -> assert false (* IMPOSSIBLE *)
 715       | `Proposition ->
 716           (match patterns_of pl with
 717               [] -> BottomElim
 718             | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
 719             | _ -> assert false)
 720       | `Type ->
 721           Match (ref,term_of status ~metasenv context t, patterns_of pl))
 722 and eat_args status metasenv acc context tyhe =
 723  function
 724     [] -> acc
 725   | arg::tl ->
 726      match fomega_whd status tyhe with
 727         Arrow (s,t) ->
 728          let acc =
 729           match s with
 730              Unit -> mk_appl acc UnitTerm
 731            | _ ->
 732              let foarg = term_of status ~metasenv context arg in
 733               (* BUG HERE, we should implement a real type-checker instead of
 734                  trusting the Cic type *)
 735              let inferredty =
 736               typ_of status ~metasenv context
 737                (NCicTypeChecker.typeof status ~metasenv ~subst:[] context arg)in
 738               if fomega_conv status inferredty s then
 739                mk_appl acc foarg
 740               else
 741 (
 742 prerr_endline ("ARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg);
 743 let context = List.map fst context in
 744 prerr_endline ("HE = " ^ do_pretty_print_term status context acc);
 745 prerr_endline ("CONTEXT= " ^ String.concat " " context);
 746 prerr_endline ("NOT CONV: " ^ do_pretty_print_type status context inferredty ^ " vs " ^ do_pretty_print_type status context s);
 747                mk_appl acc (UnsafeCoerce foarg)
 748 )
 749          in
 750           eat_args status metasenv acc context (fomega_subst 1 Unit t) tl
 751       | Top ->
 752          let arg =
 753           match classify status ~metasenv context arg with
 754            | `PropKind
 755            | `Proposition
 756            | `Term `TypeFormer
 757            | `Term `PropFormer
 758            | `Term `Proof
 759            | `Type
 760            | `KindOrType
 761            | `Kind -> UnitTerm
 762            | `Term `TypeFormerOrTerm
 763            | `Term `Term -> term_of status ~metasenv context arg
 764          in
 765           (* BUG: what if an argument of Top has been erased??? *)
 766           eat_args status metasenv
 767            (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
 768            context Top tl
 769       | Forall (_,_,t) ->
 770 (*
 771 prerr_endline "FORALL";
 772 let xcontext = List.map fst context in
 773 prerr_endline ("TYPE: " ^ do_pretty_print_type status xcontext (fomega_whd status tyhe));
 774 prerr_endline ("fARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg);
 775 prerr_endline ("fHE = " ^ do_pretty_print_term status xcontext acc);
 776 prerr_endline ("fCONTEXT= " ^ String.concat " " xcontext);
 777 *)
 778          (match classify status ~metasenv context arg with
 779            | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
 780            | `Proposition
 781            | `Kind ->
 782                eat_args status metasenv (UnsafeCoerce (Inst acc))
 783                 context (fomega_subst 1 Unit t) tl
 784            | `KindOrType
 785            | `Term `TypeFormer
 786            | `Type ->
 787                eat_args status metasenv (Inst acc)
 788                 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
 789                  tl
 790            | `Term _ -> assert false (*TODO: ????*))
 791       | TSkip t ->
 792          eat_args status metasenv acc context t tl
 793       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 794 ;;
 795
 796 type 'a result =
 797   | Erased
 798   | OutsideTheory
 799   | Failure of string
 800   | Success of 'a
 801 ;;
 802
 803 let fresh_name_of_ref status ref =
 804  (*CSC: Patch while we wait for separate compilation *)
 805  let candidate =
 806   let name = NCicPp.r2s status true ref in
 807   let Ref.Ref (uri,_) = ref in
 808   let path = NUri.baseuri_of_uri uri in
 809   let path = String.sub path 5 (String.length path - 5) in
 810   let path = Str.global_replace (Str.regexp "/") "_" path in
 811    path ^ "_" ^ name
 812  in
 813  let rec freshen candidate =
 814   if GlobalNames.mem candidate (snd status#extraction_db) then
 815    freshen (candidate ^ "'")
 816   else
 817    candidate
 818  in
 819   freshen candidate
 820
 821 let register_info (db,names) (ref,(name,_ as info_el)) =
 822  ReferenceMap.add ref info_el db,GlobalNames.add name names
 823
 824 let register_name_and_info status (ref,info_el) =
 825  let name = fresh_name_of_ref status ref in
 826  let info = ref,(name,info_el) in
 827  let infos,names = status#extraction_db in
 828   status#set_extraction_db (register_info (infos,names) info), info
 829
 830 let register_infos = List.fold_left register_info
 831
 832 let object_of_constant status ~metasenv ref bo ty =
 833   match classify status ~metasenv [] ty with
 834     | `Kind ->
 835         let ty = kind_of status ~metasenv [] ty in
 836         let ctx0,res = split_kind_prods [] ty in
 837         let ctx,bo =
 838          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 839         (match classify status ~metasenv ctx bo with
 840           | `Type
 841           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 842               let nicectx =
 843                List.map2
 844                 (fun p1 n ->
 845                   HExtlib.map_option (fun (_,k) ->
 846                    (*CSC: BUG here, clashes*)
 847                    String.uncapitalize_ascii (fst n),k) p1)
 848                 ctx0 ctx
 849               in
 850               let bo = typ_of status ~metasenv ctx bo in
 851               let info = ref,`Type (nicectx,Some bo) in
 852               let status,info = register_name_and_info status info in
 853                status,Success ([info],ref,TypeDefinition((nicectx,res),bo))
 854           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 855           | `PropKind
 856           | `Proposition -> status, Erased
 857           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 858     | `PropKind
 859     | `Proposition -> status, Erased
 860     | `KindOrType (* ??? *)
 861     | `Type ->
 862        let ty = typ_of status ~metasenv [] ty in
 863        let info = ref,`Function ty in
 864        let status,info = register_name_and_info status info in
 865         status,
 866          Success ([info],ref, TermDefinition (split_typ_prods [] ty,
 867          term_of status ~metasenv [] bo))
 868     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 869 ;;
 870
 871 let object_of_inductive status ~metasenv uri ind leftno il =
 872  let status,_,rev_tyl =
 873   List.fold_left
 874    (fun (status,i,res) (_,_,arity,cl) ->
 875      match classify_not_term status [] arity with
 876       | `Proposition
 877       | `KindOrType
 878       | `Type -> assert false (* IMPOSSIBLE *)
 879       | `PropKind -> status,i+1,res
 880       | `Kind ->
 881           let arity = kind_of status ~metasenv [] arity in
 882           let ctx,_ = split_kind_prods [] arity in
 883           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 884           let ref =
 885            Ref.reference_of_spec uri (Ref.Ind (ind,i,leftno)) in
 886           let info = ref,`Type (ctx,None) in
 887           let status,info = register_name_and_info status info in
 888           let _,status,cl_rev,infos =
 889            List.fold_left
 890             (fun (j,status,res,infos) (_,_,ty) ->
 891               let ctx,ty =
 892                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 893               let ty = typ_of status ~metasenv ctx ty in
 894               let left = term_ctx_of_type_ctx left in
 895               let full_ty = glue_ctx_typ left ty in
 896               let ref = Ref.mk_constructor j ref in
 897               let info = ref,`Constructor full_ty in
 898               let status,info = register_name_and_info status info in
 899                j+1,status,((ref,ty)::res),info::infos
 900             ) (1,status,[],[]) cl
 901           in
 902            status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
 903    ) (status,0,[]) il
 904  in
 905   match rev_tyl with
 906      [] -> status,Erased
 907    | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
 908 ;;
 909
 910 let object_of status (uri,height,metasenv,subst,obj_kind) =
 911   let obj_kind = apply_subst subst obj_kind in
 912       match obj_kind with
 913         | NCic.Constant (_,_,None,ty,_) ->
 914           let ref = Ref.reference_of_spec uri Ref.Decl in
 915           (match classify status ~metasenv [] ty with
 916             | `Kind ->
 917               let ty = kind_of status ~metasenv [] ty in
 918               let ctx,_ as res = split_kind_prods [] ty in
 919               let info = ref,`Type (ctx,None) in
 920               let status,info = register_name_and_info status info in
 921                status, Success ([info],ref, TypeDeclaration res)
 922             | `PropKind
 923             | `Proposition -> status, Erased
 924             | `Type
 925             | `KindOrType (*???*) ->
 926               let ty = typ_of status ~metasenv [] ty in
 927               let info = ref,`Function ty in
 928               let status,info = register_name_and_info status info in
 929                status,Success ([info],ref,
 930                 TermDeclaration (split_typ_prods [] ty))
 931             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 932         | NCic.Constant (_,_,Some bo,ty,_) ->
 933            let ref = Ref.reference_of_spec uri (Ref.Def height) in
 934             object_of_constant status ~metasenv ref bo ty
 935         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 936           let _,status,objs =
 937             List.fold_right
 938             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 939               let ref =
 940                if fix_or_cofix then
 941                 Ref.reference_of_spec
 942                  uri (Ref.Fix (i,recno,height))
 943                else
 944                 Ref.reference_of_spec uri (Ref.CoFix i)
 945               in
 946               let status,obj = object_of_constant ~metasenv status ref bo ty in
 947                 match obj with
 948                   | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
 949                   | _ -> i+1,status, res) fs (0,status,[])
 950           in
 951             status, Success ([],dummyref,LetRec objs)
 952         | NCic.Inductive (ind,leftno,il,_) ->
 953            object_of_inductive status ~metasenv uri ind leftno il
 954
 955 (************************ HASKELL *************************)
 956
 957 (* -----------------------------------------------------------------------------
 958  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 959  * -----------------------------------------------------------------------------
 960  *)
 961 let (|>) f g =
 962   fun x -> g (f x)
 963 ;;
 964
 965 (*let curry f x y =
 966   f (x, y)
 967 ;;*)
 968
 969 let uncurry f (x, y) =
 970   f x y
 971 ;;
 972
 973 let char_list_of_string s =
 974   let l = String.length s in
 975   let rec aux buffer s =
 976     function
 977       | 0 -> buffer
 978       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 979   in
 980     aux [] s l
 981 ;;
 982
 983 let string_of_char_list s =
 984   let rec aux buffer =
 985     function
 986       | []    -> buffer
 987       | x::xs -> aux (String.make 1 x ^ buffer) xs
 988   in
 989     aux "" s
 990 ;;
 991
 992 (* ----------------------------------------------------------------------------
 993  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 994  * and type variable names.
 995  * ----------------------------------------------------------------------------
 996  *)
 997
 998 let remove_underscores_and_mark l =
 999   let rec aux char_list_buffer positions_buffer position =
1000     function
1001       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
1002       | x::xs ->
1003         if x == '_' then
1004           aux char_list_buffer (position::positions_buffer) position xs
1005         else
1006           aux (x::char_list_buffer) positions_buffer (position + 1) xs
1007   in
1008    if l = ['_'] then "_",[] else aux [] [] 0 l
1009 ;;
1010
1011 let rec capitalize_marked_positions s =
1012   function
1013     | []    -> s
1014     | x::xs ->
1015       if x < String.length s then
1016         let c = Char.uppercase_ascii (String.get s x) in
1017         let b = Bytes.of_string s in
1018         let _ = Bytes.set b x c in
1019         let s = Bytes.to_string b in
1020           capitalize_marked_positions s xs
1021       else
1022         capitalize_marked_positions s xs
1023 ;;
1024
1025 let contract_underscores_and_capitalise =
1026   char_list_of_string |>
1027   remove_underscores_and_mark |>
1028   uncurry capitalize_marked_positions
1029 ;;
1030
1031 let idiomatic_haskell_type_name_of_string =
1032   contract_underscores_and_capitalise |>
1033   String.capitalize_ascii
1034 ;;
1035
1036 let idiomatic_haskell_term_name_of_string =
1037   contract_underscores_and_capitalise |>
1038   String.uncapitalize_ascii
1039 ;;
1040
1041 let classify_reference status ref =
1042  try
1043   match snd (ReferenceMap.find ref (fst status#extraction_db)) with
1044      `Type _ -> `TypeName
1045    | `Constructor _ -> `Constructor
1046    | `Function _ -> `FunctionName
1047  with
1048   Not_found ->
1049 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); `FunctionName
1050 ;;
1051
1052 let capitalize classification name =
1053   match classification with
1054     | `Constructor
1055     | `TypeName -> idiomatic_haskell_type_name_of_string name
1056     | `TypeVariable
1057     | `BoundVariable
1058     | `FunctionName -> idiomatic_haskell_term_name_of_string name
1059 ;;
1060
1061 let pp_ref status ref =
1062  capitalize (classify_reference status ref)
1063   (try fst (ReferenceMap.find ref (fst status#extraction_db))
1064    with Not_found ->
1065 prerr_endline ("BUG with coercions: " ^ Ref.string_of_reference ref);
1066 (*assert false*)
1067  NCicPp.r2s status true ref (* BUG: this should never happen *)
1068 )
1069
1070 (* cons avoid duplicates *)
1071 let rec (@:::) name l =
1072  if name <> "" (* propositional things *) && name.[0] = '_' then
1073   let name = String.sub name 1 (String.length name - 1) in
1074   let name = if name = "" then "a" else name in
1075    name @::: l
1076  else if List.mem name l then (name ^ "'") @::: l
1077  else name,l
1078 ;;
1079
1080 let (@::) x l = let x,l = x @::: l in x::l;;
1081
1082 let rec pretty_print_type status ctxt =
1083   function
1084     | Var n -> List.nth ctxt (n-1)
1085     | Unit -> "()"
1086     | Top -> "GHC.Prim.Any"
1087     | TConst ref -> pp_ref status ref
1088     | Arrow (t1,t2) ->
1089         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
1090          pretty_print_type status ("_"::ctxt) t2
1091     | TSkip t -> pretty_print_type status ("_"::ctxt) t
1092     | Forall (name, kind, t) ->
1093       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
1094       let name = capitalize `TypeVariable name in
1095       let name,ctxt = name@:::ctxt in
1096         if size_of_kind kind > 1 then
1097           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
1098         else
1099           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
1100    | TAppl tl ->
1101       String.concat " "
1102        (List.map
1103          (fun t -> bracket ~prec:0 size_of_type
1104           (pretty_print_type status ctxt) t) tl)
1105 ;;
1106
1107 xdo_pretty_print_type := pretty_print_type;;
1108
1109
1110 let pretty_print_term_context status ctx1 ctx2 =
1111  let name_context, rev_res =
1112   List.fold_right
1113     (fun el (ctx1,rev_res) ->
1114       match el with
1115          None -> ""@::ctx1,rev_res
1116        | Some (name,`OfKind _) ->
1117           let name = capitalize `TypeVariable name in
1118            name@::ctx1,rev_res
1119        | Some (name,`OfType typ) ->
1120           let name = capitalize `TypeVariable name in
1121           let name,ctx1 = name@:::ctx1 in
1122            name::ctx1,
1123             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
1124     ) ctx2 (ctx1,[]) in
1125   name_context, String.concat " " (List.rev rev_res)
1126
1127 let rec pretty_print_term status ctxt =
1128   function
1129     | Rel n -> List.nth ctxt (n-1)
1130     | UnitTerm -> "()"
1131     | Const ref -> pp_ref status ref
1132     | Lambda (name,t) ->
1133        let name = capitalize `BoundVariable name in
1134        let name,ctxt = name@:::ctxt in
1135         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
1136     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
1137     | LetIn (name,s,t) ->
1138        let name = capitalize `BoundVariable name in
1139        let name,ctxt = name@:::ctxt in
1140         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
1141          pretty_print_term status (name::ctxt) t
1142     | BottomElim ->
1143        "error \"Unreachable code\""
1144     | UnsafeCoerce t ->
1145        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
1146     | Match (r,matched,pl) ->
1147       if pl = [] then
1148        "error \"Case analysis over empty type\""
1149       else
1150        "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
1151          String.concat " ;\n"
1152            (HExtlib.list_mapi
1153              (fun (bound_names,rhs) i ->
1154                let ref = Ref.mk_constructor (i+1) r in
1155                let name = pp_ref status ref in
1156                let ctxt,bound_names =
1157                 pretty_print_term_context status ctxt bound_names in
1158                let body =
1159                 pretty_print_term status ctxt rhs
1160                in
1161                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
1162              ) pl) ^ "}\n  "
1163     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
1164     | TLambda (name,t) ->
1165        let name = capitalize `TypeVariable name in
1166         pretty_print_term status (name@::ctxt) t
1167     | Inst t -> pretty_print_term status ctxt t
1168 ;;
1169
1170 xdo_pretty_print_term := pretty_print_term;;
1171
1172 let rec pp_obj status (_,ref,obj_kind) =
1173   let pretty_print_context ctx =
1174     String.concat " " (List.rev (snd
1175       (List.fold_right
1176        (fun (x,kind) (l,res) ->
1177          let x,l = x @:::l in
1178          if size_of_kind kind > 1 then
1179           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
1180          else
1181           x::l,x::res)
1182        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
1183   in
1184  let namectx_of_ctx ctx =
1185   List.fold_right (@::)
1186    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
1187  match obj_kind with
1188    TypeDeclaration (ctx,_) ->
1189     (* data?? unsure semantics: inductive type without constructor, but
1190        not matchable apparently *)
1191     if List.length ctx = 0 then
1192       "data " ^ pp_ref status ref
1193     else
1194       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1195  | TypeDefinition ((ctx, _),ty) ->
1196     let namectx = namectx_of_ctx ctx in
1197     if List.length ctx = 0 then
1198       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1199     else
1200       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1201  | TermDeclaration (ctx,ty) ->
1202     let name = pp_ref status ref in
1203       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1204       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1205  | TermDefinition ((ctx,ty),bo) ->
1206     let name = pp_ref status ref in
1207     let namectx = namectx_of_ctx ctx in
1208     (*CSC: BUG here *)
1209     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1210     name ^ " = " ^ pretty_print_term status namectx bo
1211  | LetRec l ->
1212     String.concat "\n" (List.map (pp_obj status) l)
1213  | Algebraic il ->
1214     String.concat "\n"
1215      (List.map
1216       (fun _,ref,left,right,cl ->
1217         "data " ^ pp_ref status ref ^ " " ^
1218         pretty_print_context (right@left) ^ " where\n  " ^
1219         String.concat "\n  " (List.map
1220          (fun ref,tys ->
1221            let namectx = namectx_of_ctx left in
1222             pp_ref status ref ^ " :: " ^
1223              pretty_print_type status namectx tys
1224          ) cl) (*^ "\n    deriving (Prelude.Show)"*)
1225       ) il)
1226  (* inductive and records missing *)
1227
1228 let infos_of (info,_,obj_kind) =
1229  info @
1230   match obj_kind with
1231      LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1232    | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1233    | _ -> []
1234
1235 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1236  let status, obj = object_of status obj in
1237   status,
1238    match obj with
1239       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1240     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1241     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1242     | Success o -> pp_obj status o ^ "\n", infos_of o
1243
1244 let refresh_uri_in_typ ~refresh_uri_in_reference =
1245  let rec refresh_uri_in_typ =
1246   function
1247    | Var _
1248    | Unit
1249    | Top as t -> t
1250    | TConst r -> TConst (refresh_uri_in_reference r)
1251    | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1252    | TSkip t -> TSkip (refresh_uri_in_typ t)
1253    | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1254    | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1255  in
1256   refresh_uri_in_typ
1257
1258 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1259  List.map
1260   (function (ref,el) ->
1261     match el with
1262        name,`Constructor typ ->
1263         let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
1264          refresh_uri_in_reference ref, (name,`Constructor typ)
1265      | name,`Function typ ->
1266         let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
1267          refresh_uri_in_reference ref, (name,`Function typ)
1268      | name,`Type (ctx,typ) ->
1269          let typ =
1270           match typ with
1271              None -> None
1272            | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1273          in
1274           refresh_uri_in_reference ref, (name,`Type (ctx,typ)))
1275   infos