shentong-0.3.2: Shentong/Backend/Load.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE ViewPatterns #-}
module Backend.Load where
import Control.Monad.Except
import Control.Parallel
import Environment
import Core.Primitives as Primitives
import Backend.Utils
import Core.Types
import Core.Utils
import Wrap
import Backend.Toplevel
import Backend.Core
import Backend.Sys
import Backend.Sequent
import Backend.Yacc
import Backend.Reader
import Backend.Prolog
import Backend.Track
{-
Copyright (c) 2015, Mark Tarver
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. The name of Mark Tarver may not be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY
EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-}
kl_load :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_load (!kl_V1482) = do let !appl_0 = ApplC (Func "lambda" (Context (\(!kl_Load) -> do let !appl_1 = ApplC (Func "lambda" (Context (\(!kl_Infs) -> do return (Core.Types.Atom (Core.Types.UnboundSym "loaded")))))
!kl_if_2 <- value (Core.Types.Atom (Core.Types.UnboundSym "shen.*tc*"))
!appl_3 <- case kl_if_2 of
Atom (B (True)) -> do !appl_4 <- kl_inferences
let !aw_5 = Core.Types.Atom (Core.Types.UnboundSym "shen.app")
!appl_6 <- appl_4 `pseq` applyWrapper aw_5 [appl_4,
Core.Types.Atom (Core.Types.Str " inferences\n"),
Core.Types.Atom (Core.Types.UnboundSym "shen.a")]
!appl_7 <- appl_6 `pseq` cn (Core.Types.Atom (Core.Types.Str "\ntypechecked in ")) appl_6
!appl_8 <- kl_stoutput
let !aw_9 = Core.Types.Atom (Core.Types.UnboundSym "shen.prhush")
appl_7 `pseq` (appl_8 `pseq` applyWrapper aw_9 [appl_7,
appl_8])
Atom (B (False)) -> do do return (Core.Types.Atom (Core.Types.UnboundSym "shen.skip"))
_ -> throwError "if: expected boolean"
appl_3 `pseq` applyWrapper appl_1 [appl_3])))
let !appl_10 = ApplC (Func "lambda" (Context (\(!kl_Start) -> do let !appl_11 = ApplC (Func "lambda" (Context (\(!kl_Result) -> do let !appl_12 = ApplC (Func "lambda" (Context (\(!kl_Finish) -> do let !appl_13 = ApplC (Func "lambda" (Context (\(!kl_Time) -> do let !appl_14 = ApplC (Func "lambda" (Context (\(!kl_Message) -> do return kl_Result)))
!appl_15 <- kl_Time `pseq` str kl_Time
!appl_16 <- appl_15 `pseq` cn appl_15 (Core.Types.Atom (Core.Types.Str " secs\n"))
!appl_17 <- appl_16 `pseq` cn (Core.Types.Atom (Core.Types.Str "\nrun time: ")) appl_16
!appl_18 <- kl_stoutput
let !aw_19 = Core.Types.Atom (Core.Types.UnboundSym "shen.prhush")
!appl_20 <- appl_17 `pseq` (appl_18 `pseq` applyWrapper aw_19 [appl_17,
appl_18])
appl_20 `pseq` applyWrapper appl_14 [appl_20])))
!appl_21 <- kl_Finish `pseq` (kl_Start `pseq` Primitives.subtract kl_Finish kl_Start)
appl_21 `pseq` applyWrapper appl_13 [appl_21])))
!appl_22 <- getTime (Core.Types.Atom (Core.Types.UnboundSym "run"))
appl_22 `pseq` applyWrapper appl_12 [appl_22])))
!appl_23 <- value (Core.Types.Atom (Core.Types.UnboundSym "shen.*tc*"))
!appl_24 <- kl_V1482 `pseq` kl_read_file kl_V1482
!appl_25 <- appl_23 `pseq` (appl_24 `pseq` kl_shen_load_help appl_23 appl_24)
appl_25 `pseq` applyWrapper appl_11 [appl_25])))
!appl_26 <- getTime (Core.Types.Atom (Core.Types.UnboundSym "run"))
!appl_27 <- appl_26 `pseq` applyWrapper appl_10 [appl_26]
appl_27 `pseq` applyWrapper appl_0 [appl_27]
kl_shen_load_help :: Core.Types.KLValue ->
Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_load_help (!kl_V1489) (!kl_V1490) = do let pat_cond_0 = do let !appl_1 = ApplC (Func "lambda" (Context (\(!kl_X) -> do !appl_2 <- kl_X `pseq` kl_shen_eval_without_macros kl_X
let !aw_3 = Core.Types.Atom (Core.Types.UnboundSym "shen.app")
!appl_4 <- appl_2 `pseq` applyWrapper aw_3 [appl_2,
Core.Types.Atom (Core.Types.Str "\n"),
Core.Types.Atom (Core.Types.UnboundSym "shen.s")]
!appl_5 <- kl_stoutput
let !aw_6 = Core.Types.Atom (Core.Types.UnboundSym "shen.prhush")
appl_4 `pseq` (appl_5 `pseq` applyWrapper aw_6 [appl_4,
appl_5]))))
appl_1 `pseq` (kl_V1490 `pseq` kl_for_each appl_1 kl_V1490)
pat_cond_7 = do do let !appl_8 = ApplC (Func "lambda" (Context (\(!kl_RemoveSynonyms) -> do let !appl_9 = ApplC (Func "lambda" (Context (\(!kl_Table) -> do let !appl_10 = ApplC (Func "lambda" (Context (\(!kl_Assume) -> do (do let !appl_11 = ApplC (Func "lambda" (Context (\(!kl_X) -> do kl_X `pseq` kl_shen_typecheck_and_load kl_X)))
appl_11 `pseq` (kl_RemoveSynonyms `pseq` kl_for_each appl_11 kl_RemoveSynonyms)) `catchError` (\(!kl_E) -> do kl_E `pseq` (kl_Table `pseq` kl_shen_unwind_types (Excep kl_E) kl_Table)))))
let !appl_12 = ApplC (Func "lambda" (Context (\(!kl_X) -> do kl_X `pseq` kl_shen_assumetype kl_X)))
!appl_13 <- appl_12 `pseq` (kl_Table `pseq` kl_for_each appl_12 kl_Table)
appl_13 `pseq` applyWrapper appl_10 [appl_13])))
let !appl_14 = ApplC (Func "lambda" (Context (\(!kl_X) -> do kl_X `pseq` kl_shen_typetable kl_X)))
!appl_15 <- appl_14 `pseq` (kl_RemoveSynonyms `pseq` kl_mapcan appl_14 kl_RemoveSynonyms)
appl_15 `pseq` applyWrapper appl_9 [appl_15])))
let !appl_16 = ApplC (Func "lambda" (Context (\(!kl_X) -> do kl_X `pseq` kl_shen_remove_synonyms kl_X)))
!appl_17 <- appl_16 `pseq` (kl_V1490 `pseq` kl_mapcan appl_16 kl_V1490)
appl_17 `pseq` applyWrapper appl_8 [appl_17]
in case kl_V1489 of
kl_V1489@(Atom (UnboundSym "false")) -> pat_cond_0
kl_V1489@(Atom (B (False))) -> pat_cond_0
_ -> pat_cond_7
kl_shen_remove_synonyms :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_remove_synonyms (!kl_V1492) = do let pat_cond_0 kl_V1492 kl_V1492t = do !appl_1 <- kl_V1492 `pseq` kl_eval kl_V1492
let !appl_2 = Atom Nil
appl_1 `pseq` (appl_2 `pseq` kl_do appl_1 appl_2)
pat_cond_3 = do do let !appl_4 = Atom Nil
kl_V1492 `pseq` (appl_4 `pseq` klCons kl_V1492 appl_4)
in case kl_V1492 of
!(kl_V1492@(Cons (Atom (UnboundSym "shen.synonyms-help"))
(!kl_V1492t))) -> pat_cond_0 kl_V1492 kl_V1492t
!(kl_V1492@(Cons (ApplC (PL "shen.synonyms-help"
_))
(!kl_V1492t))) -> pat_cond_0 kl_V1492 kl_V1492t
!(kl_V1492@(Cons (ApplC (Func "shen.synonyms-help"
_))
(!kl_V1492t))) -> pat_cond_0 kl_V1492 kl_V1492t
_ -> pat_cond_3
kl_shen_typecheck_and_load :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_typecheck_and_load (!kl_V1494) = do !appl_0 <- kl_nl (Core.Types.Atom (Core.Types.N (Core.Types.KI 1)))
!appl_1 <- kl_gensym (Core.Types.Atom (Core.Types.UnboundSym "A"))
!appl_2 <- kl_V1494 `pseq` (appl_1 `pseq` kl_shen_typecheck_and_evaluate kl_V1494 appl_1)
appl_0 `pseq` (appl_2 `pseq` kl_do appl_0 appl_2)
kl_shen_typetable :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_typetable (!kl_V1500) = do let pat_cond_0 kl_V1500 kl_V1500t kl_V1500th kl_V1500tt = do let !appl_1 = ApplC (Func "lambda" (Context (\(!kl_Sig) -> do !appl_2 <- kl_V1500th `pseq` (kl_Sig `pseq` klCons kl_V1500th kl_Sig)
let !appl_3 = Atom Nil
appl_2 `pseq` (appl_3 `pseq` klCons appl_2 appl_3))))
let !appl_4 = ApplC (Func "lambda" (Context (\(!kl_Y) -> do kl_Y `pseq` kl_shen_LBsigPlusrestRB kl_Y)))
let !appl_5 = ApplC (Func "lambda" (Context (\(!kl_E) -> do let !aw_6 = Core.Types.Atom (Core.Types.UnboundSym "shen.app")
!appl_7 <- kl_V1500th `pseq` applyWrapper aw_6 [kl_V1500th,
Core.Types.Atom (Core.Types.Str " lacks a proper signature.\n"),
Core.Types.Atom (Core.Types.UnboundSym "shen.a")]
appl_7 `pseq` simpleError appl_7)))
!appl_8 <- appl_4 `pseq` (kl_V1500tt `pseq` (appl_5 `pseq` kl_compile appl_4 kl_V1500tt appl_5))
appl_8 `pseq` applyWrapper appl_1 [appl_8]
pat_cond_9 = do do return (Atom Nil)
in case kl_V1500 of
!(kl_V1500@(Cons (Atom (UnboundSym "define"))
(!(kl_V1500t@(Cons (!kl_V1500th)
(!kl_V1500tt)))))) -> pat_cond_0 kl_V1500 kl_V1500t kl_V1500th kl_V1500tt
!(kl_V1500@(Cons (ApplC (PL "define" _))
(!(kl_V1500t@(Cons (!kl_V1500th)
(!kl_V1500tt)))))) -> pat_cond_0 kl_V1500 kl_V1500t kl_V1500th kl_V1500tt
!(kl_V1500@(Cons (ApplC (Func "define" _))
(!(kl_V1500t@(Cons (!kl_V1500th)
(!kl_V1500tt)))))) -> pat_cond_0 kl_V1500 kl_V1500t kl_V1500th kl_V1500tt
_ -> pat_cond_9
kl_shen_assumetype :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_assumetype (!kl_V1502) = do let pat_cond_0 kl_V1502 kl_V1502h kl_V1502t = do let !aw_1 = Core.Types.Atom (Core.Types.UnboundSym "declare")
kl_V1502h `pseq` (kl_V1502t `pseq` applyWrapper aw_1 [kl_V1502h,
kl_V1502t])
pat_cond_2 = do do kl_shen_f_error (ApplC (wrapNamed "shen.assumetype" kl_shen_assumetype))
in case kl_V1502 of
!(kl_V1502@(Cons (!kl_V1502h)
(!kl_V1502t))) -> pat_cond_0 kl_V1502 kl_V1502h kl_V1502t
_ -> pat_cond_2
kl_shen_unwind_types :: Core.Types.KLValue ->
Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_unwind_types (!kl_V1509) (!kl_V1510) = do let !appl_0 = Atom Nil
!kl_if_1 <- appl_0 `pseq` (kl_V1510 `pseq` eq appl_0 kl_V1510)
case kl_if_1 of
Atom (B (True)) -> do !appl_2 <- kl_V1509 `pseq` errorToString kl_V1509
appl_2 `pseq` simpleError appl_2
Atom (B (False)) -> do let pat_cond_3 kl_V1510 kl_V1510h kl_V1510hh kl_V1510ht kl_V1510t = do !appl_4 <- kl_V1510hh `pseq` kl_shen_remtype kl_V1510hh
!appl_5 <- kl_V1509 `pseq` (kl_V1510t `pseq` kl_shen_unwind_types kl_V1509 kl_V1510t)
appl_4 `pseq` (appl_5 `pseq` kl_do appl_4 appl_5)
pat_cond_6 = do do kl_shen_f_error (ApplC (wrapNamed "shen.unwind-types" kl_shen_unwind_types))
in case kl_V1510 of
!(kl_V1510@(Cons (!(kl_V1510h@(Cons (!kl_V1510hh)
(!kl_V1510ht))))
(!kl_V1510t))) -> pat_cond_3 kl_V1510 kl_V1510h kl_V1510hh kl_V1510ht kl_V1510t
_ -> pat_cond_6
_ -> throwError "if: expected boolean"
kl_shen_remtype :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_remtype (!kl_V1512) = do !appl_0 <- value (Core.Types.Atom (Core.Types.UnboundSym "shen.*signedfuncs*"))
!appl_1 <- kl_V1512 `pseq` (appl_0 `pseq` kl_shen_removetype kl_V1512 appl_0)
appl_1 `pseq` klSet (Core.Types.Atom (Core.Types.UnboundSym "shen.*signedfuncs*")) appl_1
kl_shen_removetype :: Core.Types.KLValue ->
Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_removetype (!kl_V1520) (!kl_V1521) = do let !appl_0 = Atom Nil
!kl_if_1 <- appl_0 `pseq` (kl_V1521 `pseq` eq appl_0 kl_V1521)
case kl_if_1 of
Atom (B (True)) -> do return (Atom Nil)
Atom (B (False)) -> do let pat_cond_2 kl_V1521 kl_V1521h kl_V1521hh kl_V1521ht kl_V1521t = do kl_V1521hh `pseq` (kl_V1521t `pseq` kl_shen_removetype kl_V1521hh kl_V1521t)
pat_cond_3 kl_V1521 kl_V1521h kl_V1521t = do !appl_4 <- kl_V1520 `pseq` (kl_V1521t `pseq` kl_shen_removetype kl_V1520 kl_V1521t)
kl_V1521h `pseq` (appl_4 `pseq` klCons kl_V1521h appl_4)
pat_cond_5 = do do kl_shen_f_error (ApplC (wrapNamed "shen.removetype" kl_shen_removetype))
in case kl_V1521 of
!(kl_V1521@(Cons (!(kl_V1521h@(Cons (!kl_V1521hh)
(!kl_V1521ht))))
(!kl_V1521t))) | eqCore kl_V1521hh kl_V1520 -> pat_cond_2 kl_V1521 kl_V1521h kl_V1521hh kl_V1521ht kl_V1521t
!(kl_V1521@(Cons (!kl_V1521h)
(!kl_V1521t))) -> pat_cond_3 kl_V1521 kl_V1521h kl_V1521t
_ -> pat_cond_5
_ -> throwError "if: expected boolean"
kl_shen_LBsigPlusrestRB :: Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_shen_LBsigPlusrestRB (!kl_V1523) = do let !appl_0 = ApplC (Func "lambda" (Context (\(!kl_Parse_shen_LBsignatureRB) -> do !appl_1 <- kl_fail
!appl_2 <- appl_1 `pseq` (kl_Parse_shen_LBsignatureRB `pseq` eq appl_1 kl_Parse_shen_LBsignatureRB)
!kl_if_3 <- appl_2 `pseq` kl_not appl_2
case kl_if_3 of
Atom (B (True)) -> do let !appl_4 = ApplC (Func "lambda" (Context (\(!kl_Parse_LBExclRB) -> do !appl_5 <- kl_fail
!appl_6 <- appl_5 `pseq` (kl_Parse_LBExclRB `pseq` eq appl_5 kl_Parse_LBExclRB)
!kl_if_7 <- appl_6 `pseq` kl_not appl_6
case kl_if_7 of
Atom (B (True)) -> do !appl_8 <- kl_Parse_LBExclRB `pseq` hd kl_Parse_LBExclRB
!appl_9 <- kl_Parse_shen_LBsignatureRB `pseq` kl_shen_hdtl kl_Parse_shen_LBsignatureRB
appl_8 `pseq` (appl_9 `pseq` kl_shen_pair appl_8 appl_9)
Atom (B (False)) -> do do kl_fail
_ -> throwError "if: expected boolean")))
!appl_10 <- kl_Parse_shen_LBsignatureRB `pseq` kl_LBExclRB kl_Parse_shen_LBsignatureRB
appl_10 `pseq` applyWrapper appl_4 [appl_10]
Atom (B (False)) -> do do kl_fail
_ -> throwError "if: expected boolean")))
!appl_11 <- kl_V1523 `pseq` kl_shen_LBsignatureRB kl_V1523
appl_11 `pseq` applyWrapper appl_0 [appl_11]
kl_write_to_file :: Core.Types.KLValue ->
Core.Types.KLValue ->
Core.Types.KLContext Core.Types.Env Core.Types.KLValue
kl_write_to_file (!kl_V1526) (!kl_V1527) = do let !appl_0 = ApplC (Func "lambda" (Context (\(!kl_Stream) -> do let !appl_1 = ApplC (Func "lambda" (Context (\(!kl_String) -> do let !appl_2 = ApplC (Func "lambda" (Context (\(!kl_Write) -> do let !appl_3 = ApplC (Func "lambda" (Context (\(!kl_Close) -> do return kl_V1527)))
!appl_4 <- kl_Stream `pseq` closeStream kl_Stream
appl_4 `pseq` applyWrapper appl_3 [appl_4])))
let !aw_5 = Core.Types.Atom (Core.Types.UnboundSym "pr")
!appl_6 <- kl_String `pseq` (kl_Stream `pseq` applyWrapper aw_5 [kl_String,
kl_Stream])
appl_6 `pseq` applyWrapper appl_2 [appl_6])))
!kl_if_7 <- kl_V1527 `pseq` stringP kl_V1527
!appl_8 <- case kl_if_7 of
Atom (B (True)) -> do let !aw_9 = Core.Types.Atom (Core.Types.UnboundSym "shen.app")
kl_V1527 `pseq` applyWrapper aw_9 [kl_V1527,
Core.Types.Atom (Core.Types.Str "\n\n"),
Core.Types.Atom (Core.Types.UnboundSym "shen.a")]
Atom (B (False)) -> do do let !aw_10 = Core.Types.Atom (Core.Types.UnboundSym "shen.app")
kl_V1527 `pseq` applyWrapper aw_10 [kl_V1527,
Core.Types.Atom (Core.Types.Str "\n\n"),
Core.Types.Atom (Core.Types.UnboundSym "shen.s")]
_ -> throwError "if: expected boolean"
appl_8 `pseq` applyWrapper appl_1 [appl_8])))
!appl_11 <- kl_V1526 `pseq` openStream kl_V1526 (Core.Types.Atom (Core.Types.UnboundSym "out"))
appl_11 `pseq` applyWrapper appl_0 [appl_11]
expr8 :: Core.Types.KLContext Core.Types.Env Core.Types.KLValue
expr8 = do (do return (Core.Types.Atom (Core.Types.Str "Copyright (c) 2015, Mark Tarver\n\nAll rights reserved.\n\nRedistribution and use in source and binary forms, with or without\nmodification, are permitted provided that the following conditions are met:\n1. Redistributions of source code must retain the above copyright\n notice, this list of conditions and the following disclaimer.\n2. Redistributions in binary form must reproduce the above copyright\n notice, this list of conditions and the following disclaimer in the\n documentation and/or other materials provided with the distribution.\n3. The name of Mark Tarver may not be used to endorse or promote products\n derived from this software without specific prior written permission.\n\nTHIS SOFTWARE IS PROVIDED BY Mark Tarver ''AS IS'' AND ANY\nEXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED\nWARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE\nDISCLAIMED. IN NO EVENT SHALL Mark Tarver BE LIABLE FOR ANY\nDIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES\n(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;\nLOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND\nON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS\nSOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."))) `catchError` (\(!kl_E) -> do return (Core.Types.Atom (Core.Types.Str "E")))