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 (_, body) -> 1 + size_of_term body
 118     | Appl l -> List.length l
 119     | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
 120     | Match (_, 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 rev_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 List.rev (fst (ReferenceMap.find ref status#extraction_db))
 338       with
 339        Not_found ->
 340         (* This can happen only when we are processing the type of
 341            the constructor of a small singleton type. In this case
 342            we are not interested in all the type, but only in its
 343            backbone. That is why we can safely return the dummy context here *)
 344         let rec dummy = None::dummy in
 345         dummy)
 346   | NCic.Match _ -> assert false (* TODO ???? *)
 347   | NCic.Rel n ->
 348      let typ =
 349       match List.nth context (n-1) with
 350          _,NCic.Decl typ -> typ
 351        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 352      let typ_ctx = snd (HExtlib.split_nth n context) in
 353      let typ = kind_of status ~metasenv typ_ctx typ in
 354       List.rev (fst (split_kind_prods [] typ))
 355   | NCic.Meta _ -> assert false (* TODO *)
 356   | NCic.Const (NReference.Ref (_,NReference.Con _))
 357   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 358   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 359   | NCic.Appl _ | NCic.Prod _ ->
 360      assert false (* IMPOSSIBLE *)
 361
 362 let rec typ_of status ~metasenv context k =
 363  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 364   | NCic.Prod (b,s,t) ->
 365      (* CSC: non-invariant assumed here about "_" *)
 366      (match classify status ~metasenv context s with
 367        | `Kind ->
 368            Forall (b, kind_of status ~metasenv context s,
 369             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 370        | `Type
 371        | `KindOrType -> (* ??? *)
 372            Arrow (typ_of status ~metasenv context s,
 373             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 374        | `PropKind
 375        | `Proposition ->
 376            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 377        | `Term _ -> assert false (* IMPOSSIBLE *))
 378   | NCic.Sort _
 379   | NCic.Implicit _
 380   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 381   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 382   | NCic.Rel n -> Var n
 383   | NCic.Const ref -> TConst ref
 384   | NCic.Appl (he::args) ->
 385      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
 386      TAppl (typ_of status ~metasenv context he ::
 387       List.map
 388        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 389        (skip_args status ~metasenv context (rev_he_context,args)))
 390   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 391                                    otherwise NOT A TYPE *)
 392   | NCic.Meta _
 393   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 394 ;;
 395
 396 let rec fomega_subst k t1 =
 397  function
 398   | Var n ->
 399      if k=n then t1
 400      else if n < k then Var n
 401      else Var (n-1)
 402   | Top -> Top
 403   | TConst ref -> TConst ref
 404   | Unit -> Unit
 405   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 406   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 407   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 408   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 409
 410 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 411
 412 let rec fomega_whd status ty =
 413  match ty with
 414  | TConst r ->
 415     (match fomega_lookup status r with
 416         None -> ty
 417       | Some ty -> fomega_whd status ty)
 418  | TAppl (TConst r::args) ->
 419     (match fomega_lookup status r with
 420         None -> ty
 421       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 422  | _ -> ty
 423
 424 let rec term_of status ~metasenv context =
 425  function
 426   | NCic.Implicit _
 427   | NCic.Sort _
 428   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 429   | NCic.Lambda (b,ty,bo) ->
 430      (* CSC: non-invariant assumed here about "_" *)
 431      (match classify status ~metasenv context ty with
 432        | `Kind ->
 433            TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 434        | `KindOrType (* ??? *)
 435        | `Type ->
 436            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 437        | `PropKind
 438        | `Proposition ->
 439            (* CSC: LAZY ??? *)
 440            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 441        | `Term _ -> assert false (* IMPOSSIBLE *))
 442   | NCic.LetIn (b,ty,t,bo) ->
 443      (match classify status ~metasenv context t with
 444        | `Term `TypeFormerOrTerm (* ???? *)
 445        | `Term `Term ->
 446           LetIn (b,term_of status ~metasenv context t,
 447            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 448        | `Kind
 449        | `Type
 450        | `KindOrType
 451        | `PropKind
 452        | `Proposition
 453        | `Term `PropFormer
 454        | `Term `TypeFormer
 455        | `Term `Proof ->
 456          (* not in programming languages, we expand it *)
 457          term_of status ~metasenv context
 458           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 459   | NCic.Rel n -> Rel n
 460   | NCic.Const ref -> Const ref
 461   | NCic.Appl (he::args) ->
 462      eat_args status metasenv
 463       (term_of status ~metasenv context he) context
 464       (*BUG: recomputing every time the type of the head*)
 465       (typ_of status ~metasenv context
 466         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 467       args
 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      let patterns_of pl =
 473       let constructors, leftno =
 474        let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
 475        let _,_,_,cl  = List.nth tys n in
 476          cl,leftno
 477       in
 478        let rec eat_branch n ty context ctx pat =
 479          match (ty, pat) with
 480          | TSkip t,_
 481          | Forall (_,_,t),_
 482          | Arrow (_, t), _ when n > 0 ->
 483             eat_branch (pred n) t context ctx pat
 484          | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
 485          (*CSC: unify the three cases below? *)
 486          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
 487            let ctx =
 488             (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
 489            let context = (name,NCic.Decl ty)::context in
 490             eat_branch 0 t context ctx t'
 491          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
 492            let ctx =
 493             (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
 494            let context = (name,NCic.Decl ty)::context in
 495             eat_branch 0 t context ctx t'
 496          | TSkip t,NCic.Lambda (name, ty, t') ->
 497             let ctx = None::ctx in
 498             let context = (name,NCic.Decl ty)::context in
 499              eat_branch 0 t context ctx t'
 500          | Top,_ -> assert false (*TODO: HOW??*)
 501          (*BUG here, eta-expand!*)
 502          | _, _ -> context,ctx, pat
 503        in
 504         try
 505          List.map2
 506           (fun (_, name, ty) pat ->
 507             (*BUG: recomputing every time the type of the constructor*)
 508             let ty = typ_of status ~metasenv context ty in
 509             let context,lhs,rhs = eat_branch leftno ty context [] pat in
 510             let rhs =
 511              (* UnsafeCoerce not always required *)
 512              UnsafeCoerce (term_of status ~metasenv context rhs)
 513             in
 514              lhs,rhs
 515           ) constructors pl
 516         with Invalid_argument _ -> assert false
 517      in
 518      (match classify_not_term status [] (NCic.Const ref) with
 519       | `PropKind
 520       | `KindOrType
 521       | `Kind -> assert false (* IMPOSSIBLE *)
 522       | `Proposition ->
 523           (match patterns_of pl with
 524               [] -> BottomElim
 525             | [_lhs,rhs] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*)
 526             | _ -> assert false)
 527       | `Type ->
 528           Match (ref,term_of status ~metasenv context t, patterns_of pl))
 529 and eat_args status metasenv acc context tyhe =
 530  function
 531     [] -> acc
 532   | arg::tl ->
 533      match fomega_whd status tyhe with
 534         Arrow (s,t) ->
 535          let arg =
 536           match s with
 537              Unit -> UnitTerm
 538            | _ -> term_of status ~metasenv context arg in
 539          eat_args status metasenv (mk_appl acc arg) context t tl
 540       | Forall (_,_,t) ->
 541          eat_args status metasenv (Inst acc)
 542           context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
 543       | TSkip t ->
 544          eat_args status metasenv acc context t tl
 545       | Top -> assert false (*TODO: HOW??*)
 546       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 547 ;;
 548
 549 type 'a result =
 550   | Erased
 551   | OutsideTheory
 552   | Failure of string
 553   | Success of 'a
 554 ;;
 555
 556 let object_of_constant status ~metasenv ref bo ty =
 557   match classify status ~metasenv [] ty with
 558     | `Kind ->
 559         let ty = kind_of status ~metasenv [] ty in
 560         let ctx0,res = split_kind_prods [] ty in
 561         let ctx,bo =
 562          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 563         (match classify status ~metasenv ctx bo with
 564           | `Type
 565           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 566               let nicectx =
 567                List.map2
 568                 (fun p1 n ->
 569                   HExtlib.map_option (fun (_,k) ->
 570                    (*CSC: BUG here, clashes*)
 571                    String.uncapitalize (fst n),k) p1)
 572                 ctx0 ctx
 573               in
 574               let bo = typ_of status ~metasenv ctx bo in
 575                status#set_extraction_db
 576                 (ReferenceMap.add ref (nicectx,Some bo)
 577                   status#extraction_db),
 578                Success (ref,TypeDefinition((nicectx,res),bo))
 579           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 580           | `PropKind
 581           | `Proposition -> status, Erased
 582           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 583     | `PropKind
 584     | `Proposition -> status, Erased
 585     | `KindOrType (* ??? *)
 586     | `Type ->
 587        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 588        let ty = typ_of status ~metasenv [] ty in
 589         status,
 590         Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 591     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 592 ;;
 593
 594 let object_of_inductive status ~metasenv uri ind leftno il =
 595  let status,_,rev_tyl =
 596   List.fold_left
 597    (fun (status,i,res) (_,_,arity,cl) ->
 598      match classify_not_term status [] arity with
 599       | `Proposition
 600       | `KindOrType
 601       | `Type -> assert false (* IMPOSSIBLE *)
 602       | `PropKind -> status,i+1,res
 603       | `Kind ->
 604           let arity = kind_of status ~metasenv [] arity in
 605           let ctx,_ = split_kind_prods [] arity in
 606           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 607           let ref =
 608            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 609           let status =
 610            status#set_extraction_db
 611             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 612           let cl =
 613            HExtlib.list_mapi
 614             (fun (_,_,ty) j ->
 615               let ctx,ty =
 616                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 617               let ty = typ_of status ~metasenv ctx ty in
 618                NReference.mk_constructor (j+1) ref,ty
 619             ) cl
 620           in
 621            status,i+1,(ref,left,right,cl)::res
 622    ) (status,0,[]) il
 623  in
 624   match rev_tyl with
 625      [] -> status,Erased
 626    | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
 627 ;;
 628
 629 let object_of status (uri,height,metasenv,subst,obj_kind) =
 630   let obj_kind = apply_subst subst obj_kind in
 631       match obj_kind with
 632         | NCic.Constant (_,_,None,ty,_) ->
 633           let ref = NReference.reference_of_spec uri NReference.Decl in
 634           (match classify status ~metasenv [] ty with
 635             | `Kind ->
 636               let ty = kind_of status ~metasenv [] ty in
 637               let ctx,_ as res = split_kind_prods [] ty in
 638                 status#set_extraction_db
 639                   (ReferenceMap.add ref (ctx,None) status#extraction_db),
 640                     Success (ref, TypeDeclaration res)
 641             | `PropKind
 642             | `Proposition -> status, Erased
 643             | `Type
 644             | `KindOrType (*???*) ->
 645               let ty = typ_of status ~metasenv [] ty in
 646                 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
 647             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 648         | NCic.Constant (_,_,Some bo,ty,_) ->
 649            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 650             object_of_constant status ~metasenv ref bo ty
 651         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 652           let _,status,objs =
 653             List.fold_right
 654             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 655               let ref =
 656                if fix_or_cofix then
 657                 NReference.reference_of_spec
 658                  uri (NReference.Fix (i,recno,height))
 659                else
 660                 NReference.reference_of_spec uri (NReference.CoFix i)
 661               in
 662               let status,obj = object_of_constant ~metasenv status ref bo ty in
 663                 match obj with
 664                   | Success (ref,obj) -> i+1,status, (ref,obj)::res
 665                   | _ -> i+1,status, res) fs (0,status,[])
 666           in
 667             status, Success (dummyref,LetRec objs)
 668         | NCic.Inductive (ind,leftno,il,_) ->
 669            object_of_inductive status ~metasenv uri ind leftno il
 670
 671 (************************ HASKELL *************************)
 672
 673 (* -----------------------------------------------------------------------------
 674  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 675  * -----------------------------------------------------------------------------
 676  *)
 677 let (|>) f g =
 678   fun x -> g (f x)
 679 ;;
 680
 681 let curry f x y =
 682   f (x, y)
 683 ;;
 684
 685 let uncurry f (x, y) =
 686   f x y
 687 ;;
 688
 689 let rec char_list_of_string s =
 690   let l = String.length s in
 691   let rec aux buffer s =
 692     function
 693       | 0 -> buffer
 694       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 695   in
 696     aux [] s l
 697 ;;
 698
 699 let string_of_char_list s =
 700   let rec aux buffer =
 701     function
 702       | []    -> buffer
 703       | x::xs -> aux (String.make 1 x ^ buffer) xs
 704   in
 705     aux "" s
 706 ;;
 707
 708 (* ----------------------------------------------------------------------------
 709  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 710  * and type variable names.
 711  * ----------------------------------------------------------------------------
 712  *)
 713
 714 let remove_underscores_and_mark =
 715   let rec aux char_list_buffer positions_buffer position =
 716     function
 717       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 718       | x::xs ->
 719         if x == '_' then
 720           aux char_list_buffer (position::positions_buffer) position xs
 721         else
 722           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 723   in
 724     aux [] [] 0
 725 ;;
 726
 727 let rec capitalize_marked_positions s =
 728   function
 729     | []    -> s
 730     | x::xs ->
 731       if x < String.length s then
 732         let c = Char.uppercase (String.get s x) in
 733         let _ = String.set s x c in
 734           capitalize_marked_positions s xs
 735       else
 736         capitalize_marked_positions s xs
 737 ;;
 738
 739 let contract_underscores_and_capitalise =
 740   char_list_of_string |>
 741   remove_underscores_and_mark |>
 742   uncurry capitalize_marked_positions
 743 ;;
 744
 745 let idiomatic_haskell_type_name_of_string =
 746   contract_underscores_and_capitalise |>
 747   String.capitalize
 748 ;;
 749
 750 let idiomatic_haskell_term_name_of_string =
 751   contract_underscores_and_capitalise |>
 752   String.uncapitalize
 753 ;;
 754
 755 (*CSC: code to be changed soon when we implement constructors and
 756   we fix the code for term application *)
 757 let classify_reference status ref =
 758   if ReferenceMap.mem ref status#extraction_db then
 759     `TypeName
 760   else
 761    let NReference.Ref (_,ref) = ref in
 762     match ref with
 763        NReference.Con _ -> `Constructor
 764      | NReference.Ind _ -> assert false
 765      | _ -> `FunctionName
 766 ;;
 767
 768 let capitalize classification name =
 769   match classification with
 770     | `Constructor
 771     | `TypeName -> idiomatic_haskell_type_name_of_string name
 772     | `TypeVariable
 773     | `BoundVariable
 774     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 775 ;;
 776
 777 let pp_ref status ref =
 778  capitalize (classify_reference status ref)
 779   (NCicPp.r2s status true ref)
 780
 781 (* cons avoid duplicates *)
 782 let rec (@:::) name l =
 783  if name <> "" (* propositional things *) && name.[0] = '_' then
 784   let name = String.sub name 1 (String.length name - 1) in
 785   let name = if name = "" then "a" else name in
 786    name @::: l
 787  else if List.mem name l then (name ^ "'") @::: l
 788  else name,l
 789 ;;
 790
 791 let (@::) x l = let x,l = x @::: l in x::l;;
 792
 793 let rec pretty_print_type status ctxt =
 794   function
 795     | Var n -> List.nth ctxt (n-1)
 796     | Unit -> "()"
 797     | Top -> assert false (* ??? *)
 798     | TConst ref -> pp_ref status ref
 799     | Arrow (t1,t2) ->
 800         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 801          pretty_print_type status ("_"::ctxt) t2
 802     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 803     | Forall (name, kind, t) ->
 804       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 805       let name = capitalize `TypeVariable name in
 806       let name,ctxt = name@:::ctxt in
 807         if size_of_kind kind > 1 then
 808           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 809         else
 810           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 811    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 812
 813 let pretty_print_term_context status ctx1 ctx2 =
 814  let name_context, rev_res =
 815   List.fold_right
 816     (fun el (ctx1,rev_res) ->
 817       match el with
 818          None -> ""@::ctx1,rev_res
 819        | Some (name,`OfKind _) -> name@::ctx1,rev_res
 820        | Some (name,`OfType typ) ->
 821           let name,ctx1 = name@:::ctx1 in
 822            name::ctx1,
 823             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 824     ) ctx2 (ctx1,[]) in
 825   name_context, String.concat " " (List.rev rev_res)
 826
 827 let rec pretty_print_term status ctxt =
 828   function
 829     | Rel n -> List.nth ctxt (n-1)
 830     | UnitTerm -> "()"
 831     | Const ref -> pp_ref status ref
 832     | Lambda (name,t) ->
 833        let name = capitalize `BoundVariable name in
 834        let name,ctxt = name@:::ctxt in
 835         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 836     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 837     | LetIn (name,s,t) ->
 838        let name = capitalize `BoundVariable name in
 839        let name,ctxt = name@:::ctxt in
 840         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 841          pretty_print_term status (name::ctxt) t
 842     | BottomElim ->
 843        "error \"Unreachable code\""
 844     | UnsafeCoerce t ->
 845        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 846     | Match (r,matched,pl) ->
 847       if pl = [] then
 848        "error \"Case analysis over empty type\""
 849       else
 850        "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 851          String.concat "\n"
 852            (HExtlib.list_mapi
 853              (fun (bound_names,rhs) i ->
 854                let ref = NReference.mk_constructor (i+1) r in
 855                let name = pp_ref status ref in
 856                let ctxt,bound_names =
 857                 pretty_print_term_context status ctxt bound_names in
 858                let body =
 859                 pretty_print_term status ctxt rhs
 860                in
 861                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
 862              ) pl)
 863     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
 864     | TLambda (name,t) ->
 865        let name = capitalize `TypeVariable name in
 866         pretty_print_term status (name@::ctxt) t
 867     | Inst t -> pretty_print_term status ctxt t
 868 ;;
 869
 870 let rec pp_obj status (ref,obj_kind) =
 871   let pretty_print_context ctx =
 872     String.concat " " (List.rev (snd
 873       (List.fold_right
 874        (fun (x,kind) (l,res) ->
 875          let x,l = x @:::l in
 876          if size_of_kind kind > 1 then
 877           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 878          else
 879           x::l,x::res)
 880        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 881   in
 882  let namectx_of_ctx ctx =
 883   List.fold_right (@::)
 884    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 885  match obj_kind with
 886    TypeDeclaration (ctx,_) ->
 887     (* data?? unsure semantics: inductive type without constructor, but
 888        not matchable apparently *)
 889     if List.length ctx = 0 then
 890       "data " ^ pp_ref status ref
 891     else
 892       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
 893  | TypeDefinition ((ctx, _),ty) ->
 894     let namectx = namectx_of_ctx ctx in
 895     if List.length ctx = 0 then
 896       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
 897     else
 898       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 899  | TermDeclaration (ctx,ty) ->
 900     let name = pp_ref status ref in
 901       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 902       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 903  | TermDefinition ((ctx,ty),bo) ->
 904     let name = pp_ref status ref in
 905     let namectx = namectx_of_ctx ctx in
 906     (*CSC: BUG here *)
 907     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 908     name ^ " = " ^ pretty_print_term status namectx bo
 909  | LetRec l ->
 910     String.concat "\n" (List.map (pp_obj status) l)
 911  | Algebraic il ->
 912     String.concat "\n"
 913      (List.map
 914       (fun ref,left,right,cl ->
 915         "data " ^ pp_ref status ref ^ " " ^
 916         pretty_print_context (right@left) ^ " where\n  " ^
 917         String.concat "\n  " (List.map
 918          (fun ref,tys ->
 919            let namectx = namectx_of_ctx left in
 920             pp_ref status ref ^ " :: " ^
 921              pretty_print_type status namectx tys
 922          ) cl
 923       )) il)
 924  (* inductive and records missing *)
 925
 926 let haskell_of_obj status (uri,_,_,_,_ as obj) =
 927  let status, obj = object_of status obj in
 928   status,
 929    match obj with
 930       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
 931     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
 932     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
 933     | Success o -> pp_obj status o ^ "\n"