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