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