Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-04-03 00:37:31 -0800 (Wed, 03 Apr 2002)
Revision: 3562
Log message:

      So, I've defined the compile function in Mp_mc_compile to actually
      take an Fir.prog, convert the function definitions to terms,
      and then back again, in one big identity operation.  The current
      term representation of the FIR functions is a bit of a hack that
      will need to be cleaned up if anything non-trivial is to be done.
      (Each individual function is fine I hope.  It's the program as a whole
      that's represented rather poorly.  It's essentially a (term SymbolTable.t),
      one term for each fundef in the original Fir.prog.prog_funs.)
      Though, this should be sufficient for basic testing I think.
      

Changes  Path
+1 -1 metaprl/editor/ml/Conscript
+2 -1 metaprl/theories/mc/Conscript
+9 -1 metaprl/theories/mc/TODO
+11 -3 metaprl/theories/mc/mp_mc_compile.ml
+2 -2 metaprl/theories/mc/mp_mc_compile.mli
Deleted metaprl/theories/mc/mp_mc_connect.ml
Deleted metaprl/theories/mc/mp_mc_connect.mli
+18 -0 metaprl/theories/mc/mp_mc_connect_exp.ml
+5 -0 metaprl/theories/mc/mp_mc_connect_exp.mli
+20 -1 metaprl/theories/mc/mp_mc_fir_exp.ml
+12 -1 metaprl/theories/mc/mp_mc_fir_exp.mli
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect.ml
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect.mli
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_base.ml
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_base.mli
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_exp.ml
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_exp.mli
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_ty.ml
+2 -0 metaprl/theories/mc/tests/mp_mc_test_connect_ty.mli