Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ProgLang/listC.sml
changeset 60500 59a3af532717
parent 60337 cbad4e18e91b
child 60509 2e0b7ca391dc
equal deleted inserted replaced
60499:d2407e9cb491 60500:59a3af532717 
    42 Syntax.read_term_global @{theory} "{||1,2,3||}";
 
    42 Syntax.read_term_global @{theory} "{||1,2,3||}";
 
    43 
    43 
    44 "--------------------- NTH ---------------------------------------------------";
 
    44 "--------------------- NTH ---------------------------------------------------";
 
    45 "--------------------- NTH ---------------------------------------------------";
 
    45 "--------------------- NTH ---------------------------------------------------";
 
    46 "--------------------- NTH ---------------------------------------------------";
 
    46 "--------------------- NTH ---------------------------------------------------";
 
       
    47 val ctxt = Proof_Context.init_global @{theory}
 
    47 val prog_expr = assoc_rls "prog_expr"
 
    48 val prog_expr = assoc_rls "prog_expr"
 
    48 
    49 
    49 val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
 
    50 val t = TermC.str2term "NTH 1 [a,b,c,d,e]";
 
    50 TermC.atomty t;
 
    51 TermC.atomty t;
 
    51 val thm = Thm.prop_of @{thm NTH_NIL};
 
    52 val thm = Thm.prop_of @{thm NTH_NIL};
 
    52 TermC.atomty thm;
 
    53 TermC.atomty thm;
 
    53 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false @{thm NTH_NIL} t;
 
    54 val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false @{thm NTH_NIL} t;
 
    54 if UnparseC.term t' = "a" then () 
    55 if UnparseC.term t' = "a" then () 
    55 else error "NTH 1 [a,b,c,d,e] = a ..changed";
 
    56 else error "NTH 1 [a,b,c,d,e] = a ..changed";
 
    56 
    57 
    57 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
 
    58 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
 
    58 case TermC.str2term "NTH 3 [a,b,c,d,e]" of
 
    59 case TermC.str2term "NTH 3 [a,b,c,d,e]" of
 
    63            (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
 
    64            (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("d", _) $
 
    64              (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
 
    65              (Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("e", _) $ Const (\<^const_name>\<open>Nil\<close>, _)))))) => ()
 
    65 | _ => error "ListC.NTH changed";
 
    66 | _ => error "ListC.NTH changed";
 
    66 val thm = Thm.prop_of @{thm NTH_CONS};
 
    67 val thm = Thm.prop_of @{thm NTH_CONS};
 
    67 TermC.atomty thm;
 
    68 TermC.atomty thm;
 
    68 val SOME (t', _) = rewrite_ thy dummy_ord prog_expr false  @{thm NTH_CONS} t;
 
    69 val SOME (t', _) = rewrite_ ctxt dummy_ord prog_expr false  @{thm NTH_CONS} t;
 
    69 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    70 if UnparseC.term t' = "NTH (3 + - 1) [b, c, d, e]" then () 
    70 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
 
    71 else error "NTH 3 [a,b,c,d,e] = NTH (3 + - 1) [b, c, d, e] ..changed";
 
    71 
    72 
    72 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
 
    73 (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
 
    73 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
 
    74 val t = TermC.str2term "NTH 3 [a,b,c,d,e]";
 
    74 TermC.atomty t;
 
    75 TermC.atomty t;
 
    75 Rewrite.trace_on := false; (*true false*)
 
    76 
    76 val SOME (t', _) = rewrite_set_ thy false prog_expr t;
 
    77 val SOME (t', _) = rewrite_set_ ctxt false prog_expr t;
 
    77 Rewrite.trace_on := false; (*true false*)
 
       
    78 if UnparseC.term t' = "c" then () 
    78 if UnparseC.term t' = "c" then () 
    79 else error "NTH 3 [a,b,c,d,e] = c ..changed";
 
    79 else error "NTH 3 [a,b,c,d,e] = c ..changed";
 
    80 
    80 
    81 "--------------------- Length ------------------------------------------------";
 
    81 "--------------------- Length ------------------------------------------------";
 
    82 "--------------------- Length ------------------------------------------------";
 
    82 "--------------------- Length ------------------------------------------------";
 
    83 "--------------------- Length ------------------------------------------------";
 
    83 "--------------------- Length ------------------------------------------------";
 
    84 val prog_expr = assoc_rls "prog_expr"
 
    84 val prog_expr = assoc_rls "prog_expr"
 
    85 
    85 
    86 val thy = @{theory ListC};
 
    86 val thy = @{theory ListC};
 
    87 val t = TermC.str2term "Length [1, 1, 1]";
 
    87 val t = TermC.str2term "Length [1, 1, 1]";
 
    88 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    88 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    89 UnparseC.term t = "1 + Length [1, 1]";
 
    89 UnparseC.term t = "1 + Length [1, 1]";
 
    90 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    90 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    91 UnparseC.term t = "1 + (1 + Length [1])";
 
    91 UnparseC.term t = "1 + (1 + Length [1])";
 
    92 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    92 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    93 UnparseC.term t = "1 + (1 + (1 + Length []))";
 
    93 UnparseC.term t = "1 + (1 + (1 + Length []))";
 
    94 val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    94 val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_CONS} t;
 
    95 val SOME (t, asm) = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
 
    95 val SOME (t, asm) = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
 
    96 val NONE          = rewrite_ thy tless_true tval_rls false @{thm LENGTH_NIL} t;
 
    96 val NONE          = rewrite_ ctxt tless_true tval_rls false @{thm LENGTH_NIL} t;
 
    97 if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    97 if UnparseC.term t = "1 + (1 + (1 + 0))" then () 
    98 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
 
    98 else error "Length [1, 1, 1] = 1 + (1 + (1 + 0))  ..changed";
 
    99 
    99 
   100 val t = TermC.str2term "Length [1, 1, 1]";
 
   100 val t = TermC.str2term "Length [1, 1, 1]";
 
   101 val SOME (t, asm) = rewrite_set_ thy false prog_expr t;
 
   101 val SOME (t, asm) = rewrite_set_ ctxt false prog_expr t;
 
   102 if UnparseC.term t = "3" then ()
 
   102 if UnparseC.term t = "3" then ()
 
   103 else error "Length [1, 1, 1] = 3  ..prog_expr changed";
 
   103 else error "Length [1, 1, 1] = 3  ..prog_expr changed";
 
   104 
   104 
   105 val t = TermC.str2term "Length [1, 1, 1]";
 
   105 val t = TermC.str2term "Length [1, 1, 1]";
 
   106 val t = eval_prog_expr thy prog_expr t;
 
   106 val t = eval_prog_expr ctxt prog_expr t;
 
   107 case t of 
   107 case t of 
   108   Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 
   108   Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)) => () 
   109 | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
 
   109 | _ => error "Length [1, 1, 1] = 3  ..eval_prog_expr changed";
 
   110 
   110
wneuper/isa