0 | module Core.SchemeEval
 1 |
 2 | -- Top level interface to the scheme based evaluator
 3 | -- Drops back to the default slow evaluator if scheme isn't available
 4 |
 5 | import Core.Context
 6 | import Core.Env
 7 | import Core.Normalise
 8 | import public Core.SchemeEval.Compile
 9 | import public Core.SchemeEval.Evaluate
10 | import public Core.SchemeEval.Quote
11 | import public Core.SchemeEval.ToScheme
12 |
13 | {-
14 |
15 | Summary:
16 |
17 | SObj vars
18 |    ...is a scheme object with the scheme representation of the result
19 |    of evaluating a term vars
20 |
21 | SNF vars
22 |    ...corresponds to NF vars, and is an inspectable version of the above.
23 |    Evaluation is call by value, but there has not yet been any evaluation
24 |    under lambdas
25 |
26 | 'Evaluate.seval' gets you an SObj from a Term
27 |    - this involves compiling all the relevant definitions to scheme code
28 |    first. We make a note of what we've compiled to scheme so we don't have
29 |    to do it more than once.
30 | `Evaluate.toSNF` gets you an SNF from an SObj
31 | `Quote.quote` gets you back to a Term from an SNF
32 |
33 | `snf` gets you directly to an SNF from a Term
34 | `snormalise` packages up the whole process
35 |
36 | All of this works only on a back end which can call scheme directly, and
37 | with the relevant support files (currently: Chez)
38 |
39 | -}
40 |
41 | snormaliseMode : {auto c : Ref Ctxt Defs} ->
42 |                  {vars : _} ->
43 |                  SchemeMode -> Env Term vars -> Term vars -> Core (Term vars)
44 | snormaliseMode mode env tm
45 |     = do defs <- get Ctxt
46 |          True <- initialiseSchemeEval
47 |              | _ => normalise defs env tm
48 |          sval <- seval mode env tm
49 |          quoteObj sval
50 |
51 | export
52 | snormalise : {auto c : Ref Ctxt Defs} ->
53 |              {vars : _} ->
54 |              Env Term vars -> Term vars -> Core (Term vars)
55 | snormalise = snormaliseMode BlockExport
56 |
57 | export
58 | snormaliseAll : {auto c : Ref Ctxt Defs} ->
59 |                 {vars : _} ->
60 |                 Env Term vars -> Term vars -> Core (Term vars)
61 | snormaliseAll = snormaliseMode EvalAll
62 |
63 | export
64 | snf : {auto c : Ref Ctxt Defs} ->
65 |       {vars : _} ->
66 |       Env Term vars -> Term vars -> Core (SNF vars)
67 | snf env tm
68 |     = do True <- initialiseSchemeEval
69 |              | _ => throw (InternalError "Scheme evaluator not available")
70 |          sval <- seval BlockExport env tm
71 |          toSNF sval
72 |
73 | export
74 | snfAll : {auto c : Ref Ctxt Defs} ->
75 |          {vars : _} ->
76 |          Env Term vars -> Term vars -> Core (SNF vars)
77 | snfAll env tm
78 |     = do True <- initialiseSchemeEval
79 |              | _ => throw (InternalError "Scheme evaluator not available")
80 |          sval <- seval EvalAll env tm
81 |          toSNF sval
82 |