Changeset 737


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

Use more abstract identifiers in Clight / RTLabs.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/AST.ma

    r726 r737  
    2222include "common/Floats.ma".
    2323include "ASM/BitVector.ma".
     24include "common/Identifiers.ma".
    2425
    2526(* * * Syntactic elements *)
    2627
    27 (* * Identifiers (names of local variables, of global symbols and functions,
    28   etc) are represented by the type [positive] of positive integers. *)
    29 
    30 definition ident ≝ Word.
    31 
    32 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
    33 #x #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %) #E
    34 [ % | %2 ]
    35 lapply E @eq_bv_elim
    36 [ 1,4: #H #_ @H | *: #_ #H destruct ]
    37 qed.
    38 
    39 definition ident_of_nat ≝ bitvector_of_nat 16.
     28(* Global variables and functions are represented by identifiers with the
     29   tag for symbols.  Note that Clight also uses them for locals due to
     30   the ambiguous syntax. *)
     31
     32axiom SymbolTag : String.
     33
     34definition ident ≝ Identifier SymbolTag.
     35
     36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
     37
     38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
    4039
    4140(* Memory spaces *)
  • 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 
  • src/common/CostLabel.ma

    r720 r737  
    11include "Clight/AST.ma".
    22
    3 definition costlabel ≝ ident.
     3axiom CostTag : String.
     4
     5definition costlabel ≝ Identifier CostTag.
     6
     7(* For use in importing programs in intermediate languages. *)
     8definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
  • src/common/Identifiers.ma

    r736 r737  
    3232qed.
    3333
    34 definition identifer_of_nat : ∀tag:String. nat → Identifier tag ≝
     34definition identifier_of_nat : ∀tag:String. nat → Identifier tag ≝
    3535  λtag,n. an_identifier tag (bitvector_of_nat ? n).
    3636
Note: See TracChangeset for help on using the changeset viewer.