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