Changeset 1224 for src/LIN


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (8 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1183 r1224  
    2424      ]
    2525    ].
    26    
     26
     27definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
     28 λglobals.
     29  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
     30(*CSC: lookup function to be implemented *)
     31cases daemon
     32qed.
     33
     34definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals).
     35
    2736inductive lin_function_definition (globals: list ident): Type[0] ≝
    2837  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
Note: See TracChangeset for help on using the changeset viewer.