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