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