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 (*****************************************************************************)
30 (* This module implements a very simple Coq-like pretty printer that, given *)
31 (* an object of cic (internal representation) returns a string describing *)
32 (* the object in a syntax similar to that of coq *)
34 (* It also contains the utility functions to check a name w.r.t the Matita *)
37 (*****************************************************************************)
39 exception CicPpInternalError;;
40 exception NotEnoughElements;;
42 (* Utility functions *)
47 | Cic.Anonymous -> "_"
50 (* get_nth l n returns the nth element of the list l if it exists or *)
51 (* raises NotEnoughElements if l has less than n elements *)
55 | (n, he::tail) when n > 1 -> get_nth tail (n-1)
56 | (_,_) -> raise NotEnoughElements
60 (* pretty-prints a term t of cic in an environment l where l is a list of *)
61 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
62 (* name associated to the greatest DeBrujin index in t *)
69 (match get_nth l n with
71 | Some C.Anonymous -> "__" ^ string_of_int n
72 | None -> "_hidden_" ^ string_of_int n
75 NotEnoughElements -> string_of_int (List.length l - n)
77 | C.Var (uri,exp_named_subst) ->
78 UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
80 "?" ^ (string_of_int n) ^ "[" ^
82 (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
89 (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
92 | C.Implicit (Some `Hole) -> "%"
96 C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
97 | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
99 | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
100 | C.Lambda (b,s,t) ->
101 "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
103 "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
107 (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
110 | C.Const (uri,exp_named_subst) ->
111 UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
112 | C.MutInd (uri,n,exp_named_subst) ->
114 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
115 C.InductiveDefinition (dl,_,_,_) ->
116 let (name,_,_,_) = get_nth dl (n+1) in
117 name ^ pp_exp_named_subst exp_named_subst l
118 | _ -> raise CicPpInternalError
120 _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
122 | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
124 match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
125 C.InductiveDefinition (dl,_,_,_) ->
126 let (_,_,_,cons) = get_nth dl (n1+1) in
127 let (id,_) = get_nth cons n2 in
128 id ^ pp_exp_named_subst exp_named_subst l
129 | _ -> raise CicPpInternalError
132 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
135 | C.MutCase (uri,n1,ty,te,patterns) ->
137 (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
138 C.InductiveDefinition (dl,_,_,_) ->
139 let (_,_,_,cons) = get_nth dl (n1+1) in
140 List.map (fun (id,_) -> id) cons
141 | _ -> raise CicPpInternalError
144 let connames_and_patterns =
148 | [],l -> List.map (fun x -> "???",Some x) l
149 | l,[] -> List.map (fun x -> x,None) l
150 | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
152 combine (connames,patterns)
154 "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
156 (fun (x,y) i -> "\n " ^ x ^ " => " ^
157 (match y with None -> "" | Some y -> pp y l) ^ i)
158 connames_and_patterns "" ^
160 | C.Fix (no, funs) ->
161 let snames = List.map (fun (name,_,_,_) -> name) funs in
163 List.rev (List.map (function name -> Some (C.Name name)) snames)
165 "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
167 (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
168 " : " ^ pp ty l ^ " := \n" ^
172 | C.CoFix (no,funs) ->
173 let snames = List.map (fun (name,_,_) -> name) funs in
175 List.rev (List.map (function name -> Some (C.Name name)) snames)
177 "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
179 (fun (name,ty,bo) i -> "\n" ^ name ^
180 " : " ^ pp ty l ^ " := \n" ^
184 and pp_exp_named_subst exp_named_subst l =
185 if exp_named_subst = [] then "" else
187 String.concat " ; " (
189 (function (uri,t) -> UriManager.name_of_uri uri ^ ":=" ^ pp t l)
198 (* ppinductiveType (typename, inductive, arity, cons) *)
199 (* pretty-prints a single inductive definition *)
200 (* (typename, inductive, arity, cons) *)
201 let ppinductiveType (typename, inductive, arity, cons) =
202 (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
203 pp arity [] ^ " =\n " ^
205 (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^
206 (if i = "" then "\n" else "\n | ") ^ i)
210 let ppcontext ?(sep = "\n") context =
211 let separate s = if s = "" then "" else s ^ sep in
213 (fun context_entry (i,name_context) ->
214 match context_entry with
215 Some (n,Cic.Decl t) ->
216 Printf.sprintf "%s%s : %s" (separate i) (ppname n)
217 (pp t name_context), (Some n)::name_context
218 | Some (n,Cic.Def (bo,ty)) ->
219 Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
222 | Some ty -> pp ty name_context)
223 (pp bo name_context), (Some n)::name_context
225 Printf.sprintf "%s_ :? _" (separate i), None::name_context
228 (* ppobj obj returns a string with describing the cic object obj in a syntax *)
229 (* similar to the one used by Coq *)
231 let module C = Cic in
232 let module U = UriManager in
234 C.Constant (name, Some t1, t2, params, _) ->
235 "Definition of " ^ name ^
236 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
237 ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
238 | C.Constant (name, None, ty, params, _) ->
240 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
242 | C.Variable (name, bo, ty, params, _) ->
244 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
247 (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
248 | C.CurrentProof (name, conjectures, value, ty, params, _) ->
249 "Current Proof of " ^ name ^
250 "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
252 let separate s = if s = "" then "" else s ^ " ; " in
254 (fun (n, context, t) i ->
255 let conjectures',name_context =
257 (fun context_entry (i,name_context) ->
258 (match context_entry with
259 Some (n,C.Decl at) ->
261 ppname n ^ ":" ^ pp at name_context ^ " ",
262 (Some n)::name_context
263 | Some (n,C.Def (at,None)) ->
265 ppname n ^ ":= " ^ pp at name_context ^ " ",
266 (Some n)::name_context
268 (separate i) ^ "_ :? _ ", None::name_context
272 conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
273 pp t name_context ^ "\n" ^ i
275 "\n" ^ pp value [] ^ " : " ^ pp ty []
276 | C.InductiveDefinition (l, params, nparams, _) ->
278 String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
279 "NParams = " ^ string_of_int nparams ^ "\n" ^
280 List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
283 let ppsort = function
286 | Cic.Type _ -> "Type"
287 | Cic.CProp -> "CProp"
290 (* MATITA NAMING CONVENTION *)
292 let is_prefix prefix string =
293 let len = String.length prefix in
294 let len1 = String.length string in
297 let head = String.sub string 0 len in
298 if ((String.compare head prefix)=0) ||
299 ((String.compare head (String.lowercase prefix))=0) then
301 let diff = len1-len in
302 let tail = String.sub string len diff in
303 if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
304 Some (String.sub tail 1 (diff-1))
311 let remove_prefix prefix (last,string) =
312 if string = "" then (last,string)
314 match is_prefix prefix string with
317 match is_prefix last prefix with
318 None -> (last,string)
320 (match is_prefix prefix (last^string) with
321 None -> (last,string)
322 | Some tail -> (prefix,tail))
324 | Some tail -> (prefix, tail)
326 let legal_suffix string =
327 if string = "" then true else
329 let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in
330 (Str.string_match legal_s string 0) && (Str.matched_string string = string)
333 (** check if a prefix of string_name is legal for term and returns the tail.
334 chec_rec cannot fail: at worst it return string_name.
335 The algorithm is greedy, but last contains the last name matched, providing
337 string_name is here a pair (last,string_name).*)
339 let rec check_rec ctx string_name =
342 (match List.nth ctx (m-1) with
344 remove_prefix name string_name
345 | Cic.Anonymous -> string_name)
346 | Cic.Meta _ -> string_name
347 | Cic.Sort sort -> remove_prefix (ppsort sort) string_name
348 | Cic.Implicit _ -> string_name
349 | Cic.Cast (te,ty) -> check_rec ctx string_name te
350 | Cic.Prod (name,so,dest) ->
351 let l_string_name = check_rec ctx string_name so in
352 check_rec (name::ctx) string_name dest
353 | Cic.Lambda (name,so,dest) ->
356 Cic.Anonymous -> string_name
357 | Cic.Name name -> remove_prefix name string_name in
358 let l_string_name = check_rec ctx string_name so in
359 check_rec (name::ctx) l_string_name dest
360 | Cic.LetIn (name,so,dest) ->
361 let string_name = check_rec ctx string_name so in
362 check_rec (name::ctx) string_name dest
364 List.fold_left (check_rec ctx) string_name l
365 | Cic.Var (uri,exp_named_subst) ->
366 let name = UriManager.name_of_uri uri in
367 remove_prefix name string_name
368 | Cic.Const (uri,exp_named_subst) ->
369 let name = UriManager.name_of_uri uri in
370 remove_prefix name string_name
371 | Cic.MutInd (uri,_,exp_named_subst) ->
372 let name = UriManager.name_of_uri uri in
373 remove_prefix name string_name
374 | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
376 (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
377 Cic.InductiveDefinition (dl,_,_,_) ->
378 let (_,_,_,cons) = get_nth dl (n+1) in
379 let (id,_) = get_nth cons m in
381 | _ -> assert false) in
382 remove_prefix name string_name
383 | Cic.MutCase (_,_,_,te,pl) ->
384 let strig_name = remove_prefix "match" string_name in
385 let string_name = check_rec ctx string_name te in
386 List.fold_right (fun t s -> check_rec ctx s t) pl string_name
388 let strig_name = remove_prefix "fix" string_name in
389 let names = List.map (fun (name,_,_,_) -> name) fl in
391 List.rev (List.map (function name -> Cic.Name name) names)
394 (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
395 | Cic.CoFix (_,fl) ->
396 let strig_name = remove_prefix "cofix" string_name in
397 let names = List.map (fun (name,_,_) -> name) fl in
399 List.rev (List.map (function name -> Cic.Name name) names)
402 (fun (_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
404 let check_name ?(allow_suffix=false) ctx name term =
405 let (_,tail) = check_rec ctx ("",name) term in
406 if (not allow_suffix) then (String.length tail = 0)
407 else legal_suffix tail
409 let check_elim ctx conclusion_name =
410 let elim = Str.regexp "_elim\\|_case" in
411 if (Str.string_match elim conclusion_name 0) then
412 let len = String.length conclusion_name in
413 let tail = String.sub conclusion_name 5 (len-5) in
417 let rec check_names ctx hyp_names conclusion_name t =
419 | Cic.Prod (name,s,t) ->
420 (match hyp_names with
421 [] -> check_names (name::ctx) hyp_names conclusion_name t
423 if check_name ctx hd s then
424 check_names (name::ctx) tl conclusion_name t
426 check_names (name::ctx) hyp_names conclusion_name t)
427 | Cic.Appl ((Cic.Rel n)::args) ->
428 (match hyp_names with
430 (check_name ~allow_suffix:true ctx conclusion_name t) ||
431 (check_elim ctx conclusion_name)
433 (* what to elim could be an argument
434 of the predicate: e.g. leb_elim *)
436 List.fold_left (check_rec ctx) ("",what_to_elim) args in
437 (tail = "" && check_elim ctx conclusion_name)
439 | Cic.MutCase (_,_,Cic.Lambda(name,so,ty),te,_) ->
440 (match hyp_names with
442 (match is_prefix "match" conclusion_name with
443 None -> check_name ~allow_suffix:true ctx conclusion_name t
444 | Some tail -> check_name ~allow_suffix:true ctx tail t)
446 (* what to match could be the term te or its type so; in this case the
447 conclusion name should match ty *)
448 check_name ~allow_suffix:true (name::ctx) conclusion_name ty &&
449 (check_name ctx what_to_match te || check_name ctx what_to_match so)
452 hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
454 let check name term =
455 let names = Str.split (Str.regexp_string "_to_") name in
456 let hyp_names,conclusion_name =
457 match List.rev names with
460 let elim = Str.regexp "_elim\\|_case" in
461 let len = String.length hd in
463 let pos = Str.search_backward elim hd len in
464 let hyp = String.sub hd 0 pos in
465 let concl = String.sub hd pos (len-pos) in
466 List.rev (hyp::tl),concl
467 with Not_found -> (List.rev tl),hd in
468 check_names [] hyp_names conclusion_name term