matita/components/ng_kernel/nCicExtraction.ml

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