matita/components/ng_kernel/nCicExtraction.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
  27
  28 let fix_sorts t = t;;
  29 let apply_subst subst t = assert (subst=[]); t;;
  30
  31 type typformerreference = NReference.reference
  32 type reference = NReference.reference
  33
  34 type kind =
  35   | Type
  36   | KArrow of kind * kind
  37   | KSkip of kind (* dropped abstraction *)
  38
  39 let rec size_of_kind =
  40   function
  41     | Type -> 1
  42     | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
  43     | KSkip k -> size_of_kind k
  44 ;;
  45
  46 let bracket size_of pp o =
  47   if size_of o > 1 then
  48     "(" ^ pp o ^ ")"
  49   else
  50     pp o
  51 ;;
  52
  53 let rec pretty_print_kind =
  54   function
  55     | Type -> "*"
  56     | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
  57     | KSkip k -> pretty_print_kind k
  58 ;;
  59
  60 type typ =
  61   | Var of int
  62   | Unit
  63   | Top
  64   | TConst of typformerreference
  65   | Arrow of typ * typ
  66   | TSkip of typ
  67   | Forall of string * kind * typ
  68   | TAppl of typ list
  69
  70 let rec size_of_type =
  71   function
  72     | Var v -> 1
  73     | Unit -> 1
  74     | Top -> 1
  75     | TConst c -> 1
  76     | Arrow _ -> 2
  77     | TSkip t -> size_of_type t
  78     | Forall _ -> 2
  79     | TAppl l -> 1
  80 ;;
  81
  82 type term =
  83   | Rel of int
  84   | UnitTerm
  85   | Const of reference
  86   | Lambda of string * (* typ **) term
  87   | Appl of term list
  88   | LetIn of string * (* typ **) term * term
  89   | Match of reference * term * term list
  90   | BottomElim
  91   | TLambda of (* string **) term
  92   | Inst of (*typ_former **) term
  93   | Skip of term
  94   | UnsafeCoerce of term
  95 ;;
  96
  97 let rec size_of_term =
  98   function
  99     | Rel r -> 1
 100     | UnitTerm -> 1
 101     | Const c -> 1
 102     | Lambda (name, body) -> 1 + size_of_term body
 103     | Appl l -> List.length l
 104     | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
 105     | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
 106     | BottomElim -> 1
 107     | TLambda t -> size_of_term t
 108     | Inst t -> size_of_term t
 109     | Skip t -> size_of_term t
 110     | UnsafeCoerce t -> 1 + size_of_term t
 111 ;;
 112 let unitty =
 113  NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
 114
 115 (* None = dropped abstraction *)
 116 type typ_context = (string * kind) option list
 117 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 118
 119 type typ_former_decl = typ_context * kind
 120 type typ_former_def = typ_former_decl * typ
 121
 122 type term_former_decl = term_context * typ
 123 type term_former_def = term_former_decl * term
 124
 125 type obj_kind =
 126    TypeDeclaration of typ_former_decl
 127  | TypeDefinition of typ_former_def
 128  | TermDeclaration of term_former_decl
 129  | TermDefinition of term_former_def
 130  | LetRec of (NReference.reference * obj_kind) list
 131    (* reference, left, right, constructors *)
 132  | Algebraic of (NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
 133
 134 type obj = NReference.reference * obj_kind
 135
 136 (* For LetRec and Algebraic blocks *)
 137 let dummyref =
 138  NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
 139
 140 let rec classify_not_term status context t =
 141  match NCicReduction.whd status ~subst:[] context t with
 142   | NCic.Sort s ->
 143      (match s with
 144          NCic.Prop
 145        | NCic.Type [`CProp,_] -> `PropKind
 146        | NCic.Type [`Type,_] -> `Kind
 147        | NCic.Type _ -> assert false)
 148   | NCic.Prod (b,s,t) ->
 149      (*CSC: using invariant on "_" *)
 150      classify_not_term status ((b,NCic.Decl s)::context) t
 151   | NCic.Implicit _
 152   | NCic.LetIn _
 153   | NCic.Lambda _
 154   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 155   | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
 156   | NCic.Match _
 157   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 158      (* be aware: we can be the head of an application *)
 159      assert false (* TODO *)
 160   | NCic.Meta _ -> assert false (* TODO *)
 161   | NCic.Appl (he::_) -> classify_not_term status context he
 162   | NCic.Rel n ->
 163      let rec find_sort typ =
 164       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 165         NCic.Sort NCic.Prop -> `Proposition
 166       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 167       | NCic.Sort (NCic.Type [`Type,_]) ->
 168          (*CSC: we could be more precise distinguishing the user provided
 169                 minimal elements of the hierarchies and classify these
 170                 as `Kind *)
 171          `KindOrType
 172       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 173       | NCic.Prod (_,_,t) ->
 174          (* we skipped arguments of applications, so here we need to skip
 175             products *)
 176          find_sort t
 177       | _ -> assert false (* NOT A SORT *)
 178      in
 179       (match List.nth context (n-1) with
 180           _,NCic.Decl typ -> find_sort typ
 181         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 182   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 183      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 184       (match classify_not_term status [] ty with
 185         | `Proposition
 186         | `Type -> assert false (* IMPOSSIBLE *)
 187         | `Kind
 188         | `KindOrType -> `Type
 189         | `PropKind -> `Proposition)
 190   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 191      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 192      let _,_,arity,_ = List.nth ityl i in
 193       (match classify_not_term status [] arity with
 194         | `Proposition
 195         | `Type
 196         | `KindOrType -> assert false (* IMPOSSIBLE *)
 197         | `Kind -> `Type
 198         | `PropKind -> `Proposition)
 199   | NCic.Const (NReference.Ref (_,NReference.Con _))
 200   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 201      assert false (* IMPOSSIBLE *)
 202 ;;
 203
 204 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 205
 206 let classify status ~metasenv context t =
 207  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 208   | NCic.Sort _ ->
 209      (classify_not_term status context t : not_term :> [> not_term])
 210   | ty ->
 211      let ty = fix_sorts ty in
 212       `Term
 213         (match classify_not_term status context ty with
 214           | `Proposition -> `Proof
 215           | `Type -> `Term
 216           | `KindOrType -> `TypeFormerOrTerm
 217           | `Kind -> `TypeFormer
 218           | `PropKind -> `PropFormer)
 219 ;;
 220
 221
 222 let rec kind_of status ~metasenv context k =
 223  match NCicReduction.whd status ~subst:[] context k with
 224   | NCic.Sort NCic.Type _ -> Type
 225   | NCic.Sort _ -> assert false (* NOT A KIND *)
 226   | NCic.Prod (b,s,t) ->
 227      (match classify status ~metasenv context s with
 228        | `Kind ->
 229            KArrow (kind_of status ~metasenv context s,
 230             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 231        | `Type
 232        | `KindOrType
 233        | `Proposition
 234        | `PropKind ->
 235            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 236        | `Term _ -> assert false (* IMPOSSIBLE *))
 237   | NCic.Implicit _
 238   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 239   | NCic.Lambda _
 240   | NCic.Rel _
 241   | NCic.Const _ -> assert false (* NOT A KIND *)
 242   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 243                                    otherwise NOT A KIND *)
 244   | NCic.Meta _
 245   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 246 ;;
 247
 248 let rec skip_args status ~metasenv context =
 249  function
 250   | _,[] -> []
 251   | [],_ -> assert false (* IMPOSSIBLE *)
 252   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 253   | _::tl1,arg::tl2 ->
 254      match classify status ~metasenv context arg with
 255       | `KindOrType
 256       | `Type
 257       | `Term `TypeFormer ->
 258          Some arg::skip_args status ~metasenv context (tl1,tl2)
 259       | `Kind
 260       | `Proposition
 261       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 262       | `Term _ -> assert false (* IMPOSSIBLE *)
 263 ;;
 264
 265 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 266
 267 type db = (typ_context * typ option) ReferenceMap.t
 268
 269 class type g_status =
 270  object
 271   method extraction_db: db
 272  end
 273
 274 class virtual status =
 275  object
 276   inherit NCic.status
 277   val extraction_db = ReferenceMap.empty
 278   method extraction_db = extraction_db
 279   method set_extraction_db v = {< extraction_db = v >}
 280   method set_extraction_status
 281    : 'status. #g_status as 'status -> 'self
 282    = fun o -> {< extraction_db = o#extraction_db >}
 283  end
 284
 285 let rec split_kind_prods context =
 286  function
 287   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 288   | KSkip ta -> split_kind_prods (None::context) ta
 289   | Type -> context,Type
 290 ;;
 291
 292 let rec split_typ_prods context =
 293  function
 294   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 295   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 296   | TSkip ta -> split_typ_prods (None::context) ta
 297   | _ as t -> context,t
 298 ;;
 299
 300 let rec glue_ctx_typ ctx typ =
 301  match ctx with
 302   | [] -> typ
 303   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 304   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 305   | None::ctx -> glue_ctx_typ ctx (TSkip typ)
 306 ;;
 307
 308 let rec split_typ_lambdas status n ~metasenv context typ =
 309  if n = 0 then context,typ
 310  else
 311   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 312    | NCic.Lambda (name,s,t) ->
 313       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 314    | t ->
 315       (* eta-expansion required *)
 316       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 317       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 318        | NCic.Prod (name,typ,_) ->
 319           split_typ_lambdas status (n-1) ~metasenv
 320            ((name,NCic.Decl typ)::context)
 321            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 322        | _ -> assert false (* IMPOSSIBLE *)
 323 ;;
 324
 325
 326 let context_of_typformer status ~metasenv context =
 327  function
 328     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 329   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 330   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 331   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 332      (try fst (ReferenceMap.find ref status#extraction_db)
 333       with
 334        Not_found -> assert false (* IMPOSSIBLE *))
 335   | NCic.Match _ -> assert false (* TODO ???? *)
 336   | NCic.Rel n ->
 337      let typ =
 338       match List.nth context (n-1) with
 339          _,NCic.Decl typ -> typ
 340        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 341      let typ_ctx = snd (HExtlib.split_nth n context) in
 342      let typ = kind_of status ~metasenv typ_ctx typ in
 343       fst (split_kind_prods [] typ)
 344   | NCic.Meta _ -> assert false (* TODO *)
 345   | NCic.Const (NReference.Ref (_,NReference.Con _))
 346   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 347   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 348   | NCic.Appl _ | NCic.Prod _ ->
 349      assert false (* IMPOSSIBLE *)
 350
 351 let rec typ_of status ~metasenv context k =
 352  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 353   | NCic.Prod (b,s,t) ->
 354      (* CSC: non-invariant assumed here about "_" *)
 355      (match classify status ~metasenv context s with
 356        | `Kind ->
 357            Forall (b, kind_of status ~metasenv context s,
 358             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 359        | `Type
 360        | `KindOrType -> (* ??? *)
 361            Arrow (typ_of status ~metasenv context s,
 362             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 363        | `PropKind
 364        | `Proposition ->
 365            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 366        | `Term _ -> assert false (* IMPOSSIBLE *))
 367   | NCic.Sort _
 368   | NCic.Implicit _
 369   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 370   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 371   | NCic.Rel n -> Var n
 372   | NCic.Const ref -> TConst ref
 373   | NCic.Appl (he::args) ->
 374      let he_context = context_of_typformer status ~metasenv context he in
 375      TAppl (typ_of status ~metasenv context he ::
 376       List.map
 377        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 378        (skip_args status ~metasenv context (List.rev he_context,args)))
 379   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 380                                    otherwise NOT A TYPE *)
 381   | NCic.Meta _
 382   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 383 ;;
 384
 385 let rec fomega_subst k t1 =
 386  function
 387   | Var n ->
 388      if k=n then t1
 389      else if n < k then Var n
 390      else Var (n-1)
 391   | Top -> Top
 392   | TConst ref -> TConst ref
 393   | Unit -> Unit
 394   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 395   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 396   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 397   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 398
 399 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 400
 401 let rec fomega_whd status ty =
 402  match ty with
 403  | TConst r ->
 404     (match fomega_lookup status r with
 405         None -> ty
 406       | Some ty -> fomega_whd status ty)
 407  | TAppl (TConst r::args) ->
 408     (match fomega_lookup status r with
 409         None -> ty
 410       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 411  | _ -> ty
 412
 413 let rec term_of status ~metasenv context =
 414  function
 415   | NCic.Implicit _
 416   | NCic.Sort _
 417   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 418   | NCic.Lambda (b,ty,bo) ->
 419      (* CSC: non-invariant assumed here about "_" *)
 420      (match classify status ~metasenv context ty with
 421        | `Kind ->
 422            TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 423        | `KindOrType (* ??? *)
 424        | `Type ->
 425            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 426        | `PropKind
 427        | `Proposition ->
 428            (* CSC: LAZY ??? *)
 429            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 430        | `Term _ -> assert false (* IMPOSSIBLE *))
 431   | NCic.LetIn (b,ty,t,bo) ->
 432      (match classify status ~metasenv context t with
 433        | `Term `TypeFormerOrTerm (* ???? *)
 434        | `Term `Term ->
 435           LetIn (b,term_of status ~metasenv context t,
 436            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 437        | `Kind
 438        | `Type
 439        | `KindOrType
 440        | `PropKind
 441        | `Proposition
 442        | `Term `PropFormer
 443        | `Term `TypeFormer
 444        | `Term `Proof ->
 445          (* not in programming languages, we expand it *)
 446          term_of status ~metasenv context
 447           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 448   | NCic.Rel n -> Rel n
 449   | NCic.Const ref -> Const ref
 450   | NCic.Appl (he::args) ->
 451      eat_args status metasenv
 452       (term_of status ~metasenv context he) context
 453       (typ_of status ~metasenv context
 454         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 455       args
 456 (*
 457      let he_context = context_of_typformer status ~metasenv context he in
 458      let process_args he =
 459       function
 460          `Empty -> he
 461        | `Inst tl -> Inst (process_args he tl)
 462        | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
 463      in
 464      Appl (typ_of status ~metasenv context he ::
 465       process_args (typ_of status ~metasenv context he)
 466        (skip_term_args status ~metasenv context (List.rev he_context,args))
 467 *)
 468   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 469                                    otherwise NOT A TYPE *)
 470   | NCic.Meta _ -> assert false (* TODO *)
 471   | NCic.Match (ref,_,t,pl) ->
 472      (match classify_not_term status [] (NCic.Const ref) with
 473       | `PropKind
 474       | `KindOrType
 475       | `Kind -> assert false (* IMPOSSIBLE *)
 476       | `Proposition ->
 477           (match pl with
 478               [] -> BottomElim
 479             | [p] ->
 480                 (* UnsafeCoerce not always required *)
 481                 UnsafeCoerce
 482                  (term_of status ~metasenv context p (* Lambdas will be skipped *))
 483             | _ -> assert false)
 484       | `Type ->
 485           Match (ref,term_of status ~metasenv context t,
 486            (* UnsafeCoerce not always required *)
 487            List.map (fun p -> UnsafeCoerce (term_of status ~metasenv context p))            pl))
 488 and eat_args status metasenv acc context tyhe =
 489  function
 490     [] -> acc
 491   | arg::tl ->
 492      let mk_appl f x =
 493       match f with
 494          Appl args -> Appl (args@[x])
 495        | _ -> Appl [f;x]
 496      in
 497      match fomega_whd status tyhe with
 498         Arrow (s,t) ->
 499          let arg =
 500           match s with
 501              Unit -> UnitTerm
 502            | _ -> term_of status ~metasenv context arg in
 503          eat_args status metasenv (mk_appl acc arg) context t tl
 504       | Forall (_,_,t) ->
 505          eat_args status metasenv (Inst acc)
 506           context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
 507       | TSkip t ->
 508          eat_args status metasenv acc context t tl
 509       | Top -> assert false (*TODO: HOW??*)
 510       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 511 ;;
 512
 513 type 'a result =
 514   | Erased
 515   | OutsideTheory
 516   | Failure of string
 517   | Success of 'a
 518 ;;
 519
 520 let object_of_constant status ~metasenv ref bo ty =
 521   match classify status ~metasenv [] ty with
 522     | `Kind ->
 523         let ty = kind_of status ~metasenv [] ty in
 524         let ctx0,res = split_kind_prods [] ty in
 525         let ctx,bo =
 526          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 527         (match classify status ~metasenv ctx bo with
 528           | `Type
 529           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 530               let nicectx =
 531                List.map2
 532                 (fun p1 n ->
 533                   HExtlib.map_option (fun (_,k) ->
 534                    (*CSC: BUG here, clashes*)
 535                    String.uncapitalize (fst n),k) p1)
 536                 ctx0 ctx
 537               in
 538               let bo = typ_of status ~metasenv ctx bo in
 539                status#set_extraction_db
 540                 (ReferenceMap.add ref (nicectx,Some bo)
 541                   status#extraction_db),
 542                Success (ref,TypeDefinition((nicectx,res),bo))
 543           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 544           | `PropKind
 545           | `Proposition -> status, Erased
 546           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 547     | `PropKind
 548     | `Proposition -> status, Erased
 549     | `KindOrType (* ??? *)
 550     | `Type ->
 551        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 552        let ty = typ_of status ~metasenv [] ty in
 553         status,
 554         Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 555     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 556 ;;
 557
 558 let object_of_inductive status ~metasenv uri ind leftno il =
 559  let status,_,rev_tyl =
 560   List.fold_left
 561    (fun (status,i,res) (_,_,arity,cl) ->
 562      match classify_not_term status [] arity with
 563       | `Proposition
 564       | `KindOrType
 565       | `Type -> assert false (* IMPOSSIBLE *)
 566       | `PropKind -> status,i+1,res
 567       | `Kind ->
 568           let arity = kind_of status ~metasenv [] arity in
 569           let ctx,_ = split_kind_prods [] arity in
 570           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 571           let ref =
 572            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 573           let status =
 574            status#set_extraction_db
 575             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 576           let cl =
 577            HExtlib.list_mapi
 578             (fun (_,_,ty) j ->
 579               let ctx,ty =
 580                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 581               let ty = typ_of status ~metasenv ctx ty in
 582                NReference.mk_constructor (j+1) ref,ty
 583             ) cl
 584           in
 585            status,i+1,(ref,left,right,cl)::res
 586    ) (status,0,[]) il
 587  in
 588   match rev_tyl with
 589      [] -> status,Erased
 590    | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
 591 ;;
 592
 593 let object_of status (uri,height,metasenv,subst,obj_kind) =
 594   let obj_kind = apply_subst subst obj_kind in
 595       match obj_kind with
 596         | NCic.Constant (_,_,None,ty,_) ->
 597           let ref = NReference.reference_of_spec uri NReference.Decl in
 598           (match classify status ~metasenv [] ty with
 599             | `Kind ->
 600               let ty = kind_of status ~metasenv [] ty in
 601               let ctx,_ as res = split_kind_prods [] ty in
 602                 status#set_extraction_db
 603                   (ReferenceMap.add ref (ctx,None) status#extraction_db),
 604                     Success (ref, TypeDeclaration res)
 605             | `PropKind
 606             | `Proposition -> status, Erased
 607             | `Type
 608             | `KindOrType (*???*) ->
 609               let ty = typ_of status ~metasenv [] ty in
 610                 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
 611             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 612         | NCic.Constant (_,_,Some bo,ty,_) ->
 613            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 614             object_of_constant status ~metasenv ref bo ty
 615         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 616           let _,status,objs =
 617             List.fold_right
 618             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 619               let ref =
 620                if fix_or_cofix then
 621                 NReference.reference_of_spec
 622                  uri (NReference.Fix (i,recno,height))
 623                else
 624                 NReference.reference_of_spec uri (NReference.CoFix i)
 625               in
 626               let status,obj = object_of_constant ~metasenv status ref bo ty in
 627                 match obj with
 628                   | Success (ref,obj) -> i+1,status, (ref,obj)::res
 629                   | _ -> i+1,status, res) fs (0,status,[])
 630           in
 631             status, Success (dummyref,LetRec objs)
 632         | NCic.Inductive (ind,leftno,il,_) ->
 633            object_of_inductive status ~metasenv uri ind leftno il
 634
 635 (************************ HASKELL *************************)
 636
 637 (* -----------------------------------------------------------------------------
 638  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 639  * -----------------------------------------------------------------------------
 640  *)
 641 let (|>) f g =
 642   fun x -> g (f x)
 643 ;;
 644
 645 let curry f x y =
 646   f (x, y)
 647 ;;
 648
 649 let uncurry f (x, y) =
 650   f x y
 651 ;;
 652
 653 let rec char_list_of_string s =
 654   let l = String.length s in
 655   let rec aux buffer s =
 656     function
 657       | 0 -> buffer
 658       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 659   in
 660     aux [] s l
 661 ;;
 662
 663 let string_of_char_list s =
 664   let rec aux buffer =
 665     function
 666       | []    -> buffer
 667       | x::xs -> aux (String.make 1 x ^ buffer) xs
 668   in
 669     aux "" s
 670 ;;
 671
 672 (* ----------------------------------------------------------------------------
 673  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 674  * and type variable names.
 675  * ----------------------------------------------------------------------------
 676  *)
 677
 678 let remove_underscores_and_mark =
 679   let rec aux char_list_buffer positions_buffer position =
 680     function
 681       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 682       | x::xs ->
 683         if x == '_' then
 684           aux char_list_buffer (position::positions_buffer) position xs
 685         else
 686           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 687   in
 688     aux [] [] 0
 689 ;;
 690
 691 let rec capitalize_marked_positions s =
 692   function
 693     | []    -> s
 694     | x::xs ->
 695       if x < String.length s then
 696         let c = Char.uppercase (String.get s x) in
 697         let _ = String.set s x c in
 698           capitalize_marked_positions s xs
 699       else
 700         capitalize_marked_positions s xs
 701 ;;
 702
 703 let contract_underscores_and_capitalise =
 704   char_list_of_string |>
 705   remove_underscores_and_mark |>
 706   uncurry capitalize_marked_positions
 707 ;;
 708
 709 let idiomatic_haskell_type_name_of_string =
 710   contract_underscores_and_capitalise |>
 711   String.capitalize
 712 ;;
 713
 714 let idiomatic_haskell_term_name_of_string =
 715   contract_underscores_and_capitalise |>
 716   String.uncapitalize
 717 ;;
 718
 719 (*CSC: code to be changed soon when we implement constructors and
 720   we fix the code for term application *)
 721 let classify_reference status ref =
 722   if ReferenceMap.mem ref status#extraction_db then
 723     `TypeName
 724   else
 725    let NReference.Ref (_,ref) = ref in
 726     match ref with
 727        NReference.Con _ -> `Constructor
 728      | NReference.Ind _ -> assert false
 729      | _ -> `FunctionName
 730 ;;
 731
 732 let capitalize classification name =
 733   match classification with
 734     | `Constructor
 735     | `TypeName -> idiomatic_haskell_type_name_of_string name
 736     | `TypeVariable
 737     | `BoundVariable
 738     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 739 ;;
 740
 741 let pp_ref status ref =
 742  capitalize (classify_reference status ref)
 743   (NCicPp.r2s status true ref)
 744
 745 (* cons avoid duplicates *)
 746 let rec (@:::) name l =
 747  if name <> "" (* propositional things *) && name.[0] = '_' then
 748   let name = String.sub name 1 (String.length name - 1) in
 749   let name = if name = "" then "a" else name in
 750    name @::: l
 751  else if List.mem name l then (name ^ "'") @::: l
 752  else name,l
 753 ;;
 754
 755 let (@::) x l = let x,l = x @::: l in x::l;;
 756
 757 let rec pretty_print_type status ctxt =
 758   function
 759     | Var n -> List.nth ctxt (n-1)
 760     | Unit -> "()"
 761     | Top -> assert false (* ??? *)
 762     | TConst ref -> pp_ref status ref
 763     | Arrow (t1,t2) ->
 764         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 765          pretty_print_type status ("_"::ctxt) t2
 766     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 767     | Forall (name, kind, t) ->
 768       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 769       let name = capitalize `TypeVariable name in
 770       let name,ctxt = name@:::ctxt in
 771         if size_of_kind kind > 1 then
 772           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 773         else
 774           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 775    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 776
 777 let rec pretty_print_term status ctxt =
 778   function
 779     | Rel n -> List.nth ctxt (n-1)
 780     | UnitTerm -> "()"
 781     | Const ref -> pp_ref status ref
 782     | Lambda (name,t) ->
 783        let name = capitalize `BoundVariable name in
 784        let name,ctxt = name@:::ctxt in
 785         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 786     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 787     | LetIn (name,s,t) ->
 788        let name = capitalize `BoundVariable name in
 789        let name,ctxt = name@:::ctxt in
 790         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 791          pretty_print_term status (name::ctxt) t
 792     | BottomElim ->
 793        "error \"Unreachable code\""
 794     | UnsafeCoerce t ->
 795        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 796     | Match (r,matched,pl) ->
 797       if pl = [] then
 798        "error \"Case analysis over empty type\""
 799       else
 800       let constructors, leftno =
 801       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
 802       let _,_,_,cl  = List.nth tys n in
 803         cl,leftno
 804       in
 805         let rec eat_branch n ty pat =
 806           match (ty, pat) with
 807           | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat
 808           | NCic.Prod (_, _, t), Lambda (name, t') ->
 809             (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
 810             let cv, rhs = eat_branch 0 t t' in
 811               name :: cv, rhs
 812           | _, _ -> [], pat
 813         in
 814           let j = ref 0 in
 815           let patterns =
 816             try
 817               List.map2
 818                 (fun (_, name, ty) pat -> incr j; name, eat_branch leftno ty pat) constructors pl
 819             with Invalid_argument _ -> assert false
 820           in
 821             "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 822               String.concat "\n"
 823                 (List.map
 824                   (fun (name,(bound_names,rhs)) ->
 825                     let pattern,body =
 826                     (*CSC: BUG avoid name clashes *)
 827                     String.concat " " (String.capitalize name::bound_names),
 828                       pretty_print_term status ((List.rev bound_names)@ctxt) rhs
 829                     in
 830                       "  " ^ pattern ^ " -> " ^ body
 831                   ) patterns)
 832     | Skip t
 833     | TLambda t -> pretty_print_term status (""@::ctxt) t
 834     | Inst t -> pretty_print_term status ctxt t
 835 ;;
 836
 837 (*
 838 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 839
 840 type term_former_def = term_context * term * typ
 841 type term_former_decl = term_context * typ
 842 *)
 843
 844 let rec pp_obj status (ref,obj_kind) =
 845   let pretty_print_context ctx =
 846     String.concat " " (List.rev (snd
 847       (List.fold_right
 848        (fun (x,kind) (l,res) ->
 849          let x,l = x @:::l in
 850          if size_of_kind kind > 1 then
 851           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 852          else
 853           x::l,x::res)
 854        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 855   in
 856  let namectx_of_ctx ctx =
 857   List.fold_right (@::)
 858    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 859  match obj_kind with
 860    TypeDeclaration (ctx,_) ->
 861     (* data?? unsure semantics: inductive type without constructor, but
 862        not matchable apparently *)
 863     if List.length ctx = 0 then
 864       "data " ^ pp_ref status ref
 865     else
 866       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
 867  | TypeDefinition ((ctx, _),ty) ->
 868     let namectx = namectx_of_ctx ctx in
 869     if List.length ctx = 0 then
 870       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
 871     else
 872       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 873  | TermDeclaration (ctx,ty) ->
 874     let name = pp_ref status ref in
 875       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 876       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 877  | TermDefinition ((ctx,ty),bo) ->
 878     let name = pp_ref status ref in
 879     let namectx = namectx_of_ctx ctx in
 880     (*CSC: BUG here *)
 881     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 882     name ^ " = " ^ pretty_print_term status namectx bo
 883  | LetRec l ->
 884     String.concat "\n" (List.map (pp_obj status) l)
 885  | Algebraic il ->
 886     String.concat "\n"
 887      (List.map
 888       (fun ref,left,right,cl ->
 889         "data " ^ pp_ref status ref ^ " " ^
 890         pretty_print_context (right@left) ^ " where\n  " ^
 891         String.concat "\n  " (List.map
 892          (fun ref,tys ->
 893            let namectx = namectx_of_ctx left in
 894             pp_ref status ref ^ " :: " ^
 895              pretty_print_type status namectx tys
 896          ) cl
 897       )) il)
 898  (* inductive and records missing *)
 899
 900 let haskell_of_obj status (uri,_,_,_,_ as obj) =
 901  let status, obj = object_of status obj in
 902   status,
 903    match obj with
 904       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
 905     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
 906     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
 907     | Success o -> pp_obj status o ^ "\n"