optionally ignore errors during translation of equations
authorhaftmann
Wed Apr 21 15:20:57 2010 +0200 (2010-04-21)
changeset 362712ef9dbddfcb8
parent 36262 d7d1d87276b7
child 36272 4d358c582ffb
optionally ignore errors during translation of equations
src/Tools/Code/code_eval.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_eval.ML	Wed Apr 21 12:11:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_eval.ML	Wed Apr 21 15:20:57 2010 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  
     1.5  fun evaluation_code thy tycos consts =
     1.6    let
     1.7 -    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
     1.8 +    val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
     1.9      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
    1.10      val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
    1.11        eval_struct_name naming program (consts' @ tycos');
     2.1 --- a/src/Tools/Code/code_target.ML	Wed Apr 21 12:11:48 2010 +0200
     2.2 +++ b/src/Tools/Code/code_target.ML	Wed Apr 21 15:20:57 2010 +0200
     2.3 @@ -329,7 +329,7 @@
     2.4  
     2.5  fun code_of thy target some_width module_name cs names_stmt =
     2.6    let
     2.7 -    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
     2.8 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
     2.9    in
    2.10      string (names_stmt naming)
    2.11        (serialize thy target some_width (SOME module_name) [] naming program names_cs)
    2.12 @@ -347,15 +347,15 @@
    2.13  fun read_const_exprs thy cs =
    2.14    let
    2.15      val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
    2.16 -    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
    2.17 -    val names4 = transitivly_non_empty_funs thy naming program;
    2.18 -    val cs5 = map_filter
    2.19 -      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
    2.20 -  in fold (insert (op =)) cs5 cs1 end;
    2.21 +    val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
    2.22 +    val names3 = transitivly_non_empty_funs thy naming program;
    2.23 +    val cs3 = map_filter (fn (c, name) =>
    2.24 +      if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    2.25 +  in union (op =) cs3 cs1 end;
    2.26  
    2.27  fun export_code thy cs seris =
    2.28    let
    2.29 -    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
    2.30 +    val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
    2.31      fun mk_seri_dest dest = case dest
    2.32       of NONE => compile
    2.33        | SOME "-" => export