Add some form-judgements on plvals and pexps.

This commit is contained in:
Graydon Hoare 2010-09-15 12:29:45 -07:00
parent c61d021f6d
commit 77beffc889
2 changed files with 169 additions and 10 deletions

View File

@ -114,22 +114,22 @@ and ty_tag = { tag_id: opaque_id;
(* In closed type terms a constraint may refer to components of the term by
* anchoring off the "formal symbol" '*', which represents "the term this
* constraint is attached to".
*
*
*
*
* For example, if I have a tuple type tup(int,int), I may wish to enforce the
* lt predicate on it; I can write this as a constrained type term like:
*
*
* tup(int,int) : lt( *._0, *._1 )
*
*
* In fact all tuple types are converted to this form for purpose of
* type-compatibility testing; the argument tuple in a function
*
*
* fn (int x, int y) : lt(x, y) -> int
*
*
* desugars to
*
*
* fn (tup(int, int) : lt( *._1, *._2 )) -> int
*
*
*)
and carg_base =
@ -353,7 +353,7 @@ and plval =
| PLVAL_ext_pexp of (pexp * pexp)
| PLVAL_ext_deref of pexp
and pexp = pexp' Common.identified
and pexp = pexp' identified
and lit =
| LIT_nil
@ -481,6 +481,9 @@ and crate' =
and crate = crate' identified
;;
(* Utility values and functions. *)
let empty_crate' =
{ crate_items = ({ view_imports = Hashtbl.create 0;
view_exports = Hashtbl.create 0 },
@ -511,9 +514,82 @@ let sane_name (n:name) : bool =
| NAME_ext (prefix, _) -> sane_prefix prefix
;;
(*
* We have multiple subset-categories of expression:
*
* - Atomic expressions are just atomic-lvals and literals.
*
* - Primitive expressions are 1-level, machine-level operations on atomic
* expressions (so: 1-level binops and unops on atomics)
* - Constant expressions are those that can be evaluated at compile time,
* without calling user code or accessing the communication subsystem. So
* all expressions aside from call, port, chan or spawn, applied to all
* lvals that are themselves constant.
(***********************************************************************)
*
* We similarly have multiple subset-categories of lval:
*
* - Name lvals are those that contain no dynamic indices.
*
* - Atomic lvals are those indexed by atomic expressions.
*
* - Constant lvals are those that are only indexed by constant expressions.
*
* Rationales:
*
* - The primitives are those that can be evaluated without adjusting
* reference counts or otherwise perturbing the lifecycle of anything
* dynamically allocated.
*
* - The atomics exist to define the sub-structure of the primitives.
*
* - The constants are those we'll compile to read-only memory, either
* immediates in the code-stream or frags in the .rodata section.
*
* Note:
*
* - Constant-expression-ness is defined in semant, and can only be judged
* after resolve has run and connected idents with bindings.
*)
let rec plval_is_atomic (plval:plval) : bool =
match plval with
PLVAL_ident _
| PLVAL_app _ -> true
| PLVAL_ext_name (p, _) ->
pexp_is_atomic p
| PLVAL_ext_pexp (a, b) ->
(pexp_is_atomic a) &&
(pexp_is_atomic b)
| PLVAL_ext_deref p ->
pexp_is_atomic p
and pexp_is_atomic (pexp:pexp) : bool =
match pexp.node with
PEXP_lval pl -> plval_is_atomic pl
| PEXP_lit _ -> true
| _ -> false
;;
let pexp_is_primitive (pexp:pexp) : bool =
match pexp.node with
PEXP_binop (_, a, b) ->
(pexp_is_atomic a) &&
(pexp_is_atomic b)
| PEXP_unop (_, p) ->
pexp_is_atomic p
| PEXP_lval pl ->
plval_is_atomic pl
| PEXP_lit _ -> true
| _ -> false
;;
(* Pretty-printing. *)
let fmt_ident (ff:Format.formatter) (i:ident) : unit =
fmt ff "%s" i

View File

@ -98,6 +98,7 @@ type ctxt =
ctxt_slot_keys: (node_id,Ast.slot_key) Hashtbl.t;
ctxt_node_referenced: (node_id, unit) Hashtbl.t;
ctxt_auto_deref_lval: (node_id, bool) Hashtbl.t;
ctxt_plval_const: (node_id,bool) Hashtbl.t;
ctxt_all_item_names: (node_id,Ast.name) Hashtbl.t;
ctxt_all_item_types: (node_id,Ast.ty) Hashtbl.t;
ctxt_all_lval_types: (node_id,Ast.ty) Hashtbl.t;
@ -185,6 +186,7 @@ let new_ctxt sess abi crate =
ctxt_slot_keys = Hashtbl.create 0;
ctxt_node_referenced = Hashtbl.create 0;
ctxt_auto_deref_lval = Hashtbl.create 0;
ctxt_plval_const = Hashtbl.create 0;
ctxt_all_item_names = Hashtbl.create 0;
ctxt_all_item_types = Hashtbl.create 0;
ctxt_all_lval_types = Hashtbl.create 0;
@ -1340,6 +1342,87 @@ let expr_type (cx:ctxt) (e:Ast.expr) : Ast.ty =
| Ast.EXPR_atom a -> atom_type cx a
;;
let rec pexp_is_const (cx:ctxt) (pexp:Ast.pexp) : bool =
let check_opt po =
match po with
None -> true
| Some x -> pexp_is_const cx x
in
let check_mut_pexp mut p =
mut = Ast.MUT_immutable && pexp_is_const cx p
in
match pexp.node with
Ast.PEXP_call _
| Ast.PEXP_spawn _
| Ast.PEXP_port
| Ast.PEXP_chan _
| Ast.PEXP_custom _ -> false
| Ast.PEXP_bind (fn, args) ->
(pexp_is_const cx fn) &&
(arr_for_all
(fun _ a -> check_opt a)
args)
| Ast.PEXP_rec (elts, base) ->
(check_opt base) &&
(arr_for_all
(fun _ (_, mut, p) ->
check_mut_pexp mut p)
elts)
| Ast.PEXP_tup elts ->
arr_for_all
(fun _ (mut, p) ->
check_mut_pexp mut p)
elts
| Ast.PEXP_vec (mut, elts) ->
(arr_for_all
(fun _ p ->
check_mut_pexp mut p)
elts)
| Ast.PEXP_binop (_, a, b)
| Ast.PEXP_lazy_and (a, b)
| Ast.PEXP_lazy_or (a, b) ->
(pexp_is_const cx a) &&
(pexp_is_const cx b)
| Ast.PEXP_unop (_, p) -> pexp_is_const cx p
| Ast.PEXP_lval p ->
begin
match htab_search cx.ctxt_plval_const pexp.id with
None -> plval_is_const cx p
| Some b -> b
end
| Ast.PEXP_lit _
| Ast.PEXP_str _ -> true
| Ast.PEXP_box (mut, p) ->
check_mut_pexp mut p
and plval_is_const (cx:ctxt) (plval:Ast.plval) : bool =
match plval with
Ast.PLVAL_ident _
| Ast.PLVAL_app _ ->
bug () "Semant.plval_is_const on plval base"
| Ast.PLVAL_ext_name (pexp, _) ->
pexp_is_const cx pexp
| Ast.PLVAL_ext_pexp (a, b) ->
(pexp_is_const cx a) &&
(pexp_is_const cx b)
| Ast.PLVAL_ext_deref p ->
pexp_is_const cx p
;;
(* Mappings between mod items and their respective types. *)
let arg_slots (slots:Ast.header_slots) : Ast.slot array =