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 [] ->
 161      assert false (* NOT POSSIBLE *)
 162   | NCic.Match _
 163   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 164      (* be aware: we can be the head of an application *)
 165      assert false (* TODO *)
 166   | NCic.Meta _ -> assert false (* TODO *)
 167   | NCic.Appl (he::_) -> classify_not_term status context he
 168   | NCic.Rel n ->
 169      let rec find_sort typ =
 170       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 171         NCic.Sort NCic.Prop -> `Proposition
 172       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 173       | NCic.Sort (NCic.Type [`Type,_]) ->
 174          (*CSC: we could be more precise distinguishing the user provided
 175                 minimal elements of the hierarchies and classify these
 176                 as `Kind *)
 177          `KindOrType
 178       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 179       | NCic.Prod (_,_,t) ->
 180          (* we skipped arguments of applications, so here we need to skip
 181             products *)
 182          find_sort t
 183       | _ -> assert false (* NOT A SORT *)
 184      in
 185       (match List.nth context (n-1) with
 186           _,NCic.Decl typ -> find_sort typ
 187         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 188   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 189      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 190       (match classify_not_term status [] ty with
 191         | `Proposition
 192         | `Type -> assert false (* IMPOSSIBLE *)
 193         | `Kind
 194         | `KindOrType -> `Type
 195         | `PropKind -> `Proposition)
 196   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 197      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 198      let _,_,arity,_ = List.nth ityl i in
 199       (match classify_not_term status [] arity with
 200         | `Proposition
 201         | `Type
 202         | `KindOrType -> assert false (* IMPOSSIBLE *)
 203         | `Kind -> `Type
 204         | `PropKind -> `Proposition)
 205   | NCic.Const (NReference.Ref (_,NReference.Con _))
 206   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 207      assert false (* IMPOSSIBLE *)
 208 ;;
 209
 210 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 211
 212 let classify status ~metasenv context t =
 213  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 214   | NCic.Sort _ ->
 215      (classify_not_term status context t : not_term :> [> not_term])
 216   | ty ->
 217      let ty = fix_sorts ty in
 218       `Term
 219         (match classify_not_term status context ty with
 220           | `Proposition -> `Proof
 221           | `Type -> `Term
 222           | `KindOrType -> `TypeFormerOrTerm
 223           | `Kind -> `TypeFormer
 224           | `PropKind -> `PropFormer)
 225 ;;
 226
 227
 228 let rec kind_of status ~metasenv context k =
 229  match NCicReduction.whd status ~subst:[] context k with
 230   | NCic.Sort NCic.Type _ -> Type
 231   | NCic.Sort _ -> assert false (* NOT A KIND *)
 232   | NCic.Prod (b,s,t) ->
 233      (match classify status ~metasenv context s with
 234        | `Kind ->
 235            KArrow (kind_of status ~metasenv context s,
 236             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 237        | `Type
 238        | `KindOrType
 239        | `Proposition
 240        | `PropKind ->
 241            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 242        | `Term _ -> assert false (* IMPOSSIBLE *))
 243   | NCic.Implicit _
 244   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 245   | NCic.Lambda _
 246   | NCic.Rel _
 247   | NCic.Const _ -> assert false (* NOT A KIND *)
 248   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 249                                    otherwise NOT A KIND *)
 250   | NCic.Meta _
 251   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 252 ;;
 253
 254 let rec skip_args status ~metasenv context =
 255  function
 256   | _,[] -> []
 257   | [],_ -> assert false (* IMPOSSIBLE *)
 258   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 259   | _::tl1,arg::tl2 ->
 260      match classify status ~metasenv context arg with
 261       | `KindOrType
 262       | `Type
 263       | `Term `TypeFormer ->
 264          Some arg::skip_args status ~metasenv context (tl1,tl2)
 265       | `Kind
 266       | `Proposition
 267       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 268       | `Term _ -> assert false (* IMPOSSIBLE *)
 269 ;;
 270
 271 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 272
 273 type db = (typ_context * typ option) ReferenceMap.t
 274
 275 class type g_status =
 276  object
 277   method extraction_db: db
 278  end
 279
 280 class virtual status =
 281  object
 282   inherit NCic.status
 283   val extraction_db = ReferenceMap.empty
 284   method extraction_db = extraction_db
 285   method set_extraction_db v = {< extraction_db = v >}
 286   method set_extraction_status
 287    : 'status. #g_status as 'status -> 'self
 288    = fun o -> {< extraction_db = o#extraction_db >}
 289  end
 290
 291 let rec split_kind_prods context =
 292  function
 293   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 294   | KSkip ta -> split_kind_prods (None::context) ta
 295   | Type -> context,Type
 296 ;;
 297
 298 let rec split_typ_prods context =
 299  function
 300   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 301   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 302   | TSkip ta -> split_typ_prods (None::context) ta
 303   | _ as t -> context,t
 304 ;;
 305
 306 let rec glue_ctx_typ ctx typ =
 307  match ctx with
 308   | [] -> typ
 309   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 310   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 311   | None::ctx -> glue_ctx_typ ctx (TSkip typ)
 312 ;;
 313
 314 let rec split_typ_lambdas status n ~metasenv context typ =
 315  if n = 0 then context,typ
 316  else
 317   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 318    | NCic.Lambda (name,s,t) ->
 319       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 320    | t ->
 321       (* eta-expansion required *)
 322       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 323       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 324        | NCic.Prod (name,typ,_) ->
 325           split_typ_lambdas status (n-1) ~metasenv
 326            ((name,NCic.Decl typ)::context)
 327            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 328        | _ -> assert false (* IMPOSSIBLE *)
 329 ;;
 330
 331
 332 let rev_context_of_typformer status ~metasenv context =
 333  function
 334     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 335   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 336   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 337   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 338      (try List.rev (fst (ReferenceMap.find ref status#extraction_db))
 339       with
 340        Not_found ->
 341         (* This can happen only when we are processing the type of
 342            the constructor of a small singleton type. In this case
 343            we are not interested in all the type, but only in its
 344            backbone. That is why we can safely return the dummy context here *)
 345         let rec dummy = None::dummy in
 346         dummy)
 347   | NCic.Match _ -> assert false (* TODO ???? *)
 348   | NCic.Rel n ->
 349      let typ =
 350       match List.nth context (n-1) with
 351          _,NCic.Decl typ -> typ
 352        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 353      let typ_ctx = snd (HExtlib.split_nth n context) in
 354      let typ = kind_of status ~metasenv typ_ctx typ in
 355       List.rev (fst (split_kind_prods [] typ))
 356   | NCic.Meta _ -> assert false (* TODO *)
 357   | NCic.Const (NReference.Ref (_,NReference.Con _))
 358   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 359   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 360   | NCic.Appl _ | NCic.Prod _ ->
 361      assert false (* IMPOSSIBLE *)
 362
 363 let rec typ_of status ~metasenv context k =
 364  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 365   | NCic.Prod (b,s,t) ->
 366      (* CSC: non-invariant assumed here about "_" *)
 367      (match classify status ~metasenv context s with
 368        | `Kind ->
 369            Forall (b, kind_of status ~metasenv context s,
 370             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 371        | `Type
 372        | `KindOrType -> (* ??? *)
 373            Arrow (typ_of status ~metasenv context s,
 374             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 375        | `PropKind
 376        | `Proposition ->
 377            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 378        | `Term _ -> assert false (* IMPOSSIBLE *))
 379   | NCic.Sort _
 380   | NCic.Implicit _
 381   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 382   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 383   | NCic.Rel n -> Var n
 384   | NCic.Const ref -> TConst ref
 385   | NCic.Appl (he::args) ->
 386      let rev_he_context= rev_context_of_typformer status ~metasenv context he in
 387      TAppl (typ_of status ~metasenv context he ::
 388       List.map
 389        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 390        (skip_args status ~metasenv context (rev_he_context,args)))
 391   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 392                                    otherwise NOT A TYPE *)
 393   | NCic.Meta _
 394   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 395 ;;
 396
 397 let rec fomega_lift_type_from n k =
 398  function
 399   | Var m as t -> if m < k then t else Var (m + n)
 400   | Top -> Top
 401   | TConst _ as t -> t
 402   | Unit -> Unit
 403   | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
 404   | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
 405   | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
 406   | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
 407
 408 let fomega_lift_type n t =
 409  if n = 0 then t else fomega_lift_type_from n 0 t
 410
 411 let fomega_lift_term n t =
 412  let rec fomega_lift_term n k =
 413   function
 414    | Rel m as t -> if m < k then t else Rel (m + n)
 415    | BottomElim
 416    | UnitTerm
 417    | Const _ as t -> t
 418    | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
 419    | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
 420    | Appl args -> Appl (List.map (fomega_lift_term n k) args)
 421    | LetIn (name,m,bo) ->
 422       LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
 423    | Match (ref,t,pl) ->
 424       let lift_p (ctx,t) =
 425        let lift_context ctx =
 426         let len = List.length ctx in
 427          HExtlib.list_mapi
 428           (fun el i ->
 429             let j = len - i - 1 in
 430             match el with
 431                None
 432              | Some (_,`OfKind  _) as el -> el
 433              | Some (name,`OfType t) ->
 434                 Some (name,`OfType (fomega_lift_type_from n (k+j) t))
 435           ) ctx
 436        in
 437         lift_context ctx, fomega_lift_term n (k + List.length ctx) t
 438       in
 439       Match (ref,fomega_lift_term n k t,List.map lift_p pl)
 440    | Inst t -> Inst (fomega_lift_term n k t)
 441    | Skip t -> Skip (fomega_lift_term n (k+1) t)
 442    | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
 443  in
 444   if n = 0 then t else fomega_lift_term n 0 t
 445 ;;
 446
 447 let rec fomega_subst k t1 =
 448  function
 449   | Var n ->
 450      if k=n then fomega_lift_type k t1
 451      else if n < k then Var n
 452      else Var (n-1)
 453   | Top -> Top
 454   | TConst ref -> TConst ref
 455   | Unit -> Unit
 456   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 457   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 458   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 459   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 460
 461 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 462
 463 let rec fomega_whd status ty =
 464  match ty with
 465  | TConst r ->
 466     (match fomega_lookup status r with
 467         None -> ty
 468       | Some ty -> fomega_whd status ty)
 469  | TAppl (TConst r::args) ->
 470     (match fomega_lookup status r with
 471         None -> ty
 472       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 473  | _ -> ty
 474
 475 let rec term_of status ~metasenv context =
 476  function
 477   | NCic.Implicit _
 478   | NCic.Sort _
 479   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 480   | NCic.Lambda (b,ty,bo) ->
 481      (* CSC: non-invariant assumed here about "_" *)
 482      (match classify status ~metasenv context ty with
 483        | `Kind ->
 484            TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 485        | `KindOrType (* ??? *)
 486        | `Type ->
 487            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 488        | `PropKind
 489        | `Proposition ->
 490            (* CSC: LAZY ??? *)
 491            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 492        | `Term _ -> assert false (* IMPOSSIBLE *))
 493   | NCic.LetIn (b,ty,t,bo) ->
 494      (match classify status ~metasenv context t with
 495        | `Term `TypeFormerOrTerm (* ???? *)
 496        | `Term `Term ->
 497           LetIn (b,term_of status ~metasenv context t,
 498            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 499        | `Kind
 500        | `Type
 501        | `KindOrType
 502        | `PropKind
 503        | `Proposition
 504        | `Term `PropFormer
 505        | `Term `TypeFormer
 506        | `Term `Proof ->
 507          (* not in programming languages, we expand it *)
 508          term_of status ~metasenv context
 509           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 510   | NCic.Rel n -> Rel n
 511   | NCic.Const ref -> Const ref
 512   | NCic.Appl (he::args) ->
 513      eat_args status metasenv
 514       (term_of status ~metasenv context he) context
 515       (*BUG: recomputing every time the type of the head*)
 516       (typ_of status ~metasenv context
 517         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 518       args
 519   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 520                                    otherwise NOT A TYPE *)
 521   | NCic.Meta _ -> assert false (* TODO *)
 522   | NCic.Match (ref,_,t,pl) ->
 523      let patterns_of pl =
 524       let constructors, leftno =
 525        let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
 526        let _,_,_,cl  = List.nth tys n in
 527          cl,leftno
 528       in
 529        let rec eat_branch n ty context ctx pat =
 530          match (ty, pat) with
 531          | TSkip t,_
 532          | Forall (_,_,t),_
 533          | Arrow (_, t), _ when n > 0 ->
 534             eat_branch (pred n) t context ctx pat
 535          | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
 536          (*CSC: unify the three cases below? *)
 537          | Arrow (_, t), NCic.Lambda (name, ty, t') ->
 538            let ctx =
 539             (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
 540            let context = (name,NCic.Decl ty)::context in
 541             eat_branch 0 t context ctx t'
 542          | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
 543            let ctx =
 544             (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
 545            let context = (name,NCic.Decl ty)::context in
 546             eat_branch 0 t context ctx t'
 547          | TSkip t,NCic.Lambda (name, ty, t') ->
 548             let ctx = None::ctx in
 549             let context = (name,NCic.Decl ty)::context in
 550              eat_branch 0 t context ctx t'
 551          | Top,_ -> assert false (*TODO: HOW??*)
 552          | TSkip _, _
 553          | Forall _,_
 554          | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
 555          | _, _ -> context,ctx, pat
 556        in
 557         try
 558          List.map2
 559           (fun (_, name, ty) pat ->
 560             (*BUG: recomputing every time the type of the constructor*)
 561             let ty = typ_of status ~metasenv context ty in
 562             let context,lhs,rhs = eat_branch leftno ty context [] pat in
 563             let rhs =
 564              (* UnsafeCoerce not always required *)
 565              UnsafeCoerce (term_of status ~metasenv context rhs)
 566             in
 567              lhs,rhs
 568           ) constructors pl
 569         with Invalid_argument _ -> assert false
 570      in
 571      (match classify_not_term status [] (NCic.Const ref) with
 572       | `PropKind
 573       | `KindOrType
 574       | `Kind -> assert false (* IMPOSSIBLE *)
 575       | `Proposition ->
 576           (match patterns_of pl with
 577               [] -> BottomElim
 578             | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
 579             | _ -> assert false)
 580       | `Type ->
 581           Match (ref,term_of status ~metasenv context t, patterns_of pl))
 582 and eat_args status metasenv acc context tyhe =
 583  function
 584     [] -> acc
 585   | arg::tl ->
 586      match fomega_whd status tyhe with
 587         Arrow (s,t) ->
 588          let arg =
 589           match s with
 590              Unit -> UnitTerm
 591            | _ -> term_of status ~metasenv context arg in
 592          eat_args status metasenv (mk_appl acc arg) context t tl
 593       | Forall (_,_,t) ->
 594          (match classify status ~metasenv context arg with
 595            | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
 596            | `Proposition
 597            | `Term `TypeFormer
 598            | `Kind ->
 599                eat_args status metasenv (UnsafeCoerce (Inst acc))
 600                 context (fomega_subst 1 Unit t) tl
 601            | `Term _ -> assert false (*TODO: ????*)
 602            | `KindOrType
 603            | `Type ->
 604                eat_args status metasenv (Inst acc)
 605                 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
 606                  tl)
 607       | TSkip t ->
 608          eat_args status metasenv acc context t tl
 609       | Top -> assert false (*TODO: HOW??*)
 610       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 611 ;;
 612
 613 type 'a result =
 614   | Erased
 615   | OutsideTheory
 616   | Failure of string
 617   | Success of 'a
 618 ;;
 619
 620 let object_of_constant status ~metasenv ref bo ty =
 621   match classify status ~metasenv [] ty with
 622     | `Kind ->
 623         let ty = kind_of status ~metasenv [] ty in
 624         let ctx0,res = split_kind_prods [] ty in
 625         let ctx,bo =
 626          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 627         (match classify status ~metasenv ctx bo with
 628           | `Type
 629           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 630               let nicectx =
 631                List.map2
 632                 (fun p1 n ->
 633                   HExtlib.map_option (fun (_,k) ->
 634                    (*CSC: BUG here, clashes*)
 635                    String.uncapitalize (fst n),k) p1)
 636                 ctx0 ctx
 637               in
 638               let bo = typ_of status ~metasenv ctx bo in
 639                status#set_extraction_db
 640                 (ReferenceMap.add ref (nicectx,Some bo)
 641                   status#extraction_db),
 642                Success (ref,TypeDefinition((nicectx,res),bo))
 643           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 644           | `PropKind
 645           | `Proposition -> status, Erased
 646           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 647     | `PropKind
 648     | `Proposition -> status, Erased
 649     | `KindOrType (* ??? *)
 650     | `Type ->
 651        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 652        let ty = typ_of status ~metasenv [] ty in
 653         status,
 654         Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 655     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 656 ;;
 657
 658 let object_of_inductive status ~metasenv uri ind leftno il =
 659  let status,_,rev_tyl =
 660   List.fold_left
 661    (fun (status,i,res) (_,_,arity,cl) ->
 662      match classify_not_term status [] arity with
 663       | `Proposition
 664       | `KindOrType
 665       | `Type -> assert false (* IMPOSSIBLE *)
 666       | `PropKind -> status,i+1,res
 667       | `Kind ->
 668           let arity = kind_of status ~metasenv [] arity in
 669           let ctx,_ = split_kind_prods [] arity in
 670           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 671           let ref =
 672            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 673           let status =
 674            status#set_extraction_db
 675             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 676           let cl =
 677            HExtlib.list_mapi
 678             (fun (_,_,ty) j ->
 679               let ctx,ty =
 680                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 681               let ty = typ_of status ~metasenv ctx ty in
 682                NReference.mk_constructor (j+1) ref,ty
 683             ) cl
 684           in
 685            status,i+1,(ref,left,right,cl)::res
 686    ) (status,0,[]) il
 687  in
 688   match rev_tyl with
 689      [] -> status,Erased
 690    | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
 691 ;;
 692
 693 let object_of status (uri,height,metasenv,subst,obj_kind) =
 694   let obj_kind = apply_subst subst obj_kind in
 695       match obj_kind with
 696         | NCic.Constant (_,_,None,ty,_) ->
 697           let ref = NReference.reference_of_spec uri NReference.Decl in
 698           (match classify status ~metasenv [] ty with
 699             | `Kind ->
 700               let ty = kind_of status ~metasenv [] ty in
 701               let ctx,_ as res = split_kind_prods [] ty in
 702                 status#set_extraction_db
 703                   (ReferenceMap.add ref (ctx,None) status#extraction_db),
 704                     Success (ref, TypeDeclaration res)
 705             | `PropKind
 706             | `Proposition -> status, Erased
 707             | `Type
 708             | `KindOrType (*???*) ->
 709               let ty = typ_of status ~metasenv [] ty in
 710                 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
 711             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 712         | NCic.Constant (_,_,Some bo,ty,_) ->
 713            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 714             object_of_constant status ~metasenv ref bo ty
 715         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 716           let _,status,objs =
 717             List.fold_right
 718             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 719               let ref =
 720                if fix_or_cofix then
 721                 NReference.reference_of_spec
 722                  uri (NReference.Fix (i,recno,height))
 723                else
 724                 NReference.reference_of_spec uri (NReference.CoFix i)
 725               in
 726               let status,obj = object_of_constant ~metasenv status ref bo ty in
 727                 match obj with
 728                   | Success (ref,obj) -> i+1,status, (ref,obj)::res
 729                   | _ -> i+1,status, res) fs (0,status,[])
 730           in
 731             status, Success (dummyref,LetRec objs)
 732         | NCic.Inductive (ind,leftno,il,_) ->
 733            object_of_inductive status ~metasenv uri ind leftno il
 734
 735 (************************ HASKELL *************************)
 736
 737 (* -----------------------------------------------------------------------------
 738  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 739  * -----------------------------------------------------------------------------
 740  *)
 741 let (|>) f g =
 742   fun x -> g (f x)
 743 ;;
 744
 745 let curry f x y =
 746   f (x, y)
 747 ;;
 748
 749 let uncurry f (x, y) =
 750   f x y
 751 ;;
 752
 753 let rec char_list_of_string s =
 754   let l = String.length s in
 755   let rec aux buffer s =
 756     function
 757       | 0 -> buffer
 758       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 759   in
 760     aux [] s l
 761 ;;
 762
 763 let string_of_char_list s =
 764   let rec aux buffer =
 765     function
 766       | []    -> buffer
 767       | x::xs -> aux (String.make 1 x ^ buffer) xs
 768   in
 769     aux "" s
 770 ;;
 771
 772 (* ----------------------------------------------------------------------------
 773  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 774  * and type variable names.
 775  * ----------------------------------------------------------------------------
 776  *)
 777
 778 let remove_underscores_and_mark =
 779   let rec aux char_list_buffer positions_buffer position =
 780     function
 781       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 782       | x::xs ->
 783         if x == '_' then
 784           aux char_list_buffer (position::positions_buffer) position xs
 785         else
 786           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 787   in
 788     aux [] [] 0
 789 ;;
 790
 791 let rec capitalize_marked_positions s =
 792   function
 793     | []    -> s
 794     | x::xs ->
 795       if x < String.length s then
 796         let c = Char.uppercase (String.get s x) in
 797         let _ = String.set s x c in
 798           capitalize_marked_positions s xs
 799       else
 800         capitalize_marked_positions s xs
 801 ;;
 802
 803 let contract_underscores_and_capitalise =
 804   char_list_of_string |>
 805   remove_underscores_and_mark |>
 806   uncurry capitalize_marked_positions
 807 ;;
 808
 809 let idiomatic_haskell_type_name_of_string =
 810   contract_underscores_and_capitalise |>
 811   String.capitalize
 812 ;;
 813
 814 let idiomatic_haskell_term_name_of_string =
 815   contract_underscores_and_capitalise |>
 816   String.uncapitalize
 817 ;;
 818
 819 (*CSC: code to be changed soon when we implement constructors and
 820   we fix the code for term application *)
 821 let classify_reference status ref =
 822   if ReferenceMap.mem ref status#extraction_db then
 823     `TypeName
 824   else
 825    let NReference.Ref (_,ref) = ref in
 826     match ref with
 827        NReference.Con _ -> `Constructor
 828      | NReference.Ind _ -> assert false
 829      | _ -> `FunctionName
 830 ;;
 831
 832 let capitalize classification name =
 833   match classification with
 834     | `Constructor
 835     | `TypeName -> idiomatic_haskell_type_name_of_string name
 836     | `TypeVariable
 837     | `BoundVariable
 838     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 839 ;;
 840
 841 let pp_ref status ref =
 842  capitalize (classify_reference status ref)
 843   (NCicPp.r2s status true ref)
 844
 845 (* cons avoid duplicates *)
 846 let rec (@:::) name l =
 847  if name <> "" (* propositional things *) && name.[0] = '_' then
 848   let name = String.sub name 1 (String.length name - 1) in
 849   let name = if name = "" then "a" else name in
 850    name @::: l
 851  else if List.mem name l then (name ^ "'") @::: l
 852  else name,l
 853 ;;
 854
 855 let (@::) x l = let x,l = x @::: l in x::l;;
 856
 857 let rec pretty_print_type status ctxt =
 858   function
 859     | Var n -> List.nth ctxt (n-1)
 860     | Unit -> "()"
 861     | Top -> assert false (* ??? *)
 862     | TConst ref -> pp_ref status ref
 863     | Arrow (t1,t2) ->
 864         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 865          pretty_print_type status ("_"::ctxt) t2
 866     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 867     | Forall (name, kind, t) ->
 868       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 869       let name = capitalize `TypeVariable name in
 870       let name,ctxt = name@:::ctxt in
 871         if size_of_kind kind > 1 then
 872           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 873         else
 874           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 875    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 876
 877 let pretty_print_term_context status ctx1 ctx2 =
 878  let name_context, rev_res =
 879   List.fold_right
 880     (fun el (ctx1,rev_res) ->
 881       match el with
 882          None -> ""@::ctx1,rev_res
 883        | Some (name,`OfKind _) -> name@::ctx1,rev_res
 884        | Some (name,`OfType typ) ->
 885           let name,ctx1 = name@:::ctx1 in
 886            name::ctx1,
 887             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 888     ) ctx2 (ctx1,[]) in
 889   name_context, String.concat " " (List.rev rev_res)
 890
 891 let rec pretty_print_term status ctxt =
 892   function
 893     | Rel n -> List.nth ctxt (n-1)
 894     | UnitTerm -> "()"
 895     | Const ref -> pp_ref status ref
 896     | Lambda (name,t) ->
 897        let name = capitalize `BoundVariable name in
 898        let name,ctxt = name@:::ctxt in
 899         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 900     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 901     | LetIn (name,s,t) ->
 902        let name = capitalize `BoundVariable name in
 903        let name,ctxt = name@:::ctxt in
 904         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 905          pretty_print_term status (name::ctxt) t
 906     | BottomElim ->
 907        "error \"Unreachable code\""
 908     | UnsafeCoerce t ->
 909        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 910     | Match (r,matched,pl) ->
 911       if pl = [] then
 912        "error \"Case analysis over empty type\""
 913       else
 914        "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 915          String.concat "\n"
 916            (HExtlib.list_mapi
 917              (fun (bound_names,rhs) i ->
 918                let ref = NReference.mk_constructor (i+1) r in
 919                let name = pp_ref status ref in
 920                let ctxt,bound_names =
 921                 pretty_print_term_context status ctxt bound_names in
 922                let body =
 923                 pretty_print_term status ctxt rhs
 924                in
 925                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
 926              ) pl)
 927     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
 928     | TLambda (name,t) ->
 929        let name = capitalize `TypeVariable name in
 930         pretty_print_term status (name@::ctxt) t
 931     | Inst t -> pretty_print_term status ctxt t
 932 ;;
 933
 934 let rec pp_obj status (ref,obj_kind) =
 935   let pretty_print_context ctx =
 936     String.concat " " (List.rev (snd
 937       (List.fold_right
 938        (fun (x,kind) (l,res) ->
 939          let x,l = x @:::l in
 940          if size_of_kind kind > 1 then
 941           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 942          else
 943           x::l,x::res)
 944        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 945   in
 946  let namectx_of_ctx ctx =
 947   List.fold_right (@::)
 948    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 949  match obj_kind with
 950    TypeDeclaration (ctx,_) ->
 951     (* data?? unsure semantics: inductive type without constructor, but
 952        not matchable apparently *)
 953     if List.length ctx = 0 then
 954       "data " ^ pp_ref status ref
 955     else
 956       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
 957  | TypeDefinition ((ctx, _),ty) ->
 958     let namectx = namectx_of_ctx ctx in
 959     if List.length ctx = 0 then
 960       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
 961     else
 962       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 963  | TermDeclaration (ctx,ty) ->
 964     let name = pp_ref status ref in
 965       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 966       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 967  | TermDefinition ((ctx,ty),bo) ->
 968     let name = pp_ref status ref in
 969     let namectx = namectx_of_ctx ctx in
 970     (*CSC: BUG here *)
 971     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 972     name ^ " = " ^ pretty_print_term status namectx bo
 973  | LetRec l ->
 974     String.concat "\n" (List.map (pp_obj status) l)
 975  | Algebraic il ->
 976     String.concat "\n"
 977      (List.map
 978       (fun ref,left,right,cl ->
 979         "data " ^ pp_ref status ref ^ " " ^
 980         pretty_print_context (right@left) ^ " where\n  " ^
 981         String.concat "\n  " (List.map
 982          (fun ref,tys ->
 983            let namectx = namectx_of_ctx left in
 984             pp_ref status ref ^ " :: " ^
 985              pretty_print_type status namectx tys
 986          ) cl
 987       )) il)
 988  (* inductive and records missing *)
 989
 990 let haskell_of_obj status (uri,_,_,_,_ as obj) =
 991  let status, obj = object_of status obj in
 992   status,
 993    match obj with
 994       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
 995     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
 996     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
 997     | Success o -> pp_obj status o ^ "\n"