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