diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/initial_check.ml | 8 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 8 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 172 | ||||
| -rw-r--r-- | src/rewriter.ml | 9 | ||||
| -rw-r--r-- | src/rewrites.ml | 156 | ||||
| -rw-r--r-- | src/type_check.ml | 10 |
7 files changed, 315 insertions, 49 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 61cde224..8730d909 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -559,10 +559,12 @@ let to_ast_kdef ctx (td:P.kind_def) : unit kind_def = let kind = to_ast_kind kind in KD_aux (KD_nabbrev (kind, id, to_ast_namescm name_scm_opt, to_ast_nexp ctx atyp), (l, ())) -let to_ast_rec (P.Rec_aux(r,l): P.rec_opt) : rec_opt = +let to_ast_rec ctx (P.Rec_aux(r,l): P.rec_opt) : unit rec_opt = Rec_aux((match r with | P.Rec_nonrec -> Rec_nonrec | P.Rec_rec -> Rec_rec + | P.Rec_measure (p,e) -> + Rec_measure (to_ast_pat ctx p, to_ast_exp ctx e) ),l) let to_ast_tannot_opt ctx (P.Typ_annot_opt_aux(tp,l)) : tannot_opt ctx_out = @@ -595,7 +597,7 @@ let to_ast_fundef ctx (P.FD_aux(fd,l):P.fundef) : unit fundef = match fd with | P.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> let tannot_opt, ctx = to_ast_tannot_opt ctx tannot_opt in - FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt effects_opt, List.map (to_ast_funcl ctx) funcls), (l,())) + FD_aux(FD_function(to_ast_rec ctx rec_opt, tannot_opt, to_ast_effects_opt effects_opt, List.map (to_ast_funcl ctx) funcls), (l,())) let rec to_ast_mpat ctx (P.MP_aux(mpat,l)) = MP_aux( @@ -669,7 +671,7 @@ let to_ast_scattered ctx (P.SD_aux (aux, l)) = | P.SD_function (rec_opt, tannot_opt, effect_opt, id) -> let tannot_opt, _ = to_ast_tannot_opt ctx tannot_opt in let effect_opt = to_ast_effects_opt effect_opt in - SD_function (to_ast_rec rec_opt, tannot_opt, effect_opt, to_ast_id id), ctx + SD_function (to_ast_rec ctx rec_opt, tannot_opt, effect_opt, to_ast_id id), ctx | P.SD_funcl funcl -> SD_funcl (to_ast_funcl ctx funcl), ctx | P.SD_variant (id, namescm_opt, typq) -> diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 9b855837..65b11373 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -330,6 +330,7 @@ type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) + | Rec_measure of pat * exp (* recursive with termination measure *) type diff --git a/src/parser.mly b/src/parser.mly index 1957d7fd..6344db97 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -127,6 +127,8 @@ let doc_vs doc (VS_aux (v, l)) = VS_aux (v, Documented (doc, l)) let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l) +let mk_recr r n m = (Rec_aux(r, loc n m)) + let mk_recn = (Rec_aux((Rec_nonrec), Unknown)) let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown)) let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) @@ -1232,9 +1234,15 @@ type_unions: | type_union Comma type_unions { $1 :: $3 } +rec_measure: + | Lcurly pat EqGt exp Rcurly + { mk_recr (Rec_measure ($2, $4)) $startpos $endpos } + fun_def: | Function_ funcls { let funcls, tannot = $2 in mk_fun (FD_function (mk_recn, tannot, mk_eannotn, funcls)) $startpos $endpos } + | Function_ rec_measure funcls + { let funcls, tannot = $3 in mk_fun (FD_function ($2, tannot, mk_eannotn, funcls)) $startpos $endpos } fun_def_list: | fun_def diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 35aa9e20..053020db 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -71,6 +71,7 @@ type context = { kid_id_renames : id KBindings.t; (* tyvar -> argument renames *) bound_nvars : KidSet.t; build_ex_return : bool; + recursive_ids : IdSet.t; debug : bool; } let empty_ctxt = { @@ -79,6 +80,7 @@ let empty_ctxt = { kid_id_renames = KBindings.empty; bound_nvars = KidSet.empty; build_ex_return = false; + recursive_ids = IdSet.empty; debug = false; } @@ -605,11 +607,29 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) = end | QI_const nc -> None +let quant_item_id_name ctx (QI_aux (qi,_)) = + match qi with + | QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin + if KBindings.mem kid ctx.kid_id_renames then None else + match kind with + | K_type -> Some (doc_var ctx kid) + | K_int -> Some (doc_var ctx kid) + | K_order -> None + end + | QI_const nc -> None + let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) = match qi with | QI_id _ -> None | QI_const nc -> Some (bquote ^^ braces (doc_arithfact ctx nc)) +(* At the moment these are all anonymous - when used we rely on Coq to fill + them in. *) +let quant_item_constr_name ctx (QI_aux (qi,_)) = + match qi with + | QI_id _ -> None + | QI_const nc -> Some underscore + let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = match tq with | TypQ_tq qis -> @@ -624,6 +644,14 @@ let doc_typquant_items_separate ctx delimit (TypQ_aux (tq,_)) = Util.map_filter (doc_quant_item_constr ctx delimit) qis | TypQ_no_forall -> [], [] +let typquant_names_separate ctx (TypQ_aux (tq,_)) = + match tq with + | TypQ_tq qis -> + Util.map_filter (quant_item_id_name ctx) qis, + Util.map_filter (quant_item_constr_name ctx) qis + | TypQ_no_forall -> [], [] + + let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with | TypQ_tq ((_ :: _) as qs) -> string "forall " ^^ separate_opt space (doc_quant_item_id ctx braces) qs ^/^ @@ -879,6 +907,11 @@ let general_typ_of_annot annot = let general_typ_of (E_aux (_,annot)) = general_typ_of_annot annot +let is_prefix s s' = + let l = String.length s in + String.length s' >= l && + String.sub s' 0 l = s + let prefix_recordtype = true let report = Reporting.err_unreachable let doc_exp, doc_let = @@ -1142,11 +1175,13 @@ let doc_exp, doc_let = | _ -> let env = env_of_annot (l,annot) in let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in - let call, is_extern, is_ctor = - if Env.is_union_constructor f env then doc_id_ctor f, false, true else + let call, is_extern, is_ctor, is_rec = + if Env.is_union_constructor f env then doc_id_ctor f, false, true, false else if Env.is_extern f env "coq" - then string (Env.get_extern f env "coq"), true, false - else doc_id f, false, false in + then string (Env.get_extern f env "coq"), true, false, false + else if IdSet.mem f ctxt.recursive_ids + then doc_id f, false, false, true + else doc_id f, false, false, false in let (tqs,fn_ty) = Env.get_val_spec_orig f env in let arg_typs, ret_typ, eff = match fn_ty with | Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff @@ -1198,7 +1233,16 @@ let doc_exp, doc_let = let epp = if is_ctor then hang 2 (call ^^ break 1 ^^ parens (flow (comma ^^ break 1) (List.map2 (doc_arg false) args arg_typs))) - else hang 2 (flow (break 1) (call :: List.map2 (doc_arg true) args arg_typs)) in + else + let main_call = call :: List.map2 (doc_arg true) args arg_typs in + let all = + if is_rec then main_call @ + [parens (string "_limit_reduces _acc")] + else match f with + | Id_aux (Id x,_) when is_prefix "#rec#" x -> + main_call @ [parens (string "Zwf_well_founded _ _")] + | _ -> main_call + in hang 2 (flow (break 1) all) in (* Decide whether to unpack an existential result, pack one, or cast. To do this we compare the expected type stored in the checked expression @@ -1821,6 +1865,12 @@ let args_of_typ l env typs = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in List.split (List.mapi arg typs) +(* Sail currently has a single pattern to match against a list of + argument types. We need to tweak everything to match up, + especially so that the function is presented in curried form. In + particular, if there's a single binder for multiple arguments + (which rewriting can currently introduce) then we need to turn it + into multiple binders and reconstruct it in the function body. *) let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) = let env = env_of_annot annot in let identity = (fun body -> body) in @@ -1844,10 +1894,6 @@ let rec untuple_args_pat typs (P_aux (paux, ((l, _) as annot)) as pat) = | _, _ -> unreachable l __POS__ "Unexpected pattern/type combination" -let doc_rec (Rec_aux(r,_)) = match r with - | Rec_nonrec -> string "Definition" - | Rec_rec -> string "Fixpoint" - let doc_fun_body ctxt exp = let doc_exp = doc_exp ctxt false exp in if ctxt.early_ret @@ -1866,6 +1912,28 @@ let demote_as_pattern i (P_aux (_,p_annot) as pat,typ) = E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) else (pat,typ), fun e -> e +let pat_is_plain_binder env (P_aux (p,_)) = + match p with + | P_id id + | P_typ (_,P_aux (P_id id,_)) + when not (is_enum env id) -> Some id + | _ -> None + +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) + then (pat,typ), fun e -> e + else + (P_aux (P_id id, p_annot),typ), + fun (E_aux (_,e_ann) as e) -> + E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) + | None -> + let id = mk_id ("arg" ^ string_of_int i) in (* TODO: name conflicts *) + (P_aux (P_id id, p_annot),typ), + fun (E_aux (_,e_ann) as e) -> + E_aux (E_let (LB_aux (LB_val (pat, E_aux (E_id id, p_annot)),p_annot),e),e_ann) + (* Add equality constraints between arguments and nexps, except in the case that they've been merged. *) @@ -1963,7 +2031,7 @@ let merge_var_patterns map pats = | _ -> map, (pat,typ)::pats) (map,[]) pats in map, List.rev pats -let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = +let doc_funcl rec_opt (FCL_aux(FCL_Funcl(id, pexp), annot)) = let env = env_of_annot annot in let (tq,typ) = Env.get_val_spec_orig id env in let (arg_typs, ret_typ, eff) = match typ with @@ -1978,17 +2046,31 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = 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 - let pats, bind = untuple_args_pat arg_typs pat in (* FIXME is this needed any more? *) - let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in + let pats, bind = untuple_args_pat arg_typs pat in + (* Fixpoint definitions can only use simple binders, but even Definitions + can't handle as patterns *) + let pattern_elim = + match rec_opt with + | Rec_aux (Rec_nonrec,_) -> demote_as_pattern + | _ -> demote_all_patterns env + in + let pats, binds = List.split (Util.list_mapi pattern_elim pats) in let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in let kids_used = KidSet.diff bound_kids eliminated_kids in + let is_measured, recursive_ids = match rec_opt with + (* No mutual recursion in this backend yet; only change recursive + definitions where we have a measure *) + | Rec_aux (Rec_measure _,_) -> true, IdSet.singleton id + | _ -> false, IdSet.empty + in let ctxt = { 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_ex_return = effectful eff && build_ex; + recursive_ids = recursive_ids; debug = List.mem (string_of_id id) (!opt_debug_on) } in let () = @@ -2009,27 +2091,11 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = debug ctxt (lazy (" pattern " ^ string_of_pat pat)); debug ctxt (lazy (" with expanded type " ^ string_of_typ exp_typ)) in - match p with - | P_id id - | P_typ (_,P_aux (P_id id,_)) - when Util.is_none (is_auto_decomposed_exist env exp_typ) && - not (is_enum env id) -> - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) -(* | P_id id - | P_typ (_,P_aux (P_id id,_)) - when not (is_enum env id) -> begin - match destruct_exist env (expand_range_type exp_typ) with - | Some (kids, NC_aux (NC_true,_), typ) -> - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - | Some (kids, nc, typ) -> - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) ^^ space ^^ - bquote ^^ braces (doc_arithfact ctxt nc) - | None -> - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - end*) - | P_id id - | P_typ (_,P_aux (P_id id,_)) - when not (is_enum env id) -> begin + 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 let full_typ = (expand_range_type exp_typ) in match destruct_exist (Env.expand_synonyms env full_typ) with | Some ([kopt], NC_aux (NC_true,_), @@ -2040,17 +2106,17 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = | Some ([kopt], nc, Typ_aux (Typ_app (Id_aux (Id "atom",_), [A_aux (A_nexp (Nexp_aux (Nexp_var kid,_)),_)]),_)) - when Kid.compare (kopt_kid kopt) kid == 0 -> + when Kid.compare (kopt_kid kopt) kid == 0 && not is_measured -> (used_a_pattern := true; squote ^^ parens (separate space [string "existT"; underscore; doc_id id; underscore; colon; doc_typ ctxt typ])) | _ -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) end - | _ -> + | None -> (used_a_pattern := true; squote ^^ parens (separate space [doc_pat ctxt true true (pat, exp_typ); colon; doc_typ ctxt typ])) in - let patspp = separate_map space doc_binder pats in + let patspp = flow_map (break 1) doc_binder pats in let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in let atom_constr_pp = separate space atom_constrs in let retpp = @@ -2059,6 +2125,31 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = else doc_typ ctxt ret_typ in let idpp = doc_id id in + let intropp, accpp, measurepp, fixupspp = match rec_opt with + | Rec_aux (Rec_measure _,_) -> + let fixupspp = + Util.map_filter (fun (pat,typ) -> + match pat_is_plain_binder env pat with + | Some id -> begin + match destruct_exist (Env.expand_synonyms env (expand_range_type typ)) with + | Some (_, NC_aux (NC_true,_), _) -> None + | Some ([KOpt_aux (KOpt_kind (_, kid), _)], nc, + Typ_aux (Typ_app (Id_aux (Id "atom",_), + [A_aux (A_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_)) + when Kid.compare kid kid' == 0 -> + Some (string "let " ^^ doc_id id ^^ string " := projT1 " ^^ doc_id id ^^ string " in") + | _ -> None + end + | None -> None) pats + in + string "Fixpoint", + [parens (string "_acc : Acc (Zwf 0) _rec_limit")], + [string "{struct _acc}"], + fixupspp + | Rec_aux (r,_) -> + let d = match r with Rec_nonrec -> "Definition" | _ -> "Fixpoint" in + string d, [], [], [] + in (* Work around Coq bug 7975 about pattern binders followed by implicit arguments *) let implicitargs = if !used_a_pattern && List.length constrspp + List.length atom_constrs > 0 then @@ -2078,9 +2169,10 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = "guarded pattern expression should have been rewritten before pretty-printing") in let bodypp = doc_fun_body ctxt exp in let bodypp = if effectful eff || not build_ex then bodypp else string "build_ex" ^^ parens bodypp in + let bodypp = separate (break 1) fixupspp ^/^ bodypp in group (prefix 3 1 - (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^ - separate space [colon; retpp; coloneq]) + (flow (break 1) ([intropp; idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp] @ accpp) ^/^ + flow (break 1) (measurepp @ [colon; retpp; coloneq])) (bodypp ^^ dot)) ^^ implicitargs let get_id = function @@ -2091,7 +2183,7 @@ let get_id = function joined by "and", although it has worked for Isabelle before. However, all the funcls should have been merged by the merge_funcls rewrite now. *) let doc_fundef_rhs (FD_aux(FD_function(r, typa, efa, funcls),fannot)) = - separate_map (hardline ^^ string "and ") doc_funcl funcls + separate_map (hardline ^^ string "and ") (doc_funcl r) funcls let doc_mutrec = function | [] -> failwith "DEF_internal_mutrec with empty function list" @@ -2104,7 +2196,7 @@ let rec doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = | [] -> failwith "FD_function with empty function list" | [FCL_aux (FCL_Funcl(id,_),annot) as funcl] when not (Env.is_extern id (env_of_annot annot) "coq") -> - (doc_rec r) ^^ space ^^ (doc_funcl funcl) + doc_funcl r funcl | [_] -> empty (* extern *) | _ -> failwith "FD_function with more than one clause" diff --git a/src/rewriter.ml b/src/rewriter.ml index 200121c0..a70f6fab 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -346,7 +346,14 @@ let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) = let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) = let rewrite_funcl (FCL_aux (FCL_Funcl(id,pexp),(l,annot))) = (FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),(l,annot))) - in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) + in + let recopt = match recopt with + | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l) + | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l) + | Rec_aux (Rec_measure (pat,exp),l) -> + Rec_aux (Rec_measure (rewrite_pat rewriters pat, rewrite_exp rewriters exp),l) + in + FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot)) let rewrite_def rewriters d = match d with | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), annot)) -> diff --git a/src/rewrites.ml b/src/rewrites.ml index 30318e3f..0ad4c56e 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2204,9 +2204,11 @@ let rewrite_fix_val_specs (Defs defs) = (* Repeat once to cross-propagate effects between clauses *) let (val_specs, funcls) = List.fold_left rewrite_funcl (val_specs, []) funcls in let recopt = - if List.exists is_funcl_rec funcls then - Rec_aux (Rec_rec, Parse_ast.Unknown) - else recopt + match recopt with + | Rec_aux ((Rec_rec | Rec_measure _), _) -> recopt + | _ when List.exists is_funcl_rec funcls -> + Rec_aux (Rec_rec, Parse_ast.Unknown) + | _ -> recopt in let tannotopt = match tannotopt, funcls with | Typ_annot_opt_aux (Typ_annot_opt_some (typq, typ), l), @@ -4751,7 +4753,7 @@ let minimise_recursive_functions (Defs defs) = let rewrite_function (FD_aux (FD_function (recopt,topt,effopt,funcls),ann) as fd) = match recopt with | Rec_aux (Rec_nonrec, _) -> fd - | Rec_aux (Rec_rec, l) -> + | Rec_aux ((Rec_rec | Rec_measure _), l) -> if List.exists funcl_is_rec funcls then fd else FD_aux (FD_function (Rec_aux (Rec_nonrec, Generated l),topt,effopt,funcls),ann) @@ -4761,7 +4763,150 @@ let minimise_recursive_functions (Defs defs) = | d -> d in Defs (List.map rewrite_def defs) +(* Make recursive functions with a measure use the measure as an + explicit recursion limit, enforced by an assertion. *) +let rewrite_explicit_measure (Defs defs) = + let scan_function measures = function + | FD_aux (FD_function (Rec_aux (Rec_measure (mpat,mexp),rl),topt,effopt, + FCL_aux (FCL_Funcl (id,_),_)::_),ann) -> + Bindings.add id (mpat,mexp) measures + | _ -> measures + in + let scan_def measures = function + | DEF_fundef fd -> scan_function measures fd + | _ -> measures + in + let measures = List.fold_left scan_def Bindings.empty defs in + let add_escape eff = + union_effects eff (mk_effect [BE_escape]) + in + (* NB: the Coq backend relies on recognising the #rec# prefix *) + let rec_id = function + | Id_aux (Id id,l) + | Id_aux (DeIid id,l) -> Id_aux (Id ("#rec#" ^ id),Generated l) + in + let limit = mk_id "#reclimit" in + (* Add helper function with extra argument to spec *) + let rewrite_spec (VS_aux (VS_val_spec (typsch,id,extern,flag),ann) as vs) = + match Bindings.find id measures with + | _ -> begin + match typsch with + | TypSchm_aux (TypSchm_ts (tq, + Typ_aux (Typ_fn (args,res,eff),typl)),tsl) -> + [VS_aux (VS_val_spec ( + TypSchm_aux (TypSchm_ts (tq, + Typ_aux (Typ_fn (args@[int_typ],res,add_escape eff),typl)),tsl) + ,rec_id id,extern,flag),ann); + VS_aux (VS_val_spec ( + TypSchm_aux (TypSchm_ts (tq, + Typ_aux (Typ_fn (args,res,add_escape eff),typl)),tsl) + ,id,extern,flag),ann)] + | _ -> [vs] (* TODO warn *) + end + | exception Not_found -> [vs] + in + (* Add extra argument and assertion to each funcl, and rewrite recursive calls *) + let rewrite_funcl (FCL_aux (FCL_Funcl (id,pexp),ann) as fcl) = + let loc = Parse_ast.Generated (fst ann) in + let P_aux (pat,pann),guard,body,ann = destruct_pexp pexp in + let extra_pat = P_aux (P_id limit,(loc,empty_tannot)) in + let pat = match pat with + | P_tup pats -> P_tup (pats@[extra_pat]) + | p -> P_tup [P_aux (p,pann);extra_pat] + in + let assert_exp = + E_aux (E_assert + (E_aux (E_app (mk_id "gteq_int", + [E_aux (E_id limit,(loc,empty_tannot)); + E_aux (E_lit (L_aux (L_num Big_int.zero,loc)),(loc,empty_tannot))]), + (loc,empty_tannot)), + (E_aux (E_lit (L_aux (L_string "recursion limit reached",loc)),(loc,empty_tannot)))), + (loc,empty_tannot)) + in + let tick = + E_aux (E_app (mk_id "sub_int", + [E_aux (E_id limit,(loc,empty_tannot)); + E_aux (E_lit (L_aux (L_num (Big_int.of_int 1),loc)),(loc,empty_tannot))]), + (loc,empty_tannot)) + in + let open Rewriter in + let body = + fold_exp { id_exp_alg with + e_app = (fun (f,args) -> + if Id.compare f id == 0 + then E_app (rec_id id, args@[tick]) + else E_app (f, args)) + } body + in + let body = E_aux (E_block [assert_exp; body],(loc,empty_tannot)) in + FCL_aux (FCL_Funcl (rec_id id, construct_pexp (P_aux (pat,pann),guard,body,ann)),ann) + in + let rewrite_function (FD_aux (FD_function (r,t,e,fcls),ann) as fd) = + let loc = Parse_ast.Generated (fst ann) in + match fcls with + | FCL_aux (FCL_Funcl (id,_),fcl_ann)::_ -> begin + match Bindings.find id measures with + | (measure_pat, measure_exp) -> + let e = match e with + | Effect_opt_aux (Effect_opt_pure, _) -> + Effect_opt_aux (Effect_opt_effect (mk_effect [BE_escape]), loc) + | Effect_opt_aux (Effect_opt_effect eff,_) -> + Effect_opt_aux (Effect_opt_effect (add_escape eff), loc) + in + let arg_typs = match Env.get_val_spec id (env_of_annot fcl_ann) with + | _, Typ_aux (Typ_fn (args,_,_),_) -> args + | _, _ -> raise (Reporting.err_unreachable (fst ann) __POS__ + "Function doesn't have function type") + in + let measure_pats = match arg_typs, measure_pat with + | [_], _ -> [measure_pat] + | _, P_aux (P_tup ps,_) -> ps + | _, _ -> [measure_pat] + in + let mk_wrap i (P_aux (p,(l,_))) = + let id = + match p with + | P_id id + | P_typ (_,(P_aux (P_id id,_))) -> id + | P_wild + | P_typ (_,(P_aux (P_wild,_))) -> + mk_id ("_arg" ^ string_of_int i) + | _ -> raise (Reporting.err_todo l "Measure patterns can only be identifiers or wildcards") + in + P_aux (P_id id,(loc,empty_tannot)), + E_aux (E_id id,(loc,empty_tannot)) + in + let wpats,wexps = List.split (Util.list_mapi mk_wrap measure_pats) in + let wpat = match wpats with + | [wpat] -> wpat + | _ -> P_aux (P_tup wpats,(loc,empty_tannot)) + in + let wbody = E_aux (E_app (rec_id id,wexps@[measure_exp]),(loc,empty_tannot)) in + let wrapper = + FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (wpat,wbody),(loc,empty_tannot))),(loc,empty_tannot)) + in + let new_rec = + Rec_aux (Rec_measure (P_aux (P_tup (List.map (fun _ -> P_aux (P_wild,(loc,empty_tannot))) measure_pats @ [P_aux (P_id limit,(loc,empty_tannot))]),(loc,empty_tannot)), E_aux (E_id limit, (loc,empty_tannot))), loc) + in + [FD_aux (FD_function (new_rec,t,e,List.map rewrite_funcl fcls),ann); + FD_aux (FD_function (Rec_aux (Rec_nonrec,loc),t,e,[wrapper]),ann)] + | exception Not_found -> [fd] + end + | _ -> [fd] + in + let rewrite_def = function + | DEF_spec vs -> List.map (fun vs -> DEF_spec vs) (rewrite_spec vs) + | DEF_fundef fd -> List.map (fun f -> DEF_fundef f) (rewrite_function fd) + | d -> [d] + in + Defs (List.flatten (List.map rewrite_def defs)) + let recheck_defs defs = fst (Type_error.check initial_env defs) +let recheck_defs_without_effects defs = + let () = opt_no_effects := true in + let result,_ = Type_error.check initial_env defs in + let () = opt_no_effects := false in + result let remove_mapping_valspecs (Defs defs) = let allowed_def def = @@ -4889,8 +5034,9 @@ let rewrite_defs_coq = [ ("sizeof", rewrite_sizeof); ("early_return", rewrite_defs_early_return); ("make_cases_exhaustive", MakeExhaustive.rewrite); + ("rewrite_explicit_measure", rewrite_explicit_measure); + ("recheck_defs_without_effects", recheck_defs_without_effects); ("fix_val_specs", rewrite_fix_val_specs); - ("recheck_defs", recheck_defs); ("remove_blocks", rewrite_defs_remove_blocks); ("letbind_effects", rewrite_defs_letbind_effects); ("remove_e_assign", rewrite_defs_remove_e_assign); diff --git a/src/type_check.ml b/src/type_check.ml index 1216786e..0f083823 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4175,6 +4175,16 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) in check_tannotopt env quant vtyp_ret tannotopt; typ_debug (lazy ("Checking fundef " ^ string_of_id id ^ " has type " ^ string_of_bind (quant, typ))); + let recopt = + match recopt with + | Rec_aux (Rec_nonrec, l) -> Rec_aux (Rec_nonrec, l) + | Rec_aux (Rec_rec, l) -> Rec_aux (Rec_rec, l) + | Rec_aux (Rec_measure (measure_p, measure_e), l) -> + let typ = match vtyp_args with [x] -> x | _ -> Typ_aux (Typ_tup vtyp_args,Unknown) in + let tpat, env = bind_pat_no_guard env (strip_pat measure_p) typ in + let texp = check_exp env (strip_exp measure_e) int_typ in + Rec_aux (Rec_measure (tpat, texp), l) + in let funcl_env = add_typquant l quant env in let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in let eff = List.fold_left union_effects no_effect (List.map funcl_effect funcls) in |