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 ?(prec=1) size_of pp o =
  47   if size_of o > prec 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 _ -> 0
  73     | Unit -> 0
  74     | Top -> 0
  75     | TConst _ -> 0
  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  (*CSC: Patch while we wait for separate compilation *)
 680  let candidate =
 681   let name = NCicPp.r2s status true ref in
 682   let NReference.Ref (uri,_) = ref in
 683   let path = NUri.baseuri_of_uri uri in
 684   let path = String.sub path 5 (String.length path - 5) in
 685   let path = Str.global_replace (Str.regexp "/") "_" path in
 686    path ^ "_" ^ name
 687  in
 688  let rec freshen candidate =
 689   if GlobalNames.mem candidate (snd status#extraction_db) then
 690    freshen (candidate ^ "'")
 691   else
 692    candidate
 693  in
 694   freshen candidate
 695
 696 let register_info (db,names) (ref,(name,_ as info_el)) =
 697  ReferenceMap.add ref info_el db,GlobalNames.add name names
 698
 699 let register_name_and_info status (ref,info_el) =
 700  let name = fresh_name_of_ref status ref in
 701  let info = ref,(name,info_el) in
 702  let infos,names = status#extraction_db in
 703   status#set_extraction_db (register_info (infos,names) info), info
 704
 705 let register_infos = List.fold_left register_info
 706
 707 let object_of_constant status ~metasenv ref bo ty =
 708   match classify status ~metasenv [] ty with
 709     | `Kind ->
 710         let ty = kind_of status ~metasenv [] ty in
 711         let ctx0,res = split_kind_prods [] ty in
 712         let ctx,bo =
 713          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 714         (match classify status ~metasenv ctx bo with
 715           | `Type
 716           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 717               let nicectx =
 718                List.map2
 719                 (fun p1 n ->
 720                   HExtlib.map_option (fun (_,k) ->
 721                    (*CSC: BUG here, clashes*)
 722                    String.uncapitalize (fst n),k) p1)
 723                 ctx0 ctx
 724               in
 725               let bo = typ_of status ~metasenv ctx bo in
 726               let info = ref,`Type (nicectx,Some bo) in
 727               let status,info = register_name_and_info status info in
 728                status,Success ([info],ref,TypeDefinition((nicectx,res),bo))
 729           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 730           | `PropKind
 731           | `Proposition -> status, Erased
 732           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 733     | `PropKind
 734     | `Proposition -> status, Erased
 735     | `KindOrType (* ??? *)
 736     | `Type ->
 737        let ty = typ_of status ~metasenv [] ty in
 738        let info = ref,`Function in
 739        let status,info = register_name_and_info status info in
 740         status,
 741          Success ([info],ref, TermDefinition (split_typ_prods [] ty,
 742          term_of status ~metasenv [] bo))
 743     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 744 ;;
 745
 746 let object_of_inductive status ~metasenv uri ind leftno il =
 747  let status,_,rev_tyl =
 748   List.fold_left
 749    (fun (status,i,res) (_,_,arity,cl) ->
 750      match classify_not_term status [] arity with
 751       | `Proposition
 752       | `KindOrType
 753       | `Type -> assert false (* IMPOSSIBLE *)
 754       | `PropKind -> status,i+1,res
 755       | `Kind ->
 756           let arity = kind_of status ~metasenv [] arity in
 757           let ctx,_ = split_kind_prods [] arity in
 758           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 759           let ref =
 760            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 761           let info = ref,`Type (ctx,None) in
 762           let status,info = register_name_and_info status info in
 763           let _,status,cl_rev,infos =
 764            List.fold_left
 765             (fun (j,status,res,infos) (_,_,ty) ->
 766               let ctx,ty =
 767                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 768               let ty = typ_of status ~metasenv ctx ty in
 769               let ref = NReference.mk_constructor j ref in
 770               let info = ref,`Constructor in
 771               let status,info = register_name_and_info status info in
 772                j+1,status,((ref,ty)::res),info::infos
 773             ) (1,status,[],[]) cl
 774           in
 775            status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
 776    ) (status,0,[]) il
 777  in
 778   match rev_tyl with
 779      [] -> status,Erased
 780    | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
 781 ;;
 782
 783 let object_of status (uri,height,metasenv,subst,obj_kind) =
 784   let obj_kind = apply_subst subst obj_kind in
 785       match obj_kind with
 786         | NCic.Constant (_,_,None,ty,_) ->
 787           let ref = NReference.reference_of_spec uri NReference.Decl in
 788           (match classify status ~metasenv [] ty with
 789             | `Kind ->
 790               let ty = kind_of status ~metasenv [] ty in
 791               let ctx,_ as res = split_kind_prods [] ty in
 792               let info = ref,`Type (ctx,None) in
 793               let status,info = register_name_and_info status info in
 794                status, Success ([info],ref, TypeDeclaration res)
 795             | `PropKind
 796             | `Proposition -> status, Erased
 797             | `Type
 798             | `KindOrType (*???*) ->
 799               let ty = typ_of status ~metasenv [] ty in
 800               let info = ref,`Function in
 801               let status,info = register_name_and_info status info in
 802                status,Success ([info],ref,
 803                 TermDeclaration (split_typ_prods [] ty))
 804             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 805         | NCic.Constant (_,_,Some bo,ty,_) ->
 806            let ref = NReference.reference_of_spec uri (NReference.Def height) in
 807             object_of_constant status ~metasenv ref bo ty
 808         | NCic.Fixpoint (fix_or_cofix,fs,_) ->
 809           let _,status,objs =
 810             List.fold_right
 811             (fun (_,_name,recno,ty,bo) (i,status,res) ->
 812               let ref =
 813                if fix_or_cofix then
 814                 NReference.reference_of_spec
 815                  uri (NReference.Fix (i,recno,height))
 816                else
 817                 NReference.reference_of_spec uri (NReference.CoFix i)
 818               in
 819               let status,obj = object_of_constant ~metasenv status ref bo ty in
 820                 match obj with
 821                   | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
 822                   | _ -> i+1,status, res) fs (0,status,[])
 823           in
 824             status, Success ([],dummyref,LetRec objs)
 825         | NCic.Inductive (ind,leftno,il,_) ->
 826            object_of_inductive status ~metasenv uri ind leftno il
 827
 828 (************************ HASKELL *************************)
 829
 830 (* -----------------------------------------------------------------------------
 831  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 832  * -----------------------------------------------------------------------------
 833  *)
 834 let (|>) f g =
 835   fun x -> g (f x)
 836 ;;
 837
 838 let curry f x y =
 839   f (x, y)
 840 ;;
 841
 842 let uncurry f (x, y) =
 843   f x y
 844 ;;
 845
 846 let rec char_list_of_string s =
 847   let l = String.length s in
 848   let rec aux buffer s =
 849     function
 850       | 0 -> buffer
 851       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 852   in
 853     aux [] s l
 854 ;;
 855
 856 let string_of_char_list s =
 857   let rec aux buffer =
 858     function
 859       | []    -> buffer
 860       | x::xs -> aux (String.make 1 x ^ buffer) xs
 861   in
 862     aux "" s
 863 ;;
 864
 865 (* ----------------------------------------------------------------------------
 866  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 867  * and type variable names.
 868  * ----------------------------------------------------------------------------
 869  *)
 870
 871 let remove_underscores_and_mark l =
 872   let rec aux char_list_buffer positions_buffer position =
 873     function
 874       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 875       | x::xs ->
 876         if x == '_' then
 877           aux char_list_buffer (position::positions_buffer) position xs
 878         else
 879           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 880   in
 881    if l = ['_'] then "_",[] else aux [] [] 0 l
 882 ;;
 883
 884 let rec capitalize_marked_positions s =
 885   function
 886     | []    -> s
 887     | x::xs ->
 888       if x < String.length s then
 889         let c = Char.uppercase (String.get s x) in
 890         let _ = String.set s x c in
 891           capitalize_marked_positions s xs
 892       else
 893         capitalize_marked_positions s xs
 894 ;;
 895
 896 let contract_underscores_and_capitalise =
 897   char_list_of_string |>
 898   remove_underscores_and_mark |>
 899   uncurry capitalize_marked_positions
 900 ;;
 901
 902 let idiomatic_haskell_type_name_of_string =
 903   contract_underscores_and_capitalise |>
 904   String.capitalize
 905 ;;
 906
 907 let idiomatic_haskell_term_name_of_string =
 908   contract_underscores_and_capitalise |>
 909   String.uncapitalize
 910 ;;
 911
 912 let classify_reference status ref =
 913  try
 914   match snd (ReferenceMap.find ref (fst status#extraction_db)) with
 915      `Type _ -> `TypeName
 916    | `Constructor -> `Constructor
 917    | `Function -> `FunctionName
 918  with
 919   Not_found ->
 920 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName
 921 ;;
 922
 923 let capitalize classification name =
 924   match classification with
 925     | `Constructor
 926     | `TypeName -> idiomatic_haskell_type_name_of_string name
 927     | `TypeVariable
 928     | `BoundVariable
 929     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 930 ;;
 931
 932 let pp_ref status ref =
 933  capitalize (classify_reference status ref)
 934   (try fst (ReferenceMap.find ref (fst status#extraction_db))
 935    with Not_found ->
 936 prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref);
 937 (*assert false*)
 938  NCicPp.r2s status true ref (* BUG: this should never happen *)
 939 )
 940
 941 (* cons avoid duplicates *)
 942 let rec (@:::) name l =
 943  if name <> "" (* propositional things *) && name.[0] = '_' then
 944   let name = String.sub name 1 (String.length name - 1) in
 945   let name = if name = "" then "a" else name in
 946    name @::: l
 947  else if List.mem name l then (name ^ "'") @::: l
 948  else name,l
 949 ;;
 950
 951 let (@::) x l = let x,l = x @::: l in x::l;;
 952
 953 let rec pretty_print_type status ctxt =
 954   function
 955     | Var n -> List.nth ctxt (n-1)
 956     | Unit -> "()"
 957     | Top -> "GHC.Prim.Any"
 958     | TConst ref -> pp_ref status ref
 959     | Arrow (t1,t2) ->
 960         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 961          pretty_print_type status ("_"::ctxt) t2
 962     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 963     | Forall (name, kind, t) ->
 964       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 965       let name = capitalize `TypeVariable name in
 966       let name,ctxt = name@:::ctxt in
 967         if size_of_kind kind > 1 then
 968           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
 969         else
 970           "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
 971    | TAppl tl ->
 972       String.concat " "
 973        (List.map
 974          (fun t -> bracket ~prec:0 size_of_type
 975           (pretty_print_type status ctxt) t) tl)
 976
 977 let pretty_print_term_context status ctx1 ctx2 =
 978  let name_context, rev_res =
 979   List.fold_right
 980     (fun el (ctx1,rev_res) ->
 981       match el with
 982          None -> ""@::ctx1,rev_res
 983        | Some (name,`OfKind _) ->
 984           let name = capitalize `TypeVariable name in
 985            name@::ctx1,rev_res
 986        | Some (name,`OfType typ) ->
 987           let name = capitalize `TypeVariable name in
 988           let name,ctx1 = name@:::ctx1 in
 989            name::ctx1,
 990             ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
 991     ) ctx2 (ctx1,[]) in
 992   name_context, String.concat " " (List.rev rev_res)
 993
 994 let rec pretty_print_term status ctxt =
 995   function
 996     | Rel n -> List.nth ctxt (n-1)
 997     | UnitTerm -> "()"
 998     | Const ref -> pp_ref status ref
 999     | Lambda (name,t) ->
1000        let name = capitalize `BoundVariable name in
1001        let name,ctxt = name@:::ctxt in
1002         "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
1003     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
1004     | LetIn (name,s,t) ->
1005        let name = capitalize `BoundVariable name in
1006        let name,ctxt = name@:::ctxt in
1007         "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
1008          pretty_print_term status (name::ctxt) t
1009     | BottomElim ->
1010        "error \"Unreachable code\""
1011     | UnsafeCoerce t ->
1012        "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
1013     | Match (r,matched,pl) ->
1014       if pl = [] then
1015        "error \"Case analysis over empty type\""
1016       else
1017        "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
1018          String.concat " ;\n"
1019            (HExtlib.list_mapi
1020              (fun (bound_names,rhs) i ->
1021                let ref = NReference.mk_constructor (i+1) r in
1022                let name = pp_ref status ref in
1023                let ctxt,bound_names =
1024                 pretty_print_term_context status ctxt bound_names in
1025                let body =
1026                 pretty_print_term status ctxt rhs
1027                in
1028                  "  " ^ name ^ " " ^ bound_names ^ " -> " ^ body
1029              ) pl) ^ "}\n  "
1030     | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
1031     | TLambda (name,t) ->
1032        let name = capitalize `TypeVariable name in
1033         pretty_print_term status (name@::ctxt) t
1034     | Inst t -> pretty_print_term status ctxt t
1035 ;;
1036
1037 let rec pp_obj status (_,ref,obj_kind) =
1038   let pretty_print_context ctx =
1039     String.concat " " (List.rev (snd
1040       (List.fold_right
1041        (fun (x,kind) (l,res) ->
1042          let x,l = x @:::l in
1043          if size_of_kind kind > 1 then
1044           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
1045          else
1046           x::l,x::res)
1047        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
1048   in
1049  let namectx_of_ctx ctx =
1050   List.fold_right (@::)
1051    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
1052  match obj_kind with
1053    TypeDeclaration (ctx,_) ->
1054     (* data?? unsure semantics: inductive type without constructor, but
1055        not matchable apparently *)
1056     if List.length ctx = 0 then
1057       "data " ^ pp_ref status ref
1058     else
1059       "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1060  | TypeDefinition ((ctx, _),ty) ->
1061     let namectx = namectx_of_ctx ctx in
1062     if List.length ctx = 0 then
1063       "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1064     else
1065       "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1066  | TermDeclaration (ctx,ty) ->
1067     let name = pp_ref status ref in
1068       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1069       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1070  | TermDefinition ((ctx,ty),bo) ->
1071     let name = pp_ref status ref in
1072     let namectx = namectx_of_ctx ctx in
1073     (*CSC: BUG here *)
1074     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1075     name ^ " = " ^ pretty_print_term status namectx bo
1076  | LetRec l ->
1077     String.concat "\n" (List.map (pp_obj status) l)
1078  | Algebraic il ->
1079     String.concat "\n"
1080      (List.map
1081       (fun _,ref,left,right,cl ->
1082         "data " ^ pp_ref status ref ^ " " ^
1083         pretty_print_context (right@left) ^ " where\n  " ^
1084         String.concat "\n  " (List.map
1085          (fun ref,tys ->
1086            let namectx = namectx_of_ctx left in
1087             pp_ref status ref ^ " :: " ^
1088              pretty_print_type status namectx tys
1089          ) cl) (*^ "\n    deriving (Prelude.Show)"*)
1090       ) il)
1091  (* inductive and records missing *)
1092
1093 let rec infos_of (info,_,obj_kind) =
1094  info @
1095   match obj_kind with
1096      LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1097    | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1098    | _ -> []
1099
1100 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1101  let status, obj = object_of status obj in
1102   status,
1103    match obj with
1104       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1105     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1106     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1107     | Success o -> pp_obj status o ^ "\n", infos_of o
1108
1109 let refresh_uri_in_typ ~refresh_uri_in_reference =
1110  let rec refresh_uri_in_typ =
1111   function
1112    | Var _
1113    | Unit
1114    | Top as t -> t
1115    | TConst r -> TConst (refresh_uri_in_reference r)
1116    | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1117    | TSkip t -> TSkip (refresh_uri_in_typ t)
1118    | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1119    | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1120  in
1121   refresh_uri_in_typ
1122
1123 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1124  List.map
1125   (function (ref,el) ->
1126     match el with
1127        _,`Constructor
1128      | _,`Function -> refresh_uri_in_reference ref,el
1129      | name,`Type (ctx,typ) ->
1130          let typ =
1131           match typ with
1132              None -> None
1133            | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1134          in
1135           refresh_uri_in_reference ref, (name,`Type (ctx,typ)))
1136   infos