diff options
| -rw-r--r-- | language/l2.lem | 1 | ||||
| -rw-r--r-- | language/l2.ml | 1 | ||||
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | src/pretty_print.ml | 129 | ||||
| -rw-r--r-- | src/rewriter.ml | 63 | ||||
| -rw-r--r-- | src/rewriter.mli | 11 |
6 files changed, 136 insertions, 71 deletions
diff --git a/language/l2.lem b/language/l2.lem index 63869068..1055a8ff 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -281,6 +281,7 @@ and exp_aux 'a = (* Expression *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) and exp 'a = | E_aux of (exp_aux 'a) * annot 'a diff --git a/language/l2.ml b/language/l2.ml index ea3252da..d5ea7c33 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -270,6 +270,7 @@ type | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) and 'a exp = E_aux of 'a exp_aux * 'a annot diff --git a/language/l2.ott b/language/l2.ott index 721ee60f..eea0fba1 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -646,7 +646,7 @@ exp :: 'E_' ::= | ( annot ) exp :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} | annot :: :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} | annot , annot' :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} - + | let lexp = exp in exp' :: :: internal_let {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }} lexp :: 'LEXP_' ::= {{ com lvalue expression }} diff --git a/src/pretty_print.ml b/src/pretty_print.ml index cd5b1b91..0ca8a582 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1286,13 +1286,9 @@ let doc_pat_ocaml, doc_atomic_pat_ocaml = let non_bit_print () = parens (separate space [string "VvectorR"; squarebars (separate_map semi pat pats); underscore ; underscore]) in (match annot with | Base(([],t),_,_,_,_) -> - (match t.t with - | Tapp("vector",[_;_;_;TA_typ t]) | Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ t])}) -> - (match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> - parens (separate space [string "Vvector"; squarebars (separate_map semi pat pats); underscore ; underscore]) - | _ -> non_bit_print ()) - | _ -> non_bit_print ()) + if is_bit_vector t + then parens (separate space [string "Vvector"; squarebars (separate_map semi pat pats); underscore ; underscore]) + else non_bit_print() | _ -> non_bit_print ()) | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) @@ -1307,60 +1303,93 @@ let doc_exp_ocaml, doc_let_ocaml = if le isn't immediately a ref cell, then maybe have a function to cope? *) doc_op coloneq (doc_lexp le) (exp e) - | E_vector_append(l,r) -> - group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r)) - | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) - | E_if(c,t,E_aux(E_block [], _)) -> + | E_vector_append(l,r) -> + group (parens (string "vector_append ") ^^ (exp l) ^^ space ^^ (exp r)) + | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) + | E_if(c,t,E_aux(E_block [], _)) -> string "if" ^^ space ^^ string "toBool" ^^ (exp c) ^/^ string "then" ^^ space ^^ (exp t) - | E_if(c,t,e) -> + | E_if(c,t,e) -> string "if" ^^ space ^^ string "toBool" ^^ group (exp c) ^/^ string "then" ^^ space ^^ group (exp t) ^/^ string "else" ^^ space ^^ group (exp e) - | E_for(id,exp1,exp2,(E_aux(exp3, (l3,annot3))),(Ord_aux(order,_)),exp4) -> - (match exp3 with - | E_lit (L_aux( (L_num 1), _)) -> - string "for" ^^ space ^^ - (group ((doc_id id) ^^ space ^^ equals ^^ (exp exp1))) ^^ + | E_for(id,exp1,exp2,(E_aux(exp3, (l3,annot3))),(Ord_aux(order,_)),exp4) -> + (match exp3 with + | E_lit (L_aux( (L_num 1), _)) -> + string "for" ^^ space ^^ + (group ((doc_id id) ^^ space ^^ equals ^^ (exp exp1))) ^^ (match order with | Ord_inc -> (group (string "to" ^^ space ^^ (exp exp2))) | _ -> (group (string "downto" ^^ space ^^ (exp exp2)))) ^^ string "do" ^/^ exp exp4 ^/^ string "done" - | _ -> string "make a while loop") - | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) - | E_app(f,args) -> - (*TODO, check for external call, make call-by-copy semantics*) - doc_unop (doc_id f) (parens (separate_map comma exp args)) - | E_vector_access(v,e) -> - parens ((string "vector_access") ^^ space ^^ exp v ^^ space ^^ exp e) - | E_vector_subrange(v,e1,e2) -> + | _ -> string "make a while loop") + | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) + | E_app(f,args) -> + let call = match annot with + | Base(_,External (Some n),_,_,_) -> string n + | _ -> doc_id_ocaml f in + doc_unop call (parens (separate_map comma exp args)) + | E_vector_access(v,e) -> + let call = (match annot with + | Base((_,t),_,_,_,_) -> + (match t.t with + | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (string "bit_vector_access") + | _ -> (string "vector_access")) + | _ -> (string "vector_access")) in + parens (call ^^ space ^^ exp v ^^ space ^^ exp e) + | E_vector_subrange(v,e1,e2) -> parens ((string "vector_subrange") ^^ space ^^ exp v ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | E_field(fexp,id) -> exp fexp ^^ dot ^^ doc_id id - | E_block [] -> string "()" - | E_block exps | E_nondet exps -> + | E_field(fexp,id) -> exp fexp ^^ dot ^^ doc_id id + | E_block [] -> string "()" + | E_block exps | E_nondet exps -> let exps_doc = separate_map (semi ^^ hardline) exp exps in surround 2 1 (string "begin") exps_doc (string "end") - | E_id id -> doc_id id - | E_lit lit -> doc_lit lit - | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ typ))) - | E_tuple exps -> + | E_id id -> doc_id id + | E_lit lit -> doc_lit lit + | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ typ))) + | E_tuple exps -> parens (separate_map comma exp exps) - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> + | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> braces (separate_map semi_sp doc_fexp fexps) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> + | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) - | E_vector exps -> - (*TODO pull out direction and base value*) - group ((string "make_vector") ^^ space ^^ squarebars (separate_map semi exp exps)) - | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> - (*TODO, indexed vectors shouldn't be in anymore by this point*) - let default_string = - (match default with - | Def_val_empty -> string "" - | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in - let iexp (i,e) = doc_op equals (doc_int i) (exp e) in - brackets (concat [(separate_map comma iexp iexps); default_string]) + | E_vector exps -> + (match annot with + | Base((_,t),_,_,_,_) -> + match t.t with + | Tapp("vector", [TA_nexp start; _; TA_ord order; _]) | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) -> + let call = if is_bit_vector t then (string "make_bit_vector") else (string "make_vector") in + let dir,dir_out = match order.order with + | Oinc -> true,"true" + | _ -> false, "false" in + let start = match start.nexp with + | Nconst i -> string_of_big_int i + | N2n(_,Some i) -> string_of_big_int i + | _ -> if dir then "0" else string_of_int (List.length exps) in + group (call ^^ space ^^ squarebars (separate_map semi exp exps) ^^ string start ^^ string dir_out)) + | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> + (match annot with + | Base((_,t),_,_,_,_) -> + match t.t with + | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _]) + | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) -> + let call = if is_bit_vector t then (string "make_indexed_bitv") else (string "make_indexed_v") in + let dir,dir_out = match order.order with + | Oinc -> true,"true" + | _ -> false, "false" in + let start = match start.nexp with + | Nconst i -> string_of_big_int i + | N2n(_,Some i) -> string_of_big_int i + | _ -> if dir then "0" else string_of_int (List.length iexps) in + let size = match len.nexp with + | Nconst i | N2n(_,Some i)-> string_of_big_int i in + let default_string = + (match default with + | Def_val_empty -> string "None" + | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in + let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in + group (call ^^ (brackets (separate_map semi iexp iexps)) ^^ space ^^ default_string ^^ string start ^^ string size ^^ string dir_out)) | E_vector_update(v,e1,e2) -> (*Has never happened to date*) brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2))) @@ -1378,16 +1407,20 @@ let doc_exp_ocaml, doc_let_ocaml = | E_exit e -> separate space [string "exit"; exp e;] | E_app_infix (e1,id,e2) -> - separate space [string "get_external_function_name"; parens (separate_map semi exp [e1;e2])] + let call = + match annot with + | Base((_,t),External(Some name),_,_,_) -> string name + | _ -> doc_id_ocaml id in + separate space [call; parens (separate_map semi exp [e1;e2])] and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> prefix 2 1 - (separate space [string "let"; doc_atomic_pat pat; equals]) + (separate space [string "let"; doc_atomic_pat_ocaml pat; equals]) (exp e) | LB_val_implicit(pat,e) -> prefix 2 1 - (separate space [string "let"; doc_atomic_pat pat; equals]) + (separate space [string "let"; doc_atomic_pat_ocaml pat; equals]) (exp e) and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) diff --git a/src/rewriter.ml b/src/rewriter.ml index 74eb4bb1..8a0c0599 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -6,6 +6,15 @@ type 'a exp = 'a Ast.exp type 'a emap = 'a Envmap.t type envs = Type_check.envs +type 'a rewriters = { rewrite_exp : 'a rewriters -> nexp_map option -> 'a exp -> 'a exp; + rewrite_lexp : 'a rewriters -> nexp_map option -> 'a lexp -> 'a lexp; + rewrite_pat : 'a rewriters -> nexp_map option -> 'a pat -> 'a pat; + rewrite_let : 'a rewriters -> nexp_map option -> 'a letbind -> 'a letbind; + rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; + rewrite_def : 'a rewriters -> 'a def -> 'a def; + rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + } + let rec partial_assoc (eq: 'a -> 'a -> bool) (v: 'a) (ls : ('a *'b) list ) : 'b option = match ls with | [] -> None | (v1,v2)::ls -> if (eq v1 v) then Some v2 else partial_assoc eq v ls @@ -63,9 +72,9 @@ let rec match_to_program_vars ns bounds = (*let _ = Printf.eprintf "adding n %s to program var %s\n" (n_to_string n) ev in*) (n,(augment,ev))::(match_to_program_vars ns bounds) -let rec rewrite_exp nmap (E_aux (exp,(l,annot))) = +let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) = let rewrap e = E_aux (e,(l,annot)) in - let rewrite = rewrite_exp nmap in + let rewrite = rewriters.rewrite_exp rewriters nmap in match exp with | E_block exps -> rewrap (E_block (List.map rewrite exps)) | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps)) @@ -109,8 +118,8 @@ let rec rewrite_exp nmap (E_aux (exp,(l,annot))) = (List.map (fun (Pat_aux (Pat_exp(p,e),pannot)) -> Pat_aux (Pat_exp(p,rewrite e),pannot)) pexps))) - | E_let (letbind,body) -> rewrap (E_let(rewrite_let nmap letbind,rewrite body)) - | E_assign (lexp,exp) -> rewrap (E_assign(rewrite_lexp nmap lexp,rewrite exp)) + | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body)) + | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp)) | E_exit e -> rewrap (E_exit (rewrite e)) | E_internal_cast ((_,casted_annot),exp) -> let new_exp = rewrite exp in @@ -191,45 +200,48 @@ let rec rewrite_exp nmap (E_aux (exp,(l,annot))) = raise (Reporting_basic.err_unreachable l ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti)))) | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot"))) + | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced") -and rewrite_let map (LB_aux(letbind,(l,annot))) = +let rewrite_let rewriters map (LB_aux(letbind,(l,annot))) = let map = merge_option_maps map (get_map_tannot annot) in match letbind with | LB_val_explicit (typschm, pat,exp) -> - LB_aux(LB_val_explicit (typschm,pat, rewrite_exp map exp),(l,annot)) + LB_aux(LB_val_explicit (typschm,pat, rewriters.rewrite_exp rewriters map exp),(l,annot)) | LB_val_implicit ( pat, exp) -> - LB_aux(LB_val_implicit (pat,rewrite_exp map exp),(l,annot)) + LB_aux(LB_val_implicit (pat,rewriters.rewrite_exp rewriters map exp),(l,annot)) -and rewrite_lexp map (LEXP_aux(lexp,(l,annot))) = +let rewrite_lexp rewriters map (LEXP_aux(lexp,(l,annot))) = let rewrap le = LEXP_aux(le,(l,annot)) in match lexp with | LEXP_id _ | LEXP_cast _ -> rewrap lexp - | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewrite_exp map) exps)) - | LEXP_vector (lexp,exp) -> rewrap (LEXP_vector (rewrite_lexp map lexp,rewrite_exp map exp)) + | LEXP_memory (id,exps) -> rewrap (LEXP_memory(id,List.map (rewriters.rewrite_exp rewriters map) exps)) + | LEXP_vector (lexp,exp) -> + rewrap (LEXP_vector (rewriters.rewrite_lexp rewriters map lexp,rewriters.rewrite_exp rewriters map exp)) | LEXP_vector_range (lexp,exp1,exp2) -> - rewrap (LEXP_vector_range (rewrite_lexp map lexp,rewrite_exp map exp1,rewrite_exp map exp2)) - | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewrite_lexp map lexp,id)) + rewrap (LEXP_vector_range (rewriters.rewrite_lexp rewriters map lexp, + rewriters.rewrite_exp rewriters map exp1, + rewriters.rewrite_exp rewriters map exp2)) + | LEXP_field (lexp,id) -> rewrap (LEXP_field (rewriters.rewrite_lexp rewriters map lexp,id)) -let rewrite_fun (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = +let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),(l,annot))) = (*let _ = Printf.eprintf "Rewriting function %s, pattern %s\n" (match id with (Id_aux (Id i,_)) -> i) (Pretty_print.pat_to_string pat) in*) - (FCL_aux (FCL_Funcl (id,pat,rewrite_exp (get_map_tannot fdannot) exp),(l,annot))) + (FCL_aux (FCL_Funcl (id,pat,rewriters.rewrite_exp rewriters (get_map_tannot fdannot) exp),(l,annot))) in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) -let rewrite_def d = match d with +let rewrite_def rewriters d = match d with | DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d - | DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef) - | DEF_val letbind -> DEF_val (rewrite_let None letbind) + | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef) + | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters None letbind) | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter") -let rewrite_defs (Defs defs) = +let rewrite_defs_base rewriters (Defs defs) = let rec rewrite ds = match ds with | [] -> [] - | d::ds -> (rewrite_def d)::(rewrite ds) in + | d::ds -> (rewriters.rewrite_def rewriters d)::(rewrite ds) in Defs (rewrite defs) - let explode s = let rec exp i l = if i < 0 then l else exp (i - 1) (s.[i] :: l) in exp (String.length s - 1) [] @@ -257,7 +269,7 @@ let vector_string_to_bit_list lit = let s_bin = match lit with | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode s_hex)) - | L_bin s_bin -> explode s_bin in + | L_bin s_bin -> explode (String.uppercase s_bin) in List.map (function '0' -> L_aux (L_zero, Unknown) | '1' -> L_aux (L_one,Unknown)) s_bin @@ -274,3 +286,12 @@ let remove_vector_string_expressions exp = match exp with (vector_string_to_bit_list lit) in E_vector es | _ -> exp + +let rewrite_defs (Defs defs) = rewrite_defs_base + {rewrite_exp = rewrite_exp; + rewrite_pat = (fun _ _ p -> p); + rewrite_let = rewrite_let; + rewrite_lexp = rewrite_lexp; + rewrite_fun = rewrite_fun; + rewrite_def = rewrite_def; + rewrite_defs = rewrite_defs_base} (Defs defs) diff --git a/src/rewriter.mli b/src/rewriter.mli index 1f1a2591..419be937 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -6,5 +6,14 @@ type 'a exp = 'a Ast.exp type 'a emap = 'a Envmap.t type envs = Type_check.envs -val rewrite_exp : nexp_map option -> tannot exp -> tannot exp +type 'a rewriters = { rewrite_exp : 'a rewriters -> nexp_map option -> 'a exp -> 'a exp; + rewrite_lexp : 'a rewriters -> nexp_map option -> 'a lexp -> 'a lexp; + rewrite_pat : 'a rewriters -> nexp_map option -> 'a pat -> 'a pat; + rewrite_let : 'a rewriters -> nexp_map option -> 'a letbind -> 'a letbind; + rewrite_fun : 'a rewriters -> 'a fundef -> 'a fundef; + rewrite_def : 'a rewriters -> 'a def -> 'a def; + rewrite_defs : 'a rewriters -> 'a defs -> 'a defs; + } + +val rewrite_exp : tannot rewriters -> nexp_map option -> tannot exp -> tannot exp val rewrite_defs : tannot defs -> tannot defs |