more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
authorwenzelm
Sat, 20 Jul 2019 11:48:30 +0200
changeset 70568 38ac2e714729
parent 70567 23ba5a638e6d
child 70569 8ce08b154aa1
more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
src/Pure/term.scala
--- a/src/Pure/term.scala	Sat Jul 20 11:17:54 2019 +0200
+++ b/src/Pure/term.scala	Sat Jul 20 11:48:30 2019 +0200
@@ -11,6 +11,8 @@
 
 object Term
 {
+  /* types and terms */
+
   type Indexname = (String, Int)
 
   type Sort = List[String]
@@ -31,6 +33,32 @@
   case class App(fun: Term, arg: Term) extends Term
 
 
+  /* type arguments of consts */
+
+  def const_typargs(name: String, typ: Typ, typargs: List[String], decl: Typ): List[Typ] =
+  {
+    var subst = Map.empty[String, Typ]
+
+    def bad_match(): Nothing = error("Malformed type instance for " + name + ": " + typ)
+    def raw_match(arg: (Typ, Typ))
+    {
+      arg match {
+        case (TFree(a, _), ty) =>
+          subst.get(a) match {
+            case None => subst += (a -> ty)
+            case Some(ty1) => if (ty != ty1) bad_match()
+          }
+        case (Type(c1, args1), Type(c2, args2)) if c1 == c2 =>
+          (args1 zip args2).foreach(raw_match)
+        case _ => bad_match()
+      }
+    }
+    raw_match(decl, typ)
+
+    typargs.map(subst)
+  }
+
+
 
   /** cache **/