diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 63 | ||||
| -rw-r--r-- | src/ast_util.mli | 11 | ||||
| -rw-r--r-- | src/initial_check.ml | 336 | ||||
| -rw-r--r-- | src/lexer.mll | 4 | ||||
| -rw-r--r-- | src/parse_ast.ml | 49 | ||||
| -rw-r--r-- | src/parser.mly | 108 | ||||
| -rw-r--r-- | src/pattern_completeness.ml | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 33 | ||||
| -rw-r--r-- | src/process_file.ml | 36 | ||||
| -rw-r--r-- | src/rewriter.ml | 8 | ||||
| -rw-r--r-- | src/rewriter.mli | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 624 | ||||
| -rw-r--r-- | src/rewrites.mli | 3 | ||||
| -rw-r--r-- | src/sail_lib.ml | 87 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 6 | ||||
| -rw-r--r-- | src/type_check.ml | 650 | ||||
| -rw-r--r-- | src/type_check.mli | 44 | ||||
| -rw-r--r-- | src/value.ml | 14 |
18 files changed, 1932 insertions, 151 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 968cb320..82e39022 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -85,6 +85,9 @@ let untyp_pat = function let mk_pexp pexp_aux = Pat_aux (pexp_aux, no_annot) +let mk_mpat mpat_aux = MP_aux (mpat_aux, no_annot) +let mk_mpexp mpexp_aux = MPat_aux (mpexp_aux, no_annot) + let mk_lexp lexp_aux = LEXP_aux (lexp_aux, no_annot) let mk_typ_pat tpat_aux = TP_aux (tpat_aux, Parse_ast.Unknown) @@ -445,7 +448,32 @@ and map_pat_annot_aux f = function | P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats) | P_vector pats -> P_vector (List.map (map_pat_annot f) pats) | P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2) + | P_string_append pats -> P_string_append (List.map (map_pat_annot f) pats) + +and map_mpexp_annot f (MPat_aux (mpexp, annot)) = MPat_aux (map_mpexp_annot_aux f mpexp, f annot) +and map_mpexp_annot_aux f = function + | MPat_pat mpat -> MPat_pat (map_mpat_annot f mpat) + | MPat_when (mpat, guard) -> MPat_when (map_mpat_annot f mpat, map_exp_annot f guard) + +and map_mapcl_annot f (MCL_aux (MCL_mapcl (mpexp1, mpexp2), annot)) = + MCL_aux (MCL_mapcl (map_mpexp_annot f mpexp1, map_mpexp_annot f mpexp2), f annot) + +and map_mpat_annot f (MP_aux (mpat, annot)) = MP_aux (map_mpat_annot_aux f mpat, f annot) +and map_mpat_annot_aux f = function + | MP_lit lit -> MP_lit lit + | MP_id id -> MP_id id + | MP_app (id, mpats) -> MP_app (id, List.map (map_mpat_annot f) mpats) + | MP_record (fmpats, b) -> MP_record (List.map (map_mfpat_annot f) fmpats, b) + | MP_tup mpats -> MP_tup (List.map (map_mpat_annot f) mpats) + | MP_list mpats -> MP_list (List.map (map_mpat_annot f) mpats) + | MP_vector_concat mpats -> MP_vector_concat (List.map (map_mpat_annot f) mpats) + | MP_vector mpats -> MP_vector (List.map (map_mpat_annot f) mpats) + | MP_cons (mpat1, mpat2) -> MP_cons (map_mpat_annot f mpat1, map_mpat_annot f mpat2) + | MP_string_append mpats -> MP_string_append (List.map (map_mpat_annot f) mpats) + | MP_typ (mpat, typ) -> MP_typ (map_mpat_annot f mpat, typ) + and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot) +and map_mfpat_annot f (MFP_aux (MFP_mpat (id, mpat), annot)) = MFP_aux (MFP_mpat (id, map_mpat_annot f mpat), f annot) and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot) and map_letbind_annot_aux f = function | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp) @@ -480,6 +508,7 @@ let def_loc = function | DEF_kind (KD_aux (_, (l, _))) | DEF_type (TD_aux (_, (l, _))) | DEF_fundef (FD_aux (_, (l, _))) + | DEF_mapdef (MD_aux (_, (l, _))) | DEF_val (LB_aux (_, (l, _))) | DEF_spec (VS_aux (_, (l, _))) | DEF_default (DT_aux (_, l)) @@ -578,6 +607,7 @@ and string_of_typ_aux = function | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2 | Typ_exist (kids, nc, typ) -> "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}" and string_of_typ_arg = function @@ -718,7 +748,23 @@ and string_of_pat (P_aux (pat, l)) = | P_vector_concat pats -> string_of_list " : " string_of_pat pats | P_vector pats -> "[" ^ string_of_list ", " string_of_pat pats ^ "]" | P_as (pat, id) -> string_of_pat pat ^ " as " ^ string_of_id id + | P_string_append pats -> string_of_list " ^^ " string_of_pat pats | _ -> "PAT" + +and string_of_mpat (MP_aux (pat, l)) = + match pat with + | MP_lit lit -> string_of_lit lit + | MP_id v -> string_of_id v + | MP_tup pats -> "(" ^ string_of_list ", " string_of_mpat pats ^ ")" + | MP_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_mpat pats ^ ")" + | MP_cons (pat1, pat2) -> string_of_mpat pat1 ^ " :: " ^ string_of_mpat pat2 + | MP_list pats -> "[||" ^ string_of_list "," string_of_mpat pats ^ "||]" + | MP_vector_concat pats -> string_of_list " : " string_of_mpat pats + | MP_vector pats -> "[" ^ string_of_list ", " string_of_mpat pats ^ "]" + | MP_string_append pats -> string_of_list " ^^ " string_of_mpat pats + | MP_typ (mpat, typ) -> "(" ^ string_of_mpat mpat ^ " : " ^ string_of_typ typ ^ ")" + | _ -> "MPAT" + and string_of_lexp (LEXP_aux (lexp, _)) = match lexp with | LEXP_id v -> string_of_id v @@ -755,6 +801,9 @@ let rec pat_ids (P_aux (pat_aux, _)) = IdSet.union (pat_ids pat1) (pat_ids pat2) | P_record (fpats, _) -> List.fold_right IdSet.union (List.map fpat_ids fpats) IdSet.empty + | P_string_append pats -> + List.fold_right IdSet.union (List.map pat_ids pats) IdSet.empty + and fpat_ids (FP_aux (FP_Fpat (_, pat), _)) = pat_ids pat let id_of_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) = @@ -940,6 +989,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) = | Typ_id _ -> KidSet.empty | Typ_var kid -> KidSet.singleton kid | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) + | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2) | Typ_tup ts -> List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t)) KidSet.empty ts @@ -984,7 +1034,7 @@ let rec undefined_of_typ mwords l annot (Typ_aux (typ_aux, _) as typ) = initial_check.ml. i.e. the rewriter should only encounter this case when re-writing those functions. *) wrap (E_id (prepend_id "typ_" (id_of_kid kid))) typ - | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) + | Typ_bidir _ | Typ_fn _ | Typ_exist _ -> assert false (* Typ_exist should be re-written *) and undefined_of_typ_args mwords l annot (Typ_arg_aux (typ_arg_aux, _) as typ_arg) = match typ_arg_aux with | Typ_arg_nexp n -> [E_aux (E_sizeof n, (l, annot (atom_typ n)))] @@ -1001,6 +1051,17 @@ let construct_pexp (pat,guard,exp,ann) = | None -> Pat_aux (Pat_exp (pat,exp),ann) | Some guard -> Pat_aux (Pat_when (pat,guard,exp),ann) +let destruct_mpexp (MPat_aux (mpexp,ann)) = + match mpexp with + | MPat_pat mpat -> mpat,None,ann + | MPat_when (mpat,guard) -> mpat,Some guard,ann + +let construct_mpexp (mpat,guard,ann) = + match guard with + | None -> MPat_aux (MPat_pat mpat,ann) + | Some guard -> MPat_aux (MPat_when (mpat,guard),ann) + + let is_valspec id = function | DEF_spec (VS_aux (VS_val_spec (_, id', _, _), _)) when Id.compare id id' = 0 -> true | _ -> false diff --git a/src/ast_util.mli b/src/ast_util.mli index c07732bf..6fb1c576 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -70,7 +70,9 @@ val mk_nc : n_constraint_aux -> n_constraint val mk_nexp : nexp_aux -> nexp val mk_exp : unit exp_aux -> unit exp val mk_pat : unit pat_aux -> unit pat +val mk_mpat : unit mpat_aux -> unit mpat val mk_pexp : unit pexp_aux -> unit pexp +val mk_mpexp : unit mpexp_aux -> unit mpexp val mk_lexp : unit lexp_aux -> unit lexp val mk_lit : lit_aux -> lit val mk_lit_exp : lit_aux -> unit exp @@ -174,6 +176,10 @@ val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat val map_pexp_annot : ('a annot -> 'b annot) -> 'a pexp -> 'b pexp val map_lexp_annot : ('a annot -> 'b annot) -> 'a lexp -> 'b lexp val map_letbind_annot : ('a annot -> 'b annot) -> 'a letbind -> 'b letbind +val map_mpat_annot : ('a annot -> 'b annot) -> 'a mpat -> 'b mpat +val map_mfpat_annot : ('a annot -> 'b annot) -> 'a mfpat -> 'b mfpat +val map_mpexp_annot : ('a annot -> 'b annot) -> 'a mpexp -> 'b mpexp +val map_mapcl_annot : ('a annot -> 'b annot) -> 'a mapcl -> 'b mapcl (* Extract locations from identifiers *) val id_loc : id -> Parse_ast.l @@ -209,6 +215,7 @@ val string_of_exp : 'a exp -> string val string_of_pexp : 'a pexp -> string val string_of_lexp : 'a lexp -> string val string_of_pat : 'a pat -> string +val string_of_mpat : 'a mpat -> string val string_of_letbind : 'a letbind -> string val string_of_index_range : index_range -> string @@ -307,6 +314,10 @@ val undefined_of_typ : bool -> Ast.l -> (typ -> 'annot) -> typ -> 'annot exp val destruct_pexp : 'a pexp -> 'a pat * ('a exp) option * 'a exp * (Ast.l * 'a) val construct_pexp : 'a pat * ('a exp) option * 'a exp * (Ast.l * 'a) -> 'a pexp +val destruct_mpexp : 'a mpexp -> 'a mpat * ('a exp) option * (Ast.l * 'a) +val construct_mpexp : 'a mpat * ('a exp) option * (Ast.l * 'a) -> 'a mpexp + + val is_valspec : id -> 'a def -> bool val is_fundef : id -> 'a def -> bool diff --git a/src/initial_check.ml b/src/initial_check.ml index 1ba1b9e6..e1dd906b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -165,51 +165,53 @@ let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst), | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) : Ast.typ = -(* let _ = Printf.eprintf "to_ast_typ\n" in*) + (* let _ = Printf.eprintf "to_ast_typ\n" in*) match t with | Parse_ast.ATyp_aux(t,l) -> - Typ_aux( (match t with - | Parse_ast.ATyp_id(id) -> Typ_id (to_ast_id id) - | Parse_ast.ATyp_var(v) -> - let v = to_ast_var v in - let mk = Envmap.apply k_env (var_to_string v) in - (match mk with - | Some(k) -> (match k.k with - | K_Typ -> Typ_var v - | K_infer -> k.k <- K_Typ; Typ_var v - | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) - | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg), - (to_ast_typ k_env def_ord ret), - (to_ast_effects k_env efct)) - | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs) - | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_tb",il), [ b; r; ord ; ti]) -> - let make_r bot top = - match bot,top with - | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) - | bot,(Parse_ast.ATyp_aux(_,l) as top) -> - Parse_ast.ATyp_aux((Parse_ast.ATyp_sum - ((Parse_ast.ATyp_aux - (Parse_ast.ATyp_sum (top, - Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), - Parse_ast.Unknown)), - (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in - let base = to_ast_nexp k_env b in - let rise = match def_ord with - | Ord_aux(Ord_inc,dl) -> to_ast_nexp k_env (make_r b r) - | Ord_aux(Ord_dec,dl) -> to_ast_nexp k_env (make_r r b) - | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in - Typ_app(Id_aux(Id "vector",il), - [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown); - Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) - | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> - let make_sub_one t = - match t with + Typ_aux( (match t with + | Parse_ast.ATyp_id(id) -> Typ_id (to_ast_id id) + | Parse_ast.ATyp_var(v) -> + let v = to_ast_var v in + let mk = Envmap.apply k_env (var_to_string v) in + (match mk with + | Some(k) -> (match k.k with + | K_Typ -> Typ_var v + | K_infer -> k.k <- K_Typ; Typ_var v + | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) + | None -> typ_error l "Encountered an unbound variable" None (Some v) None) + | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg), + (to_ast_typ k_env def_ord ret), + (to_ast_effects k_env efct)) + | Parse_ast.ATyp_bidir (typ1, typ2) -> Typ_bidir ( (to_ast_typ k_env def_ord typ1), + (to_ast_typ k_env def_ord typ2)) + | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs) + | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_tb",il), [ b; r; ord ; ti]) -> + let make_r bot top = + match bot,top with + | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant b,_),Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,l) -> + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.add (Big_int.sub t b) (Big_int.of_int 1)),l) + | bot,(Parse_ast.ATyp_aux(_,l) as top) -> + Parse_ast.ATyp_aux((Parse_ast.ATyp_sum + ((Parse_ast.ATyp_aux + (Parse_ast.ATyp_sum (top, + Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.of_int 1),Parse_ast.Unknown)), + Parse_ast.Unknown)), + (Parse_ast.ATyp_aux ((Parse_ast.ATyp_neg bot),Parse_ast.Unknown)))), l) in + let base = to_ast_nexp k_env b in + let rise = match def_ord with + | Ord_aux(Ord_inc,dl) -> to_ast_nexp k_env (make_r b r) + | Ord_aux(Ord_dec,dl) -> to_ast_nexp k_env (make_r r b) + | _ -> raise (Reporting_basic.err_unreachable l "Default order not inc or dec") in + Typ_app(Id_aux(Id "vector",il), + [Typ_arg_aux (Typ_arg_nexp base,Parse_ast.Unknown); + Typ_arg_aux (Typ_arg_nexp rise,Parse_ast.Unknown); + Typ_arg_aux (Typ_arg_order def_ord,Parse_ast.Unknown); + Typ_arg_aux (Typ_arg_typ (to_ast_typ k_env def_ord ti), Parse_ast.Unknown);]) + | Parse_ast.ATyp_app(Parse_ast.Id_aux(Parse_ast.Id "vector_sugar_r",il), [b;r;ord;ti]) -> + let make_sub_one t = + match t with | Parse_ast.ATyp_aux(Parse_ast.ATyp_constant t,_) -> Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.sub t (Big_int.of_int 1)),l) - | t -> (Parse_ast.ATyp_aux + | t -> (Parse_ast.ATyp_aux (Parse_ast.ATyp_sum (t, Parse_ast.ATyp_aux(Parse_ast.ATyp_constant (Big_int.negate (Big_int.of_int 1)),Parse_ast.Unknown)), Parse_ast.Unknown)) in let (base,rise) = match def_ord with @@ -227,20 +229,20 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) let id = to_ast_id pid in let k = Envmap.apply k_env (id_to_string id) in (match k with - | Some({k = K_Lam(args,t)}) -> - if ((List.length args) = (List.length typs)) - then - Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env def_ord k a)) args typs)) - else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None - | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None - | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) - | Parse_ast.ATyp_exist (kids, nc, atyp) -> - let kids = List.map to_ast_var kids in - let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in - let exist_typ = to_ast_typ k_env def_ord atyp in - Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) - | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None - ), l) + | Some({k = K_Lam(args,t)}) -> + if ((List.length args) = (List.length typs)) + then + Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env def_ord k a)) args typs)) + else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None + | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None + | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) + | Parse_ast.ATyp_exist (kids, nc, atyp) -> + let kids = List.map to_ast_var kids in + let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in + let exist_typ = to_ast_typ k_env def_ord atyp in + Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) + | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None + ), l) and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = match n with @@ -468,6 +470,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa | Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats) | Parse_ast.P_cons(pat1, pat2) -> P_cons (to_ast_pat k_env def_ord pat1, to_ast_pat k_env def_ord pat2) + | Parse_ast.P_string_append pats -> P_string_append (List.map (to_ast_pat k_env def_ord) pats) ), (l,())) @@ -769,6 +772,44 @@ let to_ast_fundef (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.funde let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,())), (names,k_env,def_ord) +let rec to_ast_mpat k_env def_ord (Parse_ast.MP_aux(mpat,l)) = + MP_aux( + (match mpat with + | Parse_ast.MP_lit(lit) -> MP_lit(to_ast_lit lit) + | Parse_ast.MP_id(id) -> MP_id(to_ast_id id) + | Parse_ast.MP_app(id,mpats) -> + if mpats = [] + then MP_id (to_ast_id id) + else MP_app(to_ast_id id, List.map (to_ast_mpat k_env def_ord) mpats) + | Parse_ast.MP_record(mfpats,_) -> + MP_record(List.map + (fun (Parse_ast.MFP_aux(Parse_ast.MFP_mpat(id,mfp),l)) -> + MFP_aux(MFP_mpat(to_ast_id id, to_ast_mpat k_env def_ord mfp),(l,()))) + mfpats, false) + | Parse_ast.MP_vector(mpats) -> MP_vector(List.map (to_ast_mpat k_env def_ord) mpats) + | Parse_ast.MP_vector_concat(mpats) -> MP_vector_concat(List.map (to_ast_mpat k_env def_ord) mpats) + | Parse_ast.MP_tup(mpats) -> MP_tup(List.map (to_ast_mpat k_env def_ord) mpats) + | Parse_ast.MP_list(mpats) -> MP_list(List.map (to_ast_mpat k_env def_ord) mpats) + | Parse_ast.MP_cons(pat1, pat2) -> MP_cons (to_ast_mpat k_env def_ord pat1, to_ast_mpat k_env def_ord pat2) + | Parse_ast.MP_string_append pats -> MP_string_append (List.map (to_ast_mpat k_env def_ord) pats) + | Parse_ast.MP_typ (mpat, typ) -> MP_typ (to_ast_mpat k_env def_ord mpat, to_ast_typ k_env def_ord typ) + ), (l,())) + + +let to_ast_mpexp (names,k_env,def_ord) (Parse_ast.MPat_aux(mpexp, l)) = + match mpexp with + | Parse_ast.MPat_pat mpat -> MPat_aux (MPat_pat (to_ast_mpat k_env def_ord mpat), (l, ())) + | Parse_ast.MPat_when (mpat, exp) -> MPat_aux (MPat_when (to_ast_mpat k_env def_ord mpat, to_ast_exp k_env def_ord exp), (l, ())) + +let to_ast_mapcl (names,k_env,def_ord) (Parse_ast.MCL_aux(mapcl, l)) = + match mapcl with + | Parse_ast.MCL_mapcl (mpexp1, mpexp2) -> MCL_aux (MCL_mapcl (to_ast_mpexp (names,k_env,def_ord) mpexp1, to_ast_mpexp (names,k_env,def_ord) mpexp2), (l, ())) + +let to_ast_mapdef (names,k_env,def_ord) (Parse_ast.MD_aux(md,l):Parse_ast.mapdef) : (unit mapdef) envs_out = + match md with + | Parse_ast.MD_mapping(id, mapcls) -> + MD_aux(MD_mapping(to_ast_id id, List.map (to_ast_mapcl (names,k_env,def_ord)) mapcls), (l,())), (names,k_env,def_ord) + type def_progress = No_def | Def_place_holder of id * Parse_ast.l @@ -824,96 +865,123 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out | Parse_ast.DEF_fixity (prec, n, op) -> ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs) | Parse_ast.DEF_kind(k_def) -> - let kd,envs = to_ast_kdef envs k_def in - ((Finished(DEF_kind(kd))),envs),partial_defs + let kd,envs = to_ast_kdef envs k_def in + ((Finished(DEF_kind(kd))),envs),partial_defs | Parse_ast.DEF_type(t_def) -> - let td,envs = to_ast_typedef envs t_def in - ((Finished(DEF_type(td))),envs),partial_defs + let td,envs = to_ast_typedef envs t_def in + ((Finished(DEF_type(td))),envs),partial_defs | Parse_ast.DEF_fundef(f_def) -> - let fd,envs = to_ast_fundef envs f_def in - ((Finished(DEF_fundef(fd))),envs),partial_defs + let fd,envs = to_ast_fundef envs f_def in + ((Finished(DEF_fundef(fd))),envs),partial_defs + | Parse_ast.DEF_mapdef(m_def) -> + let md, envs = to_ast_mapdef envs m_def in + ((Finished(DEF_mapdef(md))),envs),partial_defs | Parse_ast.DEF_val(lbind) -> - let lb = to_ast_letbind k_env def_ord lbind in - ((Finished(DEF_val(lb))),envs),partial_defs + let lb = to_ast_letbind k_env def_ord lbind in + ((Finished(DEF_val(lb))),envs),partial_defs | Parse_ast.DEF_spec(val_spec) -> - let vs,envs = to_ast_spec envs val_spec in - ((Finished(DEF_spec(vs))),envs),partial_defs + let vs,envs = to_ast_spec envs val_spec in + ((Finished(DEF_spec(vs))),envs),partial_defs | Parse_ast.DEF_default(typ_spec) -> - let default,envs = to_ast_default envs typ_spec in - ((Finished(DEF_default(default))),envs),partial_defs + let default,envs = to_ast_default envs typ_spec in + ((Finished(DEF_default(default))),envs),partial_defs | Parse_ast.DEF_reg_dec(dec) -> - let d = to_ast_dec envs dec in - ((Finished(DEF_reg_dec(d))),envs),partial_defs + let d = to_ast_dec envs dec in + ((Finished(DEF_reg_dec(d))),envs),partial_defs | Parse_ast.DEF_pragma (_, _, l) -> typ_error l "Encountered preprocessor directive in initial check" None None None | Parse_ast.DEF_internal_mutrec _ -> (* Should never occur because of remove_mutrec *) typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) -> - (match sd with - | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> - let rec_opt = to_ast_rec rec_opt in - let unit,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in - let effects_opt = to_ast_effects_opt k_env' effects_opt in - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,unit,effects_opt,[]),(l,())))),false) in - (No_def,envs),((id,(partial_def,k_local))::partial_defs) - | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.SD_scattered_funcl(funcl) -> - (match funcl with - | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_),_) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered function definition clause does not match any existing function definition headers" (Some id) None None - | Some(d,k) -> - (* let _ = Printf.eprintf "SD_scattered_funcl processing\n" in - let _ = Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s\n" v' (kind_to_string k)) k in - let _ = Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s\n" v' (kind_to_string k) ) (Envmap.union k k_env) in *) - (match !d with - | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> - let (FCL_aux (funcl_aux, _)) = to_ast_funcl (names,Envmap.union k k_env,def_ord) funcl in - d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[FCL_aux (funcl_aux, (l, ()))]),fl)),false; - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered function definition clauses extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) - | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> - let id = to_ast_id id in - let name = to_ast_namescm naming_scheme_opt in - let typq, k_env',_ = to_ast_typquant k_env typquant in - let kind = (match (typquant_to_quantkinds k_env' typq) with - | [ ] -> {k = K_Typ} - | typs -> {k = K_Lam(typs,{k=K_Typ})}) in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,())))),false) in - (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),kind),def_ord)),(id,(partial_def,k_env'))::partial_defs - | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.SD_scattered_unioncl(id,tu) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None - | Some(d,k) -> - (match !d with - | DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> - d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k def_ord tu],false),tl)),false; - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) - | Parse_ast.SD_scattered_end(id) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None - | Some(d,k) -> - (match !d with - | (DEF_type(_) as def),false -> - d:= (def,true); - (No_def,envs),partial_defs - | (DEF_fundef(_) as def),false -> - d:= (def,true); - ((Finished def), envs),partial_defs - | _, true -> - typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) + (match sd with + | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> + let rec_opt = to_ast_rec rec_opt in + let unit,k_env',k_local = to_ast_tannot_opt k_env def_ord tannot_opt in + let effects_opt = to_ast_effects_opt k_env' effects_opt in + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,unit,effects_opt,[]),(l,())))),false) in + (No_def,envs),((id,(partial_def,k_local))::partial_defs) + | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) + | Parse_ast.SD_scattered_mapping id -> + let id = to_ast_id id in + let _,_,k_local = to_ast_tannot_opt k_env def_ord (Parse_ast.Typ_annot_opt_aux (Parse_ast.Typ_annot_opt_none, Parse_ast.Unknown)) in + (match (def_in_progress id partial_defs) with + | None -> let partial_def = ref ((DEF_mapdef(MD_aux(MD_mapping(id, []), (l, ())))), false) in + (No_def,envs),((id,(partial_def,k_local))::partial_defs) + | Some(d,k) -> typ_error l "Scattered mapping definition header name already in use by scattered definition" (Some id) None None) + + | Parse_ast.SD_scattered_mapcl (id, mapcl) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered mapping definition clause does not match any existing mapping definition headers" (Some id) None None + | Some (d, k) -> + (match !d with + | DEF_mapdef(MD_aux(MD_mapping(_,mcls),ml)),false -> + let (MCL_aux (mapcl_aux, _)) = to_ast_mapcl (names,k_env,def_ord) mapcl in + d := DEF_mapdef(MD_aux(MD_mapping(id, mcls @ [MCL_aux (mapcl_aux, (l, ()))]), ml)), false; + (No_def,envs),partial_defs + | _, true -> typ_error l "Scattered mapping definition clause extends ended definition" (Some id) None None + | _ -> typ_error l "Scattered mapping definition doesn't match existing definition header" (Some id) None None)) + + | Parse_ast.SD_scattered_funcl(funcl) -> + (match funcl with + | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_),_) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered function definition clause does not match any existing function definition headers" (Some id) None None + | Some(d,k) -> + (* let _ = Printf.eprintf "SD_scattered_funcl processing\n" in + let _ = Envmap.iter (fun v' k -> P rintf.eprintf "%s -> %s\n" v' (kind_to_string k)) k in + let _ = Envmap.iter (fun v' k -> Prin tf.eprintf "%s -> %s\n" v' (kind_to_string k) ) (Envmap.union k k_env) in *) + (match !d with + | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> + let (FCL_aux (funcl_aux, _)) = to_ast_funcl (names,Envmap.union k k_env,def_ord) funcl in + d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[FCL_aux (funcl_aux, (l, ()))]),fl)),false; + (No_def,envs),partial_defs + | _,true -> typ_error l "Scattered function definition clauses extends ended definition" (Some id) None None + | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) + | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> + let id = to_ast_id id in + let name = to_ast_namescm naming_scheme_opt in + let typq, k_env',_ = to_ast_typquant k_env typquant in + let kind = (match (typquant_to_quantkinds k_env' typq) with + | [ ] -> {k = K_Typ} + | typs -> {k = K_Lam(typs,{k=K_Typ})}) in + (match (def_in_progress id partial_defs) with + | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,())))),false) in + (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),kind),def_ord)),(id,(partial_def,k_env'))::partial_defs + | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) + | Parse_ast.SD_scattered_unioncl(id,tu) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None + | Some(d,k) -> + (match !d with + | DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> + d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k def_ord tu],false),tl)),false; + (No_def,envs),partial_defs + | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None + | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) + | Parse_ast.SD_scattered_end(id) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None + | Some(d,k) -> + (match !d with + | (DEF_type(_) as def),false -> + d:= (def,true); + (No_def,envs),partial_defs + | (DEF_fundef(_) as def),false -> + d:= (def,true); + ((Finished def), envs),partial_defs + | (DEF_mapdef(_) as def),false -> + d := (def,true); + ((Finished def), envs),partial_defs + | _, true -> + typ_error l "Scattered definition ended multiple times" (Some id) None None + | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) let rec to_ast_defs_helper envs partial_defs = function | [] -> ([],envs,partial_defs) diff --git a/src/lexer.mll b/src/lexer.mll index 0b756d84..a4ec4cc9 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -128,6 +128,7 @@ let kw_table = ("forall", (fun _ -> Forall)); ("foreach", (fun _ -> Foreach)); ("function", (fun x -> Function_)); + ("mapping", (fun _ -> Mapping)); ("overload", (fun _ -> Overload)); ("throw", (fun _ -> Throw)); ("try", (fun _ -> Try)); @@ -215,6 +216,8 @@ rule token = parse | "2" ws "^" { TwoCaret } | "^" { (Caret(r"^")) } | "::" { ColonColon(r "::") } + | "^^" { CaretCaret(r "^^") } + | "~~" { TildeTilde(r "~~") } | ":" { Colon(r ":") } | "," { Comma } | ".." { DotDot } @@ -245,6 +248,7 @@ rule token = parse | "!=" { (ExclEq(r"!=")) } | ">=" { (GtEq(r">=")) } | "->" { MinusGt } + | "<->" { Bidir } | "=>" { EqGt(r "=>") } | "<=" { (LtEq(r"<=")) } | "/*!" { Doc (doc_comment (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) 0 lexbuf) } diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 55ed57d2..607285c7 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -151,6 +151,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | ATyp_set of (base_effect) list (* effect set *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_bidir of atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) | ATyp_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) @@ -251,6 +252,7 @@ pat_aux = (* Pattern *) | P_tup of (pat) list (* tuple pattern *) | P_list of (pat) list (* list pattern *) | P_cons of pat * pat (* cons pattern *) + | P_string_append of pat list (* string append pattern, x ^^ y *) and pat = P_aux of pat_aux * l @@ -363,6 +365,7 @@ funcl_aux = (* Function clause *) type type_union_aux = (* Type union constructors *) Tu_ty_id of atyp * id + | Tu_ty_anon_rec of (atyp * id) list * id type @@ -390,7 +393,6 @@ type funcl = FCL_aux of funcl_aux * l - type type_union = Tu_aux of type_union_aux * l @@ -418,6 +420,48 @@ default_typing_spec_aux = (* Default kinding or typing assumption, and default | DT_typ of typschm * id +type mpat_aux = (* Mapping pattern. Mostly the same as normal patterns but only constructible parts *) + | MP_lit of lit + | MP_id of id + | MP_app of id * ( mpat) list + | MP_record of ( mfpat) list * bool + | MP_vector of ( mpat) list + | MP_vector_concat of ( mpat) list + | MP_tup of ( mpat) list + | MP_list of ( mpat) list + | MP_cons of ( mpat) * ( mpat) + | MP_string_append of mpat list + | MP_typ of mpat * atyp + +and mpat = + | MP_aux of ( mpat_aux) * l + +and mfpat_aux = (* Mapping field pattern, why does this have to exist *) + | MFP_mpat of id * mpat + +and mfpat = + | MFP_aux of mfpat_aux * l + +type mpexp_aux = + | MPat_pat of ( mpat) + | MPat_when of ( mpat) * ( exp) + +type mpexp = + | MPat_aux of ( mpexp_aux) * l + +type mapcl_aux = (* mapping clause (bidirectional pattern-match) *) + | MCL_mapcl of ( mpexp) * ( mpexp) + +type mapcl = + | MCL_aux of ( mapcl_aux) * l + +type mapdef_aux = (* mapping definition (bidirectional pattern-match function) *) + | MD_mapping of id * ( mapcl) list + +type mapdef = + | MD_aux of ( mapdef_aux) * l + + type fundef_aux = (* Function definition *) FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list @@ -454,6 +498,8 @@ scattered_def_aux = (* Function and type union definitions that can be spread a | SD_scattered_funcl of funcl (* scattered function definition clause *) | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_mapping of id + | SD_scattered_mapcl of id * mapcl | SD_scattered_end of id (* scattered definition end *) @@ -500,6 +546,7 @@ def = (* Top-level definition *) DEF_kind of kind_def (* definition of named kind identifiers *) | DEF_type of type_def (* type definition *) | DEF_fundef of fundef (* function definition *) + | DEF_mapdef of mapdef (* mapping definition *) | DEF_val of letbind (* value definition *) | DEF_overload of id * id list (* operator overload specifications *) | DEF_fixity of prec * Big_int.num * id (* fixity declaration *) diff --git a/src/parser.mly b/src/parser.mly index 3b7a435b..a46defd6 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -105,6 +105,11 @@ let mk_vs v n m = VS_aux (v, loc n m) let mk_reg_dec d n m = DEC_aux (d, loc n m) let mk_default d n m = DT_aux (d, loc n m) +let mk_mpexp mpexp n m = MPat_aux (mpexp, loc n m) +let mk_mpat mpat n m = MP_aux (mpat, loc n m) +let mk_mapcl mpexp1 mpexp2 n m = MCL_aux (MCL_mapcl (mpexp1, mpexp2), loc n m) +let mk_map id mapcls n m = MD_aux (MD_mapping (id, mapcls), loc n m) + let doc_vs doc (VS_aux (v, l)) = VS_aux (v, Documented (doc, l)) let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) @@ -159,7 +164,7 @@ let rec desugar_rchain chain s e = /*Terminals with no content*/ %token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op -%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast +%token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ Int Order Cast %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape @@ -170,7 +175,7 @@ let rec desugar_rchain chain s e = %token Bar Comma Dot Eof Minus Semi Under DotDot %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar LsquareBar RsquareBar -%token MinusGt +%token MinusGt Bidir /*Terminals with content*/ @@ -179,7 +184,7 @@ let rec desugar_rchain chain s e = %token <string> String Bin Hex Real %token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit -%token <string> Colon ColonColon ExclEq +%token <string> Colon ColonColon CaretCaret TildeTilde ExclEq %token <string> GtEq %token <string> LtEq @@ -641,11 +646,21 @@ typschm: { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, $5)) s e) s e) $startpos $endpos } | Forall typquant Dot typ MinusGt typ Effect effect_set { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos } + | typ Bidir typ + { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_bidir ($1, $3)) s e) s e) $startpos $endpos } + | Forall typquant Dot typ Bidir typ + { (fun s e -> mk_typschm $2 (mk_typ (ATyp_bidir ($4, $6)) s e) s e) $startpos $endpos } typschm_eof: | typschm Eof { $1 } +pat_string_append: + | atomic_pat + { [$1] } + | atomic_pat CaretCaret pat_string_append + { $1 :: $3 } + pat1: | atomic_pat { $1 } @@ -653,6 +668,8 @@ pat1: { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos } | atomic_pat ColonColon pat1 { mk_pat (P_cons ($1, $3)) $startpos $endpos } + | atomic_pat CaretCaret pat_string_append + { mk_pat (P_string_append ($1 :: $3)) $startpos $endpos } pat_concat: | atomic_pat @@ -1048,6 +1065,8 @@ atomic_exp: fexp_exp: | atomic_exp Eq exp { mk_exp (E_app_infix ($1, mk_id (Id "=") $startpos($2) $endpos($2), $3)) $startpos $endpos } + | TildeTilde id + { mk_exp (E_app_infix (mk_exp (E_id $2) $startpos($2) $endpos($2), mk_id (Id "=") $startpos $endpos, mk_exp (E_id $2) $startpos($2) $endpos($2))) $startpos $endpos } fexp_exp_list: | fexp_exp @@ -1170,6 +1189,8 @@ type_union: { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) } | id Colon typ MinusGt typ { (fun s e -> Tu_aux (Tu_ty_id (mk_typ (ATyp_fn ($3, $5, mk_typ (ATyp_set []) s e)) s e, $1), loc s e)) $startpos $endpos } + | id Colon Lcurly struct_fields Rcurly + { Tu_aux (Tu_ty_anon_rec ($4, $1), loc $startpos $endpos) } type_unions: | type_union @@ -1189,6 +1210,80 @@ fun_def_list: | fun_def fun_def_list { $1 :: $2 } +mpat_string_append: + | atomic_mpat + { [$1] } + | atomic_mpat CaretCaret mpat_string_append + { $1 :: $3 } + +mpat: + | atomic_mpat + { $1 } + | atomic_mpat At mpat_concat + { mk_mpat (MP_vector_concat ($1 :: $3)) $startpos $endpos } + | atomic_mpat ColonColon mpat + { mk_mpat (MP_cons ($1, $3)) $startpos $endpos } + | atomic_mpat CaretCaret mpat_string_append + { mk_mpat (MP_string_append ($1 :: $3)) $startpos $endpos } + +mpat_concat: + | atomic_mpat + { [$1] } + | atomic_mpat At mpat_concat + { $1 :: $3 } + +mpat_list: + | mpat + { [$1] } + | mpat Comma mpat_list + { $1 :: $3 } + +atomic_mpat: + | lit + { mk_mpat (MP_lit $1) $startpos $endpos } + | id + { mk_mpat (MP_id $1) $startpos $endpos } + | id Unit + { mk_mpat (MP_app ($1, [mk_mpat (MP_lit (mk_lit L_unit $startpos($2) $endpos($2))) $startpos($2) $endpos($2)])) $startpos $endpos } + | id Lparen mpat_list Rparen + { mk_mpat (MP_app ($1, $3)) $startpos $endpos } + | Lparen mpat Rparen + { $2 } + | Lparen mpat Comma mpat_list Rparen + { mk_mpat (MP_tup ($2 :: $4)) $startpos $endpos } + | Lsquare mpat_list Rsquare + { mk_mpat (MP_vector $2) $startpos $endpos } + | LsquareBar RsquareBar + { mk_mpat (MP_list []) $startpos $endpos } + | LsquareBar mpat_list RsquareBar + { mk_mpat (MP_list $2) $startpos $endpos } + | atomic_mpat Colon typ + { mk_mpat (MP_typ ($1, $3)) $startpos $endpos } + + + +mpexp: + | mpat + { mk_mpexp (MPat_pat $1) $startpos $endpos } + | mpat If_ exp + { mk_mpexp (MPat_when ($1, $3)) $startpos $endpos } + +mapcl: + | mpexp Bidir mpexp + { mk_mapcl $1 $3 $startpos $endpos } + +mapcl_list: + | mapcl + { [$1] } + | mapcl Comma mapcl_list + { $1 :: $3 } + +map_def: + | Mapping id Eq Lcurly mapcl_list Rcurly + { mk_map $2 $5 $startpos $endpos } + (* | Mapping id Colon typschm Eq Lcurly mapcl_list Rcurly + * { mk_map $2 $4 $7 $startpos $endpos } *) + let_def: | Let_ letbind { $2 } @@ -1238,6 +1333,8 @@ scattered_def: { mk_sd (SD_scattered_variant($2, mk_namesectn, mk_typqn)) $startpos $endpos } | Function_ id { mk_sd (SD_scattered_function(mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos } + | Mapping id + { mk_sd (SD_scattered_mapping $2) $startpos $endpos } scattered_clause: | Doc Function_ Clause funcl @@ -1245,9 +1342,12 @@ scattered_clause: | Function_ Clause funcl { mk_sd (SD_scattered_funcl $3) $startpos $endpos } + def: | fun_def { DEF_fundef $1 } + | map_def + { DEF_mapdef $1 } | Fixity { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) } | val_spec_def @@ -1268,6 +1368,8 @@ def: { DEF_scattered $1 } | Union Clause id Eq type_union { DEF_scattered (mk_sd (SD_scattered_unioncl ($3, $5)) $startpos $endpos) } + | Mapping Clause id Eq mapcl + { DEF_scattered (mk_sd (SD_scattered_mapcl ($3, $5)) $startpos $endpos) } | End id { DEF_scattered (mk_sd (SD_scattered_end $2) $startpos $endpos) } | default_def diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index c13452ff..2372ea82 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -68,6 +68,7 @@ type gpat = | GP_cons of gpat * gpat | GP_app of (gpat Bindings.t) | GP_record of (gpat Bindings.t) + | GP_string_append of gpat list let rec string_of_gpat = function | GP_lit lit -> string_of_lit lit @@ -80,12 +81,14 @@ let rec string_of_gpat = function | GP_app app -> Util.string_of_list "|" (fun (id, gpat) -> string_of_id id ^ string_of_gpat gpat) (Bindings.bindings app) | GP_record _ -> "GP RECORD" + | GP_string_append gpats -> Util.string_of_list " ^^ " string_of_gpat gpats let is_wild = function | GP_wild -> true | _ -> false let rec generalize ctx (P_aux (p_aux, _) as pat) = + match p_aux with | P_lit lit -> GP_lit lit | P_wild -> GP_wild @@ -116,6 +119,9 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) = let ghd_pat = generalize ctx hd_pat in let gtl_pat = generalize ctx tl_pat in if is_wild ghd_pat && is_wild gtl_pat then GP_wild else GP_cons (ghd_pat, gtl_pat) + | P_string_append pats -> + let gpats = List.map (generalize ctx) pats in + if List.for_all is_wild gpats then GP_wild else GP_string_append gpats | P_app (f, pats) -> let gpats = List.map (generalize ctx) pats in if List.for_all is_wild gpats then diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 5a26cb42..6ea669f9 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -159,6 +159,8 @@ let rec doc_typ (Typ_aux (typ_aux, _)) = | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) -> let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff] + | Typ_bidir (typ1, typ2) -> + separate space [doc_typ typ1; string "<->"; doc_typ typ2] and doc_typ_arg (Typ_arg_aux (ta_aux, _)) = match ta_aux with | Typ_arg_typ typ -> doc_typ typ @@ -452,6 +454,36 @@ let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) = let clauses = separate_map sep doc_funcl funcls in string "function" ^^ space ^^ clauses +let rec doc_mpat (MP_aux (mp_aux, _) as mpat) = + match mp_aux with + | MP_id id -> doc_id id + | MP_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_mpat pats ^^ rparen + | MP_lit lit -> doc_lit lit + | MP_vector pats -> brackets (separate_map (comma ^^ space) doc_mpat pats) + | MP_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_mpat pats + | MP_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_mpat pats) + | MP_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_mpat pats ^^ string "|]" + | _ -> string (string_of_mpat mpat) + + +let doc_mpexp (MPat_aux (mpexp, _)) = + match mpexp with + | MPat_pat mpat -> doc_mpat mpat + | MPat_when (mpat, guard) -> doc_mpat mpat ^^ space ^^ string "if" ^^ space ^^ doc_exp guard + +let doc_mapcl (MCL_aux (MCL_mapcl (mpexp1, mpexp2), _)) = + let left = doc_mpexp mpexp1 in + let right = doc_mpexp mpexp2 in + left ^^ space ^^ string "<->" ^^ space ^^ right + +let doc_mapdef (MD_aux (MD_mapping (id, mapcls), _)) = + match mapcls with + | [] -> failwith "Empty mapping" + | _ -> + let sep = string "," ^^ hardline in + let clauses = separate_map sep doc_mapcl mapcls in + string "mapping" ^^ space ^^ doc_id id ^^ space ^^ string "=" ^^ (surround 2 0 lbrace clauses rbrace) + let doc_dec (DEC_aux (reg,_)) = match reg with | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ] @@ -528,6 +560,7 @@ let rec doc_def def = group (match def with | DEF_type t_def -> doc_typdef t_def | DEF_kind k_def -> doc_kind_def k_def | DEF_fundef f_def -> doc_fundef f_def + | DEF_mapdef m_def -> doc_mapdef m_def | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind | DEF_internal_mutrec fundefs -> (string "mutual {" ^//^ separate_map (hardline ^^ hardline) doc_fundef fundefs) diff --git a/src/process_file.ml b/src/process_file.ml index 4856c20a..1bf8eee9 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -113,6 +113,28 @@ let cond_pragma defs = in scan defs +let astid_to_string (Ast.Id_aux (id, _)) = + match id with + | Ast.Id x | Ast.DeIid x -> x + +let parseid_to_string (Parse_ast.Id_aux (id, _)) = + match id with + | Parse_ast.Id x | Parse_ast.DeIid x -> x + +let rec realise_union_anon_rec_types (Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) as orig_union) arms = + match arms with + | [] -> [] + | arm :: arms -> + match arm with + | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms + | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) -> + let open Parse_ast in + let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in + let record_id = Id_aux (Id record_str, Generated l) in + let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in + let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in + (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms) + let rec preprocess = function | [] -> [] | Parse_ast.DEF_pragma ("define", symbol, _) :: defs -> @@ -168,6 +190,20 @@ let rec preprocess = function | Parse_ast.DEF_pragma (p, arg, _) :: defs -> (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess defs) + (* realise any anonymous record arms of variants *) + | Parse_ast.DEF_type (Parse_ast.TD_aux + (Parse_ast.TD_variant (id, name_scm_opt, typq, arms, flag) as union, l) + ) :: defs -> + let records_and_arms = realise_union_anon_rec_types union arms in + let rec filter_records = function [] -> [] + | Some x :: xs -> x :: filter_records xs + | None :: xs -> filter_records xs + in + let generated_records = filter_records (List.map fst records_and_arms) in + let rewritten_arms = List.map snd records_and_arms in + let rewritten_union = Parse_ast.TD_variant (id, name_scm_opt, typq, rewritten_arms, flag) in + generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess defs + | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs -> begin match atyp with | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess defs diff --git a/src/rewriter.ml b/src/rewriter.ml index 7d10e570..6212e0da 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -306,6 +306,7 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot)) as orig_pat) = | P_tup pats -> rewrap (P_tup (List.map rewrite pats)) | P_list pats -> rewrap (P_list (List.map rewrite pats)) | P_cons (pat1, pat2) -> rewrap (P_cons (rewrite pat1, rewrite pat2)) + | P_string_append pats -> rewrap (P_string_append (List.map rewrite pats)) let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) = let rewrap e = E_aux (e,(l,annot)) in @@ -395,7 +396,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with - | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d + | DEF_type _ | DEF_mapdef _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef) | DEF_internal_mutrec fdefs -> DEF_internal_mutrec (List.map (rewriters.rewrite_fun rewriters) fdefs) | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) @@ -455,6 +456,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux + ; p_string_append : 'pat list -> 'pat_aux ; p_aux : 'pat_aux * 'a annot -> 'pat ; fP_aux : 'fpat_aux * 'a annot -> 'fpat ; fP_Fpat : id * 'pat -> 'fpat_aux @@ -475,6 +477,7 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat | P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps) | P_list ps -> alg.p_list (List.map (fold_pat alg) ps) | P_cons (ph,pt) -> alg.p_cons (fold_pat alg ph, fold_pat alg pt) + | P_string_append ps -> alg.p_string_append (List.map (fold_pat alg) ps) and fold_pat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat -> 'pat = function @@ -501,6 +504,7 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg = ; p_tup = (fun ps -> P_tup ps) ; p_list = (fun ps -> P_list ps) ; p_cons = (fun (ph,pt) -> P_cons (ph,pt)) + ; p_string_append = (fun (ps) -> P_string_append (ps)) ; p_aux = (fun (pat,annot) -> P_aux (pat,annot)) ; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot)) ; fP_Fpat = (fun (id,pat) -> FP_Fpat (id,pat)) @@ -750,6 +754,7 @@ let compute_pat_alg bot join = ; p_tup = split_join (fun ps -> P_tup ps) ; p_list = split_join (fun ps -> P_list ps) ; p_cons = (fun ((vh,ph),(vt,pt)) -> (join vh vt, P_cons (ph,pt))) + ; p_string_append = split_join (fun ps -> P_string_append ps) ; p_aux = (fun ((v,pat),annot) -> (v, P_aux (pat,annot))) ; fP_aux = (fun ((v,fpat),annot) -> (v, FP_aux (fpat,annot))) ; fP_Fpat = (fun (id,(v,pat)) -> (v, FP_Fpat (id,pat))) @@ -855,6 +860,7 @@ let pure_pat_alg bot join = ; p_vector_concat = join_list ; p_tup = join_list ; p_list = join_list + ; p_string_append = join_list ; p_cons = (fun (vh,vt) -> join vh vt) ; p_aux = (fun (v,annot) -> v) ; fP_aux = (fun (v,annot) -> v) diff --git a/src/rewriter.mli b/src/rewriter.mli index 6e9f08c2..edc93e5d 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -95,6 +95,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg = ; p_tup : 'pat list -> 'pat_aux ; p_list : 'pat list -> 'pat_aux ; p_cons : 'pat * 'pat -> 'pat_aux + ; p_string_append : 'pat list -> 'pat_aux ; p_aux : 'pat_aux * 'a annot -> 'pat ; fP_aux : 'fpat_aux * 'a annot -> 'fpat ; fP_Fpat : id * 'pat -> 'fpat_aux diff --git a/src/rewrites.ml b/src/rewrites.ml index b59a248e..e41318dd 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -690,6 +690,7 @@ let remove_vector_concat_pat pat = ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) + ; p_string_append = (fun (ps) -> P_string_append (List.map (fun p -> p false) ps)) ; p_aux = (fun (pat,((l,_) as annot)) contained_in_p_as -> match pat with @@ -714,6 +715,7 @@ let remove_vector_concat_pat pat = | P_as (p,id) -> P_aux (P_as (p,id),a) | P_typ (typ, pat) -> P_aux (P_typ (typ, aux pat),a) | P_wild -> P_aux (P_wild,a) + | P_app (id, pats) when Env.is_mapping id (env_of_annot a) -> P_aux (P_app (id, List.map aux pats), a) | _ -> raise (Reporting_basic.err_unreachable @@ -804,6 +806,9 @@ let remove_vector_concat_pat pat = let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in (pos', pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)]) | P_typ (typ, pat) -> aux (Some typ) (pos,pat_acc,decl_acc) (pat, is_last) + (* | P_app (cname, pats) if Env.is_mapping cname (en) -> + * let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in + * (pos', pat_acc @ [P_aux (P_app (cname,pats),cannot)], decl_acc @ [((lb,decl),info)]) *) (* normal vector patterns are fine *) | _ -> (pos', pat_acc @ [P_aux (p,cannot)],decl_acc)) in let pats_tagged = tag_last pats in @@ -832,6 +837,8 @@ let remove_vector_concat_pat pat = (P_tup ps,List.flatten decls)) ; p_list = (fun ps -> let (ps,decls) = List.split ps in (P_list ps,List.flatten decls)) + ; p_string_append = (fun ps -> let (ps,decls) = List.split ps in + (P_string_append ps,List.flatten decls)) ; p_cons = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls')) ; p_aux = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot)) ; fP_aux = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls)) @@ -1086,6 +1093,8 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) = | P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats)) | P_list pats -> rewrap (E_list (List.map pat_to_exp pats)) | P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps)) + | P_string_append (ps) -> raise (Reporting_basic.err_unreachable l + "pat_to_exp not implemented for P_string_append") and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) = FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot)) @@ -1174,6 +1183,7 @@ let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with | P_app (_,pats) | P_tup pats | P_list pats -> List.exists contains_bitvector_pat pats | P_cons (p,ps) -> contains_bitvector_pat p || contains_bitvector_pat ps +| P_string_append (ps) -> List.exists contains_bitvector_pat ps | P_record (fpats,_) -> List.exists (fun (FP_aux (FP_Fpat (_,pat),_)) -> contains_bitvector_pat pat) fpats @@ -1199,6 +1209,7 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = ; p_record = (fun (fpats,b) -> P_record (fpats, b)) ; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps)) ; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps)) + ; p_string_append = (fun ps -> P_string_append (List.map (fun p -> p false) ps)) ; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps)) ; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps)) ; p_cons = (fun (p,ps) -> P_cons (p false, ps false)) @@ -1350,6 +1361,8 @@ let remove_bitvector_pat (P_aux (_, (l, _)) as pat) = (P_vector ps, flatten_guards_decls gdls)) ; p_vector_concat = (fun ps -> let (ps,gdls) = List.split ps in (P_vector_concat ps, flatten_guards_decls gdls)) + ; p_string_append = (fun ps -> let (ps,gdls) = List.split ps in + (P_string_append ps, flatten_guards_decls gdls)) ; p_tup = (fun ps -> let (ps,gdls) = List.split ps in (P_tup ps, flatten_guards_decls gdls)) ; p_list = (fun ps -> let (ps,gdls) = List.split ps in @@ -1488,7 +1501,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) = | Pat_aux (Pat_exp (pat, body), annot) -> (pat, None, rewrite_rec body, annot) | Pat_aux (Pat_when (pat, guard, body), annot) -> - (pat, Some guard, rewrite_rec body, annot) in + (pat, Some (rewrite_rec guard), rewrite_rec body, annot) in let clauses = rewrite_guarded_clauses l (List.map clause ps) in if (effectful e) then let e = rewrite_rec e in @@ -2803,6 +2816,393 @@ let rewrite_defs_internal_lets = ; rewrite_defs = rewrite_defs_base } + +let fold_guards guards = + match guards with + | [] -> (mk_exp (E_lit (mk_lit L_true))) + | g :: gs -> List.fold_left (fun g g' -> mk_exp (E_app (mk_id "and_bool", [strip_exp g; strip_exp g']))) g gs + +let fold_typed_guards env guards = + match guards with + | [] -> annot_exp (E_lit (mk_lit L_true)) Parse_ast.Unknown env bool_typ + | g :: gs -> List.fold_left (fun g g' -> annot_exp (E_app (mk_id "and_bool", [g; g'])) Parse_ast.Unknown env bool_typ) g gs + + +let rewrite_pexp_with_guards rewrite_pat (Pat_aux (pexp_aux, (annot: tannot annot)) as pexp) = + let guards = ref [] in + + match pexp_aux with + | Pat_exp (pat, exp) -> + begin + let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in + match !guards with + | [] -> pexp + | gs -> + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp gs |> fold_guards, strip_exp exp)) in + check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp) + end + | Pat_when (pat, guard, exp) -> + begin + let pat = fold_pat { id_pat_alg with p_aux = rewrite_pat guards } pat in + let unchecked_pexp = mk_pexp (Pat_when (strip_pat pat, List.map strip_exp !guards |> fold_guards, strip_exp exp)) in + check_case (pat_env_of pat) (pat_typ_of pat) unchecked_pexp (typ_of exp) + end + + +let pexp_rewriters rewrite_pexp = + let alg = { id_exp_alg with pat_aux = (fun (pexp_aux, annot) -> rewrite_pexp (Pat_aux (pexp_aux, annot))) } in + rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } + + +let stringappend_counter = ref 0 + +let fresh_stringappend_id () = + let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in + stringappend_counter := !stringappend_counter + 1; + id + +let construct_bool_match match_on pexp = + let true_exp = (mk_exp (E_lit (mk_lit L_true))) in + let false_exp = (mk_exp (E_lit (mk_lit L_false))) in + let true_pexp = + match pexp with + | Pat_aux (Pat_exp (pat, exp), _) -> + mk_pexp (Pat_exp (pat, true_exp)) + | Pat_aux (Pat_when (pat, guards, exp), _) -> + mk_pexp (Pat_when (pat, guards, true_exp)) + in + let false_pexp = mk_pexp (Pat_exp (mk_pat P_wild, false_exp)) in + mk_exp (E_case (match_on, [true_pexp; false_pexp])) + + +let rec rewrite_defs_pat_string_append = + let rec rewrite_pat env (pat, guards, expr) = + let guards_ref = ref guards in + let expr_ref = ref expr in + let folder p = + let p, g, e = rewrite_pat env (p, !guards_ref, !expr_ref) in + guards_ref := g; + expr_ref := e; + p + in + match pat with + (* + "lit" ^^ pat2 => expr ---> s# if startswith(s#, "lit") + && match str_drop(s#, strlen("lit")) { + pat2 => true, _ => false + } + => match str_drop(s#, strlen("lit")) { + pat2 => expr + } + *) + | P_aux (P_string_append ( + P_aux (P_lit (L_aux (L_string s, _) as lit), _) + :: pats + ), psa_annot) -> + + let id = mk_id ("_stringappend_" ^ (string_of_int !stringappend_counter) ^ "#") in + stringappend_counter := !stringappend_counter + 1; + + (* construct drop expression -- string_drop(s#, strlen("lit")) *) + let drop_exp = mk_exp (E_app (mk_id "string_drop", [mk_exp (E_id id); mk_exp (E_app (mk_id "string_length", [mk_exp (E_lit lit)]))])) in + + (* recurse into pat2 *) + let new_pat2_pexp = + match rewrite_pat env (P_aux (P_string_append (pats), psa_annot), guards, expr) with + | pat, [], expr -> mk_pexp (Pat_exp (pat, expr)) + | pat, gs, expr -> mk_pexp (Pat_when (pat, fold_guards gs, expr)) + in + + (* construct the two new guards *) + let guard1 = mk_exp (E_app (mk_id "string_startswith", [mk_exp (E_id id); mk_exp (E_lit lit)])) in + let guard2 = construct_bool_match drop_exp new_pat2_pexp in + + (* construct new match expr *) + let new_expr = mk_exp (E_case (drop_exp, [new_pat2_pexp])) in + + (* construct final result *) + mk_pat (P_id id), guard1 :: guard2 :: guards, new_expr + + (* + (builtin x) ^^ pat2 => expr ---> s# if match maybe_atoi s# { + Some (n#, len#) => + match string_drop(s#, len#) { + pat2 => true, _ => false + } + None => false + } + => let (x, len#) = match maybe_int_of_prefix s# { + Some (n#, len#) => (n#, len#) + } in + match string_drop(s#, len#) { + pat2 => expr + } + *) + + | P_aux (P_string_append ( + P_aux (P_app (mapping_id, arg_pats) , _) + :: pats + ), psa_annot) + when Env.is_mapping mapping_id env -> + + (* common things *) + let mapping_prefix_func = + match mapping_id with + | Id_aux (Id id, _) + | Id_aux (DeIid id, _) -> id ^ "_matches_prefix" + in + let mapping_inner_typ = + match Env.get_val_spec (mk_id mapping_prefix_func) env with + | (_, Typ_aux (Typ_fn (_, Typ_aux (Typ_app (_, [Typ_arg_aux (Typ_arg_typ typ, _)]), _), _), _)) -> typ + | _ -> typ_error Parse_ast.Unknown "mapping prefix func without correct function type?" + in + + let s_id = fresh_stringappend_id () in + let n_id = fresh_stringappend_id () in + let len_id = fresh_stringappend_id () in + + (* construct drop expression -- string_drop(s#, len#) *) + let drop_exp = mk_exp (E_app (mk_id "string_drop", [mk_exp (E_id s_id); mk_exp (E_id len_id)])) in + (* construct func expression -- maybe_atoi s# *) + let func_exp = mk_exp (E_app (mk_id mapping_prefix_func, [mk_exp (E_id s_id)])) in + (* construct some pattern -- Some (n#, len#) *) + let some_exp = mk_pat (P_app (mk_id "Some", [mk_pat (P_id n_id); mk_pat (P_id len_id)])) in + (* construct None pattern *) + let none_exp = mk_pat (P_app (mk_id "None", [mk_pat (P_lit (mk_lit L_unit))])) in + + (* recurse into pat2 *) + let new_pat2_pexp = + match rewrite_pat env (P_aux (P_string_append (pats), psa_annot), guards, expr) with + | pat, [], expr -> mk_pexp (Pat_exp (pat, expr)) + | pat, gs, expr -> mk_pexp (Pat_when (pat, fold_guards gs, expr)) + in + + (* construct the new guard *) + let guard_inner_match = construct_bool_match drop_exp new_pat2_pexp in + let new_guard = mk_exp (E_case (func_exp, [ + mk_pexp (Pat_exp (some_exp, guard_inner_match)); + mk_pexp (Pat_exp (none_exp, mk_exp (E_lit (mk_lit (L_false))))) + ])) in + + (* construct the new match *) + let new_match = mk_exp (E_case (drop_exp, [new_pat2_pexp])) in + + (* construct the new let *) + let new_binding = mk_exp (E_cast (mapping_inner_typ, mk_exp (E_case (func_exp, [ + mk_pexp (Pat_exp (some_exp, mk_exp (E_tuple [ + mk_exp (E_id n_id); + mk_exp (E_id len_id) + ]))) + ])))) in + let new_letbind = + match arg_pats with + | [] -> assert false + | [arg_pat] -> mk_letbind (mk_pat (P_tup [arg_pat; mk_pat (P_id len_id)])) new_binding + | arg_pats -> mk_letbind (mk_pat (P_tup [mk_pat (P_tup arg_pats); mk_pat (P_id len_id)])) new_binding + in + let new_let = mk_exp (E_let (new_letbind, new_match)) in + + (* construct final result *) + mk_pat (P_id s_id), new_guard :: guards, new_let + + | P_aux (P_string_append [pat], _) -> + pat, guards, expr + + | P_aux (P_string_append [], _) -> + mk_pat (P_lit (mk_lit (L_string ""))), guards, expr + + | P_aux (P_string_append _, _) -> + failwith ("encountered a variety of string append pattern that is not yet implemented: " ^ string_of_pat pat) + + | P_aux (P_as (inner_pat, inner_id), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_as (inner_pat, inner_id), p_annot), guards, expr + | P_aux (P_typ (inner_typ, inner_pat), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_typ (inner_typ, inner_pat), p_annot), guards, expr + | P_aux (P_var (inner_pat, typ_pat), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr + | P_aux (P_record _, p_annot) -> + failwith "record patterns not yet implemented" + | P_aux (P_vector pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_vector_concat pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_vector_concat pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_tup pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_tup pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_list pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_list pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_app (f, pats), p_annot) -> + let pats = List.map folder pats in + P_aux (P_app (f, pats), p_annot), !guards_ref, !expr_ref + | P_aux (P_cons (pat1, pat2), p_annot) -> + let pat1, guards, expr = rewrite_pat env (pat1, guards, expr) in + let pat2, guards, expr = rewrite_pat env (pat2, guards, expr) in + P_aux (P_cons (pat1, pat2), p_annot), guards, expr + | P_aux (P_id _, _) + | P_aux (P_lit _, _) + | P_aux (P_wild, _) -> pat, guards, expr + in + + let rec rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = + + let (pat, _, _, _) = destruct_pexp pexp in + + (* merge cases of Pat_exp and Pat_when *) + let (P_aux (p_aux, p_annot), guards, expr) = + match pexp_aux with + | Pat_exp (pat, expr) -> (pat, [], expr) + | Pat_when (pat, guard, expr) -> (pat, [guard], expr) + in + + let (new_pat, new_guards, new_expr) = + rewrite_pat (env_of_annot p_annot) (strip_pat pat, List.map strip_exp guards, strip_exp expr) + in + + (* un-merge Pat_exp and Pat_when cases *) + let new_pexp = match new_guards with + | [] -> mk_pexp (Pat_exp (new_pat, new_expr)) + | gs -> mk_pexp (Pat_when (new_pat, fold_guards gs, new_expr)) + in + check_case (pat_env_of pat) (pat_typ_of pat) new_pexp (typ_of expr) + + in + pexp_rewriters rewrite_pexp + + +let mappingpatterns_counter = ref 0 + +let fresh_mappingpatterns_id () = + let id = mk_id ("_mappingpatterns_" ^ (string_of_int !mappingpatterns_counter) ^ "#") in + mappingpatterns_counter := !mappingpatterns_counter + 1; + id + +let rewrite_defs_mapping_patterns = + let rec rewrite_pat env (pat, guards, expr) = + let guards_ref = ref guards in + let expr_ref = ref expr in + let folder p = + let p, g, e = rewrite_pat env (p, !guards_ref, !expr_ref) in + guards_ref := g; + expr_ref := e; + p + in + let env = pat_env_of pat in + match pat with + (* + mapping(args) => expr ----> s# if mapping_matches(s#) => let args = mapping(s#) in expr + + (plus 'infer the mapping type' shenanigans) + *) + | P_aux (P_app (mapping_id, arg_pats), p_annot) when Env.is_mapping mapping_id env -> + + let mapping_in_typ = typ_of_annot p_annot in + + let x = Env.get_val_spec mapping_id env in + let (_, Typ_aux(Typ_bidir(typ1, typ2), _)) = x in + + let mapping_direction = + if mapping_in_typ = typ1 then + "forwards" + else + "backwards" + in + + let mapping_name = + match mapping_id with + | Id_aux (Id id, _) + | Id_aux (DeIid id, _) -> id + in + + let mapping_matches_id = mk_id (mapping_name ^ "_" ^ mapping_direction ^ "_matches") in + let mapping_perform_id = mk_id (mapping_name ^ "_" ^ mapping_direction) in + let s_id = fresh_mappingpatterns_id () in + + let s_exp = annot_exp (E_id s_id) Parse_ast.Unknown env mapping_in_typ in + let new_guard = annot_exp (E_app (mapping_matches_id, [s_exp])) Parse_ast.Unknown env bool_typ in + let new_binding = annot_exp (E_app (mapping_perform_id, [s_exp])) Parse_ast.Unknown env typ2 in + let new_letbind = match arg_pats with + | [] -> assert false + | [arg_pat] -> LB_aux (LB_val (arg_pat, new_binding), (Parse_ast.Unknown, None)) + | arg_pats -> + let (checked_tup, new_env, []) = infer_pat env (mk_pat (P_tup (List.map strip_pat arg_pats))) in + LB_aux (LB_val (checked_tup, new_binding), (Parse_ast.Unknown, None)) + in + + let new_let = annot_exp (E_let (new_letbind, expr)) Parse_ast.Unknown env (typ_of expr) in + + annot_pat (P_id s_id) Parse_ast.Unknown env mapping_in_typ, new_guard :: guards, new_let + + | P_aux (P_as (inner_pat, inner_id), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_as (inner_pat, inner_id), p_annot), guards, expr + | P_aux (P_typ (inner_typ, inner_pat), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_typ (inner_typ, inner_pat), p_annot), guards, expr + | P_aux (P_var (inner_pat, typ_pat), p_annot) -> + let inner_pat, guards, expr = rewrite_pat env (inner_pat, guards, expr) in + P_aux (P_var (inner_pat, typ_pat), p_annot), guards, expr + | P_aux (P_record _, p_annot) -> + failwith "record patterns not yet implemented" + | P_aux (P_vector pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_vector pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_vector_concat pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_vector_concat pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_tup pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_tup pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_list pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_list pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_app (f, pats), p_annot) -> + let pats = List.map folder pats in + P_aux (P_app (f, pats), p_annot), !guards_ref, !expr_ref + | P_aux (P_string_append pats, p_annot) -> + let pats = List.map folder pats in + P_aux (P_string_append pats, p_annot), !guards_ref, !expr_ref + | P_aux (P_cons (pat1, pat2), p_annot) -> + let pat1, guards, expr = rewrite_pat env (pat1, guards, expr) in + let pat2, guards, expr = rewrite_pat env (pat2, guards, expr) in + P_aux (P_cons (pat1, pat2), p_annot), guards, expr + | P_aux (P_id _, _) + | P_aux (P_lit _, _) + | P_aux (P_wild, _) -> pat, guards, expr + in + + let rec rewrite_pexp (Pat_aux (pexp_aux, pexp_annot) as pexp) = + + (* merge cases of Pat_exp and Pat_when *) + let (P_aux (p_aux, p_annot) as pat, guards, expr) = + match pexp_aux with + | Pat_exp (pat, expr) -> (pat, [], expr) + | Pat_when (pat, guard, expr) -> (pat, [guard], expr) + in + + let env = env_of_annot p_annot in + + let (new_pat, new_guards, new_expr) = + rewrite_pat env (pat, guards, expr) + in + + (* un-merge Pat_exp and Pat_when cases *) + let new_pexp = match new_guards with + | [] -> Pat_aux (Pat_exp (new_pat, new_expr), pexp_annot) + | gs -> Pat_aux (Pat_when (new_pat, fold_typed_guards env gs, new_expr), pexp_annot) + in + typ_debug (lazy (Printf.sprintf "rewritten pexp: %s\n%!" (Pretty_print_sail.doc_pexp new_pexp |> Pretty_print_sail.to_string))); + new_pexp + + in + pexp_rewriters rewrite_pexp + + let rewrite_defs_pat_lits = let rewrite_pexp (Pat_aux (pexp_aux, annot) as pexp) = let guards = ref [] in @@ -3257,9 +3657,222 @@ let merge_funcls (Defs defs) = | d -> d in Defs (List.map merge_in_def defs) + +let rec exp_of_mpat (MP_aux (mpat, annot)) = + let empty_vec = E_aux (E_vector [], annot) in + let concat_vectors annot vec1 vec2 = (* TODO FIXME, this should be OK for typing but doesn't attach location information properly *) + E_aux (E_vector_append (vec1, vec2), annot) + in + let empty_string = E_aux (E_lit (L_aux (L_string "", Parse_ast.Unknown)), annot) in + let string_append annot str1 str2 = + E_aux (E_app (mk_id "string_append", [str1; str2]), annot) + in + match mpat with + | MP_lit lit -> E_aux (E_lit lit, annot) + | MP_id id -> E_aux (E_id id, annot) + | MP_app (id, args) -> E_aux (E_app (id, (List.map exp_of_mpat args)), annot) + | MP_record (mfpats, flag) -> E_aux (E_record (fexps_of_mfpats mfpats flag annot), annot) + | MP_vector mpats -> E_aux (E_vector (List.map exp_of_mpat mpats), annot) + | MP_vector_concat mpats -> List.fold_right (concat_vectors annot) (List.map exp_of_mpat mpats) empty_vec + | MP_tup mpats -> E_aux (E_tuple (List.map exp_of_mpat mpats), annot) + | MP_list mpats -> E_aux (E_list (List.map exp_of_mpat mpats), annot) + | MP_cons (mpat1, mpat2) -> E_aux (E_cons (exp_of_mpat mpat1, exp_of_mpat mpat2), annot) + | MP_string_append mpats -> List.fold_right (string_append annot) (List.map exp_of_mpat mpats) empty_string + | MP_typ (mpat, typ) -> E_aux (E_cast (typ, exp_of_mpat mpat), annot) + +and fexps_of_mfpats mfpats flag annot = + let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) = + FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot) + in + FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot) + +let rec pat_of_mpat (MP_aux (mpat, annot)) = + match mpat with + | MP_lit lit -> P_aux (P_lit lit, annot) + | MP_id id -> P_aux (P_id id, annot) + | MP_app (id, args) -> P_aux (P_app (id, (List.map pat_of_mpat args)), annot) + | MP_record (mfpats, flag) -> P_aux (P_record ((fpats_of_mfpats mfpats), flag), annot) + | MP_vector mpats -> P_aux (P_vector (List.map pat_of_mpat mpats), annot) + | MP_vector_concat mpats -> P_aux (P_vector_concat (List.map pat_of_mpat mpats), annot) + | MP_tup mpats -> P_aux (P_tup (List.map pat_of_mpat mpats), annot) + | MP_list mpats -> P_aux (P_list (List.map pat_of_mpat mpats), annot) + | MP_cons (mpat1, mpat2) -> P_aux ((P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2), annot)) + | MP_string_append (mpats) -> P_aux ((P_string_append (List.map pat_of_mpat mpats), annot)) + | MP_typ (mpat, typ) -> P_aux (P_typ (typ, pat_of_mpat mpat), annot) + +and fpats_of_mfpats mfpats = + let fpat_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) = + FP_aux (FP_Fpat (id, pat_of_mpat mpat), annot) + in + List.map fpat_of_mfpat mfpats + +let rewrite_defs_realise_mappings (Defs defs) = + let realise_mpexps forwards mpexp1 mpexp2 = + let mpexp_pat, mpexp_exp = + if forwards then mpexp1, mpexp2 + else mpexp2, mpexp1 + in + let exp = + match mpexp_exp with + | MPat_aux ((MPat_pat mpat), _) -> exp_of_mpat mpat + | MPat_aux ((MPat_when (mpat, _), _)) -> exp_of_mpat mpat + in + match mpexp_pat with + | MPat_aux (MPat_pat mpat, annot) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), annot) + | MPat_aux (MPat_when (mpat, guard), annot) -> Pat_aux (Pat_when (pat_of_mpat mpat, guard, exp), annot) + in + let realise_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) = + realise_mpexps forwards mpexp1 mpexp2 + in + let realise_bool_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) = + let mpexp = if forwards then mpexp1 else mpexp2 in + realise_mpexps true mpexp (mk_mpexp (MPat_pat (mk_mpat (MP_lit (mk_lit L_true))))) + in + let arg_id = mk_id "arg#" in + let arg_exp = (mk_exp (E_id arg_id)) in + let arg_pat = mk_pat (P_id arg_id) in + let placeholder_id = mk_id "s#" in + let append_placeholder = function + | MPat_aux (MPat_pat (MP_aux (MP_string_append mpats, p_annot)), aux_annot) -> + MPat_aux (MPat_pat (MP_aux (MP_string_append (mpats @ [mk_mpat (MP_id placeholder_id)]), p_annot)), aux_annot) + | MPat_aux (MPat_when (MP_aux (MP_string_append mpats, p_annot), guard), aux_annot) -> + MPat_aux (MPat_when (MP_aux (MP_string_append (mpats @ [mk_mpat (MP_id placeholder_id)]), p_annot), guard), aux_annot) + | MPat_aux (MPat_pat mpat, aux_annot) -> + MPat_aux (MPat_pat (mk_mpat (MP_string_append [mpat; mk_mpat (MP_id placeholder_id)])), aux_annot) + | MPat_aux (MPat_when (mpat, guard), aux_annot) -> + MPat_aux (MPat_when (mk_mpat (MP_string_append [mpat; mk_mpat (MP_id placeholder_id)]), guard), aux_annot) + in + let realise_prefix_mapcl forwards id (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, ()))) = + let mpexp = if forwards then mpexp1 else mpexp2 in + let other = if forwards then mpexp2 else mpexp1 in + let strlen = ( + mk_mpat (MP_app ( mk_id "sub_nat", + [ + mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id arg_id )])); + mk_mpat (MP_app ( mk_id "string_length" , [mk_mpat (MP_id placeholder_id)])); + ] + )) + ) in + match other with + | MPat_aux (MPat_pat mpat2, _) + | MPat_aux (MPat_when (mpat2, _), _)-> + realise_mpexps true (append_placeholder mpexp) (mk_mpexp (MPat_pat (mk_mpat (MP_app ((mk_id "Some"), [ mk_mpat (MP_tup [mpat2; strlen]) ]))))) + in + let realise_mapdef (MD_aux (MD_mapping (id, mapcls), ((l, (tannot:tannot)) as annot))) = + let forwards_id = mk_id (string_of_id id ^ "_forwards") in + let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in + let backwards_id = mk_id (string_of_id id ^ "_backwards") in + let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in + + let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in + let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in + let env = match mapcls with + | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot + | _ -> Type_check.typ_error l "mapping with no clauses?" + in + let (typq, bidir_typ) = Env.get_val_spec id env in + let (typ1, typ2, l) = match bidir_typ with + | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l + | _ -> Type_check.typ_error l "non-bidir type of mapping?" + in + let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), l) in + let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), l) in + let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), l) in + let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), l) in + + let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_matches_typ, forwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let backwards_matches_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_matches_typ, backwards_matches_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + + let forwards_spec, env = Type_check.check_val_spec env forwards_spec in + let backwards_spec, env = Type_check.check_val_spec env backwards_spec in + let forwards_matches_spec, env = Type_check.check_val_spec env forwards_matches_spec in + let backwards_matches_spec, env = Type_check.check_val_spec env backwards_matches_spec in + + let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in + let forwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl true forwards_id) mapcls))) in + let backwards_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_mapcl false backwards_id) mapcls))) in + + let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_lit (mk_lit L_false)))) in + let forwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) @ [wildcard])) in + let backwards_matches_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) @ [wildcard])) in + + let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in + let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in + let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in + let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in + + typ_debug (lazy (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string))); + typ_debug (lazy (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string))); + typ_debug (lazy (Printf.sprintf "forwards matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_matches_fun |> Pretty_print_sail.to_string))); + typ_debug (lazy (Printf.sprintf "backwards matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_matches_fun |> Pretty_print_sail.to_string))); + let forwards_fun, _ = Type_check.check_fundef env forwards_fun in + let backwards_fun, _ = Type_check.check_fundef env backwards_fun in + let forwards_matches_fun, _ = Type_check.check_fundef env forwards_matches_fun in + let backwards_matches_fun, _ = Type_check.check_fundef env backwards_matches_fun in + + let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in + let prefix_wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_exp (E_lit (mk_lit L_unit))])))) in + let string_defs = + begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then + let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in + let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in + let forwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) @ [prefix_wildcard])) in + let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in + typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string))); + let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in + forwards_prefix_spec @ forwards_prefix_fun + else + if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then + let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in + let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in + let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in + let backwards_prefix_match = mk_exp (E_case (arg_exp, (List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) @ [prefix_wildcard])) in + let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in + typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string))); + let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in + backwards_prefix_spec @ backwards_prefix_fun + else + [] + end + in + + forwards_spec + @ forwards_fun + @ backwards_spec + @ backwards_fun + @ forwards_matches_spec + @ forwards_matches_fun + @ backwards_matches_spec + @ backwards_matches_fun + @ string_defs + in + let rewrite_def def = + match def with + | DEF_mapdef mdef -> realise_mapdef mdef + | d -> [d] + in + Defs (List.map rewrite_def defs |> List.flatten) + let recheck_defs defs = fst (check initial_env defs) +let remove_mapping_valspecs (Defs defs) = + let allowed_def def = + match def with + | DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (_, Typ_aux (Typ_bidir _, _)), _), _, _, _), _)) -> false + | _ -> true + in + Defs (List.filter allowed_def defs) + + let rewrite_defs_lem = [ + ("realise_mappings", rewrite_defs_realise_mappings); + ("remove_mapping_valspecs", remove_mapping_valspecs); + ("pat_string_append", rewrite_defs_pat_string_append); + ("mapping_builtins", rewrite_defs_mapping_patterns); + ("pat_lits", rewrite_defs_pat_lits); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); @@ -3294,6 +3907,9 @@ let rewrite_defs_lem = [ let rewrite_defs_ocaml = [ (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("realise_mappings", rewrite_defs_realise_mappings); + ("pat_string_append", rewrite_defs_pat_string_append); + ("mapping_builtins", rewrite_defs_mapping_patterns); ("pat_lits", rewrite_defs_pat_lits); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -3313,6 +3929,9 @@ let rewrite_defs_ocaml = [ let rewrite_defs_c = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("realise_mappings", rewrite_defs_realise_mappings); + ("pat_string_append", rewrite_defs_pat_string_append); + ("mapping_builtins", rewrite_defs_mapping_patterns); ("pat_lits", rewrite_defs_pat_lits); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -3330,6 +3949,9 @@ let rewrite_defs_c = [ let rewrite_defs_interpreter = [ ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); + ("realise_mappings", rewrite_defs_realise_mappings); + ("pat_string_append", rewrite_defs_pat_string_append); + ("mapping_builtins", rewrite_defs_mapping_patterns); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); diff --git a/src/rewrites.mli b/src/rewrites.mli index 41a13ffa..70cb75af 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -51,6 +51,9 @@ open Ast open Type_check +(* Generate a fresh id with the given prefix *) +val fresh_id : string -> l -> id + (* Re-write undefined to functions created by -undefined_gen flag *) val rewrite_undefined : bool -> tannot defs -> tannot defs diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 47acae88..81685bec 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -1,6 +1,9 @@ module Big_int = Nat_big_num type 'a return = { return : 'b . 'a -> 'b } +type 'za zoption = | ZNone of unit | ZSome of 'za;; + +let zint_forwards i = string_of_int (Big_int.to_int i) let opt_trace = ref false @@ -461,6 +464,28 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ Big_int.to_string n ^ str2 let eq_string (str1, str2) = String.compare str1 str2 == 0 +let string_startswith (str1, str2) = String.compare (String.sub str1 0 (String.length str2)) str2 == 0 + +let string_drop (str, n) = let n = Big_int.to_int n in String.sub str n (String.length str - n) + +let string_length str = Big_int.of_int (String.length str) + +let string_append (s1, s2) = s1 ^ s2 + +(* highly inefficient recursive implementation *) +let rec maybe_int_of_prefix = function + | "" -> ZNone () + | str -> + let len = String.length str in + match int_of_string_opt str with + | Some n -> ZSome (Big_int.of_int n, Big_int.of_int len) + | None -> maybe_int_of_prefix (String.sub str 0 (len - 1)) + +let maybe_int_of_string str = + match int_of_string_opt str with + | None -> ZNone () + | Some n -> ZSome (Big_int.of_int n) + let lt_int (x, y) = Big_int.less x y let set_slice (out_len, slice_len, out, n, slice) = @@ -597,3 +622,65 @@ let speculate_conditional_success () = true (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *) let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ())) +let rec n_leading_spaces s = + match String.length s with + | 0 -> 0 + | 1 -> begin match s with + | " " -> 1 + | _ -> 0 + end + | len -> begin match String.get s 0 with + | ' ' -> 1 + (n_leading_spaces (String.sub s 1 (len - 1))) + | _ -> 0 + end + + +let opt_spaces_matches_prefix s = + ZSome ((), n_leading_spaces s |> Big_int.of_int) + +let spaces_matches_prefix s = + let n = n_leading_spaces s in + match n with + | 0 -> ZNone () + | n -> ZSome ((), Big_int.of_int n) + + +let hex_bits_12_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 4096 then + ZSome ((bits_of_int 2048 n, len)) + else + ZNone () + +let hex_bits_13_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 8192 then + ZSome ((bits_of_int 4096 n, len)) + else + ZNone () + +let hex_bits_20_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 1048576 then + ZSome ((bits_of_int 524288 n, len)) + else + ZNone () + +let hex_bits_21_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + let n = Big_int.to_int n in + if 0 <= n && n < 2097152 then + ZSome ((bits_of_int 1048576 n, len)) + else + ZNone () diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 97b634da..7bb82719 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -88,7 +88,9 @@ let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt | Typ_id name -> Nameset.add (string_of_id name) mt | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1) - (free_type_names_t consider_var t2) + (free_type_names_t consider_var t2) + | Typ_bidir (t1, t2) -> Nameset.union (free_type_names_t consider_var t1) + (free_type_names_t consider_var t2) | Typ_tup ts -> free_type_names_ts consider_var ts | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs) | Typ_exist (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids @@ -116,6 +118,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t = else used | Typ_id id -> conditional_add_typ bound used id | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret + | Typ_bidir(t1, t2) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *) | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used | Typ_app(id,targs) -> List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id) @@ -451,6 +454,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_kind kdef -> fv_of_kind_def consider_var kdef | DEF_type tdef -> fv_of_type_def consider_var tdef | DEF_fundef fdef -> fv_of_fun consider_var fdef + | DEF_mapdef mdef -> mt,mt (* fv_of_map consider_var mdef *) | DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind)) | DEF_spec vspec -> fv_of_vspec consider_var vspec | DEF_fixity _ -> mt,mt diff --git a/src/type_check.ml b/src/type_check.ml index 65d07859..09b8a9c7 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -180,6 +180,85 @@ let is_atom (Typ_aux (typ_aux, _)) = | Typ_app (f, [_]) when string_of_id f = "atom" -> true | _ -> false + + +let rec strip_id = function + | Id_aux (Id x, _) -> Id_aux (Id x, Parse_ast.Unknown) + | Id_aux (DeIid x, _) -> Id_aux (DeIid x, Parse_ast.Unknown) +and strip_kid = function + | Kid_aux (Var x, _) -> Kid_aux (Var x, Parse_ast.Unknown) +and strip_base_effect = function + | BE_aux (eff, _) -> BE_aux (eff, Parse_ast.Unknown) +and strip_effect = function + | Effect_aux (Effect_set effects, _) -> Effect_aux (Effect_set (List.map strip_base_effect effects), Parse_ast.Unknown) +and strip_nexp_aux = function + | Nexp_id id -> Nexp_id (strip_id id) + | Nexp_var kid -> Nexp_var (strip_kid kid) + | Nexp_constant n -> Nexp_constant n + | Nexp_app (id, nexps) -> Nexp_app (id, List.map strip_nexp nexps) + | Nexp_times (nexp1, nexp2) -> Nexp_times (strip_nexp nexp1, strip_nexp nexp2) + | Nexp_sum (nexp1, nexp2) -> Nexp_sum (strip_nexp nexp1, strip_nexp nexp2) + | Nexp_minus (nexp1, nexp2) -> Nexp_minus (strip_nexp nexp1, strip_nexp nexp2) + | Nexp_exp nexp -> Nexp_exp (strip_nexp nexp) + | Nexp_neg nexp -> Nexp_neg (strip_nexp nexp) +and strip_nexp = function + | Nexp_aux (nexp_aux, _) -> Nexp_aux (strip_nexp_aux nexp_aux, Parse_ast.Unknown) +and strip_n_constraint_aux = function + | NC_equal (nexp1, nexp2) -> NC_equal (strip_nexp nexp1, strip_nexp nexp2) + | NC_bounded_ge (nexp1, nexp2) -> NC_bounded_ge (strip_nexp nexp1, strip_nexp nexp2) + | NC_bounded_le (nexp1, nexp2) -> NC_bounded_le (strip_nexp nexp1, strip_nexp nexp2) + | NC_not_equal (nexp1, nexp2) -> NC_not_equal (strip_nexp nexp1, strip_nexp nexp2) + | NC_set (kid, nums) -> NC_set (strip_kid kid, nums) + | NC_or (nc1, nc2) -> NC_or (strip_n_constraint nc1, strip_n_constraint nc2) + | NC_and (nc1, nc2) -> NC_and (strip_n_constraint nc1, strip_n_constraint nc2) + | NC_true -> NC_true + | NC_false -> NC_false +and strip_n_constraint = function + | NC_aux (nc_aux, _) -> NC_aux (strip_n_constraint_aux nc_aux, Parse_ast.Unknown) +and strip_typ_arg = function + | Typ_arg_aux (typ_arg_aux, _) -> Typ_arg_aux (strip_typ_arg_aux typ_arg_aux, Parse_ast.Unknown) +and strip_typ_arg_aux = function + | Typ_arg_nexp nexp -> Typ_arg_nexp (strip_nexp nexp) + | Typ_arg_typ typ -> Typ_arg_typ (strip_typ typ) + | Typ_arg_order ord -> Typ_arg_order (strip_order ord) +and strip_order = function + | Ord_aux (ord_aux, _) -> Ord_aux (strip_order_aux ord_aux, Parse_ast.Unknown) +and strip_order_aux = function + | Ord_var kid -> Ord_var (strip_kid kid) + | Ord_inc -> Ord_inc + | Ord_dec -> Ord_dec +and strip_typ_aux : typ_aux -> typ_aux = function + | Typ_id id -> Typ_id (strip_id id) + | Typ_var kid -> Typ_var (strip_kid kid) + | Typ_fn (typ1, typ2, effect) -> Typ_fn (strip_typ typ1, strip_typ typ2, strip_effect effect) + | Typ_bidir (typ1, typ2) -> Typ_bidir (strip_typ typ1, strip_typ typ2) + | Typ_tup typs -> Typ_tup (List.map strip_typ typs) + | Typ_exist (kids, constr, typ) -> Typ_exist ((List.map strip_kid kids), strip_n_constraint constr, strip_typ typ) + | Typ_app (id, args) -> Typ_app (strip_id id, List.map strip_typ_arg args) +and strip_typ : typ -> typ = function + | Typ_aux (typ_aux, _) -> Typ_aux (strip_typ_aux typ_aux, Parse_ast.Unknown) +and strip_typq = function TypQ_aux (typq_aux, l) -> TypQ_aux (strip_typq_aux typq_aux, Parse_ast.Unknown) +and strip_typq_aux = function + | TypQ_no_forall -> TypQ_no_forall + | TypQ_tq quants -> TypQ_tq (List.map strip_quant_item quants) +and strip_quant_item = function + | QI_aux (qi_aux, _) -> QI_aux (strip_qi_aux qi_aux, Parse_ast.Unknown) +and strip_qi_aux = function + | QI_id kinded_id -> QI_id (strip_kinded_id kinded_id) + | QI_const constr -> QI_const (strip_n_constraint constr) +and strip_kinded_id = function + | KOpt_aux (kinded_id_aux, _) -> KOpt_aux (strip_kinded_id_aux kinded_id_aux, Parse_ast.Unknown) +and strip_kinded_id_aux = function + | KOpt_none kid -> KOpt_none (strip_kid kid) + | KOpt_kind (kind, kid) -> KOpt_kind (strip_kind kind, strip_kid kid) +and strip_kind = function + | K_aux (k_aux, _) -> K_aux (strip_kind_aux k_aux, Parse_ast.Unknown) +and strip_kind_aux = function + | K_kind base_kinds -> K_kind (List.map strip_base_kind base_kinds) +and strip_base_kind = function + | BK_aux (bk_aux, _) -> BK_aux (bk_aux, Parse_ast.Unknown) + + (**************************************************************************) (* 1. Substitutions *) (**************************************************************************) @@ -221,6 +300,7 @@ and typ_subst_nexp_aux sv subst = function | Typ_id v -> Typ_id v | Typ_var kid -> Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2) | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args) | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) @@ -236,6 +316,7 @@ and typ_subst_typ_aux sv subst = function | Typ_id v -> Typ_id v | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2) | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args) | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_typ sv subst typ) @@ -257,6 +338,7 @@ and typ_subst_order_aux sv subst = function | Typ_id v -> Typ_id v | Typ_var kid -> Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2) | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args) | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, typ_subst_order sv subst typ) @@ -271,6 +353,7 @@ and typ_subst_kid_aux sv subst = function | Typ_id v -> Typ_id v | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs) + | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2) | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs) | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args) | Typ_exist (kids, nc, typ) when KidSet.mem sv (KidSet.of_list kids) -> Typ_exist (kids, nc, typ) @@ -308,6 +391,7 @@ module Env : sig val get_val_spec : id -> t -> typquant * typ val get_val_spec_orig : id -> t -> typquant * typ val is_union_constructor : id -> t -> bool + val is_mapping : id -> t -> bool val add_record : id -> typquant -> (typ * id) list -> t -> t val is_record : id -> t -> bool val get_accessor_fn : id -> id -> t -> typquant * typ @@ -315,6 +399,7 @@ module Env : sig val add_local : id -> mut * typ -> t -> t val get_locals : t -> (mut * typ) Bindings.t val add_variant : id -> typquant * type_union list -> t -> t + val add_mapping : id -> typquant * typ * typ -> t -> t val add_union_id : id -> typquant * typ -> t -> t val add_flow : id -> (typ -> typ) -> t -> t val get_flow : id -> t -> typ -> typ @@ -383,6 +468,7 @@ end = struct union_ids : (typquant * typ) Bindings.t; registers : typ Bindings.t; variants : (typquant * type_union list) Bindings.t; + mappings : (typquant * typ * typ) Bindings.t; typ_vars : base_kind_aux KBindings.t; typ_synonyms : (t -> typ_arg list -> typ) Bindings.t; num_defs : nexp Bindings.t; @@ -409,6 +495,7 @@ end = struct union_ids = Bindings.empty; registers = Bindings.empty; variants = Bindings.empty; + mappings = Bindings.empty; typ_vars = KBindings.empty; typ_synonyms = Bindings.empty; num_defs = Bindings.empty; @@ -459,6 +546,13 @@ end = struct ("itself", [BK_int]) ] + let builtin_mappings = + List.fold_left (fun m (name, typ) -> Bindings.add (mk_id name) typ m) Bindings.empty + [ + ("int", Typ_bidir(int_typ, string_typ)); + ("nat", Typ_bidir(nat_typ, string_typ)); + ] + let bound_typ_id env id = Bindings.mem id env.typ_synonyms || Bindings.mem id env.variants @@ -528,6 +622,7 @@ end = struct match typ with | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l) | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l) + | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l) | Typ_app (id, args) -> begin try @@ -648,6 +743,9 @@ end = struct | Typ_var kid when KBindings.mem kid env.typ_vars -> () | Typ_var kid -> typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret + | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 -> + typ_error l "Bidirectional types cannot be the same on both sides" + | Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2 | Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg ~exs:exs env) args; @@ -739,17 +837,56 @@ end = struct with | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) - let update_val_spec id (typq, typ) env = + let rec update_val_spec id (typq, typ) env = begin let typ = expand_synonyms env typ in typ_print (lazy ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind (typq, typ))); + let env = match typ with + | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env + | _ -> env + in { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } end - - let add_val_spec id bind env = - if Bindings.mem id env.top_val_specs - then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound") - else update_val_spec id bind env + and add_val_spec id (bind_typq, bind_typ) env = + if not (Bindings.mem id env.top_val_specs) + then update_val_spec id (bind_typq, bind_typ) env + else + let (existing_typq, existing_typ) = Bindings.find id env.top_val_specs in + let existing_cmp = (strip_typq existing_typq, strip_typ existing_typ) in + let bind_cmp = (strip_typq bind_typq, strip_typ bind_typ) in + if existing_cmp <> bind_cmp then + typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound as " ^ string_of_bind (existing_typq, existing_typ) ^ ", cannot rebind as " ^ string_of_bind (bind_typq, bind_typ)) + else + env + and add_mapping id (typq, typ1, typ2) env = + begin + typ_print (lazy ("Adding mapping " ^ string_of_id id)); + let forwards_id = mk_id (string_of_id id ^ "_forwards") in + let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in + let backwards_id = mk_id (string_of_id id ^ "_backwards") in + let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in + let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), Parse_ast.Unknown) in + let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), Parse_ast.Unknown) in + let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), Parse_ast.Unknown) in + let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), Parse_ast.Unknown) in + let env = + { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings } + |> add_val_spec forwards_id (typq, forwards_typ) + |> add_val_spec backwards_id (typq, backwards_typ) + |> add_val_spec forwards_matches_id (typq, forwards_matches_typ) + |> add_val_spec backwards_matches_id (typq, backwards_matches_typ) + in + let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in + begin if strip_typ typ1 = string_typ then + let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in + add_val_spec prefix_id (typq, forwards_prefix_typ) env + else if strip_typ typ2 = string_typ then + let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in + add_val_spec prefix_id (typq, backwards_prefix_typ) env + else + env + end + end let define_val_spec id env = if IdSet.mem id env.defined_val_specs @@ -764,6 +901,8 @@ end = struct let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in List.exists (is_ctor id) type_unions + let is_mapping id env = Bindings.mem id env.mappings + let add_enum id ids env = if bound_typ_id env id then typ_error (id_loc id) ("Cannot create enum " ^ string_of_id id ^ ", type name is already bound") @@ -1143,6 +1282,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, _)) = | Typ_tup typs -> List.for_all is_typ_monomorphic typs | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args | Typ_fn (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2 + | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2 | Typ_exist _ | Typ_var _ -> false and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) = match arg with @@ -1303,6 +1443,8 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) = | Typ_exist (kids, nc, typ) -> typ_nexps typ | Typ_fn (typ1, typ2, _) -> typ_nexps typ1 @ typ_nexps typ2 + | Typ_bidir (typ1, typ2) -> + typ_nexps typ1 @ typ_nexps typ2 and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with | Typ_arg_nexp n -> [n] @@ -1318,6 +1460,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) = | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args) | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2) + | Typ_bidir (typ1, typ2) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2) and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) = match typ_arg_aux with | Typ_arg_nexp n -> nexp_frees ~exs:exs n @@ -1679,7 +1822,7 @@ let rec kid_order kids (Typ_aux (aux, l) as typ) = List.fold_left (fun (ord, kids) typ -> let (ord', kids) = kid_order kids typ in (ord @ ord', kids)) ([], kids) typs | Typ_app (_, args) -> List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args - | Typ_fn _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ) + | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ) and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) = match aux with | Typ_arg_typ typ -> kid_order kids typ @@ -1695,6 +1838,7 @@ let rec alpha_equivalent env typ1 typ2 = match aux with | Typ_id _ | Typ_var _ -> aux | Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff) + | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2) | Typ_tup typs -> Typ_tup (List.map relabel typs) | Typ_exist (kids, nc, typ) -> let (kids, _) = kid_order (KidSet.of_list kids) typ in @@ -1928,6 +2072,18 @@ let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot) +let typ_of_pexp (Pat_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let env_of_pexp (Pat_aux (_, (l, tannot))) = env_of_annot (l, tannot) + +let typ_of_mpat (MP_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let env_of_mpat (MP_aux (_, (l, tannot))) = env_of_annot (l, tannot) + +let typ_of_mpexp (MPat_aux (_, (l, tannot))) = typ_of_annot (l, tannot) + +let env_of_mpexp (MPat_aux (_, (l, tannot))) = env_of_annot (l, tannot) + let lexp_typ_of (LEXP_aux (_, (l, tannot))) = typ_of_annot (l, tannot) let lexp_env_of (LEXP_aux (_, (l, tannot))) = env_of_annot (l, tannot) @@ -2137,6 +2293,10 @@ let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) - let strip_pexp : 'a pexp -> unit pexp = function pexp -> map_pexp_annot (fun (l, _) -> (l, ())) pexp let strip_lexp : 'a lexp -> unit lexp = function lexp -> map_lexp_annot (fun (l, _) -> (l, ())) lexp +let strip_mpat : 'a mpat -> unit mpat = function mpat -> map_mpat_annot (fun (l, _) -> (l, ())) mpat +let strip_mpexp : 'a mpexp -> unit mpexp = function mpexp -> map_mpexp_annot (fun (l, _) -> (l, ())) mpexp +let strip_mapcl : 'a mapcl -> unit mapcl = function mapcl -> map_mapcl_annot (fun (l, _) -> (l, ())) mapcl + let fresh_var = let counter = ref 0 in fun () -> let n = !counter in @@ -2263,6 +2423,20 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ print_endline ("Solved " ^ string_of_nexp nexp ^ " = " ^ Big_int.to_string n); annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ end + | E_app (mapping, xs), _ when Env.is_mapping mapping env -> + let forwards_id = mk_id (string_of_id mapping ^ "_forwards") in + let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in + typ_print (lazy("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); + begin try crule check_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) typ with + | Type_error (_, err1) -> + typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); + typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); + begin try crule check_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) typ with + | Type_error (_, err2) -> + typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); + typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) + end + end | E_app (f, xs), _ when List.length (Env.get_overloads f env) > 0 -> let rec try_overload = function | (errs, []) -> typ_raise l (Err_no_overloading (f, errs)) @@ -2380,6 +2554,29 @@ and check_case env pat_typ pexp typ = check_case env pat_typ (Pat_aux (Pat_when (mk_pat (P_id (mk_id "p#")), guard, case), annot)) typ | _ -> raise typ_exn +and check_mpexp env mpexp typ = + let mpat,guard,((l,_) as annot) = destruct_mpexp mpexp in + match bind_mpat env mpat typ with + | checked_mpat, env, guards -> + let guard = match guard, guards with + | None, h::t -> Some (h,t) + | Some x, l -> Some (x,l) + | None, [] -> None + in + let guard = match guard with + | Some (h,t) -> + Some (List.fold_left (fun acc guard -> mk_exp (E_app_infix (acc, mk_id "&", guard))) h t) + | None -> None + in + let checked_guard, env' = match guard with + | None -> None, env + | Some guard -> + let checked_guard = check_exp env guard bool_typ in + let flows, constrs = infer_flow env checked_guard in + Some checked_guard, add_constraints constrs (add_flows true flows env) + in + construct_mpexp (checked_mpat, checked_guard, (l, None)) + (* type_coercion env exp typ takes a fully annoted (i.e. already type checked) expression exp, and attempts to cast (coerce) it to the type typ by inserting a coercion function that transforms the @@ -2496,6 +2693,21 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) annot_pat (P_cons (hd_pat, tl_pat)) typ, env, hd_guards @ tl_guards | _ -> typ_error l "Cannot match cons pattern against non-list type" end + | P_string_append pats -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 -> + let rec process_pats env = function + | [] -> [], env, [] + | pat :: pats -> + let pat', env, guards = bind_pat env pat typ in + let pats', env, guards' = process_pats env pats in + pat' :: pats', env, guards @ guards' + in + let pats, env, guards = process_pats env pats in + annot_pat (P_string_append pats) typ, env, guards + | _ -> typ_error l "Cannot match string-append pattern against non-string type" + end | P_list pats -> begin match Env.expand_synonyms env typ with @@ -2560,8 +2772,59 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) end | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f) end - | P_app (f, _) when not (Env.is_union_constructor f env) -> - typ_error l (string_of_id f ^ " is not a union constructor in pattern " ^ string_of_pat pat) + + | P_app (f, pats) when Env.is_mapping f env -> + begin + let (typq, mapping_typ) = Env.get_val_spec f env in + let quants = quant_items typq in + let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with + | Typ_tup typs -> typs + | _ -> [typ] + in + match Env.expand_synonyms env mapping_typ with + | Typ_aux (Typ_bidir (typ1, typ2), _) -> + begin + try + typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); + let unifiers, _, _ (* FIXME! *) = unify l env typ2 typ in + typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); + let arg_typ' = subst_unifiers unifiers typ1 in + let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in + if (match quants' with [] -> false | _ -> true) + then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat) + else (); + let ret_typ' = subst_unifiers unifiers typ2 in + let tpats, env, guards = + try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with + | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length" + in + annot_pat (P_app (f, List.rev tpats)) typ, env, guards + with + | Unification_error (l, m) -> + try + typ_debug (lazy "Unifying mapping forwards failed, trying backwards."); + typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); + let unifiers, _, _ (* FIXME! *) = unify l env typ1 typ in + typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); + let arg_typ' = subst_unifiers unifiers typ2 in + let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in + if (match quants' with [] -> false | _ -> true) + then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat) + else (); + let ret_typ' = subst_unifiers unifiers typ1 in + let tpats, env, guards = + try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with + | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length" + in + annot_pat (P_app (f, List.rev tpats)) typ, env, guards + with + | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against mapping constructor: " ^ m) + end + | _ -> typ_error l ("Mal-formed mapping " ^ string_of_id f) + end + + | P_app (f, _) when (not (Env.is_union_constructor f env) && not (Env.is_mapping f env)) -> + typ_error l (string_of_id f ^ " is not a union constructor or mapping in pattern " ^ string_of_pat pat) | P_as (pat, id) -> let (typed_pat, env, guards) = bind_pat env pat typ in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), Env.add_local id (Immutable, pat_typ_of typed_pat) env, guards @@ -2625,6 +2888,16 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = in let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_pats)) in annot_pat (P_vector_concat inferred_pats) (dvector_typ env len vtyp), env, guards + | P_string_append pats -> + let fold_pats (pats, env, guards) pat = + let inferred_pat, env, guards' = infer_pat env pat in + typ_equality l env (pat_typ_of inferred_pat) string_typ; + pats @ [inferred_pat], env, guards' @ guards + in + let typed_pats, env, guards = + List.fold_left fold_pats ([], env, []) pats + in + annot_pat (P_string_append typed_pats) string_typ, env, guards | P_as (pat, id) -> let (typed_pat, env, guards) = infer_pat env pat in annot_pat (P_as (typed_pat, id)) (pat_typ_of typed_pat), @@ -2935,6 +3208,20 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = let checked_exp = crule check_exp env exp typ in annot_exp (E_cast (typ, checked_exp)) typ | E_app_infix (x, op, y) -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) + | E_app (mapping, xs) when Env.is_mapping mapping env -> + let forwards_id = mk_id (string_of_id mapping ^ "_forwards") in + let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in + typ_print (lazy ("Trying forwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); + begin try irule infer_exp env (E_aux (E_app (forwards_id, xs), (l, ()))) with + | Type_error (_, err1) -> + typ_print (lazy ("Error in forwards direction: " ^ string_of_type_error err1)); + typ_print (lazy ("Trying backwards direction for mapping " ^ string_of_id mapping ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")")); + begin try irule infer_exp env (E_aux (E_app (backwards_id, xs), (l, ()))) with + | Type_error (_, err2) -> + typ_print (lazy ("Error in backwards direction: " ^ string_of_type_error err2)); + typ_raise l (Err_no_overloading (mapping, [(forwards_id, err1); (backwards_id, err2)])) + end + end | E_app (f, xs) when List.length (Env.get_overloads f env) > 0 -> let rec try_overload = function | (errs, []) -> typ_raise l (Err_no_overloading (f, errs)) @@ -2985,6 +3272,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_vector_access (v, n) -> infer_exp env (E_aux (E_app (mk_id "vector_access", [v; n]), (l, ()))) | E_vector_update (v, n, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update", [v; n; exp]), (l, ()))) | E_vector_update_subrange (v, n, m, exp) -> infer_exp env (E_aux (E_app (mk_id "vector_update_subrange", [v; n; m; exp]), (l, ()))) + | E_vector_append (v1, E_aux (E_vector [], _)) -> infer_exp env v1 | E_vector_append (v1, v2) -> infer_exp env (E_aux (E_app (mk_id "append", [v1; v2]), (l, ()))) | E_vector_subrange (v, n, m) -> infer_exp env (E_aux (E_app (mk_id "vector_subrange", [v; n; m]), (l, ()))) | E_vector [] -> typ_error l "Cannot infer type of empty vector" @@ -3210,6 +3498,243 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ = typ_debug (lazy ("RETURNING AFTER COERCION " ^ string_of_typ (typ_of exp))); exp, !all_unifiers +and bind_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) (Typ_aux (typ_aux, _) as typ) = + let (Typ_aux (typ_aux, _) as typ), env = bind_existential typ env in + typ_print (lazy ("Binding " ^ string_of_mpat mpat ^ " to " ^ string_of_typ typ)); + let annot_mpat mpat typ = MP_aux (mpat, (l, Some (env, typ, no_effect))) in + let switch_typ mpat typ = match mpat with + | MP_aux (pat_aux, (l, Some (env, _, eff))) -> MP_aux (pat_aux, (l, Some (env, typ, eff))) + | _ -> typ_error l "Cannot switch type for unannotated mapping-pattern" + in + let bind_tuple_mpat (tpats, env, guards) mpat typ = + let tpat, env, guards' = bind_mpat env mpat typ in tpat :: tpats, env, guards' @ guards + in + match mpat_aux with + | MP_id v -> + begin + (* If the identifier we're matching on is also a constructor of + a union, that's probably a mistake, so warn about it. *) + if Env.is_union_constructor v env then + Util.warn (Printf.sprintf "Identifier %s found in mapping-pattern is also a union constructor at %s\n" + (string_of_id v) + (Reporting_basic.loc_to_string l)) + else (); + match Env.lookup_id v env with + | Local (Immutable, _) | Unbound -> annot_mpat (MP_id v) typ, Env.add_local v (Immutable, typ) env, [] + | Local (Mutable, _) | Register _ -> + typ_error l ("Cannot shadow mutable local or register in switch statement mapping-pattern " ^ string_of_mpat mpat) + | Enum enum -> subtyp l env enum typ; annot_mpat (MP_id v) typ, env, [] + end + | MP_cons (hd_mpat, tl_mpat) -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 -> + let hd_mpat, env, hd_guards = bind_mpat env hd_mpat ltyp in + let tl_mpat, env, tl_guards = bind_mpat env tl_mpat typ in + annot_mpat (MP_cons (hd_mpat, tl_mpat)) typ, env, hd_guards @ tl_guards + | _ -> typ_error l "Cannot match cons mapping-pattern against non-list type" + end + | MP_string_append mpats -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_id id, _) when Id.compare id (mk_id "string") = 0 -> + let rec process_mpats env = function + | [] -> [], env, [] + | pat :: pats -> + let pat', env, guards = bind_mpat env pat typ in + let pats', env, guards' = process_mpats env pats in + pat' :: pats', env, guards @ guards' + in + let pats, env, guards = process_mpats env mpats in + annot_mpat (MP_string_append pats) typ, env, guards + | _ -> typ_error l "Cannot match string-append pattern against non-string type" + end + | MP_list mpats -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ ltyp, _)]), _) when Id.compare f (mk_id "list") = 0 -> + let rec process_mpats env = function + | [] -> [], env, [] + | (pat :: mpats) -> + let mpat', env, guards = bind_mpat env mpat ltyp in + let mpats', env, guards' = process_mpats env mpats in + mpat' :: mpats', env, guards @ guards' + in + let mpats, env, guards = process_mpats env mpats in + annot_mpat (MP_list mpats) typ, env, guards + | _ -> typ_error l ("Cannot match list mapping-pattern " ^ string_of_mpat mpat ^ " against non-list type " ^ string_of_typ typ) + end + | MP_tup [] -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_id typ_id, _) when string_of_id typ_id = "unit" -> + annot_mpat (MP_tup []) typ, env, [] + | _ -> typ_error l "Cannot match unit mapping-pattern against non-unit type" + end + | MP_tup mpats -> + begin + match Env.expand_synonyms env typ with + | Typ_aux (Typ_tup typs, _) -> + let tpats, env, guards = + try List.fold_left2 bind_tuple_mpat ([], env, []) mpats typs with + | Invalid_argument _ -> typ_error l "Tuple mapping-pattern and tuple type have different length" + in + annot_mpat (MP_tup (List.rev tpats)) typ, env, guards + | _ -> typ_error l "Cannot bind tuple mapping-pattern against non tuple type" + end + | MP_app (f, mpats) when Env.is_union_constructor f env -> + begin + let (typq, ctor_typ) = Env.get_val_spec f env in + let quants = quant_items typq in + let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with + | Typ_tup typs -> typs + | _ -> [typ] + in + match Env.expand_synonyms env ctor_typ with + | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) -> + begin + try + typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ)); + let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in + typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); + let arg_typ' = subst_unifiers unifiers arg_typ in + let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in + if (match quants' with [] -> false | _ -> true) + then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in mapping-pattern " ^ string_of_mpat mpat) + else (); + let ret_typ' = subst_unifiers unifiers ret_typ in + let tpats, env, guards = + try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with + | Invalid_argument _ -> typ_error l "Union constructor mapping-pattern arguments have incorrect length" + in + annot_mpat (MP_app (f, List.rev tpats)) typ, env, guards + with + | Unification_error (l, m) -> typ_error l ("Unification error when mapping-pattern matching against union constructor: " ^ m) + end + | _ -> typ_error l ("Mal-formed constructor " ^ string_of_id f) + end + | MP_app (other, mpats) when Env.is_mapping other env -> + begin + let (typq, mapping_typ) = Env.get_val_spec other env in + let quants = quant_items typq in + let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with + | Typ_tup typs -> typs + | _ -> [typ] + in + match Env.expand_synonyms env mapping_typ with + | Typ_aux (Typ_bidir (typ1, typ2), _) -> + begin + try + typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); + let unifiers, _, _ (* FIXME! *) = unify l env typ2 typ in + typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); + let arg_typ' = subst_unifiers unifiers typ1 in + let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in + if (match quants' with [] -> false | _ -> true) + then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_mpat mpat) + else (); + let ret_typ' = subst_unifiers unifiers typ2 in + let tpats, env, guards = + try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with + | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length" + in + annot_mpat (MP_app (other, List.rev tpats)) typ, env, guards + with + | Unification_error (l, m) -> + try + typ_debug (lazy "Unifying mapping forwards failed, trying backwards."); + typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ)); + let unifiers, _, _ (* FIXME! *) = unify l env typ1 typ in + typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers))); + let arg_typ' = subst_unifiers unifiers typ2 in + let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in + if (match quants' with [] -> false | _ -> true) + then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_mpat mpat) + else (); + let ret_typ' = subst_unifiers unifiers typ1 in + let tpats, env, guards = + try List.fold_left2 bind_tuple_mpat ([], env, []) mpats (untuple arg_typ') with + | Invalid_argument _ -> typ_error l "Mapping pattern arguments have incorrect length" + in + annot_mpat (MP_app (other, List.rev tpats)) typ, env, guards + with + | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against mapping constructor: " ^ m) + end + end + | MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env)-> + typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat) + (* This is a special case for flow typing when we match a constant numeric literal. *) + | MP_lit (L_aux (L_num n, _) as lit) when is_atom typ -> + let nexp = match destruct_atom_nexp env typ with Some n -> n | None -> assert false in + annot_mpat (MP_lit lit) (atom_typ (nconstant n)), Env.add_constraint (nc_eq nexp (nconstant n)) env, [] + | _ -> + let (inferred_mpat, env, guards) = infer_mpat env mpat in + match subtyp l env typ (typ_of_mpat inferred_mpat) with + | () -> switch_typ inferred_mpat (typ_of_mpat inferred_mpat), env, guards + | exception (Type_error _ as typ_exn) -> + match mpat_aux with + | MP_lit lit -> + let var = fresh_var () in + let guard = mk_exp (E_app_infix (mk_exp (E_id var), mk_id "==", mk_exp (E_lit lit))) in + let (typed_mpat, env, guards) = bind_mpat env (mk_mpat (MP_id var)) typ in + typed_mpat, env, guard::guards + | _ -> raise typ_exn +and infer_mpat env (MP_aux (mpat_aux, (l, ())) as mpat) = + let annot_mpat mpat typ = MP_aux (mpat, (l, Some (env, typ, no_effect))) in + match mpat_aux with + | MP_id v -> + begin + match Env.lookup_id v env with + | Local (Immutable, _) | Unbound -> + typ_error l ("Cannot infer identifier in mapping-pattern " ^ string_of_mpat mpat ^ " - try adding a type annotation") + | Local (Mutable, _) | Register _ -> + typ_error l ("Cannot shadow mutable local or register in mapping-pattern " ^ string_of_mpat mpat) + | Enum enum -> annot_mpat (MP_id v) enum, env, [] + end + | MP_lit lit -> + annot_mpat (MP_lit lit) (infer_lit env lit), env, [] + | MP_typ (mpat, typ_annot) -> + Env.wf_typ env typ_annot; + let (typed_mpat, env, guards) = bind_mpat env mpat typ_annot in + annot_mpat (MP_typ (typed_mpat, typ_annot)) typ_annot, env, guards + | MP_vector (mpat :: mpats) -> + let fold_mpats (mpats, env, guards) mpat = + let typed_mpat, env, guards' = bind_mpat env mpat bit_typ in + mpats @ [typed_mpat], env, guards' @ guards + in + let mpats, env, guards = List.fold_left fold_mpats ([], env, []) (mpat :: mpats) in + let len = nexp_simp (nint (List.length mpats)) in + let etyp = typ_of_mpat (List.hd mpats) in + List.iter (fun mpat -> typ_equality l env etyp (typ_of_mpat mpat)) mpats; + annot_mpat (MP_vector mpats) (dvector_typ env len etyp), env, guards + | MP_vector_concat (mpat :: mpats) -> + let fold_mpats (mpats, env, guards) mpat = + let inferred_mpat, env, guards' = infer_mpat env mpat in + mpats @ [inferred_mpat], env, guards' @ guards + in + let inferred_mpats, env, guards = + List.fold_left fold_mpats ([], env, []) (mpat :: mpats) in + let (len, _, vtyp) = destruct_vec_typ l env (typ_of_mpat (List.hd inferred_mpats)) in + let fold_len len mpat = + let (len', _, vtyp') = destruct_vec_typ l env (typ_of_mpat mpat) in + typ_equality l env vtyp vtyp'; + nsum len len' + in + let len = nexp_simp (List.fold_left fold_len len (List.tl inferred_mpats)) in + annot_mpat (MP_vector_concat inferred_mpats) (dvector_typ env len vtyp), env, guards + | MP_string_append mpats -> + let fold_pats (pats, env, guards) pat = + let inferred_pat, env, guards' = infer_mpat env pat in + typ_equality l env (typ_of_mpat inferred_pat) string_typ; + pats @ [inferred_pat], env, guards' @ guards + in + let typed_mpats, env, guards = + List.fold_left fold_pats ([], env, []) mpats + in + annot_mpat (MP_string_append typed_mpats) string_typ, env, guards + + | _ -> typ_error l ("Couldn't infer type of mapping-pattern " ^ string_of_mpat mpat) + (**************************************************************************) (* 6. Effect system *) (**************************************************************************) @@ -3233,15 +3758,20 @@ let add_effect_lexp (LEXP_aux (lexp, (l, annot))) eff = LEXP_aux (lexp, (l, add_effect_annot annot eff)) let effect_of_pat (P_aux (exp, (l, annot))) = effect_of_annot annot +let effect_of_mpat (MP_aux (exp, (l, annot))) = effect_of_annot annot let add_effect_pat (P_aux (pat, (l, annot))) eff = P_aux (pat, (l, add_effect_annot annot eff)) +let add_effect_mpat (MP_aux (mpat, (l, annot))) eff = + MP_aux (mpat, (l, add_effect_annot annot eff)) + let collect_effects xs = List.fold_left union_effects no_effect (List.map effect_of xs) let collect_effects_lexp xs = List.fold_left union_effects no_effect (List.map effect_of_lexp xs) let collect_effects_pat xs = List.fold_left union_effects no_effect (List.map effect_of_pat xs) +let collect_effects_mpat xs = List.fold_left union_effects no_effect (List.map effect_of_mpat xs) (* Traversal that propagates effects upwards through expressions *) @@ -3411,6 +3941,30 @@ and propagate_pexp_effect = function | None -> Pat_aux (Pat_when (p_pat, p_guard, p_exp), (l, None)), p_eff end +and propagate_mpexp_effect = function + | MPat_aux (MPat_pat mpat, (l, annot)) -> + begin + let p_mpat = propagate_mpat_effect mpat in + let p_eff = effect_of_mpat p_mpat in + match annot with + | Some (typq, typ, eff) -> + MPat_aux (MPat_pat p_mpat, (l, Some (typq, typ, union_effects eff p_eff))), + union_effects eff p_eff + | None -> MPat_aux (MPat_pat p_mpat, (l, None)), p_eff + end + | MPat_aux (MPat_when (mpat, guard), (l, annot)) -> + begin + let p_mpat = propagate_mpat_effect mpat in + let p_guard = propagate_exp_effect guard in + let p_eff = union_effects (effect_of_mpat p_mpat) (effect_of p_guard) + in + match annot with + | Some (typq, typ, eff) -> + MPat_aux (MPat_when (p_mpat, p_guard), (l, Some (typq, typ, union_effects eff p_eff))), + union_effects eff p_eff + | None -> MPat_aux (MPat_when (p_mpat, p_guard), (l, None)), p_eff + end + and propagate_pat_effect (P_aux (pat, annot)) = let p_pat, eff = propagate_pat_effect_aux pat in add_effect_pat (P_aux (p_pat, annot)) eff @@ -3421,6 +3975,9 @@ and propagate_pat_effect_aux = function let p_pat1 = propagate_pat_effect pat1 in let p_pat2 = propagate_pat_effect pat2 in P_cons (p_pat1, p_pat2), union_effects (effect_of_pat p_pat1) (effect_of_pat p_pat2) + | P_string_append pats -> + let p_pats = List.map propagate_pat_effect pats in + P_string_append p_pats, collect_effects_pat p_pats | P_as (pat, id) -> let p_pat = propagate_pat_effect pat in P_as (p_pat, id), effect_of_pat p_pat @@ -3448,6 +4005,40 @@ and propagate_pat_effect_aux = function P_vector p_pats, collect_effects_pat p_pats | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in pat" +and propagate_mpat_effect (MP_aux (mpat, annot)) = + let p_mpat, eff = propagate_mpat_effect_aux mpat in + add_effect_mpat (MP_aux (p_mpat, annot)) eff +and propagate_mpat_effect_aux = function + | MP_lit lit -> MP_lit lit, no_effect + | MP_cons (mpat1, mpat2) -> + let p_mpat1 = propagate_mpat_effect mpat1 in + let p_mpat2 = propagate_mpat_effect mpat2 in + MP_cons (p_mpat1, p_mpat2), union_effects (effect_of_mpat p_mpat1) (effect_of_mpat p_mpat2) + | MP_string_append mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_string_append p_mpats, collect_effects_mpat p_mpats + | MP_id id -> MP_id id, no_effect + | MP_app (id, mpats) -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_app (id, p_mpats), collect_effects_mpat p_mpats + | MP_tup mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_tup p_mpats, collect_effects_mpat p_mpats + | MP_list mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_list p_mpats, collect_effects_mpat p_mpats + | MP_vector_concat mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_vector_concat p_mpats, collect_effects_mpat p_mpats + | MP_vector mpats -> + let p_mpats = List.map propagate_mpat_effect mpats in + MP_vector p_mpats, collect_effects_mpat p_mpats + | MP_typ (mpat, typ) -> + let p_mpat = propagate_mpat_effect mpat in + MP_typ (p_mpat, typ), effect_of_mpat mpat + | _ -> typ_error Parse_ast.Unknown "Unimplemented: Cannot propagate effect in mpat" + + and propagate_letbind_effect (LB_aux (lb, (l, annot))) = let p_lb, eff = propagate_letbind_effect_aux lb in match annot with @@ -3537,11 +4128,30 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ = end | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") + +let check_mapcl env (MCL_aux (MCL_mapcl (mpexp1, mpexp2), (l, _))) typ = + match typ with + | Typ_aux (Typ_bidir (typ1, typ2), _) -> + begin + let typed_mpexp1, prop_eff1 = propagate_mpexp_effect (check_mpexp env (strip_mpexp mpexp1) typ1) in + let typed_mpexp2, prop_eff2 = propagate_mpexp_effect (check_mpexp env (strip_mpexp mpexp2) typ2) in + MCL_aux (MCL_mapcl (typed_mpexp1, typed_mpexp2), (l, Some (env, typ, union_effects prop_eff1 prop_eff2))) + end + | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type") + + let funcl_effect (FCL_aux (FCL_Funcl (id, typed_pexp), (l, annot))) = match annot with | Some (_, _, eff) -> eff | None -> no_effect (* Maybe could be assert false. This should never happen *) + +let mapcl_effect (MCL_aux (MCL_mapcl _, (l, annot))) = + match annot with + | Some (_, _, eff) -> eff + | None -> no_effect (* Maybe could be assert false. This should never happen *) + + let infer_funtyp l env tannotopt funcls = match tannotopt with | Typ_annot_opt_aux (Typ_annot_opt_some (quant, ret_typ), _) -> @@ -3620,6 +4230,24 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) vs_def @ [DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, None)))], env else typ_error l ("Effects do not match: " ^ string_of_effect declared_eff ^ " declared and " ^ string_of_effect eff ^ " found") + +let check_mapdef env (MD_aux (MD_mapping (id, mapcls), (l, _)) as md_aux) = + typ_print (lazy ("\nChecking mapping " ^ string_of_id id)); + let quant, typ = Env.get_val_spec id env in + let vtyp1, vtyp2, vl = match typ with + | Typ_aux (Typ_bidir (vtyp1, vtyp2), vl) -> vtyp1, vtyp2, vl + | _ -> typ_error l "Mapping val spec was not a mapping type" + in + typ_debug (lazy ("Checking mapdef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ))); + let mapcl_env = add_typquant quant env in + let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in + let eff = List.fold_left union_effects no_effect (List.map mapcl_effect mapcls) in + if equal_effects eff no_effect then + [DEF_mapdef (MD_aux (MD_mapping (id, mapcls), (l, None)))], env + else + typ_error l ("Mapping not pure:" ^ string_of_effect eff ^ " found") + + (* Checking a val spec simply adds the type as a binding in the context. We have to destructure the various kinds of val specs, but the difference is irrelevant for the typechecker. *) @@ -3765,6 +4393,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_type tdef -> check_typedef env tdef | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env | DEF_fundef fdef -> check_fundef env fdef + | DEF_mapdef mdef -> check_mapdef env mdef | DEF_internal_mutrec fdefs -> let defs = List.concat (List.map (fun fdef -> fst (check_fundef env fdef)) fdefs) in let split_fundef (defs, fdefs) def = match def with @@ -3808,6 +4437,9 @@ let initial_env = (* Internal functions for Monomorphise.AtomToItself *) + (* |> Env.add_val_spec (mk_id "int") + * (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *) + |> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int") |> Env.add_val_spec (mk_id "size_itself_int") (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)), diff --git a/src/type_check.mli b/src/type_check.mli index 1c0e2f09..f1ce967e 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -81,6 +81,9 @@ exception Type_error of l * type_error;; val string_of_type_error : type_error -> string +val typ_debug : string Lazy.t -> unit +val typ_print : string Lazy.t -> unit + (** {2 Environments} *) (** The env module defines the internal type checking environment, and @@ -158,6 +161,8 @@ module Env : sig val is_union_constructor : id -> t -> bool + val is_mapping : id -> t -> bool + val is_register : id -> t -> bool (** Return a fresh kind identifier that doesn't exist in the @@ -213,9 +218,28 @@ val strip_exp : 'a exp -> unit exp (** Strip the type annotations from a pattern *) val strip_pat : 'a pat -> unit pat +(** Strip the type annotations from a pattern-expression *) +val strip_pexp : 'a pexp -> unit pexp + (** Strip the type annotations from an l-expression *) val strip_lexp : 'a lexp -> unit lexp +val strip_mpexp : 'a mpexp -> unit mpexp +val strip_mapcl : 'a mapcl -> unit mapcl + +(* Strip location information from types for comparison purposes *) +val strip_typ : typ -> typ +val strip_typq : typquant -> typquant +val strip_id : id -> id +val strip_kid : kid -> kid +val strip_base_effect : base_effect -> base_effect +val strip_effect : effect -> effect +val strip_nexp_aux : nexp_aux -> nexp_aux +val strip_nexp : nexp -> nexp +val strip_n_constraint_aux : n_constraint_aux -> n_constraint_aux +val strip_n_constraint : n_constraint -> n_constraint +val strip_typ_aux : typ_aux -> typ_aux + (** {2 Checking expressions and patterns} *) (** Check an expression has some type. Returns a fully annotated @@ -228,6 +252,14 @@ val check_exp : Env.t -> unit exp -> typ -> tannot exp val infer_exp : Env.t -> unit exp -> tannot exp +val infer_pat : Env.t -> unit pat -> tannot pat * Env.t * unit exp list + +val check_case : Env.t -> typ -> unit pexp -> typ -> tannot pexp + +val check_fundef : Env.t -> 'a fundef -> tannot def list * Env.t + +val check_val_spec : Env.t -> 'a val_spec -> tannot def list * Env.t + val prove : Env.t -> n_constraint -> bool val solve : Env.t -> nexp -> Big_int.num option @@ -241,6 +273,8 @@ val bind_pat : Env.t -> unit pat -> typ -> tannot pat * Env.t * unit Ast.exp lis on patterns that have previously been type checked. *) val bind_pat_no_guard : Env.t -> unit pat -> typ -> tannot pat * Env.t +val typ_error : Ast.l -> string -> 'a + (** {2 Destructuring type annotations} Partial functions: The expressions and patterns passed to these functions must be guaranteed to have tannots of the form Some (env, typ) for these to @@ -252,9 +286,19 @@ val env_of_annot : Ast.l * tannot -> Env.t val typ_of : tannot exp -> typ val typ_of_annot : Ast.l * tannot -> typ + val pat_typ_of : tannot pat -> typ val pat_env_of : tannot pat -> Env.t +val typ_of_pexp : tannot pexp -> typ +val env_of_pexp : tannot pexp -> Env.t + +val typ_of_mpat : tannot mpat -> typ +val env_of_mpat : tannot mpat -> Env.t + +val typ_of_mpexp : tannot mpexp -> typ +val env_of_mpexp : tannot mpexp -> Env.t + val effect_of : tannot exp -> effect val effect_of_pat : tannot pat -> effect val effect_of_annot : tannot -> effect diff --git a/src/value.ml b/src/value.ml index e9a98160..858a17d9 100644 --- a/src/value.ml +++ b/src/value.ml @@ -183,6 +183,17 @@ let value_eq_string = function | [v1; v2] -> V_bool (Sail_lib.eq_string (coerce_string v1, coerce_string v2)) | _ -> failwith "value eq_string" +let value_string_startswith = function + | [v1; v2] -> V_bool (Sail_lib.string_startswith (coerce_string v1, coerce_string v2)) + | _ -> failwith "value string_startswith" + +let value_string_drop = function + | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2)) + | _ -> failwith "value string_drop" + +let value_string_length = function + | [v] -> V_int (coerce_string v |> Sail_lib.string_length) + | _ -> failwith "value string_length" let value_eq_bit = function | [v1; v2] -> V_bool (Sail_lib.eq_bit (coerce_bit v1, coerce_bit v2)) | _ -> failwith "value eq_bit" @@ -421,6 +432,9 @@ let primops = ("eq_list", value_eq_list); ("eq_bool", value_eq_bool); ("eq_string", value_eq_string); + ("string_startswith", value_string_startswith); + ("string_drop", value_string_drop); + ("string_length", value_string_length); ("eq_bit", value_eq_bit); ("eq_anything", value_eq_anything); ("length", value_length); |