annotate ppc/mach.mli @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
rev   line source
mike@0 1 (* ppc/mach.mli *)
mike@0 2 (* Copyright (c) 2017 J. M. Spivey *)
mike@0 3
mike@0 4 (*
mike@0 5 This module contains a number of constants that define the layout of
mike@0 6 data in the target machine. The |metrics| records |int_rep|, etc.,
mike@0 7 define the representation of the primitive types of picoPascal;
mike@0 8 |param_rep| defines the representation of procedure parameters, and
mike@0 9 |proc_rep| defines the representation of closures.
mike@0 10
mike@0 11 |addr_size| is the size of an address in the target machine,
mike@0 12 |param_size| is the size of a parameter, and |max_align| is the
mike@0 13 maximum alignment constraint of any primitive type. Arrays and
mike@0 14 records are always aligned to a multiple of |max_align|, so that all
mike@0 15 their elements will be correctly aligned. |frame_head level| is the
mike@0 16 size of the fixed part of a procedure frame for static level
mike@0 17 |level|.
mike@0 18 *)
mike@0 19
mike@0 20 (* |metrics| -- target representation of data object *)
mike@0 21 type metrics =
mike@0 22 { r_size: int; (* Size of object *)
mike@0 23 r_align: int } (* Address must be multiple of this *)
mike@0 24
mike@0 25 val int_rep : metrics (* Integer type *)
mike@0 26 val char_rep : metrics (* Char type *)
mike@0 27 val bool_rep : metrics (* Boolean type *)
mike@0 28 val void_rep : metrics (* Void type *)
mike@0 29 val addr_rep : metrics (* All addresses *)
mike@0 30 val proc_rep : metrics (* Closures *)
mike@0 31 val param_rep : metrics (* Procedure parameters *)
mike@0 32 val max_align : int
mike@0 33
mike@0 34 val param_base : int (* +ve offset of first param from fp *)
mike@0 35 val local_base : int (* -ve offset of bottom of frame head *)
mike@0 36 val stat_link : int (* Offset of static link *)