diff options
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 21 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 24 |
2 files changed, 34 insertions, 11 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 336ca8de..6448e81b 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -30,6 +30,27 @@ match l with foreachM xs vars body end. +Fixpoint foreach_ZM_up' {rv e Vars} from to step off n `{ArithFact (from <= to)} `{ArithFact (0 < step)} `{ArithFact (0 <= off)} (vars : Vars) (body : forall (z : Z) `(ArithFact (from <= z <= to)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := + if sumbool_of_bool (from + off <=? to) then + match n with + | O => returnm vars + | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_up' from to step (off + step) n vars body + end + else returnm vars. + +Fixpoint foreach_ZM_down' {rv e Vars} from to step off n `{ArithFact (to <= from)} `{ArithFact (0 < step)} `{ArithFact (off <= 0)} (vars : Vars) (body : forall (z : Z) `(ArithFact (to <= z <= from)), Vars -> monad rv Vars e) {struct n} : monad rv Vars e := + if sumbool_of_bool (to <=? from + off) then + match n with + | O => returnm vars + | S n => body (from + off) _ vars >>= fun vars => foreach_ZM_down' from to step (off - step) n vars body + end + else returnm vars. + +Definition foreach_ZM_up {rv e Vars} from to step vars body `{ArithFact (from <= to)} `{ArithFact (0 < step)} := + foreach_ZM_up' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. +Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (to <= from)} `{ArithFact (0 < step)} := + foreach_ZM_down' (rv := rv) (e := e) (Vars := Vars) from to step 0 (S (Z.abs_nat (from - to))) vars body. + (*declare {isabelle} termination_argument foreachM = automatic*) (*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 7d8d0e5a..38395b07 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -831,7 +831,7 @@ let doc_exp_lem, doc_let_lem = | Id_aux (Id "foreach", _) -> begin match args with - | [exp1; exp2; exp3; ord_exp; vartuple; body] -> + | [from_exp; to_exp; step_exp; ord_exp; vartuple; body] -> let loopvar, body = match body with | E_aux (E_let (LB_aux (LB_val (_, _), _), E_aux (E_let (LB_aux (LB_val (_, _), _), @@ -842,13 +842,13 @@ let doc_exp_lem, doc_let_lem = | (P_aux (P_id id, _))), _), _), body), _), _), _)), _)), _) -> id, body | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in - let step = match ord_exp with - | E_aux (E_lit (L_aux (L_false, _)), _) -> - parens (separate space [string "integerNegate"; expY exp3]) - | _ -> expY exp3 + let dir = match ord_exp with + | E_aux (E_lit (L_aux (L_false, _)), _) -> "_down" + | E_aux (E_lit (L_aux (L_true, _)), _) -> "_up" + | _ -> raise (Reporting_basic.err_unreachable l ("Unexpected loop direction " ^ string_of_exp ord_exp)) in - let combinator = if effectful (effect_of body) then "foreachM" else "foreach" in - let indices_pp = parens (separate space [string "index_list"; expY exp1; expY exp2; step]) in + let combinator = if effectful (effect_of body) then "foreach_ZM" else "foreach_Z" in + let combinator = combinator ^ dir in let used_vars_body = find_e_ids body in let body_lambda = (* Work around indentation issues in Lem when translating @@ -856,18 +856,20 @@ let doc_exp_lem, doc_let_lem = match fst (uncast_exp vartuple) with | E_aux (E_tuple _, _) when not (IdSet.mem (mk_id "varstup") used_vars_body)-> - separate space [string "fun"; doc_id loopvar; string "varstup"; bigarrow] + separate space [string "fun"; doc_id loopvar; string "_"; string "varstup"; bigarrow] ^^ break 1 ^^ separate space [string "let"; expY vartuple; string ":= varstup in"] | E_aux (E_lit (L_aux (L_unit, _)), _) when not (IdSet.mem (mk_id "unit_var") used_vars_body) -> - separate space [string "fun"; doc_id loopvar; string "unit_var"; bigarrow] + separate space [string "fun"; doc_id loopvar; string "_"; string "unit_var"; bigarrow] | _ -> - separate space [string "fun"; doc_id loopvar; expY vartuple; bigarrow] + separate space [string "fun"; doc_id loopvar; string "_"; expY vartuple; bigarrow] in parens ( (prefix 2 1) - ((separate space) [string combinator; indices_pp; expY vartuple]) + ((separate space) [string combinator; + expY from_exp; expY to_exp; expY step_exp; + expY vartuple]) (parens (prefix 2 1 (group body_lambda) (expN body)) ) |