diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 158 | ||||
| -rw-r--r-- | src/pretty_print.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 12 | ||||
| -rw-r--r-- | src/type_internal.ml | 5 | ||||
| -rw-r--r-- | src/type_internal.mli | 3 |
5 files changed, 155 insertions, 26 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 0da54e53..1515ff00 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -246,38 +246,38 @@ let pp_format_lit_lem (L_aux(lit,l)) = let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l) -let rec pp_format_t t = +let rec pp_format_t_lem t = match t.t with | Tid i -> "(T_id \"" ^ i ^ "\")" | Tvar i -> "(T_var \"" ^ i ^ "\")" - | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")" - | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])" - | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ args ^ "]))" - | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")" + | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t_lem t1) ^ " " ^ (pp_format_t_lem t2) ^ " " ^ pp_format_e_lem e ^ ")" + | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t_lem tups) ^ "])" + | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ_lem args ^ "]))" + | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t_lem ti) ^ " " ^ (pp_format_t_lem ta) ^ ")" | Tuvar(_) -> "(T_var \"fresh_v\")" | Toptions _ -> "(T_var \"fresh_v\")" -and pp_format_targ = function - | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")" - | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")" - | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")" - | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")" -and pp_format_n n = +and pp_format_targ_lem = function + | TA_typ t -> "(T_arg_typ " ^ pp_format_t_lem t ^ ")" + | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n_lem n ^ ")" + | TA_eft e -> "(T_arg_effect " ^ pp_format_e_lem e ^ ")" + | TA_ord o -> "(T_arg_order " ^ pp_format_o_lem o ^ ")" +and pp_format_n_lem n = match n.nexp with | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")" | Nvar i -> "(Ne_var \"" ^ i ^ "\")" | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")" | Npos_inf -> "Ne_inf" - | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])" - | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" - | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" - | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" - | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")" - | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")" + | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n_lem n1) ^ "; " ^ (pp_format_n_lem n2) ^ "])" + | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" + | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" + | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" + | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ ")" + | Nneg n -> "(Ne_unary " ^ (pp_format_n_lem n) ^ ")" | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")" | Nneg_inf -> "(Ne_unary Ne_inf)" | Npow _ -> "power_not_implemented" | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)" -and pp_format_e e = +and pp_format_e_lem e = "(Effect_aux " ^ (match e.effect with | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" @@ -285,7 +285,7 @@ and pp_format_e e = (list_format "; " pp_format_base_effect_lem es) ^ " ])" | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" -and pp_format_o o = +and pp_format_o_lem o = "(Ord_aux " ^ (match o.order with | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" @@ -312,9 +312,9 @@ let rec pp_format_nes nes = "[" ^ (* (list_format "; " (fun ne -> match ne with - | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" + | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" + | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" + | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" | InS(_,_,ns) -> @@ -330,8 +330,8 @@ let pp_format_annot = function | NoTyp -> "Nothing" | Base((_,t),tag,nes,efct,efctsum,_) -> (*TODO print out bindings for use in pattern match in interpreter*) - "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ - pp_format_e efct ^ ", " ^ pp_format_e efctsum ^ "))" + "(Just (" ^ pp_format_t_lem t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ + pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" | Overload _ -> "Nothing" let pp_annot ppf ant = base ppf (pp_format_annot ant) @@ -675,6 +675,116 @@ let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs + +(* ************************************************************************** + * pp from tannot to ASCII source, for pp of built-in type environment +*) + + + +let rec pp_format_t_ascii t = + match t.t with + | Tid i -> i + | Tvar i -> "'" ^ i + | Tfn(t1,t2,_,e) -> (pp_format_t_ascii t1) ^ " -> " ^ (pp_format_t_ascii t2) ^ " effect " ^ pp_format_e_ascii e + | Ttup(tups) -> "(" ^ (list_format ", " pp_format_t_ascii tups) ^ ")" + | Tapp(i,args) -> i ^ "<" ^ list_format ", " pp_format_targ_ascii args ^ ">" + | Tabbrev(ti,ta) -> (pp_format_t_ascii ti) (* (pp_format_t_ascii ta) *) + | Tuvar(_) -> failwith "Tuvar in pp_format_t_ascii" + | Toptions _ -> failwith "Toptions in pp_format_t_ascii" +and pp_format_targ_ascii = function + | TA_typ t -> pp_format_t_ascii t + | TA_nexp n -> pp_format_n_ascii n + | TA_eft e -> pp_format_e_ascii e + | TA_ord o -> pp_format_o_ascii o +and pp_format_n_ascii n = + match n.nexp with + | Nid (i, n) -> i (* from an abbreviation *) + | Nvar i -> "'" ^ i + | Nconst i -> (string_of_int (int_of_big_int i)) + | Npos_inf -> "infinity" + | Nadd(n1,n2) -> (pp_format_n_ascii n1) ^ "+" ^ (pp_format_n_ascii n2) + | Nsub(n1,n2) -> (pp_format_n_ascii n1) ^ "-" ^ (pp_format_n_ascii n2) + | Nmult(n1,n2) -> (pp_format_n_ascii n1) ^ "*" ^ (pp_format_n_ascii n2) + | N2n(n,_) -> "2**"^(pp_format_n_ascii n) (* string_of_big_int i ^ *) + | Nneg n -> "-" ^ (pp_format_n_ascii n) + | Nuvar _ -> failwith "Nuvar in pp_format_n_ascii" + | Nneg_inf -> "-infinity" + | Npow _ -> failwith "Npow in pp_format_n_ascii" + | Ninexact -> failwith "Ninexact in pp_format_n_ascii" +and pp_format_e_ascii e = + match e.effect with + | Evar i -> "'" ^ i + | Eset es -> "{" ^ + (list_format ", " pp_format_base_effect_ascii es) ^ "}" + | Euvar(_) -> failwith "Euvar in pp_format_e_ascii" +and pp_format_o_ascii o = + match o.order with + | Ovar i -> "'" ^ i + | Oinc -> "inc" + | Odec -> "dec" + | Ouvar(_) -> failwith "Ouvar in pp_format_o_ascii" +and pp_format_base_effect_ascii (BE_aux(e,l)) = + match e with + | BE_rreg -> "rreg" + | BE_wreg -> "wreg" + | BE_rmem -> "rmem" + | BE_wmem -> "wmem" + | BE_wmv -> "wmv" + | BE_eamem -> "eamem" + | BE_barr -> "barr" + | BE_depend -> "depend" + | BE_undef -> "undef" + | BE_unspec -> "unspec" + | BE_nondet -> "nondet" + | BE_lset -> "lset" + | BE_lret -> "lret" + | BE_escape -> "escape" + +and pp_format_nes_ascii nes = + list_format ", " pp_format_ne_ascii nes + +and pp_format_ne_ascii ne = + match ne with + | Lt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " < " ^ pp_format_n_ascii n2 + | LtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " <= " ^ pp_format_n_ascii n2 + | NtEq(_,n1,n2) -> pp_format_n_ascii n1 ^ " != " ^ pp_format_n_ascii n2 + | Eq(_,n1,n2) -> pp_format_n_ascii n1 ^ " = " ^ pp_format_n_ascii n2 + | GtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " >= " ^ pp_format_n_ascii n2 + | Gt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " > " ^ pp_format_n_ascii n2 + | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> + i ^ " IN {" ^ (list_format ", " string_of_int ns)^ "}" + | InS(_,_,ns) -> (* when the variable has been replaced by a unification variable, we use this *) + failwith "InS in pp_format_nes_ascii" (*"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"*) + | Predicate(_,n1,n2) -> "flow_constraints(" ^ pp_format_ne_ascii n1 ^", "^ pp_format_ne_ascii n2 ^")" + | CondCons(_,_,_,nes_c,nes_t) -> + failwith "CondCons in pp_format_nes_ascii" (*"(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"*) + | BranchCons(_,_,nes_b) -> + failwith "BranchCons in pp_format_nes_ascii" (*"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"*) + + + +let rec pp_format_annot_ascii = function + | NoTyp -> "Nothing" + | Base((targs,t),tag,nes,efct,efctsum,_) -> + (*TODO print out bindings for use in pattern match in interpreter*) + "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" "^ i) targs ^ + (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes) + ^ ". " + ^ pp_format_t_ascii t + +(* +^ " ********** " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ + pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" +*) + | Overload (tannot, return_type_overloading_allowed, tannots) -> + pp_format_annot_ascii tannot ^ "\n" ^ String.concat "" (List.map (function tannot' -> " " ^ pp_format_annot_ascii tannot' ^ "\n") tannots) + + + + + + (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 500d19e2..aa924383 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -11,3 +11,6 @@ val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit + + +val pp_format_annot_ascii : tannot -> string diff --git a/src/sail.ml b/src/sail.ml index 80560746..eeaea04e 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -104,6 +104,18 @@ let main() = if !(opt_print_version) then Printf.printf "Sail private release \n" else + let ppd_initial_typ_env = + String.concat "" + (List.map + (function (id,tannot) -> + id ^ " : " ^ + Pretty_print.pp_format_annot_ascii tannot + ^ "\n") + (Type_internal.Envmap.to_list Type_internal.initial_typ_env)) in + Printf.printf "%s" ppd_initial_typ_env ; + + + let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in let ast = List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) diff --git a/src/type_internal.ml b/src/type_internal.ml index 2770d827..56c84e31 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -200,7 +200,7 @@ type tannot = (*See .mli for purpose of attributes *) | Base of (t_params * t) * tag * nexp_range list * effect * effect * bounds_env (* First tannot is the most polymorphic version; the list includes all variants. All included t are Tfn *) - | Overload of tannot * bool * tannot list + | Overload of tannot * bool * tannot list (* these tannot's should all be Base *) type 'a emap = 'a Envmap.t @@ -1954,7 +1954,7 @@ let mk_bitwise_op name symb arity = (*lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg single_bit_vec_typ) (Some name) [];*) lib_tannot ([],mk_pure_fun barg bit_t) (Some (name ^ "_bit")) []])) -let initial_typ_env = +let initial_typ_env : tannot Envmap.t = Envmap.from_list [ ("ignore",lib_tannot ([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t) None []); ("Some", Base((["a",{k=K_Typ}], mk_pure_fun {t=Tvar "a"} {t=Tapp("option", [TA_typ {t=Tvar "a"}])}), @@ -2703,6 +2703,7 @@ let initial_typ_env = (mk_atom (mk_nv "o")))), External (Some "min"),[],pure_e,pure_e,nob)); ] + let rec typ_subst s_env leave_imp t = diff --git a/src/type_internal.mli b/src/type_internal.mli index b55418fe..e45796a4 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -337,3 +337,6 @@ val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool -> When merging atoms, use bool to control widening. *) val tannot_merge : constraint_origin -> def_envs -> bool -> tannot -> tannot -> tannot + +val initial_typ_env : tannot Envmap.t + |