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 *)
42 | TConst of typformerreference
45 | Forall of string * kind * typ
51 | Lambda of string * (* typ **) term
53 | LetIn of string * (* typ **) term * term
54 | Match of reference * term * term list
55 | TLambda of (* string **) term
56 | Inst of (*typ_former **) term
59 NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
61 (* None = dropped abstraction *)
62 type typ_context = (string * kind) option list
63 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
65 type typ_former_decl = typ_context * kind
66 type typ_former_def = typ_former_decl * typ
68 type term_former_decl = term_context * typ
69 type term_former_def = term_former_decl * term
72 TypeDeclaration of typ_former_decl
73 | TypeDefinition of typ_former_def
74 | TermDeclaration of term_former_decl
75 | TermDefinition of term_former_def
76 | LetRec of (string * typ * term) list
77 (* inductive and records missing *)
79 type obj = NUri.uri * obj_kind
83 let rec classify_not_term status no_dep_prods context t =
84 match NCicReduction.whd status ~subst:[] context t with
88 | NCic.Type [`CProp,_] -> `PropKind
89 | NCic.Type [`Type,_] ->
90 if no_dep_prods then `Kind
92 raise NotInFOmega (* ?? *)
93 | NCic.Type _ -> assert false)
94 | NCic.Prod (b,s,t) ->
95 (*CSC: using invariant on "_" *)
96 classify_not_term status (no_dep_prods && b.[0] = '_')
97 ((b,NCic.Decl s)::context) t
101 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
102 | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
104 | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
105 (* be aware: we can be the head of an application *)
106 assert false (* TODO *)
107 | NCic.Meta _ -> assert false (* TODO *)
108 | NCic.Appl (he::_) -> classify_not_term status no_dep_prods context he
109 | NCic.Rel _ -> `KindOrType
110 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
111 let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
112 (match classify_not_term status true [] ty with
114 | `Type -> assert false (* IMPOSSIBLE *)
116 | `KindOrType -> `KindOrType
117 | `PropKind -> `Proposition)
118 | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
119 let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
120 let _,_,arity,_ = List.nth ityl i in
121 (match classify_not_term status true [] arity with
124 | `KindOrType -> assert false (* IMPOSSIBLE *)
126 | `PropKind -> `Proposition)
127 | NCic.Const (NReference.Ref (_,NReference.Con _))
128 | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
129 assert false (* IMPOSSIBLE *)
132 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
134 let classify status ~metasenv context t =
135 match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
137 (classify_not_term status true context t : not_term :> [> not_term])
139 let ty = fix_sorts ty in
141 (match classify_not_term status true context ty with
142 | `Proposition -> `Proof
144 | `KindOrType -> `TypeFormerOrTerm
145 | `Kind -> `TypeFormer
146 | `PropKind -> `PropFormer)
150 let rec kind_of status ~metasenv context k =
151 match NCicReduction.whd status ~subst:[] context k with
152 | NCic.Sort _ -> Type
153 | NCic.Prod (b,s,t) ->
154 (* CSC: non-invariant assumed here about "_" *)
155 (match classify status ~metasenv context s with
157 | `KindOrType -> (* KindOrType OK?? *)
158 KArrow (kind_of status ~metasenv context s,
159 kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
163 KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
164 | `Term _ -> assert false (* IMPOSSIBLE *))
166 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
169 | NCic.Const _ -> assert false (* NOT A KIND *)
170 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
171 otherwise NOT A KIND *)
173 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
176 let rec skip_args status ~metasenv context =
179 | [],_ -> assert false (* IMPOSSIBLE *)
180 | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
182 match classify status ~metasenv context arg with
185 | `Term `TypeFormer -> arg::skip_args status ~metasenv context (tl1,tl2)
188 | `PropKind -> unitty::skip_args status ~metasenv context (tl1,tl2)
189 | `Term _ -> assert false (* IMPOSSIBLE *)
192 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
194 type db = typ_context ReferenceMap.t
196 class type g_status =
198 method extraction_db: db
201 class virtual status =
204 val extraction_db = ReferenceMap.empty
205 method extraction_db = extraction_db
206 method set_extraction_db v = {< extraction_db = v >}
207 method set_extraction_status
208 : 'status. #g_status as 'status -> 'self
209 = fun o -> {< extraction_db = o#extraction_db >}
212 let rec split_kind_prods context =
214 | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
215 | KSkip ta -> split_kind_prods (None::context) ta
216 | Type -> context,Type
219 let rec split_typ_prods context =
221 | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
222 | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
223 | Skip ta -> split_typ_prods (None::context) ta
224 | _ as t -> context,t
227 let rec glue_ctx_typ ctx typ =
230 | Some (_,`OfType so)::ctx -> Arrow (so,glue_ctx_typ ctx typ)
231 | Some (name,`OfKind so)::ctx -> Forall (name,so,glue_ctx_typ ctx typ)
232 | None::ctx -> Skip (glue_ctx_typ ctx typ)
235 let rec split_typ_lambdas status n ~metasenv context typ =
236 if n = 0 then context,typ
238 match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
239 | NCic.Lambda (name,s,t) ->
240 split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
242 (* eta-expansion required *)
243 let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
244 match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
245 | NCic.Prod (name,typ,_) ->
246 split_typ_lambdas status (n-1) ~metasenv
247 ((name,NCic.Decl typ)::context)
248 (NCicUntrusted.mk_appl t [NCic.Rel 1])
249 | _ -> assert false (* IMPOSSIBLE *)
253 let context_of_typformer status ~metasenv context =
255 NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
256 | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
257 | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
258 | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
259 (try ReferenceMap.find ref status#extraction_db
261 Not_found -> assert false (* IMPOSSIBLE *))
262 | NCic.Match _ -> assert false (* TODO ???? *)
265 match List.nth context (n-1) with
266 _,NCic.Decl typ -> typ
267 | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
268 let typ_ctx = snd (HExtlib.split_nth n context) in
269 let typ = kind_of status ~metasenv typ_ctx typ in
270 fst (split_kind_prods [] typ)
271 | NCic.Meta _ -> assert false (* TODO *)
272 | NCic.Const (NReference.Ref (_,NReference.Con _))
273 | NCic.Const (NReference.Ref (_,NReference.CoFix _))
274 | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
275 | NCic.Appl _ | NCic.Prod _ ->
276 assert false (* IMPOSSIBLE *)
278 let rec typ_of status ~metasenv context k =
279 match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
280 | NCic.Prod (b,s,t) ->
281 (* CSC: non-invariant assumed here about "_" *)
282 (match classify status ~metasenv context s with
284 Forall (b, kind_of status ~metasenv context s,
285 typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
287 | `KindOrType -> (* ??? *)
288 Arrow (typ_of status ~metasenv context s,
289 typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
292 Skip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
293 | `Term _ -> assert false (* IMPOSSIBLE *))
296 | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
297 | NCic.Lambda _ -> assert false (* NOT A TYPE *)
298 | NCic.Rel n -> Var n
299 | NCic.Const ref -> TConst ref
300 | NCic.Appl (he::args) ->
301 let he_context = context_of_typformer status ~metasenv context he in
302 TAppl (typ_of status ~metasenv context he ::
303 List.map (typ_of status ~metasenv context)
304 (skip_args status ~metasenv context (List.rev he_context,args)))
305 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
306 otherwise NOT A TYPE *)
308 | NCic.Match (_,_,_,_) -> assert false (* TODO *)
311 let rec term_of status ~metasenv context =
315 | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
316 | NCic.Lambda (b,ty,bo) ->
317 (* CSC: non-invariant assumed here about "_" *)
318 (match classify status ~metasenv context ty with
320 TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
321 | `KindOrType (* ??? *)
323 Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
327 term_of status ~metasenv ((b,NCic.Decl ty)::context) bo
328 | `Term _ -> assert false (* IMPOSSIBLE *))
329 | NCic.LetIn (b,ty,t,bo) ->
330 (match classify status ~metasenv context t with
332 LetIn (b,term_of status ~metasenv context t,
333 term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
341 | `Term `TypeFormerOrTerm
342 | `Term `Proof -> assert false (* NOT IN PROGRAMMING LANGUAGES? EXPAND IT ??? *))
343 | NCic.Rel n -> Rel n
344 | NCic.Const ref -> Const ref
345 | NCic.Appl (he::args) ->
347 let he_context = context_of_typformer status ~metasenv context he in
348 TAppl (typ_of status ~metasenv context he ::
349 List.map (typ_of status ~metasenv context)
350 (skip_args status ~metasenv context (List.rev he_context,args)))*)
351 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
352 otherwise NOT A TYPE *)
353 | NCic.Meta _ -> assert false (* TODO *)
354 | NCic.Match (ref,_,t,pl) ->
355 Match (ref,term_of status ~metasenv context t,
356 List.map (term_of status ~metasenv context) pl)
359 let obj_of status (uri,height,metasenv,subst,obj_kind) =
360 let obj_kind = apply_subst subst obj_kind in
363 | NCic.Constant (_,_,None,ty,_) ->
364 (match classify status ~metasenv [] ty with
366 let ty = kind_of status ~metasenv [] ty in
367 let ctx,_ as res = split_kind_prods [] ty in
368 let ref = NReference.reference_of_spec uri NReference.Decl in
369 status#set_extraction_db
370 (ReferenceMap.add ref ctx status#extraction_db),
371 Some (uri, TypeDeclaration res)
372 | `KindOrType -> assert false (* TODO ??? *)
374 | `Proposition -> status, None
376 let ty = typ_of status ~metasenv [] ty in
378 Some (uri, TermDeclaration (split_typ_prods [] ty))
379 | `Term _ -> assert false (* IMPOSSIBLE *))
380 | NCic.Constant (_,_,Some bo,ty,_) ->
381 (match classify status ~metasenv [] ty with
383 let ty = kind_of status ~metasenv [] ty in
384 let ctx0,res = split_kind_prods [] ty in
386 split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
387 (match classify status ~metasenv ctx bo with
389 | `KindOrType -> (* ?? no kind formers in System F_omega *)
393 HExtlib.map_option (fun (_,k) ->
394 (*CSC: BUG here, clashes*)
395 String.uncapitalize (fst n),k) p1)
399 NReference.reference_of_spec uri (NReference.Def height) in
400 status#set_extraction_db
401 (ReferenceMap.add ref ctx0 status#extraction_db),
402 Some (uri,TypeDefinition((nicectx,res),typ_of status ~metasenv ctx bo))
403 | `Kind -> status, None
405 | `Proposition -> status, None
406 | `Term _ -> assert false (* IMPOSSIBLE *))
408 | `Proposition -> status, None
409 | `KindOrType (* ??? *)
411 (* CSC: TO BE FINISHED, REF NON REGISTERED *)
412 let ty = typ_of status ~metasenv [] ty in
414 Some (uri, TermDefinition (split_typ_prods [] ty,
415 term_of status ~metasenv [](* BAD! *) bo))
416 | `Term _ -> assert false (* IMPOSSIBLE *))
419 prerr_endline "NOT IN F_omega";
422 (************************ HASKELL *************************)
424 (*CSC: code to be changed soon when we implement constructors and
425 we fix the code for term application *)
426 let classify_reference status ref =
427 if ReferenceMap.mem ref status#extraction_db then
432 let capitalize classification name =
433 match classification with
435 | `TypeName -> String.capitalize name
436 | `FunctionName -> String.uncapitalize name
438 let pp_ref status ref =
439 capitalize (classify_reference status ref)
440 (NCicPp.r2s status false ref)
442 let name_of_uri classification uri =
443 capitalize classification (NUri.name_of_uri uri)
445 (* cons avoid duplicates *)
446 let rec (@::) name l =
447 if name <> "" (* propositional things *) && name.[0] = '_' then
448 let name = String.sub name 1 (String.length name - 1) in
449 let name = if name = "" then "a" else name in
451 else if List.mem name l then (name ^ "'") @:: l
458 | KArrow (k1,k2) -> "(" ^ pp_kind k1 ^ ") -> " ^ pp_kind k2
459 | KSkip k -> pp_kind k
461 let rec pp_typ status ctx =
463 Var n -> List.nth ctx (n-1)
464 | Top -> assert false (* ??? *)
465 | TConst ref -> pp_ref status ref
466 | Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2
467 | Skip t -> pp_typ status ("_"::ctx) t
468 | Forall (name,_,t) ->
469 (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
470 let name = String.uncapitalize name in
471 "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")"
472 | TAppl tl -> "(" ^ String.concat " " (List.map (pp_typ status ctx) tl) ^ ")"
474 let rec pp_term status ctx =
476 Rel n -> List.nth ctx (n-1)
477 | Const ref -> pp_ref status ref
478 | Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")"
479 | Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")"
480 | LetIn (name,s,t) ->
481 "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
483 | Match _ -> assert false (* TODO of reference * term * term list *)
484 | TLambda t -> pp_term status ctx t
485 | Inst t -> pp_term status ctx t
488 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
490 type term_former_def = term_context * term * typ
491 type term_former_decl = term_context * typ
494 let pp_obj status (uri,obj_kind) =
496 String.concat " " (List.rev
497 (List.fold_right (fun (x,_) l -> x@::l)
498 (HExtlib.filter_map (fun x -> x) ctx) [])) in
499 let namectx_of_ctx ctx =
500 List.fold_right (@::)
501 (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
503 TypeDeclaration (ctx,_) ->
504 (* data?? unsure semantics: inductive type without constructor, but
505 not matchable apparently *)
506 "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx
507 | TypeDefinition ((ctx,_),ty) ->
508 let namectx = namectx_of_ctx ctx in
509 "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
510 pp_typ status namectx ty
511 | TermDeclaration (ctx,ty) ->
512 (* Implemented with undefined, the best we can do *)
513 let name = name_of_uri `FunctionName uri in
514 name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
515 name ^ " = undefined"
516 | TermDefinition ((ctx,ty),bo) ->
517 let name = name_of_uri `FunctionName uri in
518 let namectx = namectx_of_ctx ctx in
519 name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
520 name ^ " = " ^ pp_term status namectx bo
521 | LetRec _ -> assert false (* TODO
522 (* inductive and records missing *)*)
524 let haskell_of_obj status obj =
525 let status, obj = obj_of status obj in
526 status,HExtlib.map_option (pp_obj status) obj
529 let rec typ_of context =
535 (match get_nth context n with
536 Some (C.Name s,_) -> ppid s
537 | Some (C.Anonymous,_) -> "__" ^ string_of_int n
538 | None -> "_hidden_" ^ string_of_int n
541 NotEnoughElements -> string_of_int (List.length context - n)
546 "?" ^ (string_of_int n) ^ "[" ^
551 | Some t -> pp ~in_type:false t context) l1) ^
555 let _,context,_ = CicUtil.lookup_meta n metasenv in
556 "?" ^ (string_of_int n) ^ "[" ^
564 | Some _, Some t -> pp ~in_type:false t context
568 CicUtil.Meta_not_found _
569 | Invalid_argument _ ->
570 "???" ^ (string_of_int n) ^ "[" ^
572 (List.rev_map (function None -> "_" | Some t ->
573 pp ~in_type:false t context) l1) ^
581 (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
582 | C.CProp _ -> "CProp"
584 | C.Implicit (Some `Hole) -> "%"
585 | C.Implicit _ -> "?"
587 (match b, is_term s with
588 _, true -> typ_of (None::context) t
589 | "_",_ -> Arrow (typ_of context s) (typ_of (Some b::context) t)
590 | _,_ -> Forall (b,typ_of (Some b::context) t)
591 | C.Lambda (b,s,t) ->
592 (match analyze_type context s with
594 | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
595 | `Optimize -> prerr_endline "XXX lambda";assert false
597 "(function " ^ ppname b ^ " -> " ^
598 pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
599 | C.LetIn (b,s,ty,t) ->
600 (match analyze_term context s with
602 | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
605 "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
606 " = " ^ pp ~in_type:false s context ^ " in " ^
607 pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
608 | C.Appl (he::tl) when in_type ->
609 let hes = pp ~in_type he context in
610 let stl = String.concat "," (clean_args_for_ty context tl) in
611 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
612 | C.Appl (C.MutInd _ as he::tl) ->
613 let hes = pp ~in_type he context in
614 let stl = String.concat "," (clean_args_for_ty context tl) in
615 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
616 | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
618 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
619 C.InductiveDefinition (_,_,nparams,_) -> nparams
620 | _ -> assert false in
621 let hes = pp ~in_type he context in
622 let stl = String.concat "," (clean_args_for_constr nparams context tl) in
623 "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
625 "(" ^ String.concat " " (clean_args context li) ^ ")"
626 | C.Const (uri,exp_named_subst) ->
627 qualified_name_of_uri status current_module_uri uri ^
628 pp_exp_named_subst exp_named_subst context
629 | C.MutInd (uri,n,exp_named_subst) ->
631 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
632 C.InductiveDefinition (dl,_,_,_) ->
633 let (name,_,_,_) = get_nth dl (n+1) in
634 qualified_name_of_uri status current_module_uri
635 (UriManager.uri_of_string
636 (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
637 pp_exp_named_subst exp_named_subst context
638 | _ -> raise CicExportationInternalError
640 Sys.Break as exn -> raise exn
641 | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
643 | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
645 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
646 C.InductiveDefinition (dl,_,_,_) ->
647 let _,_,_,cons = get_nth dl (n1+1) in
648 let id,_ = get_nth cons n2 in
649 qualified_name_of_uri status current_module_uri ~capitalize:true
650 (UriManager.uri_of_string
651 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
652 pp_exp_named_subst exp_named_subst context
653 | _ -> raise CicExportationInternalError
655 Sys.Break as exn -> raise exn
657 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
660 | C.MutCase (uri,n1,ty,te,patterns) ->
662 "unit (* TOO POLYMORPHIC TYPE *)"
664 let rec needs_obj_magic ty =
665 match CicReduction.whd context ty with
666 | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
667 | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
668 | _ -> false (* it can be a Rel, e.g. in *_rec *)
670 let needs_obj_magic = needs_obj_magic ty in
671 (match analyze_term context te with
672 `Type -> assert false
675 [] -> "assert false" (* empty type elimination *)
677 pp ~in_type:false he context (* singleton elimination *)
681 if patterns = [] then "assert false"
683 (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
684 (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
685 C.InductiveDefinition (dl,_,paramsno,_) ->
686 let (_,_,_,cons) = get_nth dl (n1+1) in
690 (* this is just an approximation since we do not have
692 let rec count_prods toskip =
694 C.Prod (_,_,bo) when toskip > 0 ->
695 count_prods (toskip - 1) bo
696 | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
699 qualified_name_of_uri status current_module_uri
701 (UriManager.uri_of_string
702 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
703 count_prods paramsno ty
706 if not (is_mcu_type uri) then rc, "","","",""
707 else rc, !current_go_up, "))", "( .< (", " ) >.)"
708 | _ -> raise CicExportationInternalError
711 let connames_and_argsno_and_patterns =
715 | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
716 | _,_ -> assert false
718 combine (connames_and_argsno,patterns)
721 "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^
722 (String.concat "\n | "
725 let rec aux argsno context =
727 Cic.Lambda (name,ty,bo) when argsno > 0 ->
730 Cic.Anonymous -> Cic.Anonymous
731 | Cic.Name n -> Cic.Name (ppid n) in
733 aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
736 (match analyze_type context ty with
737 | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
739 | `Sort _ -> args,res
743 | C.Name s -> s)::args,res)
744 | t when argsno = 0 -> [],pp ~in_type:false t context
746 ["{" ^ string_of_int argsno ^ " args missing}"],
747 pp ~in_type:false t context
750 if argsno = 0 then x,pp ~in_type:false y context
752 let args,body = aux argsno context y in
753 let sargs = String.concat "," args in
754 x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
757 pattern ^ " -> " ^ go_down ^
758 (if needs_obj_magic then
759 "Obj.magic (" ^ body ^ ")"
762 ) connames_and_argsno_and_patterns)) ^
764 | C.Fix (no, funs) ->
767 (fun (types,len) (n,_,ty,_) ->
768 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
774 (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
775 pp ~in_type:false bo (names@context) ^ i)
778 (match get_nth names (no + 1) with
779 Some (Cic.Name n,_) -> n
781 | C.CoFix (no,funs) ->
784 (fun (types,len) (n,ty,_) ->
785 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
791 (fun (name,ty,bo) i -> "\n" ^ name ^
792 " : " ^ pp ~in_type:true ty context ^ " := \n" ^
793 pp ~in_type:false bo (names@context) ^ i)
799 exception CicExportationInternalError;;
800 exception NotEnoughElements;;
805 UriManager.eq (UriManager.uri_of_string
806 "cic:/matita/freescale/opcode/mcu_type.ind") u
809 (* Utility functions *)
811 let analyze_term context t =
812 match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
813 | Cic.Sort _ -> `Type
814 | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
817 fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
819 | Cic.Sort Cic.Prop -> `Proof
823 let analyze_type context t =
826 Cic.Sort s -> `Sort s
827 | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
828 | Cic.Prod (_,_,t) -> aux t
829 | _ -> `SomethingElse
832 `Sort _ | `Optimize as res -> res
835 fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
837 Cic.Sort Cic.Prop -> `Statement
851 let n = String.uncapitalize n in
852 if List.mem n reserved then n ^ "_" else n
858 | Cic.Anonymous -> "_"
861 (* get_nth l n returns the nth element of the list l if it exists or *)
862 (* raises NotEnoughElements if l has less than n elements *)
863 let rec get_nth l n =
866 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
867 | (_,_) -> raise NotEnoughElements
870 let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
873 String.capitalize (UriManager.name_of_uri status uri)
875 ppid (UriManager.name_of_uri status uri) in
877 let suri = UriManager.buri_of_uri uri in
878 let s = String.sub suri 5 (String.length suri - 5) in
879 let s = Pcre.replace ~pat:"/" ~templ:"_" s in
880 String.uncapitalize s in
881 if current_module_uri = UriManager.buri_of_uri uri then
884 String.capitalize filename ^ "." ^ name
887 let current_go_up = ref "(.!(";;
890 current_go_up := "(.~(";
892 current_go_up := "(.!(";
895 current_go_up := "(.!(";
899 let pp current_module_uri ?metasenv ~in_type =
900 let rec pp ~in_type t context =
901 let module C = Cic in
906 (match get_nth context n with
907 Some (C.Name s,_) -> ppid s
908 | Some (C.Anonymous,_) -> "__" ^ string_of_int n
909 | None -> "_hidden_" ^ string_of_int n
912 NotEnoughElements -> string_of_int (List.length context - n)
914 | C.Var (uri,exp_named_subst) ->
915 qualified_name_of_uri status current_module_uri uri ^
916 pp_exp_named_subst exp_named_subst context
920 "?" ^ (string_of_int n) ^ "[" ^
925 | Some t -> pp ~in_type:false t context) l1) ^
929 let _,context,_ = CicUtil.lookup_meta n metasenv in
930 "?" ^ (string_of_int n) ^ "[" ^
938 | Some _, Some t -> pp ~in_type:false t context
942 CicUtil.Meta_not_found _
943 | Invalid_argument _ ->
944 "???" ^ (string_of_int n) ^ "[" ^
946 (List.rev_map (function None -> "_" | Some t ->
947 pp ~in_type:false t context) l1) ^
955 (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
956 | C.CProp _ -> "CProp"
958 | C.Implicit (Some `Hole) -> "%"
959 | C.Implicit _ -> "?"
963 let n = "'" ^ String.uncapitalize n in
964 "(" ^ pp ~in_type:true s context ^ " -> " ^
965 pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
967 "(" ^ pp ~in_type:true s context ^ " -> " ^
968 pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
969 | C.Cast (v,t) -> pp ~in_type v context
970 | C.Lambda (b,s,t) ->
971 (match analyze_type context s with
973 | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
974 | `Optimize -> prerr_endline "XXX lambda";assert false
976 "(function " ^ ppname b ^ " -> " ^
977 pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
978 | C.LetIn (b,s,ty,t) ->
979 (match analyze_term context s with
981 | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
984 "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
985 " = " ^ pp ~in_type:false s context ^ " in " ^
986 pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
987 | C.Appl (he::tl) when in_type ->
988 let hes = pp ~in_type he context in
989 let stl = String.concat "," (clean_args_for_ty context tl) in
990 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
991 | C.Appl (C.MutInd _ as he::tl) ->
992 let hes = pp ~in_type he context in
993 let stl = String.concat "," (clean_args_for_ty context tl) in
994 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
995 | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
997 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
998 C.InductiveDefinition (_,_,nparams,_) -> nparams
999 | _ -> assert false in
1000 let hes = pp ~in_type he context in
1001 let stl = String.concat "," (clean_args_for_constr nparams context tl) in
1002 "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
1004 "(" ^ String.concat " " (clean_args context li) ^ ")"
1005 | C.Const (uri,exp_named_subst) ->
1006 qualified_name_of_uri status current_module_uri uri ^
1007 pp_exp_named_subst exp_named_subst context
1008 | C.MutInd (uri,n,exp_named_subst) ->
1010 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1011 C.InductiveDefinition (dl,_,_,_) ->
1012 let (name,_,_,_) = get_nth dl (n+1) in
1013 qualified_name_of_uri status current_module_uri
1014 (UriManager.uri_of_string
1015 (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
1016 pp_exp_named_subst exp_named_subst context
1017 | _ -> raise CicExportationInternalError
1019 Sys.Break as exn -> raise exn
1020 | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
1022 | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
1024 match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1025 C.InductiveDefinition (dl,_,_,_) ->
1026 let _,_,_,cons = get_nth dl (n1+1) in
1027 let id,_ = get_nth cons n2 in
1028 qualified_name_of_uri status current_module_uri ~capitalize:true
1029 (UriManager.uri_of_string
1030 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
1031 pp_exp_named_subst exp_named_subst context
1032 | _ -> raise CicExportationInternalError
1034 Sys.Break as exn -> raise exn
1036 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
1039 | C.MutCase (uri,n1,ty,te,patterns) ->
1041 "unit (* TOO POLYMORPHIC TYPE *)"
1043 let rec needs_obj_magic ty =
1044 match CicReduction.whd context ty with
1045 | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t
1046 | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
1047 | _ -> false (* it can be a Rel, e.g. in *_rec *)
1049 let needs_obj_magic = needs_obj_magic ty in
1050 (match analyze_term context te with
1051 `Type -> assert false
1053 (match patterns with
1054 [] -> "assert false" (* empty type elimination *)
1056 pp ~in_type:false he context (* singleton elimination *)
1057 | _ -> assert false)
1060 if patterns = [] then "assert false"
1062 (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
1063 (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
1064 C.InductiveDefinition (dl,_,paramsno,_) ->
1065 let (_,_,_,cons) = get_nth dl (n1+1) in
1069 (* this is just an approximation since we do not have
1071 let rec count_prods toskip =
1073 C.Prod (_,_,bo) when toskip > 0 ->
1074 count_prods (toskip - 1) bo
1075 | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
1078 qualified_name_of_uri status current_module_uri
1080 (UriManager.uri_of_string
1081 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
1082 count_prods paramsno ty
1085 if not (is_mcu_type uri) then rc, "","","",""
1086 else rc, !current_go_up, "))", "( .< (", " ) >.)"
1087 | _ -> raise CicExportationInternalError
1090 let connames_and_argsno_and_patterns =
1094 | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
1095 | _,_ -> assert false
1097 combine (connames_and_argsno,patterns)
1100 "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^
1101 (String.concat "\n | "
1103 (fun (x,argsno,y) ->
1104 let rec aux argsno context =
1106 Cic.Lambda (name,ty,bo) when argsno > 0 ->
1109 Cic.Anonymous -> Cic.Anonymous
1110 | Cic.Name n -> Cic.Name (ppid n) in
1112 aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
1115 (match analyze_type context ty with
1116 | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
1118 | `Sort _ -> args,res
1122 | C.Name s -> s)::args,res)
1123 | t when argsno = 0 -> [],pp ~in_type:false t context
1125 ["{" ^ string_of_int argsno ^ " args missing}"],
1126 pp ~in_type:false t context
1129 if argsno = 0 then x,pp ~in_type:false y context
1131 let args,body = aux argsno context y in
1132 let sargs = String.concat "," args in
1133 x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
1136 pattern ^ " -> " ^ go_down ^
1137 (if needs_obj_magic then
1138 "Obj.magic (" ^ body ^ ")"
1141 ) connames_and_argsno_and_patterns)) ^
1143 | C.Fix (no, funs) ->
1146 (fun (types,len) (n,_,ty,_) ->
1147 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1153 (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
1154 pp ~in_type:false bo (names@context) ^ i)
1157 (match get_nth names (no + 1) with
1158 Some (Cic.Name n,_) -> n
1159 | _ -> assert false)
1160 | C.CoFix (no,funs) ->
1163 (fun (types,len) (n,ty,_) ->
1164 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1170 (fun (name,ty,bo) i -> "\n" ^ name ^
1171 " : " ^ pp ~in_type:true ty context ^ " := \n" ^
1172 pp ~in_type:false bo (names@context) ^ i)
1175 and pp_exp_named_subst exp_named_subst context =
1176 if exp_named_subst = [] then "" else
1178 String.concat " ; " (
1180 (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
1183 and clean_args_for_constr nparams context =
1184 let nparams = ref nparams in
1188 match analyze_term context t with
1189 `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
1194 and clean_args context =
1196 | [] | [_] -> assert false
1197 | he::arg1::tl as l ->
1198 let head_arg1, rest =
1199 match analyze_term context arg1 with
1201 !current_go_up :: pp ~in_type:false he context ::
1202 pp ~in_type:false arg1 context :: ["))"], tl
1208 match analyze_term context t with
1209 | `Term -> Some (pp ~in_type:false t context)
1211 prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
1213 | `Proof -> None) rest
1214 and clean_args_for_ty context =
1217 match analyze_term context t with
1218 `Type -> Some (pp ~in_type:true t context)
1226 let ppty current_module_uri =
1227 (* nparams is the number of left arguments
1228 left arguments should either become parameters or be skipped altogether *)
1229 let rec args nparams context =
1234 Cic.Anonymous -> Cic.Anonymous
1235 | Cic.Name n -> Cic.Name (String.uncapitalize n)
1237 (match analyze_type context s with
1241 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1242 | `Type when nparams > 0 ->
1243 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1246 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
1247 abstr,pp ~in_type:true current_module_uri s context::args
1248 | `Sort _ when nparams <= 0 ->
1249 let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
1250 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1254 Cic.Anonymous -> Cic.Anonymous
1255 | Cic.Name name -> Cic.Name ("'" ^ name) in
1257 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
1260 Cic.Anonymous -> abstr
1261 | Cic.Name name -> name::abstr),
1268 exception DoNotExtract;;
1270 let pp_abstracted_ty current_module_uri =
1271 let rec args context =
1273 Cic.Lambda (n,s,t) ->
1276 Cic.Anonymous -> Cic.Anonymous
1277 | Cic.Name n -> Cic.Name (String.uncapitalize n)
1279 (match analyze_type context s with
1284 args ((Some (n,Cic.Decl s))::context) t
1288 Cic.Anonymous -> Cic.Anonymous
1289 | Cic.Name name -> Cic.Name ("'" ^ name) in
1291 args ((Some (n,Cic.Decl s))::context) t
1294 Cic.Anonymous -> abstr
1295 | Cic.Name name -> name::abstr),
1298 match analyze_type context ty with
1300 prerr_endline "XXX abstracted l2 ty"; assert false
1302 | `Statement -> raise DoNotExtract
1304 (* BUG HERE: this can be a real System F type *)
1305 let head = pp ~in_type:true current_module_uri ty context in
1312 (* ppinductiveType (typename, inductive, arity, cons) *)
1313 (* pretty-prints a single inductive definition *)
1314 (* (typename, inductive, arity, cons) *)
1315 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
1317 match analyze_type [] arity with
1318 `Sort Cic.Prop -> ""
1321 | `Type -> assert false
1324 "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
1328 (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
1329 let abstr',sargs = ppty current_module_uri nparams [] ty in
1330 let sargs = String.concat " * " sargs in
1332 String.capitalize id ^
1333 (if sargs = "" then "" else " of " ^ sargs) ^
1334 (if i = "" then "" else "\n | ") ^ i)
1338 let s = String.concat "," abstr in
1339 if s = "" then "" else "(" ^ s ^ ") "
1341 "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
1344 let ppobj current_module_uri obj =
1345 let module C = Cic in
1346 let module U = UriManager in
1347 let pp ~in_type = pp ~in_type current_module_uri in
1349 C.Constant (name, Some t1, t2, params, _) ->
1350 (match analyze_type [] t2 with
1356 | Cic.Lambda (Cic.Name arg, s, t) ->
1357 (match analyze_type [] s with
1360 "let " ^ ppid name ^ "__1 = function " ^ ppid arg
1362 at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)]
1364 ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n"
1365 ^ "let " ^ ppid name ^ " = function " ^ ppid arg
1366 ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic !"^ppid name
1367 ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic ("
1368 ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!"
1369 ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
1370 ^ppid name^"__2)) >.\n;;\n"
1371 ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid
1372 name^" Matita_freescale_opcode.HCS08)"
1374 "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1375 | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
1377 match analyze_type [] t1 with
1378 `Sort Cic.Prop -> ""
1379 | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
1382 let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
1384 let s = String.concat "," abstr in
1385 if s = "" then "" else "(" ^ s ^ ") "
1387 "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
1389 DoNotExtract -> ""))
1390 | C.Constant (name, None, ty, params, _) ->
1391 (match analyze_type [] ty with
1393 | `Optimize -> prerr_endline "XXX axiom l2"; assert false
1395 | `Sort _ -> "type " ^ ppid name ^ "\n"
1396 | `Type -> "let " ^ ppid name ^ " = assert false\n")
1397 | C.Variable (name, bo, ty, params, _) ->
1398 "Variable " ^ name ^
1399 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1401 pp ~in_type:true ty [] ^ "\n" ^
1402 (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
1403 | C.CurrentProof (name, conjectures, value, ty, params, _) ->
1404 "Current Proof of " ^ name ^
1405 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
1407 let separate s = if s = "" then "" else s ^ " ; " in
1409 (fun (n, context, t) i ->
1410 let conjectures',name_context =
1412 (fun context_entry (i,name_context) ->
1413 (match context_entry with
1414 Some (n,C.Decl at) ->
1417 pp ~in_type:true ~metasenv:conjectures
1418 at name_context ^ " ",
1419 context_entry::name_context
1420 | Some (n,C.Def (at,aty)) ->
1423 pp ~in_type:true ~metasenv:conjectures
1425 ":= " ^ pp ~in_type:false
1426 ~metasenv:conjectures at name_context ^ " ",
1427 context_entry::name_context
1429 (separate i) ^ "_ :? _ ", context_entry::name_context)
1432 conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
1433 pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
1435 "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
1436 pp ~in_type:true ~metasenv:conjectures ty []
1437 | C.InductiveDefinition (l, params, nparams, _) ->
1439 (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
1442 let ppobj current_module_uri obj =
1443 let res = ppobj current_module_uri obj in
1444 if res = "" then "" else res ^ ";;\n\n"