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 $ *)
28 exception CicExportationInternalError;;
29 exception NotEnoughElements;;
34 UriManager.eq (UriManager.uri_of_string
35 "cic:/matita/freescale/opcode/mcu_type.ind") u
38 (* Utility functions *)
40 let analyze_term context t =
41 match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with
43 | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
46 fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph)
48 | Cic.Sort Cic.Prop -> `Proof
52 let analyze_type context t =
56 | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize
57 | Cic.Prod (_,_,t) -> aux t
61 `Sort _ | `Optimize as res -> res
64 fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)
66 Cic.Sort Cic.Prop -> `Statement
80 let n = String.uncapitalize n in
81 if List.mem n reserved then n ^ "_" else n
87 | Cic.Anonymous -> "_"
90 (* get_nth l n returns the nth element of the list l if it exists or *)
91 (* raises NotEnoughElements if l has less than n elements *)
95 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
96 | (_,_) -> raise NotEnoughElements
99 let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
102 String.capitalize (UriManager.name_of_uri uri)
104 ppid (UriManager.name_of_uri uri) in
106 let suri = UriManager.buri_of_uri uri in
107 let s = String.sub suri 5 (String.length suri - 5) in
108 let s = Pcre.replace ~pat:"/" ~templ:"_" s in
109 String.uncapitalize s in
110 if current_module_uri = UriManager.buri_of_uri uri then
113 String.capitalize filename ^ "." ^ name
116 let pp current_module_uri ?metasenv ~in_type =
117 let rec pp ~in_type t context =
118 let module C = Cic in
123 (match get_nth context n with
124 Some (C.Name s,_) -> ppid s
125 | Some (C.Anonymous,_) -> "__" ^ string_of_int n
126 | None -> "_hidden_" ^ string_of_int n
129 NotEnoughElements -> string_of_int (List.length context - n)
131 | C.Var (uri,exp_named_subst) ->
132 qualified_name_of_uri current_module_uri uri ^
133 pp_exp_named_subst exp_named_subst context
137 "?" ^ (string_of_int n) ^ "[" ^
142 | Some t -> pp ~in_type:false t context) l1) ^
146 let _,context,_ = CicUtil.lookup_meta n metasenv in
147 "?" ^ (string_of_int n) ^ "[" ^
155 | Some _, Some t -> pp ~in_type:false t context
159 CicUtil.Meta_not_found _
160 | Invalid_argument _ ->
161 "???" ^ (string_of_int n) ^ "[" ^
163 (List.rev_map (function None -> "_" | Some t ->
164 pp ~in_type:false t context) l1) ^
172 (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
175 | C.Implicit (Some `Hole) -> "%"
176 | C.Implicit _ -> "?"
180 let n = "'" ^ String.uncapitalize n in
181 "(" ^ pp ~in_type:true s context ^ " -> " ^
182 pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
184 "(" ^ pp ~in_type:true s context ^ " -> " ^
185 pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
186 | C.Cast (v,t) -> pp ~in_type v context
187 | C.Lambda (b,s,t) ->
188 (match analyze_type context s with
190 | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
191 | `Optimize -> prerr_endline "XXX lambda";assert false
193 "(function " ^ ppname b ^ " -> " ^
194 pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
195 | C.LetIn (b,s,ty,t) ->
196 (match analyze_term context s with
197 | `Optimize -> prerr_endline "XXX letin";assert false
199 | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
201 "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
202 " = " ^ pp ~in_type:false s context ^ " in " ^
203 pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
204 | C.Appl (he::tl) when in_type ->
205 let hes = pp ~in_type he context in
206 let stl = String.concat "," (clean_args_for_ty context tl) in
207 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
208 | C.Appl (C.MutInd _ as he::tl) ->
209 let hes = pp ~in_type he context in
210 let stl = String.concat "," (clean_args_for_ty context tl) in
211 (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
212 | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
214 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
215 C.InductiveDefinition (_,_,nparams,_) -> nparams
216 | _ -> assert false in
217 let hes = pp ~in_type he context in
218 let stl = String.concat "," (clean_args_for_constr nparams context tl) in
219 "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
221 "(" ^ String.concat " " (clean_args context li) ^ ")"
222 | C.Const (uri,exp_named_subst) ->
223 qualified_name_of_uri current_module_uri uri ^
224 pp_exp_named_subst exp_named_subst context
225 | C.MutInd (uri,n,exp_named_subst) ->
227 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
228 C.InductiveDefinition (dl,_,_,_) ->
229 let (name,_,_,_) = get_nth dl (n+1) in
230 qualified_name_of_uri current_module_uri
231 (UriManager.uri_of_string
232 (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
233 pp_exp_named_subst exp_named_subst context
234 | _ -> raise CicExportationInternalError
236 Sys.Break as exn -> raise exn
237 | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
239 | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
241 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
242 C.InductiveDefinition (dl,_,_,_) ->
243 let _,_,_,cons = get_nth dl (n1+1) in
244 let id,_ = get_nth cons n2 in
245 qualified_name_of_uri current_module_uri ~capitalize:true
246 (UriManager.uri_of_string
247 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
248 pp_exp_named_subst exp_named_subst context
249 | _ -> raise CicExportationInternalError
251 Sys.Break as exn -> raise exn
253 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
256 | C.MutCase (uri,n1,ty,te,patterns) ->
258 "unit (* TOO POLYMORPHIC TYPE *)"
260 let needs_obj_magic =
261 (* BUG HERE: we should consider also the right parameters *)
262 match CicReduction.whd context ty with
263 Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
264 | _ -> false (* it can be a Rel, e.g. in *_rec *)
266 (match analyze_term context te with
267 `Type -> assert false
270 [] -> "assert false" (* empty type elimination *)
272 pp ~in_type:false he context (* singleton elimination *)
276 if patterns = [] then "assert false"
278 (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
279 (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
280 C.InductiveDefinition (dl,_,paramsno,_) ->
281 let (_,_,_,cons) = get_nth dl (n1+1) in
285 (* this is just an approximation since we do not have
287 let rec count_prods toskip =
289 C.Prod (_,_,bo) when toskip > 0 ->
290 count_prods (toskip - 1) bo
291 | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
294 qualified_name_of_uri current_module_uri
296 (UriManager.uri_of_string
297 (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
298 count_prods paramsno ty
301 if not (is_mcu_type uri) then rc, "","","",""
302 else rc, "(.~(", "))", "( .< (", " ) >.)"
303 | _ -> raise CicExportationInternalError
306 let connames_and_argsno_and_patterns =
310 | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
311 | _,_ -> assert false
313 combine (connames_and_argsno,patterns)
316 "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^
317 (String.concat "\n | "
320 let rec aux argsno context =
322 Cic.Lambda (name,ty,bo) when argsno > 0 ->
325 Cic.Anonymous -> Cic.Anonymous
326 | Cic.Name n -> Cic.Name (ppid n) in
328 aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
331 (match analyze_type context ty with
332 | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false
334 | `Sort _ -> args,res
338 | C.Name s -> s)::args,res)
339 | t when argsno = 0 -> [],pp ~in_type:false t context
341 ["{" ^ string_of_int argsno ^ " args missing}"],
342 pp ~in_type:false t context
345 if argsno = 0 then x,pp ~in_type:false y context
347 let args,body = aux argsno context y in
348 let sargs = String.concat "," args in
349 x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
352 pattern ^ " -> " ^ go_down ^
353 (if needs_obj_magic then
354 "Obj.magic (" ^ body ^ ")"
357 ) connames_and_argsno_and_patterns)) ^
359 | C.Fix (no, funs) ->
362 (fun (types,len) (n,_,ty,_) ->
363 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
369 (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
370 pp ~in_type:false bo (names@context) ^ i)
373 (match get_nth names (no + 1) with
374 Some (Cic.Name n,_) -> n
376 | C.CoFix (no,funs) ->
379 (fun (types,len) (n,ty,_) ->
380 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
386 (fun (name,ty,bo) i -> "\n" ^ name ^
387 " : " ^ pp ~in_type:true ty context ^ " := \n" ^
388 pp ~in_type:false bo (names@context) ^ i)
391 and pp_exp_named_subst exp_named_subst context =
392 if exp_named_subst = [] then "" else
394 String.concat " ; " (
396 (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
399 and clean_args_for_constr nparams context =
400 let nparams = ref nparams in
404 match analyze_term context t with
405 `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
410 and clean_args context =
412 | [] | [_] -> assert false
413 | he::arg1::tl as l ->
414 let head_arg1, rest =
415 match analyze_term context arg1 with
417 "(.~(" :: pp ~in_type:false he context ::
418 pp ~in_type:false arg1 context :: ["))"], tl
424 match analyze_term context t with
425 | `Term -> Some (pp ~in_type:false t context)
427 prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false
429 | `Proof -> None) rest
430 and clean_args_for_ty context =
433 match analyze_term context t with
434 `Type -> Some (pp ~in_type:true t context)
442 let ppty current_module_uri =
443 (* nparams is the number of left arguments
444 left arguments should either become parameters or be skipped altogether *)
445 let rec args nparams context =
450 Cic.Anonymous -> Cic.Anonymous
451 | Cic.Name n -> Cic.Name (String.uncapitalize n)
453 (match analyze_type context s with
457 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
458 | `Type when nparams > 0 ->
459 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
462 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
463 abstr,pp ~in_type:true current_module_uri s context::args
464 | `Sort _ when nparams <= 0 ->
465 let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
466 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
470 Cic.Anonymous -> Cic.Anonymous
471 | Cic.Name name -> Cic.Name ("'" ^ name) in
473 args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
476 Cic.Anonymous -> abstr
477 | Cic.Name name -> name::abstr),
484 exception DoNotExtract;;
486 let pp_abstracted_ty current_module_uri =
487 let rec args context =
489 Cic.Lambda (n,s,t) ->
492 Cic.Anonymous -> Cic.Anonymous
493 | Cic.Name n -> Cic.Name (String.uncapitalize n)
495 (match analyze_type context s with
500 args ((Some (n,Cic.Decl s))::context) t
504 Cic.Anonymous -> Cic.Anonymous
505 | Cic.Name name -> Cic.Name ("'" ^ name) in
507 args ((Some (n,Cic.Decl s))::context) t
510 Cic.Anonymous -> abstr
511 | Cic.Name name -> name::abstr),
514 match analyze_type context ty with
516 prerr_endline "XXX abstracted l2 ty"; assert false
518 | `Statement -> raise DoNotExtract
520 (* BUG HERE: this can be a real System F type *)
521 let head = pp ~in_type:true current_module_uri ty context in
528 (* ppinductiveType (typename, inductive, arity, cons) *)
529 (* pretty-prints a single inductive definition *)
530 (* (typename, inductive, arity, cons) *)
531 let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
533 match analyze_type [] arity with
537 | `Type -> assert false
540 "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n"
544 (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
545 let abstr',sargs = ppty current_module_uri nparams [] ty in
546 let sargs = String.concat " * " sargs in
548 String.capitalize id ^
549 (if sargs = "" then "" else " of " ^ sargs) ^
550 (if i = "" then "" else "\n | ") ^ i)
554 let s = String.concat "," abstr in
555 if s = "" then "" else "(" ^ s ^ ") "
557 "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
560 let ppobj current_module_uri obj =
561 let module C = Cic in
562 let module U = UriManager in
563 let pp ~in_type = pp ~in_type current_module_uri in
565 C.Constant (name, Some t1, t2, params, _) ->
566 (match analyze_type [] t2 with
567 | `Optimize -> prerr_endline "XXX definition of an l2 term"; assert false
572 | Cic.Lambda (Cic.Name arg, s, t) ->
573 (match analyze_type [] s with
575 "let " ^ ppid name ^ "__1 = function " ^ ppid arg
576 ^ " -> .< " ^ pp ~in_type:false t [Some (Cic.Name arg, Cic.Decl s)]
578 ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit*unit) list);;\n"
579 ^ "let " ^ ppid name ^ " = function " ^ ppid arg
580 ^ " -> (try ignore (List.assoc "^ppid arg^"(Obj.magic !"^ppid name
581 ^"__2)) with Not_found -> "^ppid name^"__2 := ("
582 ^ ppid arg^",Obj.magic (.! ("^ppid name^"__1 "^ppid arg^")))::!"
583 ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!"
584 ^ppid name^"__2) >.\n"
586 "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
587 | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n")
589 match analyze_type [] t1 with
591 | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false
594 let abstr,res = pp_abstracted_ty current_module_uri [] t1 in
596 let s = String.concat "," abstr in
597 if s = "" then "" else "(" ^ s ^ ") "
599 "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n"
602 | C.Constant (name, None, ty, params, _) ->
603 (match analyze_type [] ty with
605 | `Optimize -> prerr_endline "XXX axiom l2"; assert false
607 | `Sort _ -> "type " ^ ppid name ^ "\n"
608 | `Type -> "let " ^ ppid name ^ " = assert false\n")
609 | C.Variable (name, bo, ty, params, _) ->
611 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
613 pp ~in_type:true ty [] ^ "\n" ^
614 (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
615 | C.CurrentProof (name, conjectures, value, ty, params, _) ->
616 "Current Proof of " ^ name ^
617 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
619 let separate s = if s = "" then "" else s ^ " ; " in
621 (fun (n, context, t) i ->
622 let conjectures',name_context =
624 (fun context_entry (i,name_context) ->
625 (match context_entry with
626 Some (n,C.Decl at) ->
629 pp ~in_type:true ~metasenv:conjectures
630 at name_context ^ " ",
631 context_entry::name_context
632 | Some (n,C.Def (at,aty)) ->
635 pp ~in_type:true ~metasenv:conjectures
637 ":= " ^ pp ~in_type:false
638 ~metasenv:conjectures at name_context ^ " ",
639 context_entry::name_context
641 (separate i) ^ "_ :? _ ", context_entry::name_context)
644 conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
645 pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
647 "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
648 pp ~in_type:true ~metasenv:conjectures ty []
649 | C.InductiveDefinition (l, params, nparams, _) ->
651 (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
654 let ppobj current_module_uri obj =
655 let res = ppobj current_module_uri obj in
656 if res = "" then "" else res ^ ";;\n\n"