Changeset 753


Ignore:
Timestamp:
Apr 14, 2011, 5:54:37 PM (9 years ago)
Author:
mulligan
Message:

Work from today.

Location:
src
Files:
1 deleted
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r745 r753  
    5858  ERTL_Pr_Main: option Identifier
    5959}.
     60
     61definition ERTL_Pr_Vars: ERTLProgram → list (Identifier × nat).
     62  # E
     63  cases E
     64  # H1 # H2 # H3
     65  @ H1
     66qed.
  • src/ERTL/ERTLToLTL.ma

    r752 r753  
    11include "ERTL/ERTL.ma".
    2  
    3 axiom translate_func:
     2include "LTL/LTL.ma".
     3 
     4axiom translate_ERTL_func:
    45  ∀globals: list Identifier.
    56    list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
    67 
    7 definition translate: ERTLProgram → LTLProgram
     8definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e)
    89  λp.
    9     let globals ≝ map ? ? \fst (ERTL_Pr_Vars e) in
    10     let ltl_pr_var ≝ ERTL_Pr_Vars e in
    11     let ltl_pr_funcs ≝ map ? ? (translate_func globals) (ERTL_Pr_Funcs e) in
     10    let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in
     11    let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in
     12      mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).
     13    # H1
     14    @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
  • src/LTL/LTL.ma

    r723 r753  
    2121  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
    2222 
    23 record LTLProgram (globals: list Identifier): Type[0] ≝
     23record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
    26   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
     25  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    2726  LTL_Pr_Main: option Identifier
    2827}.
  • src/LTL/LTLToLIN.ma

    r733 r753  
    33include "utilities/BitVectorTrieSet.ma".
    44include "common/Graphs.ma".
     5
     6axiom LTLTag: String.
    57
    68definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
     
    2628  λl: Identifier.
    2729  λg: BitVectorTrieSet 16.
    28     set_member ? l g.   
     30    set_member ? l g.
     31   
     32definition graph_lookup ≝
     33  λglobals.
     34  λl: Identifier.
     35  λg: LTLStatementGraph globals.
     36    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    2937   
    3038definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
     
    3240  λl: Identifier.
    3341  λg: LTLStatementGraph globals.
    34     graph_lookup ? g l.
     42    graph_lookup globals l g.
    3543
    36 definition foo ≝ λl2,visited,required,globals,generated,g,n.
    37  λvisit:∀globals: list Identifier.∀g: LTLStatementGraph globals.∀required: BitVectorTrieSet 16.
    38   ∀visited: BitVectorTrieSet 16.∀generated: list (PreLINStatement globals).∀l: Identifier.
    39   ∀n: nat.BitVectorTrieSet 16 × (list (PreLINStatement globals)).
     44definition foo ≝
     45  λl2, visited, required, globals, generated, g, n.
     46  λvisit:
     47  ∀globals: list Identifier.
     48  ∀g: LTLStatementGraph globals.
     49  ∀required: BitVectorTrieSet 16.
     50  ∀visited: BitVectorTrieSet 16.
     51  ∀generated: list (PreLINStatement globals).
     52  ∀l: Identifier.
     53  ∀n: nat.
     54    BitVectorTrieSet 16 × (list (PreLINStatement globals)).
    4055  if marked l2 visited then
    41     〈require lbl required, (Joint_St_Goto ? globals l2) :: generated〉
     56    〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
    4257  else
    4358   visit globals g required visited generated l2 n.
  • src/common/Identifiers.ma

    r738 r753  
    4040include "ASM/BitVectorTrie.ma".
    4141
    42 inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     42inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
     43  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
     44 
     45 
    4346definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    4447  λtag,A. an_id_map tag A (Stub A 16).
  • src/utilities/BitVectorTrieSet.ma

    r746 r753  
    7777qed.
    7878
    79 (*
    80 let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
    81   match b with
    82   [ Stub ⇒
    83 *)
    84 
    8579definition set_insert ≝
    8680  λn: nat.
Note: See TracChangeset for help on using the changeset viewer.