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 type info_el = typ_context * typ option
131 type info = (NReference.reference * info_el) list
132 type db = info_el ReferenceMap.t
136 let register_info db (ref,info) = ReferenceMap.add ref info db
138 let register_infos = List.fold_left register_info
141 TypeDeclaration of typ_former_decl
142 | TypeDefinition of typ_former_def
143 | TermDeclaration of term_former_decl
144 | TermDefinition of term_former_def
145 | LetRec of (info * NReference.reference * obj_kind) list
146 (* reference, left, right, constructors *)
147 | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
149 type obj = info * NReference.reference * obj_kind
151 (* For LetRec and Algebraic blocks *)
153 NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
155 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
157 let max_not_term t1 t2 =
160 | _,`KindOrType -> `KindOrType
166 | _,`PropKind -> `PropKind
167 | `Proposition,`Proposition -> `Proposition
169 let sup = List.fold_left max_not_term `Proposition
171 let rec classify_not_term status context t =
172 match NCicReduction.whd status ~subst:[] context t with
176 | NCic.Type [`CProp,_] -> `PropKind
177 | NCic.Type [`Type,_] -> `Kind
178 | NCic.Type _ -> assert false)
179 | NCic.Prod (b,s,t) ->
180 (*CSC: using invariant on "_" *)
181 classify_not_term status ((b,NCic.Decl s)::context) t
184 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
186 assert false (* NOT POSSIBLE *)
187 | NCic.Lambda (n,s,t) ->
188 (* Lambdas can me met in branches of matches, expecially when the
189 output type is a product *)
190 classify_not_term status ((n,NCic.Decl s)::context) t
191 | NCic.Match (_,_,_,pl) ->
192 let classified_pl = List.map (classify_not_term status context) pl in
194 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
195 assert false (* IMPOSSIBLE *)
196 | NCic.Meta _ -> assert false (* TODO *)
197 | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)->
198 let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
199 let _,_,_,_,bo = List.nth l i in
200 classify_not_term status [] bo
201 | NCic.Appl (he::_) -> classify_not_term status context he
203 let rec find_sort typ =
204 match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
205 NCic.Sort NCic.Prop -> `Proposition
206 | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
207 | NCic.Sort (NCic.Type [`Type,_]) ->
208 (*CSC: we could be more precise distinguishing the user provided
209 minimal elements of the hierarchies and classify these
212 | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
213 | NCic.Prod (_,_,t) ->
214 (* we skipped arguments of applications, so here we need to skip
217 | _ -> assert false (* NOT A SORT *)
219 (match List.nth context (n-1) with
220 _,NCic.Decl typ -> find_sort typ
221 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
222 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
223 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
224 (match classify_not_term status [] ty with
226 | `Type -> assert false (* IMPOSSIBLE *)
228 | `KindOrType -> `Type
229 | `PropKind -> `Proposition)
230 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
231 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
232 let _,_,arity,_ = List.nth ityl i in
233 (match classify_not_term status [] arity with
236 | `KindOrType -> assert false (* IMPOSSIBLE *)
238 | `PropKind -> `Proposition)
239 | NCic.Const (NReference.Ref (_,NReference.Con _))
240 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
241 assert false (* IMPOSSIBLE *)
244 let classify status ~metasenv context t =
245 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
247 (classify_not_term status context t : not_term :> [> not_term])
249 let ty = fix_sorts ty in
251 (match classify_not_term status context ty with
252 | `Proposition -> `Proof
254 | `KindOrType -> `TypeFormerOrTerm
255 | `Kind -> `TypeFormer
256 | `PropKind -> `PropFormer)
260 let rec kind_of status ~metasenv context k =
261 match NCicReduction.whd status ~subst:[] context k with
262 | NCic.Sort NCic.Type _ -> Type
263 | NCic.Sort _ -> assert false (* NOT A KIND *)
264 | NCic.Prod (b,s,t) ->
265 (match classify status ~metasenv context s with
267 KArrow (kind_of status ~metasenv context s,
268 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
273 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
274 | `Term _ -> assert false (* IMPOSSIBLE *))
276 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
279 | NCic.Const _ -> assert false (* NOT A KIND *)
280 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
281 otherwise NOT A KIND *)
283 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
286 let rec skip_args status ~metasenv context =
289 | [],_ -> assert false (* IMPOSSIBLE *)
290 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
292 match classify status ~metasenv context arg with
295 | `Term `TypeFormer ->
296 Some arg::skip_args status ~metasenv context (tl1,tl2)
299 | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
300 | `Term _ -> assert false (* IMPOSSIBLE *)
303 class type g_status =
305 method extraction_db: db
308 class virtual status =
311 val extraction_db = ReferenceMap.empty
312 method extraction_db = extraction_db
313 method set_extraction_db v = {< extraction_db = v >}
314 method set_extraction_status
315 : 'status. #g_status as 'status -> 'self
316 = fun o -> {< extraction_db = o#extraction_db >}
319 let rec split_kind_prods context =
321 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
322 | KSkip ta -> split_kind_prods (None::context) ta
323 | Type -> context,Type
326 let rec split_typ_prods context =
328 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
329 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
330 | TSkip ta -> split_typ_prods (None::context) ta
331 | _ as t -> context,t
334 let rec glue_ctx_typ ctx typ =
337 | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
338 | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
339 | None::ctx -> glue_ctx_typ ctx (TSkip typ)
342 let rec split_typ_lambdas status n ~metasenv context typ =
343 if n = 0 then context,typ
345 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
346 | NCic.Lambda (name,s,t) ->
347 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
349 (* eta-expansion required *)
350 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
351 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
352 | NCic.Prod (name,typ,_) ->
353 split_typ_lambdas status (n-1) ~metasenv
354 ((name,NCic.Decl typ)::context)
355 (NCicUntrusted.mk_appl t [NCic.Rel 1])
356 | _ -> assert false (* IMPOSSIBLE *)
360 let rev_context_of_typformer status ~metasenv context =
362 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
363 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
364 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
365 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
366 (try List.rev (fst (ReferenceMap.find ref status#extraction_db))
369 (* This can happen only when we are processing the type of
370 the constructor of a small singleton type. In this case
371 we are not interested in all the type, but only in its
372 backbone. That is why we can safely return the dummy context here *)
373 let rec dummy = None::dummy in
375 | NCic.Match _ -> assert false (* TODO ???? *)
378 match List.nth context (n-1) with
379 _,NCic.Decl typ -> typ
380 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
381 let typ_ctx = snd (HExtlib.split_nth n context) in
382 let typ = kind_of status ~metasenv typ_ctx typ in
383 List.rev (fst (split_kind_prods [] typ))
384 | NCic.Meta _ -> assert false (* TODO *)
385 | NCic.Const (NReference.Ref (_,NReference.Con _))
386 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
387 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
388 | NCic.Appl _ | NCic.Prod _ ->
389 assert false (* IMPOSSIBLE *)
391 let rec typ_of status ~metasenv context k =
392 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
393 | NCic.Prod (b,s,t) ->
394 (* CSC: non-invariant assumed here about "_" *)
395 (match classify status ~metasenv context s with
397 Forall (b, kind_of status ~metasenv context s,
398 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
400 | `KindOrType -> (* ??? *)
401 Arrow (typ_of status ~metasenv context s,
402 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
405 TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
406 | `Term _ -> assert false (* IMPOSSIBLE *))
409 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
410 | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
411 | NCic.Rel n -> Var n
412 | NCic.Const ref -> TConst ref
413 | NCic.Match (_,_,_,_)
414 | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) ->
416 | NCic.Appl (he::args) ->
417 let rev_he_context= rev_context_of_typformer status ~metasenv context he in
418 TAppl (typ_of status ~metasenv context he ::
420 (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
421 (skip_args status ~metasenv context (rev_he_context,args)))
422 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
423 otherwise NOT A TYPE *)
424 | NCic.Meta _ -> assert false (*TODO*)
427 let rec fomega_lift_type_from n k =
429 | Var m as t -> if m < k then t else Var (m + n)
433 | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
434 | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
435 | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
436 | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
438 let fomega_lift_type n t =
439 if n = 0 then t else fomega_lift_type_from n 0 t
441 let fomega_lift_term n t =
442 let rec fomega_lift_term n k =
444 | Rel m as t -> if m < k then t else Rel (m + n)
448 | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
449 | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
450 | Appl args -> Appl (List.map (fomega_lift_term n k) args)
451 | LetIn (name,m,bo) ->
452 LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
453 | Match (ref,t,pl) ->
455 let lift_context ctx =
456 let len = List.length ctx in
459 let j = len - i - 1 in
462 | Some (_,`OfKind _) as el -> el
463 | Some (name,`OfType t) ->
464 Some (name,`OfType (fomega_lift_type_from n (k+j) t))
467 lift_context ctx, fomega_lift_term n (k + List.length ctx) t
469 Match (ref,fomega_lift_term n k t,List.map lift_p pl)
470 | Inst t -> Inst (fomega_lift_term n k t)
471 | Skip t -> Skip (fomega_lift_term n (k+1) t)
472 | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
474 if n = 0 then t else fomega_lift_term n 0 t
477 let rec fomega_subst k t1 =
480 if k=n then fomega_lift_type k t1
481 else if n < k then Var n
484 | TConst ref -> TConst ref
486 | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
487 | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
488 | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
489 | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
491 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
493 let rec fomega_whd status ty =
496 (match fomega_lookup status r with
498 | Some ty -> fomega_whd status ty)
499 | TAppl (TConst r::args) ->
500 (match fomega_lookup status r with
502 | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
505 let rec term_of status ~metasenv context =
509 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
510 | NCic.Lambda (b,ty,bo) ->
511 (* CSC: non-invariant assumed here about "_" *)
512 (match classify status ~metasenv context ty with
514 TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
515 | `KindOrType (* ??? *)
517 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
521 Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
522 | `Term _ -> assert false (* IMPOSSIBLE *))
523 | NCic.LetIn (b,ty,t,bo) ->
524 (match classify status ~metasenv context t with
525 | `Term `TypeFormerOrTerm (* ???? *)
527 LetIn (b,term_of status ~metasenv context t,
528 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
537 (* not in programming languages, we expand it *)
538 term_of status ~metasenv context
539 (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
540 | NCic.Rel n -> Rel n
541 | NCic.Const ref -> Const ref
542 | NCic.Appl (he::args) ->
543 eat_args status metasenv
544 (term_of status ~metasenv context he) context
545 (*BUG: recomputing every time the type of the head*)
546 (typ_of status ~metasenv context
547 (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
549 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
550 otherwise NOT A TYPE *)
551 | NCic.Meta _ -> assert false (* TODO *)
552 | NCic.Match (ref,_,t,pl) ->
554 let constructors, leftno =
555 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in
556 let _,_,_,cl = List.nth tys n in
559 let rec eat_branch n ty context ctx pat =
563 | Arrow (_, t), _ when n > 0 ->
564 eat_branch (pred n) t context ctx pat
565 | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
566 (*CSC: unify the three cases below? *)
567 | Arrow (_, t), NCic.Lambda (name, ty, t') ->
569 (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
570 let context = (name,NCic.Decl ty)::context in
571 eat_branch 0 t context ctx t'
572 | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
574 (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
575 let context = (name,NCic.Decl ty)::context in
576 eat_branch 0 t context ctx t'
577 | TSkip t,NCic.Lambda (name, ty, t') ->
578 let ctx = None::ctx in
579 let context = (name,NCic.Decl ty)::context in
580 eat_branch 0 t context ctx t'
581 | Top,_ -> assert false (* IMPOSSIBLE *)
584 | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
585 | _, _ -> context,ctx, pat
589 (fun (_, _name, ty) pat ->
590 (*BUG: recomputing every time the type of the constructor*)
591 let ty = typ_of status ~metasenv context ty in
592 let context,lhs,rhs = eat_branch leftno ty context [] pat in
594 (* UnsafeCoerce not always required *)
595 UnsafeCoerce (term_of status ~metasenv context rhs)
599 with Invalid_argument _ -> assert false
601 (match classify_not_term status [] (NCic.Const ref) with
604 | `Kind -> assert false (* IMPOSSIBLE *)
606 (match patterns_of pl with
608 | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
611 Match (ref,term_of status ~metasenv context t, patterns_of pl))
612 and eat_args status metasenv acc context tyhe =
616 match fomega_whd status tyhe with
621 | _ -> term_of status ~metasenv context arg in
622 eat_args status metasenv (mk_appl acc arg) context t tl
625 match classify status ~metasenv context arg with
634 | `Term `TypeFormerOrTerm
635 | `Term `Term -> term_of status ~metasenv context arg
637 eat_args status metasenv
638 (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
641 (match classify status ~metasenv context arg with
642 | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
646 eat_args status metasenv (UnsafeCoerce (Inst acc))
647 context (fomega_subst 1 Unit t) tl
648 | `Term _ -> assert false (*TODO: ????*)
651 eat_args status metasenv (Inst acc)
652 context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
655 eat_args status metasenv acc context t tl
656 | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
666 let object_of_constant status ~metasenv ref bo ty =
667 match classify status ~metasenv [] ty with
669 let ty = kind_of status ~metasenv [] ty in
670 let ctx0,res = split_kind_prods [] ty in
672 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
673 (match classify status ~metasenv ctx bo with
675 | `KindOrType -> (* ?? no kind formers in System F_omega *)
679 HExtlib.map_option (fun (_,k) ->
680 (*CSC: BUG here, clashes*)
681 String.uncapitalize (fst n),k) p1)
684 let bo = typ_of status ~metasenv ctx bo in
685 let info = ref,(nicectx,Some bo) in
686 status#set_extraction_db
687 (register_info status#extraction_db info),
688 Success ([info],ref,TypeDefinition((nicectx,res),bo))
689 | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
691 | `Proposition -> status, Erased
692 | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
694 | `Proposition -> status, Erased
695 | `KindOrType (* ??? *)
697 (* CSC: TO BE FINISHED, REF NON REGISTERED *)
698 let ty = typ_of status ~metasenv [] ty in
700 Success ([],ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
701 | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
704 let object_of_inductive status ~metasenv uri ind leftno il =
705 let status,_,rev_tyl =
707 (fun (status,i,res) (_,_,arity,cl) ->
708 match classify_not_term status [] arity with
711 | `Type -> assert false (* IMPOSSIBLE *)
712 | `PropKind -> status,i+1,res
714 let arity = kind_of status ~metasenv [] arity in
715 let ctx,_ = split_kind_prods [] arity in
716 let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
718 NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
719 let info = ref,(ctx,None) in
721 status#set_extraction_db
722 (register_info status#extraction_db info) in
727 NCicReduction.split_prods status ~subst:[] [] leftno ty in
728 let ty = typ_of status ~metasenv ctx ty in
729 NReference.mk_constructor (j+1) ref,ty
732 status,i+1,([info],ref,left,right,cl)::res
737 | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
740 let object_of status (uri,height,metasenv,subst,obj_kind) =
741 let obj_kind = apply_subst subst obj_kind in
743 | NCic.Constant (_,_,None,ty,_) ->
744 let ref = NReference.reference_of_spec uri NReference.Decl in
745 (match classify status ~metasenv [] ty with
747 let ty = kind_of status ~metasenv [] ty in
748 let ctx,_ as res = split_kind_prods [] ty in
749 let info = ref,(ctx,None) in
750 status#set_extraction_db
751 (register_info status#extraction_db info),
752 Success ([info],ref, TypeDeclaration res)
754 | `Proposition -> status, Erased
756 | `KindOrType (*???*) ->
757 let ty = typ_of status ~metasenv [] ty in
758 status, Success ([],ref, TermDeclaration (split_typ_prods [] ty))
759 | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
760 | NCic.Constant (_,_,Some bo,ty,_) ->
761 let ref = NReference.reference_of_spec uri (NReference.Def height) in
762 object_of_constant status ~metasenv ref bo ty
763 | NCic.Fixpoint (fix_or_cofix,fs,_) ->
766 (fun (_,_name,recno,ty,bo) (i,status,res) ->
769 NReference.reference_of_spec
770 uri (NReference.Fix (i,recno,height))
772 NReference.reference_of_spec uri (NReference.CoFix i)
774 let status,obj = object_of_constant ~metasenv status ref bo ty in
776 | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
777 | _ -> i+1,status, res) fs (0,status,[])
779 status, Success ([],dummyref,LetRec objs)
780 | NCic.Inductive (ind,leftno,il,_) ->
781 object_of_inductive status ~metasenv uri ind leftno il
783 (************************ HASKELL *************************)
785 (* -----------------------------------------------------------------------------
786 * Helper functions I can't seem to find anywhere in the OCaml stdlib?
787 * -----------------------------------------------------------------------------
797 let uncurry f (x, y) =
801 let rec char_list_of_string s =
802 let l = String.length s in
803 let rec aux buffer s =
806 | m -> aux (s.[m - 1]::buffer) s (m - 1)
811 let string_of_char_list s =
815 | x::xs -> aux (String.make 1 x ^ buffer) xs
820 (* ----------------------------------------------------------------------------
821 * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
822 * and type variable names.
823 * ----------------------------------------------------------------------------
826 let remove_underscores_and_mark =
827 let rec aux char_list_buffer positions_buffer position =
829 | [] -> (string_of_char_list char_list_buffer, positions_buffer)
832 aux char_list_buffer (position::positions_buffer) position xs
834 aux (x::char_list_buffer) positions_buffer (position + 1) xs
839 let rec capitalize_marked_positions s =
843 if x < String.length s then
844 let c = Char.uppercase (String.get s x) in
845 let _ = String.set s x c in
846 capitalize_marked_positions s xs
848 capitalize_marked_positions s xs
851 let contract_underscores_and_capitalise =
852 char_list_of_string |>
853 remove_underscores_and_mark |>
854 uncurry capitalize_marked_positions
857 let idiomatic_haskell_type_name_of_string =
858 contract_underscores_and_capitalise |>
862 let idiomatic_haskell_term_name_of_string =
863 contract_underscores_and_capitalise |>
867 (*CSC: code to be changed soon when we implement constructors and
868 we fix the code for term application *)
869 let classify_reference status ref =
870 if ReferenceMap.mem ref status#extraction_db then
873 let NReference.Ref (_,r) = ref in
875 NReference.Con _ -> `Constructor
876 | NReference.Ind _ -> assert false
880 let capitalize classification name =
881 match classification with
883 | `TypeName -> idiomatic_haskell_type_name_of_string name
886 | `FunctionName -> idiomatic_haskell_term_name_of_string name
889 let pp_ref status ref =
890 capitalize (classify_reference status ref)
891 (NCicPp.r2s status true ref)
893 (* cons avoid duplicates *)
894 let rec (@:::) name l =
895 if name <> "" (* propositional things *) && name.[0] = '_' then
896 let name = String.sub name 1 (String.length name - 1) in
897 let name = if name = "" then "a" else name in
899 else if List.mem name l then (name ^ "'") @::: l
903 let (@::) x l = let x,l = x @::: l in x::l;;
905 let rec pretty_print_type status ctxt =
907 | Var n -> List.nth ctxt (n-1)
910 | TConst ref -> pp_ref status ref
912 bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
913 pretty_print_type status ("_"::ctxt) t2
914 | TSkip t -> pretty_print_type status ("_"::ctxt) t
915 | Forall (name, kind, t) ->
916 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
917 let name = capitalize `TypeVariable name in
918 let name,ctxt = name@:::ctxt in
919 if size_of_kind kind > 1 then
920 "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
922 "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
923 | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
925 let pretty_print_term_context status ctx1 ctx2 =
926 let name_context, rev_res =
928 (fun el (ctx1,rev_res) ->
930 None -> ""@::ctx1,rev_res
931 | Some (name,`OfKind _) -> name@::ctx1,rev_res
932 | Some (name,`OfType typ) ->
933 let name,ctx1 = name@:::ctx1 in
935 ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
937 name_context, String.concat " " (List.rev rev_res)
939 let rec pretty_print_term status ctxt =
941 | Rel n -> List.nth ctxt (n-1)
943 | Const ref -> pp_ref status ref
945 let name = capitalize `BoundVariable name in
946 let name,ctxt = name@:::ctxt in
947 "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
948 | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
949 | LetIn (name,s,t) ->
950 let name = capitalize `BoundVariable name in
951 let name,ctxt = name@:::ctxt in
952 "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
953 pretty_print_term status (name::ctxt) t
955 "error \"Unreachable code\""
957 "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
958 | Match (r,matched,pl) ->
960 "error \"Case analysis over empty type\""
962 "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
965 (fun (bound_names,rhs) i ->
966 let ref = NReference.mk_constructor (i+1) r in
967 let name = pp_ref status ref in
968 let ctxt,bound_names =
969 pretty_print_term_context status ctxt bound_names in
971 pretty_print_term status ctxt rhs
973 " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
975 | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
976 | TLambda (name,t) ->
977 let name = capitalize `TypeVariable name in
978 pretty_print_term status (name@::ctxt) t
979 | Inst t -> pretty_print_term status ctxt t
982 let rec pp_obj status (_,ref,obj_kind) =
983 let pretty_print_context ctx =
984 String.concat " " (List.rev (snd
986 (fun (x,kind) (l,res) ->
988 if size_of_kind kind > 1 then
989 x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
992 (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
994 let namectx_of_ctx ctx =
995 List.fold_right (@::)
996 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
998 TypeDeclaration (ctx,_) ->
999 (* data?? unsure semantics: inductive type without constructor, but
1000 not matchable apparently *)
1001 if List.length ctx = 0 then
1002 "data " ^ pp_ref status ref
1004 "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
1005 | TypeDefinition ((ctx, _),ty) ->
1006 let namectx = namectx_of_ctx ctx in
1007 if List.length ctx = 0 then
1008 "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
1010 "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
1011 | TermDeclaration (ctx,ty) ->
1012 let name = pp_ref status ref in
1013 name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
1014 name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
1015 | TermDefinition ((ctx,ty),bo) ->
1016 let name = pp_ref status ref in
1017 let namectx = namectx_of_ctx ctx in
1019 name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
1020 name ^ " = " ^ pretty_print_term status namectx bo
1022 String.concat "\n" (List.map (pp_obj status) l)
1026 (fun _,ref,left,right,cl ->
1027 "data " ^ pp_ref status ref ^ " " ^
1028 pretty_print_context (right@left) ^ " where\n " ^
1029 String.concat "\n " (List.map
1031 let namectx = namectx_of_ctx left in
1032 pp_ref status ref ^ " :: " ^
1033 pretty_print_type status namectx tys
1036 (* inductive and records missing *)
1038 let rec infos_of (info,_,obj_kind) =
1041 LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
1042 | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
1045 let haskell_of_obj status (uri,_,_,_,_ as obj) =
1046 let status, obj = object_of status obj in
1049 Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
1050 | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
1051 | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
1052 | Success o -> pp_obj status o ^ "\n", infos_of o
1054 let refresh_uri_in_typ ~refresh_uri_in_reference =
1055 let rec refresh_uri_in_typ =
1060 | TConst r -> TConst (refresh_uri_in_reference r)
1061 | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
1062 | TSkip t -> TSkip (refresh_uri_in_typ t)
1063 | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
1064 | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
1068 let refresh_uri_in_info ~refresh_uri_in_reference infos =
1070 (function (ref,(ctx,typ)) ->
1074 | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
1076 refresh_uri_in_reference ref,(ctx,typ))