merged
authorwenzelm
Tue Dec 03 19:32:26 2019 +0100 (2 days ago)
changeset 71223d411d5c84a4b
parent 71220 6f8422385878
parent 71222 2bc39c80a95d
child 71224 54a7ad860a76
merged
     1.1 --- a/src/Pure/Thy/export_theory.ML	Tue Dec 03 16:12:20 2019 +0100
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Dec 03 19:32:26 2019 +0100
     1.3 @@ -55,18 +55,6 @@
     1.4    (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
     1.5  
     1.6  
     1.7 -(* spec rules *)
     1.8 -
     1.9 -fun primrec_types ctxt const =
    1.10 -  Spec_Rules.retrieve ctxt (Const const)
    1.11 -  |> get_first
    1.12 -    (#rough_classification #>
    1.13 -      (fn Spec_Rules.Equational (Spec_Rules.Primrec types) => SOME (types, false)
    1.14 -        | Spec_Rules.Equational (Spec_Rules.Primcorec types) => SOME (types, true)
    1.15 -        | _ => NONE))
    1.16 -  |> the_default ([], false);
    1.17 -
    1.18 -
    1.19  (* locales *)
    1.20  
    1.21  fun locale_content thy loc =
    1.22 @@ -216,23 +204,19 @@
    1.23      val encode_term = Term_XML.Encode.term consts;
    1.24  
    1.25      val encode_const =
    1.26 -      let open XML.Encode Term_XML.Encode in
    1.27 -        pair encode_syntax
    1.28 -          (pair (list string)
    1.29 -            (pair typ (pair (option encode_term) (pair bool (pair (list string) bool)))))
    1.30 -      end;
    1.31 +      let open XML.Encode Term_XML.Encode
    1.32 +      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
    1.33  
    1.34      fun export_const c (T, abbrev) =
    1.35        let
    1.36          val syntax = get_syntax_const thy_ctxt c;
    1.37          val U = Logic.unvarifyT_global T;
    1.38          val U0 = Type.strip_sorts U;
    1.39 -        val recursion = primrec_types thy_ctxt (c, U);
    1.40          val abbrev' = abbrev
    1.41            |> Option.map (Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts);
    1.42          val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
    1.43          val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
    1.44 -      in encode_const (syntax, (args, (U0, (abbrev', (propositional, recursion))))) end;
    1.45 +      in encode_const (syntax, (args, (U0, (abbrev', propositional)))) end;
    1.46  
    1.47      val _ =
    1.48        export_entities "consts" (SOME oo export_const) Sign.const_space
     2.1 --- a/src/Pure/Thy/export_theory.scala	Tue Dec 03 16:12:20 2019 +0100
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Tue Dec 03 19:32:26 2019 +0100
     2.3 @@ -284,9 +284,7 @@
     2.4      typargs: List[String],
     2.5      typ: Term.Typ,
     2.6      abbrev: Option[Term.Term],
     2.7 -    propositional: Boolean,
     2.8 -    primrec_types: List[String],
     2.9 -    corecursive: Boolean)
    2.10 +    propositional: Boolean)
    2.11    {
    2.12      def cache(cache: Term.Cache): Const =
    2.13        Const(entity.cache(cache),
    2.14 @@ -294,25 +292,22 @@
    2.15          typargs.map(cache.string(_)),
    2.16          cache.typ(typ),
    2.17          abbrev.map(cache.term(_)),
    2.18 -        propositional,
    2.19 -        primrec_types.map(cache.string(_)),
    2.20 -        corecursive)
    2.21 +        propositional)
    2.22    }
    2.23  
    2.24    def read_consts(provider: Export.Provider): List[Const] =
    2.25      provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
    2.26        {
    2.27          val (entity, body) = decode_entity(Kind.CONST, tree)
    2.28 -        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
    2.29 +        val (syntax, (typargs, (typ, (abbrev, propositional)))) =
    2.30          {
    2.31            import XML.Decode._
    2.32            pair(decode_syntax,
    2.33              pair(list(string),
    2.34                pair(Term_XML.Decode.typ,
    2.35 -                pair(option(Term_XML.Decode.term), pair(bool,
    2.36 -                  pair(list(string), bool))))))(body)
    2.37 +                pair(option(Term_XML.Decode.term), bool))))(body)
    2.38          }
    2.39 -        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
    2.40 +        Const(entity, syntax, typargs, typ, abbrev, propositional)
    2.41        })
    2.42  
    2.43  
     3.1 --- a/src/Pure/term.scala	Tue Dec 03 16:12:20 2019 +0100
     3.2 +++ b/src/Pure/term.scala	Tue Dec 03 19:32:26 2019 +0100
     3.3 @@ -53,6 +53,13 @@
     3.4    val dummyT = Type("dummy")
     3.5  
     3.6    sealed abstract class Term
     3.7 +  {
     3.8 +    def head: Term =
     3.9 +      this match {
    3.10 +        case App(fun, _) => fun.head
    3.11 +        case _ => this
    3.12 +      }
    3.13 +  }
    3.14    case class Const(name: String, typargs: List[Typ] = Nil) extends Term
    3.15    {
    3.16      override def toString: String =