package Ġarrow . meta . plugins . pro ofs . ph ases Ċ Ċ import Ġarrow . meta . dsl . platform . cli Ċ import Ġarrow . meta . ph ases . Compiler Context Ċ import Ġarrow . meta . ph ases . analysis . diagnostic . Proof Renderer Ċ import Ġarrow . meta . ph ases . resolve . base Line Type Checker Ċ import Ġarrow . meta . plugins . pro ofs . ph ases . resolve . cache . initialize Proof Cache Ċ import Ġarrow . meta . plugins . pro ofs . ph ases . resolve . is Resolved Ċ import Ġarrow . meta . plugins . pro ofs . ph ases . resolve . matching Candidates Ċ import Ġarrow . meta . plugins . pro ofs . ph ases . resolve . scopes . discard Platform Base Object Fake Overrides Ċ import Ġarrow . meta . plugins . pro ofs . ph ases . resolve . skipped Pro ofs Due To Amb igu ities Ċ import Ġorg . jetbrains . kotlin . descriptors . Callable Member Descriptor Ċ import Ġorg . jetbrains . kotlin . descriptors . Declaration Descriptor With Visibility Ċ import Ġorg . jetbrains . kotlin . descriptors . Descriptor Vis ibilities Ċ import Ġorg . jetbrains . kotlin . descriptors . Module Descriptor Ċ import Ġorg . jetbrains . kotlin . descriptors . annotations . Annotated Ċ import Ġorg . jetbrains . kotlin . descriptors . annotations . Annotation Descriptor Ċ import Ġorg . jetbrains . kotlin . descriptors . impl . Module Descriptor Impl Ċ import Ġorg . jetbrains . kotlin . name . Fq Name Ċ import Ġorg . jetbrains . kotlin . name . Name Ċ import Ġorg . jetbrains . kotlin . psi . Kt Annotated Ċ import Ġorg . jetbrains . kotlin . resolve . Binding Context Ċ import Ġorg . jetbrains . kotlin . resolve . Binding Trace Ċ import Ġorg . jetbrains . kotlin . resolve . descriptor Util . fq Name Safe Ċ import Ġorg . jetbrains . kotlin . types . Kotlin Type Ċ import Ġorg . jetbrains . kotlin . utils . addTo Std lib . safe As Ċ Ċ val ĠArrow Extension Proof : ĠF q Name Ġ= ĠF q Name (" arrow . Extension ") Ċ val ĠArrow Given Proof : ĠF q Name Ġ= ĠF q Name (" arrow . Given ") Ċ val ĠArrow Co erc ion Proof : ĠF q Name Ġ= ĠF q Name (" arrow . Co erc ion ") Ċ val ĠArrow Ref inement Proof : ĠF q Name Ġ= ĠF q Name (" arrow . Ref inement ") Ċ val ĠArrow Ref ined By : ĠF q Name Ġ= ĠF q Name (" arrow . Ref ined By ") Ċ val ĠArrow Ref ined : ĠF q Name Ġ= ĠF q Name (" arrow . Ref ined ") Ċ Ċ val ĠArrow Proof Set : ĠSet < Fq Name > Ġ= Ġset Of ( ĊĠ ĠArrow Extension Proof , ĊĠ ĠArrow Given Proof , ĊĠ ĠArrow Co erc ion Proof , ĊĠ ĠArrow Ref inement Proof , ĊĠ ĠArrow Ref ined By Ċ ) Ċ Ċ fun ĠK t Annotated . is Proof ( trace : ĠBinding Trace ): ĠBoolean Ġ= ĊĠ ĠArrow Proof Set . any Ġ{ Ġhas Annotation ( trace , Ġit ) Ġ} Ċ Ċ fun ĠK t Annotated . is Proof ( ctx : ĠBinding Context ): ĠBoolean Ġ= ĊĠ ĠArrow Proof Set . any Ġ{ Ġhas Annotation ( ctx , Ġit ) Ġ} Ċ Ċ fun ĠK t Annotated . annotations ( trace : ĠBinding Trace ): ĠList < Annotation Descriptor > Ġ= ĊĠ Ġannotation Entries . map NotNull Ġ{ Ġtrace . get ( Binding Context . AN NOT ATION , Ġit ) Ġ} Ċ Ċ fun ĠK t Annotated . annotations ( ctx : ĠBinding Context ): ĠList < Annotation Descriptor > Ġ= ĊĠ Ġannotation Entries . map NotNull Ġ{ Ġctx . get ( Binding Context . AN NOT ATION , Ġit ) Ġ} Ċ Ċ fun ĠK t Annotated . has Annotation ( trace : ĠBinding Trace , Ġfq Name : ĠF q Name ): ĠBoolean Ġ= ĊĠ Ġannotations ( trace ). any Ġ{ Ġit . fq Name Ġ== Ġfq Name Ġ} Ċ Ċ fun ĠK t Annotated . has Annotation ( ctx : ĠBinding Context , Ġfq Name : ĠF q Name ): ĠBoolean Ġ= ĊĠ Ġannotations ( ctx ). any Ġ{ Ġit . fq Name Ġ== Ġfq Name Ġ} Ċ Ċ fun ĠAnnot ated . is Proof (): ĠBoolean Ġ= ĊĠ ĠArrow Proof Set . any ( annotations :: has Annotation ) Ċ Ċ fun ĠCompiler Context . ext ending ( types : ĠCollection < Kotlin Type >): ĠList < Extension Proof > Ġ= ĊĠ Ġtypes . flatMap Ġ{ Ġextension Pro ofs ( it , Ġit . constructor . built Ins . nullable Any Type ) Ġ} Ċ Ċ fun ĠPro of . call ables ( descriptor Name Filter : Ġ( Name ) Ġ-> ĠBoolean Ġ= Ġ{ Ġtrue Ġ}): ĠList < Callable Member Descriptor > Ġ= ĊĠ Ġto . member Scope ĊĠĠĠ Ġ. get Cont ributed Descriptors ( name Filter Ġ= Ġdescriptor Name Filter ) ĊĠĠĠ Ġ. toList () ĊĠĠĠ Ġ. filter Is Instance < Callable Member Descriptor >() ĊĠĠĠ Ġ. map NotNull ( Callable Member Descriptor :: discard Platform Base Object Fake Overrides ) Ċ Ċ fun ĠCompiler Context . extension Proof ( sub Type : ĠKotlin Type , Ġsuper Type : ĠKotlin Type ): ĠExtension Proof ? Ġ= ĊĠ Ġextension Proof Candidate ( extension Pro ofs ( sub Type , Ġsuper Type )) Ċ Ċ fun ĠCompiler Context . extension Proof Candidate ( candidates : ĠList < Extension Proof >): ĠExtension Proof ? Ġ= ĊĠ Ġcandidates ĊĠĠĠ Ġ. filter Ġ{ ĊĠĠĠĠĠ Ġextension Pro ofs (). skipped Pro ofs Due To Amb igu ities () ĊĠĠĠĠĠĠĠ Ġ. first OrNull Ġ{ Ġ( p , Ġ_) Ġ-> Ġp Ġ== Ġit Ġ} Ġ== Ġnull ĊĠĠĠ Ġ}. min By OrNull Ġ{ Ġit . through . visibility Ġ!= ĠDescriptor Vis ibilities . INTERNAL Ġ} Ċ Ċ fun ĠCompiler Context . extension Pro ofs ( sub Type : ĠKotlin Type , Ġsuper Type : ĠKotlin Type ): ĠList < Extension Proof > Ġ= ĊĠ Ġproof < Extension Proof >(). matching Candidates ( this , Ġsub Type , Ġsuper Type ) Ċ Ċ fun ĠCompiler Context . given Proof ( super Type : ĠKotlin Type ): ĠGiven Proof ? Ġ= ĊĠ Ġgiven Proof Candidate ( given Pro ofs ( super Type )) Ċ Ċ fun ĠCompiler Context . given Pro ofs ( super Type : ĠKotlin Type ): ĠList < Given Proof > Ġ= ĊĠ Ġproof < Given Proof >(). matching Candidates ( this , Ġsuper Type ) Ċ Ċ fun ĠCompiler Context . given Proof Candidate ( candidates : ĠList < Given Proof >): ĠGiven Proof ? Ġ= ĊĠ Ġcandidates ĊĠĠĠ Ġ. filter Ġ{ ĊĠĠĠĠĠ Ġit . is Resolved ( given Pro ofs ()) Ġ&& ĊĠĠĠĠĠĠĠ Ġgiven Pro ofs (). skipped Pro ofs Due To Amb igu ities () ĊĠĠĠĠĠĠĠĠĠ Ġ. first OrNull Ġ{ Ġ( p , Ġ_) Ġ-> Ġp Ġ== Ġit Ġ} Ġ== Ġnull ĊĠĠĠ Ġ}. min By OrNull Ġ{ Ġit . through . safe As < Declaration Descriptor With Visibility >() ?. visibility Ġ!= ĠDescriptor Vis ibilities . INTERNAL Ġ} Ċ Ċ inline Ġfun Ġ< re ified ĠP Ġ: ĠPro of > ĠCompiler Context . proof (): ĠList < P > Ġ= ĊĠ Ġmodule ?. pro ofs ( this )?. filter Is Instance < P >() !! Ċ Ċ /** Ċ Ġ* Ġreturns Ġa ĠMap , Ġwhere Ġthe Ġkeys Ġare Ġfrom Ġ[ Kotlin Type ] Ġ-> Ġto Ġ[ Kotlin Type ] Ġand Ġthe Ġvalues Ġare Ġthe Ġcorresponding ĠPro ofs Ċ Ġ*/ Ċ fun ĠCompiler Context . extension Pro ofs (): ĠMap < Pair < Kotlin Type , ĠKotlin Type >, ĠList < Extension Proof >> Ġ= ĊĠ Ġproof < Extension Proof >() ĊĠĠĠ Ġ. fold ( mutable Map Of < Pair < Kotlin Type , ĠKotlin Type >, ĠList < Extension Proof >> ()) Ġ{ Ġacc , Ġproof Ġ-> ĊĠĠĠĠĠ Ġval Ġkey Ġ= Ġproof . from Ġto Ġproof . to ĊĠĠĠĠĠ Ġacc . apply Ġ{ ĊĠĠĠĠĠĠĠ Ġif Ġ( acc . containsKey ( key )) Ġacc [ key ] Ġ= Ġacc [ key ]. or Empty () Ġ+ Ġproof ĊĠĠĠĠĠĠĠ Ġelse Ġacc [ key ] Ġ= ĠlistOf ( proof ) ĊĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ}. toMap () Ċ Ċ /** Ċ Ġ* Ġreturns Ġa ĠMap , Ġwhere Ġthe Ġkeys Ġare Ġ[ Kotlin Type ] Ġand Ġthe Ġvalues Ġare Ċ Ġ* Ġall Ġcorresponding Ġpro ofs Ġwithout Ġref ining Ġthe Ġlist Ġas Ġit Ġis Ġdone Ġin Ġ[ given Pro ofs ]. Ċ Ġ*/ Ċ fun ĠCompiler Context . all Given Pro ofs (): ĠMap < Kotlin Type , ĠList < Given Proof >> Ġ= ĊĠ Ġproof < Given Proof >() ĊĠĠĠ Ġ. fold ( mutable Map Of < Kotlin Type , ĠList < Given Proof >> ()) Ġ{ Ġacc , Ġproof Ġ-> ĊĠĠĠĠĠ Ġval Ġkey Ġ= Ġproof . to ĊĠĠĠĠĠ Ġacc . apply Ġ{ ĊĠĠĠĠĠĠĠ Ġif Ġ( acc . containsKey ( key )) Ġacc [ key ] Ġ= Ġacc [ key ]. or Empty () Ġ+ Ġproof ĊĠĠĠĠĠĠĠ Ġelse Ġacc [ key ] Ġ= ĠlistOf ( proof ) ĊĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ}. toMap () Ċ Ċ /** Ċ Ġ* Ġcontr ary Ġto Ġ[ all Given Pro ofs ] Ġit Ġref ines Ġthe ĠList Ġas Ġit Ġis Ġdone Ġin Ġ[ given Pro ofs ] Ċ Ġ*/ Ċ fun ĠCompiler Context . given Pro ofs (): ĠMap < Kotlin Type , ĠList < Given Proof >> Ġ= ĊĠ Ġall Given Pro ofs () ĊĠĠĠ Ġ. map Values Ġ{ Ġ( type , Ġpro ofs ) Ġ-> ĊĠĠĠĠĠ Ġpro ofs . matching Candidates ( this , Ġtype ) ĊĠĠĠ Ġ}. filter Values Ġ{ Ġit . isNotEmpty () Ġ} Ċ Ċ fun ĠCompiler Context . coerce Proof ( sub Type : ĠKotlin Type , Ġsuper Type : ĠKotlin Type ): ĠCo erc ion Proof ? Ġ= ĊĠ Ġco erce Pro ofs ( sub Type , Ġsuper Type ). first OrNull () Ċ Ċ fun ĠCompiler Context . coerce Pro ofs ( sub Type : ĠKotlin Type , Ġsuper Type : ĠKotlin Type ): ĠList < Co erc ion Proof > Ġ= ĊĠ Ġproof < Co erc ion Proof >(). filter Ġ{ Ġit . coerce Ġ}. matching Candidates ( this , Ġsub Type , Ġsuper Type ) Ċ Ċ fun ĠCompiler Context ?. are Types Co er ced ( sub Type : ĠKotlin Type , Ġsup ertype : ĠKotlin Type ): ĠBoolean Ġ= ĊĠ Ġ! base Line Type Checker . is Subtype Of ( sub Type , Ġsup ertype ) Ġ&& Ġthis ?. coerce Proof ( sub Type , Ġsup ertype ) Ġ!= Ġnull Ċ Ċ fun ĠModule Descriptor . pro ofs ( ctx : ĠCompiler Context ): ĠList < Proof > Ġ= ĊĠ Ġif Ġ( this Ġis ĠModule Descriptor Impl ) Ġ{ ĊĠĠĠ Ġtry Ġ{ ĊĠĠĠĠĠ Ġval Ġcache Value Ġ= Ġctx . proof Cache [ this ] ĊĠĠĠĠĠ Ġwhen Ġ{ ĊĠĠĠĠĠĠĠ Ġcache Value Ġ!= Ġnull Ġ-> Ġ{ ĊĠĠĠĠĠĠĠĠĠ Ġcache Value . pro ofs ĊĠĠĠĠĠĠĠ Ġ} ĊĠĠĠĠĠĠĠ Ġelse Ġ-> Ġcli Ġ{ Ġinitialize Proof Cache ( ctx ) Ġ} Ġ?: Ġempty List () ĊĠĠĠĠĠ Ġ} ĊĠĠĠ Ġ} Ġcatch Ġ( e : ĠRuntimeException ) Ġ{ ĊĠĠĠĠĠ Ġprintln (" TODO () ĠDet ected Ġexception : Ġ${ e . printStackTrace () }") ĊĠĠĠĠĠ Ġempty List < Proof >() ĊĠĠĠ Ġ} ĊĠ Ġ} Ġelse Ġempty List () Ċ Ċ fun ĠPro of . asString (): ĠString Ġ= ĊĠ Ġwhen Ġ( this ) Ġ{ ĊĠĠĠ Ġis ĠGiven Proof Ġ-> Ġ" Given Proof Ġ${ through . fq Name Safe . asString ()} Ġon Ġthe Ġtype Ġ${ Proof Renderer . render Type ( to )}" ĊĠĠĠ Ġis ĠExtension Proof Ġ-> Ġ" Extension Proof Ġ${ through . fq Name Safe . asString ()} : Ġ${ Proof Renderer . render Type ( from )} Ġ-> Ġ${ Proof Renderer . render Type ( to )}" ĊĠ Ġ} Ċ