From fb362fcb5671b6f008794d0a7db31b1f2685e413 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 28 Feb 2019 16:28:56 +0000 Subject: Allow user-specified state to be passed through generated C For example: sail -c_extra_params "CPUMIPSState *env" -c_extra_args env would pass a QEMU MIPS cpu state to every non-builtin function call. Also add documentation for each C compilation option in C_backend.mli --- src/c_backend.ml | 27 ++++++++++++++++++++------- src/c_backend.mli | 49 +++++++++++++++++++++++++++++++++++++++++++------ src/sail.ml | 6 ++++++ 3 files changed, 69 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/c_backend.ml b/src/c_backend.ml index a656a097..ab388223 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -71,6 +71,18 @@ let opt_no_main = ref false let opt_memo_cache = ref false let opt_no_rts = ref false let opt_prefix = ref "z" +let opt_extra_params = ref None +let opt_extra_arguments = ref None + +let extra_params () = + match !opt_extra_params with + | Some str -> str ^ ", " + | _ -> "" + +let extra_arguments is_extern = + match !opt_extra_arguments with + | Some str when not is_extern -> str ^ ", " + | _ -> "" (* Optimization flags *) let optimize_primops = ref false @@ -2588,6 +2600,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = | I_funcall (x, extern, f, args) -> let c_args = Util.string_of_list ", " sgen_cval args in let ctyp = clexp_ctyp x in + let is_extern = Env.is_extern f ctx.tc_env "c" || extern in let fname = if Env.is_extern f ctx.tc_env "c" then Env.get_extern f ctx.tc_env "c" @@ -2649,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) else if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) + string (Printf.sprintf " %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args) else - string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) + string (Printf.sprintf " %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args) | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty @@ -2867,7 +2880,7 @@ let codegen_type_def ctx = function in Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty in - string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_function_id ctor_id) (sgen_id id) ctor_args) ^^ hardline + string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline ^^ surround 2 0 lbrace (tuple ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline @@ -3183,9 +3196,9 @@ let codegen_def' ctx = function if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_function_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else (); @@ -3226,12 +3239,12 @@ let codegen_def' ctx = function | None -> assert (is_stack_ctyp ret_ctyp); (if !opt_static then string "static " else empty) - ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string args) ^^ hardline + ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline | Some gs -> assert (not (is_stack_ctyp ret_ctyp)); (if !opt_static then string "static " else empty) ^^ string "void" ^^ space ^^ codegen_function_id id - ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) + ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args) ^^ hardline in function_header diff --git a/src/c_backend.mli b/src/c_backend.mli index e6cc783c..3b26acdf 100644 --- a/src/c_backend.mli +++ b/src/c_backend.mli @@ -53,18 +53,54 @@ open Type_check (** Global compilation options *) +(** Output a dataflow graph for each generated function in Graphviz + (dot) format. *) val opt_debug_flow_graphs : bool ref + +(** Print the ANF and IR representations of a specific function. *) val opt_debug_function : string ref + +(** Instrument generated code to output a trace. opt_smt_trace is WIP + but intended to enable generating traces suitable for concolic + execution with SMT. *) val opt_trace : bool ref val opt_smt_trace : bool ref + +(** Define generated functions as static *) val opt_static : bool ref + +(** Do not generate a main function *) val opt_no_main : bool ref + +(** (WIP) Do not include rts.h (the runtime), and do not generate code + that requires any setup or teardown routines to be run by a runtime + before executing any instruction semantics. *) val opt_no_rts : bool ref + +(** Ordinarily we use plain z-encoding to name-mangle generated Sail + identifiers into a form suitable for C. If opt_prefix is set, then + the "z" which is added on the front of each generated C function + will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would + give sail_my_function rather than zmy_function. *) val opt_prefix : string ref -(** [opt_memo_cache] will store the compiled function definitions in - file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the - original function to be compiled. Enabled using the -memo +(** opt_extra_params and opt_extra_arguments allow additional state to + be threaded through the generated C code by adding an additional + parameter to each function type, and then giving an extra argument + to each function call. For example we could have + + opt_extra_params := Some "CPUMIPSState *env" + opt_extra_arguments := Some "env" + + and every generated function will take a pointer to a QEMU MIPS + processor state, and each function will be passed the env argument + when it is called. *) +val opt_extra_params : string option ref +val opt_extra_arguments : string option ref + +(** (WIP) [opt_memo_cache] will store the compiled function + definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum + of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of the Sail version. This cache can obviously become stale if the C backend changes - it'll load an old version compiled without said @@ -82,13 +118,14 @@ val optimize_experimental : bool ref (** The compilation context. *) type ctx -(** Convert a typ to a IR ctyp *) -val ctyp_of_typ : ctx -> Ast.typ -> ctyp - (** Create a context from a typechecking environment. This environment should be the environment returned by typechecking the full AST. *) val initial_ctx : Env.t -> ctx +(** Convert a typ to a IR ctyp *) +val ctyp_of_typ : ctx -> Ast.typ -> ctyp + + val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit diff --git a/src/sail.ml b/src/sail.ml index 0450c0ca..949663d4 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -145,6 +145,12 @@ let options = Arg.align ([ ( "-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), " prefix generated C functions" ); + ( "-c_extra_params", + Arg.String (fun params -> C_backend.opt_extra_params := Some params), + " generate C functions with additional parameters" ); + ( "-c_extra_args", + Arg.String (fun args -> C_backend.opt_extra_arguments := Some args), + " supply extra argument to every generated C function call" ); ( "-elf", Arg.String (fun elf -> opt_process_elf := Some elf), " process an ELF file so that it can be executed by compiled C code"); -- cgit v1.2.3 From 2fd45fa939ddae7cdb31ee0495e622e6e6a6235f Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 09:55:19 +0000 Subject: Coq: some work on bool simplification This introduces some simplification of informative booleans, but tries too hard to eliminate all of the existentials resulting in difficulties in and/or trees. --- src/pretty_print_coq.ml | 213 ++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 172 insertions(+), 41 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 430eb40d..c4983597 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -350,6 +350,14 @@ match nc1, nc2 with | _, NC_aux (NC_true,_) -> nc1 | _,_ -> nc_and nc1 nc2 +let nice_imp nc1 nc2 = +match nc1, nc2 with +| NC_aux (NC_true,_), _ -> nc2 +| _, NC_aux (NC_true,_) -> nc2 +| NC_aux (NC_false,l), _ -> NC_aux (NC_true,l) +| _, NC_aux (NC_false,_) -> nc_not nc1 +| _,_ -> nc_or (nc_not nc1) nc2 + let nice_iff nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 @@ -370,30 +378,151 @@ let doc_nc_fn id = | "not" -> string "negb" | s -> string s -type ex_atom_bool = ExBool_simple | ExBool_val of bool | ExBool_complex +let merge_bool_count = KBindings.union (fun _ m n -> Some (m+n)) -let non_trivial_ex_atom_bool l kopts nc atom_nc = - let vars = KOptSet.union (kopts_of_constraint nc) (kopts_of_constraint atom_nc) in - let exists = KOptSet.of_list kopts in - if KOptSet.subset vars exists then - let kenv = List.fold_left (fun kenv kopt -> KBindings.add (kopt_kid kopt) (unaux_kind (kopt_kind kopt)) kenv) KBindings.empty kopts in - match Constraint.call_smt l kenv (nc_and nc atom_nc), - Constraint.call_smt l kenv (nc_and nc (nc_not atom_nc)) with - | Sat, Sat -> ExBool_simple - | Sat, Unsat -> ExBool_val true - | Unsat, Sat -> ExBool_val false - | _ -> ExBool_complex - else ExBool_complex - -type ex_kind = ExNone | ExBool | ExGeneral +let rec count_bool_vars (NC_aux (nc,_)) = + let count_arg (A_aux (arg,_)) = + match arg with + | A_bool nc -> count_bool_vars nc + | A_nexp _ | A_typ _ | A_order _ -> KBindings.empty + in + match nc with + | NC_or (nc1,nc2) + | NC_and (nc1,nc2) + -> merge_bool_count (count_bool_vars nc1) (count_bool_vars nc2) + | NC_var kid -> KBindings.singleton kid 1 + | NC_equal _ | NC_bounded_ge _ | NC_bounded_le _ | NC_not_equal _ + | NC_set _ | NC_true | NC_false + -> KBindings.empty + | NC_app (_,args) -> + List.fold_left merge_bool_count KBindings.empty (List.map count_arg args) + +type prop_dir = Implied_by | Implies | Iff + +type atom_bool_prop = + Bool_boring +| Bool_complex of prop_dir * kinded_id list * n_constraint * n_constraint + +let simplify_atom_bool l kopts nc atom_nc = +prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); + let counter = ref 0 in + let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in + let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in + let lin_bool_vars = KBindings.filter (fun kid n -> is_bound kid && n = 1) bool_vars in + let rec simplify (NC_aux (nc,l) as nc_full) = + let is_ex_var news (NC_aux (nc,_)) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> Some kid + | NC_var kid when KidSet.mem kid news -> Some kid + | _ -> None + in + let replace kills vars = + let v = mk_kid ("simp#" ^ string_of_int !counter) in + let kills = KidSet.union kills (KidSet.of_list vars) in + counter := !counter + 1; + KidSet.singleton v, kills, NC_aux (NC_var v,l) + in + match nc with + | NC_or (nc1,nc2) -> begin + let new1, kill1, nc1 = simplify nc1 in + let new2, kill2, nc2 = simplify nc2 in + let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in + match is_ex_var news nc1, is_ex_var news nc2 with + | Some kid1, Some kid2 -> replace kills [kid1;kid2] + | _ -> news, kills, NC_aux (NC_or (nc1,nc2),l) + end + | NC_and (nc1,nc2) -> begin + let new1, kill1, nc1 = simplify nc1 in + let new2, kill2, nc2 = simplify nc2 in + let news, kills = KidSet.union new1 new2, KidSet.union kill1 kill2 in + match is_ex_var news nc1, is_ex_var news nc2 with + | Some kid1, Some kid2 -> replace kills [kid1;kid2] + | _ -> news, kills, NC_aux (NC_and (nc1,nc2),l) + end + | NC_app (Id_aux (Id "not",_) as id,[A_aux (A_bool nc1,al)]) -> begin + let new1, kill1, nc1 = simplify nc1 in + match is_ex_var new1 nc1 with + | Some kid -> replace kill1 [kid] + | None -> new1, kill1, NC_aux (NC_app (id,[A_aux (A_bool nc1,al)]),l) + end + (* We don't currently recurse into general uses of NC_app, but the + "boring" cases we really want to get rid of won't contain + those. *) + | _ -> KidSet.empty, KidSet.empty, nc_full + in + let new_nc, kill_nc, nc = simplify nc in + let new_atom, kill_atom, atom_nc = simplify atom_nc in + let new_kids = KidSet.union new_nc new_atom in + let kill_kids = KidSet.union kill_nc kill_atom in + let rec strip_implied (NC_aux (nc,l) as nc_full) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> None + | NC_var kid when KidSet.mem kid new_kids -> None + | NC_and (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) + | Some nc, None + | None, Some nc -> Some nc + | None, None -> None + end + | NC_or (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) + | _ -> None + end + | _ -> Some nc_full + in + let rec strip_implies (NC_aux (nc,l) as nc_full) = + match nc with + | NC_var kid when KBindings.mem kid lin_bool_vars -> None + | NC_var kid when KidSet.mem kid new_kids -> None + | NC_and (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) + | _ -> None + end + | NC_or (nc1,nc2) -> begin + match strip_implied nc1, strip_implied nc2 with + | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) + | Some nc, None + | None, Some nc -> Some nc + | None, None -> None + end + | _ -> Some nc_full + in + let strip_implied (NC_aux (_,l) as nc) = + Util.option_default (NC_aux (NC_true,l)) (strip_implied nc) + in + let strip_implies (NC_aux (_,l) as nc) = + Util.option_default (NC_aux (NC_true,l)) (strip_implies nc) + in + let kopts = + List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ + List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts + in +prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); + match atom_nc with + | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring + | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring + | NC_aux (NC_and (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implies, kopts, nc, strip_implied nc') + | NC_aux (NC_and (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implies, kopts, nc, strip_implied nc') + | NC_aux (NC_or (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implied_by, kopts, nc, strip_implies nc') + | NC_aux (NC_or (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> + Bool_complex (Implied_by, kopts, nc, strip_implies nc') + | _ -> Bool_complex (Iff, kopts, nc, atom_nc) + + +type ex_kind = ExNone | ExGeneral let classify_ex_type (Typ_aux (t,l) as t0) = match t with | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> ExNone, t1 - | ExBool_val _ -> ExBool, t1 - | ExBool_complex -> ExGeneral, t1 + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> ExNone, t1 + | Bool_complex _ -> ExGeneral, t1 end | Typ_exist (_,_,t1) -> ExGeneral,t1 | _ -> ExNone,t0 @@ -505,12 +634,15 @@ let rec doc_typ_fns ctx = ampersand; doc_arithfact ctx ~exists:(List.map kopt_kid kopts) ?extra:length_constraint_pp nc]) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> string "bool" - | ExBool_val t -> string "Bool(" ^^ if t then string "True)" else string "False)" - | ExBool_complex -> + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> string "bool" + | Bool_complex (dir,kopts,nc,atom_nc) -> let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in + let nc = nice_and + (match dir with + | Implies -> nice_imp (nc_var var) atom_nc + | Implied_by -> nice_imp atom_nc (nc_var var) + | Iff -> nice_iff (nc_var var) atom_nc) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -816,9 +948,9 @@ let is_ctor env id = match Env.lookup_id id env with let is_auto_decomposed_exist env typ = let typ = expand_range_type typ in - match destruct_exist_plain (Env.expand_synonyms env typ) with - | Some (_, _, typ') -> Some typ' - | _ -> None + match classify_ex_type (Env.expand_synonyms env typ) with + | ExGeneral, typ' -> Some typ' + | ExNone, _ -> None (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen @@ -828,6 +960,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty let typ = Env.expand_synonyms env typ in match exists_as_pairs, is_auto_decomposed_exist env typ with | true, Some typ' -> +prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'); let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp @@ -1068,10 +1201,9 @@ let doc_exp, doc_let = match destruct_exist_plain typ with | None -> epp | Some (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> epp - | ExBool_val t -> wrap_parens (string "build_Bool" ^/^ epp) - | ExBool_complex -> wrap_parens (string "build_ex" ^/^ epp) + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> epp + | Bool_complex _ -> wrap_parens (string "build_ex" ^/^ epp) end | Some _ -> wrap_parens (string "build_ex" ^/^ epp) @@ -1088,10 +1220,9 @@ let doc_exp, doc_let = let build_ex, out_typ = match destruct_exist_plain typ' with | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin - match non_trivial_ex_atom_bool l kopts nc atom_nc with - | ExBool_simple -> None, t - | ExBool_val _ -> Some "build_Bool", t - | ExBool_complex -> Some "build_ex", t + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> None, t + | Bool_complex _ -> Some "build_ex", t end | Some (_,_,t) -> Some "build_ex", t | None -> None, typ' @@ -1204,7 +1335,11 @@ let doc_exp, doc_let = | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> let call = doc_id (append_id f "M") in - wrap_parens (hang 2 (flow (break 1) (call :: List.map expY args))) + let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in + let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with + | Some _ -> string "build_ex" ^^ space ^^ parens epp + | None -> epp + in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach#", _) -> @@ -1574,7 +1709,6 @@ let doc_exp, doc_let = | ExNone, ExNone -> epp else match cast_ex with | ExGeneral -> string "build_ex" ^^ space ^^ epp - | ExBool -> string "build_Bool" ^^ space ^^ epp | ExNone -> epp in let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in @@ -1582,11 +1716,9 @@ let doc_exp, doc_let = if effects then match cast_ex, outer_ex with | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp - | ExBool, ExNone -> string "projBool_m" ^^ space ^^ parens epp | _ -> epp else match cast_ex with | ExGeneral -> string "projT1" ^^ space ^^ parens epp - | ExBool -> string "projBool" ^^ space ^^ parens epp | ExNone -> epp in let epp = @@ -1759,7 +1891,7 @@ let doc_exp, doc_let = let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with | ExGeneral, _ -> squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) - | (ExBool | ExNone), _ -> + | ExNone, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] | _ -> @@ -2244,7 +2376,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = let build_ex, ret_typ = replace_atom_return_type ret_typ in let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with | ExGeneral, _ -> Some "build_ex" - | ExBool, _ -> Some "build_Bool" | ExNone, _ -> build_ex in let ids_to_avoid = all_ids pexp in -- cgit v1.2.3 From 78281d7e30a4d59f499895fae2960248d936eaf9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 11:47:46 +0000 Subject: Coq: strip informative bools back to more uniform types Also make pretty printing more keen on line breaking --- src/pretty_print_coq.ml | 106 +++++++++++++++--------------------------------- 1 file changed, 32 insertions(+), 74 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index c4983597..3d2e238d 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -401,7 +401,7 @@ type prop_dir = Implied_by | Implies | Iff type atom_bool_prop = Bool_boring -| Bool_complex of prop_dir * kinded_id list * n_constraint * n_constraint +| Bool_complex of kinded_id list * n_constraint * n_constraint let simplify_atom_bool l kopts nc atom_nc = prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); @@ -454,48 +454,6 @@ prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_o let new_atom, kill_atom, atom_nc = simplify atom_nc in let new_kids = KidSet.union new_nc new_atom in let kill_kids = KidSet.union kill_nc kill_atom in - let rec strip_implied (NC_aux (nc,l) as nc_full) = - match nc with - | NC_var kid when KBindings.mem kid lin_bool_vars -> None - | NC_var kid when KidSet.mem kid new_kids -> None - | NC_and (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) - | Some nc, None - | None, Some nc -> Some nc - | None, None -> None - end - | NC_or (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) - | _ -> None - end - | _ -> Some nc_full - in - let rec strip_implies (NC_aux (nc,l) as nc_full) = - match nc with - | NC_var kid when KBindings.mem kid lin_bool_vars -> None - | NC_var kid when KidSet.mem kid new_kids -> None - | NC_and (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_and (nc1,nc2),l)) - | _ -> None - end - | NC_or (nc1,nc2) -> begin - match strip_implied nc1, strip_implied nc2 with - | Some nc1, Some nc2 -> Some (NC_aux (NC_or (nc1,nc2),l)) - | Some nc, None - | None, Some nc -> Some nc - | None, None -> None - end - | _ -> Some nc_full - in - let strip_implied (NC_aux (_,l) as nc) = - Util.option_default (NC_aux (NC_true,l)) (strip_implied nc) - in - let strip_implies (NC_aux (_,l) as nc) = - Util.option_default (NC_aux (NC_true,l)) (strip_implies nc) - in let kopts = List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts @@ -504,15 +462,7 @@ prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_o match atom_nc with | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring - | NC_aux (NC_and (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implies, kopts, nc, strip_implied nc') - | NC_aux (NC_and (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implies, kopts, nc, strip_implied nc') - | NC_aux (NC_or (NC_aux (NC_var kid,_),nc'),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implied_by, kopts, nc, strip_implies nc') - | NC_aux (NC_or (nc',NC_aux (NC_var kid,_)),_) when KBindings.mem kid lin_bool_vars -> - Bool_complex (Implied_by, kopts, nc, strip_implies nc') - | _ -> Bool_complex (Iff, kopts, nc, atom_nc) + | _ -> Bool_complex (kopts, nc, atom_nc) type ex_kind = ExNone | ExGeneral @@ -571,9 +521,13 @@ let rec doc_typ_fns ctx = | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) -> (string "Z") | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool" - | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool nc,_)]) -> - let tpp = string "Bool" ^^ space ^^ doc_nc_prop ~top:false ctx nc in - if atyp_needed then parens tpp else tpp + | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool atom_nc,_)]) -> + let var = mk_kid "_bool" in (* TODO collision avoid *) + let nc = nice_iff (nc_var var) atom_nc in + braces (separate space + [doc_var ctx var; colon; string "bool"; + ampersand; + doc_arithfact ctx nc]) | Typ_app(id,args) -> let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in if atyp_needed then parens tpp else tpp @@ -636,13 +590,9 @@ let rec doc_typ_fns ctx = | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) -> begin match simplify_atom_bool l kopts nc atom_nc with | Bool_boring -> string "bool" - | Bool_complex (dir,kopts,nc,atom_nc) -> + | Bool_complex (kopts,nc,atom_nc) -> let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_and - (match dir with - | Implies -> nice_imp (nc_var var) atom_nc - | Implied_by -> nice_imp atom_nc (nc_var var) - | Iff -> nice_iff (nc_var var) atom_nc) nc in + let nc = nice_and (nice_iff (nc_var var) atom_nc) nc in braces (separate space [doc_var ctx var; colon; string "bool"; ampersand; @@ -1150,7 +1100,7 @@ let replace_atom_return_type ret_typ = (* For informative booleans tweak the type name so that doc_typ knows that the constraint should be output. *) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) -> - Some "build_Bool", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) + Some "build_ex", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) | _ -> None, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -1246,7 +1196,7 @@ let doc_exp, doc_let = else exp_pp in match build_ex with | Some s -> - let exp_pp = string s ^^ space ^^ exp_pp in + let exp_pp = string s ^/^ exp_pp in if want_parens then parens exp_pp else exp_pp | None -> exp_pp in aux @@ -1335,9 +1285,17 @@ let doc_exp, doc_let = | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> let call = doc_id (append_id f "M") in - let epp = hang 2 (flow (break 1) (call :: List.map expY args)) in + let doc_arg exp = + let epp = expY exp in + match is_auto_decomposed_exist (env_of exp) (typ_of exp) with + | Some _ -> + let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in + parens (string proj ^/^ epp) + | None -> epp + in + let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with - | Some _ -> string "build_ex" ^^ space ^^ parens epp + | Some _ -> string "build_ex_m" ^/^ parens epp | None -> epp in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) @@ -1610,12 +1568,12 @@ let doc_exp, doc_let = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in - let epp = if unpack && not (effectful eff) then string proj_id ^^ space ^^ parens epp else epp in - let epp = if projbool && not (effectful eff) then string "projBool" ^^ space ^^ parens epp else epp in + let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in + let epp = if projbool && not (effectful eff) then string "projT1" ^/^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack - then string "build_ex_m" ^^ space ^^ parens epp + then string "build_ex_m" ^^ break 1 ^^ parens epp else epp in liftR (if aexp_needed then parens (align epp) else epp) @@ -1701,24 +1659,24 @@ let doc_exp, doc_let = otherwise derive the new type from the old one. *) if alpha_equivalent env inner_typ cast_typ then epp - else string "derive_m" ^^ space ^^ epp + else string "derive_m" ^/^ epp | ExGeneral, ExNone -> - string "projT1_m" ^^ space ^^ epp + string "projT1_m" ^/^ epp | ExNone, ExGeneral -> - string "build_ex_m" ^^ space ^^ epp + string "build_ex_m" ^/^ epp | ExNone, ExNone -> epp else match cast_ex with - | ExGeneral -> string "build_ex" ^^ space ^^ epp + | ExGeneral -> string "build_ex" ^/^ epp | ExNone -> epp in let epp = epp ^/^ doc_tannot ctxt (env_of e) effects typ in let epp = if effects then match cast_ex, outer_ex with - | ExGeneral, ExNone -> string "projT1_m" ^^ space ^^ parens epp + | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp | _ -> epp else match cast_ex with - | ExGeneral -> string "projT1" ^^ space ^^ parens epp + | ExGeneral -> string "projT1" ^/^ parens epp | ExNone -> epp in let epp = -- cgit v1.2.3 From a49a5087d0a2aa25f87bf17a1baa71a29e260b72 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Feb 2019 13:47:10 +0000 Subject: Coq: merge tyvars with corresponding variables --- src/pretty_print_coq.ml | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 3d2e238d..1f37ada5 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1278,7 +1278,35 @@ let doc_exp, doc_let = | E_loop _ -> raise (report l __POS__ "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> - let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in + (* TODO: move the context update out of here and use for other binders, too *) + let pat = match leb with LB_aux (LB_val (p,_),_) -> p in + let old_env = env_of_annot (l,annot) in + let new_env = env_of e in + let is_new_binding id = + match Env.lookup_id ~raw:true id old_env with + | Unbound -> true + | _ -> false + in + let new_ids = IdSet.filter is_new_binding (pat_ids pat) in + let merge_new_kids id m = + let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in + debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); + match destruct_numeric typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + begin try + let _ = Env.get_typ_var kid old_env in + debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); + m + with _ -> + debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); + KBindings.add kid id m + end + | _ -> + debug ctxt (lazy (" not suitable type")); + m + in + let new_ctxt = { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } in + let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with -- cgit v1.2.3 From 0bb1456fccfd3914b4ec7a714f3479f665711790 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 21 Feb 2019 14:39:34 +0000 Subject: Turn off some debugging messages --- src/pretty_print_coq.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1f37ada5..c4e4e1c1 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -404,7 +404,7 @@ type atom_bool_prop = | Bool_complex of kinded_id list * n_constraint * n_constraint let simplify_atom_bool l kopts nc atom_nc = -prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); +(*prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*) let counter = ref 0 in let is_bound kid = List.exists (fun kopt -> Kid.compare kid (kopt_kid kopt) == 0) kopts in let bool_vars = merge_bool_count (count_bool_vars nc) (count_bool_vars atom_nc) in @@ -458,7 +458,7 @@ prerr_endline ("simplify " ^ string_of_n_constraint nc ^ " for bool " ^ string_o List.map (fun kid -> mk_kopt K_bool kid) (KidSet.elements new_kids) @ List.filter (fun kopt -> not (KidSet.mem (kopt_kid kopt) kill_kids)) kopts in -prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc); +(*prerr_endline ("now have " ^ string_of_n_constraint nc ^ " for bool " ^ string_of_n_constraint atom_nc);*) match atom_nc with | NC_aux (NC_var kid,_) when KBindings.mem kid lin_bool_vars -> Bool_boring | NC_aux (NC_var kid,_) when KidSet.mem kid new_kids -> Bool_boring @@ -910,7 +910,7 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty let typ = Env.expand_synonyms env typ in match exists_as_pairs, is_auto_decomposed_exist env typ with | true, Some typ' -> -prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ'); +(*prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ');*) let pat_pp = doc_pat ctxt true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp -- cgit v1.2.3 From 9e0a49a8aa56affa8018e5978616fc01521c50dc Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 21 Feb 2019 15:13:58 +0000 Subject: Coq: update tyvar merge information at other binders --- src/pretty_print_coq.ml | 72 +++++++++++++++++++++++++------------------------ 1 file changed, 37 insertions(+), 35 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index c4e4e1c1..2da2b024 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1125,6 +1125,32 @@ let is_prefix s s' = String.length s' >= l && String.sub s' 0 l = s +let merge_new_tyvars ctxt old_env pat new_env = + let is_new_binding id = + match Env.lookup_id ~raw:true id old_env with + | Unbound -> true + | _ -> false + in + let new_ids = IdSet.filter is_new_binding (pat_ids pat) in + let merge_new_kids id m = + let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in + debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); + match destruct_numeric typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + begin try + let _ = Env.get_typ_var kid old_env in + debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); + m + with _ -> + debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); + KBindings.add kid id m + end + | _ -> + debug ctxt (lazy (" not suitable type")); + m + in + { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } + let prefix_recordtype = true let report = Reporting.err_unreachable let doc_exp, doc_let = @@ -1278,34 +1304,8 @@ let doc_exp, doc_let = | E_loop _ -> raise (report l __POS__ "E_loop should have been rewritten before pretty-printing") | E_let(leb,e) -> - (* TODO: move the context update out of here and use for other binders, too *) let pat = match leb with LB_aux (LB_val (p,_),_) -> p in - let old_env = env_of_annot (l,annot) in - let new_env = env_of e in - let is_new_binding id = - match Env.lookup_id ~raw:true id old_env with - | Unbound -> true - | _ -> false - in - let new_ids = IdSet.filter is_new_binding (pat_ids pat) in - let merge_new_kids id m = - let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in - debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); - match destruct_numeric typ with - | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> - begin try - let _ = Env.get_typ_var kid old_env in - debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); - m - with _ -> - debug ctxt (lazy (" adding tyvar mapping " ^ string_of_kid kid ^ " to " ^ string_of_id id)); - KBindings.add kid id m - end - | _ -> - debug ctxt (lazy (" not suitable type")); - m - in - let new_ctxt = { ctxt with kid_id_renames = IdSet.fold merge_new_kids new_ids ctxt.kid_id_renames } in + let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e) in let epp = let_exp ctxt leb ^^ space ^^ string "in" ^^ hardline ^^ top_exp new_ctxt false e in if aexp_needed then parens epp else epp | E_app(f,args) -> @@ -1794,7 +1794,7 @@ let doc_exp, doc_let = let only_integers e = expY e in let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ - (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) (typ_of e)) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_try (e, pexps) -> @@ -1803,7 +1803,7 @@ let doc_exp, doc_let = let epp = (* TODO capture avoidance for __catch_val *) group ((separate space [string try_catch; expY e; string "(fun __catch_val => match __catch_val with "]) ^/^ - (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (env_of_annot (l,annot)) exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp else @@ -1826,11 +1826,12 @@ let doc_exp, doc_let = debug ctxt (lazy ("Internal plet, pattern " ^ string_of_pat pat)); debug ctxt (lazy (" type of e1 " ^ string_of_typ (typ_of e1))) in + let new_ctxt = merge_new_tyvars ctxt (env_of_annot (l,annot)) pat (env_of e2) in match pat, e1, e2 with | (P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _)), (E_aux (E_assert (assert_e1,assert_e2),_)), _ -> let epp = liftR (separate space [string "assert_exp'"; expY assert_e1; expY assert_e2]) in - let epp = infix 0 1 (string ">>= fun _ =>") epp (expN e2) in + let epp = infix 0 1 (string ">>= fun _ =>") epp (top_exp new_ctxt false e2) in if aexp_needed then parens (align epp) else align epp (* Special case because we don't handle variables with nested existentials well yet. TODO: check that id1 is not used in e2' *) @@ -1854,7 +1855,7 @@ let doc_exp, doc_let = separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] in - infix 0 1 middle e1_pp (expN e2') + infix 0 1 middle e1_pp (top_exp new_ctxt false e2') | _ -> let epp = let middle = @@ -1883,7 +1884,7 @@ let doc_exp, doc_let = | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in - infix 0 1 middle (expY e1) (expN e2) + infix 0 1 middle (expY e1) (top_exp new_ctxt false e2) in if aexp_needed then parens (align epp) else epp end @@ -1975,10 +1976,11 @@ let doc_exp, doc_let = else doc_id id in group (doc_op coloneq fname (top_exp ctxt true e)) - and doc_case ctxt typ = function + and doc_case ctxt old_env typ = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) - (group (top_exp ctxt false e))) + let new_ctxt = merge_new_tyvars ctxt old_env pat (env_of e) in + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false false (pat,typ);bigarrow]) + (group (top_exp new_ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting.err_unreachable l __POS__ "guarded pattern expression should have been rewritten before pretty-printing") -- cgit v1.2.3 From 143ae2d39ede6bef3e39e2ec4d407ddfdd281a0c Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 22 Feb 2019 12:22:06 +0000 Subject: Coq: more for informative booleans Make internal_plet produce annotations (with code to replace unusable type variables) Add mappings for bool kids at bindings Add version of and_bool that proves a property --- src/pretty_print_coq.ml | 76 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 68 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 2da2b024..1079d68e 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -477,6 +477,43 @@ let classify_ex_type (Typ_aux (t,l) as t0) = | Typ_exist (_,_,t1) -> ExGeneral,t1 | _ -> ExNone,t0 +(* The AST doesn't generally have enough type annotations for the booleans, + so we attempt to add some (for internal_plet at the moment). This + function helps by checking that the type variables that appear can be + printed for Coq, and attempts to replace them if not. *) +(* TODO: actually check the substitution applies *somewhere* *) +let clean_typ ctxt env typ = + let kids = tyvars_of_typ typ in + let is_equal kid kid' = + prove __POS__ env (nc_eq (nvar kid) (nvar kid')) + in + let check kid subst = + if KidSet.mem kid ctxt.bound_nvars || + KBindings.mem kid ctxt.kid_renames || + KBindings.mem kid ctxt.kid_id_renames + then subst + else + match KidSet.find_first_opt (is_equal kid) ctxt.bound_nvars with + | Some kid' -> KBindings.add kid kid' subst + | None -> + match KBindings.find_first_opt (is_equal kid) ctxt.kid_renames with + | Some (kid',_) -> KBindings.add kid kid' subst + | None -> + match KBindings.find_first_opt (is_equal kid) ctxt.kid_id_renames with + | Some (kid',_) -> KBindings.add kid kid' subst + | None -> + raise Not_found + in + try + let subst = KidSet.fold check kids KBindings.empty in + (* TODO: this is an awful way to do the subsitution! *) + let typ = KBindings.fold (fun kid kid' typ -> subst_kid typ_subst kid kid' typ) subst typ in + Some typ + with Not_found -> + debug ctxt (lazy ("Failed to clean type " ^ string_of_typ typ ^ " under constraints " ^ + Util.string_of_list ", " string_of_n_constraint (Env.get_constraints env))); + None + (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx = (* following the structure of parser for precedence *) @@ -1135,8 +1172,9 @@ let merge_new_tyvars ctxt old_env pat new_env = let merge_new_kids id m = let typ = lvar_typ (Env.lookup_id ~raw:true id new_env) in debug ctxt (lazy (" considering tyvar mapping for " ^ string_of_id id ^ " at type " ^ string_of_typ typ )); - match destruct_numeric typ with - | Some ([],_,Nexp_aux (Nexp_var kid,_)) -> + match destruct_numeric typ, destruct_atom_bool new_env typ with + | Some ([],_,Nexp_aux (Nexp_var kid,_)), _ + | _, Some (NC_aux (NC_var kid,_)) -> begin try let _ = Env.get_typ_var kid old_env in debug ctxt (lazy (" tyvar " ^ string_of_kid kid ^ " already in env")); @@ -1312,20 +1350,22 @@ let doc_exp, doc_let = begin match f with | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> - let call = doc_id (append_id f "M") in + let informative = Util.is_some (is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp)) in + let suffix = if informative then "MP" else "M" in + let call = doc_id (append_id f suffix) in let doc_arg exp = let epp = expY exp in match is_auto_decomposed_exist (env_of exp) (typ_of exp) with | Some _ -> + if informative then epp else let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in parens (string proj ^/^ epp) - | None -> epp + | None -> + if informative then parens (string "build_trivial_ex" ^/^ epp) + else epp in let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in - let epp = match is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp) with - | Some _ -> string "build_ex_m" ^/^ parens epp - | None -> epp - in wrap_parens epp + wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none | Id_aux (Id "foreach#", _) -> @@ -1881,6 +1921,26 @@ let doc_exp, doc_let = | ExNone, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] + | P_aux (P_id id,_) -> + let typ = typ_of e1 in + let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in + let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) typ) with + | ExGeneral, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> + begin match clean_typ ctxt (env_of_pat pat) typ with + | Some typ' -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) + | None -> plain_binder end + | ExNone, typ' -> begin + match typ' with + | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) -> + begin match clean_typ ctxt (env_of_pat pat) typ with + | Some typ' -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) + | None -> plain_binder end + | _ -> plain_binder + end + | _ -> plain_binder + in separate space [string ">>= fun"; binder; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat, typ_of e1); bigarrow] in -- cgit v1.2.3 From f86ce3508a9909032d1168091989b65a796314a6 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 16:47:00 +0000 Subject: Coq: Clean up rich boolean handling in backend Now generates something vaguely sensible for RISC-V, although the solver needs a little work. Adds type annotations around effectful, rich and/or expressions. --- src/pretty_print_coq.ml | 230 ++++++++++++++++++++++-------------------------- 1 file changed, 104 insertions(+), 126 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1079d68e..5dfeb7ba 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -467,52 +467,36 @@ let simplify_atom_bool l kopts nc atom_nc = type ex_kind = ExNone | ExGeneral -let classify_ex_type (Typ_aux (t,l) as t0) = +(* Should a Sail type be turned into a dependent pair in Coq? + Optionally takes a variable that we're binding (to avoid trivial cases where + the type is exactly the boolean we're binding), and whether to turn bools + with interesting type-expressions into dependent pairs. *) +let classify_ex_type ctxt env ?binding ?(rawbools=false) (Typ_aux (t,l) as t0) = + let is_binding kid = + match binding, KBindings.find_opt kid ctxt.kid_id_renames with + | Some id, Some id' when Id.compare id id' == 0 -> true + | _ -> false + in + let simplify_atom_bool l kopts nc atom_nc = + match simplify_atom_bool l kopts nc atom_nc with + | Bool_boring -> Bool_boring + | Bool_complex (_,_,NC_aux (NC_var kid,_)) when is_binding kid -> Bool_boring + | Bool_complex (x,y,z) -> Bool_complex (x,y,z) + in match t with - | Typ_exist (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_) as t1)) -> begin + | Typ_exist (kopts,nc,Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),_)) -> begin match simplify_atom_bool l kopts nc atom_nc with - | Bool_boring -> ExNone, t1 - | Bool_complex _ -> ExGeneral, t1 + | Bool_boring -> ExNone, [], bool_typ + | Bool_complex _ -> ExGeneral, [], bool_typ end - | Typ_exist (_,_,t1) -> ExGeneral,t1 - | _ -> ExNone,t0 - -(* The AST doesn't generally have enough type annotations for the booleans, - so we attempt to add some (for internal_plet at the moment). This - function helps by checking that the type variables that appear can be - printed for Coq, and attempts to replace them if not. *) -(* TODO: actually check the substitution applies *somewhere* *) -let clean_typ ctxt env typ = - let kids = tyvars_of_typ typ in - let is_equal kid kid' = - prove __POS__ env (nc_eq (nvar kid) (nvar kid')) - in - let check kid subst = - if KidSet.mem kid ctxt.bound_nvars || - KBindings.mem kid ctxt.kid_renames || - KBindings.mem kid ctxt.kid_id_renames - then subst - else - match KidSet.find_first_opt (is_equal kid) ctxt.bound_nvars with - | Some kid' -> KBindings.add kid kid' subst - | None -> - match KBindings.find_first_opt (is_equal kid) ctxt.kid_renames with - | Some (kid',_) -> KBindings.add kid kid' subst - | None -> - match KBindings.find_first_opt (is_equal kid) ctxt.kid_id_renames with - | Some (kid',_) -> KBindings.add kid kid' subst - | None -> - raise Not_found - in - try - let subst = KidSet.fold check kids KBindings.empty in - (* TODO: this is an awful way to do the subsitution! *) - let typ = KBindings.fold (fun kid kid' typ -> subst_kid typ_subst kid kid' typ) subst typ in - Some typ - with Not_found -> - debug ctxt (lazy ("Failed to clean type " ^ string_of_typ typ ^ " under constraints " ^ - Util.string_of_list ", " string_of_n_constraint (Env.get_constraints env))); - None + | Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]) -> begin + match rawbools, simplify_atom_bool l [] nc_true atom_nc with + | false, _ -> ExNone, [], bool_typ + | _,Bool_boring -> ExNone, [], bool_typ + | _,Bool_complex _ -> ExGeneral, [], bool_typ + end + | Typ_exist (kopts,_,t1) -> ExGeneral,kopts,t1 + | _ -> ExNone,[],t0 (* When making changes here, check whether they affect coq_nvars_of_typ *) let rec doc_typ_fns ctx = @@ -557,14 +541,17 @@ let rec doc_typ_fns ctx = (string "Z") | Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) -> (string "Z") - | Typ_app(Id_aux (Id "atom_bool", _), [_]) -> string "bool" - | Typ_app (Id_aux (Id "atom#bool",_), [A_aux (A_bool atom_nc,_)]) -> - let var = mk_kid "_bool" in (* TODO collision avoid *) - let nc = nice_iff (nc_var var) atom_nc in - braces (separate space - [doc_var ctx var; colon; string "bool"; - ampersand; - doc_arithfact ctx nc]) + | Typ_app(Id_aux (Id "atom_bool", _), [A_aux (A_bool atom_nc,_)]) -> + begin match simplify_atom_bool l [] nc_true atom_nc with + | Bool_boring -> string "bool" + | Bool_complex (_,_,atom_nc) -> (* simplify won't introduce new kopts *) + let var = mk_kid "_bool" in (* TODO collision avoid *) + let nc = nice_iff (nc_var var) atom_nc in + braces (separate space + [doc_var ctx var; colon; string "bool"; + ampersand; + doc_arithfact ctx nc]) + end | Typ_app(id,args) -> let tpp = (doc_id_type id) ^^ space ^^ (separate_map space doc_typ_arg args) in if atyp_needed then parens tpp else tpp @@ -933,11 +920,11 @@ let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false -let is_auto_decomposed_exist env typ = +let is_auto_decomposed_exist ctxt env ?(rawbools=false) typ = let typ = expand_range_type typ in - match classify_ex_type (Env.expand_synonyms env typ) with - | ExGeneral, typ' -> Some typ' - | ExNone, _ -> None + match classify_ex_type ctxt env ~rawbools (Env.expand_synonyms env typ) with + | ExGeneral, kopts, typ' -> Some (kopts, typ') + | ExNone, _, _ -> None (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen @@ -945,10 +932,11 @@ let is_auto_decomposed_exist env typ = let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, typ) = let env = env_of_annot (l,annot) in let typ = Env.expand_synonyms env typ in - match exists_as_pairs, is_auto_decomposed_exist env typ with - | true, Some typ' -> -(*prerr_endline ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ');*) - let pat_pp = doc_pat ctxt true true (pat, typ') in + match exists_as_pairs, is_auto_decomposed_exist ctxt env typ with + | true, Some (kopts,typ') -> + debug ctxt (lazy ("decomposing for pattern " ^ string_of_pat pat ^ " at type " ^ string_of_typ typ ^ " with internal type " ^ string_of_typ typ')); + let ctxt' = { ctxt with bound_nvars = List.fold_left (fun s kopt -> KidSet.add (kopt_kid kopt) s) ctxt.bound_nvars kopts } in + let pat_pp = doc_pat ctxt' true true (pat, typ') in let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in if apat_needed then parens pat_pp else pat_pp | _ -> @@ -1134,10 +1122,8 @@ let replace_atom_return_type ret_typ = | Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) Some "build_ex", Typ_aux (Typ_exist ([mk_kopt K_int kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l) - (* For informative booleans tweak the type name so that doc_typ knows that the - constraint should be output. *) | Typ_aux (Typ_app (Id_aux (Id "atom_bool",il), ([A_aux (A_bool _,_)] as args)),l) -> - Some "build_ex", Typ_aux (Typ_app (Id_aux (Id "atom#bool",il), args),l) + Some "build_ex", ret_typ | _ -> None, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -1222,7 +1208,7 @@ let doc_exp, doc_let = | Some _ -> wrap_parens (string "build_ex" ^/^ epp) in - let rec construct_dep_pairs env = + let construct_dep_pairs ?(rawbools=false) env = let rec aux want_parens (E_aux (e,_) as exp) (Typ_aux (t,_) as typ) = match e,t with | E_tuple exps, Typ_tup typs @@ -1231,15 +1217,11 @@ let doc_exp, doc_let = parens (separate (string ", ") (List.map2 (aux false) exps typs)) | _ -> let typ' = expand_range_type (Env.expand_synonyms (env_of exp) typ) in + debug ctxt (lazy ("Constructing " ^ string_of_exp exp ^ " at type " ^ string_of_typ typ)); let build_ex, out_typ = - match destruct_exist_plain typ' with - | Some (kopts,nc,(Typ_aux (Typ_app (Id_aux (Id "atom_bool",_), [A_aux (A_bool atom_nc,_)]),l) as t)) -> begin - match simplify_atom_bool l kopts nc atom_nc with - | Bool_boring -> None, t - | Bool_complex _ -> Some "build_ex", t - end - | Some (_,_,t) -> Some "build_ex", t - | None -> None, typ' + match classify_ex_type ctxt (env_of exp) ~rawbools typ' with + | ExNone, _, _ -> None, typ' + | ExGeneral, _, typ' -> Some "build_ex", typ' in let in_typ = expand_range_type (Env.expand_synonyms (env_of exp) (typ_of exp)) in let in_typ = match destruct_exist_plain in_typ with Some (_,_,t) -> t | None -> in_typ in @@ -1350,14 +1332,14 @@ let doc_exp, doc_let = begin match f with | Id_aux (Id "and_bool", _) | Id_aux (Id "or_bool", _) when effectful (effect_of full_exp) -> - let informative = Util.is_some (is_auto_decomposed_exist (env_of full_exp) (typ_of full_exp)) in + let informative = Util.is_some (is_auto_decomposed_exist ctxt (env_of full_exp) (general_typ_of full_exp)) in let suffix = if informative then "MP" else "M" in let call = doc_id (append_id f suffix) in let doc_arg exp = let epp = expY exp in - match is_auto_decomposed_exist (env_of exp) (typ_of exp) with + match is_auto_decomposed_exist ctxt (env_of exp) ~rawbools:true (general_typ_of exp) with | Some _ -> - if informative then epp else + if informative then parens (epp ^^ doc_tannot ctxt (env_of exp) true (general_typ_of exp)) else let proj = if effectful (effect_of exp) then "projT1_m" else "projT1" in parens (string proj ^/^ epp) | None -> @@ -1365,6 +1347,7 @@ let doc_exp, doc_let = else epp in let epp = hang 2 (flow (break 1) (call :: List.map doc_arg args)) in + let epp = if informative then epp ^^ doc_tannot ctxt (env_of full_exp) true (general_typ_of full_exp) else epp in wrap_parens epp (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux (Id "None", _) as none -> doc_id_ctor none @@ -1596,21 +1579,22 @@ let doc_exp, doc_let = let ret_typ_inst = subst_unifiers inst ret_typ in - let packeff,unpack,autocast,projbool = + let packeff,unpack,autocast = let ann_typ = Env.expand_synonyms env (general_typ_of_annot (l,annot)) in let ann_typ = expand_range_type ann_typ in let ret_typ_inst = expand_range_type (Env.expand_synonyms env ret_typ_inst) in let ret_typ_inst = if is_no_proof_fn env f then ret_typ_inst else snd (replace_atom_return_type ret_typ_inst) in - let () = + let () = debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst)); debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ)) in let unpack, in_typ = - match ret_typ_inst with - | Typ_aux (Typ_exist (_,_,t1),_) -> true,t1 - | t1 -> false,t1 + if is_no_proof_fn env f then false, ret_typ_inst else + match classify_ex_type ctxt env ~rawbools:true ret_typ_inst with + | ExGeneral, _, t1 -> true,t1 + | ExNone, _, t1 -> false,t1 in let pack,out_typ = match ann_typ with @@ -1625,19 +1609,13 @@ let doc_exp, doc_let = Typ_aux (Typ_app (_,[A_aux (A_nexp n2,_);_;_]),_) -> not (similar_nexps ctxt env n1 n2) | _ -> false - in - let projbool = - match in_typ with - | Typ_aux (Typ_app (Id_aux (Id "atom#bool",_),_),_) -> true - | _ -> false - in pack,unpack,autocast,projbool + in pack,unpack,autocast in let autocast_id, proj_id = if effectful eff then "autocast_m", "projT1_m" else "autocast", "projT1" in let epp = if unpack && not (effectful eff) then string proj_id ^/^ parens epp else epp in - let epp = if projbool && not (effectful eff) then string "projT1" ^/^ parens epp else epp in let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in let epp = if effectful eff && packeff && not unpack @@ -1706,9 +1684,9 @@ let doc_exp, doc_let = debug ctxt (lazy (" on expr of type " ^ string_of_typ inner_typ)); debug ctxt (lazy (" where type expected is " ^ string_of_typ outer_typ)) in - let outer_ex,outer_typ' = classify_ex_type outer_typ in - let cast_ex,cast_typ' = classify_ex_type cast_typ in - let inner_ex,inner_typ' = classify_ex_type inner_typ in + let outer_ex,_,outer_typ' = classify_ex_type ctxt env outer_typ in + let cast_ex,_,cast_typ' = classify_ex_type ctxt env ~rawbools:true cast_typ in + let inner_ex,_,inner_typ' = classify_ex_type ctxt env inner_typ in let autocast = (* Avoid using helper functions which simplify the nexps *) is_bitvector_typ outer_typ' && is_bitvector_typ cast_typ' && @@ -1886,11 +1864,11 @@ let doc_exp, doc_let = let middle = match pat' with | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | _ -> separate space [string ">>= fun"; squote ^^ doc_pat ctxt true true (pat', typ'); bigarrow] @@ -1899,44 +1877,39 @@ let doc_exp, doc_let = | _ -> let epp = let middle = + let env1 = env_of e1 in match pat with | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) (typ_of e1)) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) - when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e1) typ) && not (is_enum (env_of e1) id) -> separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow] | P_aux (P_typ (typ, P_aux (P_id id,_)),_) | P_aux (P_typ (typ, P_aux (P_var (P_aux (P_id id,_),_),_)),_) | P_aux (P_var (P_aux (P_typ (typ, P_aux (P_id id,_)),_),_),_) - when not (is_enum (env_of e1) id) -> + when not (is_enum env1 id) -> let full_typ = (expand_range_type typ) in - let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) full_typ) with - | ExGeneral, _ -> + let binder = match classify_ex_type ctxt env1 (Env.expand_synonyms env1 full_typ) with + | ExGeneral, _, _ -> squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) - | ExNone, _ -> + | ExNone, _, _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) in separate space [string ">>= fun"; binder; bigarrow] | P_aux (P_id id,_) -> let typ = typ_of e1 in let plain_binder = squote ^^ doc_pat ctxt true true (pat, typ_of e1) in - let binder = match classify_ex_type (Env.expand_synonyms (env_of e1) typ) with - | ExGeneral, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> - begin match clean_typ ctxt (env_of_pat pat) typ with - | Some typ' -> - squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) - | None -> plain_binder end - | ExNone, typ' -> begin + let binder = match classify_ex_type ctxt env1 ~binding:id (Env.expand_synonyms env1 typ) with + | ExGeneral, _, (Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) as typ') -> + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) + | ExNone, _, typ' -> begin match typ' with | Typ_aux (Typ_app (Id_aux (Id "atom_bool",_),_),_) -> - begin match clean_typ ctxt (env_of_pat pat) typ with - | Some typ' -> - squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ']) - | None -> plain_binder end + squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ]) | _ -> plain_binder end | _ -> plain_binder @@ -1958,7 +1931,7 @@ let doc_exp, doc_let = in let valpp = let env = env_of e1 in - construct_dep_pairs env true e1 ret_typ + construct_dep_pairs env true e1 ret_typ ~rawbools:true in wrap_parens (align (separate space [string "returnm"; valpp])) | E_sizeof nexp -> @@ -2009,13 +1982,13 @@ let doc_exp, doc_let = (* Prefer simple lets over patterns, because I've found Coq can struggle to work out return types otherwise *) | LB_val(P_aux (P_id id,_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) (typ_of e)) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; coloneq]) (top_exp ctxt false e) | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e) - when Util.is_none (is_auto_decomposed_exist (env_of e) typ) && + when Util.is_none (is_auto_decomposed_exist ctxt (env_of e) typ) && not (is_enum (env_of e) id) -> prefix 2 1 (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq]) @@ -2298,7 +2271,7 @@ let pat_is_plain_binder env (P_aux (p,_)) = let demote_all_patterns env i (P_aux (p,p_annot) as pat,typ) = match pat_is_plain_binder env pat with | Some id -> - if Util.is_none (is_auto_decomposed_exist env typ) + if Util.is_none (is_auto_decomposed_exist empty_ctxt env typ) then (pat,typ), fun e -> e else (P_aux (P_id id, p_annot),typ), @@ -2421,11 +2394,6 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type") in - let build_ex, ret_typ = replace_atom_return_type ret_typ in - let build_ex = match classify_ex_type (Env.expand_synonyms env (expand_range_type ret_typ)) with - | ExGeneral, _ -> Some "build_ex" - | ExNone, _ -> build_ex - in let ids_to_avoid = all_ids pexp in let bound_kids = tyvars_of_typquant tq in let pat,guard,exp,(l,_) = destruct_pexp pexp in @@ -2447,15 +2415,23 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id | _ -> false, IdSet.empty in - let ctxt = + let ctxt0 = { early_ret = contains_early_return exp; kid_renames = mk_kid_renames ids_to_avoid kids_used; kid_id_renames = kid_to_arg_rename; bound_nvars = bound_kids; - build_at_return = if effectful eff then build_ex else None; + build_at_return = None; (* filled in below *) recursive_ids = recursive_ids; debug = List.mem (string_of_id id) (!opt_debug_on) } in + let build_ex, ret_typ = replace_atom_return_type ret_typ in + let build_ex = match classify_ex_type ctxt0 env (Env.expand_synonyms env (expand_range_type ret_typ)) with + | ExGeneral, _, _ -> Some "build_ex" + | ExNone, _, _ -> build_ex + in + let ctxt = { ctxt0 with + build_at_return = if effectful eff then build_ex else None; + } in let () = debug ctxt (lazy ("Function " ^ string_of_id id)); debug ctxt (lazy (" return type " ^ string_of_typ ret_typ)); @@ -2478,19 +2454,21 @@ let doc_funcl mutrec rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) in match pat_is_plain_binder env pat with - | Some id -> - if Util.is_none (is_auto_decomposed_exist env exp_typ) then - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - else begin + | Some id -> begin + match classify_ex_type ctxt env ~binding:id exp_typ with + | ExNone, _, typ' -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ']) + | ExGeneral, _, _ -> let full_typ = (expand_range_type exp_typ) in match destruct_exist_plain (Env.expand_synonyms env full_typ) with | Some ([kopt], NC_aux (NC_true,_), - Typ_aux (Typ_app (Id_aux (Id "atom",_), + Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool" as tyname),_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 -> - parens (separate space [doc_id id; colon; string "Z"]) + let coqty = if tyname = "atom" then "Z" else "bool" in + parens (separate space [doc_id id; colon; string coqty]) | Some ([kopt], nc, - Typ_aux (Typ_app (Id_aux (Id "atom",_), + Typ_aux (Typ_app (Id_aux (Id ("atom" | "atom_bool"),_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured -> (used_a_pattern := true; -- cgit v1.2.3 From 7503075ef8e9a3698b7bd9c8033ae36a2d0776b9 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 28 Feb 2019 17:54:06 +0000 Subject: Handle implicits in destruct_atom_nexp --- src/type_check.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index 8de4a904..b058d514 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1793,7 +1793,7 @@ and ambiguous_nexp_vars (Nexp_aux (aux, _)) = let destruct_atom_nexp env typ = match Env.expand_synonyms env typ with | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _)]), _) - when string_of_id f = "atom" -> Some n + when string_of_id f = "atom" || string_of_id f = "implicit" -> Some n | Typ_aux (Typ_app (f, [A_aux (A_nexp n, _); A_aux (A_nexp m, _)]), _) when string_of_id f = "range" && nexp_identical n m -> Some n | _ -> None -- cgit v1.2.3 From dfb2ca35204870809730a0feb0ba98c1f45f57ac Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 10:39:37 +0000 Subject: Coq: make iff `iff` Also drop unused implication function --- src/pretty_print_coq.ml | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 5dfeb7ba..d205e46b 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -350,21 +350,14 @@ match nc1, nc2 with | _, NC_aux (NC_true,_) -> nc1 | _,_ -> nc_and nc1 nc2 -let nice_imp nc1 nc2 = -match nc1, nc2 with -| NC_aux (NC_true,_), _ -> nc2 -| _, NC_aux (NC_true,_) -> nc2 -| NC_aux (NC_false,l), _ -> NC_aux (NC_true,l) -| _, NC_aux (NC_false,_) -> nc_not nc1 -| _,_ -> nc_or (nc_not nc1) nc2 - let nice_iff nc1 nc2 = match nc1, nc2 with | NC_aux (NC_true,_), _ -> nc2 | _, NC_aux (NC_true,_) -> nc1 | NC_aux (NC_false,_), _ -> nc_not nc2 | _, NC_aux (NC_false,_) -> nc_not nc1 -| _,_ -> nc_or (nc_and nc1 nc2) (nc_and (nc_not nc1) (nc_not nc2)) + (* TODO: replace this hacky iff with a proper NC_ constructor *) +| _,_ -> mk_nc (NC_app (mk_id "iff",[arg_bool nc1; arg_bool nc2])) (* n_constraint functions are currently just Z3 functions *) let doc_nc_fn_prop id = -- cgit v1.2.3 From 2e835b683c23aa4a63a9d5dac7628b0953be5f24 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 12:14:45 +0000 Subject: Coq tidying: remove old definition, complete a pattern match --- src/pretty_print_coq.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index d205e46b..d323d639 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -390,8 +390,6 @@ let rec count_bool_vars (NC_aux (nc,_)) = | NC_app (_,args) -> List.fold_left merge_bool_count KBindings.empty (List.map count_arg args) -type prop_dir = Implied_by | Implies | Iff - type atom_bool_prop = Bool_boring | Bool_complex of kinded_id list * n_constraint * n_constraint @@ -2746,6 +2744,9 @@ let rec doc_def unimplemented generic_eq_types def = | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" | DEF_pragma _ -> empty + | DEF_measure (id,_,_) -> unreachable (id_loc id) __POS__ + ("Termination measure for " ^ string_of_id id ^ + " should have been rewritten before backend") let find_exc_typ defs = let is_exc_typ_def = function -- cgit v1.2.3 From 6091ce6ef24cb8ab8b65f528f28109dd15b8cb54 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Mar 2019 15:28:56 +0000 Subject: Fill in some edge cases in monomorphisation --- src/monomorphise.ml | 23 ++++++++++++++++++----- 1 file changed, 18 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 784929e1..f0472385 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -344,6 +344,7 @@ and inst_src_typ_arg insts (A_aux (ta,l) as tyarg) = match ta with | A_nexp _ | A_order _ + | A_bool _ -> insts, tyarg | A_typ typ -> let insts', typ' = inst_src_type insts typ in @@ -364,6 +365,7 @@ and contains_exist_arg (A_aux (arg,_)) = match arg with | A_nexp _ | A_order _ + | A_bool _ -> false | A_typ typ -> contains_exist typ @@ -2085,19 +2087,26 @@ let split_defs all_errors splits defs = | LEXP_vector_concat les -> re (LEXP_vector_concat (List.map map_lexp les)) | LEXP_field (le,id) -> re (LEXP_field (map_lexp le, id)) | LEXP_deref e -> re (LEXP_deref (map_exp e)) - in map_pexp, map_letbind - in + in map_exp, map_pexp, map_letbind + in + let map_exp r = let (f,_,_) = map_fns r in f in + let map_pexp r = let (_,f,_) = map_fns r in f in + let map_letbind r = let (_,_,f) = map_fns r in f in + let map_exp exp = + let ref_vars = referenced_vars exp in + map_exp ref_vars exp + in let map_pexp top_pexp = (* Construct the set of referenced variables so that we don't accidentally make false assumptions about them during constant propagation. Note that we assume there aren't any in the guard. *) let (_,_,body,_) = destruct_pexp top_pexp in let ref_vars = referenced_vars body in - fst (map_fns ref_vars) top_pexp + map_pexp ref_vars top_pexp in let map_letbind (LB_aux (LB_val (_,e),_) as lb) = let ref_vars = referenced_vars e in - snd (map_fns ref_vars) lb + map_letbind ref_vars lb in let map_funcl (FCL_aux (FCL_Funcl (id,pexp),annot)) = @@ -2128,6 +2137,7 @@ let split_defs all_errors splits defs = | DEF_mapdef (MD_aux (_, (l, _))) -> Reporting.unreachable l __POS__ "mappings should be gone by now" | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) + | DEF_measure (id,pat,exp) -> [DEF_measure (id,pat,map_exp exp)] in Defs (List.concat (List.map map_def defs)) in @@ -2210,6 +2220,7 @@ and sizes_of_typarg (A_aux (ta,_)) = match ta with A_nexp _ | A_order _ + | A_bool _ -> KidSet.empty | A_typ typ -> sizes_of_typ typ @@ -4380,7 +4391,9 @@ let replace_nexp_in_typ env typ orig new_nexp = | A_typ typ -> let f, typ = aux typ in f, A_aux (A_typ typ,l) - | A_order _ -> false, typ_arg + | A_order _ + | A_bool _ + -> false, typ_arg in aux typ let fresh_nexp_kid nexp = -- cgit v1.2.3 From a8da14a23cd8dfdd5fcc527b930ed553d376d18f Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 1 Mar 2019 15:45:46 +0000 Subject: Make Sail more flexible with existentials in union types Issues came up with Christophers translation of hand-written ARM into Sail2 where we were being overly pedantic about the exact position of existential quantifiers in constructors with multiple arguments. This commit generalises unify_typ and type_coercion_unify to be more flexible and support this. Should think at some point if unify_typ can be generalised further. This fix should fix the decode side of things, but may be some issues with the executes that still need looking into when existentials and multiple argument constructors are mixed. --- src/type_check.ml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/type_check.ml b/src/type_check.ml index b058d514..a2612794 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1304,6 +1304,15 @@ let bind_existential l name typ env = | Some (kids, nc, typ) -> typ, add_existential l kids nc env | None -> typ, env +let bind_tuple_existentials l name (Typ_aux (aux, annot) as typ) env = + match aux with + | Typ_tup typs -> + let typs, env = + List.fold_right (fun typ (typs, env) -> let typ, env = bind_existential l name typ env in typ :: typs, env) typs ([], env) + in + Typ_aux (Typ_tup typs, annot), env + | _ -> typ, env + let destruct_range env typ = let kopts, constr, (Typ_aux (typ_aux, _)) = Util.option_default ([], nc_true, typ) (destruct_exist (Env.expand_synonyms env typ)) @@ -1567,6 +1576,8 @@ let merge_uvars l unifiers1 unifiers2 = KBindings.merge (merge_unifiers l) unifiers1 unifiers2 let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as typ2) = + typ_debug (lazy (Util.("Unify type " |> magenta |> clear) ^ string_of_typ typ1 ^ " and " ^ string_of_typ typ2 + ^ " goals " ^ string_of_list ", " string_of_kid (KidSet.elements goals))); match aux1, aux2 with | Typ_internal_unknown, _ | _, Typ_internal_unknown when Env.allow_unknowns env -> @@ -1577,7 +1588,14 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]), Typ_app (atom, [A_aux (A_nexp m, _)]) when string_of_id range = "range" && string_of_id atom = "atom" -> - merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m) + let n1, n2 = nexp_simp n1, nexp_simp n2 in + begin match n1, n2 with + | Nexp_aux (Nexp_constant c1, _), Nexp_aux (Nexp_constant c2, _) -> + if prove __POS__ env (nc_and (nc_lteq n1 m) (nc_lteq m n2)) then KBindings.empty + else unify_error l (string_of_typ typ1 ^ " is not contained within " ^ string_of_typ typ1) + | _, _ -> + merge_uvars l (unify_nexp l env goals n1 m) (unify_nexp l env goals n2 m) + end | Typ_app (id1, args1), Typ_app (id2, args2) when List.length args1 = List.length args2 && Id.compare id1 id2 = 0 -> List.fold_left (merge_uvars l) KBindings.empty (List.map2 (unify_typ_arg l env goals) args1 args2) @@ -2932,6 +2950,7 @@ and type_coercion_unify env goals (E_aux (_, (l, _)) as annotated_exp) typ = try typ_debug (lazy ("Coercing unification: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); let atyp, env = bind_existential l None (typ_of annotated_exp) env in + let atyp, env = bind_tuple_existentials l None atyp env in annotated_exp, unify l env (KidSet.diff goals (ambiguous_vars typ)) typ atyp, env with | Unification_error (_, m) when Env.allow_casts env -> -- cgit v1.2.3