diff options
| -rw-r--r-- | src/rewriter.ml | 7 | ||||
| -rw-r--r-- | src/type_internal.ml | 8 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
3 files changed, 12 insertions, 5 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index 2487f8d6..bae26679 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -44,14 +44,17 @@ let rec rewrite_nexp_to_exp program_vars l nexp = or vectors *) (* let _ = Printf.printf "unbound variable here %s\n" v in*) E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) - | Some ev -> E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ))) + | Some(None,ev) -> E_aux (E_id (Id_aux (Id ev,l)), (l, simple_annot typ)) + | Some(Some f,ev) -> + E_aux (E_app ((Id_aux (Id f,l)), [ (E_aux (E_id (Id_aux (Id ev,l)), (l,simple_annot typ)))]), + (l, tag_annot typ (External (Some f))))) let rec match_to_program_vars vs bounds = match vs with | [] -> [] | v::vs -> match find_var_from_nvar v bounds with | None -> match_to_program_vars vs bounds - | Some ev -> (v,ev)::(match_to_program_vars vs bounds) + | Some(augment,ev) -> (v,(augment,ev))::(match_to_program_vars vs bounds) let rec rewrite_exp (E_aux (exp,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in diff --git a/src/type_internal.ml b/src/type_internal.ml index 1ec081a8..c8cb500d 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1810,9 +1810,13 @@ let find_var_from_nvar v bounds = match bounds with let rec find_rec bs = match bs with | [] -> None | b::bs -> (match b with - | VR_eq(ev,n) | VR_vec_eq (ev,n)-> + | VR_eq(ev,n) -> (match n.nexp with - | Nvar nv -> if nv = v then Some ev else find_rec bs + | Nvar nv -> if nv = v then Some (None,ev) else find_rec bs + | _ -> find_rec bs) + | VR_vec_eq (ev,n)-> + (match n.nexp with + | Nvar nv -> if nv = v then Some (Some "length",ev) else find_rec bs | _ -> find_rec bs) | _ -> find_rec bs) in find_rec bs diff --git a/src/type_internal.mli b/src/type_internal.mli index f50d73af..4345de7a 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -184,7 +184,7 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list) val extract_bounds : def_envs -> string -> t -> bounds_env val merge_bounds : bounds_env -> bounds_env -> bounds_env -val find_var_from_nvar : string -> bounds_env -> string option +val find_var_from_nvar : string -> bounds_env -> (string option * string) option val normalize_nexp : nexp -> nexp val get_index : nexp -> int (*TEMPORARILY expose nindex through this for debugging purposes*) |