Changeset 757 for src/LTL


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r753 r757  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 
    43include "LIN/LIN.ma".
    54
    6 definition LTLStatement ≝ JointStatement Identifier.
     5definition ltl_statement ≝ joint_statement ident.
    76 
    8 definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
     7definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
    98 
    10 record LTLInternalFunction (globals: list Identifier): Type[0] ≝
     9record ltl_internal_function (globals: list ident): Type[0] ≝
    1110{
    12   LTL_IF_LUniverse: Universe;
    13   LTL_IF_StackSize: nat;
    14   LTL_IF_Graph: LTLStatementGraph globals;
    15   LTL_IF_Entry: label;
    16   LTL_IF_Exit: label
     11  ltl_if_luniverse: universe LabelTag;
     12  ltl_if_runiverse: universe RegisterTag;
     13  ltl_if_StackSize: nat;
     14  ltl_if_Graph: ltl_statement_graph globals;
     15  ltl_if_Entry: label;
     16  ltl_if_Exit: label
    1717}.
    1818
    19 inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
    20   | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
    21   | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
     19inductive ltl_function_definition (globals: list ident): Type[0] ≝
     20  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
     21  | ltl_fu_external_function: external_function → ltl_function_definition globals.
    2222 
    23 record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
     23record ltl_program (globals: list (ident × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    26   LTL_Pr_Main: option Identifier
     25  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
     26  ltl_pr_main: option ident
    2727}.
  • src/LTL/LTLToLIN.ma

    r753 r757  
    66axiom LTLTag: String.
    77
    8 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
    9   λglobals: list Identifier.
    10   λs: LTLStatement globals.
     8definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
     9  λglobals: list ident.
     10  λs: ltl_statement globals.
    1111    match s with
    12     [ Joint_St_Return ⇒ Joint_St_Return ? globals
    13     | Joint_St_Sequential instr _ ⇒ Joint_St_Sequential ? globals instr it
    14     | Joint_St_Goto lbl ⇒ Joint_St_Goto ? globals lbl
     12    [ joint_st_return ⇒ joint_st_return ? globals
     13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
     14    | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
    1515    ].
    1616   
    17 definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: Identifier.
     17definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     18  λl: ident.
    1919  λg: BitVectorTrieSet 16.
    2020    set_insert ? l g.
    2121   
    22 definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: Identifier.
     22definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     23  λl: ident.
    2424  λg: BitVectorTrieSet 16.
    2525    set_insert ? l g.
    2626   
    27 definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
    28   λl: Identifier.
     27definition marked: ident → BitVectorTrieSet 16 → bool ≝
     28  λl: ident.
    2929  λg: BitVectorTrieSet 16.
    3030    set_member ? l g.
     
    3232definition graph_lookup ≝
    3333  λglobals.
    34   λl: Identifier.
    35   λg: LTLStatementGraph globals.
     34  λl: ident.
     35  λg: ltl_statement_graph globals.
    3636    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    3737   
     
    5858   visit globals g required visited generated l2 n.
    5959
    60 let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
     60let rec visit (globals: list ident) (g: ltl_statement_graph globals)
    6161              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    62               (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     62              (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
    6363  match n with
    6464  [ O ⇒ 〈required, generated〉
     
    7171      let generated'' ≝ translated_statement :: generated in
    7272      match statement with
    73       [ Joint_St_Sequential instr l2 ⇒
     73      [ joint_st_sequential instr l2 ⇒
    7474        match instr with
    75         [ Joint_Instr_CondAcc l1 ⇒
     75        [ joint_instr_cond_acc l1 ⇒
    7676            let required' ≝
    7777              if marked l2 visited' then
     
    101101            visit globals g required' visited' generated'' l2 n'
    102102        ]
    103       | Joint_St_Goto lbl ⇒
     103      | joint_st_goto lbl ⇒
    104104        let required' ≝
    105105          if marked lbl visited' then
     
    111111        else
    112112          visit globals g required' visited' generated'' lbl n'
    113       | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     113      | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    114114      ]
    115115    ]
Note: See TracChangeset for help on using the changeset viewer.