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 prerr_endline ("AGGIUNGO" ^ NReference.string_of_reference ref);
 720           let info = ref,(ctx,None) in
 721           let status =
 722            status#set_extraction_db
 723             (register_info status#extraction_db info) in
 724           let cl =
 725            HExtlib.list_mapi
 726             (fun (_,_,ty) j ->
 727               let ctx,ty =
 728                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 729               let ty = typ_of status ~metasenv ctx ty in
 730                NReference.mk_constructor (j+1) ref,ty
 731             ) cl
 732           in
 733            status,i+1,([info],ref,left,right,cl)::res
 734    ) (status,0,[]) il
 735  in
 736   match rev_tyl with
 737      [] -> status,Erased
 738    | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
 739 ;;
 740
 741 let object_of status (uri,height,metasenv,subst,obj_kind) =
 742   let obj_kind = apply_subst subst obj_kind in
 743       match obj_kind with
 744         | NCic.Constant (_,_,None,ty,_) ->
 745           let ref = NReference.reference_of_spec uri NReference.Decl in
 746           (match classify status ~metasenv [] ty with
 747             | `Kind ->
 748               let ty = kind_of status ~metasenv [] ty in
 749               let ctx,_ as res = split_kind_prods [] ty in
 750               let info = ref,(ctx,None) in
 751                 status#set_extraction_db
 752                   (register_info status#extraction_db info),
 753                     Success ([info],ref, TypeDeclaration res)
 754             | `PropKind
 755             | `Proposition -> status, Erased
 756             | `Type
 757             | `KindOrType (*???*) ->
 758               let ty = typ_of status ~metasenv [] ty in
 759                 status, Success ([],ref, TermDeclaration (split_typ_prods [] ty))
 760             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 761         | NCic.Constant (_,_,Some bo,ty,_) ->
 762            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 763             object_of_constant status ~metasenv ref bo ty
 764         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 765           let _,status,objs =
 766             List.fold_right
 767             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 768               let ref =
 769                if fix_or_cofix then
 770                 NReference.reference_of_spec
 771                  uri (NReference.Fix (i,recno,height))
 772                else
 773                 NReference.reference_of_spec uri (NReference.CoFix i)
 774               in
 775               let status,obj = object_of_constant ~metasenv status ref bo ty in
 776                 match obj with
 777                   | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
 778                   | _ -> i+1,status, res) fs (0,status,[])
 779           in
 780             status, Success ([],dummyref,LetRec objs)
 781         | NCic.Inductive (ind,leftno,il,_) ->
 782            object_of_inductive status ~metasenv uri ind leftno il
 783
 784 (************************ HASKELL *************************)
 785
 786 (* -----------------------------------------------------------------------------
 787  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 788  * -----------------------------------------------------------------------------
 789  *)
 790 let (|>) f g =
 791   fun x -> g (f x)
 792 ;;
 793
 794 let curry f x y =
 795   f (x, y)
 796 ;;
 797
 798 let uncurry f (x, y) =
 799   f x y
 800 ;;
 801
 802 let rec char_list_of_string s =
 803   let l = String.length s in
 804   let rec aux buffer s =
 805     function
 806       | 0 -> buffer
 807       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 808   in
 809     aux [] s l
 810 ;;
 811
 812 let string_of_char_list s =
 813   let rec aux buffer =
 814     function
 815       | []    -> buffer
 816       | x::xs -> aux (String.make 1 x ^ buffer) xs
 817   in
 818     aux "" s
 819 ;;
 820
 821 (* ----------------------------------------------------------------------------
 822  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 823  * and type variable names.
 824  * ----------------------------------------------------------------------------
 825  *)
 826
 827 let remove_underscores_and_mark =
 828   let rec aux char_list_buffer positions_buffer position =
 829     function
 830       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 831       | x::xs ->
 832         if x == '_' then
 833           aux char_list_buffer (position::positions_buffer) position xs
 834         else
 835           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 836   in
 837     aux [] [] 0
 838 ;;
 839
 840 let rec capitalize_marked_positions s =
 841   function
 842     | []    -> s
 843     | x::xs ->
 844       if x < String.length s then
 845         let c = Char.uppercase (String.get s x) in
 846         let _ = String.set s x c in
 847           capitalize_marked_positions s xs
 848       else
 849         capitalize_marked_positions s xs
 850 ;;
 851
 852 let contract_underscores_and_capitalise =
 853   char_list_of_string |>
 854   remove_underscores_and_mark |>
 855   uncurry capitalize_marked_positions
 856 ;;
 857
 858 let idiomatic_haskell_type_name_of_string =
 859   contract_underscores_and_capitalise |>
 860   String.capitalize
 861 ;;
 862
 863 let idiomatic_haskell_term_name_of_string =
 864   contract_underscores_and_capitalise |>
 865   String.uncapitalize
 866 ;;
 867
 868 (*CSC: code to be changed soon when we implement constructors and
 869   we fix the code for term application *)
 870 let classify_reference status ref =
 871   if ReferenceMap.mem ref status#extraction_db then
 872     `TypeName
 873   else
 874    let NReference.Ref (_,r) = ref in
 875     match r with
 876        NReference.Con _ -> `Constructor
 877      | NReference.Ind _ -> assert false
 878      | _ -> `FunctionName
 879 ;;
 880
 881 let capitalize classification name =
 882   match classification with
 883     | `Constructor
 884     | `TypeName -> idiomatic_haskell_type_name_of_string name
 885     | `TypeVariable
 886     | `BoundVariable
 887     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 888 ;;
 889
 890 let pp_ref status ref =
 891  capitalize (classify_reference status ref)
 892   (NCicPp.r2s status true ref)
 893
 894 (* cons avoid duplicates *)
 895 let rec (@:::) name l =
 896  if name <> "" (* propositional things *) && name.[0] = '_' then
 897   let name = String.sub name 1 (String.length name - 1) in
 898   let name = if name = "" then "a" else name in
 899    name @::: l
 900  else if List.mem name l then (name ^ "'") @::: l
 901  else name,l
 902 ;;
 903
 904 let (@::) x l = let x,l = x @::: l in x::l;;
 905
 906 let rec pretty_print_type status ctxt =
 907   function
 908     | Var n -> List.nth ctxt (n-1)
 909     | Unit -> "()"
 910     | Top -> "Top"
 911     | TConst ref -> pp_ref status ref
 912     | Arrow (t1,t2) ->
 913         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 914          pretty_print_type status ("_"::ctxt) t2
 915     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 916     | Forall (name, kind, t) ->
 917       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 918       let name = capitalize `TypeVariable name in
 919       let name,ctxt = name@:::ctxt in
 920         if size_of_kind kind > 1 then
 921           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 922         else
 923           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 924    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 925
 926 let pretty_print_term_context status ctx1 ctx2 =
 927  let name_context, rev_res =
 928   List.fold_right
 929     (fun el (ctx1,rev_res) ->
 930       match el with
 931          None -> ""@::ctx1,rev_res
 932        | Some (name,`OfKind _) -> name@::ctx1,rev_res
 933        | Some (name,`OfType typ) ->
 934           let name,ctx1 = name@:::ctx1 in
 935            name::ctx1,
 936             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 937     ) ctx2 (ctx1,[]) in
 938   name_context, String.concat " " (List.rev rev_res)
 939
 940 let rec pretty_print_term status ctxt =
 941   function
 942     | Rel n -> List.nth ctxt (n-1)
 943     | UnitTerm -> "()"
 944     | Const ref -> pp_ref status ref
 945     | Lambda (name,t) ->
 946        let name = capitalize `BoundVariable name in
 947        let name,ctxt = name@:::ctxt in
 948         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
 949     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 950     | LetIn (name,s,t) ->
 951        let name = capitalize `BoundVariable name in
 952        let name,ctxt = name@:::ctxt in
 953         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
 954          pretty_print_term status (name::ctxt) t
 955     | BottomElim ->
 956        "error \"Unreachable code\""
 957     | UnsafeCoerce t ->
 958        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
 959     | Match (r,matched,pl) ->
 960       if pl = [] then
 961        "error \"Case analysis over empty type\""
 962       else
 963        "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 964          String.concat "\n"
 965            (HExtlib.list_mapi
 966              (fun (bound_names,rhs) i ->
 967                let ref = NReference.mk_constructor (i+1) r in
 968                let name = pp_ref status ref in
 969                let ctxt,bound_names =
 970                 pretty_print_term_context status ctxt bound_names in
 971                let body =
 972                 pretty_print_term status ctxt rhs
 973                in
 974                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
 975              ) pl)
 976     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
 977     | TLambda (name,t) ->
 978        let name = capitalize `TypeVariable name in
 979         pretty_print_term status (name@::ctxt) t
 980     | Inst t -> pretty_print_term status ctxt t
 981 ;;
 982
 983 let rec pp_obj status (_,ref,obj_kind) =
 984   let pretty_print_context ctx =
 985     String.concat " " (List.rev (snd
 986       (List.fold_right
 987        (fun (x,kind) (l,res) ->
 988          let x,l = x @:::l in
 989          if size_of_kind kind > 1 then
 990           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 991          else
 992           x::l,x::res)
 993        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 994   in
 995  let namectx_of_ctx ctx =
 996   List.fold_right (@::)
 997    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 998  match obj_kind with
 999    TypeDeclaration (ctx,_) ->
1000     (* data?? unsure semantics: inductive type without constructor, but
1001        not matchable apparently *)
1002     if List.length ctx = 0 then
1003       "data " ^ pp_ref status ref
1004     else
1005       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1006  | TypeDefinition ((ctx, _),ty) ->
1007     let namectx = namectx_of_ctx ctx in
1008     if List.length ctx = 0 then
1009       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1010     else
1011       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1012  | TermDeclaration (ctx,ty) ->
1013     let name = pp_ref status ref in
1014       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1015       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1016  | TermDefinition ((ctx,ty),bo) ->
1017     let name = pp_ref status ref in
1018     let namectx = namectx_of_ctx ctx in
1019     (*CSC: BUG here *)
1020     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1021     name ^ " = " ^ pretty_print_term status namectx bo
1022  | LetRec l ->
1023     String.concat "\n" (List.map (pp_obj status) l)
1024  | Algebraic il ->
1025     String.concat "\n"
1026      (List.map
1027       (fun _,ref,left,right,cl ->
1028         "data " ^ pp_ref status ref ^ " " ^
1029         pretty_print_context (right@left) ^ " where\n  " ^
1030         String.concat "\n  " (List.map
1031          (fun ref,tys ->
1032            let namectx = namectx_of_ctx left in
1033             pp_ref status ref ^ " :: " ^
1034              pretty_print_type status namectx tys
1035          ) cl
1036       )) il)
1037  (* inductive and records missing *)
1038
1039 let rec infos_of (info,_,obj_kind) =
1040  info @
1041   match obj_kind with
1042      LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1043    | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1044    | _ -> []
1045
1046 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1047  let status, obj = object_of status obj in
1048   status,
1049    match obj with
1050       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1051     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1052     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1053     | Success o -> pp_obj status o ^ "\n", infos_of o
1054
1055 let refresh_uri_in_typ ~refresh_uri_in_reference =
1056  let rec refresh_uri_in_typ =
1057   function
1058    | Var _
1059    | Unit
1060    | Top as t -> t
1061    | TConst r -> TConst (refresh_uri_in_reference r)
1062    | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1063    | TSkip t -> TSkip (refresh_uri_in_typ t)
1064    | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1065    | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1066  in
1067   refresh_uri_in_typ
1068
1069 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1070  List.map
1071   (function (ref,(ctx,typ)) ->
1072     let typ =
1073      match typ with
1074         None -> None
1075       | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1076     in
1077      refresh_uri_in_reference ref,(ctx,typ))
1078   infos