From 248df6a4cf147bd127e11c489e7f17cf65dfb5cb Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Tue, 20 Aug 2013 11:03:33 +0100 Subject: Set some initial kind environments; start pretty printing --- src/initial_check.ml | 75 +++++++++++++++------------- src/pretty_print.ml | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/pretty_print.mli | 4 ++ src/process_file.ml | 2 +- src/type_internal.ml | 8 +++ src/type_internal.mli | 2 + 6 files changed, 190 insertions(+), 36 deletions(-) create mode 100644 src/pretty_print.ml create mode 100644 src/pretty_print.mli (limited to 'src') diff --git a/src/initial_check.ml b/src/initial_check.ml index b6e00400..3b27b840 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -89,7 +89,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ = 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)}) -> Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env k a)) args typs)) + | 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 k a)) args typs)) + else typ_error l "Type constructor given incorrect number of arguments" (Some id) None | None -> typ_error l "Required a type constructor, encountered an unbound variable" (Some id) None | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None) | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None @@ -204,8 +208,9 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain NC_nat_set_bounded(to_ast_id id, bounds) ), l) -let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t = - let opt_kind_to_ast k_env local_names (Parse_ast.KOpt_aux(ki,l)) = +(* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) +let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t = + let opt_kind_to_ast k_env local_names local_env (Parse_ast.KOpt_aux(ki,l)) = let id, key, kind, ktyp = match ki with | Parse_ast.KOpt_none(id) -> @@ -223,42 +228,42 @@ let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant then typ_error l "Encountered duplicate name in type scheme" (Some id) None else let local_names = Nameset.add key local_names in - let kopt,k_env = (match kind,ktyp with - | Some(k),Some(kt) -> KOpt_kind(k,id), (Envmap.insert k_env (key,kt)) - | None, Some(kt) -> KOpt_none(id), (Envmap.insert k_env (key,kt)) - | _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom true but apply gives None")) in - KOpt_aux(kopt,l),k_env,local_names + let kopt,k_env,k_env_local = (match kind,ktyp with + | Some(k),Some(kt) -> KOpt_kind(k,id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) + | None, Some(kt) -> KOpt_none(id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) + | _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in + KOpt_aux(kopt,l),k_env,local_names,local_env in match tq with | Parse_ast.TypQ_aux(tqa,l) -> (match tqa with - | Parse_ast.TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env + | Parse_ast.TypQ_no_forall -> TypQ_aux(TypQ_no_forall,l), k_env, Envmap.empty | Parse_ast.TypQ_tq(qlist) -> - let rec to_ast_q_items k_env local_names = function - | [] -> [],k_env + let rec to_ast_q_items k_env local_names local_env = function + | [] -> [],k_env,local_env | q::qs -> (match q with | Parse_ast.QI_aux(qi,l) -> (match qi with | Parse_ast.QI_const(n_const) -> let c = QI_aux(QI_const(to_ast_nexp_constraint k_env n_const),l) in - let qis,k_env = to_ast_q_items k_env local_names qs in - (c::qis),k_env + let qis,k_env,local_env = to_ast_q_items k_env local_names local_env qs in + (c::qis),k_env,local_env | Parse_ast.QI_id(kid) -> - let kid,k_env,local_names = opt_kind_to_ast k_env local_names kid in + let kid,k_env,local_names,local_env = opt_kind_to_ast k_env local_names local_env kid in let c = QI_aux(QI_id(kid),l) in - let qis,k_env = to_ast_q_items k_env local_names qs in - (c::qis),k_env)) + let qis,k_env,local_env = to_ast_q_items k_env local_names local_env qs in + (c::qis),k_env,local_env)) in - let lst,k_env = to_ast_q_items k_env Nameset.empty qlist in - TypQ_aux(TypQ_tq(lst),l), k_env) + let lst,k_env,local_env = to_ast_q_items k_env Nameset.empty Envmap.empty qlist in + TypQ_aux(TypQ_tq(lst),l), k_env, local_env) -let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm * kind Envmap.t = +let to_ast_typschm (k_env : kind Envmap.t) (tschm : Parse_ast.typschm) : Ast.typschm * kind Envmap.t * kind Envmap.t = match tschm with | Parse_ast.TypSchm_aux(ts,l) -> (match ts with | Parse_ast.TypSchm_ts(tquant,t) -> - let tq,k_env = to_ast_typquant k_env tquant in + let tq,k_env,local_env = to_ast_typquant k_env tquant in let typ = to_ast_typ k_env t in - TypSchm_aux(TypSchm_ts(tq,typ),l),k_env) + TypSchm_aux(TypSchm_ts(tq,typ),l),k_env,local_env) let to_ast_lit (Parse_ast.L_aux(lit,l)) : lit = L_aux( @@ -298,7 +303,7 @@ let rec to_ast_letbind (k_env : kind Envmap.t) (Parse_ast.LB_aux(lb,l) : Parse_a LB_aux( (match lb with | Parse_ast.LB_val_explicit(typschm,pat,exp) -> - let typsch, k_env = to_ast_typschm k_env typschm in + let typsch, k_env, _ = to_ast_typschm k_env typschm in LB_val_explicit(typsch,to_ast_pat k_env pat, to_ast_exp k_env exp) | Parse_ast.LB_val_implicit(pat,exp) -> LB_val_implicit(to_ast_pat k_env pat, to_ast_exp k_env exp) @@ -392,7 +397,7 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe let key = id_to_string id in DT_aux(DT_kind(k,id),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env) | Parse_ast.DT_typ(typschm,id) -> - let tps,_ = to_ast_typschm k_env typschm in + let tps,_,_ = to_ast_typschm k_env typschm in DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *) ) @@ -401,7 +406,7 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec | Parse_ast.VS_aux(vs,l) -> (match vs with | Parse_ast.VS_val_spec(ts,id) -> - let typsch,_ = to_ast_typschm k_env ts in + let typsch,_,_ = to_ast_typschm k_env ts in VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)) (*Do names and t_env need updating this pass? *) let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = @@ -426,7 +431,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de | Parse_ast.TD_abbrev(id,name_scm_opt,typschm) -> let id = to_ast_id id in let key = id_to_string id in - let typschm,_ = to_ast_typschm k_env typschm in + let typschm,_,_ = to_ast_typschm k_env typschm in let td_abrv = TD_aux(TD_abbrev(id,to_ast_namescm name_scm_opt,typschm),(l,None)) in let typ = (match typschm with | TypSchm_aux(TypSchm_ts(tq,typ), _) -> @@ -438,7 +443,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de | Parse_ast.TD_record(id,name_scm_opt,typq,fields,_) -> let id = to_ast_id id in let key = id_to_string id in - let typq,k_env = to_ast_typquant k_env typq in + let typq,k_env,_ = to_ast_typquant k_env typq in let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *) let td_rec = TD_aux(TD_record(id,to_ast_namescm name_scm_opt,typq,fields,false),(l,None)) in let typ = (match (typquant_to_quantkinds k_env typq) with @@ -448,7 +453,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de | Parse_ast.TD_variant(id,name_scm_opt,typq,arms,_) -> let id = to_ast_id id in let key = id_to_string id in - let typq,k_env = to_ast_typquant k_env typq in + let typq,k_env,_ = to_ast_typquant k_env typq in let arms = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) arms in (* Add check that all arms have unique names *) let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in let typ = (match (typquant_to_quantkinds k_env typq) with @@ -477,12 +482,12 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt = | Parse_ast.Rec_rec -> Rec_rec ),l) -let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t = +let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t * kind Envmap.t= match tp with | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none") | Parse_ast.Typ_annot_opt_some(tq,typ) -> - let typq,k_env = to_ast_typquant k_env tq in - Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env + let typq,k_env,k_local = to_ast_typquant k_env tq in + Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effects_opt_aux(e,l)) : tannot effects_opt = match e with @@ -496,7 +501,7 @@ let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl let to_ast_fundef (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = match fd with | Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> - let tannot_opt, k_env = to_ast_tannot_opt k_env tannot_opt in + let tannot_opt, k_env,_ = to_ast_tannot_opt k_env 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, t_env)) funcls), (l,None)), (names,k_env,t_env) type def_progress = @@ -540,12 +545,12 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * ((Finished(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*) | Parse_ast.DEF_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> let rec_opt = to_ast_rec rec_opt in - let tannot,k_env' = to_ast_tannot_opt k_env tannot_opt in + let tannot,k_env',k_local = to_ast_tannot_opt k_env 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_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in - (No_def,envs),((id,(partial_def,k_env))::partial_defs) + (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) | Parse_ast.DEF_scattered_funcl(funcl) -> (match funcl with @@ -556,7 +561,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * | Some(d,k) -> (match !d with | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> - let funcl = to_ast_funcl (names,k,t_env) funcl in (* Needs to be a merging of the new type vars added from the back typq and the types seen since then *) + let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false); (No_def,envs),partial_defs | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None @@ -564,7 +569,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * | Parse_ast.DEF_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 typq, k_env',_ = to_ast_typquant k_env typquant in (match (def_in_progress id partial_defs) with | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs diff --git a/src/pretty_print.ml b/src/pretty_print.ml new file mode 100644 index 00000000..400b5f0b --- /dev/null +++ b/src/pretty_print.ml @@ -0,0 +1,135 @@ +open Ast + +let rec list_format (sep : string) (fmt : 'a -> string) (ls : 'a list) : string = + match ls with + | [] -> "" + | [a] -> fmt a + | a::ls -> (fmt a) ^ sep ^ (list_format sep fmt ls) + +let pp_format_id (Id_aux(i,_)) = + match i with + | Id(i) -> i + | DeIid(x) -> "(:" ^ x ")" + +let pp_format_bkind (BK_aux(k,_)) = + match k with + | BK_type -> "Type" + | BK_nat -> "Nat" + | BK_order -> "Order" + | BK_effects -> "Effects" + +let pp_format_kind (K_aux(K_kind(klst),_)) = + list_format " -> " pp_format_bkind klst + +let rec pp_format_typ (Typ_aux(t,_)) = + match t with + | Typ_id(id) -> pp_format_id id + | Typ_wild -> "_" + | Typ_fn(arg,ret,efct) -> (pp_format_typ arg) ^ " -> " ^ + (pp_format_typ ret) ^ " " ^ + (pp_format_effect efct) + | Typ_tup(typs) -> "(" ^ (list_format ", " pp_format_typ args) ^ ")" + | Typ_app(id,args) -> (pp_format_id id) ^ (list_format " " pp_format_typ_arg args) +and pp_format_nexp (Nexp_aux(n,_)) = + match n with + | Nexp_id(id) -> pp_format_id id + | Nexp_constant(i) -> string_of_int i + | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + ^ " (pp_format_nexp n2) ^ ")" + | Nexp_times(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " * " ^ (pp_format_nexp n2) ^ ")" + | Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")" +and pp_format_ord (Ord_aux(o,_)) = + match o with + | Ord_id(id) -> pp_format_id id + | Ord_inc -> "inc" + | Ord_dec -> "dec" +and pp_format_effect (Effects_aux(e,_)) = + match e with + | Effects_var(id) -> "effect " ^ pp_format id + | Effects_set(efcts) -> + if (efcts = []) + then "pure" + else "effect {" ^ + (list_format "," + (fun (Effect_aux(e,l)) -> + match e with + | Effect_rreg -> "rreg" + | Effect_wreg -> "wreg" + | Effect_rmem -> "rmem" + | Effect_wmem -> "wmem" + | Effect_undef -> "undef" + | Effect_unspec -> "unspec" + | Effect_nondet -> "nondet") + efcts) " }" +and pp_format_typ_arg (Typ_arg_aux(t,_)) = + match t with + | Typ_arg_typ(t) -> pp_format_typ t + | Typ_arg_nexp(n) -> pp_format_nexp n + | Typ_arg_order(o) -> pp_format_ord o + | Typ_arg_Efct(e) -> pp_format_effects e + +let pp_format_nexp_constraint (NC_aux(nc,_)) = + match nc with + | NC_fixed(n1,n2) -> pp_format_nexp n1 ^ " = " ^ pp_format_nexp n2 + | NC_bounded_ge(n1,n2) -> pp_format_nexp n1 ^ " >= " ^ pp_format_nexp n2 + | NC_bounded_le(n1,n2) -> pp_format_nexp n1 ^ " <= " ^ pp_format_nexp n2 + | NC_nat_set_bounded(id,bounds) -> + pp_format_id id ^ + " In {" ^ + list_format ", " string_of_int bounds ^ + "}" + +let pp_format_qi (QI_aux(qi,_)) = + match qi with + | QI_const(n_const) -> pp_format_nexp_constraint qi + | QI_id(KOpt_aux(ki,_)) -> + (match ki with + | KOpt_none(id) -> pp_format_id id + | KOpt_kind(k,id) -> pp_format_kind k ^ " " pp_format_id id) + +let pp_format_typquant (TypQ_aux(tq,_)) = + match tq with + | TypQ_no_forall -> "" + | TypQ_tq(qlist) -> + "forall " ^ + (list_format ", " pp_format_qi qlist) ^ + ". " + +let pp_format_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) = + (pp_format_typquant tq) ^ pp_format_typ t + +let pp_format_lit (L_aux(l,_)) = + match l with + | L_unit -> "()" + | L_zero -> "0" + | L_one -> "1" + | L_true -> "true" + | L_false -> "false" + | L_num(i) -> string_of_int i + | L_hex(n) | L_bin(n) -> n + | L_string(s) -> "\"" ^ s "\"" + +let rec pp_format_pat (P_aux(p,l)) = + match p with + | P_lit(lit) -> pp_format_lit lit + | P_wild -> "_" + | P_id(id) -> pp_format_id id + | P_as(pat,id) -> "(" ^ pp_format_pat pat ^ " as " ^ pp_format_id id ^ ")" + | P_typ(typ,pat) -> "<" ^ pp_format_typ typ ^ "> " ^ pp_format_pat pat + | P_app(id,pats) -> pp_format_id id ^ "(" ^ + list_format ", " pp_format_pat pats ^ ")" + | P_record(fpats) -> "{" ^ + list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> + pp_format_id id ^ " = " pp_format_pat fpat) fpats + ^ "}" + | P_vector(pats) -> "[" ^ list_format "; " pp_format_pats pats ^ "]" + | P_vector_indexed(ipats) -> + "[" ^ list_format "; " (fun (i,p) -> string_of_int i ^ " = " pp_format_pat p) ipats ^ "]" + | P_vector_concat(pats) -> + list_format " ^ " pp_format_pats pats + | P_tup(pats) -> "(" ^ (list_format ", " pp_format_pats pats) ^ ")" + | P_list(pats) -> "[|" ^ (list_format "; " pp_format_pats pats) ^ "|]" + + + + +let pp_format_ast defs = assert false diff --git a/src/pretty_print.mli b/src/pretty_print.mli new file mode 100644 index 00000000..54a5555b --- /dev/null +++ b/src/pretty_print.mli @@ -0,0 +1,4 @@ +open Ast +open Type_internal + +val pp_format_ast : tannot defs -> string diff --git a/src/process_file.ml b/src/process_file.ml index d3b5604b..e642baf5 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -70,7 +70,7 @@ let parse_file (f : string) : Parse_ast.defs = raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs = - Initial_check.to_ast Nameset.empty Envmap.empty Envmap.empty defs + Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs (* type instances = Types.instance list Types.Pfmap.t diff --git a/src/type_internal.ml b/src/type_internal.ml index c4d6ecbc..c3258da1 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -64,3 +64,11 @@ type nexp_range = type tannot = (t * nexp_range list) option +let initial_kind_env = + Envmap.from_list [ + ("bool", {k = K_Typ}); + ("nat", {k = K_Typ}); + ("list", {k = K_Lam( [{k = K_Typ}], {k = K_Typ})}); + ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}; {k=K_Ord} ], {k = K_Typ}) }); + ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ) + ] diff --git a/src/type_internal.mli b/src/type_internal.mli index 1857b007..f53ac9dd 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -60,3 +60,5 @@ type nexp_range = | In of Parse_ast.l * nexp * nexp list type tannot = (t * nexp_range list) option + +val initial_kind_env : kind Envmap.t -- cgit v1.2.3