diff options
| -rw-r--r-- | language/sail.ott | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 1 | ||||
| -rw-r--r-- | src/parser.mly | 4 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 3 | ||||
| -rw-r--r-- | src/rewriter.ml | 1 | ||||
| -rw-r--r-- | src/rewrites.ml | 31 | ||||
| -rw-r--r-- | src/type_check.ml | 21 |
9 files changed, 62 insertions, 4 deletions
diff --git a/language/sail.ott b/language/sail.ott index dfd9a423..a07f19ff 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -990,6 +990,8 @@ def :: 'DEF_' ::= {{ com default kind and type assumptions }} | scattered_def :: :: scattered {{ com scattered function and type definition }} + | 'termination_measure' id pat = exp :: :: measure + {{ com separate termination measure declaration }} | dec_spec :: :: reg_dec {{ com register declaration }} | fundef1 .. fundefn :: I :: internal_mutrec diff --git a/src/initial_check.ml b/src/initial_check.ml index 17b4b515..78314363 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -743,6 +743,8 @@ let to_ast_def ctx def : unit def ctx_out = | P.DEF_scattered sdef -> let sdef, ctx = to_ast_scattered ctx sdef in DEF_scattered sdef, ctx + | P.DEF_measure (id, pat, exp) -> + DEF_measure (to_ast_id id, to_ast_pat ctx pat, to_ast_exp ctx exp), ctx let rec remove_mutrec = function | [] -> [] diff --git a/src/lexer.mll b/src/lexer.mll index 57580e7a..1d48b82b 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -182,6 +182,7 @@ let kw_table = ("nondet", (fun x -> Nondet)); ("escape", (fun x -> Escape)); ("configuration", (fun _ -> Configuration)); + ("termination_measure", (fun _ -> TerminationMeasure)); ] diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 65b11373..20a0f48a 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -531,6 +531,7 @@ def = (* Top-level definition *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) + | DEF_measure of id * pat * exp (* separate termination measure declaration *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list diff --git a/src/parser.mly b/src/parser.mly index 66902953..3ad0931a 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -183,7 +183,7 @@ let rec desugar_rchain chain s e = %token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Constant Constraint Throw Try Catch Exit Bitfield %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape -%token Repeat Until While Do Mutual Var Ref Configuration +%token Repeat Until While Do Mutual Var Ref Configuration TerminationMeasure %nonassoc Then %nonassoc Else @@ -1430,6 +1430,8 @@ def: { DEF_internal_mutrec $3 } | Pragma { DEF_pragma (fst $1, snd $1, loc $startpos $endpos) } + | TerminationMeasure id pat Eq exp + { DEF_measure ($2, $3, $5) } defs_list: | def diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 345312f7..d5758303 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -662,6 +662,9 @@ let rec doc_def def = group (match def with ^^ hardline ^^ string "}" | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef + | DEF_measure (id,pat,exp) -> + string "termination_measure" ^^ space ^^ doc_id id ^/^ doc_pat pat ^^ + space ^^ equals ^/^ doc_exp exp | DEF_pragma (pragma, arg, l) -> string ("$" ^ pragma ^ " " ^ arg) | DEF_fixity (prec, n, id) -> diff --git a/src/rewriter.ml b/src/rewriter.ml index a70f6fab..21310b91 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -364,6 +364,7 @@ let rewrite_def rewriters d = match d with | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind) | DEF_pragma (pragma, arg, l) -> DEF_pragma (pragma, arg, l) | DEF_scattered _ -> raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "DEF_scattered survived to rewritter") + | DEF_measure (id,pat,exp) -> DEF_measure (id,rewriters.rewrite_pat rewriters pat, rewriters.rewrite_exp rewriters exp) let rewrite_defs_base rewriters (Defs defs) = let rec rewrite ds = match ds with diff --git a/src/rewrites.ml b/src/rewrites.ml index 0ad4c56e..8d53ea54 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4763,6 +4763,35 @@ let minimise_recursive_functions (Defs defs) = | d -> d in Defs (List.map rewrite_def defs) +let move_termination_measures (Defs defs) = + let scan_for id defs = + let rec aux = function + | [] -> None + | (DEF_measure (id',pat,exp))::t -> + if Id.compare id id' == 0 then Some (pat,exp) else aux t + | (DEF_fundef (FD_aux (FD_function (_,_,_,FCL_aux (FCL_Funcl (id',_),_)::_),_)))::_ + | (DEF_spec (VS_aux (VS_val_spec (_,id',_,_),_))::_) + when Id.compare id id' == 0 -> None + | _::t -> aux t + in aux defs + in + let rec aux acc = function + | [] -> List.rev acc + | (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann))) as d)::t -> begin + let id = match fs with + | [] -> assert false (* TODO *) + | (FCL_aux (FCL_Funcl (id,_),_))::_ -> id + in + match scan_for id t with + | None -> aux (d::acc) t + | Some (pat,exp) -> + let r = Rec_aux (Rec_measure (pat,exp), Generated l) in + aux (DEF_fundef (FD_aux (FD_function (r,ty,e,fs),(l,f_ann)))::acc) t + end + | (DEF_measure _)::t -> aux acc t + | h::t -> aux (h::acc) t + in Defs (aux [] 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) = @@ -4881,6 +4910,7 @@ let rewrite_explicit_measure (Defs defs) = | [wpat] -> wpat | _ -> P_aux (P_tup wpats,(loc,empty_tannot)) in + let measure_exp = E_aux (E_cast (int_typ, measure_exp),(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)) @@ -5008,6 +5038,7 @@ let rewrite_defs_coq = [ ("toplevel_string_append", rewrite_defs_toplevel_string_append); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("move_termination_measures", move_termination_measures); ("rewrite_undefined", rewrite_undefined_if_gen true); ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list); ("remove_not_pats", rewrite_defs_not_pats); diff --git a/src/type_check.ml b/src/type_check.ml index 53d87a05..ee80296f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -4158,6 +4158,22 @@ let check_tannotopt env typq ret_typ = function then () else typ_error l (string_of_bind (typq, ret_typ) ^ " and " ^ string_of_bind (annot_typq, annot_ret_typ) ^ " do not match between function and val spec") +let check_termination_measure env arg_typs pat exp = + let typ = match arg_typs with [x] -> x | _ -> Typ_aux (Typ_tup arg_typs,Unknown) in + let tpat, env = bind_pat_no_guard env (strip_pat pat) typ in + let texp = check_exp env (strip_exp exp) int_typ in + tpat, texp + +let check_termination_measure_decl env (id, pat, exp) = + let quant, typ = Env.get_val_spec id env in + let arg_typs, l = match typ with + | Typ_aux (Typ_fn (arg_typs, _ ,_),l) -> arg_typs,l + | _ -> typ_error (id_loc id) "Function val spec is not a function type" + in + let env = add_typquant l quant env in + let tpat, texp = check_termination_measure env arg_typs pat exp in + DEF_measure (id, tpat, texp) + let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls), (l, _)) as fd_aux) = let id = match (List.fold_right @@ -4190,9 +4206,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) | 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 funcl_env (strip_pat measure_p) typ in - let texp = check_exp env (strip_exp measure_e) int_typ in + let tpat, texp = check_termination_measure funcl_env vtyp_args measure_p measure_e in Rec_aux (Rec_measure (tpat, texp), l) in let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in @@ -4439,6 +4453,7 @@ and check_def : 'a. Env.t -> 'a def -> (tannot def) list * Env.t = | DEF_reg_dec (DEC_aux (DEC_alias (id, aspec), (l, annot))) -> cd_err () | DEF_reg_dec (DEC_aux (DEC_typ_alias (typ, id, aspec), (l, tannot))) -> cd_err () | DEF_scattered sdef -> check_scattered env sdef + | DEF_measure (id, pat, exp) -> [check_termination_measure_decl env (id, pat, exp)], env and check : 'a. Env.t -> 'a defs -> tannot defs * Env.t = fun env (Defs defs) -> |