Merge remote-tracking branch 'origin/develop' into probability_dev

Manual/Developers/developers.md

@@ -151,7 +151,7 @@ Under both Moscow ML and Poly/ML the following are created:
 : This tool creates LaTeX mungers, as described in the *DESCRIPTION* manual.
 
 `unquote`
-: This is the quotation filter embodied as a Unix filter, with a variety of options to specify behaviour. Note that this is not used by Poly/ML HOL, but can be useful there to see what the filter (as embodied by the `QFRead` module) is doing when it messes with user input.
+: This is the quotation filter embodied as a Unix filter, with a variety of options to specify behaviour. Note that this is not used by Poly/ML HOL, but can be useful there to see what the filter (as embodied by the `HolParser` module) is doing when it messes with user input.
 
 Under Poly/ML, the following additional files will appear:
 

examples/cv_compute/cv_eval_exampleScript.sml

@@ -0,0 +1,38 @@
+(*
+  Demonstrates use of cv_eval_pat
+*)
+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;
+
+(* 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)
+*)
+
+val res = cv_eval “LENGTH big_replicate”;
+(* returns:
+     ⊢ LENGTH big_replicate = 10000
+*)
+
+val _ = (max_print_depth := 10);
+val _ = export_theory();

examples/separationLogic/src/holfoot/poly/build-state.hol

@@ -31,8 +31,6 @@ val _ = holfoot_auto_verify_spec (examplesDir ^ "/automatic/list.sf")
 val _ = holfoot_verify_spec (examplesDir ^ "/automatic/mergesort.sf") [];
 
 
-use (Globals.HOLDIR ^ "/tools/Holmake/QuoteFilter.sml");
-
 val _ = HOL_Interactive.toggle_quietdec();
 
 (* save state *)

src/1/TypeBase.sml

