Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add cv_eval_pat to cv_transLib (and an example) #1406

Open
wants to merge 6 commits into
base: develop
Choose a base branch
from
Open

Add cv_eval_pat to cv_transLib (and an example) #1406

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0040928
Add cv_eval_raw_save to cv_transLib (and an example)
myreen Feb 24, 2025
3d6d2d5
Generalise interface
myreen Feb 24, 2025
f1f4644
Try to better match old behaviour
myreen Feb 25, 2025
54bc88c
UNDISCH --> DISCH
myreen Feb 25, 2025
bd8568b
Change Pair to Tuple in new pat datatype
myreen Feb 26, 2025
e211611
Fix a comment and add new comment
myreen Feb 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions examples/cv_compute/cv_eval_exampleScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
(*
Demonstrates use of cv_eval_raw_save
*)
open HolKernel Parse boolLib bossLib;
open cv_transLib cv_stdTheory

val _ = new_theory "cv_eval_example";

Definition test_def:
test n = if n = 0 then NONE else SOME (n+1, n+2, REPLICATE n T)
End

val _ = cv_trans test_def;

val pat = Some (Tuple [Eval EVAL, Raw, Name "big_replicate"]);

val res = cv_eval_pat pat “test 10000”;
(* returns:
⊢ test 10000 = SOME (10001,cv$c2n (Num 10002),big_replicate)
*)

val res = cv_eval “LENGTH big_replicate”;
(* returns:
⊢ LENGTH big_replicate = 10000
*)

val _ = (max_print_depth := 10);
val _ = export_theory();
13 changes: 10 additions & 3 deletions src/num/theories/cv_compute/automation/cv_transLib.sig
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,16 @@ sig
(* The conv should evaluate `from <deep_embedding>` *)
val cv_trans_deep_embedding : conv -> thm -> unit

val cv_eqs_for : term -> thm list
val cv_eval_raw : term -> thm
val cv_eval : term -> thm
datatype pat = Raw
| Eval of conv
| Name of string
| Tuple of pat list
| Some of pat;

val cv_eqs_for : term -> thm list
val cv_eval : term -> thm
val cv_eval_raw : term -> thm
val cv_eval_pat : pat -> term -> thm

val cv_termination_tac : tactic

Expand Down
82 changes: 68 additions & 14 deletions src/num/theories/cv_compute/automation/cv_transLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -876,7 +876,13 @@ fun cv_eqs_for tm = let

val _ = computeLib.add_funs [cv_fst_def,cv_snd_def];

fun cv_eval_raw tm = let
datatype pat = Raw
| Eval of conv
| Name of string
| Tuple of pat list
| Some of pat;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the difference between Some p and Tuple [p]?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This comment makes me realise that it's unclear what the pattern means. I wrote a long comment in the file, see:

HOL/examples/cv_compute/cv_eval_exampleScript.sml

Lines 15 to 24 in e211611

(* The following example demonstrates that the given pattern,
Some (Tuple ...), instructs cv_eval_pat what to do with the
result of evaluation. In this example, we can see that the
result must be a SOME containing a tuple and the elements
of the tuple are handled as follows.
- The first is just directly evaluated.
- The second is left untouched after the raw cv computation.
- The third is stored in a new constant, big_replicate, that
can be used in subsequent calls to cv_trans, cv_eval, etc.
*)

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So is Tuple [Some (Tuple [])] just not really supposed to be used? Or does that also make sense?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

cv_eval_pat will raise an exception if users write Tuple [] in their pattern.

Writing Tuple [x] will mean the same as a single-element tuple in HOL, i.e. it's not a tuple. What's the difference between (2) and 2 in HOL? No difference.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some additional context: the constructor Tuple was originally Pair (which avoids some of the above issues). However, the Pair constructor would need to be disambiguated because it is also used elsewhere in CV.


fun cv_eval_pat pat tm = let
val _ = List.null (free_vars tm) orelse failwith "cv_eval needs input to be closed"
val th = cv_rep_for [] tm
val ty = type_of tm
Expand All @@ -887,19 +893,67 @@ fun cv_eval_raw tm = let
val cv_eqs = cv_time cv_eqs_for cv_tm
val _ = cv_print Verbose ("Found " ^ int_to_string (length cv_eqs) ^ " cv code equations to use.\n")
val cv_conv = cv_computeLib.cv_compute cv_eqs
val th1 = MATCH_MP cv_rep_eval th
val th2 = MATCH_MP th1 from_to_thm
val th3 = th2 |> UNDISCH_ALL
val _ = cv_print Verbose "Calling cv_compute.\n"
val th4 = cv_time (CONV_RULE (RAND_CONV (RAND_CONV cv_conv))) th3
val th5 = remove_T_IMP (DISCH_ALL th4)
in th5 end;

