Changeset 757 for src/LIN/LIN.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r723 r757  
    11include "LIN/JointLTLLIN.ma".
    22 
    3 definition PreLINStatement ≝ JointStatement unit.
     3definition pre_lin_statement ≝ joint_statement unit.
    44
    5 definition LINStatement ≝
     5definition lin_statement ≝
    66  λglobals.
    7     option Identifier × (PreLINStatement globals).
     7    option ident × (pre_lin_statement globals).
    88
    9 definition WellFormedP ≝
     9definition well_formed_P ≝
    1010  λA, B: Type[0].
    1111  λcode: list (option A × B).
     
    1919    ].
    2020   
    21 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    22   LIN_Fu_Internal: ∀code: list (LINStatement globals). WellFormedP ? ? code → LINFunctionDefinition globals
    23 | LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
     21inductive lin_function_definition (globals: list ident): Type[0] ≝
     22  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
     23| lin_fu_external: external_function → lin_function_definition globals.
    2424
    25 record LINProgram: Type[0] ≝
     25record lin_program: Type[0] ≝
    2626{
    27   LIN_Pr_vars: list (Identifier × nat);
    28   LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
    29   LIN_Pr_main: option Identifier
     27  lin_pr_vars: list (ident × nat);
     28  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
     29  lin_pr_main: option ident
    3030}.
    3131
    32 definition LIN_Pr_vars:
    33     LINProgram → list (Identifier × nat).
     32definition lin_pr_vars:
     33    lin_program → list (ident × nat).
    3434  # r
    3535  cases r
     
    3838qed.
    3939
    40 definition LIN_Pr_funs:
    41   ∀p: LINProgram.
    42     list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
     40definition lin_pr_funcs:
     41  ∀p: lin_program.
     42    list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))).
    4343  # r
    4444  cases r
Note: See TracChangeset for help on using the changeset viewer.