- | Error s => fail ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s)
- | OK me =>
- match weakExprToStrongExpr (*(makeClosedExpression me)*) me Γ Δ φ ψ ξ nil with
- | Indexed_Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
- | Indexed_OK τ e => match e with
- | Error s => fail ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
- | OK e' => header +++ (nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')) +++ footer
- end
- end
+ | Error s => Prelude_error ("unable to convert GHC Core expression into Coq HaskWeak expression due to:\n "+++s)
+ | OK we => match weakTypeOfWeakExpr we >>= fun t => weakTypeToType φ t with
+ | Error s => Prelude_error ("unable to calculate HaskType of a HaskWeak expression because: " +++ s)
+ | OK τ => match τ with
+ | haskTypeOfSomeKind ★ τ' =>
+ match weakExprToStrongExpr Γ Δ φ ψ ξ τ' nil (*(makeClosedExpression*) we (* ) *) with
+ | Error s => Prelude_error ("unable to convert HaskWeak to HaskStrong due to:\n "+++s)
+ | OK e' => eol+++"$$"+++ nd_ml_toLatex (@expr2proof _ _ _ _ _ _ e')+++"$$"+++eol
+ end
+ | haskTypeOfSomeKind κ τ' =>
+ Prelude_error ("encountered 'expression' of kind "+++κ+++" at top level (type "+++τ'
+ +++"); shouldn't happen")
+ end
+ end