wneuper/isa: comparison test/Tools/isac/ProgLang/prog

equal deleted inserted replaced

-:7701598a2182
+:dcb37736d573
 "-------- fun eval_const -----------------------------------------------------------------------";
 "-------- fun eval_const -----------------------------------------------------------------------";
 "-------- fun eval_const -----------------------------------------------------------------------";
 val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
 case rewrite_set_ @{theory Test} false tval_rls t of
-SOME (Const ("HOL.True", _), []) => ()
+SOME (Const (\<^const_name>\<open>True\<close>, _), []) => ()
 | _ => error "2 is_const CHANGED";
 val t = TermC.str2term "2 * x is_const";
 val SOME (str, t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
 if UnparseC.term t' = "(2 * x is_const) = False" then ()
 eval_equ: string -> string -> term -> 'a -> (string * term) option;
 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (2::real)"} "" of
 SOME
 ("#less_1_2",
-Const ("HOL.Trueprop", _) $
+Const (\<^const_name>\<open>Trueprop\<close>, _) $
-(Const ("HOL.eq", _) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $
-(Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $
+(Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $
-(Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $ Const ("Num.num.One", _)))) $
+(Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) $
-Const ("HOL.True", _))) => ()
+Const (\<^const_name>\<open>True\<close>, _))) => ()
 | _ => error "eval_equ   1 < 2   CHANGED";
 case eval_equ "#less_" "Orderings.ord_class.less" @{term "1 < (1::real)"} "" of
 SOME
 ("#less_1_1",
-Const ("HOL.Trueprop", _) $
+Const (\<^const_name>\<open>Trueprop\<close>, _) $
-(Const ("HOL.eq", _) $ (Const ("Orderings.ord_class.less", _) $ Const ("Groups.one_class.one", _) $ Const ("Groups.one_class.one", _)) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>ord_class.less\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) $
-Const ("HOL.False", _))) => ()
+Const (\<^const_name>\<open>False\<close>, _))) => ()
 | _ => error "eval_equ   1 < 1   CHANGED";
 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
 "-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";
 "---------fun eval_sameFunId -------------------------------------------------------------------";
 "---------fun eval_sameFunId -------------------------------------------------------------------";
 "---------fun eval_sameFunId -------------------------------------------------------------------";
 val t = @{term "M_b L"}; TermC.atomty t;
 val t as f1 $ _ = @{term "M_b L"};
-val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
+val t as Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _ = @{term "M_b x = c + L*x"};
 f1 = f2 (*true*);
-val (p as Const ("Prog_Expr.sameFunId",_) $
+val (p as Const (\<^const_name>\<open>sameFunId\<close>, _) $
 			(f1 $ _) $
 			(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (f2 $ _) $ _)) =
 @{term "sameFunId (M_b L) (M_b x = c + L*x)"};
 f1 = f2 (*true*);
 eval_sameFunId "" "Prog_Expr.sameFunId"
 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
 val flhs as (fid $ _) = @{term "y' L"};
 val fs = @{term "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
-val (p as Const ("Prog_Expr.filter_sameFunId",_) $ (fid $ _) $ fs) =
+val (p as Const (\<^const_name>\<open>filter_sameFunId\<close>,_) $ (fid $ _) $ fs) =
 @{term "filter_sameFunId (y' L) [M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]"};
 val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
 if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()
 else error "atools.slm diff.behav. in filter_sameFunId";
 "---------fun eval_boollist2sum ----------------------------------------------------------------";
 "---------fun eval_boollist2sum ----------------------------------------------------------------";
 "---------fun eval_boollist2sum ----------------------------------------------------------------";
-fun lhs (Const ("HOL.eq",_) $ l $ _) = l
+fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
 | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");
 "----------- \<up> redefined due to overwritten identifier -----------";
 val u_ = @{term "[]"};
 val u_ = @{term "[b1 = k - 2*q]"};
 val u_ = @{term "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
 val t = list2sum sum_;
 UnparseC.term t;
 val t = @{term "boollist2sum [b1 = k - 2*(q::real), b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"};
 case t of
-Const ("Prog_Expr.boollist2sum", _) $
+Const (\<^const_name>\<open>boollist2sum\<close>, _) $
-(Const ("List.list.Cons", _) $
+(Const (\<^const_name>\<open>Cons\<close>, _) $
-(Const ("HOL.eq", _) $ Free ("b1", _) $ _ ) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b1", _) $ _ ) $
-(Const ("List.list.Cons", _) $
+(Const (\<^const_name>\<open>Cons\<close>, _) $
-(Const ("HOL.eq", _) $ Free ("b2", _) $ _ ) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b2", _) $ _ ) $
-(Const ("List.list.Cons", _) $
+(Const (\<^const_name>\<open>Cons\<close>, _) $
-(Const ("HOL.eq", _) $ Free ("b3", _) $ _ ) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b3", _) $ _ ) $
-(Const ("List.list.Cons", _) $
+(Const (\<^const_name>\<open>Cons\<close>, _) $
-(Const ("HOL.eq", _) $ Free ("b4", _) $ _ ) $
+(Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("b4", _) $ _ ) $
-Const ("List.list.Nil", _))))) => ()
+Const (\<^const_name>\<open>Nil\<close>, _))))) => ()
 | _ => error "boollist2sum CHANGED";
 val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";
 if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()
 else error "atools.sml diff.behav. in eval_boollist2sum";
 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
 "see: --------- search for Or_to_List ---";
-case or2list @{term True} of Const ("ListC.UniversalList", _) => ()
+case or2list @{term True} of Const (\<^const_name>\<open>UniversalList\<close>, _) => ()
 | _ => error "TermC.UniversalList changed 1";
 case or2list @{term False} of Const (\<^const_name>\<open>Nil\<close>, _) => ()
 | _ => error "TermC.UniversalList changed 2";
 val t =  (TermC.str2term "x=3");
 if UnparseC.term (or2list t) = "[x = 3]" then ()

changeset 60336	dcb37736d573
parent 60331	40eb8aa2b0d6
child 60339	0d22a6bf1fc6