Changeset 737 for src/RTLabs


Ignore:
Timestamp:
Apr 4, 2011, 5:13:09 PM (9 years ago)
Author:
campbell
Message:

Use more abstract identifiers in Clight / RTLabs.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r729 r737  
    214214    | RTLabs.St_cost (lbl, _) ->
    215215        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"
    217217          (n_spaces n)
    218218          lbl
     
    314314
    315315let 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"
    317317    (print_fun_decls 2 p.RTLabs.functs)
    318318    (print_fun 2 p.RTLabs.functs)
  • src/RTLabs/test/search.ma

    r731 r737  
    4747  definition search1 := 1.
    4848  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.
    5858
    5959
     
    154154  definition main1 := 1.
    155155  definition main0 := 0.
    156   definition C_cost9 := ident_of_nat 0.
     156  definition C_cost9 := costlabel_of_nat 0.
    157157
    158158
     
    229229   normalize  (* you can examine the result here *)
    230230   % qed.
    231 
Note: See TracChangeset for help on using the changeset viewer.