Compiler.Parser

2305def termSpelling =
2306  (lambda unrestricted term : (family Term) .
2307    (eliminate
2308      Term
2309      (lambda unrestricted value : (family Term) . (family TermSpellingResult))
2310      term
2311      (branch Variable spelling . (constructor TermSpellingResult TermSpellingDecoded spelling))
2312      (branch Universe level . (constructor TermSpellingResult TermHasNoSpelling))
2313      (branch NaturalType . (constructor TermSpellingResult TermHasNoSpelling))
2314      (branch NaturalZero . (constructor TermSpellingResult TermHasNoSpelling))
2315      (branch
2316        NaturalLiteral
2317        naturalLiteralValue
2318        .
2319        (constructor TermSpellingResult TermHasNoSpelling))
2320      (branch
2321        NaturalSuccessor
2322        predecessor
2323        ih_predecessor
2324        .
2325        (constructor TermSpellingResult TermHasNoSpelling))
2326      (branch
2327        Application
2328        function
2329        argument
2330        ih_function
2331        ih_argument
2332        .
2333        (constructor TermSpellingResult TermHasNoSpelling))
2334      (branch
2335        NaturalArithmetic
2336        operation
2337        function
2338        argument
2339        ih_function
2340        ih_argument
2341        .
2342        (constructor TermSpellingResult TermHasNoSpelling))
2343      (branch
2344        Lambda
2345        quantityTag
2346        binderSpelling
2347        domain
2348        body
2349        ih_domain
2350        ih_body
2351        .
2352        (constructor TermSpellingResult TermHasNoSpelling))
2353      (branch
2354        Pi
2355        quantityTag
2356        binderSpelling
2357        domain
2358        codomain
2359        ih_domain
2360        ih_codomain
2361        .
2362        (constructor TermSpellingResult TermHasNoSpelling))
2363      (branch BytesType . (constructor TermSpellingResult TermHasNoSpelling))
2364      (branch BytesLiteral bytesValue . (constructor TermSpellingResult TermHasNoSpelling))
2365      (branch ByteType . (constructor TermSpellingResult TermHasNoSpelling))
2366      (branch ByteLiteral byteValue . (constructor TermSpellingResult TermHasNoSpelling))
2367      (branch TermSequenceEnd . (constructor TermSpellingResult TermHasNoSpelling))
2368      (branch
2369        TermSequenceNext
2370        sequenceHead
2371        sequenceTail
2372        ih_sequenceHead
2373        ih_sequenceTail
2374        .
2375        (constructor TermSpellingResult TermHasNoSpelling))
2376      (branch
2377        TermEliminatorBranch
2378        constructorSpelling
2379        binderNames
2380        body
2381        ih_binderNames
2382        ih_body
2383        .
2384        (constructor TermSpellingResult TermHasNoSpelling))
2385      (branch
2386        FamilyApplication
2387        familySpelling
2388        familyArguments
2389        ih_familyArguments
2390        .
2391        (constructor TermSpellingResult TermHasNoSpelling))
2392      (branch
2393        ConstructorApplication
2394        familySpelling
2395        constructorSpelling
2396        constructorArguments
2397        ih_constructorArguments
2398        .
2399        (constructor TermSpellingResult TermHasNoSpelling))
2400      (branch
2401        Eliminator
2402        eliminatedFamilySpelling
2403        motive
2404        scrutinee
2405        branches
2406        ih_motive
2407        ih_scrutinee
2408        ih_branches
2409        .
2410        (constructor TermSpellingResult TermHasNoSpelling))
2411      (branch
2412        Match
2413        family
2414        scrutinee
2415        branches
2416        ih_scrutinee
2417        ih_branches
2418        .
2419        (constructor TermSpellingResult TermHasNoSpelling))
2420      (branch
2421        MatchWith
2422        family
2423        motive
2424        scrutinee
2425        branches
2426        ih_motive
2427        ih_scrutinee
2428        ih_branches
2429        .
2430        (constructor TermSpellingResult TermHasNoSpelling))
2431      (branch
2432        IntegerLiteral
2433        integerLiteralSpelling
2434        .
2435        (constructor TermSpellingResult TermHasNoSpelling))
2436      (branch
2437        RecordConstruction
2438        name
2439        origin
2440        bindings
2441        ih_bindings
2442        .
2443        (constructor TermSpellingResult TermHasNoSpelling))
2444      (branch
2445        RecordAssignment
2446        name
2447        origin
2448        value
2449        ih_value
2450        .
2451        (constructor TermSpellingResult TermHasNoSpelling))
2452      (branch
2453        RecordProjection
2454        name
2455        field
2456        origin
2457        value
2458        ih_value
2459        .
2460        (constructor TermSpellingResult TermHasNoSpelling))
2461      (branch
2462        RecordUpdate
2463        name
2464        origin
2465        value
2466        bindings
2467        ih_value
2468        ih_bindings
2469        .
2470        (constructor TermSpellingResult TermHasNoSpelling))
2471      (branch
2472        LocalLet
2473        quantity
2474        binder
2475        hasAnnotation
2476        annotation
2477        value
2478        body
2479        ih_annotation
2480        ih_value
2481        ih_body
2482        .
2483        (constructor TermSpellingResult TermHasNoSpelling))
2484      (branch
2485        DoBlock
2486        effects
2487        result
2488        body
2489        ih_effects
2490        ih_result
2491        ih_body
2492        .
2493        (constructor TermSpellingResult TermHasNoSpelling))
2494      (branch
2495        DoStep
2496        named
2497        quantity
2498        binder
2499        computation
2500        continuation
2501        ih_computation
2502        ih_continuation
2503        .
2504        (constructor TermSpellingResult TermHasNoSpelling))
2505      (branch DoReturn value ih_value . (constructor TermSpellingResult TermHasNoSpelling))))