Skip to content
No description or website provided.
Standard ML Emacs Lisp Shell
Find file
Failed to load latest commit information.
Binarymap Initial revision.
emacs Add a celf emacs mode, which appears to just be Twelf mode (???) and …
tests Initial printing of epsilons - vars in ctx don't match names in terms?
.gitignore Ignore generated l10.sml files
.mkexec *** empty log message ***
AbstractRecursion.sml *** empty log message ***
ApproxTypes.sig *** empty log message ***
ApproxTypes.sml *** empty log message ***
BackTrack.sig added copyright header
BackTrack.sml *** empty log message ***
CHANGELOG Fixed a unification bug concerning lowering of logic variables in let…
Context.sig Changed datatype name Context.mode -> Context.modality
Context.sml Changed datatype name Context.mode -> Context.modality
Conv.sig added copyright header
Conv.sml *** empty log message ***
DestCheck.sig Fix nontermination bug
DestCheck.sml Fix nontermination bug
Eta.sig Changed datatype name Context.mode -> Context.modality
Eta.sml Changed datatype name Context.mode -> Context.modality
ExactTypes.sig *** empty log message ***
ExactTypes.sml *** empty log message ***
GFPrint.sml fixed a bug in GFPrint
GoalMode.sig Mode checker now uses normalized types. Fixes the issue of unhandled …
GoalMode.sml Mode checker now uses normalized types. Fixes the issue of unhandled …
ImplicitVars.sig *** empty log message ***
ImplicitVars.sml *** empty log message ***
ImplicitVarsConvert.sig *** empty log message ***
ImplicitVarsConvert.sml *** empty log message ***
Makefile Removed heap-size flag
ModeCheck.sig Mode checker now uses normalized types. Fixes the issue of unhandled …
ModeCheck.sml Integrated Twelf timing structures for profiling purposes
ModeDec.sig Mode checker now uses normalized types. Fixes the issue of unhandled …
ModeDec.sml Multiple files at the command line and better reporting of a number o…
NatSet.sig NatSet
NatSet.sml changed to sorted list representation
NoPermuteList.sml added no permutelist.sml
OpSem.sig Initial printing of epsilons - vars in ctx don't match names in terms?
OpSem.sml Fixed OpSem interface.
OpSemFair.sml Changed datatype name Context.mode -> Context.modality
OpSemFair2.sml Comment out unnecessary printing in trace commands.
Parse.sig clf ver 2
Parse.sml *** empty log message ***
PatternBind.sig *** empty log message ***
PatternBind.sml *** empty log message ***
PatternNormalize.sig Mode checker now uses normalized types. Fixes the issue of unhandled …
PatternNormalize.sml Mode checker now uses normalized types. Fixes the issue of unhandled …
PermuteList.sig *** empty log message ***
PermuteList.sml *** empty log message ***
PrettyPrint.sig Initial printing of epsilons - vars in ctx don't match names in terms?
PrettyPrint.sml
README Fix makefile installation error, add Smackage instructions to README
RandomAccessList.sig Changed ctx to RAList
RandomAccessList.sml *** empty log message ***
RedBlackTree.fun Reimplemented fresh-name generation for pretty-printing.
RemDepend.sig *** empty log message ***
RemDepend.sml Changed ctx to RAList
Rnd-mlkit.sml added copyright header
Rnd-smlnj-mlton.sml *** empty log message ***
Rnd.sig added copyright header
Signatur.sml Make major whitespare/style changes in TypeRecon, because I couldn't …
SignaturTable.sig Signature reset function
SignaturTable.sml Signature reset function
SimpleList.sml Added SimpleList.sml: implementation of RandomAccessList using ML lists.
Skel.sig Add Skel, which I think will help me write DestCheck
Skel.sml Change exex
Subst.sml Changed datatype name Context.mode -> Context.modality
SymbTable.sig added copyright header
SymbTable.sml *** empty log message ***
Syntax.sig Merge branch 'master' of github.com:clf/celf
Syntax.sml Merge branch 'master' of github.com:clf/celf
Table.sig Reimplemented fresh-name generation for pretty-printing.
Table.sml Reimplemented fresh-name generation for pretty-printing.
Timers.sig Added unification Timer.
Timers.sml Added unification Timer.
Timing.sig added the missing files to git
Timing.sml added no permutelist.sml
TopLevelUtil.sml Add ability to do regression testing
TypeCheck.sig clf ver 2
TypeCheck.sml Changed ctx to RAList
TypeRecon.sig added printgf
TypeRecon.sml added printgf
Unify.sig *** empty log message ***
Unify.sml Added unification Timer.
Util.sig *** empty log message ***
Util.sml *** empty log message ***
VRef.sig added copyright header
VRef.sml *** empty log message ***
celf-mlkit.mlb Changed ctx to RAList
celf.grm Removing unneccesary whitespace changes
celf.lex Delete redundant eof function.
celf.mlb
license-gpl3.txt *** empty log message ***
main-export.sml *** empty log message ***
main-run.sml *** empty log message ***
main.sml Add a -time flag to report Carsten's timing information
makedist.sh *** empty log message ***
notes
sources.cm fixed omitted function problem

README

Celf README

Celf can be compiled with several different ML compilers.
Here is instructions for a few of them:

To compile with Smackage:

      $ smackage get celf
      $ smackage make celf smlnj (or mlton)
      $ smackage make celf install

To compile Celf with SML/NJ:

1. Compile the source into a heapimage (.heapimg.<arch>-<opsys>):

      sml < main-export.sml

2. Create a shell script to load the runtime with the heap image,
   e.g. with the .mkexec script:

      ./.mkexec `which sml` `pwd` celf


To compile Celf with MLton:

1. Compile the lexer definition, parser definition, and the rest
   of the source:

      mllex celf.lex
      mlyacc celf.grm
      mlton celf.mlb


TROUBLESHOOTING
If you get the following error when compiling with SML/NJ

      ["/usr/lib/smlnj/bin/ml-yacc" "" "celf.grm"]
      Usage: ml-yacc filename
      sources.cm:25.1-25.9 Error: tool "ML-Yacc" failed: "/usr/lib/smlnj/bin/ml-yacc" "" "celf.grm"

then simply run ml-yacc manually by removing the superfluous argument added by
the compilation manager and rerun sml:

      /usr/lib/smlnj/bin/ml-yacc celf.grm
      sml < main-export.sml

Something went wrong with that request. Please try again.