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
86 | Lambda of string * (* typ **) term
88 | LetIn of string * (* typ **) term * term
89 | Match of reference * term * term list
91 | TLambda of (* string **) term
92 | Inst of (*typ_former **) term
94 | UnsafeCoerce of term
97 let rec size_of_term =
102 | Lambda (name, body) -> 1 + size_of_term body
103 | Appl l -> List.length l
104 | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
105 | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
107 | TLambda t -> size_of_term t
108 | Inst t -> size_of_term t
109 | Skip t -> size_of_term t
110 | UnsafeCoerce t -> 1 + size_of_term t
113 NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
115 (* None = dropped abstraction *)
116 type typ_context = (string * kind) option list
117 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
119 type typ_former_decl = typ_context * kind
120 type typ_former_def = typ_former_decl * typ
122 type term_former_decl = term_context * typ
123 type term_former_def = term_former_decl * term
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 obj_kind list
131 (* name, left, right, constructors *)
132 | Algebraic of (string * typ_context * typ_context * (string * typ) list) list
134 type obj = NUri.uri * obj_kind
136 let rec classify_not_term status context t =
137 match NCicReduction.whd status ~subst:[] context t with
141 | NCic.Type [`CProp,_] -> `PropKind
142 | NCic.Type [`Type,_] -> `Kind
143 | NCic.Type _ -> assert false)
144 | NCic.Prod (b,s,t) ->
145 (*CSC: using invariant on "_" *)
146 classify_not_term status ((b,NCic.Decl s)::context) t
150 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
151 | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
153 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
154 (* be aware: we can be the head of an application *)
155 assert false (* TODO *)
156 | NCic.Meta _ -> assert false (* TODO *)
157 | NCic.Appl (he::_) -> classify_not_term status context he
159 let rec find_sort typ =
160 match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
161 NCic.Sort NCic.Prop -> `Proposition
162 | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
163 | NCic.Sort (NCic.Type [`Type,_]) ->
164 (*CSC: we could be more precise distinguishing the user provided
165 minimal elements of the hierarchies and classify these
168 | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
169 | NCic.Prod (_,_,t) ->
170 (* we skipped arguments of applications, so here we need to skip
173 | _ -> assert false (* NOT A SORT *)
175 (match List.nth context (n-1) with
176 _,NCic.Decl typ -> find_sort typ
177 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
178 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
179 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
180 (match classify_not_term status [] ty with
182 | `Type -> assert false (* IMPOSSIBLE *)
184 | `KindOrType -> `Type
185 | `PropKind -> `Proposition)
186 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
187 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
188 let _,_,arity,_ = List.nth ityl i in
189 (match classify_not_term status [] arity with
192 | `KindOrType -> assert false (* IMPOSSIBLE *)
194 | `PropKind -> `Proposition)
195 | NCic.Const (NReference.Ref (_,NReference.Con _))
196 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
197 assert false (* IMPOSSIBLE *)
200 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
202 let classify status ~metasenv context t =
203 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
205 (classify_not_term status context t : not_term :> [> not_term])
207 let ty = fix_sorts ty in
209 (match classify_not_term status context ty with
210 | `Proposition -> `Proof
212 | `KindOrType -> `TypeFormerOrTerm
213 | `Kind -> `TypeFormer
214 | `PropKind -> `PropFormer)
218 let rec kind_of status ~metasenv context k =
219 match NCicReduction.whd status ~subst:[] context k with
220 | NCic.Sort NCic.Type _ -> Type
221 | NCic.Sort _ -> assert false (* NOT A KIND *)
222 | NCic.Prod (b,s,t) ->
223 (match classify status ~metasenv context s with
225 KArrow (kind_of status ~metasenv context s,
226 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
231 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
232 | `Term _ -> assert false (* IMPOSSIBLE *))
234 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
237 | NCic.Const _ -> assert false (* NOT A KIND *)
238 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
239 otherwise NOT A KIND *)
241 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
244 let rec skip_args status ~metasenv context =
247 | [],_ -> assert false (* IMPOSSIBLE *)
248 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
250 match classify status ~metasenv context arg with
253 | `Term `TypeFormer ->
254 Some arg::skip_args status ~metasenv context (tl1,tl2)
257 | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
258 | `Term _ -> assert false (* IMPOSSIBLE *)
261 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
263 type db = (typ_context * typ option) ReferenceMap.t
265 class type g_status =
267 method extraction_db: db
270 class virtual status =
273 val extraction_db = ReferenceMap.empty
274 method extraction_db = extraction_db
275 method set_extraction_db v = {< extraction_db = v >}
276 method set_extraction_status
277 : 'status. #g_status as 'status -> 'self
278 = fun o -> {< extraction_db = o#extraction_db >}
281 let rec split_kind_prods context =
283 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
284 | KSkip ta -> split_kind_prods (None::context) ta
285 | Type -> context,Type
288 let rec split_typ_prods context =
290 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
291 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
292 | TSkip ta -> split_typ_prods (None::context) ta
293 | _ as t -> context,t
296 let rec glue_ctx_typ ctx typ =
299 | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
300 | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
301 | None::ctx -> glue_ctx_typ ctx (TSkip typ)
304 let rec split_typ_lambdas status n ~metasenv context typ =
305 if n = 0 then context,typ
307 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
308 | NCic.Lambda (name,s,t) ->
309 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
311 (* eta-expansion required *)
312 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
313 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
314 | NCic.Prod (name,typ,_) ->
315 split_typ_lambdas status (n-1) ~metasenv
316 ((name,NCic.Decl typ)::context)
317 (NCicUntrusted.mk_appl t [NCic.Rel 1])
318 | _ -> assert false (* IMPOSSIBLE *)
322 let context_of_typformer status ~metasenv context =
324 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
325 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
326 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
327 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
328 (try fst (ReferenceMap.find ref status#extraction_db)
330 Not_found -> assert false (* IMPOSSIBLE *))
331 | NCic.Match _ -> assert false (* TODO ???? *)
334 match List.nth context (n-1) with
335 _,NCic.Decl typ -> typ
336 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
337 let typ_ctx = snd (HExtlib.split_nth n context) in
338 let typ = kind_of status ~metasenv typ_ctx typ in
339 fst (split_kind_prods [] typ)
340 | NCic.Meta _ -> assert false (* TODO *)
341 | NCic.Const (NReference.Ref (_,NReference.Con _))
342 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
343 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
344 | NCic.Appl _ | NCic.Prod _ ->
345 assert false (* IMPOSSIBLE *)
347 let rec typ_of status ~metasenv context k =
348 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
349 | NCic.Prod (b,s,t) ->
350 (* CSC: non-invariant assumed here about "_" *)
351 (match classify status ~metasenv context s with
353 Forall (b, kind_of status ~metasenv context s,
354 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
356 | `KindOrType -> (* ??? *)
357 Arrow (typ_of status ~metasenv context s,
358 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
361 TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
362 | `Term _ -> assert false (* IMPOSSIBLE *))
365 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
366 | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
367 | NCic.Rel n -> Var n
368 | NCic.Const ref -> TConst ref
369 | NCic.Appl (he::args) ->
370 let he_context = context_of_typformer status ~metasenv context he in
371 TAppl (typ_of status ~metasenv context he ::
373 (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
374 (skip_args status ~metasenv context (List.rev he_context,args)))
375 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
376 otherwise NOT A TYPE *)
378 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
381 let rec fomega_subst k t1 =
385 else if n < k then Var n
388 | TConst ref -> TConst ref
390 | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
391 | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
392 | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
393 | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
395 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
397 let rec fomega_whd status ty =
400 (match fomega_lookup status r with
402 | Some ty -> fomega_whd status ty)
403 | TAppl (TConst r::args) ->
404 (match fomega_lookup status r with
406 | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
409 let rec term_of status ~metasenv context =
413 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
414 | NCic.Lambda (b,ty,bo) ->
415 (* CSC: non-invariant assumed here about "_" *)
416 (match classify status ~metasenv context ty with
418 TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
419 | `KindOrType (* ??? *)
421 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
425 Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
426 | `Term _ -> assert false (* IMPOSSIBLE *))
427 | NCic.LetIn (b,ty,t,bo) ->
428 (match classify status ~metasenv context t with
429 | `Term `TypeFormerOrTerm (* ???? *)
431 LetIn (b,term_of status ~metasenv context t,
432 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
441 (* not in programming languages, we expand it *)
442 term_of status ~metasenv context
443 (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
444 | NCic.Rel n -> Rel n
445 | NCic.Const ref -> Const ref
446 | NCic.Appl (he::args) ->
447 eat_args status metasenv
448 (term_of status ~metasenv context he) context
449 (typ_of status ~metasenv context
450 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
453 let he_context = context_of_typformer status ~metasenv context he in
454 let process_args he =
457 | `Inst tl -> Inst (process_args he tl)
458 | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
460 Appl (typ_of status ~metasenv context he ::
461 process_args (typ_of status ~metasenv context he)
462 (skip_term_args status ~metasenv context (List.rev he_context,args))
464 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
465 otherwise NOT A TYPE *)
466 | NCic.Meta _ -> assert false (* TODO *)
467 | NCic.Match (ref,_,t,pl) ->
468 (match classify_not_term status [] (NCic.Const ref) with
471 | `Kind -> assert false (* IMPOSSIBLE *)
476 (* UnsafeCoerce not always required *)
478 (term_of status ~metasenv context p (* Lambdas will be skipped *))
481 Match (ref,term_of status ~metasenv context t,
482 (* UnsafeCoerce not always required *)
483 List.map (fun p -> UnsafeCoerce (term_of status ~metasenv context p)) pl))
484 and eat_args status metasenv acc context tyhe =
490 Appl args -> Appl (args@[x])
493 match fomega_whd status tyhe with
498 | _ -> term_of status ~metasenv context arg in
499 eat_args status metasenv (mk_appl acc arg) context t tl
501 eat_args status metasenv (Inst acc)
502 context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
504 eat_args status metasenv acc context t tl
505 | Top -> assert false (*TODO: HOW??*)
506 | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
516 let object_of_constant status ~metasenv uri height bo ty =
517 match classify status ~metasenv [] ty with
519 let ty = kind_of status ~metasenv [] ty in
520 let ctx0,res = split_kind_prods [] ty in
522 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
523 (match classify status ~metasenv ctx bo with
525 | `KindOrType -> (* ?? no kind formers in System F_omega *)
529 HExtlib.map_option (fun (_,k) ->
530 (*CSC: BUG here, clashes*)
531 String.uncapitalize (fst n),k) p1)
534 (* BUG here: for mutual type definitions the spec is not good *)
536 NReference.reference_of_spec uri (NReference.Def height) in
537 let bo = typ_of status ~metasenv ctx bo in
538 status#set_extraction_db
539 (ReferenceMap.add ref (nicectx,Some bo)
540 status#extraction_db),
541 Success (uri,TypeDefinition((nicectx,res),bo))
542 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
544 | `Proposition -> status, Erased
545 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
547 | `Proposition -> status, Erased
548 | `KindOrType (* ??? *)
550 (* CSC: TO BE FINISHED, REF NON REGISTERED *)
551 let ty = typ_of status ~metasenv [] ty in
553 Success (uri, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
554 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
557 let object_of_inductive status ~metasenv uri ind leftno il =
558 let status,_,rev_tyl =
560 (fun (status,i,res) (_,name,arity,cl) ->
561 match classify_not_term status [] arity with
564 | `Type -> assert false (* IMPOSSIBLE *)
565 | `PropKind -> status,i+1,res
567 let arity = kind_of status ~metasenv [] arity in
568 let ctx,_ = split_kind_prods [] arity in
569 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
571 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
573 status#set_extraction_db
574 (ReferenceMap.add ref (ctx,None) status#extraction_db) in
579 NCicReduction.split_prods status ~subst:[] [] leftno ty in
580 let ty = typ_of status ~metasenv ctx ty in
584 status,i+1,(name,left,right,cl)::res
589 | _ -> status, Success (uri, Algebraic (List.rev rev_tyl))
592 let object_of status (uri,height,metasenv,subst,obj_kind) =
593 let obj_kind = apply_subst subst obj_kind in
595 | NCic.Constant (_,_,None,ty,_) ->
596 (match classify status ~metasenv [] ty with
598 let ty = kind_of status ~metasenv [] ty in
599 let ctx,_ as res = split_kind_prods [] ty in
600 let ref = NReference.reference_of_spec uri NReference.Decl in
601 status#set_extraction_db
602 (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res)
604 | `Proposition -> status, Erased
606 | `KindOrType (*???*) ->
607 let ty = typ_of status ~metasenv [] ty in
608 status, Success (uri, TermDeclaration (split_typ_prods [] ty))
609 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
610 | NCic.Constant (_,_,Some bo,ty,_) ->
611 object_of_constant status ~metasenv uri height bo ty
612 | NCic.Fixpoint (_fix_or_cofix,fs,_) ->
615 (fun (_,_name,_,ty,bo) (status,res) ->
616 let status,obj = object_of_constant ~metasenv status uri height bo ty in
618 | Success (_uri,obj) -> status, obj::res
619 | _ -> status, res) fs (status,[])
621 status, Success (uri,LetRec objs)
622 | NCic.Inductive (ind,leftno,il,_) ->
623 object_of_inductive status ~metasenv uri ind leftno il
625 (************************ HASKELL *************************)
627 (* -----------------------------------------------------------------------------
628 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
629 * -----------------------------------------------------------------------------
639 let uncurry f (x, y) =
643 let rec char_list_of_string s =
644 let l = String.length s in
645 let rec aux buffer s =
648 | m -> aux (s.[m - 1]::buffer) s (m - 1)
653 let string_of_char_list s =
657 | x::xs -> aux (String.make 1 x ^ buffer) xs
662 (* ----------------------------------------------------------------------------
663 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
664 * and type variable names.
665 * ----------------------------------------------------------------------------
668 let remove_underscores_and_mark =
669 let rec aux char_list_buffer positions_buffer position =
671 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
674 aux char_list_buffer (position::positions_buffer) position xs
676 aux (x::char_list_buffer) positions_buffer (position + 1) xs
681 let rec capitalize_marked_positions s =
685 if x < String.length s then
686 let c = Char.uppercase (String.get s x) in
687 let _ = String.set s x c in
688 capitalize_marked_positions s xs
690 capitalize_marked_positions s xs
693 let contract_underscores_and_capitalise =
694 char_list_of_string |>
695 remove_underscores_and_mark |>
696 uncurry capitalize_marked_positions
699 let idiomatic_haskell_type_name_of_string =
700 contract_underscores_and_capitalise |>
704 let idiomatic_haskell_term_name_of_string =
705 contract_underscores_and_capitalise |>
709 (*CSC: code to be changed soon when we implement constructors and
710 we fix the code for term application *)
711 let classify_reference status ref =
712 if ReferenceMap.mem ref status#extraction_db then
715 let NReference.Ref (_,ref) = ref in
717 NReference.Con _ -> `Constructor
718 | NReference.Ind _ -> assert false
722 let capitalize classification name =
723 match classification with
725 | `TypeName -> idiomatic_haskell_type_name_of_string name
728 | `FunctionName -> idiomatic_haskell_term_name_of_string name
731 let pp_ref status ref =
732 capitalize (classify_reference status ref)
733 (NCicPp.r2s status false ref)
735 let name_of_uri classification uri =
736 capitalize classification (NUri.name_of_uri uri)
738 (* cons avoid duplicates *)
739 let rec (@:::) name l =
740 if name <> "" (* propositional things *) && name.[0] = '_' then
741 let name = String.sub name 1 (String.length name - 1) in
742 let name = if name = "" then "a" else name in
744 else if List.mem name l then (name ^ "'") @::: l
748 let (@::) x l = let x,l = x @::: l in x::l;;
750 let rec pretty_print_type status ctxt =
752 | Var n -> List.nth ctxt (n-1)
754 | Top -> assert false (* ??? *)
755 | TConst ref -> pp_ref status ref
757 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
758 pretty_print_type status ("_"::ctxt) t2
759 | TSkip t -> pretty_print_type status ("_"::ctxt) t
760 | Forall (name, kind, t) ->
761 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
762 let name = capitalize `TypeVariable name in
763 let name,ctxt = name@:::ctxt in
764 if size_of_kind kind > 1 then
765 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
767 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
768 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
770 let rec pretty_print_term status ctxt =
772 | Rel n -> List.nth ctxt (n-1)
774 | Const ref -> pp_ref status ref
776 let name = capitalize `BoundVariable name in
777 let name,ctxt = name@:::ctxt in
778 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
779 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
780 | LetIn (name,s,t) ->
781 let name = capitalize `BoundVariable name in
782 let name,ctxt = name@:::ctxt in
783 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
784 pretty_print_term status (name::ctxt) t
786 "error \"Unreachable code\""
788 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
789 | Match (r,matched,pl) ->
791 "error \"Case analysis over empty type\""
793 let constructors, leftno =
794 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
795 let _,_,_,cl = List.nth tys n in
798 let rec eat_branch n ty pat =
800 | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat
801 | NCic.Prod (_, _, t), Lambda (name, t') ->
802 (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
803 let cv, rhs = eat_branch 0 t t' in
811 (fun (_, name, ty) pat -> incr j; name, eat_branch leftno ty pat) constructors pl
812 with Invalid_argument _ -> assert false
814 "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
817 (fun (name,(bound_names,rhs)) ->
819 (*CSC: BUG avoid name clashes *)
820 String.concat " " (String.capitalize name::bound_names),
821 pretty_print_term status ((List.rev bound_names)@ctxt) rhs
823 " " ^ pattern ^ " -> " ^ body
826 | TLambda t -> pretty_print_term status (""@::ctxt) t
827 | Inst t -> pretty_print_term status ctxt t
831 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
833 type term_former_def = term_context * term * typ
834 type term_former_decl = term_context * typ
837 let rec pp_obj status (uri,obj_kind) =
838 let pretty_print_context ctx =
839 String.concat " " (List.rev (snd
841 (fun (x,kind) (l,res) ->
843 if size_of_kind kind > 1 then
844 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
847 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
849 let namectx_of_ctx ctx =
850 List.fold_right (@::)
851 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
853 TypeDeclaration (ctx,_) ->
854 (* data?? unsure semantics: inductive type without constructor, but
855 not matchable apparently *)
856 if List.length ctx = 0 then
857 "data " ^ name_of_uri `TypeName uri
859 "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx
860 | TypeDefinition ((ctx, _),ty) ->
861 let namectx = namectx_of_ctx ctx in
862 if List.length ctx = 0 then
863 "type " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty
865 "type " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
866 | TermDeclaration (ctx,ty) ->
867 let name = name_of_uri `FunctionName uri in
868 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
869 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
870 | TermDefinition ((ctx,ty),bo) ->
871 let name = name_of_uri `FunctionName uri in
872 let namectx = namectx_of_ctx ctx in
874 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
875 name ^ " = " ^ pretty_print_term status namectx bo
877 (*CSC: BUG always uses the name of the URI *)
878 String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
882 (fun _name,left,right,cl ->
883 (*CSC: BUG always uses the name of the URI *)
884 "data " ^ name_of_uri `TypeName uri ^ " " ^
885 pretty_print_context (right@left) ^ " where\n " ^
886 String.concat "\n " (List.map
888 let namectx = namectx_of_ctx left in
889 capitalize `Constructor name ^ " :: " ^
890 pretty_print_type status namectx tys
893 (* inductive and records missing *)
895 let haskell_of_obj status (uri,_,_,_,_ as obj) =
896 let status, obj = object_of status obj in
899 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
900 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
901 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
902 | Success o -> pp_obj status o ^ "\n"