]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic_proof_checking/cicPp.ml
BIG FAT COMMIT REGARDING COERCIONS:
[helm.git] / helm / software / components / cic_proof_checking / cicPp.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*****************************************************************************)
27 (*                                                                           *)
28 (*                               PROJECT HELM                                *)
29 (*                                                                           *)
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                             *)
33 (*                                                                           *)
34 (* It also contains the utility functions to check a name w.r.t the Matita   *)
35 (* naming policy                                                             *)
36 (*                                                                           *)
37 (*****************************************************************************)
38
39 (* $Id$ *)
40
41 exception CicPpInternalError;;
42 exception NotEnoughElements;;
43
44 (* Utility functions *)
45
46 let ppname =
47  function
48     Cic.Name s     -> s
49   | Cic.Anonymous  -> "_"
50 ;;
51
52 (* get_nth l n   returns the nth element of the list l if it exists or *)
53 (* raises NotEnoughElements if l has less than n elements             *)
54 let rec get_nth l n =
55  match (n,l) with
56     (1, he::_) -> he
57   | (n, he::tail) when n > 1 -> get_nth tail (n-1)
58   | (_,_) -> raise NotEnoughElements
59 ;;
60
61 (* pp t l                                                                  *)
62 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
63 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
64 (* name associated to the greatest DeBrujin index in t                     *)
65 let rec pp t l =
66  let module C = Cic in
67    match t with
68       C.Rel n ->
69        begin
70         try
71          (match get_nth l n with
72              Some (C.Name s) -> s
73            | Some C.Anonymous -> "__" ^ string_of_int n
74            | None -> "_hidden_" ^ string_of_int n
75          )
76         with
77          NotEnoughElements -> string_of_int (List.length l - n)
78        end
79     | C.Var (uri,exp_named_subst) ->
80        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
81     | C.Meta (n,l1) ->
82        "?" ^ (string_of_int n) ^ "[" ^ 
83         String.concat " ; "
84          (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
85         "]"
86     | C.Sort s ->
87        (match s with
88            C.Prop  -> "Prop"
89          | C.Set   -> "Set"
90          | C.Type _ -> "Type"
91          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
92          | C.CProp -> "CProp" 
93        )
94     | C.Implicit (Some `Hole) -> "%"
95     | C.Implicit _ -> "?"
96     | C.Prod (b,s,t) ->
97        (match b with
98           C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
99         | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
100        )
101     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
102     | C.Lambda (b,s,t) ->
103        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
104     | C.LetIn (b,s,t) ->
105        " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
106     | C.Appl li ->
107        "(" ^
108        (List.fold_right
109         (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
110         li ""
111        ) ^ ")"
112     | C.Const (uri,exp_named_subst) ->
113        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
114     | C.MutInd (uri,n,exp_named_subst) ->
115        (try
116          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
117             C.InductiveDefinition (dl,_,_,_) ->
118              let (name,_,_,_) = get_nth dl (n+1) in
119               name ^ pp_exp_named_subst exp_named_subst l
120           | _ -> raise CicPpInternalError
121         with
122            Sys.Break as exn -> raise exn
123          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
124        )
125     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
126        (try
127          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
128             C.InductiveDefinition (dl,_,_,_) ->
129              let (_,_,_,cons) = get_nth dl (n1+1) in
130               let (id,_) = get_nth cons n2 in
131                id ^ pp_exp_named_subst exp_named_subst l
132           | _ -> raise CicPpInternalError
133         with
134            Sys.Break as exn -> raise exn
135          | _ ->
136           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
137            string_of_int n2
138        )
139     | C.MutCase (uri,n1,ty,te,patterns) ->
140        let connames =
141         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
142             C.InductiveDefinition (dl,_,_,_) ->
143              let (_,_,_,cons) = get_nth dl (n1+1) in
144               List.map (fun (id,_) -> id) cons
145           | _ -> raise CicPpInternalError
146         )
147        in
148         let connames_and_patterns =
149          let rec combine =
150             function
151                [],[] -> []
152              | [],l -> List.map (fun x -> "???",Some x) l
153              | l,[] -> List.map (fun x -> x,None) l
154              | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
155          in
156           combine (connames,patterns)
157         in
158         "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
159           List.fold_right
160            (fun (x,y) i -> "\n " ^ x ^ " => " ^
161              (match y with None -> "" | Some y -> pp y l) ^ i)
162            connames_and_patterns "" ^
163           "\nend"
164     | C.Fix (no, funs) ->
165        let snames = List.map (fun (name,_,_,_) -> name) funs in
166         let names =
167          List.rev (List.map (function name -> Some (C.Name name)) snames)
168         in
169          "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
170          List.fold_right
171           (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
172             " : " ^ pp ty l ^ " := \n" ^
173             pp bo (names@l) ^ i)
174           funs "" ^
175          "}\n"
176     | C.CoFix (no,funs) ->
177        let snames = List.map (fun (name,_,_) -> name) funs in
178         let names =
179          List.rev (List.map (function name -> Some (C.Name name)) snames)
180         in
181          "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
182          List.fold_right
183           (fun (name,ty,bo) i -> "\n" ^ name ^ 
184             " : " ^ pp ty l ^ " := \n" ^
185             pp bo (names@l) ^ i)
186           funs "" ^
187          "}\n"
188 and pp_exp_named_subst exp_named_subst l =
189  if exp_named_subst = [] then "" else
190   "\\subst[" ^
191    String.concat " ; " (
192     List.map
193      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
194      exp_named_subst
195    ) ^ "]"
196 ;;
197
198 let ppterm t =
199  pp t []
200 ;;
201
202 (* ppinductiveType (typename, inductive, arity, cons)                       *)
203 (* pretty-prints a single inductive definition                              *)
204 (* (typename, inductive, arity, cons)                                       *)
205 let ppinductiveType (typename, inductive, arity, cons) =
206   (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
207   pp arity [] ^ " =\n   " ^
208   List.fold_right
209    (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ 
210     (if i = "" then "\n" else "\n | ") ^ i)
211    cons ""
212 ;;
213
214 let ppcontext ?(sep = "\n") context =
215  let separate s = if s = "" then "" else s ^ sep in
216  fst (List.fold_right 
217    (fun context_entry (i,name_context) ->
218      match context_entry with
219         Some (n,Cic.Decl t) ->
220          Printf.sprintf "%s%s : %s" (separate i) (ppname n)
221           (pp t name_context), (Some n)::name_context
222       | Some (n,Cic.Def (bo,ty)) ->
223          Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
224           (match ty with
225               None -> "_"
226             | Some ty -> pp ty name_context)
227           (pp bo name_context), (Some n)::name_context
228        | None ->
229           Printf.sprintf "%s_ :? _" (separate i), None::name_context
230     ) context ("",[]))
231
232 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
233 (* similar to the one used by Coq                                             *)
234 let ppobj obj =
235  let module C = Cic in
236  let module U = UriManager in
237   match obj with
238     C.Constant (name, Some t1, t2, params, _) ->
239       "Definition of " ^ name ^
240        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
241        ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
242    | C.Constant (name, None, ty, params, _) ->
243       "Axiom " ^ name ^
244        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
245        "):\n" ^ pp ty []
246    | C.Variable (name, bo, ty, params, _) ->
247       "Variable " ^ name ^
248        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
249        ")" ^ ":\n" ^
250        pp ty [] ^ "\n" ^
251        (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
252    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
253       "Current Proof of " ^ name ^
254        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
255        ")" ^ ":\n" ^
256       let separate s = if s = "" then "" else s ^ " ; " in
257        List.fold_right
258         (fun (n, context, t) i -> 
259           let conjectures',name_context =
260                  List.fold_right 
261                   (fun context_entry (i,name_context) ->
262                     (match context_entry with
263                         Some (n,C.Decl at) ->
264                    (separate i) ^
265                      ppname n ^ ":" ^ pp at name_context ^ " ",
266                       (Some n)::name_context
267                       | Some (n,C.Def (at,None)) ->
268                    (separate i) ^
269                      ppname n ^ ":= " ^ pp at name_context ^ " ",
270                       (Some n)::name_context
271                 | None ->
272                    (separate i) ^ "_ :? _ ", None::name_context
273                 | _ -> assert false)
274             ) context ("",[])
275           in
276            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
277             pp t name_context ^ "\n" ^ i
278         ) conjectures "" ^
279         "\n" ^ pp value [] ^ " : " ^ pp ty [] 
280    | C.InductiveDefinition (l, params, nparams, _) ->
281       "Parameters = " ^
282        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
283        "NParams = " ^ string_of_int nparams ^ "\n" ^
284         List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
285 ;;
286
287 let ppsort = function
288   | Cic.Prop -> "Prop"
289   | Cic.Set -> "Set"
290   | Cic.Type _ -> "Type"
291   | Cic.CProp -> "CProp"
292
293
294 (* MATITA NAMING CONVENTION *)
295
296 let is_prefix prefix string =
297   let len = String.length prefix in
298   let len1 = String.length string in
299   if len <= len1 then
300     begin
301       let head = String.sub string 0 len in
302       if 
303       (String.compare (String.lowercase head) (String.lowercase prefix)=0) then 
304         begin
305           let diff = len1-len in
306           let tail = String.sub string len diff in
307           if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
308             Some (String.sub tail 1 (diff-1))
309             else Some tail
310           end
311         else None
312     end
313   else None
314
315 let remove_prefix prefix (last,string) =
316   if string = "" then (last,string)
317   else 
318     match is_prefix prefix string with
319       None ->
320         if last <> "" then 
321           match is_prefix last prefix with
322             None -> (last,string)
323           | Some _ ->
324               (match is_prefix prefix (last^string) with
325                 None -> (last,string)
326               | Some tail -> (prefix,tail))
327         else (last,string)
328     | Some tail -> (prefix, tail)
329         
330 let legal_suffix string = 
331   if string = "" then true else
332   begin
333     let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in
334     (Str.string_match legal_s string 0) && (Str.matched_string string = string)
335   end
336
337 (** check if a prefix of string_name is legal for term and returns the tail.
338     chec_rec cannot fail: at worst it return string_name.
339     The algorithm is greedy, but last contains the last name matched, providing
340     a one slot buffer. 
341     string_name is here a pair (last,string_name).*)
342
343 let rec check_rec ctx string_name =
344   function
345     | Cic.Rel m -> 
346         (match List.nth ctx (m-1) with
347           Cic.Name name ->
348             remove_prefix name string_name
349         | Cic.Anonymous -> string_name)
350     | Cic.Meta _ -> string_name
351     | Cic.Sort sort -> remove_prefix (ppsort sort) string_name  
352     | Cic.Implicit _ -> string_name
353     | Cic.Cast (te,ty) -> check_rec ctx string_name te
354     | Cic.Prod (name,so,dest) -> 
355         let l_string_name = check_rec ctx string_name so in
356         check_rec (name::ctx) string_name dest
357     | Cic.Lambda (name,so,dest) -> 
358         let string_name =
359           match name with
360             Cic.Anonymous -> string_name
361           | Cic.Name name -> remove_prefix name string_name in
362         let l_string_name = check_rec ctx string_name so in
363         check_rec (name::ctx) l_string_name dest
364     | Cic.LetIn (name,so,dest) -> 
365         let string_name = check_rec ctx string_name so in
366         check_rec (name::ctx) string_name dest
367     | Cic.Appl l ->
368         List.fold_left (check_rec ctx) string_name l
369     | Cic.Var (uri,exp_named_subst) ->
370         let name = UriManager.name_of_uri uri in
371         remove_prefix name string_name
372     | Cic.Const (uri,exp_named_subst) ->
373         let name = UriManager.name_of_uri uri in
374         remove_prefix name string_name
375     | Cic.MutInd (uri,_,exp_named_subst) -> 
376         let name = UriManager.name_of_uri uri in
377         remove_prefix name string_name  
378     | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
379         let name =
380           (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
381             Cic.InductiveDefinition (dl,_,_,_) ->
382               let (_,_,_,cons) = get_nth dl (n+1) in
383               let (id,_) = get_nth cons m in
384               id 
385           | _ -> assert false) in
386         remove_prefix name string_name  
387     | Cic.MutCase (_,_,_,te,pl) ->
388         let strig_name = remove_prefix "match" string_name in
389         let string_name = check_rec ctx string_name te in
390         List.fold_right (fun t s -> check_rec ctx s t) pl string_name
391     | Cic.Fix (_,fl) ->
392         let strig_name = remove_prefix "fix" string_name in
393         let names = List.map (fun (name,_,_,_) -> name) fl in
394         let onames =
395           List.rev (List.map (function name -> Cic.Name name) names)
396         in
397         List.fold_right 
398           (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
399     | Cic.CoFix (_,fl) ->
400         let strig_name = remove_prefix "cofix" string_name in
401         let names = List.map (fun (name,_,_) -> name) fl in
402         let onames =
403           List.rev (List.map (function name -> Cic.Name name) names)
404         in
405         List.fold_right 
406           (fun (_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
407
408 let check_name ?(allow_suffix=false) ctx name term =
409   let (_,tail) = check_rec ctx ("",name) term in
410   if (not allow_suffix) then (String.length tail = 0) 
411   else legal_suffix tail
412
413 let check_elim ctx conclusion_name =
414   let elim = Str.regexp "_elim\\|_case" in
415   if (Str.string_match elim conclusion_name 0) then
416     let len = String.length conclusion_name in
417     let tail = String.sub conclusion_name 5 (len-5) in
418     legal_suffix tail
419   else false
420
421 let rec check_names ctx hyp_names conclusion_name t =
422   match t with
423     | Cic.Prod (name,s,t) -> 
424         (match hyp_names with
425              [] -> check_names (name::ctx) hyp_names conclusion_name t
426            | hd::tl ->
427                if check_name ctx hd s then 
428                  check_names (name::ctx) tl conclusion_name t
429                else 
430                  check_names (name::ctx) hyp_names conclusion_name t)
431     | Cic.Appl ((Cic.Rel n)::args) -> 
432         (match hyp_names with
433           | [] ->
434               (check_name ~allow_suffix:true ctx conclusion_name t) ||
435               (check_elim ctx conclusion_name)
436           | [what_to_elim] ->   
437               (* what to elim could be an argument 
438                  of the predicate: e.g. leb_elim *)
439               let (last,tail) = 
440                 List.fold_left (check_rec ctx) ("",what_to_elim) args in
441               (tail = "" && check_elim ctx conclusion_name)
442           | _ -> false)
443     | Cic.MutCase  (_,_,Cic.Lambda(name,so,ty),te,_) ->
444         (match hyp_names with
445           | [] ->
446                (match is_prefix "match" conclusion_name with
447                    None -> check_name ~allow_suffix:true ctx conclusion_name t
448                | Some tail -> check_name ~allow_suffix:true ctx tail t)
449           | [what_to_match] ->   
450               (* what to match could be the term te or its type so; in this case the
451                  conclusion name should match ty *)
452               check_name ~allow_suffix:true (name::ctx) conclusion_name ty &&
453               (check_name ctx what_to_match te || check_name ctx what_to_match so)
454           | _ -> false)
455     | _ -> 
456         hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
457
458 let check name term =
459   let names = Str.split (Str.regexp_string "_to_") name in
460   let hyp_names,conclusion_name =
461     match List.rev names with
462         [] -> assert false
463       | hd::tl -> 
464           let elim = Str.regexp "_elim\\|_case" in
465           let len = String.length hd in
466           try 
467             let pos = Str.search_backward elim hd len in
468             let hyp = String.sub hd 0 pos in
469             let concl = String.sub hd pos (len-pos) in
470             List.rev (hyp::tl),concl
471           with Not_found -> (List.rev tl),hd in
472   check_names [] hyp_names conclusion_name term
473 ;;
474
475