12570def inferCore :
12571 (pi unrestricted term : (family CoreTerm) .
12572 (pi unrestricted context : (family TypeContext) . (family CoreInferenceResult))) =
12573 (lambda unrestricted term : (family CoreTerm) .
12574 (eliminate
12575 CoreTerm
12576 (lambda unrestricted value : (family CoreTerm) .
12577 (pi unrestricted context : (family TypeContext) . (family CoreInferenceResult)))
12578 term
12579 (branch
12580 CoreUniverse
12581 level
12582 .
12583 (lambda unrestricted context : (family TypeContext) .
12584 (constructor
12585 CoreInferenceResult
12586 CoreInferred
12587 (constructor CoreTerm CoreUniverse (succ level)))))
12588 (branch
12589 CoreNatural
12590 .
12591 (lambda unrestricted context : (family TypeContext) .
12592 (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero))))
12593 (branch
12594 CoreNaturalLiteral
12595 value
12596 .
12597 (lambda unrestricted context : (family TypeContext) . (inferCoreNaturalMagnitude value)))
12598 (branch
12599 CoreBound
12600 index
12601 .
12602 (lambda unrestricted context : (family TypeContext) .
12603 (eliminate
12604 TypeLookupResult
12605 (lambda unrestricted result : (family TypeLookupResult) . (family CoreInferenceResult))
12606 (lookupType context index)
12607 (branch
12608 TypeFound
12609 variableType
12610 .
12611 (constructor CoreInferenceResult CoreInferred variableType))
12612 (branch
12613 TypeNotFound
12614 missingIndex
12615 .
12616 (constructor CoreInferenceResult CoreInferenceFailed (succ zero))))))
12617 (branch
12618 CorePi
12619 multiplicity
12620 domain
12621 codomain
12622 ih_domain
12623 ih_codomain
12624 .
12625 (lambda unrestricted context : (family TypeContext) .
12626 (inferPiType
12627 multiplicity
12628 (ih_domain context)
12629 (ih_codomain (constructor TypeContext TypeContextBinding domain context)))))
12630 (branch
12631 CoreLambda
12632 multiplicity
12633 domain
12634 body
12635 ih_domain
12636 ih_body
12637 .
12638 (lambda unrestricted context : (family TypeContext) .
12639 (inferLambdaType
12640 multiplicity
12641 domain
12642 (ih_domain context)
12643 (ih_body (constructor TypeContext TypeContextBinding domain context)))))
12644 (branch
12645 CoreLet
12646 multiplicity
12647 annotation
12648 value
12649 body
12650 ih_annotation
12651 ih_value
12652 ih_body
12653 .
12654 (lambda unrestricted context : (family TypeContext) .
12655 (finishInferCoreLetAnnotation
12656 annotation
12657 value
12658 (ih_annotation context)
12659 (ih_value context)
12660 (ih_body (constructor TypeContext TypeContextBinding annotation context)))))
12661 (branch
12662 CoreApplication
12663 function
12664 argument
12665 ih_function
12666 ih_argument
12667 .
12668 (lambda unrestricted context : (family TypeContext) .
12669 (inferCoreApplicationWithEffects
12670 function
12671 argument
12672 (ih_function context)
12673 (ih_argument context))))
12674 (branch
12675 CoreNaturalArithmetic
12676 operation
12677 function
12678 argument
12679 ih_function
12680 ih_argument
12681 .
12682 (lambda unrestricted context : (family TypeContext) .
12683 (inferCoreArithmeticOperands
12684 operation
12685 function
12686 argument
12687 (ih_function context)
12688 (ih_argument context))))
12689 (branch
12690 CoreNaturalSuccessor
12691 predecessor
12692 ih_predecessor
12693 .
12694 (lambda unrestricted context : (family TypeContext) .
12695 (inferNaturalSuccessorType (ih_predecessor context))))
12696 (branch
12697 CoreByte
12698 .
12699 (lambda unrestricted context : (family TypeContext) .
12700 (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero))))
12701 (branch
12702 CoreByteLiteral
12703 value
12704 .
12705 (lambda unrestricted context : (family TypeContext) .
12706 (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreByte))))
12707 (branch
12708 CoreBytes
12709 .
12710 (lambda unrestricted context : (family TypeContext) .
12711 (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreUniverse zero))))
12712 (branch
12713 CoreBytesLiteral
12714 value
12715 .
12716 (lambda unrestricted context : (family TypeContext) .
12717 (constructor CoreInferenceResult CoreInferred (constructor CoreTerm CoreBytes))))
12718 (branch
12719 CorePrimitiveTerm
12720 primitive
12721 .
12722 (lambda unrestricted context : (family TypeContext) .
12723 (constructor CoreInferenceResult CoreInferred (corePrimitiveType primitive))))
12724 (branch
12725 CoreTermSequenceEnd
12726 .
12727 (lambda unrestricted context : (family TypeContext) .
12728 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))
12729 (branch
12730 CoreTermSequenceNext
12731 head
12732 tail
12733 ih_head
12734 ih_tail
12735 .
12736 (lambda unrestricted context : (family TypeContext) .
12737 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))
12738 (branch
12739 CoreFamilyApplication
12740 familyName
12741 arguments
12742 ih_arguments
12743 .
12744 (lambda unrestricted context : (family TypeContext) .
12745 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))
12746 (branch
12747 CoreConstructorApplication
12748 familyName
12749 constructorName
12750 arguments
12751 ih_arguments
12752 .
12753 (lambda unrestricted context : (family TypeContext) .
12754 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))
12755 (branch
12756 CoreEliminatorBranch
12757 constructorName
12758 binderCount
12759 body
12760 ih_body
12761 .
12762 (lambda unrestricted context : (family TypeContext) .
12763 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))
12764 (branch
12765 CoreEliminator
12766 familyName
12767 motive
12768 scrutinee
12769 branches
12770 ih_motive
12771 ih_scrutinee
12772 ih_branches
12773 .
12774 (lambda unrestricted context : (family TypeContext) .
12775 (constructor CoreInferenceResult CoreInferenceFailed coreFamilyInferenceFailureCode)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.