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 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
130 module GlobalNames = Set.Make(String)
133 string * [`Type of typ_context * typ option | `Constructor | `Function ]
134 type info = (NReference.reference * info_el) list
135 type db = info_el ReferenceMap.t * GlobalNames.t
140 TypeDeclaration of typ_former_decl
141 | TypeDefinition of typ_former_def
142 | TermDeclaration of term_former_decl
143 | TermDefinition of term_former_def
144 | LetRec of (info * NReference.reference * obj_kind) list
145 (* reference, left, right, constructors *)
146 | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
148 type obj = info * NReference.reference * obj_kind
150 (* For LetRec and Algebraic blocks *)
152 NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
154 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
156 let max_not_term t1 t2 =
159 | _,`KindOrType -> `KindOrType
165 | _,`PropKind -> `PropKind
166 | `Proposition,`Proposition -> `Proposition
168 let sup = List.fold_left max_not_term `Proposition
170 let rec classify_not_term status context t =
171 match NCicReduction.whd status ~subst:[] context t with
175 | NCic.Type [`CProp,_] -> `PropKind
176 | NCic.Type [`Type,_] -> `Kind
177 | NCic.Type _ -> assert false)
178 | NCic.Prod (b,s,t) ->
179 (*CSC: using invariant on "_" *)
180 classify_not_term status ((b,NCic.Decl s)::context) t
183 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
185 assert false (* NOT POSSIBLE *)
186 | NCic.Lambda (n,s,t) ->
187 (* Lambdas can me met in branches of matches, expecially when the
188 output type is a product *)
189 classify_not_term status ((n,NCic.Decl s)::context) t
190 | NCic.Match (_,_,_,pl) ->
191 let classified_pl = List.map (classify_not_term status context) pl in
193 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
194 assert false (* IMPOSSIBLE *)
195 | NCic.Meta _ -> assert false (* TODO *)
196 | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)->
197 let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
198 let _,_,_,_,bo = List.nth l i in
199 classify_not_term status [] bo
200 | NCic.Appl (he::_) -> classify_not_term status context he
202 let rec find_sort typ =
203 match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
204 NCic.Sort NCic.Prop -> `Proposition
205 | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
206 | NCic.Sort (NCic.Type [`Type,_]) ->
207 (*CSC: we could be more precise distinguishing the user provided
208 minimal elements of the hierarchies and classify these
211 | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
212 | NCic.Prod (_,_,t) ->
213 (* we skipped arguments of applications, so here we need to skip
216 | _ -> assert false (* NOT A SORT *)
218 (match List.nth context (n-1) with
219 _,NCic.Decl typ -> find_sort typ
220 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
221 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
222 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
223 (match classify_not_term status [] ty with
225 | `Type -> assert false (* IMPOSSIBLE *)
227 | `KindOrType -> `Type
228 | `PropKind -> `Proposition)
229 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
230 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
231 let _,_,arity,_ = List.nth ityl i in
232 (match classify_not_term status [] arity with
235 | `KindOrType -> assert false (* IMPOSSIBLE *)
237 | `PropKind -> `Proposition)
238 | NCic.Const (NReference.Ref (_,NReference.Con _))
239 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
240 assert false (* IMPOSSIBLE *)
243 let classify status ~metasenv context t =
244 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
246 (classify_not_term status context t : not_term :> [> not_term])
248 let ty = fix_sorts ty in
250 (match classify_not_term status context ty with
251 | `Proposition -> `Proof
253 | `KindOrType -> `TypeFormerOrTerm
254 | `Kind -> `TypeFormer
255 | `PropKind -> `PropFormer)
259 let rec kind_of status ~metasenv context k =
260 match NCicReduction.whd status ~subst:[] context k with
261 | NCic.Sort NCic.Type _ -> Type
262 | NCic.Sort _ -> assert false (* NOT A KIND *)
263 | NCic.Prod (b,s,t) ->
264 (match classify status ~metasenv context s with
266 KArrow (kind_of status ~metasenv context s,
267 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
272 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
273 | `Term _ -> assert false (* IMPOSSIBLE *))
275 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
278 | NCic.Const _ -> assert false (* NOT A KIND *)
279 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
280 otherwise NOT A KIND *)
282 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
285 let rec skip_args status ~metasenv context =
288 | [],_ -> assert false (* IMPOSSIBLE *)
289 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
291 match classify status ~metasenv context arg with
294 | `Term `TypeFormer ->
295 Some arg::skip_args status ~metasenv context (tl1,tl2)
298 | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
299 | `Term _ -> assert false (* IMPOSSIBLE *)
302 class type g_status =
304 method extraction_db: db
307 class virtual status =
310 val extraction_db = ReferenceMap.empty, GlobalNames.empty
311 method extraction_db = extraction_db
312 method set_extraction_db v = {< extraction_db = v >}
313 method set_extraction_status
314 : 'status. #g_status as 'status -> 'self
315 = fun o -> {< extraction_db = o#extraction_db >}
318 let rec split_kind_prods context =
320 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
321 | KSkip ta -> split_kind_prods (None::context) ta
322 | Type -> context,Type
325 let rec split_typ_prods context =
327 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
328 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
329 | TSkip ta -> split_typ_prods (None::context) ta
330 | _ as t -> context,t
333 let rec glue_ctx_typ ctx typ =
336 | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
337 | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
338 | None::ctx -> glue_ctx_typ ctx (TSkip typ)
341 let rec split_typ_lambdas status n ~metasenv context typ =
342 if n = 0 then context,typ
344 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
345 | NCic.Lambda (name,s,t) ->
346 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
348 (* eta-expansion required *)
349 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
350 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
351 | NCic.Prod (name,typ,_) ->
352 split_typ_lambdas status (n-1) ~metasenv
353 ((name,NCic.Decl typ)::context)
354 (NCicUntrusted.mk_appl t [NCic.Rel 1])
355 | _ -> assert false (* IMPOSSIBLE *)
359 let rev_context_of_typformer status ~metasenv context =
361 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
362 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
363 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
364 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
366 match snd (ReferenceMap.find ref (fst status#extraction_db)) with
367 `Type (ctx,_) -> List.rev ctx
369 | `Function -> assert false
372 (* This can happen only when we are processing the type of
373 the constructor of a small singleton type. In this case
374 we are not interested in all the type, but only in its
375 backbone. That is why we can safely return the dummy context
377 let rec dummy = None::dummy in
379 | NCic.Match _ -> assert false (* TODO ???? *)
382 match List.nth context (n-1) with
383 _,NCic.Decl typ -> typ
384 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
385 let typ_ctx = snd (HExtlib.split_nth n context) in
386 let typ = kind_of status ~metasenv typ_ctx typ in
387 List.rev (fst (split_kind_prods [] typ))
388 | NCic.Meta _ -> assert false (* TODO *)
389 | NCic.Const (NReference.Ref (_,NReference.Con _))
390 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
391 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
392 | NCic.Appl _ | NCic.Prod _ ->
393 assert false (* IMPOSSIBLE *)
395 let rec typ_of status ~metasenv context k =
396 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
397 | NCic.Prod (b,s,t) ->
398 (* CSC: non-invariant assumed here about "_" *)
399 (match classify status ~metasenv context s with
401 Forall (b, kind_of status ~metasenv context s,
402 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
404 | `KindOrType -> (* ??? *)
405 Arrow (typ_of status ~metasenv context s,
406 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
409 TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
410 | `Term _ -> assert false (* IMPOSSIBLE *))
413 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
414 | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
415 | NCic.Rel n -> Var n
416 | NCic.Const ref -> TConst ref
417 | NCic.Match (_,_,_,_)
418 | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) ->
420 | NCic.Appl (he::args) ->
421 let rev_he_context= rev_context_of_typformer status ~metasenv context he in
422 TAppl (typ_of status ~metasenv context he ::
424 (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
425 (skip_args status ~metasenv context (rev_he_context,args)))
426 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
427 otherwise NOT A TYPE *)
428 | NCic.Meta _ -> assert false (*TODO*)
431 let rec fomega_lift_type_from n k =
433 | Var m as t -> if m < k then t else Var (m + n)
437 | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
438 | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
439 | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
440 | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
442 let fomega_lift_type n t =
443 if n = 0 then t else fomega_lift_type_from n 0 t
445 let fomega_lift_term n t =
446 let rec fomega_lift_term n k =
448 | Rel m as t -> if m < k then t else Rel (m + n)
452 | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
453 | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
454 | Appl args -> Appl (List.map (fomega_lift_term n k) args)
455 | LetIn (name,m,bo) ->
456 LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
457 | Match (ref,t,pl) ->
459 let lift_context ctx =
460 let len = List.length ctx in
463 let j = len - i - 1 in
466 | Some (_,`OfKind _) as el -> el
467 | Some (name,`OfType t) ->
468 Some (name,`OfType (fomega_lift_type_from n (k+j) t))
471 lift_context ctx, fomega_lift_term n (k + List.length ctx) t
473 Match (ref,fomega_lift_term n k t,List.map lift_p pl)
474 | Inst t -> Inst (fomega_lift_term n k t)
475 | Skip t -> Skip (fomega_lift_term n (k+1) t)
476 | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
478 if n = 0 then t else fomega_lift_term n 0 t
481 let rec fomega_subst k t1 =
484 if k=n then fomega_lift_type k t1
485 else if n < k then Var n
488 | TConst ref -> TConst ref
490 | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
491 | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
492 | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
493 | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
495 let fomega_lookup status ref =
497 match snd (ReferenceMap.find ref (fst status#extraction_db)) with
500 | `Function -> assert false
503 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); None
505 let rec fomega_whd status ty =
508 (match fomega_lookup status r with
510 | Some ty -> fomega_whd status ty)
511 | TAppl (TConst r::args) ->
512 (match fomega_lookup status r with
514 | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
517 let rec term_of status ~metasenv context =
521 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
522 | NCic.Lambda (b,ty,bo) ->
523 (* CSC: non-invariant assumed here about "_" *)
524 (match classify status ~metasenv context ty with
526 TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
527 | `KindOrType (* ??? *)
529 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
533 Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
534 | `Term _ -> assert false (* IMPOSSIBLE *))
535 | NCic.LetIn (b,ty,t,bo) ->
536 (match classify status ~metasenv context t with
537 | `Term `TypeFormerOrTerm (* ???? *)
539 LetIn (b,term_of status ~metasenv context t,
540 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
549 (* not in programming languages, we expand it *)
550 term_of status ~metasenv context
551 (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
552 | NCic.Rel n -> Rel n
553 | NCic.Const ref -> Const ref
554 | NCic.Appl (he::args) ->
555 eat_args status metasenv
556 (term_of status ~metasenv context he) context
557 (*BUG: recomputing every time the type of the head*)
558 (typ_of status ~metasenv context
559 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
561 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
562 otherwise NOT A TYPE *)
563 | NCic.Meta _ -> assert false (* TODO *)
564 | NCic.Match (ref,_,t,pl) ->
566 let constructors, leftno =
567 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
568 let _,_,_,cl = List.nth tys n in
571 let rec eat_branch n ty context ctx pat =
575 | Arrow (_, t), _ when n > 0 ->
576 eat_branch (pred n) t context ctx pat
577 | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
578 (*CSC: unify the three cases below? *)
579 | Arrow (_, t), NCic.Lambda (name, ty, t') ->
581 (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
582 let context = (name,NCic.Decl ty)::context in
583 eat_branch 0 t context ctx t'
584 | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
586 (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
587 let context = (name,NCic.Decl ty)::context in
588 eat_branch 0 t context ctx t'
589 | TSkip t,NCic.Lambda (name, ty, t') ->
590 let ctx = None::ctx in
591 let context = (name,NCic.Decl ty)::context in
592 eat_branch 0 t context ctx t'
593 | Top,_ -> assert false (* IMPOSSIBLE *)
596 | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
597 | _, _ -> context,ctx, pat
601 (fun (_, _name, ty) pat ->
602 (*BUG: recomputing every time the type of the constructor*)
603 let ty = typ_of status ~metasenv context ty in
604 let context,lhs,rhs = eat_branch leftno ty context [] pat in
606 (* UnsafeCoerce not always required *)
607 UnsafeCoerce (term_of status ~metasenv context rhs)
611 with Invalid_argument _ -> assert false
613 (match classify_not_term status [] (NCic.Const ref) with
616 | `Kind -> assert false (* IMPOSSIBLE *)
618 (match patterns_of pl with
620 | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
623 Match (ref,term_of status ~metasenv context t, patterns_of pl))
624 and eat_args status metasenv acc context tyhe =
628 match fomega_whd status tyhe with
633 | _ -> term_of status ~metasenv context arg in
634 eat_args status metasenv (mk_appl acc arg) context t tl
637 match classify status ~metasenv context arg with
646 | `Term `TypeFormerOrTerm
647 | `Term `Term -> term_of status ~metasenv context arg
649 eat_args status metasenv
650 (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
653 (match classify status ~metasenv context arg with
654 | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
658 eat_args status metasenv (UnsafeCoerce (Inst acc))
659 context (fomega_subst 1 Unit t) tl
660 | `Term _ -> assert false (*TODO: ????*)
663 eat_args status metasenv (Inst acc)
664 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
667 eat_args status metasenv acc context t tl
668 | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
678 let fresh_name_of_ref status ref =
679 let candidate = NCicPp.r2s status true ref in
680 let rec freshen candidate =
681 if GlobalNames.mem candidate (snd status#extraction_db) then
682 freshen (candidate ^ "'")
688 let register_info (db,names) (ref,(name,_ as info_el)) =
689 ReferenceMap.add ref info_el db,GlobalNames.add name names
691 let register_name_and_info status (ref,info_el) =
692 let name = fresh_name_of_ref status ref in
693 let info = ref,(name,info_el) in
694 let infos,names = status#extraction_db in
695 status#set_extraction_db (register_info (infos,names) info), info
697 let register_infos = List.fold_left register_info
699 let object_of_constant status ~metasenv ref bo ty =
700 match classify status ~metasenv [] ty with
702 let ty = kind_of status ~metasenv [] ty in
703 let ctx0,res = split_kind_prods [] ty in
705 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
706 (match classify status ~metasenv ctx bo with
708 | `KindOrType -> (* ?? no kind formers in System F_omega *)
712 HExtlib.map_option (fun (_,k) ->
713 (*CSC: BUG here, clashes*)
714 String.uncapitalize (fst n),k) p1)
717 let bo = typ_of status ~metasenv ctx bo in
718 let info = ref,`Type (nicectx,Some bo) in
719 let status,info = register_name_and_info status info in
720 status,Success ([info],ref,TypeDefinition((nicectx,res),bo))
721 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
723 | `Proposition -> status, Erased
724 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
726 | `Proposition -> status, Erased
727 | `KindOrType (* ??? *)
729 let ty = typ_of status ~metasenv [] ty in
730 let info = ref,`Function in
731 let status,info = register_name_and_info status info in
733 Success ([info],ref, TermDefinition (split_typ_prods [] ty,
734 term_of status ~metasenv [] bo))
735 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
738 let object_of_inductive status ~metasenv uri ind leftno il =
739 let status,_,rev_tyl =
741 (fun (status,i,res) (_,_,arity,cl) ->
742 match classify_not_term status [] arity with
745 | `Type -> assert false (* IMPOSSIBLE *)
746 | `PropKind -> status,i+1,res
748 let arity = kind_of status ~metasenv [] arity in
749 let ctx,_ = split_kind_prods [] arity in
750 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
752 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
753 let info = ref,`Type (ctx,None) in
754 let status,info = register_name_and_info status info in
755 let _,status,cl_rev,infos =
757 (fun (j,status,res,infos) (_,_,ty) ->
759 NCicReduction.split_prods status ~subst:[] [] leftno ty in
760 let ty = typ_of status ~metasenv ctx ty in
761 let ref = NReference.mk_constructor j ref in
762 let info = ref,`Constructor in
763 let status,info = register_name_and_info status info in
764 j+1,status,((ref,ty)::res),info::infos
765 ) (1,status,[],[]) cl
767 status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
772 | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
775 let object_of status (uri,height,metasenv,subst,obj_kind) =
776 let obj_kind = apply_subst subst obj_kind in
778 | NCic.Constant (_,_,None,ty,_) ->
779 let ref = NReference.reference_of_spec uri NReference.Decl in
780 (match classify status ~metasenv [] ty with
782 let ty = kind_of status ~metasenv [] ty in
783 let ctx,_ as res = split_kind_prods [] ty in
784 let info = ref,`Type (ctx,None) in
785 let status,info = register_name_and_info status info in
786 status, Success ([info],ref, TypeDeclaration res)
788 | `Proposition -> status, Erased
790 | `KindOrType (*???*) ->
791 let ty = typ_of status ~metasenv [] ty in
792 let info = ref,`Function in
793 let status,info = register_name_and_info status info in
794 status,Success ([info],ref,
795 TermDeclaration (split_typ_prods [] ty))
796 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
797 | NCic.Constant (_,_,Some bo,ty,_) ->
798 let ref = NReference.reference_of_spec uri (NReference.Def height) in
799 object_of_constant status ~metasenv ref bo ty
800 | NCic.Fixpoint (fix_or_cofix,fs,_) ->
803 (fun (_,_name,recno,ty,bo) (i,status,res) ->
806 NReference.reference_of_spec
807 uri (NReference.Fix (i,recno,height))
809 NReference.reference_of_spec uri (NReference.CoFix i)
811 let status,obj = object_of_constant ~metasenv status ref bo ty in
813 | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
814 | _ -> i+1,status, res) fs (0,status,[])
816 status, Success ([],dummyref,LetRec objs)
817 | NCic.Inductive (ind,leftno,il,_) ->
818 object_of_inductive status ~metasenv uri ind leftno il
820 (************************ HASKELL *************************)
822 (* -----------------------------------------------------------------------------
823 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
824 * -----------------------------------------------------------------------------
834 let uncurry f (x, y) =
838 let rec char_list_of_string s =
839 let l = String.length s in
840 let rec aux buffer s =
843 | m -> aux (s.[m - 1]::buffer) s (m - 1)
848 let string_of_char_list s =
852 | x::xs -> aux (String.make 1 x ^ buffer) xs
857 (* ----------------------------------------------------------------------------
858 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
859 * and type variable names.
860 * ----------------------------------------------------------------------------
863 let remove_underscores_and_mark l =
864 let rec aux char_list_buffer positions_buffer position =
866 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
869 aux char_list_buffer (position::positions_buffer) position xs
871 aux (x::char_list_buffer) positions_buffer (position + 1) xs
873 if l = ['_'] then "_",[] else aux [] [] 0 l
876 let rec capitalize_marked_positions s =
880 if x < String.length s then
881 let c = Char.uppercase (String.get s x) in
882 let _ = String.set s x c in
883 capitalize_marked_positions s xs
885 capitalize_marked_positions s xs
888 let contract_underscores_and_capitalise =
889 char_list_of_string |>
890 remove_underscores_and_mark |>
891 uncurry capitalize_marked_positions
894 let idiomatic_haskell_type_name_of_string =
895 contract_underscores_and_capitalise |>
899 let idiomatic_haskell_term_name_of_string =
900 contract_underscores_and_capitalise |>
904 let classify_reference status ref =
906 match snd (ReferenceMap.find ref (fst status#extraction_db)) with
908 | `Constructor -> `Constructor
909 | `Function -> `FunctionName
912 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName
915 let capitalize classification name =
916 match classification with
918 | `TypeName -> idiomatic_haskell_type_name_of_string name
921 | `FunctionName -> idiomatic_haskell_term_name_of_string name
924 let pp_ref status ref =
925 capitalize (classify_reference status ref)
926 (try fst (ReferenceMap.find ref (fst status#extraction_db))
928 prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref);
930 NCicPp.r2s status true ref (* BUG: this should never happen *)
933 (* cons avoid duplicates *)
934 let rec (@:::) name l =
935 if name <> "" (* propositional things *) && name.[0] = '_' then
936 let name = String.sub name 1 (String.length name - 1) in
937 let name = if name = "" then "a" else name in
939 else if List.mem name l then (name ^ "'") @::: l
943 let (@::) x l = let x,l = x @::: l in x::l;;
945 let rec pretty_print_type status ctxt =
947 | Var n -> List.nth ctxt (n-1)
950 | TConst ref -> pp_ref status ref
952 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
953 pretty_print_type status ("_"::ctxt) t2
954 | TSkip t -> pretty_print_type status ("_"::ctxt) t
955 | Forall (name, kind, t) ->
956 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
957 let name = capitalize `TypeVariable name in
958 let name,ctxt = name@:::ctxt in
959 if size_of_kind kind > 1 then
960 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
962 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
963 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
965 let pretty_print_term_context status ctx1 ctx2 =
966 let name_context, rev_res =
968 (fun el (ctx1,rev_res) ->
970 None -> ""@::ctx1,rev_res
971 | Some (name,`OfKind _) ->
972 let name = capitalize `TypeVariable name in
974 | Some (name,`OfType typ) ->
975 let name = capitalize `TypeVariable name in
976 let name,ctx1 = name@:::ctx1 in
978 ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
980 name_context, String.concat " " (List.rev rev_res)
982 let rec pretty_print_term status ctxt =
984 | Rel n -> List.nth ctxt (n-1)
986 | Const ref -> pp_ref status ref
988 let name = capitalize `BoundVariable name in
989 let name,ctxt = name@:::ctxt in
990 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
991 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
992 | LetIn (name,s,t) ->
993 let name = capitalize `BoundVariable name in
994 let name,ctxt = name@:::ctxt in
995 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
996 pretty_print_term status (name::ctxt) t
998 "error \"Unreachable code\""
1000 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
1001 | Match (r,matched,pl) ->
1003 "error \"Case analysis over empty type\""
1005 "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
1006 String.concat " ;\n"
1008 (fun (bound_names,rhs) i ->
1009 let ref = NReference.mk_constructor (i+1) r in
1010 let name = pp_ref status ref in
1011 let ctxt,bound_names =
1012 pretty_print_term_context status ctxt bound_names in
1014 pretty_print_term status ctxt rhs
1016 " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
1018 | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
1019 | TLambda (name,t) ->
1020 let name = capitalize `TypeVariable name in
1021 pretty_print_term status (name@::ctxt) t
1022 | Inst t -> pretty_print_term status ctxt t
1025 let rec pp_obj status (_,ref,obj_kind) =
1026 let pretty_print_context ctx =
1027 String.concat " " (List.rev (snd
1029 (fun (x,kind) (l,res) ->
1030 let x,l = x @:::l in
1031 if size_of_kind kind > 1 then
1032 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
1035 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
1037 let namectx_of_ctx ctx =
1038 List.fold_right (@::)
1039 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
1041 TypeDeclaration (ctx,_) ->
1042 (* data?? unsure semantics: inductive type without constructor, but
1043 not matchable apparently *)
1044 if List.length ctx = 0 then
1045 "data " ^ pp_ref status ref
1047 "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1048 | TypeDefinition ((ctx, _),ty) ->
1049 let namectx = namectx_of_ctx ctx in
1050 if List.length ctx = 0 then
1051 "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1053 "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1054 | TermDeclaration (ctx,ty) ->
1055 let name = pp_ref status ref in
1056 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1057 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1058 | TermDefinition ((ctx,ty),bo) ->
1059 let name = pp_ref status ref in
1060 let namectx = namectx_of_ctx ctx in
1062 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1063 name ^ " = " ^ pretty_print_term status namectx bo
1065 String.concat "\n" (List.map (pp_obj status) l)
1069 (fun _,ref,left,right,cl ->
1070 "data " ^ pp_ref status ref ^ " " ^
1071 pretty_print_context (right@left) ^ " where\n " ^
1072 String.concat "\n " (List.map
1074 let namectx = namectx_of_ctx left in
1075 pp_ref status ref ^ " :: " ^
1076 pretty_print_type status namectx tys
1077 ) cl) ^ "\n deriving (Prelude.Show)"
1079 (* inductive and records missing *)
1081 let rec infos_of (info,_,obj_kind) =
1084 LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1085 | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1088 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1089 let status, obj = object_of status obj in
1092 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1093 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1094 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1095 | Success o -> pp_obj status o ^ "\n", infos_of o
1097 let refresh_uri_in_typ ~refresh_uri_in_reference =
1098 let rec refresh_uri_in_typ =
1103 | TConst r -> TConst (refresh_uri_in_reference r)
1104 | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1105 | TSkip t -> TSkip (refresh_uri_in_typ t)
1106 | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1107 | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1111 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1113 (function (ref,el) ->
1116 | _,`Function -> refresh_uri_in_reference ref,el
1117 | name,`Type (ctx,typ) ->
1121 | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1123 refresh_uri_in_reference ref, (name,`Type (ctx,typ)))