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