summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/monomorphise.ml259
-rw-r--r--src/sail.ml3
2 files changed, 262 insertions, 0 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
new file mode 100644
index 00000000..3d81ecb1
--- /dev/null
+++ b/src/monomorphise.ml
@@ -0,0 +1,259 @@
+open Parse_ast
+open Ast
+open Type_internal
+
+(* TODO: put this somewhere common *)
+
+let id_to_string (Id_aux(id,l)) =
+ match id with
+ | Id(s) -> s
+ | DeIid(s) -> s
+
+(* TODO: check for temporary failwiths *)
+
+let optmap v f =
+ match v with
+ | None -> None
+ | Some v -> Some (f v)
+
+let split_defs splits (Type_check.Env (d_env,t_env,b_env,tp_env)) defs =
+
+ (* Split a variable pattern into every possible value *)
+
+ let split id l tannot =
+ let new_l = Generated l in
+ let new_id i = Id_aux (Id i, new_l) in
+ match tannot with
+ | Type_internal.NoTyp ->
+ raise (Reporting_basic.err_general l ("No type information for variable " ^ id ^ " to split on"))
+ | Type_internal.Overload _ ->
+ raise (Reporting_basic.err_general l ("Type for variable " ^ id ^ " to split on is overloaded"))
+ | Type_internal.Base ((tparams,ty0),_,cs,_,_,_) ->
+ let () = match tparams with
+ | [] -> ()
+ | _ -> raise (Reporting_basic.err_general l ("Type for variable " ^ id ^ " to split on has parameters"))
+ in
+ let ty = match ty0.t with Tabbrev(_,ty) -> ty | _ -> ty0 in
+ let cannot () =
+ raise (Reporting_basic.err_general l
+ ("Cannot split type " ^ Type_internal.t_to_string ty ^ " for variable " ^ id))
+ in
+ (match ty.t with
+ | Tid i ->
+ (match Envmap.apply d_env.enum_env i with
+ (* enumerations *)
+ | Some ns -> List.map (fun n -> (P_aux (P_id (new_id n),(l,tannot)),
+ (id,E_aux (E_id (new_id n),(new_l,tannot))))) ns
+ | None -> cannot ())
+ (*| vectors TODO *)
+ (*| numbers TODO *)
+ | _ -> cannot ())
+ in
+
+ (* Split variable patterns at the given locations *)
+
+ let map_locs ls (Defs defs) =
+ let rec match_l = function
+ | Unknown
+ | Int _ -> []
+ | Generated l -> [] (* Could do match_l l, but only want to split user-written patterns *)
+ | Range (p,q) ->
+ List.filter (fun ((filename,line),_) ->
+ Filename.basename p.Lexing.pos_fname = filename &&
+ p.Lexing.pos_lnum <= line && line <= q.Lexing.pos_lnum) ls
+ in
+
+ let split_pat var p =
+ let rec list f = function
+ | [] -> None
+ | h::t ->
+ match f h with
+ | None -> (match list f t with None -> None | Some (l,ps,r) -> Some (h::l,ps,r))
+ | Some ps -> Some ([],ps,t)
+ in
+ let rec spl (P_aux (p,(l,annot))) =
+ let relist f ctx ps =
+ optmap (list f ps)
+ (fun (left,ps,right) ->
+ List.map (fun (p,sub) -> P_aux (ctx (left@p::right),(l,annot)),sub) ps)
+ in
+ let re f p =
+ optmap (spl p)
+ (fun ps -> List.map (fun (p,sub) -> (P_aux (f p,(l,annot)), sub)) ps)
+ in
+ let fpat (FP_aux ((FP_Fpat (id,p),annot))) =
+ optmap (spl p)
+ (fun ps -> List.map (fun (p,sub) -> FP_aux (FP_Fpat (id,p), annot), sub) ps)
+ in
+ let ipat (i,p) = optmap (spl p) (List.map (fun (p,sub) -> (i,p),sub))
+ in
+ match p with
+ | P_lit _
+ | P_wild
+ -> None
+ | P_as (p',id) ->
+ let i = id_to_string id in
+ if i = var
+ then raise (Reporting_basic.err_general l
+ ("Cannot split " ^ var ^ " on 'as' pattern"))
+ else re (fun p -> P_as (p,id)) p'
+ | P_typ (t,p') -> re (fun p -> P_typ (t,p)) p'
+ | P_id id ->
+ let i = id_to_string id in
+ if i = var
+ then Some (split i l annot)
+ else None
+ | P_app (id,ps) ->
+ relist spl (fun ps -> P_app (id,ps)) ps
+ | P_record (fps,flag) ->
+ relist fpat (fun fps -> P_record (fps,flag)) fps
+ | P_vector ps ->
+ relist spl (fun ps -> P_vector ps) ps
+ | P_vector_indexed ips ->
+ relist ipat (fun ips -> P_vector_indexed ips) ips
+ | P_vector_concat ps ->
+ relist spl (fun ps -> P_vector_concat ps) ps
+ | P_tup ps ->
+ relist spl (fun ps -> P_tup ps) ps
+ | P_list ps ->
+ relist spl (fun ps -> P_list ps) ps
+ in spl p
+ in
+
+ let map_pat (P_aux (_,(l,_)) as p) =
+ match match_l l with
+ | [] -> None
+ | [(_,var)] -> split_pat var p
+ | lvs -> raise (Reporting_basic.err_general l
+ ("Multiple variables to split on: " ^ String.concat ", " (List.map snd lvs)))
+ in
+
+ (* TODO: only warn if one of the variables is present *)
+ let check_single_pat (P_aux (_,(l,_)) as p) =
+ match match_l l with
+ | [] -> p
+ | _ -> (Reporting_basic.print_err false true l "Monomorphisation"
+ "Splitting a singleton pattern is not possible"; p)
+ in
+
+ let subst_exp subst exp =
+ (* TODO: This just sticks a let in - we really need propogation *)
+ let (subi,(E_aux (_,subannot) as sube)) = subst in
+ let E_aux (e,(l,annot)) = exp in
+ let lg = Generated l in
+ let p = P_aux (P_id (Id_aux (Id subi, lg)), subannot) in
+ E_aux (E_let (LB_aux (LB_val_implicit (p,sube),(lg,annot)), exp),(lg,annot))
+ in
+
+ let rec map_exp ((E_aux (e,annot)) as ea) =
+ let re e = E_aux (e,annot) in
+ match e with
+ | E_block es -> re (E_block (List.map map_exp es))
+ | E_nondet es -> re (E_nondet (List.map map_exp es))
+ | E_id _
+ | E_lit _
+ | E_sizeof _
+ | E_internal_exp _
+ | E_sizeof_internal _
+ | E_internal_exp_user _
+ | E_comment _
+ -> ea
+ | E_cast (t,e') -> re (E_cast (t, map_exp e'))
+ | E_app (id,es) -> re (E_app (id,List.map map_exp es))
+ | E_app_infix (e1,id,e2) -> re (E_app_infix (map_exp e1,id,map_exp e2))
+ | E_tuple es -> re (E_tuple (List.map map_exp es))
+ | E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3))
+ | E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,map_exp e1,map_exp e2,map_exp e3,ord,map_exp e4))
+ | E_vector es -> re (E_vector (List.map map_exp es))
+ | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,map_exp e)) ies,
+ map_opt_default ed))
+ | E_vector_access (e1,e2) -> re (E_vector_access (map_exp e1,map_exp e2))
+ | E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (map_exp e1,map_exp e2,map_exp e3))
+ | E_vector_update (e1,e2,e3) -> re (E_vector_update (map_exp e1,map_exp e2,map_exp e3))
+ | E_vector_update_subrange (e1,e2,e3,e4) -> re (E_vector_update_subrange (map_exp e1,map_exp e2,map_exp e3,map_exp e4))
+ | E_vector_append (e1,e2) -> re (E_vector_append (map_exp e1,map_exp e2))
+ | E_list es -> re (E_list (List.map map_exp es))
+ | E_cons (e1,e2) -> re (E_cons (map_exp e1,map_exp e2))
+ | E_record fes -> re (E_record (map_fexps fes))
+ | E_record_update (e,fes) -> re (E_record_update (map_exp e, map_fexps fes))
+ | E_field (e,id) -> re (E_field (map_exp e,id))
+ | E_case (e,cases) -> re (E_case (map_exp e, List.concat (List.map map_pexp cases)))
+ | E_let (lb,e) -> re (E_let (map_letbind lb, map_exp e))
+ | E_assign (le,e) -> re (E_assign (map_lexp le, map_exp e))
+ | E_exit e -> re (E_exit (map_exp e))
+ | E_return e -> re (E_return (map_exp e))
+ | E_assert (e1,e2) -> re (E_assert (map_exp e1,map_exp e2))
+ | E_internal_cast (ann,e) -> re (E_internal_cast (ann,map_exp e))
+ | E_comment_struc e -> re (E_comment_struc e)
+ | E_internal_let (le,e1,e2) -> re (E_internal_let (map_lexp le, map_exp e1, map_exp e2))
+ | E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
+ | E_internal_return e -> re (E_internal_return (map_exp e))
+ and map_opt_default ((Def_val_aux (ed,annot)) as eda) =
+ match ed with
+ | Def_val_empty -> eda
+ | Def_val_dec e -> Def_val_aux (Def_val_dec (map_exp e),annot)
+ and map_fexps (FES_aux (FES_Fexps (fes,flag), annot)) =
+ FES_aux (FES_Fexps (List.map map_fexp fes, flag), annot)
+ and map_fexp (FE_aux (FE_Fexp (id,e), annot)) =
+ FE_aux (FE_Fexp (id,map_exp e),annot)
+ and map_pexp (Pat_aux (Pat_exp (p,e),l)) =
+ match map_pat p with
+ | None -> [Pat_aux (Pat_exp (p,map_exp e),l)]
+ | Some patsubsts ->
+ List.map (fun (pat',subst) ->
+ let exp' = subst_exp subst e in
+ Pat_aux (Pat_exp (pat', map_exp exp'),l))
+ patsubsts
+ and map_letbind (LB_aux (lb,annot)) =
+ match lb with
+ | LB_val_explicit (tysch,p,e) -> LB_aux (LB_val_explicit (tysch,check_single_pat p,map_exp e), annot)
+ | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit (check_single_pat p,map_exp e), annot)
+ and map_lexp ((LEXP_aux (e,annot)) as le) =
+ let re e = LEXP_aux (e,annot) in
+ match e with
+ | LEXP_id _
+ | LEXP_cast _
+ -> le
+ | LEXP_memory (id,es) -> re (LEXP_memory (id,List.map map_exp es))
+ | LEXP_tup les -> re (LEXP_tup (List.map map_lexp les))
+ | LEXP_vector (le,e) -> re (LEXP_vector (map_lexp le, map_exp e))
+ | LEXP_vector_range (le,e1,e2) -> re (LEXP_vector_range (map_lexp le, map_exp e1, map_exp e2))
+ | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id))
+ in
+
+ let map_funcl (FCL_aux (FCL_Funcl (id,pat,exp),annot)) =
+ match map_pat pat with
+ | None -> [FCL_aux (FCL_Funcl (id, pat, map_exp exp), annot)]
+ | Some patsubsts ->
+ List.map (fun (pat',subst) ->
+ let exp' = subst_exp subst exp in
+ FCL_aux (FCL_Funcl (id, pat', map_exp exp'), annot))
+ patsubsts
+ in
+
+ let map_fundef (FD_aux (FD_function (r,t,e,fcls),annot)) =
+ FD_aux (FD_function (r,t,e,List.concat (List.map map_funcl fcls)),annot)
+ in
+ let map_scattered_def sd =
+ match sd with
+ | SD_aux (SD_scattered_funcl fcl, annot) ->
+ List.map (fun fcl' -> SD_aux (SD_scattered_funcl fcl', annot)) (map_funcl fcl)
+ | _ -> [sd]
+ in
+ let map_def d =
+ match d with
+ | DEF_kind _
+ | DEF_type _
+ | DEF_spec _
+ | DEF_default _
+ | DEF_reg_dec _
+ | DEF_comm _
+ -> [d]
+ | DEF_fundef fd -> [DEF_fundef (map_fundef fd)]
+ | DEF_val lb -> [DEF_val (map_letbind lb)]
+ | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd)
+
+ in
+ Defs (List.concat (List.map map_def defs))
+
+ in map_locs splits defs
diff --git a/src/sail.ml b/src/sail.ml
index 4e76551f..6ca46844 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -129,6 +129,9 @@ let main() =
-> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
let (ast,kenv,ord) = convert_ast ast in
let (ast,type_envs) = check_ast ast kenv ord in
+
+(* let ast = Monomorphise.split_defs [(("mips_insts.sail",1120),"width")] type_envs ast in*)
+
let ast = rewrite_ast ast in
let out_name = match !opt_file_out with
| None -> fst (List.hd parsed)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 13:20:04 +0000