<commit_before>module TTImp.Elab.RunElab

import Core.Context
import Core.Core
import Core.Env
import Core.GetType
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Reflect
import TTImp.TTImp
import TTImp.Unelab

elabScript : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             FC -> ElabInfo -> NestedNames vars ->
             Env Term vars -> NF vars -> Maybe (Glued vars) ->
             Core (NF vars)
elabScript fc elabinfo nest env tm@(NDCon _ nm _ _ args) exp
    = do defs <- get Ctxt
         fnm <- toFullNames nm
         case fnm of
              NS ["Reflection", "Language"] (UN n)
                 => elabCon defs n args
              _ => failWith defs
  where
    failWith : Defs -> Core a
    failWith defs
      = do defs <- get Ctxt
           empty <- clearDefs defs
           throw (BadRunElab fc env !(quote empty env tm))

    scriptRet : Reflect a => a -> Core (NF vars)
    scriptRet tm
        = do defs <- get Ctxt
             nfOpts withAll defs env !(reflect fc defs env tm)

    elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
    elabCon defs "Pure" [_,val] = evalClosure defs val
    elabCon defs "Bind" [_,_,act,k]
        = do act' <- elabScript fc elabinfo nest env
                                !(evalClosure defs act) exp
             case !(evalClosure defs k) of
                  NBind _ x (Lam _ _ _) sc =>
                      elabScript fc elabinfo nest env
                                 !(sc defs (toClosure withAll env
                                                 !(quote defs env act'))) exp
                  _ => failWith defs
    elabCon defs "LogMsg" [lvl, str]
        = do lvl' <- evalClosure defs lvl
             logC !(reify defs lvl') $
                  do str' <- evalClosure defs str
                     reify defs str'
             scriptRet ()
    elabCon defs "LogTerm" [lvl, str, tm]
        = do lvl' <- evalClosure defs lvl
             logC !(reify defs lvl') $
                  do str' <- evalClosure defs str
                     tm' <- evalClosure defs tm<commit_msg>Workaround for bug in bootstrap version<commit_after>module TTImp.Elab.RunElab

import Core.Context
import Core.Core
import Core.Env
import Core.GetType
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Reflect
import TTImp.TTImp
import TTImp.Unelab

elabScript : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             FC -> ElabInfo -> NestedNames vars ->
             Env Term vars -> NF vars -> Maybe (Glued vars) ->
             Core (NF vars)
elabScript fc elabinfo nest env (NDCon nfc nm t ar args) exp
    = do defs <- get Ctxt
         fnm <- toFullNames nm
         case fnm of
              NS ["Reflection", "Language"] (UN n)
                 => elabCon defs n args
              _ => failWith defs
  where
    failWith : Defs -> Core a
    failWith defs
      = do defs <- get Ctxt
           empty <- clearDefs defs
           throw (BadRunElab fc env !(quote empty env (NDCon nfc nm t ar args)))

    scriptRet : Reflect a => a -> Core (NF vars)
    scriptRet tm
        = do defs <- get Ctxt
             nfOpts withAll defs env !(reflect fc defs env tm)

    elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
    elabCon defs "Pure" [_,val] = evalClosure defs val
    elabCon defs "Bind" [_,_,act,k]
        = do act' <- elabScript fc elabinfo nest env
                                !(evalClosure defs act) exp
             case !(evalClosure defs k) of
                  NBind _ x (Lam _ _ _) sc =>
                      elabScript fc elabinfo nest env
                                 !(sc defs (toClosure withAll env
                                                 !(quote defs env act'))) exp
                  _ => failWith defs
    elabCon defs "LogMsg" [lvl, str]
        = do lvl' <- evalClosure defs lvl
             logC !(reify defs lvl') $
                  do str' <- evalClosure defs str
                     reify defs str'
             scriptRet ()
    elabCon defs "LogTerm" [lvl, str, tm]
        = do lvl' <- evalClosure defs lvl
             logC !(reify defs lvl') $
                  do str' <- evalClosure defs str
                     tm' <- evalClosure defs tm
{'fraction_non_alphanumeric': 0.0854933110367893, 'fraction_numerical': 0.0, 'mean_word_length': 1.5492807671816728, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4523332', 'n_tokens_mistral': 1514, 'n_tokens_neox': 1457, 'n_words': 512}