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 (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 rec 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 (String.get s x) in
1017         let _ = String.set s x c in
1018           capitalize_marked_positions s xs
1019       else
1020         capitalize_marked_positions s xs
1021 ;;
1022
1023 let contract_underscores_and_capitalise =
1024   char_list_of_string |>
1025   remove_underscores_and_mark |>
1026   uncurry capitalize_marked_positions
1027 ;;
1028
1029 let idiomatic_haskell_type_name_of_string =
1030   contract_underscores_and_capitalise |>
1031   String.capitalize
1032 ;;
1033
1034 let idiomatic_haskell_term_name_of_string =
1035   contract_underscores_and_capitalise |>
1036   String.uncapitalize
1037 ;;
1038
1039 let classify_reference status ref =
1040  try
1041   match snd (ReferenceMap.find ref (fst status#extraction_db)) with
1042      `Type _ -> `TypeName
1043    | `Constructor _ -> `Constructor
1044    | `Function _ -> `FunctionName
1045  with
1046   Not_found ->
1047 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ Ref.string_of_reference ref); `FunctionName
1048 ;;
1049
1050 let capitalize classification name =
1051   match classification with
1052     | `Constructor
1053     | `TypeName -> idiomatic_haskell_type_name_of_string name
1054     | `TypeVariable
1055     | `BoundVariable
1056     | `FunctionName -> idiomatic_haskell_term_name_of_string name
1057 ;;
1058
1059 let pp_ref status ref =
1060  capitalize (classify_reference status ref)
1061   (try fst (ReferenceMap.find ref (fst status#extraction_db))
1062    with Not_found ->
1063 prerr_endline ("BUG with coercions: " ^ Ref.string_of_reference ref);
1064 (*assert false*)
1065  NCicPp.r2s status true ref (* BUG: this should never happen *)
1066 )
1067
1068 (* cons avoid duplicates *)
1069 let rec (@:::) name l =
1070  if name <> "" (* propositional things *) && name.[0] = '_' then
1071   let name = String.sub name 1 (String.length name - 1) in
1072   let name = if name = "" then "a" else name in
1073    name @::: l
1074  else if List.mem name l then (name ^ "'") @::: l
1075  else name,l
1076 ;;
1077
1078 let (@::) x l = let x,l = x @::: l in x::l;;
1079
1080 let rec pretty_print_type status ctxt =
1081   function
1082     | Var n -> List.nth ctxt (n-1)
1083     | Unit -> "()"
1084     | Top -> "GHC.Prim.Any"
1085     | TConst ref -> pp_ref status ref
1086     | Arrow (t1,t2) ->
1087         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
1088          pretty_print_type status ("_"::ctxt) t2
1089     | TSkip t -> pretty_print_type status ("_"::ctxt) t
1090     | Forall (name, kind, t) ->
1091       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
1092       let name = capitalize `TypeVariable name in
1093       let name,ctxt = name@:::ctxt in
1094         if size_of_kind kind > 1 then
1095           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
1096         else
1097           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
1098    | TAppl tl ->
1099       String.concat " "
1100        (List.map
1101          (fun t -> bracket ~prec:0 size_of_type
1102           (pretty_print_type status ctxt) t) tl)
1103 ;;
1104
1105 xdo_pretty_print_type := pretty_print_type;;
1106
1107
1108 let pretty_print_term_context status ctx1 ctx2 =
1109  let name_context, rev_res =
1110   List.fold_right
1111     (fun el (ctx1,rev_res) ->
1112       match el with
1113          None -> ""@::ctx1,rev_res
1114        | Some (name,`OfKind _) ->
1115           let name = capitalize `TypeVariable name in
1116            name@::ctx1,rev_res
1117        | Some (name,`OfType typ) ->
1118           let name = capitalize `TypeVariable name in
1119           let name,ctx1 = name@:::ctx1 in
1120            name::ctx1,
1121             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
1122     ) ctx2 (ctx1,[]) in
1123   name_context, String.concat " " (List.rev rev_res)
1124
1125 let rec pretty_print_term status ctxt =
1126   function
1127     | Rel n -> List.nth ctxt (n-1)
1128     | UnitTerm -> "()"
1129     | Const ref -> pp_ref status ref
1130     | Lambda (name,t) ->
1131        let name = capitalize `BoundVariable name in
1132        let name,ctxt = name@:::ctxt in
1133         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
1134     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
1135     | LetIn (name,s,t) ->
1136        let name = capitalize `BoundVariable name in
1137        let name,ctxt = name@:::ctxt in
1138         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
1139          pretty_print_term status (name::ctxt) t
1140     | BottomElim ->
1141        "error \"Unreachable code\""
1142     | UnsafeCoerce t ->
1143        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
1144     | Match (r,matched,pl) ->
1145       if pl = [] then
1146        "error \"Case analysis over empty type\""
1147       else
1148        "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
1149          String.concat " ;\n"
1150            (HExtlib.list_mapi
1151              (fun (bound_names,rhs) i ->
1152                let ref = Ref.mk_constructor (i+1) r in
1153                let name = pp_ref status ref in
1154                let ctxt,bound_names =
1155                 pretty_print_term_context status ctxt bound_names in
1156                let body =
1157                 pretty_print_term status ctxt rhs
1158                in
1159                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
1160              ) pl) ^ "}\n  "
1161     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
1162     | TLambda (name,t) ->
1163        let name = capitalize `TypeVariable name in
1164         pretty_print_term status (name@::ctxt) t
1165     | Inst t -> pretty_print_term status ctxt t
1166 ;;
1167
1168 xdo_pretty_print_term := pretty_print_term;;
1169
1170 let rec pp_obj status (_,ref,obj_kind) =
1171   let pretty_print_context ctx =
1172     String.concat " " (List.rev (snd
1173       (List.fold_right
1174        (fun (x,kind) (l,res) ->
1175          let x,l = x @:::l in
1176          if size_of_kind kind > 1 then
1177           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
1178          else
1179           x::l,x::res)
1180        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
1181   in
1182  let namectx_of_ctx ctx =
1183   List.fold_right (@::)
1184    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
1185  match obj_kind with
1186    TypeDeclaration (ctx,_) ->
1187     (* data?? unsure semantics: inductive type without constructor, but
1188        not matchable apparently *)
1189     if List.length ctx = 0 then
1190       "data " ^ pp_ref status ref
1191     else
1192       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1193  | TypeDefinition ((ctx, _),ty) ->
1194     let namectx = namectx_of_ctx ctx in
1195     if List.length ctx = 0 then
1196       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1197     else
1198       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1199  | TermDeclaration (ctx,ty) ->
1200     let name = pp_ref status ref in
1201       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1202       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1203  | TermDefinition ((ctx,ty),bo) ->
1204     let name = pp_ref status ref in
1205     let namectx = namectx_of_ctx ctx in
1206     (*CSC: BUG here *)
1207     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1208     name ^ " = " ^ pretty_print_term status namectx bo
1209  | LetRec l ->
1210     String.concat "\n" (List.map (pp_obj status) l)
1211  | Algebraic il ->
1212     String.concat "\n"
1213      (List.map
1214       (fun _,ref,left,right,cl ->
1215         "data " ^ pp_ref status ref ^ " " ^
1216         pretty_print_context (right@left) ^ " where\n  " ^
1217         String.concat "\n  " (List.map
1218          (fun ref,tys ->
1219            let namectx = namectx_of_ctx left in
1220             pp_ref status ref ^ " :: " ^
1221              pretty_print_type status namectx tys
1222          ) cl) (*^ "\n    deriving (Prelude.Show)"*)
1223       ) il)
1224  (* inductive and records missing *)
1225
1226 let rec infos_of (info,_,obj_kind) =
1227  info @
1228   match obj_kind with
1229      LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1230    | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1231    | _ -> []
1232
1233 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1234  let status, obj = object_of status obj in
1235   status,
1236    match obj with
1237       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1238     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1239     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1240     | Success o -> pp_obj status o ^ "\n", infos_of o
1241
1242 let refresh_uri_in_typ ~refresh_uri_in_reference =
1243  let rec refresh_uri_in_typ =
1244   function
1245    | Var _
1246    | Unit
1247    | Top as t -> t
1248    | TConst r -> TConst (refresh_uri_in_reference r)
1249    | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1250    | TSkip t -> TSkip (refresh_uri_in_typ t)
1251    | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1252    | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1253  in
1254   refresh_uri_in_typ
1255
1256 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1257  List.map
1258   (function (ref,el) ->
1259     match el with
1260        name,`Constructor typ ->
1261         let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
1262          refresh_uri_in_reference ref, (name,`Constructor typ)
1263      | name,`Function typ ->
1264         let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
1265          refresh_uri_in_reference ref, (name,`Function typ)
1266      | name,`Type (ctx,typ) ->
1267          let typ =
1268           match typ with
1269              None -> None
1270            | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1271          in
1272           refresh_uri_in_reference ref, (name,`Type (ctx,typ)))
1273   infos