Documentation

type T_Format_14 = Format Source #

d_Format_14 ∷ a Source #

type T_Input_16 = Input Source #

d_Input_16 ∷ a Source #

type T_ProgramN_18 = Program TyName Name DefaultUni DefaultFun SrcSpan Source #

d_ProgramN_18 ∷ a Source #

type T_Program_20 = Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun () Source #

d_Program_20 ∷ a Source #

d_convP_22 ∷ T_Program_20 → T_RawTm_32 Source #

d_deBruijnify_24 ∷ T_ProgramN_18 → T_Either_6 T_FreeVariableError_574 T_Program_20 Source #

type T_ProgramNU_26 = Program Name DefaultUni DefaultFun SrcSpan Source #

d_ProgramNU_26 ∷ a Source #

type T_ProgramU_28 = Program NamedDeBruijn DefaultUni DefaultFun () Source #

d_ProgramU_28 ∷ a Source #

d_deBruijnifyU_30 ∷ T_ProgramNU_26 → T_Either_6 T_FreeVariableError_574 T_ProgramU_28 Source #

d_convPU_32 ∷ T_ProgramU_28 → T_Untyped_210 Source #

d_BudgetMode_36 ∷ p → () Source #

type T_BudgetMode_36 a0 = BudgetMode a0 Source #

pattern C_Silent_40 ∷ BudgetMode a Source #

pattern C_Counting_42 ∷ a → BudgetMode a Source #

pattern C_Tallying_44 ∷ a → BudgetMode a Source #

check_Silent_40 ∷ ∀ xA. T_BudgetMode_36 xA Source #

check_Counting_42 ∷ ∀ xA. xA → T_BudgetMode_36 xA Source #

check_Tallying_44 ∷ ∀ xA. xA → T_BudgetMode_36 xA Source #

cover_BudgetMode_36 ∷ BudgetMode a1 → () Source #

d_EvalMode_46 ∷ () Source #

type T_EvalMode_46 = EvalMode Source #

pattern C_U_48 ∷ EvalMode Source #

pattern C_TL_50 ∷ EvalMode Source #

pattern C_TCK_52 ∷ EvalMode Source #

pattern C_TCEK_54 ∷ EvalMode Source #

check_U_48 ∷ T_EvalMode_46 Source #

check_TL_50 ∷ T_EvalMode_46 Source #

check_TCK_52 ∷ T_EvalMode_46 Source #

check_TCEK_54 ∷ T_EvalMode_46 Source #

cover_EvalMode_46 ∷ EvalMode → () Source #

d_parsePLC_56 ∷ T_ProgramN_18 → T_Either_6 T_ERROR_12 T_ScopedTm_522 Source #

d_parseUPLC_62 ∷ T_ProgramNU_26 → T_Either_6 T_ERROR_12 T__'8866'_14 Source #

d_typeCheckPLC_70 ∷ T_ScopedTm_522 → T_Either_6 T_TypeError_12 T_Σ_14 Source #

d_checkError_76 ∷ T__'8866'Nf'8902'__4 → T__'8866'__184 → T_Either_6 T_ERROR_12 T__'8866'__184 Source #

du_checkError_76 ∷ T__'8866'__184 → T_Either_6 T_ERROR_12 T__'8866'__184 Source #

d_executePLC_80 ∷ T_EvalMode_46 → T_ScopedTm_522 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_showUPLCResult_138 ∷ T_State_218 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_executeUPLCwithMP_144 ∷ () → T__'215'__436 T_HCekMachineCosts_4 (T_List_454 (T__'215'__436 T_String_6 T_CpuAndMemoryModel_196)) → (T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_MachineParameters_46) → (AgdaAny → T_String_6) → T__'8866'_14 → T_Either_6 T_ERROR_12 T_String_6 Source #

du_executeUPLCwithMP_144 ∷ T__'215'__436 T_HCekMachineCosts_4 (T_List_454 (T__'215'__436 T_String_6 T_CpuAndMemoryModel_196)) → (T__'215'__436 T_HCekMachineCosts_4 (T_Builtin_2 → T_BuiltinModel_68) → T_MachineParameters_46) → (AgdaAny → T_String_6) → T__'8866'_14 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_executeUPLC_192 ∷ T_BudgetMode_36 (T__'215'__436 T_HCekMachineCosts_4 (T_List_454 (T__'215'__436 T_String_6 T_CpuAndMemoryModel_196))) → T__'8866'_14 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_evalProgramNU_204 ∷ T_BudgetMode_36 (T__'215'__436 T_HCekMachineCosts_4 (T_List_454 (T__'215'__436 T_String_6 T_CpuAndMemoryModel_196))) → T_ProgramNU_26 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_evalProgramN_212 ∷ T_EvalMode_46 → T_ProgramN_18 → T_Either_6 T_ERROR_12 T_String_6 Source #

d_typeCheckProgramN_220 ∷ T_ProgramN_18 → T_Either_6 T_ERROR_12 T_String_6 Source #