@@ -65,11 +65,7 @@ val bool_info =
       {ax=ORIG boolTheory.boolAxiom,
        induction = ORIG boolTheory.bool_INDUCT,
        case_def = boolTheory.bool_case_thm,
-       case_eq =
-         Prim_rec.prove_case_eq_thm{
-           case_def = boolTheory.bool_case_thm,
-           nchotomy = boolTheory.BOOL_CASES_AX
-         },
+       case_eq = boolTheory.bool_case_eq,
        case_elim =
          Prim_rec.prove_case_ho_elim_thm{
            case_def = boolTheory.bool_case_thm,

src/bool/boolScript.sml

@@ -3534,6 +3534,64 @@ in
            COND_CLAUSES |> SPECL vs |> CONJUNCTS |> map (GENL vs) |> LIST_CONJ)
 end
 
+
+(*---------------------------------------------------------------------------
+    bool_case_eq =
+        |- (bool_case t1 t2 x = v) <=>
+        (x <=> T) /\ t1 = v \/ (x <=> F) /\ t2 = v
+ ---------------------------------------------------------------------------*)
+val bool_case_eq = thm (#(FILE), #(LINE))("bool_case_eq",
+let val x    = “x:bool”
+    val t1   = “t1:'a”
+    val t2   = “t2:'a”
+    val v    = “v:'a”
+    val eq = “$=”
+    val conj = “$/\”
+    val disj = “$\/”
+    val tm1 = “t1 = v”
+    val tm2 = “t2 = v”
+    val [COND1, COND2] = (CONJUNCTS (SPEC t2 (SPEC t1 COND_CLAUSES)))
+    and [OR1,OR2,OR3,OR4,_] = map GEN_ALL (CONJUNCTS (SPEC_ALL OR_CLAUSES))
+    and [AND1,AND2,AND3,AND4,_] = map GEN_ALL (CONJUNCTS(SPEC_ALL AND_CLAUSES))
+    val thmT1 = AP_THM (AP_TERM eq COND1) v
+    val thmF1 = AP_THM (AP_TERM eq COND2) v
+    val [TF,FT] = map EQF_INTRO (CONJUNCTS BOOL_EQ_DISTINCT)
+    val [TT,FF] = map (EQT_INTRO o REFL) [“T”,“F”]
+    val thmT2 =
+      let
+          val thml1 = AP_THM (AP_TERM conj TT) tm1
+          val thml2 = SPEC tm1 AND1
+          val thml = TRANS thml1 thml2
+          val thmr1 = AP_THM (AP_TERM conj TF) tm2
+          val thmr2 = SPEC tm2 AND3
+          val thmr = TRANS thmr1 thmr2
+          val thm1 = MK_COMB (AP_TERM disj thml, thmr)
+      in
+          TRANS thm1 (SPEC tm1 OR4)
+      end
+    val thmF2 =
+      let
+          val thmr1 = AP_THM (AP_TERM conj FF) tm2
+          val thmr2 = SPEC tm2 AND1
+          val thmr = TRANS thmr1 thmr2
+          val thml1 = AP_THM (AP_TERM conj FT) tm1
+          val thml2 = SPEC tm1 AND3
+          val thml = TRANS thml1 thml2
+          val thm1 = MK_COMB (AP_TERM disj thml, thmr)
+      in
+          TRANS thm1 (SPEC tm2 OR3)
+      end
+    val thmT3 = TRANS thmT1 (SYM thmT2)
+    val thmF3 = TRANS thmF1 (SYM thmF2)
+    val tm = “(if x then t1 else t2) = v <=> (((x <=> T) /\ t1 = v) \/ ((x <=> F) /\ t2 = v))”
+    val thT4 = SUBST_CONV [x |-> ASSUME “x = T”] tm tm
+    and thF4 = SUBST_CONV [x |-> ASSUME “x = F”] tm tm
+    val thmT = EQ_MP (SYM thT4) thmT3
+    val thmF = EQ_MP (SYM thF4) thmF3
+ in
+    DISJ_CASES (SPEC x BOOL_CASES_AX) thmT thmF
+ end);
+
 (* ------------------------------------------------------------------------- *)
 (*    bool_case_ID = |- !x b. bool_case x x b = x                            *)
 (* ------------------------------------------------------------------------- *)

src/num/theories/cv_compute/automation/cv_transLib.sig

@@ -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
 

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 tm = let
+datatype pat = Raw
+             | Eval of conv
+             | Name of string
+             | Tuple of pat list
+             | 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
@@ -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

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();

tools-poly/configure.sml

@@ -426,7 +426,6 @@ val _ = work_in_dir
           "Holmake" (fullPath [HOLDIR, "tools", "Holmake", "poly"])
           (fn () => (OS.FileSys.chDir "..";
                      systeml [lexer, "HolLex"];
-                     systeml [lexer, "QuoteFilter"];
                      OS.FileSys.chDir "poly";
                      polyc_compile (SOME "../mlton/Holmake.mlb")
                                    "poly-Holmake.ML" hmakebin))

tools-poly/poly/poly-init2.ML

@@ -7,7 +7,6 @@ val _ = use "Holmake/Systeml.sml"
 val _ = use "../tools/Holmake/AttributeSyntax.sig";
 val _ = use "../tools/Holmake/AttributeSyntax.sml";
 val _ = use "../tools/Holmake/HolLex.sml";
-val _ = use "../tools/Holmake/QuoteFilter.sml";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sig";
 val _ = use "../tools/Holmake/HM_SimpleBuffer.sml";
 val _ = use "../tools/Holmake/HOLFS_dtype.sml";
@@ -16,8 +15,6 @@ val _ = use "../tools/Holmake/poly/HFS_NameMunge.sml";
 val _ = use "../tools/Holmake/HOLFS_dtype.sml";
 val _ = use "../tools/Holmake/HOLFileSys.sig";
 val _ = use "../tools/Holmake/HOLFileSys.sml";
-val _ = use "../tools/Holmake/QFRead.sig";
-val _ = use "../tools/Holmake/QFRead.sml";
 val _ = use "../tools/Holmake/HolParser.sig";
 val _ = use "../tools/Holmake/HolParser.sml";
 val _ = use "poly/quse.sig";

tools/Holmake/.gitignore

@@ -1,2 +1 @@
-QuoteFilter.sml
 HolLex.sml

tools/Holmake/HolParser.sml

@@ -309,8 +309,6 @@ structure ToSML = struct
     val filename = ref filename
     val {read, readAt} = mkDoubleReader read 0
     val feed = mkParser {read = read, pos = ~1 (* fix for mllex bug *), parseError = parseError}
-    val lookahead = ref NONE
-    fun feed' () = case !lookahead of SOME tk => tk | NONE => feed ()
     val inThmVal = ref false
     fun finishThmVal () = if !inThmVal then (aux ");"; inThmVal := false) else ()
     val line = ref (0, 0)
@@ -551,7 +549,7 @@ structure ToSML = struct
     and doDecls start [] stop = regular (start, stop)
       | doDecls start (d :: ds) stop = doDecls (doDecl false start d) ds stop
     in {
-      feed = feed',
+      feed = feed,
       regular = regular,
       finishThmVal = finishThmVal,
       doDecl = doDecl
@@ -595,8 +593,6 @@ fun exhaust_parser (read, close) =
     recurse []
   end
 
-fun mkstate b = {inscriptp = b, quotefixp = false}
-
 fun file_to_parser fname = let
   val instrm = openIn fname
   (* val isscript = String.isSuffix "Script.sml" fname *)