1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
29 let apply_subst subst t = assert (subst=[]); t;;
31 type typformerreference = NReference.reference
32 type reference = NReference.reference
36 | KArrow of kind * kind
37 | KSkip of kind (* dropped abstraction *)
39 let rec size_of_kind =
42 | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
43 | KSkip k -> size_of_kind k
46 let bracket size_of pp o =
53 let rec pretty_print_kind =
56 | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
57 | KSkip k -> pretty_print_kind k
64 | TConst of typformerreference
67 | Forall of string * kind * typ
70 let rec size_of_type =
77 | TSkip t -> size_of_type t
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
86 type typ_former_decl = typ_context * kind
87 type typ_former_def = typ_former_decl * typ
93 | Lambda of string * (* typ **) term
95 | LetIn of string * (* typ **) term * term
96 | Match of reference * term * (term_context * term) list
98 | TLambda of (* string **) term
99 | Inst of (*typ_former **) term
101 | UnsafeCoerce of term
104 type term_former_decl = term_context * typ
105 type term_former_def = term_former_decl * term
107 let rec size_of_term =
112 | Lambda (name, body) -> 1 + size_of_term body
113 | Appl l -> List.length l
114 | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
115 | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
117 | TLambda t -> size_of_term t
118 | Inst t -> size_of_term t
119 | Skip t -> size_of_term t
120 | UnsafeCoerce t -> 1 + size_of_term t
123 NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
126 TypeDeclaration of typ_former_decl
127 | TypeDefinition of typ_former_def
128 | TermDeclaration of term_former_decl
129 | TermDefinition of term_former_def
130 | LetRec of (NReference.reference * obj_kind) list
131 (* reference, left, right, constructors *)
132 | Algebraic of (NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
134 type obj = NReference.reference * obj_kind
136 (* For LetRec and Algebraic blocks *)
138 NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
140 let rec classify_not_term status context t =
141 match NCicReduction.whd status ~subst:[] context t with
145 | NCic.Type [`CProp,_] -> `PropKind
146 | NCic.Type [`Type,_] -> `Kind
147 | NCic.Type _ -> assert false)
148 | NCic.Prod (b,s,t) ->
149 (*CSC: using invariant on "_" *)
150 classify_not_term status ((b,NCic.Decl s)::context) t
154 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
155 | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
157 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
158 (* be aware: we can be the head of an application *)
159 assert false (* TODO *)
160 | NCic.Meta _ -> assert false (* TODO *)
161 | NCic.Appl (he::_) -> classify_not_term status context he
163 let rec find_sort typ =
164 match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
165 NCic.Sort NCic.Prop -> `Proposition
166 | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
167 | NCic.Sort (NCic.Type [`Type,_]) ->
168 (*CSC: we could be more precise distinguishing the user provided
169 minimal elements of the hierarchies and classify these
172 | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
173 | NCic.Prod (_,_,t) ->
174 (* we skipped arguments of applications, so here we need to skip
177 | _ -> assert false (* NOT A SORT *)
179 (match List.nth context (n-1) with
180 _,NCic.Decl typ -> find_sort typ
181 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
182 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
183 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
184 (match classify_not_term status [] ty with
186 | `Type -> assert false (* IMPOSSIBLE *)
188 | `KindOrType -> `Type
189 | `PropKind -> `Proposition)
190 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
191 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
192 let _,_,arity,_ = List.nth ityl i in
193 (match classify_not_term status [] arity with
196 | `KindOrType -> assert false (* IMPOSSIBLE *)
198 | `PropKind -> `Proposition)
199 | NCic.Const (NReference.Ref (_,NReference.Con _))
200 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
201 assert false (* IMPOSSIBLE *)
204 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
206 let classify status ~metasenv context t =
207 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
209 (classify_not_term status context t : not_term :> [> not_term])
211 let ty = fix_sorts ty in
213 (match classify_not_term status context ty with
214 | `Proposition -> `Proof
216 | `KindOrType -> `TypeFormerOrTerm
217 | `Kind -> `TypeFormer
218 | `PropKind -> `PropFormer)
222 let rec kind_of status ~metasenv context k =
223 match NCicReduction.whd status ~subst:[] context k with
224 | NCic.Sort NCic.Type _ -> Type
225 | NCic.Sort _ -> assert false (* NOT A KIND *)
226 | NCic.Prod (b,s,t) ->
227 (match classify status ~metasenv context s with
229 KArrow (kind_of status ~metasenv context s,
230 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
235 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
236 | `Term _ -> assert false (* IMPOSSIBLE *))
238 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
241 | NCic.Const _ -> assert false (* NOT A KIND *)
242 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
243 otherwise NOT A KIND *)
245 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
248 let rec skip_args status ~metasenv context =
251 | [],_ -> assert false (* IMPOSSIBLE *)
252 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
254 match classify status ~metasenv context arg with
257 | `Term `TypeFormer ->
258 Some arg::skip_args status ~metasenv context (tl1,tl2)
261 | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
262 | `Term _ -> assert false (* IMPOSSIBLE *)
265 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
267 type db = (typ_context * typ option) ReferenceMap.t
269 class type g_status =
271 method extraction_db: db
274 class virtual status =
277 val extraction_db = ReferenceMap.empty
278 method extraction_db = extraction_db
279 method set_extraction_db v = {< extraction_db = v >}
280 method set_extraction_status
281 : 'status. #g_status as 'status -> 'self
282 = fun o -> {< extraction_db = o#extraction_db >}
285 let rec split_kind_prods context =
287 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
288 | KSkip ta -> split_kind_prods (None::context) ta
289 | Type -> context,Type
292 let rec split_typ_prods context =
294 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
295 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
296 | TSkip ta -> split_typ_prods (None::context) ta
297 | _ as t -> context,t
300 let rec glue_ctx_typ ctx typ =
303 | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
304 | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
305 | None::ctx -> glue_ctx_typ ctx (TSkip typ)
308 let rec split_typ_lambdas status n ~metasenv context typ =
309 if n = 0 then context,typ
311 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
312 | NCic.Lambda (name,s,t) ->
313 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
315 (* eta-expansion required *)
316 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
317 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
318 | NCic.Prod (name,typ,_) ->
319 split_typ_lambdas status (n-1) ~metasenv
320 ((name,NCic.Decl typ)::context)
321 (NCicUntrusted.mk_appl t [NCic.Rel 1])
322 | _ -> assert false (* IMPOSSIBLE *)
326 let context_of_typformer status ~metasenv context =
328 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
329 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
330 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
331 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
332 (try fst (ReferenceMap.find ref status#extraction_db)
334 Not_found -> assert false (* IMPOSSIBLE *))
335 | NCic.Match _ -> assert false (* TODO ???? *)
338 match List.nth context (n-1) with
339 _,NCic.Decl typ -> typ
340 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
341 let typ_ctx = snd (HExtlib.split_nth n context) in
342 let typ = kind_of status ~metasenv typ_ctx typ in
343 fst (split_kind_prods [] typ)
344 | NCic.Meta _ -> assert false (* TODO *)
345 | NCic.Const (NReference.Ref (_,NReference.Con _))
346 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
347 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
348 | NCic.Appl _ | NCic.Prod _ ->
349 assert false (* IMPOSSIBLE *)
351 let rec typ_of status ~metasenv context k =
352 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
353 | NCic.Prod (b,s,t) ->
354 (* CSC: non-invariant assumed here about "_" *)
355 (match classify status ~metasenv context s with
357 Forall (b, kind_of status ~metasenv context s,
358 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
360 | `KindOrType -> (* ??? *)
361 Arrow (typ_of status ~metasenv context s,
362 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
365 TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
366 | `Term _ -> assert false (* IMPOSSIBLE *))
369 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
370 | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
371 | NCic.Rel n -> Var n
372 | NCic.Const ref -> TConst ref
373 | NCic.Appl (he::args) ->
374 let he_context = context_of_typformer status ~metasenv context he in
375 TAppl (typ_of status ~metasenv context he ::
377 (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
378 (skip_args status ~metasenv context (List.rev he_context,args)))
379 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
380 otherwise NOT A TYPE *)
382 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
385 let rec fomega_subst k t1 =
389 else if n < k then Var n
392 | TConst ref -> TConst ref
394 | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
395 | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
396 | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
397 | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
399 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
401 let rec fomega_whd status ty =
404 (match fomega_lookup status r with
406 | Some ty -> fomega_whd status ty)
407 | TAppl (TConst r::args) ->
408 (match fomega_lookup status r with
410 | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
413 let rec term_of status ~metasenv context =
417 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
418 | NCic.Lambda (b,ty,bo) ->
419 (* CSC: non-invariant assumed here about "_" *)
420 (match classify status ~metasenv context ty with
422 TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
423 | `KindOrType (* ??? *)
425 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
429 Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
430 | `Term _ -> assert false (* IMPOSSIBLE *))
431 | NCic.LetIn (b,ty,t,bo) ->
432 (match classify status ~metasenv context t with
433 | `Term `TypeFormerOrTerm (* ???? *)
435 LetIn (b,term_of status ~metasenv context t,
436 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
445 (* not in programming languages, we expand it *)
446 term_of status ~metasenv context
447 (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
448 | NCic.Rel n -> Rel n
449 | NCic.Const ref -> Const ref
450 | NCic.Appl (he::args) ->
451 eat_args status metasenv
452 (term_of status ~metasenv context he) context
453 (typ_of status ~metasenv context
454 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
457 let he_context = context_of_typformer status ~metasenv context he in
458 let process_args he =
461 | `Inst tl -> Inst (process_args he tl)
462 | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
464 Appl (typ_of status ~metasenv context he ::
465 process_args (typ_of status ~metasenv context he)
466 (skip_term_args status ~metasenv context (List.rev he_context,args))
468 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
469 otherwise NOT A TYPE *)
470 | NCic.Meta _ -> assert false (* TODO *)
471 | NCic.Match (ref,_,t,pl) ->
473 let constructors, leftno =
474 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
475 let _,_,_,cl = List.nth tys n in
478 let rec eat_branch n ty context ctx pat =
480 | NCic.Prod (_, _, t), _ when n > 0 ->
481 eat_branch (pred n) t context ctx pat
482 | NCic.Prod (_, _, t), NCic.Lambda (name, ty, t') ->
484 (*BUG: we should classify according to the constructor type*)
485 (Some (name,`OfType (*(typ_of status ~metasenv context ty)*)Unit))::ctx in
486 let context = (name,NCic.Decl ty)::context in
487 eat_branch 0 t context ctx t'
488 (*BUG here, eta-expand!*)
489 | _, _ -> context,ctx, pat
493 (fun (_, name, ty) pat ->
494 let context,lhs,rhs = eat_branch leftno ty context [] pat in
496 (* UnsafeCoerce not always required *)
497 UnsafeCoerce (term_of status ~metasenv context rhs)
501 with Invalid_argument _ -> assert false
503 (match classify_not_term status [] (NCic.Const ref) with
506 | `Kind -> assert false (* IMPOSSIBLE *)
508 (match patterns_of pl with
510 | [_lhs,rhs] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*)
513 Match (ref,term_of status ~metasenv context t, patterns_of pl))
514 and eat_args status metasenv acc context tyhe =
520 Appl args -> Appl (args@[x])
523 match fomega_whd status tyhe with
528 | _ -> term_of status ~metasenv context arg in
529 eat_args status metasenv (mk_appl acc arg) context t tl
531 eat_args status metasenv (Inst acc)
532 context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
534 eat_args status metasenv acc context t tl
535 | Top -> assert false (*TODO: HOW??*)
536 | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
546 let object_of_constant status ~metasenv ref bo ty =
547 match classify status ~metasenv [] ty with
549 let ty = kind_of status ~metasenv [] ty in
550 let ctx0,res = split_kind_prods [] ty in
552 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
553 (match classify status ~metasenv ctx bo with
555 | `KindOrType -> (* ?? no kind formers in System F_omega *)
559 HExtlib.map_option (fun (_,k) ->
560 (*CSC: BUG here, clashes*)
561 String.uncapitalize (fst n),k) p1)
564 let bo = typ_of status ~metasenv ctx bo in
565 status#set_extraction_db
566 (ReferenceMap.add ref (nicectx,Some bo)
567 status#extraction_db),
568 Success (ref,TypeDefinition((nicectx,res),bo))
569 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
571 | `Proposition -> status, Erased
572 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
574 | `Proposition -> status, Erased
575 | `KindOrType (* ??? *)
577 (* CSC: TO BE FINISHED, REF NON REGISTERED *)
578 let ty = typ_of status ~metasenv [] ty in
580 Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
581 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
584 let object_of_inductive status ~metasenv uri ind leftno il =
585 let status,_,rev_tyl =
587 (fun (status,i,res) (_,_,arity,cl) ->
588 match classify_not_term status [] arity with
591 | `Type -> assert false (* IMPOSSIBLE *)
592 | `PropKind -> status,i+1,res
594 let arity = kind_of status ~metasenv [] arity in
595 let ctx,_ = split_kind_prods [] arity in
596 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
598 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
600 status#set_extraction_db
601 (ReferenceMap.add ref (ctx,None) status#extraction_db) in
606 NCicReduction.split_prods status ~subst:[] [] leftno ty in
607 let ty = typ_of status ~metasenv ctx ty in
608 NReference.mk_constructor (j+1) ref,ty
611 status,i+1,(ref,left,right,cl)::res
616 | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
619 let object_of status (uri,height,metasenv,subst,obj_kind) =
620 let obj_kind = apply_subst subst obj_kind in
622 | NCic.Constant (_,_,None,ty,_) ->
623 let ref = NReference.reference_of_spec uri NReference.Decl in
624 (match classify status ~metasenv [] ty with
626 let ty = kind_of status ~metasenv [] ty in
627 let ctx,_ as res = split_kind_prods [] ty in
628 status#set_extraction_db
629 (ReferenceMap.add ref (ctx,None) status#extraction_db),
630 Success (ref, TypeDeclaration res)
632 | `Proposition -> status, Erased
634 | `KindOrType (*???*) ->
635 let ty = typ_of status ~metasenv [] ty in
636 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
637 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
638 | NCic.Constant (_,_,Some bo,ty,_) ->
639 let ref = NReference.reference_of_spec uri (NReference.Def height) in
640 object_of_constant status ~metasenv ref bo ty
641 | NCic.Fixpoint (fix_or_cofix,fs,_) ->
644 (fun (_,_name,recno,ty,bo) (i,status,res) ->
647 NReference.reference_of_spec
648 uri (NReference.Fix (i,recno,height))
650 NReference.reference_of_spec uri (NReference.CoFix i)
652 let status,obj = object_of_constant ~metasenv status ref bo ty in
654 | Success (ref,obj) -> i+1,status, (ref,obj)::res
655 | _ -> i+1,status, res) fs (0,status,[])
657 status, Success (dummyref,LetRec objs)
658 | NCic.Inductive (ind,leftno,il,_) ->
659 object_of_inductive status ~metasenv uri ind leftno il
661 (************************ HASKELL *************************)
663 (* -----------------------------------------------------------------------------
664 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
665 * -----------------------------------------------------------------------------
675 let uncurry f (x, y) =
679 let rec char_list_of_string s =
680 let l = String.length s in
681 let rec aux buffer s =
684 | m -> aux (s.[m - 1]::buffer) s (m - 1)
689 let string_of_char_list s =
693 | x::xs -> aux (String.make 1 x ^ buffer) xs
698 (* ----------------------------------------------------------------------------
699 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
700 * and type variable names.
701 * ----------------------------------------------------------------------------
704 let remove_underscores_and_mark =
705 let rec aux char_list_buffer positions_buffer position =
707 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
710 aux char_list_buffer (position::positions_buffer) position xs
712 aux (x::char_list_buffer) positions_buffer (position + 1) xs
717 let rec capitalize_marked_positions s =
721 if x < String.length s then
722 let c = Char.uppercase (String.get s x) in
723 let _ = String.set s x c in
724 capitalize_marked_positions s xs
726 capitalize_marked_positions s xs
729 let contract_underscores_and_capitalise =
730 char_list_of_string |>
731 remove_underscores_and_mark |>
732 uncurry capitalize_marked_positions
735 let idiomatic_haskell_type_name_of_string =
736 contract_underscores_and_capitalise |>
740 let idiomatic_haskell_term_name_of_string =
741 contract_underscores_and_capitalise |>
745 (*CSC: code to be changed soon when we implement constructors and
746 we fix the code for term application *)
747 let classify_reference status ref =
748 if ReferenceMap.mem ref status#extraction_db then
751 let NReference.Ref (_,ref) = ref in
753 NReference.Con _ -> `Constructor
754 | NReference.Ind _ -> assert false
758 let capitalize classification name =
759 match classification with
761 | `TypeName -> idiomatic_haskell_type_name_of_string name
764 | `FunctionName -> idiomatic_haskell_term_name_of_string name
767 let pp_ref status ref =
768 capitalize (classify_reference status ref)
769 (NCicPp.r2s status true ref)
771 (* cons avoid duplicates *)
772 let rec (@:::) name l =
773 if name <> "" (* propositional things *) && name.[0] = '_' then
774 let name = String.sub name 1 (String.length name - 1) in
775 let name = if name = "" then "a" else name in
777 else if List.mem name l then (name ^ "'") @::: l
781 let (@::) x l = let x,l = x @::: l in x::l;;
783 let rec pretty_print_type status ctxt =
785 | Var n -> List.nth ctxt (n-1)
787 | Top -> assert false (* ??? *)
788 | TConst ref -> pp_ref status ref
790 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
791 pretty_print_type status ("_"::ctxt) t2
792 | TSkip t -> pretty_print_type status ("_"::ctxt) t
793 | Forall (name, kind, t) ->
794 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
795 let name = capitalize `TypeVariable name in
796 let name,ctxt = name@:::ctxt in
797 if size_of_kind kind > 1 then
798 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
800 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
801 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
803 let pretty_print_term_context status ctx1 ctx2 =
804 let name_context, res =
806 (fun el (ctx1,res) ->
808 None -> ""@::ctx1,res
809 | Some (name,`OfKind _) -> name@::ctx1,res
810 | Some (name,`OfType typ) ->
811 let name,ctx1 = name@:::ctx1 in
813 ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::res
815 name_context, String.concat " " res
817 let rec pretty_print_term status ctxt =
819 | Rel n -> List.nth ctxt (n-1)
821 | Const ref -> pp_ref status ref
823 let name = capitalize `BoundVariable name in
824 let name,ctxt = name@:::ctxt in
825 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
826 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
827 | LetIn (name,s,t) ->
828 let name = capitalize `BoundVariable name in
829 let name,ctxt = name@:::ctxt in
830 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
831 pretty_print_term status (name::ctxt) t
833 "error \"Unreachable code\""
835 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
836 | Match (r,matched,pl) ->
838 "error \"Case analysis over empty type\""
840 "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
843 (fun (bound_names,rhs) i ->
844 let ref = NReference.mk_constructor (i+1) r in
845 let name = pp_ref status ref in
846 let names,bound_names =
847 pretty_print_term_context status ctxt bound_names in
849 pretty_print_term status ((List.rev names)@ctxt) rhs
851 " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
854 | TLambda t -> pretty_print_term status (""@::ctxt) t
855 | Inst t -> pretty_print_term status ctxt t
858 let rec pp_obj status (ref,obj_kind) =
859 let pretty_print_context ctx =
860 String.concat " " (List.rev (snd
862 (fun (x,kind) (l,res) ->
864 if size_of_kind kind > 1 then
865 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
868 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
870 let namectx_of_ctx ctx =
871 List.fold_right (@::)
872 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
874 TypeDeclaration (ctx,_) ->
875 (* data?? unsure semantics: inductive type without constructor, but
876 not matchable apparently *)
877 if List.length ctx = 0 then
878 "data " ^ pp_ref status ref
880 "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
881 | TypeDefinition ((ctx, _),ty) ->
882 let namectx = namectx_of_ctx ctx in
883 if List.length ctx = 0 then
884 "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
886 "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
887 | TermDeclaration (ctx,ty) ->
888 let name = pp_ref status ref in
889 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
890 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
891 | TermDefinition ((ctx,ty),bo) ->
892 let name = pp_ref status ref in
893 let namectx = namectx_of_ctx ctx in
895 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
896 name ^ " = " ^ pretty_print_term status namectx bo
898 String.concat "\n" (List.map (pp_obj status) l)
902 (fun ref,left,right,cl ->
903 "data " ^ pp_ref status ref ^ " " ^
904 pretty_print_context (right@left) ^ " where\n " ^
905 String.concat "\n " (List.map
907 let namectx = namectx_of_ctx left in
908 pp_ref status ref ^ " :: " ^
909 pretty_print_type status namectx tys
912 (* inductive and records missing *)
914 let haskell_of_obj status (uri,_,_,_,_ as obj) =
915 let status, obj = object_of status obj in
918 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
919 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
920 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
921 | Success o -> pp_obj status o ^ "\n"