equal
deleted
inserted
replaced
426 then error (env_var ^ " not set; cannot check code for " ^ target) |
426 then error (env_var ^ " not set; cannot check code for " ^ target) |
427 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
427 else warning (env_var ^ " not set; skipped checking code for " ^ target) |
428 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
428 else Isabelle_System.with_tmp_dir "Code_Test" ext_check |
429 end; |
429 end; |
430 |
430 |
431 fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) = |
431 fun subevaluator mounted_serializer prepared_program syms all_public ((vs, ty), t) = |
432 let |
432 let |
433 val _ = if Code_Thingol.contains_dict_var t then |
433 val _ = if Code_Thingol.contains_dict_var t then |
434 error "Term to be evaluated contains free dictionaries" else (); |
434 error "Term to be evaluated contains free dictionaries" else (); |
435 val v' = singleton (Name.variant_list (map fst vs)) "a"; |
435 val v' = singleton (Name.variant_list (map fst vs)) "a"; |
436 val vs' = (v', []) :: vs; |
436 val vs' = (v', []) :: vs; |
447 |
447 |
448 fun evaluator ctxt target program syms = |
448 fun evaluator ctxt target program syms = |
449 let |
449 let |
450 val (mounted_serializer, (_, prepared_program)) = |
450 val (mounted_serializer, (_, prepared_program)) = |
451 mount_serializer ctxt target NONE generatedN [] program syms; |
451 mount_serializer ctxt target NONE generatedN [] program syms; |
452 in evaluation mounted_serializer prepared_program syms end; |
452 in subevaluator mounted_serializer prepared_program syms end; |
453 |
453 |
454 end; (* local *) |
454 end; (* local *) |
455 |
455 |
456 |
456 |
457 (* code generation *) |
457 (* code generation *) |