/[mojave]/metaprl/theories/mc/mp_mc_compile.ml
ViewVC logotype

Diff of /metaprl/theories/mc/mp_mc_compile.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3561 by emre, Sun Mar 24 22:35:29 2002 UTC revision 3562 by emre, Wed Apr 3 08:37:31 2002 UTC
# Line 34  Line 34 
34    
35  include Base_theory  include Base_theory
36    
37    open Symbol
38  open Fir  open Fir
39    
40    open Mp_mc_connect_exp
41    
42  (*  (*
43   * This is an identity operation for an FIR program.   * Despite the apparently complexity, this is an identity operation for
44     * an Fir.prog. We convert the function definitions (fundef SymbolTable.t)
45     * to terms (term SymbolTable.t), and then back again.  Later, we'd
46     * like to do optimizations and proofs after we converted to terms.
47   *)   *)
48    
49  let compile fir_prog =  let compile prog =
50     fir_prog     let term_table = SymbolTable.map term_of_fundef prog.prog_funs in
51       (* Here, we'd do something like optimize or generate a proof. *)
52       let new_prog_funs = SymbolTable.map fundef_of_term term_table in
53          { prog with prog_funs = new_prog_funs }

Legend:
Removed from v.3561  
changed lines
  Added in v.3562

  ViewVC Help
Powered by ViewVC 1.1.26