]> matita.cs.unibo.it Git - helm.git/blob - cic_proof_checking/cicPp.ml
made executable again
[helm.git] / 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 pp ?metasenv =
66 let rec pp t l =
67  let module C = Cic in
68    match t with
69       C.Rel n ->
70        begin
71         try
72          (match get_nth l n with
73              Some (C.Name s) -> s
74            | Some C.Anonymous -> "__" ^ string_of_int n
75            | None -> "_hidden_" ^ string_of_int n
76          )
77         with
78          NotEnoughElements -> string_of_int (List.length l - n)
79        end
80     | C.Var (uri,exp_named_subst) ->
81        UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
82     | C.Meta (n,l1) ->
83        (match metasenv with
84            None ->
85             "?" ^ (string_of_int n) ^ "[" ^ 
86              String.concat " ; "
87               (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
88              "]"
89          | Some metasenv ->
90             try
91              let _,context,_ = CicUtil.lookup_meta n metasenv in
92               "?" ^ (string_of_int n) ^ "[" ^ 
93                String.concat " ; "
94                 (List.rev
95                   (List.map2
96                     (fun x y ->
97                       match x,y with
98                          _, None
99                        | None, _ -> "_"
100                        | Some _, Some t -> pp t l
101                     ) context l1)) ^
102                "]"
103             with
104               CicUtil.Meta_not_found _ 
105             | Invalid_argument _ ->
106               "???" ^ (string_of_int n) ^ "[" ^ 
107                String.concat " ; "
108                 (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
109                "]"
110        )
111     | C.Sort s ->
112        (match s with
113            C.Prop  -> "Prop"
114          | C.Set   -> "Set"
115          | C.Type _ -> "Type"
116          (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
117          | C.CProp -> "CProp" 
118        )
119     | C.Implicit (Some `Hole) -> "%"
120     | C.Implicit _ -> "?"
121     | C.Prod (b,s,t) ->
122        (match b with
123           C.Name n -> "(\\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
124         | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
125        )
126     | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
127     | C.Lambda (b,s,t) ->
128        "(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
129     | C.LetIn (b,s,t) ->
130        " let " ^ ppname b ^ " \\def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
131     | C.Appl li ->
132        "(" ^
133        (List.fold_right
134         (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
135         li ""
136        ) ^ ")"
137     | C.Const (uri,exp_named_subst) ->
138        UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
139     | C.MutInd (uri,n,exp_named_subst) ->
140        (try
141          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
142             C.InductiveDefinition (dl,_,_,_) ->
143              let (name,_,_,_) = get_nth dl (n+1) in
144               name ^ pp_exp_named_subst exp_named_subst l
145           | _ -> raise CicPpInternalError
146         with
147            Sys.Break as exn -> raise exn
148          | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
149        )
150     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
151        (try
152          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
153             C.InductiveDefinition (dl,_,_,_) ->
154              let (_,_,_,cons) = get_nth dl (n1+1) in
155               let (id,_) = get_nth cons n2 in
156                id ^ pp_exp_named_subst exp_named_subst l
157           | _ -> raise CicPpInternalError
158         with
159            Sys.Break as exn -> raise exn
160          | _ ->
161           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
162            string_of_int n2
163        )
164     | C.MutCase (uri,n1,ty,te,patterns) ->
165        let connames_and_argsno =
166         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
167             C.InductiveDefinition (dl,_,paramsno,_) ->
168              let (_,_,_,cons) = get_nth dl (n1+1) in
169               List.map
170                (fun (id,ty) ->
171                  (* this is just an approximation since we do not have
172                     reduction yet! *)
173                  let rec count_prods toskip =
174                   function
175                      C.Prod (_,_,bo) when toskip > 0 ->
176                       count_prods (toskip - 1) bo
177                    | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
178                    | _ -> 0
179                  in
180                   id, count_prods paramsno ty
181                ) cons
182           | _ -> raise CicPpInternalError
183         )
184        in
185         let connames_and_argsno_and_patterns =
186          let rec combine =
187             function
188                [],[] -> []
189              | [],l -> List.map (fun x -> "???",0,Some x) l
190              | l,[] -> List.map (fun (x,no) -> x,no,None) l
191              | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
192          in
193           combine (connames_and_argsno,patterns)
194         in
195          "\nmatch " ^ pp te l ^ " return " ^ pp ty l ^ " with \n [ " ^
196           (String.concat "\n | "
197            (List.map
198             (fun (x,argsno,y) ->
199               let rec aux argsno l =
200                function
201                   Cic.Lambda (name,ty,bo) when argsno > 0 ->
202                    let args,res = aux (argsno - 1) (Some name::l) bo in
203                     ("(" ^ (match name with C.Anonymous -> "_" | C.Name s -> s)^
204                      ":" ^ pp ty l ^ ")")::args, res
205                 | t when argsno = 0 -> [],pp t l
206                 | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t l
207               in
208                let pattern,body =
209                 match y with
210                    None -> x,""
211                  | Some y when argsno = 0 -> x,pp y l
212                  | Some y ->
213                     let args,body = aux argsno l y in
214                      "(" ^ x ^ " " ^ String.concat " " args ^ ")",body
215                in
216                 pattern ^ " => " ^ body
217             ) connames_and_argsno_and_patterns)) ^
218           "\n]"
219     | C.Fix (no, funs) ->
220        let snames = List.map (fun (name,_,_,_) -> name) funs in
221         let names =
222          List.rev (List.map (function name -> Some (C.Name name)) snames)
223         in
224          "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
225          List.fold_right
226           (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
227             " : " ^ pp ty l ^ " := \n" ^
228             pp bo (names@l) ^ i)
229           funs "" ^
230          "}\n"
231     | C.CoFix (no,funs) ->
232        let snames = List.map (fun (name,_,_) -> name) funs in
233         let names =
234          List.rev (List.map (function name -> Some (C.Name name)) snames)
235         in
236          "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
237          List.fold_right
238           (fun (name,ty,bo) i -> "\n" ^ name ^ 
239             " : " ^ pp ty l ^ " := \n" ^
240             pp bo (names@l) ^ i)
241           funs "" ^
242          "}\n"
243 and pp_exp_named_subst exp_named_subst l =
244  if exp_named_subst = [] then "" else
245   "\\subst[" ^
246    String.concat " ; " (
247     List.map
248      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
249      exp_named_subst
250    ) ^ "]"
251 in
252  pp
253 ;;
254
255 let ppterm ?metasenv t =
256  pp ?metasenv t []
257 ;;
258
259 (* ppinductiveType (typename, inductive, arity, cons)                       *)
260 (* pretty-prints a single inductive definition                              *)
261 (* (typename, inductive, arity, cons)                                       *)
262 let ppinductiveType (typename, inductive, arity, cons) =
263   (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
264   pp arity [] ^ " =\n   " ^
265   List.fold_right
266    (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ 
267     (if i = "" then "\n" else "\n | ") ^ i)
268    cons ""
269 ;;
270
271 let ppcontext ?metasenv ?(sep = "\n") context =
272  let separate s = if s = "" then "" else s ^ sep in
273  fst (List.fold_right 
274    (fun context_entry (i,name_context) ->
275      match context_entry with
276         Some (n,Cic.Decl t) ->
277          Printf.sprintf "%s%s : %s" (separate i) (ppname n)
278           (pp ?metasenv t name_context), (Some n)::name_context
279       | Some (n,Cic.Def (bo,ty)) ->
280          Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
281           (match ty with
282               None -> "_"
283             | Some ty -> pp ?metasenv ty name_context)
284           (pp ?metasenv bo name_context), (Some n)::name_context
285        | None ->
286           Printf.sprintf "%s_ :? _" (separate i), None::name_context
287     ) context ("",[]))
288
289 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
290 (* similar to the one used by Coq                                             *)
291 let ppobj obj =
292  let module C = Cic in
293  let module U = UriManager in
294   match obj with
295     C.Constant (name, Some t1, t2, params, _) ->
296       "Definition of " ^ name ^
297        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
298        ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
299    | C.Constant (name, None, ty, params, _) ->
300       "Axiom " ^ name ^
301        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
302        "):\n" ^ pp ty []
303    | C.Variable (name, bo, ty, params, _) ->
304       "Variable " ^ name ^
305        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
306        ")" ^ ":\n" ^
307        pp ty [] ^ "\n" ^
308        (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
309    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
310       "Current Proof of " ^ name ^
311        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
312        ")" ^ ":\n" ^
313       let separate s = if s = "" then "" else s ^ " ; " in
314        List.fold_right
315         (fun (n, context, t) i -> 
316           let conjectures',name_context =
317                  List.fold_right 
318                   (fun context_entry (i,name_context) ->
319                     (match context_entry with
320                         Some (n,C.Decl at) ->
321                    (separate i) ^
322                      ppname n ^ ":" ^
323                       pp ~metasenv:conjectures at name_context ^ " ",
324                       (Some n)::name_context
325                       | Some (n,C.Def (at,None)) ->
326                    (separate i) ^
327                      ppname n ^ ":= " ^ pp ~metasenv:conjectures
328                       at name_context ^ " ",
329                       (Some n)::name_context
330                 | None ->
331                    (separate i) ^ "_ :? _ ", None::name_context
332                 | _ -> assert false)
333             ) context ("",[])
334           in
335            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
336             pp ~metasenv:conjectures t name_context ^ "\n" ^ i
337         ) conjectures "" ^
338         "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
339           pp ~metasenv:conjectures ty [] 
340    | C.InductiveDefinition (l, params, nparams, _) ->
341       "Parameters = " ^
342        String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
343        "NParams = " ^ string_of_int nparams ^ "\n" ^
344         List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
345 ;;
346
347 let ppsort = function
348   | Cic.Prop -> "Prop"
349   | Cic.Set -> "Set"
350   | Cic.Type _ -> "Type"
351   | Cic.CProp -> "CProp"
352
353
354 (* MATITA NAMING CONVENTION *)
355
356 let is_prefix prefix string =
357   let len = String.length prefix in
358   let len1 = String.length string in
359   if len <= len1 then
360     begin
361       let head = String.sub string 0 len in
362       if 
363       (String.compare (String.lowercase head) (String.lowercase prefix)=0) then 
364         begin
365           let diff = len1-len in
366           let tail = String.sub string len diff in
367           if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
368             Some (String.sub tail 1 (diff-1))
369             else Some tail
370           end
371         else None
372     end
373   else None
374
375 let remove_prefix prefix (last,string) =
376   if string = "" then (last,string)
377   else 
378     match is_prefix prefix string with
379       None ->
380         if last <> "" then 
381           match is_prefix last prefix with
382             None -> (last,string)
383           | Some _ ->
384               (match is_prefix prefix (last^string) with
385                 None -> (last,string)
386               | Some tail -> (prefix,tail))
387         else (last,string)
388     | Some tail -> (prefix, tail)
389         
390 let legal_suffix string = 
391   if string = "" then true else
392   begin
393     let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in
394     (Str.string_match legal_s string 0) && (Str.matched_string string = string)
395   end
396
397 (** check if a prefix of string_name is legal for term and returns the tail.
398     chec_rec cannot fail: at worst it return string_name.
399     The algorithm is greedy, but last contains the last name matched, providing
400     a one slot buffer. 
401     string_name is here a pair (last,string_name).*)
402
403 let rec check_rec ctx string_name =
404   function
405     | Cic.Rel m -> 
406         (match List.nth ctx (m-1) with
407           Cic.Name name ->
408             remove_prefix name string_name
409         | Cic.Anonymous -> string_name)
410     | Cic.Meta _ -> string_name
411     | Cic.Sort sort -> remove_prefix (ppsort sort) string_name  
412     | Cic.Implicit _ -> string_name
413     | Cic.Cast (te,ty) -> check_rec ctx string_name te
414     | Cic.Prod (name,so,dest) -> 
415         let l_string_name = check_rec ctx string_name so in
416         check_rec (name::ctx) string_name dest
417     | Cic.Lambda (name,so,dest) -> 
418         let string_name =
419           match name with
420             Cic.Anonymous -> string_name
421           | Cic.Name name -> remove_prefix name string_name in
422         let l_string_name = check_rec ctx string_name so in
423         check_rec (name::ctx) l_string_name dest
424     | Cic.LetIn (name,so,dest) -> 
425         let string_name = check_rec ctx string_name so in
426         check_rec (name::ctx) string_name dest
427     | Cic.Appl l ->
428         List.fold_left (check_rec ctx) string_name l
429     | Cic.Var (uri,exp_named_subst) ->
430         let name = UriManager.name_of_uri uri in
431         remove_prefix name string_name
432     | Cic.Const (uri,exp_named_subst) ->
433         let name = UriManager.name_of_uri uri in
434         remove_prefix name string_name
435     | Cic.MutInd (uri,_,exp_named_subst) -> 
436         let name = UriManager.name_of_uri uri in
437         remove_prefix name string_name  
438     | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
439         let name =
440           (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
441             Cic.InductiveDefinition (dl,_,_,_) ->
442               let (_,_,_,cons) = get_nth dl (n+1) in
443               let (id,_) = get_nth cons m in
444               id 
445           | _ -> assert false) in
446         remove_prefix name string_name  
447     | Cic.MutCase (_,_,_,te,pl) ->
448         let string_name = remove_prefix "match" string_name in
449         let string_name = check_rec ctx string_name te in
450         List.fold_right (fun t s -> check_rec ctx s t) pl string_name
451     | Cic.Fix (_,fl) ->
452         let string_name = remove_prefix "fix" string_name in
453         let names = List.map (fun (name,_,_,_) -> name) fl in
454         let onames =
455           List.rev (List.map (function name -> Cic.Name name) names)
456         in
457         List.fold_right 
458           (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
459     | Cic.CoFix (_,fl) ->
460         let string_name = remove_prefix "cofix" string_name in
461         let names = List.map (fun (name,_,_) -> name) fl in
462         let onames =
463           List.rev (List.map (function name -> Cic.Name name) names)
464         in
465         List.fold_right 
466           (fun (_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
467
468 let check_name ?(allow_suffix=false) ctx name term =
469   let (_,tail) = check_rec ctx ("",name) term in
470   if (not allow_suffix) then (String.length tail = 0) 
471   else legal_suffix tail
472
473 let check_elim ctx conclusion_name =
474   let elim = Str.regexp "_elim\\|_case" in
475   if (Str.string_match elim conclusion_name 0) then
476     let len = String.length conclusion_name in
477     let tail = String.sub conclusion_name 5 (len-5) in
478     legal_suffix tail
479   else false
480
481 let rec check_names ctx hyp_names conclusion_name t =
482   match t with
483     | Cic.Prod (name,s,t) -> 
484         (match hyp_names with
485              [] -> check_names (name::ctx) hyp_names conclusion_name t
486            | hd::tl ->
487                if check_name ctx hd s then 
488                  check_names (name::ctx) tl conclusion_name t
489                else 
490                  check_names (name::ctx) hyp_names conclusion_name t)
491     | Cic.Appl ((Cic.Rel n)::args) -> 
492         (match hyp_names with
493           | [] ->
494               (check_name ~allow_suffix:true ctx conclusion_name t) ||
495               (check_elim ctx conclusion_name)
496           | [what_to_elim] ->   
497               (* what to elim could be an argument 
498                  of the predicate: e.g. leb_elim *)
499               let (last,tail) = 
500                 List.fold_left (check_rec ctx) ("",what_to_elim) args in
501               (tail = "" && check_elim ctx conclusion_name)
502           | _ -> false)
503     | Cic.MutCase  (_,_,Cic.Lambda(name,so,ty),te,_) ->
504         (match hyp_names with
505           | [] ->
506                (match is_prefix "match" conclusion_name with
507                    None -> check_name ~allow_suffix:true ctx conclusion_name t
508                | Some tail -> check_name ~allow_suffix:true ctx tail t)
509           | [what_to_match] ->   
510               (* what to match could be the term te or its type so; in this case the
511                  conclusion name should match ty *)
512               check_name ~allow_suffix:true (name::ctx) conclusion_name ty &&
513               (check_name ctx what_to_match te || check_name ctx what_to_match so)
514           | _ -> false)
515     | _ -> 
516         hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
517
518 let check name term =
519   let names = Str.split (Str.regexp_string "_to_") name in
520   let hyp_names,conclusion_name =
521     match List.rev names with
522         [] -> assert false
523       | hd::tl -> 
524           let elim = Str.regexp "_elim\\|_case" in
525           let len = String.length hd in
526           try 
527             let pos = Str.search_backward elim hd len in
528             let hyp = String.sub hd 0 pos in
529             let concl = String.sub hd pos (len-pos) in
530             List.rev (hyp::tl),concl
531           with Not_found -> (List.rev tl),hd in
532   check_names [] hyp_names conclusion_name term
533 ;;
534
535