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