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