Changeset 725 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Mar 30, 2011, 4:16:08 PM (9 years ago)
Author:
campbell
Message:

Do some light manual disambiguation to make Clight examples go through more
easily.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r720 r725  
    326326}.
    327327
    328 (* * Functions can either be defined ([Internal]) or declared as
    329   external functions ([External]). *)
    330 
    331 inductive fundef : Type[0] ≝
    332   | Internal: function → fundef
    333   | External: ident → typelist → type → fundef.
     328(* * Functions can either be defined ([CL_Internal]) or declared as
     329  external functions ([CL_External]).  Similar to the AST definition, but
     330  with high level type information for external functions. *)
     331
     332inductive clight_fundef : Type[0] ≝
     333  | CL_Internal: function → clight_fundef
     334  | CL_External: ident → typelist → type → clight_fundef.
    334335
    335336(* * ** Programs *)
     
    339340  data.  See module [AST] for more details. *)
    340341
    341 definition clight_program : Type[0] ≝ program fundef type.
     342definition clight_program : Type[0] ≝ program clight_fundef type.
    342343
    343344(* * * Operations over types *)
     
    354355  Tfunction (type_of_params (fn_params f)) (fn_return f).
    355356
    356 definition type_of_fundef : fundef → type ≝ λf.
     357definition type_of_fundef : clight_fundef → type ≝ λf.
    357358  match f with
    358   [ Internal fd ⇒ type_of_function fd
    359   | External id args res ⇒ Tfunction args res
     359  [ CL_Internal fd ⇒ type_of_function fd
     360  | CL_External id args res ⇒ Tfunction args res
    360361  ].
    361362
Note: See TracChangeset for help on using the changeset viewer.