# HG changeset patch # User haftmann # Date 1139933268 -3600 # Node ID 8eae46249628fbc216cee211ecdf725b42910723 # Parent 62c5f7591a433734d1383bb3de3614832c94522e added theory of executable rational numbers diff -r 62c5f7591a43 -r 8eae46249628 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Feb 14 17:07:11 2006 +0100 +++ b/src/HOL/HOL.thy Tue Feb 14 17:07:48 2006 +0100 @@ -1397,9 +1397,9 @@ "op -->" "HOL.op_implies" "op &" "HOL.op_and" "op |" "HOL.op_or" - "op +" "IntDef.op_add" - "op -" "IntDef.op_minus" - "op *" "IntDef.op_times" + "op +" "HOL.op_add" + "op -" "HOL.op_minus" + "op *" "HOL.op_times" Not "HOL.not" uminus "HOL.uminus" arbitrary "HOL.arbitrary" @@ -1419,9 +1419,9 @@ ml (infixl 0 "orelse") haskell (infixl 2 "||") If - ml ("if __/ then __/ else __") - haskell ("if __/ then __/ else __") - "op =" (* an intermediate solution *) + ml (target_atom "(if __/ then __/ else __)") + haskell (target_atom "(if __/ then __/ else __)") + "op =" (* an intermediate solution for polymorphic equality *) ml (infixl 6 "=") haskell (infixl 4 "==") arbitrary diff -r 62c5f7591a43 -r 8eae46249628 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Feb 14 17:07:11 2006 +0100 +++ b/src/HOL/IsaMakefile Tue Feb 14 17:07:48 2006 +0100 @@ -183,7 +183,7 @@ $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ Library/SetsAndFunctions.thy Library/BigO.thy \ - Library/EfficientNat.thy Library/ExecutableSet.thy \ + Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \ Library/FuncSet.thy Library/Library.thy \ Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \ Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \ diff -r 62c5f7591a43 -r 8eae46249628 src/HOL/Library/ExecutableRat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ExecutableRat.thy Tue Feb 14 17:07:48 2006 +0100 @@ -0,0 +1,197 @@ +ML {* + +fun strip_abs_split 0 t = ([], t) + | strip_abs_split i (Abs (s, T, t)) = + let + val s' = Codegen.new_name t s; + val v = Free (s', T) + in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end + | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of + (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u) + | _ => ([], u)) + | strip_abs_split i t = ([], t); + +fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of + (t1 as Const ("Let", _), t2 :: t3 :: ts) => + let + fun dest_let (l as Const ("Let", _) $ t $ u) = + (case strip_abs_split 1 u of + ([p], u') => apfst (cons (p, t)) (dest_let u') + | _ => ([], l)) + | dest_let t = ([], t); + fun mk_code (gr, (l, r)) = + let + val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l); + val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r); + in (gr2, (pl, pr)) end + in case dest_let (t1 $ t2 $ t3) of + ([], _) => NONE + | (ps, u) => + let + val (gr1, qs) = foldl_map mk_code (gr, ps); + val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u); + val (gr3, pargs) = foldl_map + (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts) + in + SOME (gr3, Codegen.mk_app brack + (Pretty.blk (0, [Pretty.str "let ", Pretty.blk (0, List.concat + (separate [Pretty.str ";", Pretty.brk 1] (map (fn (pl, pr) => + [Pretty.block [Pretty.str "val ", pl, Pretty.str " =", + Pretty.brk 1, pr]]) qs))), + Pretty.brk 1, Pretty.str "in ", pu, + Pretty.brk 1, Pretty.str "end"])) pargs) + end + end + | _ => NONE); + +fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of + (t1 as Const ("split", _), t2 :: ts) => + (case strip_abs_split 1 (t1 $ t2) of + ([p], u) => + let + val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p); + val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u); + val (gr3, pargs) = foldl_map + (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts) + in + SOME (gr2, Codegen.mk_app brack + (Pretty.block [Pretty.str "(fn ", q, Pretty.str " =>", + Pretty.brk 1, pu, Pretty.str ")"]) pargs) + end + | _ => NONE) + | _ => NONE); + +val prod_codegen_setup = + Codegen.add_codegen "let_codegen" let_codegen #> + Codegen.add_codegen "split_codegen" split_codegen #> + CodegenPackage.add_appconst + ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #> + CodegenPackage.add_appconst + ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split)); + +*} + +(* Title: HOL/Library/ExecutableRat.thy + ID: $Id$ + Author: Florian Haftmann, TU Muenchen +*) + +header {* Executable implementation of rational numbers in HOL *} + +theory ExecutableRat +imports "~~/src/HOL/Real/Rational" "~~/src/HOL/NumberTheory/IntPrimes" +begin + +text {* + Actually nothing is proved about the implementation. +*} + +datatype erat = Rat bool int int + +instance erat :: zero by intro_classes +instance erat :: one by intro_classes +instance erat :: plus by intro_classes +instance erat :: minus by intro_classes +instance erat :: times by intro_classes +instance erat :: inverse by intro_classes +instance erat :: ord by intro_classes + +consts + norm :: "erat \ erat" + common :: "(int * int) * (int * int) \ (int * int) * int" + of_quotient :: "int * int \ erat" + of_rat :: "rat \ erat" + to_rat :: "erat \ rat" + +defs + norm_def [simp]: "norm r == case r of (Rat a p q) \ + if p = 0 then Rat True 0 1 + else + let + absp = abs p + in let + m = zgcd (absp, q) + in Rat (a = (0 <= p)) (absp div m) (q div m)" + common_def [simp]: "common r == case r of ((p1, q1), (p2, q2)) \ + let q' = q1 * q2 div int (gcd (nat q1, nat q2)) + in ((p1 * (q' div q1), p2 * (q' div q2)), q')" + of_quotient_def [simp]: "of_quotient r == case r of (a, b) \ + norm (Rat True a b)" + of_rat_def [simp]: "of_rat r == of_quotient (THE s. s : Rep_Rat r)" + to_rat_def [simp]: "to_rat r == case r of (Rat a p q) \ + if a then Fract p q else Fract (uminus p) q" + +consts + zero :: erat + one :: erat + add :: "erat \ erat \ erat" + neg :: "erat \ erat" + mult :: "erat \ erat \ erat" + inv :: "erat \ erat" + le :: "erat \ erat \ bool" + +defs (overloaded) + zero_rat_def [simp]: "0 == Rat False 0 1" + one_rat_def [simp]: "1 == Rat False 1 1" + add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ + let + ((r1, r2), den) = common ((p1, q1), (p2, q2)) + in let + num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2) + in norm (Rat True num den)" + uminus_rat_def [simp]: "- r == case r of Rat a p q \ + if p = 0 then Rat a p q + else Rat (\ a) p q" + times_rat_def [simp]: "r * s == case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ + norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))" + inverse_rat_def [simp]: "inverse r == case r of Rat a p q \ + if p = 0 then arbitrary + else Rat a q p" + le_rat_def [simp]: "r <= s == case r of Rat a1 p1 q1 \ case s of Rat a2 p2 q2 \ + (\ a1 \ a2) \ + (\ (a1 \ \ a2) \ + (let + ((r1, r2), dummy) = common ((p1, q1), (p2, q2)) + in if a1 then r1 <= r2 else r2 <= r1))" + +code_syntax_tyco rat + ml (target_atom "{*erat*}") + haskell (target_atom "{*erat*}") + +code_alias + (* an intermediate solution until name resolving of ad-hoc overloaded + constants is refined *) + "HOL.inverse" "Rational.inverse" + "HOL.divide" "Rational.divide" + +code_syntax_const + Fract + ml ("{*of_quotient*}") + haskell ("{*of_quotient*}") + 0 :: "rat" + ml ("{*0::erat*}") + haskell ("{*1::erat*}") + 1 :: "rat" + ml ("{*1::erat*}") + haskell ("{*1::erat*}") + "op +" :: "rat \ rat \ rat" + ml ("{*op + :: erat \ erat \ erat*}") + haskell ("{*op + :: erat \ erat \ erat*}") + uminus :: "rat \ rat" + ml ("{*uminus :: erat \ erat*}") + haskell ("{*uminus :: erat \ erat*}") + "op *" :: "rat \ rat \ rat" + ml ("{*op * :: erat \ erat \ erat*}") + haskell ("{*op * :: erat \ erat \ erat*}") + inverse :: "rat \ rat" + ml ("{*inverse :: erat \ erat*}") + haskell ("{*inverse :: erat \ erat*}") + divide :: "rat \ rat \ rat" + ml ("{*op * :: erat \ erat \ erat*}/ _/ ({*inverse :: erat \ erat*}/ _)") + haskell ("{*op * :: erat \ erat \ erat*}/ _/ ({*inverse :: erat \ erat*}/ _)") + "op <=" :: "rat \ rat \ bool" + ml ("{*op <= :: erat \ erat \ bool*}") + haskell ("{*op <= :: erat \ erat \ bool*}") + +end + diff -r 62c5f7591a43 -r 8eae46249628 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue Feb 14 17:07:11 2006 +0100 +++ b/src/HOL/Orderings.thy Tue Feb 14 17:07:48 2006 +0100 @@ -706,7 +706,7 @@ subsection {* Code generator setup *} code_alias - "op <=" "IntDef.op_le" - "op <" "IntDef.op_lt" + "op <=" "Orderings.op_le" + "op <" "Orderings.op_lt" end diff -r 62c5f7591a43 -r 8eae46249628 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Feb 14 17:07:11 2006 +0100 +++ b/src/HOL/Product_Type.thy Tue Feb 14 17:07:48 2006 +0100 @@ -808,36 +808,22 @@ ML {* -signature PRODUCT_TYPE_CODEGEN = -sig - val strip_abs: int -> term -> term list * term; -end; - -structure ProductTypeCodegen : PRODUCT_TYPE_CODEGEN = -struct - -fun strip_abs 0 t = ([], t) - | strip_abs i (Abs (s, T, t)) = +fun strip_abs_split 0 t = ([], t) + | strip_abs_split i (Abs (s, T, t)) = let val s' = Codegen.new_name t s; val v = Free (s', T) - in apfst (cons v) (strip_abs (i-1) (subst_bound (v, t))) end - | strip_abs i (u as Const ("split", _) $ t) = (case strip_abs (i+1) t of + in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end + | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u) | _ => ([], u)) - | strip_abs i t = ([], t); - -end; - -local - -open ProductTypeCodegen; + | strip_abs_split i t = ([], t); fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of (t1 as Const ("Let", _), t2 :: t3 :: ts) => let fun dest_let (l as Const ("Let", _) $ t $ u) = - (case strip_abs 1 u of + (case strip_abs_split 1 u of ([p], u') => apfst (cons (p, t)) (dest_let u') | _ => ([], l)) | dest_let t = ([], t); @@ -868,7 +854,7 @@ fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of (t1 as Const ("split", _), t2 :: ts) => - (case strip_abs 1 (t1 $ t2) of + (case strip_abs_split 1 (t1 $ t2) of ([p], u) => let val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p); @@ -883,17 +869,14 @@ | _ => NONE) | _ => NONE); -in - val prod_codegen_setup = Codegen.add_codegen "let_codegen" let_codegen #> Codegen.add_codegen "split_codegen" split_codegen #> CodegenPackage.add_appconst - ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs)) #> + ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #> CodegenPackage.add_appconst - ("split", ((1, 1), CodegenPackage.appgen_split strip_abs)); + ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split)); -end; *} setup prod_codegen_setup