up

chester-lang · Sep 17, 2024 · 37ef65b · 37ef65b
1 parent ddd0f60
commit 37ef65b
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 10 deletions.
diff --git a/core/shared/src/main/scala/chester/error/TyckError.scala b/core/shared/src/main/scala/chester/error/TyckError.scala
@@ -194,4 +194,7 @@ case class EffectUnifyError(lhs: Effects, rhs: Judge) extends TyckError {
 
 case class UnexpectedTelescope(cause: MaybeTelescope) extends TyckError {
   override def toDoc(implicit options: PrettierOptions = PrettierOptions.Default): Doc = t"Unexpected telescope"
+}
+case class NotAFunctionError(cause: Expr) extends TyckError {
+  override def toDoc(implicit options: PrettierOptions = PrettierOptions.Default): Doc = t"Expected a function, but got ${cause}"
 }
diff --git a/core/shared/src/main/scala/chester/syntax/core/Term.scala b/core/shared/src/main/scala/chester/syntax/core/Term.scala
@@ -372,14 +372,14 @@ case class ObjectClauseValueTerm(key: Term, value: Term)derives ReadWriter {
 
 case class ObjectTerm(clauses: Vector[ObjectClauseValueTerm]) extends Term {
   override def toDoc(implicit options: PrettierOptions): Doc =
-    Doc.wrapperlist(Docs.`{`, Docs.`}`, ",")(clauses.map(_.toDoc)*)
+    Doc.wrapperlist(Docs.`{`, Docs.`}`, ",")(clauses.map(_.toDoc) *)
 }
 
 
 // exactFields is a hint: subtype relationship should not include different number of fields. Otherwise, throw a warning (only warning no error)
 case class ObjectType(fieldTypes: Vector[ObjectClauseValueTerm], exactFields: Boolean = false) extends Term {
   override def toDoc(implicit options: PrettierOptions): Doc =
-    Doc.wrapperlist("Object" </> Docs.`{`, Docs.`}`, ",")(fieldTypes.map(_.toDoc)*)
+    Doc.wrapperlist("Object" </> Docs.`{`, Docs.`}`, ",")(fieldTypes.map(_.toDoc) *)
 }
 
 sealed trait Builtin extends Term derives ReadWriter
@@ -397,7 +397,7 @@ case class ListType(ty: Term) extends Constructed with TypeTerm {
 case class Union(xs: Vector[Term]) extends TypeTerm {
   require(xs.nonEmpty)
 
-  override def toDoc(implicit options: PrettierOptions): Doc = Doc.wrapperlist(Docs.`(`, Docs.`)`, " | ")(xs*)
+  override def toDoc(implicit options: PrettierOptions): Doc = Doc.wrapperlist(Docs.`(`, Docs.`)`, " | ")(xs *)
 }
 
 
@@ -423,7 +423,7 @@ object Union {
 case class Intersection(xs: Vector[Term]) extends TypeTerm derives ReadWriter {
   require(xs.nonEmpty)
 
-  override def toDoc(implicit options: PrettierOptions): Doc = Doc.wrapperlist(Docs.`(`, Docs.`)`, " & ")(xs*)
+  override def toDoc(implicit options: PrettierOptions): Doc = Doc.wrapperlist(Docs.`(`, Docs.`)`, " & ")(xs *)
 }
 
 object Intersection {
@@ -447,7 +447,7 @@ case class Effects private[syntax](effects: Map[Effect, Vector[LocalVar]]) exten
   override def toDoc(implicit options: PrettierOptions): Doc =
     Doc.wrapperlist(Docs.`[`, Docs.`]`, ",")(effects.map { case (effect, names) =>
       Doc.text(s"${effect.toDoc} -> ${names.map(_.toDoc).mkString(", ")}")
-    }.toSeq*)
+    }.toSeq *)
 
   def descentEffects(f: Effect => Effect): Effects =
     Effects(effects.map { case (effect, names) => f(effect) -> names })
@@ -476,6 +476,7 @@ case class Effects private[syntax](effects: Map[Effect, Vector[LocalVar]]) exten
     })
 
   def isEmpty: Boolean = effects.isEmpty
+
   def nonEmpty: Boolean = effects.nonEmpty
 }
 
@@ -533,6 +534,8 @@ case class ErrorTerm(val error: TyckError) extends Term {
   override def toDoc(implicit options: PrettierOptions): Doc = error.toDoc
 }
 
+def ErrorType(error: TyckError): ErrorTerm = ErrorTerm(error)
+
 case class MetaTerm(description: String, uniqId: UniqId, ty: Term, effect: Effects = NoEffect, meta: OptionTermMeta = None) extends Term with HasUniqId {
   override def toDoc(implicit options: PrettierOptions): Doc = Doc.text("MetaTerm#" + uniqId)
 }

diff --git a/core/shared/src/main/scala/chester/tyck/FunctionTycker.scala b/core/shared/src/main/scala/chester/tyck/FunctionTycker.scala
@@ -78,21 +78,25 @@ trait FunctionTycker[Self <: TyckerBase[Self] & FunctionTycker[Self] & EffTycker
     //val result = Judge(Function(funcTy, body.wellTyped), funcTy, NoEffect)
     this.cleanupFunction(Function(funcTy, body.wellTyped))
   }
-
-  def checkCallingTelescope(f: FunctionType, telescope: Vector[MaybeTelescope], effects: Option[Effects]) = ???
+  
+  def synthesizeCall(function: Judge, fTy: FunctionType, telescopes: Vector[DesaltCallingTelescope], effects: Option[Effects]): Judge = ???
 
   def synthesizeFunctionCall(call: DesaltFunctionCall, effects: Option[Effects]): Judge = {
     val function = this.synthesize(call.function, effects)
     function.ty match {
-      case fty: FunctionType => ???
+      case fty: FunctionType => 
+        synthesizeCall(function, fty, call.telescopes, effects)
       case i: Intersection => {
         val fs = i.xs.filter {
           case f: FunctionType => true
           case _ => false
         }
-        ???
+        tryAll(fs.map(fty => _.synthesizeCall(function, fty.asInstanceOf[FunctionType], call.telescopes, effects)))
       }
-      case _ => ???
+      case _ => 
+        val error = NotAFunctionError(call)
+        tyck.report(error)
+        Judge(ErrorTerm(error), ErrorType(error), NoEffect)
     }
   }