Skip to content

Commit

Permalink
moved CoqExport code to StepperBase, unfortunately
Browse files Browse the repository at this point in the history
  • Loading branch information
@nskh
nskh committed Feb 25, 2025
1 parent 48c7620 commit 9ead118
Show file tree
Hide file tree
Showing 2 changed files with 285 additions and 96 deletions.
184 changes: 92 additions & 92 deletions src/haz3lweb/app/editors/stepper/CoqExport.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,101 +80,101 @@ let rec string_of_d = (d: DHExp.t) => {
++ ")";
};
// Takes a single step
let single_step_export = (ind, step, forall_str) => {
let {expr, next_step, state, editor, step_kind, hidden} = step;
// let single_step_export = (ind, step, forall_str) => {
// let {expr, next_step, state, editor, step_kind, hidden} = step;

let oldFragmentString = string_of_d(expr);
let newFragmentString = string_of_d(next_step.expr);
// let oldFragmentString = string_of_d(expr);
// let newFragmentString = string_of_d(next_step.expr);

//Printf.printf("Step: %s -> %s\n", oldFragmentString, newFragmentString);
let oldExprString = string_of_d(EvalCtx.compose(ctx, expr));
let newExpr = EvalCtx.compose(ctx, next_step.expr);
let newExprString = string_of_d(newExpr);
//Printf.printf("old: %s\n", oldExprString);
//Printf.printf("new: %s\n", newExprString);
// TODO(nishant): unpack the axiom correctly
let evalTactic =
switch (step.step_kind) {
// switch (step.name) {
// | IdPlusL => "rewrite Qplus_0_l"
// | CommPlus => "rewrite Qplus_comm"
// | AssocPlusL => "rewrite Qplus_assoc"
// | AssocPlusR => "rewrite Qplus_assoc"
// | IdTimesL => "rewrite Qmult_1_r"
// | CommTimes => "rewrite Qmult_comm"
// | AssocTimesL => "rewrite Qmult_assoc"
// | AssocTimesR => "rewrite Qmult_assoc"
// | DistPlusTimesL => "rewrite Qmult_plus_distr_l"
// | DistPlusTimesR => "rewrite Qmult_plus_distr_l"
// | DistPlusTimesLC => "rewrite Qmult_plus_distr_r"
// | DistPlusTimesRC => "rewrite Qmult_plus_distr_r"
// | DistPlusDivL => "unfold Qdiv. rewrite Qmult_plus_distr_l"
// | DistPlusDivR => "unfold Qdiv. rewrite Qmult_plus_distr_l"
// | DefDivL => "unfold Qdiv. rewrite Qmult_1_l"
// | DefDivR => "unfold Qdiv. rewrite Qmult_1_l"
// | NilTimesL => "rewrite Qmult_0_l"
// | AssocTimesDivL => "unfold Qdiv. rewrite Qmult_assoc"
// | AssocTimesDivR => "unfold Qdiv. rewrite Qmult_assoc"
// };
| _ => "cbv"
};
let rewriteIndex = index_of_like_terms(ctx, d_loc');
let coqLemmaString =
Printf.sprintf(
"Lemma equiv_exp%d:%s%s == %s.\nProof.\nintros.\ncut (%s==%s).\n- intros. rewrite <- H at %d. reflexivity.\n- intros. %s. reflexivity.\nQed.",
ind,
forall_str,
newExprString,
oldExprString,
oldFragmentString,
newFragmentString,
rewriteIndex,
evalTactic,
);
//Printf.printf("Coq proof:\n%s\n", coqLemmaString);
coqLemmaString;
};
// //Printf.printf("Step: %s -> %s\n", oldFragmentString, newFragmentString);
// let oldExprString = string_of_d(EvalCtx.compose(ctx, expr));
// let newExpr = EvalCtx.compose(ctx, next_step.expr);
// let newExprString = string_of_d(newExpr);
// //Printf.printf("old: %s\n", oldExprString);
// //Printf.printf("new: %s\n", newExprString);
// // TODO(nishant): unpack the axiom correctly
// let evalTactic =
// switch (step.step_kind) {
// // switch (step.name) {
// // | IdPlusL => "rewrite Qplus_0_l"
// // | CommPlus => "rewrite Qplus_comm"
// // | AssocPlusL => "rewrite Qplus_assoc"
// // | AssocPlusR => "rewrite Qplus_assoc"
// // | IdTimesL => "rewrite Qmult_1_r"
// // | CommTimes => "rewrite Qmult_comm"
// // | AssocTimesL => "rewrite Qmult_assoc"
// // | AssocTimesR => "rewrite Qmult_assoc"
// // | DistPlusTimesL => "rewrite Qmult_plus_distr_l"
// // | DistPlusTimesR => "rewrite Qmult_plus_distr_l"
// // | DistPlusTimesLC => "rewrite Qmult_plus_distr_r"
// // | DistPlusTimesRC => "rewrite Qmult_plus_distr_r"
// // | DistPlusDivL => "unfold Qdiv. rewrite Qmult_plus_distr_l"
// // | DistPlusDivR => "unfold Qdiv. rewrite Qmult_plus_distr_l"
// // | DefDivL => "unfold Qdiv. rewrite Qmult_1_l"
// // | DefDivR => "unfold Qdiv. rewrite Qmult_1_l"
// // | NilTimesL => "rewrite Qmult_0_l"
// // | AssocTimesDivL => "unfold Qdiv. rewrite Qmult_assoc"
// // | AssocTimesDivR => "unfold Qdiv. rewrite Qmult_assoc"
// // };
// | _ => "cbv"
// };
// let rewriteIndex = index_of_like_terms(ctx, d_loc');
// let coqLemmaString =
// Printf.sprintf(
// "Lemma equiv_exp%d:%s%s == %s.\nProof.\nintros.\ncut (%s==%s).\n- intros. rewrite <- H at %d. reflexivity.\n- intros. %s. reflexivity.\nQed.",
// ind,
// forall_str,
// newExprString,
// oldExprString,
// oldFragmentString,
// newFragmentString,
// rewriteIndex,
// evalTactic,
// );
// //Printf.printf("Coq proof:\n%s\n", coqLemmaString);
// coqLemmaString;
// };

// Takes a list of steps and generates the Coq proof of equivalence between the first and last steps
let exportCoq = (steps: list(Model.step)) =>
if (List.length(steps) == 0) {
"Not exporting proof with no steps";
} else {
let firstD = List.nth(steps, List.length(steps) - 1).d;
let unique_vars = unique_vars_in_ast(firstD);
let forall_str =
if (List.length(unique_vars) == 0) {
"";
} else {
"forall " ++ String.concat(" ", unique_vars) ++ ",";
};
// // Takes a list of steps and generates the Coq proof of equivalence between the first and last steps
// let exportCoq = (steps: list(Model.step)) =>
// if (List.length(steps) == 0) {
// "Not exporting proof with no steps";
// } else {
// let firstD = List.nth(steps, List.length(steps) - 1).d;
// let unique_vars = unique_vars_in_ast(firstD);
// let forall_str =
// if (List.length(unique_vars) == 0) {
// "";
// } else {
// "forall " ++ String.concat(" ", unique_vars) ++ ",";
// };

let lemmasAndInvocations =
List.mapi(
(ind, step) =>
(
single_step_export(List.length(steps) - ind, step, forall_str),
Printf.sprintf(
"rewrite -> equiv_exp%d.",
List.length(steps) - ind,
),
),
steps,
);
let (lemmas, invocations) = List.split(lemmasAndInvocations);
// let lemmasAndInvocations =
// List.mapi(
// (ind, step) =>
// (
// single_step_export(List.length(steps) - ind, step, forall_str),
// Printf.sprintf(
// "rewrite -> equiv_exp%d.",
// List.length(steps) - ind,
// ),
// ),
// steps,
// );
// let (lemmas, invocations) = List.split(lemmasAndInvocations);

let finalExpr =
string_of_d(
EvalCtx.compose(List.hd(steps).ctx, List.hd(steps).d_loc'),
);
let firstExpr = string_of_d(firstD);
// let finalExpr =
// string_of_d(
// EvalCtx.compose(List.hd(steps).ctx, List.hd(steps).d_loc'),
// );
// let firstExpr = string_of_d(firstD);

Printf.sprintf(
"Require Import QArith.\nRequire Export Plus.\nRequire Export Mult.\n%s\nTheorem equiv_exp:%s%s==%s.\nProof.\nintros.\n%s\nreflexivity. Qed.",
String.concat("\n", lemmas),
forall_str,
finalExpr,
firstExpr,
String.concat("\n", invocations),
);
};
// Printf.sprintf(
// "Require Import QArith.\nRequire Export Plus.\nRequire Export Mult.\n%s\nTheorem equiv_exp:%s%s==%s.\nProof.\nintros.\n%s\nreflexivity. Qed.",
// String.concat("\n", lemmas),
// forall_str,
// finalExpr,
// firstExpr,
// String.concat("\n", invocations),
// );
// };
Loading

0 comments on commit 9ead118

Please sign in to comment.