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