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 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 24/01/2000                                 *)
  32 (*                                                                            *)
  33 (* This module implements a very simple Coq-like pretty printer that, given   *)
  34 (* an object of cic (internal representation) returns a string describing the *)
  35 (* object in a syntax similar to that of coq                                  *)
  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 check_name ctx name term =
 281   let cut_off_name name string_name =
 282     let len = String.length name in
 283     let len1 = String.length string_name in
 284     if len <= len1 then
 285       begin
 286         let head = String.sub string_name 0 len in
 287         if ((String.compare head name)=0) ||
 288            ((String.compare head (String.lowercase name))=0) then
 289           begin
 290             let diff = len1-len in
 291             let tail = String.sub string_name len diff in
 292             if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
 293               String.sub tail 1 (diff-1)
 294             else tail
 295           end
 296         else string_name
 297       end
 298     else string_name in
 299   let rec check_aux ctx string_name =
 300     function
 301       | Cic.Rel m ->
 302           (match List.nth ctx (m-1) with
 303                Cic.Name name ->
 304                  cut_off_name name string_name
 305              | Cic.Anonymous -> string_name)
 306       | Cic.Meta _ -> string_name
 307       | Cic.Sort sort -> cut_off_name (ppsort sort) string_name
 308       | Cic.Implicit _ -> string_name
 309       | Cic.Cast (te,ty) -> check_aux ctx string_name te
 310       | Cic.Prod (name,so,dest) ->
 311           let string_name = check_aux ctx string_name so in
 312           check_aux (name::ctx) string_name dest
 313       | Cic.Lambda (name,so,dest) ->
 314           let string_name = check_aux ctx string_name so in
 315           check_aux (name::ctx) string_name dest
 316       | Cic.LetIn (name,so,dest) ->
 317           let string_name = check_aux ctx string_name so in
 318           check_aux (name::ctx) string_name dest
 319       | Cic.Appl l ->
 320           List.fold_left (check_aux ctx) string_name l
 321       | Cic.Var (uri,exp_named_subst) ->
 322           let name = UriManager.name_of_uri uri in
 323           cut_off_name name string_name
 324       | Cic.Const (uri,exp_named_subst) ->
 325           let name = UriManager.name_of_uri uri in
 326           cut_off_name name string_name
 327       | Cic.MutInd (uri,_,exp_named_subst) ->
 328           let name = UriManager.name_of_uri uri in
 329           cut_off_name name string_name
 330       | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
 331           let name =
 332             (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
 333                 Cic.InductiveDefinition (dl,_,_,_) ->
 334                   let (_,_,_,cons) = get_nth dl (n+1) in
 335                   let (id,_) = get_nth cons m in
 336                     id
 337                | _ -> assert false) in
 338           cut_off_name name string_name
 339       | Cic.MutCase (_,_,_,te,pl) ->
 340           let strig_name = cut_off_name "match" string_name in
 341           let string_name = check_aux ctx string_name te in
 342           List.fold_right (fun t s -> check_aux ctx s t) pl string_name
 343       | Cic.Fix (_,fl) ->
 344           let strig_name = cut_off_name "fix" string_name in
 345           let names = List.map (fun (name,_,_,_) -> name) fl in
 346           let onames =
 347             List.rev (List.map (function name -> Cic.Name name) names)
 348           in
 349           List.fold_right
 350             (fun (_,_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
 351       | Cic.CoFix (_,fl) ->
 352           let strig_name = cut_off_name "cofix" string_name in
 353           let names = List.map (fun (name,_,_) -> name) fl in
 354           let onames =
 355             List.rev (List.map (function name -> Cic.Name name) names)
 356           in
 357           List.fold_right
 358             (fun (_,_,bo) s -> check_aux (onames@ctx) s bo) fl string_name
 359   in
 360   if (String.length (check_aux ctx name term) = 0) then true
 361   else false
 362
 363 let rec check_names ctx hyp_names conclusion_name t =
 364   match t with
 365     | Cic.Prod (name,s,t) ->
 366         (match hyp_names with
 367              [] -> check_names (name::ctx) hyp_names conclusion_name t
 368            | hd::tl ->
 369                if check_name ctx hd s then
 370                  check_names (name::ctx) tl conclusion_name t
 371                else
 372                  check_names (name::ctx) hyp_names conclusion_name t)
 373     | _ ->
 374         hyp_names=[] && (check_name ctx conclusion_name t)
 375
 376 let check name term =
 377   let names = Str.split (Str.regexp_string "_to_") name in
 378   let hyp_names,conclusion_name =
 379     match List.rev names with
 380         [] -> assert false
 381       | hd::tl -> (List.rev tl),hd in
 382   check_names [] hyp_names conclusion_name term
 383 ;;
 384
 385