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