Changeset 737 for src/RTLabs
 Timestamp:
 Apr 4, 2011, 5:13:09 PM (9 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsMatitaPrinter.ml
r729 r737 214 214  RTLabs.St_cost (lbl, _) > 215 215 i+1, 216 Printf.sprintf "%sdefinition C%s := ident_of_nat %d.\n%s"216 Printf.sprintf "%sdefinition C%s := costlabel_of_nat %d.\n%s" 217 217 (n_spaces n) 218 218 lbl … … 314 314 315 315 let print_program p = 316 Printf.sprintf "include \"RTLabs/import.ma\".\n \n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"316 Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n" 317 317 (print_fun_decls 2 p.RTLabs.functs) 318 318 (print_fun 2 p.RTLabs.functs) 
src/RTLabs/test/search.ma
r731 r737 47 47 definition search1 := 1. 48 48 definition search0 := 0. 49 definition C_cost0 := ident_of_nat 8.50 definition C_cost1 := ident_of_nat 7.51 definition C_cost8 := ident_of_nat 6.52 definition C_cost6 := ident_of_nat 5.53 definition C_cost7 := ident_of_nat 4.54 definition C_cost4 := ident_of_nat 3.55 definition C_cost5 := ident_of_nat 2.56 definition C_cost2 := ident_of_nat 1.57 definition C_cost3 := ident_of_nat 0.49 definition C_cost0 := costlabel_of_nat 8. 50 definition C_cost1 := costlabel_of_nat 7. 51 definition C_cost8 := costlabel_of_nat 6. 52 definition C_cost6 := costlabel_of_nat 5. 53 definition C_cost7 := costlabel_of_nat 4. 54 definition C_cost4 := costlabel_of_nat 3. 55 definition C_cost5 := costlabel_of_nat 2. 56 definition C_cost2 := costlabel_of_nat 1. 57 definition C_cost3 := costlabel_of_nat 0. 58 58 59 59 … … 154 154 definition main1 := 1. 155 155 definition main0 := 0. 156 definition C_cost9 := ident_of_nat 0.156 definition C_cost9 := costlabel_of_nat 0. 157 157 158 158 … … 229 229 normalize (* you can examine the result here *) 230 230 % qed. 231
Note: See TracChangeset
for help on using the changeset viewer.