fun cv_eval tm = let
val th = cv_eval_raw tm
val _ = cv_print Verbose "Using EVAL to convert from cv to original types.\n"
val th = cv_time (CONV_RULE (RAND_CONV EVAL)) (UNDISCH_ALL th)
val th = th |> DISCH_ALL |> remove_T_IMP
in th end;
val th0 = th |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) cv_conv)
|> CONV_RULE (REWR_CONV cv_rep_def) |> UNDISCH
val _ = cv_print Verbose "Abbreviating result.\n"
val abbrev_defs = ref ([] : (string * thm) list)
fun make_abbrevs Raw th = th
| make_abbrevs (Eval _) th = th
| make_abbrevs (Name name) th = let
val (tm1,tm2) = concl th |> dest_eq
val cv_ty = cvSyntax.cv
val name_tm = mk_var("cv_" ^ name, mk_type("fun",[cv_ty,cv_ty]))
val num_0 = cvSyntax.mk_cv_num(numSyntax.term_of_int 0)
val def_eq = mk_eq(mk_comb(name_tm,mk_var("x",cv_ty)),tm2)
val cv_def = new_definition("cv_" ^ name ^ "_def", def_eq)
val th1 = th |> CONV_RULE (RAND_CONV (fn tm => SPEC num_0 cv_def |> SYM))
val tm3 = tm1 |> rand
val abbrev_def = new_definition(name ^ "_def", mk_eq(mk_var(name,type_of tm3),tm3))
val _ = (abbrev_defs := (name,abbrev_def) :: (!abbrev_defs))
val th2 = th1 |> CONV_RULE ((RATOR_CONV o RAND_CONV o RAND_CONV)
(fn tm => abbrev_def |> SYM))
val th3 = remove_T_IMP (DISCH_ALL th2) handle HOL_ERR _ => th2
val _ = save_thm("cv_" ^ name ^ "_thm[cv_rep]",th3)
in th1 end
| make_abbrevs (Tuple []) th = failwith "Empty Tuples are not supported"
| make_abbrevs (Tuple [x]) th = make_abbrevs x th
| make_abbrevs (Tuple (x::xs)) th = let
val th0 = MATCH_MP from_pair_eq_IMP th
val th1 = make_abbrevs x (CONJUNCT1 th0)
val th2 = make_abbrevs (Tuple xs) (CONJUNCT2 th0)
in MATCH_MP IMP_from_pair_eq (CONJ th1 th2) end
| make_abbrevs (Some x) th = let
val th0 = MATCH_MP from_option_eq_IMP th
val th1 = make_abbrevs x (CONJUNCT1 th0)
val th2 = CONJUNCT2 th0
in MATCH_MP IMP_from_option_eq (CONJ th1 th2) end
val th1 = make_abbrevs pat th0
val th2 = CONV_RULE (REWR_CONV (GSYM cv_rep_def)) (DISCH T th1)
val th3 = MATCH_MP cv_rep_eval th2
val th4 = MATCH_MP (MATCH_MP th3 from_to_thm) TRUTH
fun use_abbrevs Raw th = th
| use_abbrevs (Eval conv) th =
CONV_RULE (RAND_CONV (QCONV conv)) th
| use_abbrevs (Name name) th =
snd (first (fn (n,th) => n = name) (!abbrev_defs)) |> SYM
| use_abbrevs (Tuple []) th = failwith "Empty Tuples are not supported"
| use_abbrevs (Tuple [x]) th = use_abbrevs x th
| use_abbrevs (Tuple (x::xs)) th = let
val th0 = MATCH_MP to_pair_IMP th
val th1 = use_abbrevs x (CONJUNCT1 th0)
val th2 = use_abbrevs (Tuple xs) (CONJUNCT2 th0)
in MATCH_MP IMP_to_pair (CONJ th1 th2) end
| use_abbrevs (Some x) th = let
val th0 = MATCH_MP to_option_IMP th
val th1 = use_abbrevs x (CONJUNCT1 th0)
val th2 = CONJUNCT2 th0
in MATCH_MP IMP_to_option (CONJ th1 th2) end
val th5 = use_abbrevs pat th4
in DISCH_ALL th5 end;

fun cv_eval_raw tm = cv_eval_pat Raw tm;

fun cv_eval tm = cv_eval_pat (Eval EVAL) tm;

end
54 changes: 54 additions & 0 deletions src/num/theories/cv_compute/automation/cv_typeScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -284,4 +284,58 @@ Proof
Cases_on ‘v’ \\ fs [from_pair_def]
QED

Theorem from_pair_eq_IMP:
from_pair f1 f2 x = Pair y1 y2 ==>
f1 (FST x) = y1 /\ f2 (SND x) = y2
Proof
Cases_on ‘x’ \\ rw [] \\ gvs [from_pair_def]
QED

Theorem IMP_from_pair_eq:
f1 (FST x) = y1 /\ f2 (SND x) = y2 ==>
from_pair f1 f2 x = Pair y1 y2
Proof
Cases_on ‘x’ \\ rw [] \\ gvs [from_pair_def]
QED

Theorem from_option_eq_IMP:
from_option f1 x = Pair (Num 1) y1 ==>
f1 (THE x) = y1 /\ IS_SOME x
Proof
Cases_on ‘x’ \\ rw [] \\ gvs [from_option_def]
QED

Theorem IMP_from_option_eq:
f1 (THE x) = y1 /\ IS_SOME x ==>
from_option f1 x = Pair (Num 1) y1
Proof
Cases_on ‘x’ \\ rw [] \\ gvs [from_option_def]
QED

Theorem to_pair_IMP:
x = to_pair t1 t2 (Pair x1 x2) ==>
FST x = t1 x1 /\ SND x = t2 x2
Proof
rw [to_pair_def]
QED

Theorem IMP_to_pair:
FST x = y1 /\ SND x = y2 ==> x = (y1,y2)
Proof
Cases_on ‘x’ \\ gvs []
QED

Theorem to_option_IMP:
x = to_option t1 (Pair x1 x2) ==>
THE x = t1 x2 /\ IS_SOME x
Proof
rw [to_option_def]
QED

Theorem IMP_to_option:
THE x = y1 /\ IS_SOME x ==> x = SOME y1
Proof
Cases_on ‘x’ \\ gvs []
QED

val _ = export_theory();