From 004092810bf08314a763836287750dbb433e689c Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 24 Feb 2025 12:45:20 +0100 Subject: [PATCH 1/6] Add cv_eval_raw_save to cv_transLib (and an example) --- examples/cv_compute/cv_eval_exampleScript.sml | 20 +++++++++++ .../cv_compute/automation/cv_transLib.sig | 7 ++-- .../cv_compute/automation/cv_transLib.sml | 33 +++++++++++++++---- 3 files changed, 51 insertions(+), 9 deletions(-) create mode 100644 examples/cv_compute/cv_eval_exampleScript.sml diff --git a/examples/cv_compute/cv_eval_exampleScript.sml b/examples/cv_compute/cv_eval_exampleScript.sml new file mode 100644 index 0000000000..10257bde59 --- /dev/null +++ b/examples/cv_compute/cv_eval_exampleScript.sml @@ -0,0 +1,20 @@ +(* + Demonstrates use of cv_eval_raw_save +*) +open HolKernel Parse boolLib bossLib; +open cv_transLib cv_stdTheory + +val _ = new_theory "cv_eval_example"; + +val (def, res) = cv_eval_raw_save "big_replicate" “REPLICATE 100000 T” +(* returns: + def: ⊢ big_replicate = REPLICATE 100000 T + res: ⊢ big_replicate = to_list cv$c2b (cv_big_replicate (Num 0)) + where cv_big_replicate is a constant holding the huge cv value *) + +val res = cv_eval “LENGTH big_replicate”; +(* returns: + res: ⊢ LENGTH big_replicate = 100000 *) + +val _ = (max_print_depth := 10); +val _ = export_theory(); diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sig b/src/num/theories/cv_compute/automation/cv_transLib.sig index 4124865ba2..faad391a79 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sig +++ b/src/num/theories/cv_compute/automation/cv_transLib.sig @@ -15,9 +15,10 @@ sig (* The conv should evaluate `from ` *) 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 + val cv_eqs_for : term -> thm list + val cv_eval : term -> thm + val cv_eval_raw : term -> thm + val cv_eval_raw_save : string -> term -> thm * thm val cv_termination_tac : tactic diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index 1feb53b86a..38db210f87 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -876,7 +876,7 @@ fun cv_eqs_for tm = let val _ = computeLib.add_funs [cv_fst_def,cv_snd_def]; -fun cv_eval_raw tm = let +fun cv_eval_raw_gen tm save_name = 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 @@ -887,13 +887,34 @@ 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 _ = cv_print Verbose "Calling cv_compute.\n" + val th0 = th |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) cv_conv) + val (abbrev_def,thA) = + case save_name of NONE => (TRUTH,th0) | SOME name => let + fun cv_def_conv tm = let + 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)),tm) + val cv_def = new_definition("cv_" ^ name ^ "_def", def_eq) + in SPEC num_0 cv_def |> SYM end + val th0a = th0 |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) cv_def_conv) + val tm = th0a |> concl |> rand + val abbrev_def = new_definition(name ^ "_def",mk_eq(mk_var(name,type_of tm),tm)) + val th0b = th0a |> CONV_RULE (RAND_CONV (fn tm => SYM abbrev_def)) + val th0c = th0b |> CONV_RULE (REWR_CONV cv_rep_def) + val th0d = remove_T_IMP (DISCH_ALL th0c) handle HOL_ERR _ => th0c + val _ = save_thm("cv_" ^ name ^ "_thm[cv_rep]",th0d) + in (abbrev_def,th0b) end + val th1 = MATCH_MP cv_rep_eval thA 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; + val th4 = remove_T_IMP (DISCH_ALL th3) + in (abbrev_def,th4) end; + +fun cv_eval_raw_save save_name tm = cv_eval_raw_gen tm (SOME save_name); + +fun cv_eval_raw tm = snd (cv_eval_raw_gen tm NONE); fun cv_eval tm = let val th = cv_eval_raw tm From 3d6d2d5534c16a40ed674abac2554d51f910af17 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 24 Feb 2025 22:35:31 +0100 Subject: [PATCH 2/6] Generalise interface --- examples/cv_compute/cv_eval_exampleScript.sml | 18 +++- .../cv_compute/automation/cv_transLib.sig | 14 ++- .../cv_compute/automation/cv_transLib.sml | 97 ++++++++++++------- .../cv_compute/automation/cv_typeScript.sml | 54 +++++++++++ 4 files changed, 140 insertions(+), 43 deletions(-) diff --git a/examples/cv_compute/cv_eval_exampleScript.sml b/examples/cv_compute/cv_eval_exampleScript.sml index 10257bde59..301e069780 100644 --- a/examples/cv_compute/cv_eval_exampleScript.sml +++ b/examples/cv_compute/cv_eval_exampleScript.sml @@ -6,15 +6,23 @@ open cv_transLib cv_stdTheory val _ = new_theory "cv_eval_example"; -val (def, res) = cv_eval_raw_save "big_replicate" “REPLICATE 100000 T” +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 (Pair (Eval EVAL, Pair (Raw, Name "big_replicate"))); + +val res = cv_eval_pat pat “test 10000”; (* returns: - def: ⊢ big_replicate = REPLICATE 100000 T - res: ⊢ big_replicate = to_list cv$c2b (cv_big_replicate (Num 0)) - where cv_big_replicate is a constant holding the huge cv value *) + ⊢ test 10000 = SOME (10001,cv$c2n (Num 10002),big_replicate) +*) val res = cv_eval “LENGTH big_replicate”; (* returns: - res: ⊢ LENGTH big_replicate = 100000 *) + ⊢ LENGTH big_replicate = 10000 +*) val _ = (max_print_depth := 10); val _ = export_theory(); diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sig b/src/num/theories/cv_compute/automation/cv_transLib.sig index faad391a79..c692937f17 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sig +++ b/src/num/theories/cv_compute/automation/cv_transLib.sig @@ -15,10 +15,16 @@ sig (* The conv should evaluate `from ` *) val cv_trans_deep_embedding : conv -> thm -> unit - val cv_eqs_for : term -> thm list - val cv_eval : term -> thm - val cv_eval_raw : term -> thm - val cv_eval_raw_save : string -> term -> thm * thm + datatype pat = Raw + | Eval of conv + | Name of string + | Pair of pat * pat + | 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 diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index 38db210f87..d113ed0714 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -876,7 +876,13 @@ fun cv_eqs_for tm = let val _ = computeLib.add_funs [cv_fst_def,cv_snd_def]; -fun cv_eval_raw_gen tm save_name = let +datatype pat = Raw + | Eval of conv + | Name of string + | Pair of pat * pat + | Some of pat; + +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 @@ -889,38 +895,61 @@ fun cv_eval_raw_gen tm save_name = let val cv_conv = cv_computeLib.cv_compute cv_eqs val _ = cv_print Verbose "Calling cv_compute.\n" val th0 = th |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) cv_conv) - val (abbrev_def,thA) = - case save_name of NONE => (TRUTH,th0) | SOME name => let - fun cv_def_conv tm = let - 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)),tm) - val cv_def = new_definition("cv_" ^ name ^ "_def", def_eq) - in SPEC num_0 cv_def |> SYM end - val th0a = th0 |> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV) cv_def_conv) - val tm = th0a |> concl |> rand - val abbrev_def = new_definition(name ^ "_def",mk_eq(mk_var(name,type_of tm),tm)) - val th0b = th0a |> CONV_RULE (RAND_CONV (fn tm => SYM abbrev_def)) - val th0c = th0b |> CONV_RULE (REWR_CONV cv_rep_def) - val th0d = remove_T_IMP (DISCH_ALL th0c) handle HOL_ERR _ => th0c - val _ = save_thm("cv_" ^ name ^ "_thm[cv_rep]",th0d) - in (abbrev_def,th0b) end - val th1 = MATCH_MP cv_rep_eval thA - val th2 = MATCH_MP th1 from_to_thm - val th3 = th2 |> UNDISCH_ALL - val th4 = remove_T_IMP (DISCH_ALL th3) - in (abbrev_def,th4) end; - -fun cv_eval_raw_save save_name tm = cv_eval_raw_gen tm (SOME save_name); - -fun cv_eval_raw tm = snd (cv_eval_raw_gen tm NONE); - -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; + |> 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 (Pair (x,y)) th = let + val th0 = MATCH_MP from_pair_eq_IMP th + val th1 = make_abbrevs x (CONJUNCT1 th0) + val th2 = make_abbrevs y (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 (Pair (x,y)) th = let + val th0 = MATCH_MP to_pair_IMP th + val th1 = use_abbrevs x (CONJUNCT1 th0) + val th2 = use_abbrevs y (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 th5 end; + +fun cv_eval_raw tm = cv_eval_pat Raw tm; + +fun cv_eval tm = cv_eval_pat (Eval EVAL) tm; end diff --git a/src/num/theories/cv_compute/automation/cv_typeScript.sml b/src/num/theories/cv_compute/automation/cv_typeScript.sml index d2fb5a2936..509719f5d2 100644 --- a/src/num/theories/cv_compute/automation/cv_typeScript.sml +++ b/src/num/theories/cv_compute/automation/cv_typeScript.sml @@ -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(); From f1f464407cf261e022fb910c6565fbc7490cd11a Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 25 Feb 2025 10:26:21 +0100 Subject: [PATCH 3/6] Try to better match old behaviour --- src/num/theories/cv_compute/automation/cv_transLib.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index d113ed0714..7fe9cb6e17 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -946,7 +946,7 @@ fun cv_eval_pat pat tm = let val th2 = CONJUNCT2 th0 in MATCH_MP IMP_to_option (CONJ th1 th2) end val th5 = use_abbrevs pat th4 - in th5 end; + in UNDISCH_ALL th5 end; fun cv_eval_raw tm = cv_eval_pat Raw tm; From 54bc88cde1ca44f96b1596f303c05060d8bba2af Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 25 Feb 2025 10:26:59 +0100 Subject: [PATCH 4/6] UNDISCH --> DISCH --- src/num/theories/cv_compute/automation/cv_transLib.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index 7fe9cb6e17..b167d8c14b 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -946,7 +946,7 @@ fun cv_eval_pat pat tm = let val th2 = CONJUNCT2 th0 in MATCH_MP IMP_to_option (CONJ th1 th2) end val th5 = use_abbrevs pat th4 - in UNDISCH_ALL th5 end; + in DISCH_ALL th5 end; fun cv_eval_raw tm = cv_eval_pat Raw tm; From bd8568b56db0d54019a6443e14bd207a1620f3de Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 26 Feb 2025 11:48:06 +0100 Subject: [PATCH 5/6] Change Pair to Tuple in new pat datatype --- examples/cv_compute/cv_eval_exampleScript.sml | 2 +- .../theories/cv_compute/automation/cv_transLib.sig | 2 +- .../theories/cv_compute/automation/cv_transLib.sml | 14 +++++++++----- 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/examples/cv_compute/cv_eval_exampleScript.sml b/examples/cv_compute/cv_eval_exampleScript.sml index 301e069780..b4c77ec725 100644 --- a/examples/cv_compute/cv_eval_exampleScript.sml +++ b/examples/cv_compute/cv_eval_exampleScript.sml @@ -12,7 +12,7 @@ End val _ = cv_trans test_def; -val pat = Some (Pair (Eval EVAL, Pair (Raw, Name "big_replicate"))); +val pat = Some (Tuple [Eval EVAL, Raw, Name "big_replicate"]); val res = cv_eval_pat pat “test 10000”; (* returns: diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sig b/src/num/theories/cv_compute/automation/cv_transLib.sig index c692937f17..539380702f 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sig +++ b/src/num/theories/cv_compute/automation/cv_transLib.sig @@ -18,7 +18,7 @@ sig datatype pat = Raw | Eval of conv | Name of string - | Pair of pat * pat + | Tuple of pat list | Some of pat; val cv_eqs_for : term -> thm list diff --git a/src/num/theories/cv_compute/automation/cv_transLib.sml b/src/num/theories/cv_compute/automation/cv_transLib.sml index b167d8c14b..40ef295d98 100644 --- a/src/num/theories/cv_compute/automation/cv_transLib.sml +++ b/src/num/theories/cv_compute/automation/cv_transLib.sml @@ -879,7 +879,7 @@ val _ = computeLib.add_funs [cv_fst_def,cv_snd_def]; datatype pat = Raw | Eval of conv | Name of string - | Pair of pat * pat + | Tuple of pat list | Some of pat; fun cv_eval_pat pat tm = let @@ -916,10 +916,12 @@ fun cv_eval_pat pat tm = let 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 (Pair (x,y)) th = let + | 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 y (CONJUNCT2 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 @@ -935,10 +937,12 @@ fun cv_eval_pat pat tm = let CONV_RULE (RAND_CONV (QCONV conv)) th | use_abbrevs (Name name) th = snd (first (fn (n,th) => n = name) (!abbrev_defs)) |> SYM - | use_abbrevs (Pair (x,y)) th = let + | 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 y (CONJUNCT2 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 From e211611d3319151d421bac5caee5265866f6ec7b Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 27 Feb 2025 08:58:15 +0100 Subject: [PATCH 6/6] Fix a comment and add new comment --- examples/cv_compute/cv_eval_exampleScript.sml | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/examples/cv_compute/cv_eval_exampleScript.sml b/examples/cv_compute/cv_eval_exampleScript.sml index b4c77ec725..cc5918c25c 100644 --- a/examples/cv_compute/cv_eval_exampleScript.sml +++ b/examples/cv_compute/cv_eval_exampleScript.sml @@ -1,5 +1,5 @@ (* - Demonstrates use of cv_eval_raw_save + Demonstrates use of cv_eval_pat *) open HolKernel Parse boolLib bossLib; open cv_transLib cv_stdTheory @@ -12,9 +12,19 @@ End val _ = cv_trans test_def; -val pat = Some (Tuple [Eval EVAL, Raw, Name "big_replicate"]); - -val res = cv_eval_pat pat “test 10000”; +(* 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. +*) +val res = cv_eval_pat + (Some (Tuple [Eval EVAL, Raw, Name "big_replicate"])) + “test 10000”; (* returns: ⊢ test 10000 = SOME (10001,cv$c2n (Num 10002),big_replicate) *)