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 (*CSC: Patch while we wait for separate compilation *)
681 let name = NCicPp.r2s status true ref in
682 let NReference.Ref (uri,_) = ref in
683 let path = NUri.baseuri_of_uri uri in
684 let path = String.sub path 5 (String.length path - 5) in
685 let path = Str.global_replace (Str.regexp "/") "_" path in
688 let rec freshen candidate =
689 if GlobalNames.mem candidate (snd status#extraction_db) then
690 freshen (candidate ^ "'")
696 let register_info (db,names) (ref,(name,_ as info_el)) =
697 ReferenceMap.add ref info_el db,GlobalNames.add name names
699 let register_name_and_info status (ref,info_el) =
700 let name = fresh_name_of_ref status ref in
701 let info = ref,(name,info_el) in
702 let infos,names = status#extraction_db in
703 status#set_extraction_db (register_info (infos,names) info), info
705 let register_infos = List.fold_left register_info
707 let object_of_constant status ~metasenv ref bo ty =
708 match classify status ~metasenv [] ty with
710 let ty = kind_of status ~metasenv [] ty in
711 let ctx0,res = split_kind_prods [] ty in
713 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
714 (match classify status ~metasenv ctx bo with
716 | `KindOrType -> (* ?? no kind formers in System F_omega *)
720 HExtlib.map_option (fun (_,k) ->
721 (*CSC: BUG here, clashes*)
722 String.uncapitalize (fst n),k) p1)
725 let bo = typ_of status ~metasenv ctx bo in
726 let info = ref,`Type (nicectx,Some bo) in
727 let status,info = register_name_and_info status info in
728 status,Success ([info],ref,TypeDefinition((nicectx,res),bo))
729 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
731 | `Proposition -> status, Erased
732 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
734 | `Proposition -> status, Erased
735 | `KindOrType (* ??? *)
737 let ty = typ_of status ~metasenv [] ty in
738 let info = ref,`Function in
739 let status,info = register_name_and_info status info in
741 Success ([info],ref, TermDefinition (split_typ_prods [] ty,
742 term_of status ~metasenv [] bo))
743 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
746 let object_of_inductive status ~metasenv uri ind leftno il =
747 let status,_,rev_tyl =
749 (fun (status,i,res) (_,_,arity,cl) ->
750 match classify_not_term status [] arity with
753 | `Type -> assert false (* IMPOSSIBLE *)
754 | `PropKind -> status,i+1,res
756 let arity = kind_of status ~metasenv [] arity in
757 let ctx,_ = split_kind_prods [] arity in
758 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
760 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
761 let info = ref,`Type (ctx,None) in
762 let status,info = register_name_and_info status info in
763 let _,status,cl_rev,infos =
765 (fun (j,status,res,infos) (_,_,ty) ->
767 NCicReduction.split_prods status ~subst:[] [] leftno ty in
768 let ty = typ_of status ~metasenv ctx ty in
769 let ref = NReference.mk_constructor j ref in
770 let info = ref,`Constructor in
771 let status,info = register_name_and_info status info in
772 j+1,status,((ref,ty)::res),info::infos
773 ) (1,status,[],[]) cl
775 status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
780 | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
783 let object_of status (uri,height,metasenv,subst,obj_kind) =
784 let obj_kind = apply_subst subst obj_kind in
786 | NCic.Constant (_,_,None,ty,_) ->
787 let ref = NReference.reference_of_spec uri NReference.Decl in
788 (match classify status ~metasenv [] ty with
790 let ty = kind_of status ~metasenv [] ty in
791 let ctx,_ as res = split_kind_prods [] ty in
792 let info = ref,`Type (ctx,None) in
793 let status,info = register_name_and_info status info in
794 status, Success ([info],ref, TypeDeclaration res)
796 | `Proposition -> status, Erased
798 | `KindOrType (*???*) ->
799 let ty = typ_of status ~metasenv [] ty in
800 let info = ref,`Function in
801 let status,info = register_name_and_info status info in
802 status,Success ([info],ref,
803 TermDeclaration (split_typ_prods [] ty))
804 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
805 | NCic.Constant (_,_,Some bo,ty,_) ->
806 let ref = NReference.reference_of_spec uri (NReference.Def height) in
807 object_of_constant status ~metasenv ref bo ty
808 | NCic.Fixpoint (fix_or_cofix,fs,_) ->
811 (fun (_,_name,recno,ty,bo) (i,status,res) ->
814 NReference.reference_of_spec
815 uri (NReference.Fix (i,recno,height))
817 NReference.reference_of_spec uri (NReference.CoFix i)
819 let status,obj = object_of_constant ~metasenv status ref bo ty in
821 | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
822 | _ -> i+1,status, res) fs (0,status,[])
824 status, Success ([],dummyref,LetRec objs)
825 | NCic.Inductive (ind,leftno,il,_) ->
826 object_of_inductive status ~metasenv uri ind leftno il
828 (************************ HASKELL *************************)
830 (* -----------------------------------------------------------------------------
831 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
832 * -----------------------------------------------------------------------------
842 let uncurry f (x, y) =
846 let rec char_list_of_string s =
847 let l = String.length s in
848 let rec aux buffer s =
851 | m -> aux (s.[m - 1]::buffer) s (m - 1)
856 let string_of_char_list s =
860 | x::xs -> aux (String.make 1 x ^ buffer) xs
865 (* ----------------------------------------------------------------------------
866 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
867 * and type variable names.
868 * ----------------------------------------------------------------------------
871 let remove_underscores_and_mark l =
872 let rec aux char_list_buffer positions_buffer position =
874 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
877 aux char_list_buffer (position::positions_buffer) position xs
879 aux (x::char_list_buffer) positions_buffer (position + 1) xs
881 if l = ['_'] then "_",[] else aux [] [] 0 l
884 let rec capitalize_marked_positions s =
888 if x < String.length s then
889 let c = Char.uppercase (String.get s x) in
890 let _ = String.set s x c in
891 capitalize_marked_positions s xs
893 capitalize_marked_positions s xs
896 let contract_underscores_and_capitalise =
897 char_list_of_string |>
898 remove_underscores_and_mark |>
899 uncurry capitalize_marked_positions
902 let idiomatic_haskell_type_name_of_string =
903 contract_underscores_and_capitalise |>
907 let idiomatic_haskell_term_name_of_string =
908 contract_underscores_and_capitalise |>
912 let classify_reference status ref =
914 match snd (ReferenceMap.find ref (fst status#extraction_db)) with
916 | `Constructor -> `Constructor
917 | `Function -> `FunctionName
920 prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName
923 let capitalize classification name =
924 match classification with
926 | `TypeName -> idiomatic_haskell_type_name_of_string name
929 | `FunctionName -> idiomatic_haskell_term_name_of_string name
932 let pp_ref status ref =
933 capitalize (classify_reference status ref)
934 (try fst (ReferenceMap.find ref (fst status#extraction_db))
936 prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref);
938 NCicPp.r2s status true ref (* BUG: this should never happen *)
941 (* cons avoid duplicates *)
942 let rec (@:::) name l =
943 if name <> "" (* propositional things *) && name.[0] = '_' then
944 let name = String.sub name 1 (String.length name - 1) in
945 let name = if name = "" then "a" else name in
947 else if List.mem name l then (name ^ "'") @::: l
951 let (@::) x l = let x,l = x @::: l in x::l;;
953 let rec pretty_print_type status ctxt =
955 | Var n -> List.nth ctxt (n-1)
958 | TConst ref -> pp_ref status ref
960 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
961 pretty_print_type status ("_"::ctxt) t2
962 | TSkip t -> pretty_print_type status ("_"::ctxt) t
963 | Forall (name, kind, t) ->
964 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
965 let name = capitalize `TypeVariable name in
966 let name,ctxt = name@:::ctxt in
967 if size_of_kind kind > 1 then
968 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
970 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
971 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
973 let pretty_print_term_context status ctx1 ctx2 =
974 let name_context, rev_res =
976 (fun el (ctx1,rev_res) ->
978 None -> ""@::ctx1,rev_res
979 | Some (name,`OfKind _) ->
980 let name = capitalize `TypeVariable name in
982 | Some (name,`OfType typ) ->
983 let name = capitalize `TypeVariable name in
984 let name,ctx1 = name@:::ctx1 in
986 ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
988 name_context, String.concat " " (List.rev rev_res)
990 let rec pretty_print_term status ctxt =
992 | Rel n -> List.nth ctxt (n-1)
994 | Const ref -> pp_ref status ref
996 let name = capitalize `BoundVariable name in
997 let name,ctxt = name@:::ctxt in
998 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
999 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
1000 | LetIn (name,s,t) ->
1001 let name = capitalize `BoundVariable name in
1002 let name,ctxt = name@:::ctxt in
1003 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
1004 pretty_print_term status (name::ctxt) t
1006 "error \"Unreachable code\""
1008 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
1009 | Match (r,matched,pl) ->
1011 "error \"Case analysis over empty type\""
1013 "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
1014 String.concat " ;\n"
1016 (fun (bound_names,rhs) i ->
1017 let ref = NReference.mk_constructor (i+1) r in
1018 let name = pp_ref status ref in
1019 let ctxt,bound_names =
1020 pretty_print_term_context status ctxt bound_names in
1022 pretty_print_term status ctxt rhs
1024 " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
1026 | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
1027 | TLambda (name,t) ->
1028 let name = capitalize `TypeVariable name in
1029 pretty_print_term status (name@::ctxt) t
1030 | Inst t -> pretty_print_term status ctxt t
1033 let rec pp_obj status (_,ref,obj_kind) =
1034 let pretty_print_context ctx =
1035 String.concat " " (List.rev (snd
1037 (fun (x,kind) (l,res) ->
1038 let x,l = x @:::l in
1039 if size_of_kind kind > 1 then
1040 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
1043 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
1045 let namectx_of_ctx ctx =
1046 List.fold_right (@::)
1047 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
1049 TypeDeclaration (ctx,_) ->
1050 (* data?? unsure semantics: inductive type without constructor, but
1051 not matchable apparently *)
1052 if List.length ctx = 0 then
1053 "data " ^ pp_ref status ref
1055 "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1056 | TypeDefinition ((ctx, _),ty) ->
1057 let namectx = namectx_of_ctx ctx in
1058 if List.length ctx = 0 then
1059 "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1061 "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1062 | TermDeclaration (ctx,ty) ->
1063 let name = pp_ref status ref in
1064 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1065 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1066 | TermDefinition ((ctx,ty),bo) ->
1067 let name = pp_ref status ref in
1068 let namectx = namectx_of_ctx ctx in
1070 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1071 name ^ " = " ^ pretty_print_term status namectx bo
1073 String.concat "\n" (List.map (pp_obj status) l)
1077 (fun _,ref,left,right,cl ->
1078 "data " ^ pp_ref status ref ^ " " ^
1079 pretty_print_context (right@left) ^ " where\n " ^
1080 String.concat "\n " (List.map
1082 let namectx = namectx_of_ctx left in
1083 pp_ref status ref ^ " :: " ^
1084 pretty_print_type status namectx tys
1085 ) cl) ^ "\n deriving (Prelude.Show)"
1087 (* inductive and records missing *)
1089 let rec infos_of (info,_,obj_kind) =
1092 LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1093 | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1096 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1097 let status, obj = object_of status obj in
1100 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1101 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1102 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1103 | Success o -> pp_obj status o ^ "\n", infos_of o
1105 let refresh_uri_in_typ ~refresh_uri_in_reference =
1106 let rec refresh_uri_in_typ =
1111 | TConst r -> TConst (refresh_uri_in_reference r)
1112 | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1113 | TSkip t -> TSkip (refresh_uri_in_typ t)
1114 | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1115 | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1119 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1121 (function (ref,el) ->
1124 | _,`Function -> refresh_uri_in_reference ref,el
1125 | name,`Type (ctx,typ) ->
1129 | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1131 refresh_uri_in_reference ref, (name,`Type (ctx,typ)))