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
109 Appl args -> Appl (args@[x])
112 let rec size_of_term =
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
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
128 NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
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
139 type obj = NReference.reference * obj_kind
141 (* For LetRec and Algebraic blocks *)
143 NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
145 let rec classify_not_term status context t =
146 match NCicReduction.whd status ~subst:[] context t with
150 | NCic.Type [`CProp,_] -> `PropKind
151 | NCic.Type [`Type,_] -> `Kind
152 | NCic.Type _ -> assert false)
153 | NCic.Prod (b,s,t) ->
154 (*CSC: using invariant on "_" *)
155 classify_not_term status ((b,NCic.Decl s)::context) t
159 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
161 assert false (* NOT POSSIBLE *)
163 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
164 (* be aware: we can be the head of an application *)
165 assert false (* TODO *)
166 | NCic.Meta _ -> assert false (* TODO *)
167 | NCic.Appl (he::_) -> classify_not_term status context he
169 let rec find_sort typ =
170 match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
171 NCic.Sort NCic.Prop -> `Proposition
172 | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
173 | NCic.Sort (NCic.Type [`Type,_]) ->
174 (*CSC: we could be more precise distinguishing the user provided
175 minimal elements of the hierarchies and classify these
178 | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
179 | NCic.Prod (_,_,t) ->
180 (* we skipped arguments of applications, so here we need to skip
183 | _ -> assert false (* NOT A SORT *)
185 (match List.nth context (n-1) with
186 _,NCic.Decl typ -> find_sort typ
187 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
188 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
189 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
190 (match classify_not_term status [] ty with
192 | `Type -> assert false (* IMPOSSIBLE *)
194 | `KindOrType -> `Type
195 | `PropKind -> `Proposition)
196 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
197 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
198 let _,_,arity,_ = List.nth ityl i in
199 (match classify_not_term status [] arity with
202 | `KindOrType -> assert false (* IMPOSSIBLE *)
204 | `PropKind -> `Proposition)
205 | NCic.Const (NReference.Ref (_,NReference.Con _))
206 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
207 assert false (* IMPOSSIBLE *)
210 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
212 let classify status ~metasenv context t =
213 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
215 (classify_not_term status context t : not_term :> [> not_term])
217 let ty = fix_sorts ty in
219 (match classify_not_term status context ty with
220 | `Proposition -> `Proof
222 | `KindOrType -> `TypeFormerOrTerm
223 | `Kind -> `TypeFormer
224 | `PropKind -> `PropFormer)
228 let rec kind_of status ~metasenv context k =
229 match NCicReduction.whd status ~subst:[] context k with
230 | NCic.Sort NCic.Type _ -> Type
231 | NCic.Sort _ -> assert false (* NOT A KIND *)
232 | NCic.Prod (b,s,t) ->
233 (match classify status ~metasenv context s with
235 KArrow (kind_of status ~metasenv context s,
236 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
241 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
242 | `Term _ -> assert false (* IMPOSSIBLE *))
244 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
247 | NCic.Const _ -> assert false (* NOT A KIND *)
248 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
249 otherwise NOT A KIND *)
251 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
254 let rec skip_args status ~metasenv context =
257 | [],_ -> assert false (* IMPOSSIBLE *)
258 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
260 match classify status ~metasenv context arg with
263 | `Term `TypeFormer ->
264 Some arg::skip_args status ~metasenv context (tl1,tl2)
267 | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
268 | `Term _ -> assert false (* IMPOSSIBLE *)
271 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
273 type db = (typ_context * typ option) ReferenceMap.t
275 class type g_status =
277 method extraction_db: db
280 class virtual status =
283 val extraction_db = ReferenceMap.empty
284 method extraction_db = extraction_db
285 method set_extraction_db v = {< extraction_db = v >}
286 method set_extraction_status
287 : 'status. #g_status as 'status -> 'self
288 = fun o -> {< extraction_db = o#extraction_db >}
291 let rec split_kind_prods context =
293 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
294 | KSkip ta -> split_kind_prods (None::context) ta
295 | Type -> context,Type
298 let rec split_typ_prods context =
300 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
301 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
302 | TSkip ta -> split_typ_prods (None::context) ta
303 | _ as t -> context,t
306 let rec glue_ctx_typ ctx typ =
309 | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
310 | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
311 | None::ctx -> glue_ctx_typ ctx (TSkip typ)
314 let rec split_typ_lambdas status n ~metasenv context typ =
315 if n = 0 then context,typ
317 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
318 | NCic.Lambda (name,s,t) ->
319 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
321 (* eta-expansion required *)
322 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
323 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
324 | NCic.Prod (name,typ,_) ->
325 split_typ_lambdas status (n-1) ~metasenv
326 ((name,NCic.Decl typ)::context)
327 (NCicUntrusted.mk_appl t [NCic.Rel 1])
328 | _ -> assert false (* IMPOSSIBLE *)
332 let rev_context_of_typformer status ~metasenv context =
334 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
335 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
336 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
337 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
338 (try List.rev (fst (ReferenceMap.find ref status#extraction_db))
341 (* This can happen only when we are processing the type of
342 the constructor of a small singleton type. In this case
343 we are not interested in all the type, but only in its
344 backbone. That is why we can safely return the dummy context here *)
345 let rec dummy = None::dummy in
347 | NCic.Match _ -> assert false (* TODO ???? *)
350 match List.nth context (n-1) with
351 _,NCic.Decl typ -> typ
352 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
353 let typ_ctx = snd (HExtlib.split_nth n context) in
354 let typ = kind_of status ~metasenv typ_ctx typ in
355 List.rev (fst (split_kind_prods [] typ))
356 | NCic.Meta _ -> assert false (* TODO *)
357 | NCic.Const (NReference.Ref (_,NReference.Con _))
358 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
359 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
360 | NCic.Appl _ | NCic.Prod _ ->
361 assert false (* IMPOSSIBLE *)
363 let rec typ_of status ~metasenv context k =
364 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
365 | NCic.Prod (b,s,t) ->
366 (* CSC: non-invariant assumed here about "_" *)
367 (match classify status ~metasenv context s with
369 Forall (b, kind_of status ~metasenv context s,
370 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
372 | `KindOrType -> (* ??? *)
373 Arrow (typ_of status ~metasenv context s,
374 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
377 TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
378 | `Term _ -> assert false (* IMPOSSIBLE *))
381 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
382 | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
383 | NCic.Rel n -> Var n
384 | NCic.Const ref -> TConst ref
385 | NCic.Appl (he::args) ->
386 let rev_he_context= rev_context_of_typformer status ~metasenv context he in
387 TAppl (typ_of status ~metasenv context he ::
389 (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
390 (skip_args status ~metasenv context (rev_he_context,args)))
391 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
392 otherwise NOT A TYPE *)
394 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
397 let rec fomega_subst k t1 =
401 else if n < k then Var n
404 | TConst ref -> TConst ref
406 | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
407 | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
408 | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
409 | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
411 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
413 let rec fomega_whd status ty =
416 (match fomega_lookup status r with
418 | Some ty -> fomega_whd status ty)
419 | TAppl (TConst r::args) ->
420 (match fomega_lookup status r with
422 | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
425 let rec term_of status ~metasenv context =
429 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
430 | NCic.Lambda (b,ty,bo) ->
431 (* CSC: non-invariant assumed here about "_" *)
432 (match classify status ~metasenv context ty with
434 TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
435 | `KindOrType (* ??? *)
437 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
441 Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
442 | `Term _ -> assert false (* IMPOSSIBLE *))
443 | NCic.LetIn (b,ty,t,bo) ->
444 (match classify status ~metasenv context t with
445 | `Term `TypeFormerOrTerm (* ???? *)
447 LetIn (b,term_of status ~metasenv context t,
448 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
457 (* not in programming languages, we expand it *)
458 term_of status ~metasenv context
459 (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
460 | NCic.Rel n -> Rel n
461 | NCic.Const ref -> Const ref
462 | NCic.Appl (he::args) ->
463 eat_args status metasenv
464 (term_of status ~metasenv context he) context
465 (*BUG: recomputing every time the type of the head*)
466 (typ_of status ~metasenv context
467 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
469 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
470 otherwise NOT A TYPE *)
471 | NCic.Meta _ -> assert false (* TODO *)
472 | NCic.Match (ref,_,t,pl) ->
474 let constructors, leftno =
475 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
476 let _,_,_,cl = List.nth tys n in
479 let rec eat_branch n ty context ctx pat =
483 | Arrow (_, t), _ when n > 0 ->
484 eat_branch (pred n) t context ctx pat
485 | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
486 (*CSC: unify the three cases below? *)
487 | Arrow (_, t), NCic.Lambda (name, ty, t') ->
489 (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
490 let context = (name,NCic.Decl ty)::context in
491 eat_branch 0 t context ctx t'
492 | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
494 (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
495 let context = (name,NCic.Decl ty)::context in
496 eat_branch 0 t context ctx t'
497 | TSkip t,NCic.Lambda (name, ty, t') ->
498 let ctx = None::ctx in
499 let context = (name,NCic.Decl ty)::context in
500 eat_branch 0 t context ctx t'
501 | Top,_ -> assert false (*TODO: HOW??*)
502 (*BUG here, eta-expand!*)
503 | _, _ -> context,ctx, pat
507 (fun (_, name, ty) pat ->
508 (*BUG: recomputing every time the type of the constructor*)
509 let ty = typ_of status ~metasenv context ty in
510 let context,lhs,rhs = eat_branch leftno ty context [] pat in
512 (* UnsafeCoerce not always required *)
513 UnsafeCoerce (term_of status ~metasenv context rhs)
517 with Invalid_argument _ -> assert false
519 (match classify_not_term status [] (NCic.Const ref) with
522 | `Kind -> assert false (* IMPOSSIBLE *)
524 (match patterns_of pl with
526 | [_lhs,rhs] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*)
529 Match (ref,term_of status ~metasenv context t, patterns_of pl))
530 and eat_args status metasenv acc context tyhe =
534 match fomega_whd status tyhe with
539 | _ -> term_of status ~metasenv context arg in
540 eat_args status metasenv (mk_appl acc arg) context t tl
542 (match classify status ~metasenv context arg with
543 | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
547 eat_args status metasenv (UnsafeCoerce (Inst acc))
548 context (fomega_subst 1 Unit t) tl
549 | `Term _ -> assert false (*TODO: ????*)
552 eat_args status metasenv (Inst acc)
553 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
556 eat_args status metasenv acc context t tl
557 | Top -> assert false (*TODO: HOW??*)
558 | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
568 let object_of_constant status ~metasenv ref bo ty =
569 match classify status ~metasenv [] ty with
571 let ty = kind_of status ~metasenv [] ty in
572 let ctx0,res = split_kind_prods [] ty in
574 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
575 (match classify status ~metasenv ctx bo with
577 | `KindOrType -> (* ?? no kind formers in System F_omega *)
581 HExtlib.map_option (fun (_,k) ->
582 (*CSC: BUG here, clashes*)
583 String.uncapitalize (fst n),k) p1)
586 let bo = typ_of status ~metasenv ctx bo in
587 status#set_extraction_db
588 (ReferenceMap.add ref (nicectx,Some bo)
589 status#extraction_db),
590 Success (ref,TypeDefinition((nicectx,res),bo))
591 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
593 | `Proposition -> status, Erased
594 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
596 | `Proposition -> status, Erased
597 | `KindOrType (* ??? *)
599 (* CSC: TO BE FINISHED, REF NON REGISTERED *)
600 let ty = typ_of status ~metasenv [] ty in
602 Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
603 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
606 let object_of_inductive status ~metasenv uri ind leftno il =
607 let status,_,rev_tyl =
609 (fun (status,i,res) (_,_,arity,cl) ->
610 match classify_not_term status [] arity with
613 | `Type -> assert false (* IMPOSSIBLE *)
614 | `PropKind -> status,i+1,res
616 let arity = kind_of status ~metasenv [] arity in
617 let ctx,_ = split_kind_prods [] arity in
618 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
620 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
622 status#set_extraction_db
623 (ReferenceMap.add ref (ctx,None) status#extraction_db) in
628 NCicReduction.split_prods status ~subst:[] [] leftno ty in
629 let ty = typ_of status ~metasenv ctx ty in
630 NReference.mk_constructor (j+1) ref,ty
633 status,i+1,(ref,left,right,cl)::res
638 | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl))
641 let object_of status (uri,height,metasenv,subst,obj_kind) =
642 let obj_kind = apply_subst subst obj_kind in
644 | NCic.Constant (_,_,None,ty,_) ->
645 let ref = NReference.reference_of_spec uri NReference.Decl in
646 (match classify status ~metasenv [] ty with
648 let ty = kind_of status ~metasenv [] ty in
649 let ctx,_ as res = split_kind_prods [] ty in
650 status#set_extraction_db
651 (ReferenceMap.add ref (ctx,None) status#extraction_db),
652 Success (ref, TypeDeclaration res)
654 | `Proposition -> status, Erased
656 | `KindOrType (*???*) ->
657 let ty = typ_of status ~metasenv [] ty in
658 status, Success (ref, TermDeclaration (split_typ_prods [] ty))
659 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
660 | NCic.Constant (_,_,Some bo,ty,_) ->
661 let ref = NReference.reference_of_spec uri (NReference.Def height) in
662 object_of_constant status ~metasenv ref bo ty
663 | NCic.Fixpoint (fix_or_cofix,fs,_) ->
666 (fun (_,_name,recno,ty,bo) (i,status,res) ->
669 NReference.reference_of_spec
670 uri (NReference.Fix (i,recno,height))
672 NReference.reference_of_spec uri (NReference.CoFix i)
674 let status,obj = object_of_constant ~metasenv status ref bo ty in
676 | Success (ref,obj) -> i+1,status, (ref,obj)::res
677 | _ -> i+1,status, res) fs (0,status,[])
679 status, Success (dummyref,LetRec objs)
680 | NCic.Inductive (ind,leftno,il,_) ->
681 object_of_inductive status ~metasenv uri ind leftno il
683 (************************ HASKELL *************************)
685 (* -----------------------------------------------------------------------------
686 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
687 * -----------------------------------------------------------------------------
697 let uncurry f (x, y) =
701 let rec char_list_of_string s =
702 let l = String.length s in
703 let rec aux buffer s =
706 | m -> aux (s.[m - 1]::buffer) s (m - 1)
711 let string_of_char_list s =
715 | x::xs -> aux (String.make 1 x ^ buffer) xs
720 (* ----------------------------------------------------------------------------
721 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
722 * and type variable names.
723 * ----------------------------------------------------------------------------
726 let remove_underscores_and_mark =
727 let rec aux char_list_buffer positions_buffer position =
729 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
732 aux char_list_buffer (position::positions_buffer) position xs
734 aux (x::char_list_buffer) positions_buffer (position + 1) xs
739 let rec capitalize_marked_positions s =
743 if x < String.length s then
744 let c = Char.uppercase (String.get s x) in
745 let _ = String.set s x c in
746 capitalize_marked_positions s xs
748 capitalize_marked_positions s xs
751 let contract_underscores_and_capitalise =
752 char_list_of_string |>
753 remove_underscores_and_mark |>
754 uncurry capitalize_marked_positions
757 let idiomatic_haskell_type_name_of_string =
758 contract_underscores_and_capitalise |>
762 let idiomatic_haskell_term_name_of_string =
763 contract_underscores_and_capitalise |>
767 (*CSC: code to be changed soon when we implement constructors and
768 we fix the code for term application *)
769 let classify_reference status ref =
770 if ReferenceMap.mem ref status#extraction_db then
773 let NReference.Ref (_,ref) = ref in
775 NReference.Con _ -> `Constructor
776 | NReference.Ind _ -> assert false
780 let capitalize classification name =
781 match classification with
783 | `TypeName -> idiomatic_haskell_type_name_of_string name
786 | `FunctionName -> idiomatic_haskell_term_name_of_string name
789 let pp_ref status ref =
790 capitalize (classify_reference status ref)
791 (NCicPp.r2s status true ref)
793 (* cons avoid duplicates *)
794 let rec (@:::) name l =
795 if name <> "" (* propositional things *) && name.[0] = '_' then
796 let name = String.sub name 1 (String.length name - 1) in
797 let name = if name = "" then "a" else name in
799 else if List.mem name l then (name ^ "'") @::: l
803 let (@::) x l = let x,l = x @::: l in x::l;;
805 let rec pretty_print_type status ctxt =
807 | Var n -> List.nth ctxt (n-1)
809 | Top -> assert false (* ??? *)
810 | TConst ref -> pp_ref status ref
812 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
813 pretty_print_type status ("_"::ctxt) t2
814 | TSkip t -> pretty_print_type status ("_"::ctxt) t
815 | Forall (name, kind, t) ->
816 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
817 let name = capitalize `TypeVariable name in
818 let name,ctxt = name@:::ctxt in
819 if size_of_kind kind > 1 then
820 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
822 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
823 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
825 let pretty_print_term_context status ctx1 ctx2 =
826 let name_context, rev_res =
828 (fun el (ctx1,rev_res) ->
830 None -> ""@::ctx1,rev_res
831 | Some (name,`OfKind _) -> name@::ctx1,rev_res
832 | Some (name,`OfType typ) ->
833 let name,ctx1 = name@:::ctx1 in
835 ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
837 name_context, String.concat " " (List.rev rev_res)
839 let rec pretty_print_term status ctxt =
841 | Rel n -> List.nth ctxt (n-1)
843 | Const ref -> pp_ref status ref
845 let name = capitalize `BoundVariable name in
846 let name,ctxt = name@:::ctxt in
847 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
848 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
849 | LetIn (name,s,t) ->
850 let name = capitalize `BoundVariable name in
851 let name,ctxt = name@:::ctxt in
852 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
853 pretty_print_term status (name::ctxt) t
855 "error \"Unreachable code\""
857 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
858 | Match (r,matched,pl) ->
860 "error \"Case analysis over empty type\""
862 "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
865 (fun (bound_names,rhs) i ->
866 let ref = NReference.mk_constructor (i+1) r in
867 let name = pp_ref status ref in
868 let ctxt,bound_names =
869 pretty_print_term_context status ctxt bound_names in
871 pretty_print_term status ctxt rhs
873 " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
875 | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
876 | TLambda (name,t) ->
877 let name = capitalize `TypeVariable name in
878 pretty_print_term status (name@::ctxt) t
879 | Inst t -> pretty_print_term status ctxt t
882 let rec pp_obj status (ref,obj_kind) =
883 let pretty_print_context ctx =
884 String.concat " " (List.rev (snd
886 (fun (x,kind) (l,res) ->
888 if size_of_kind kind > 1 then
889 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
892 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
894 let namectx_of_ctx ctx =
895 List.fold_right (@::)
896 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
898 TypeDeclaration (ctx,_) ->
899 (* data?? unsure semantics: inductive type without constructor, but
900 not matchable apparently *)
901 if List.length ctx = 0 then
902 "data " ^ pp_ref status ref
904 "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
905 | TypeDefinition ((ctx, _),ty) ->
906 let namectx = namectx_of_ctx ctx in
907 if List.length ctx = 0 then
908 "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
910 "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
911 | TermDeclaration (ctx,ty) ->
912 let name = pp_ref status ref in
913 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
914 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
915 | TermDefinition ((ctx,ty),bo) ->
916 let name = pp_ref status ref in
917 let namectx = namectx_of_ctx ctx in
919 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
920 name ^ " = " ^ pretty_print_term status namectx bo
922 String.concat "\n" (List.map (pp_obj status) l)
926 (fun ref,left,right,cl ->
927 "data " ^ pp_ref status ref ^ " " ^
928 pretty_print_context (right@left) ^ " where\n " ^
929 String.concat "\n " (List.map
931 let namectx = namectx_of_ctx left in
932 pp_ref status ref ^ " :: " ^
933 pretty_print_type status namectx tys
936 (* inductive and records missing *)
938 let haskell_of_obj status (uri,_,_,_,_ as obj) =
939 let status, obj = object_of status obj in
942 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
943 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
944 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
945 | Success o -> pp_obj status o ^ "\n"