Changes by: Adam Granicz (granicz at cs.caltech.edu)
Date: 2003-02-27 01:40:58 -0800 (Thu, 27 Feb 2003)
Revision: 4145
Log message:

      Added M source language definition. It is a superset of the M IR,
      the only extension is our own tuple terms which are used to encode
      function arguments.
      The parser takes care of currying function definitions and properly
      declares all mutually recursive functions before their definition.
      These are implemented with relaxed rewrites.
      Then in m_post_parsing, we curry function calls by partially applying
      them one by one, storing the result of each partial function
      application in a temporary variable.
      There is one step missing, which is identifying function variables
      in the program term. This should be easy enough:
      
      FunDecl{f. 'e[AtomVar{'f}]} <--> FunDecl{f. 'e[AtomFunVar{'f}]}
      
      but a straight rewrite rule just does not cut it. So this remains
      to be done.
      I put a test program in m_test, but the old stuff should work as
      before. The post-processing tactic is called ppT.
      

Changes  Path
+2 -0 metaprl/theories/experimental/compile/Makefile
Added metaprl/theories/experimental/compile/m_ast.ml
Properties metaprl/theories/experimental/compile/m_ast.ml
Added metaprl/theories/experimental/compile/m_ast.mli
Properties metaprl/theories/experimental/compile/m_ast.mli
+57 -18 metaprl/theories/experimental/compile/m_ast.pho
+0 -3 metaprl/theories/experimental/compile/m_closure.ml
Added metaprl/theories/experimental/compile/m_post_parsing.ml
Properties metaprl/theories/experimental/compile/m_post_parsing.ml
Added metaprl/theories/experimental/compile/m_post_parsing.mli
Properties metaprl/theories/experimental/compile/m_post_parsing.mli
+6 -2 metaprl/theories/experimental/compile/m_test.ml
+7 -1 metaprl/theories/experimental/compile/m_theory.ml
+2 -0 metaprl/theories/experimental/compile/m_theory.mli