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