src/Pure/Proof/proof_syntax.ML
author wenzelm
Tue May 31 11:53:40 2005 +0200 (2005-05-31)
changeset 16149 d8cac577493c
parent 15574 b1d1b5bfc464
child 16182 a5c77d298ad7
permissions -rw-r--r--
Theory.restore_naming;
tuned fold;
     1 (*  Title:      Pure/Proof/proof_syntax.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 
     5 Function for parsing and printing proof terms.
     6 *)
     7 
     8 signature PROOF_SYNTAX =
     9 sig
    10   val proofT : typ
    11   val add_proof_syntax : Sign.sg -> Sign.sg
    12   val disambiguate_names : theory -> Proofterm.proof ->
    13     Proofterm.proof * Proofterm.proof Symtab.table
    14   val proof_of_term : theory -> Proofterm.proof Symtab.table ->
    15     bool -> term -> Proofterm.proof
    16   val term_of_proof : Proofterm.proof -> term
    17   val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
    18   val read_term : theory -> typ -> string -> term
    19   val read_proof : theory -> bool -> string -> Proofterm.proof
    20   val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
    21   val pretty_proof_of : bool -> thm -> Pretty.T
    22   val print_proof_of : bool -> thm -> unit
    23 end;
    24 
    25 structure ProofSyntax : PROOF_SYNTAX =
    26 struct
    27 
    28 open Proofterm;
    29 
    30 (**** add special syntax for embedding proof terms ****)
    31 
    32 val proofT = Type ("proof", []);
    33 val paramT = Type ("param", []);
    34 val paramsT = Type ("params", []);
    35 val idtT = Type ("idt", []);
    36 val aT = TFree ("'a", []);
    37 
    38 (** constants for theorems and axioms **)
    39 
    40 fun add_prefix a b = NameSpace.pack (a :: NameSpace.unpack b);
    41 
    42 fun add_proof_atom_consts names sg = Sign.add_consts_i
    43   (map (fn name => (name, proofT, NoSyn)) names) (Sign.add_path "//" sg);
    44 
    45 (** constants for application and abstraction **)
    46 
    47 fun add_proof_syntax sg =
    48   sg
    49   |> Sign.copy
    50   |> Sign.add_path "/"
    51   |> Sign.add_defsort_i []
    52   |> Sign.add_types [("proof", 0, NoSyn)]
    53   |> Sign.add_consts_i
    54       [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    55        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    56        ("Abst", (aT --> proofT) --> proofT, NoSyn),
    57        ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
    58        ("Hyp", propT --> proofT, NoSyn),
    59        ("Oracle", propT --> proofT, NoSyn),
    60        ("MinProof", proofT, Delimfix "?")]
    61   |> Sign.add_nonterminals ["param", "params"]
    62   |> Sign.add_syntax_i
    63       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    64        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    65        ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    66        ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
    67        ("", paramT --> paramT, Delimfix "'(_')"),
    68        ("", idtT --> paramsT, Delimfix "_"),
    69        ("", paramT --> paramsT, Delimfix "_")]
    70   |> Sign.add_modesyntax_i (("xsymbols", true),
    71       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    72        ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    73        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    74   |> Sign.add_modesyntax_i (("latex", false),
    75       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))])
    76   |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    77       [(Syntax.mk_appl (Constant "_Lam")
    78           [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    79         Syntax.mk_appl (Constant "_Lam")
    80           [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
    81        (Syntax.mk_appl (Constant "_Lam")
    82           [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
    83         Syntax.mk_appl (Constant "AbsP") [Variable "A",
    84           (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
    85        (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
    86         Syntax.mk_appl (Constant "Abst")
    87           [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
    88 
    89 
    90 (**** create unambiguous theorem names ****)
    91 
    92 fun disambiguate_names thy prf =
    93   let
    94     val thms = thms_of_proof Symtab.empty prf;
    95     val thms' = map (apsnd (#prop o rep_thm)) (List.concat
    96       (map PureThy.thms_of (thy :: Theory.ancestors_of thy)));
    97 
    98     val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    99       let val prop = getOpt (assoc (thms', key), Bound 0)
   100       in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
   101         if prop <> prop' then
   102           (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
   103         else x) (tab, 1) ps)
   104       end) (Symtab.empty, thms);
   105 
   106     fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
   107       | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
   108       | rename (prf1 %% prf2) = rename prf1 %% rename prf2
   109       | rename (prf % t) = rename prf % t
   110       | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
   111           let
   112             val prop' = getOpt (assoc (thms', s), Bound 0);
   113             val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop'
   114           in if prop = prop' then prf' else
   115             PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
   116               prf, prop, Ts)
   117           end
   118       | rename prf = prf
   119 
   120   in (rename prf, tab) end;
   121 
   122 
   123 (**** translation between proof terms and pure terms ****)
   124 
   125 fun proof_of_term thy tab ty =
   126   let
   127     val thys = thy :: Theory.ancestors_of thy;
   128     val thms = List.concat (map thms_of thys);
   129     val axms = List.concat (map (Symtab.dest o #axioms o rep_theory) thys);
   130 
   131     fun mk_term t = (if ty then I else map_term_types (K dummyT))
   132       (Term.no_dummy_patterns t);
   133 
   134     fun prf_of [] (Bound i) = PBound i
   135       | prf_of Ts (Const (s, Type ("proof", _))) =
   136           change_type (if ty then SOME Ts else NONE)
   137             (case NameSpace.unpack s of
   138                "axm" :: xs =>
   139                  let
   140                    val name = NameSpace.pack xs;
   141                    val prop = (case assoc (axms, name) of
   142                        SOME prop => prop
   143                      | NONE => error ("Unknown axiom " ^ quote name))
   144                  in PAxm (name, prop, NONE) end
   145              | "thm" :: xs =>
   146                  let val name = NameSpace.pack xs;
   147                  in (case assoc (thms, name) of
   148                      SOME thm => fst (strip_combt (Thm.proof_of thm))
   149                    | NONE => (case Symtab.lookup (tab, name) of
   150                          SOME prf => prf
   151                        | NONE => error ("Unknown theorem " ^ quote name)))
   152                  end
   153              | _ => error ("Illegal proof constant name: " ^ quote s))
   154       | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
   155       | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
   156       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
   157           Abst (s, if ty then SOME T else NONE,
   158             incr_pboundvars (~1) 0 (prf_of [] prf))
   159       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
   160           AbsP (s, case t of
   161                 Const ("dummy_pattern", _) => NONE
   162               | _ $ Const ("dummy_pattern", _) => NONE
   163               | _ => SOME (mk_term t),
   164             incr_pboundvars 0 (~1) (prf_of [] prf))
   165       | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
   166           prf_of [] prf1 %% prf_of [] prf2
   167       | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
   168           prf_of (T::Ts) prf
   169       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
   170           (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
   171       | prf_of _ t = error ("Not a proof term:\n" ^
   172           Sign.string_of_term (sign_of thy) t)
   173 
   174   in prf_of [] end;
   175 
   176 
   177 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
   178 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
   179 val Hypt = Const ("Hyp", propT --> proofT);
   180 val Oraclet = Const ("Oracle", propT --> proofT);
   181 val MinProoft = Const ("MinProof", proofT);
   182 
   183 val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt",
   184   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   185 
   186 fun term_of _ (PThm ((name, _), _, _, NONE)) =
   187       Const (add_prefix "thm" name, proofT)
   188   | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
   189       mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
   190   | term_of _ (PAxm (name, _, NONE)) = Const (add_prefix "axm" name, proofT)
   191   | term_of _ (PAxm (name, _, SOME Ts)) =
   192       mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
   193   | term_of _ (PBound i) = Bound i
   194   | term_of Ts (Abst (s, opT, prf)) = 
   195       let val T = getOpt (opT,dummyT)
   196       in Const ("Abst", (T --> proofT) --> proofT) $
   197         Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
   198       end
   199   | term_of Ts (AbsP (s, t, prf)) =
   200       AbsPt $ getOpt (t, Const ("dummy_pattern", propT)) $
   201         Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   202   | term_of Ts (prf1 %% prf2) =
   203       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   204   | term_of Ts (prf % opt) = 
   205       let val t = getOpt (opt, Const ("dummy_pattern", dummyT))
   206       in Const ("Appt",
   207         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
   208           term_of Ts prf $ t
   209       end
   210   | term_of Ts (Hyp t) = Hypt $ t
   211   | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
   212   | term_of Ts (MinProof _) = MinProoft;
   213 
   214 val term_of_proof = term_of [];
   215 
   216 fun cterm_of_proof thy prf =
   217   let
   218     val (prf', tab) = disambiguate_names thy prf;
   219     val thys = thy :: Theory.ancestors_of thy;
   220     val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys))) @
   221       map fst (Symtab.dest tab);
   222     val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
   223     val sg = sign_of thy |>
   224       add_proof_syntax |>
   225       add_proof_atom_consts
   226         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   227   in
   228     (cterm_of sg (term_of_proof prf'),
   229      proof_of_term thy tab true o Thm.term_of)
   230   end;
   231 
   232 fun read_term thy =
   233   let
   234     val thys = thy :: Theory.ancestors_of thy;
   235     val thm_names = filter_out (equal "") (map fst (List.concat (map thms_of thys)));
   236     val axm_names = map fst (List.concat (map (Symtab.dest o #axioms o rep_theory) thys));
   237     val sg = sign_of thy |>
   238       add_proof_syntax |>
   239       add_proof_atom_consts
   240         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   241   in
   242     (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   243   end;
   244 
   245 fun read_proof thy =
   246   let val rd = read_term thy proofT
   247   in
   248     (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
   249   end;
   250 
   251 fun pretty_proof sg prf =
   252   let
   253     val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
   254     val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
   255     val sg' = sg |>
   256       add_proof_syntax |>
   257       add_proof_atom_consts
   258         (map (add_prefix "thm") thm_names @ map (add_prefix "axm") axm_names)
   259   in
   260     Sign.pretty_term sg' (term_of_proof prf)
   261   end;
   262 
   263 fun pretty_proof_of full thm =
   264   let
   265     val {sign, der = (_, prf), prop, ...} = rep_thm thm;
   266     val prf' = (case strip_combt (fst (strip_combP prf)) of
   267         (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
   268       | _ => prf)
   269   in
   270     pretty_proof sign
   271       (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   272   end;
   273 
   274 val print_proof_of = Pretty.writeln oo pretty_proof_of;
   275 
   276 end;