# HG changeset patch # User haftmann # Date 1178540432 -7200 # Node ID e795b5a031af623fc48b0423a4e4c7a5eccf5013 # Parent 3c41e8492ba67b75f30ae09ddb258cf1571b670f added further equality example diff -r 3c41e8492ba6 -r e795b5a031af doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML Mon May 07 14:20:32 2007 +0200 @@ -0,0 +1,338 @@ +structure ROOT = +struct + +structure Nat = +struct + +datatype nat = Zero_nat | Suc of nat; + +fun plus_nat (Suc m) n = plus_nat m (Suc n) + | plus_nat Zero_nat n = n; + +fun op_eq_nat Zero_nat (Suc m) = false + | op_eq_nat (Suc n) Zero_nat = false + | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m + | op_eq_nat Zero_nat Zero_nat = true; + +end; (*struct Nat*) + +structure Code_Generator = +struct + +type 'a eq = {op_eq : 'a -> 'a -> bool}; +fun op_eq (A_:'a eq) = #op_eq A_; + +end; (*struct Code_Generator*) + +structure List = +struct + +datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | + Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB | + NibbleC | NibbleD | NibbleE | NibbleF; + +datatype char = Char of nibble * nibble; + +fun zip xs (y :: ys) = + (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys) + | zip xs [] = []; + +fun null (x :: xs) = false + | null [] = true; + +fun op_eq_nibble Nibble0 Nibble0 = true + | op_eq_nibble Nibble1 Nibble1 = true + | op_eq_nibble Nibble2 Nibble2 = true + | op_eq_nibble Nibble3 Nibble3 = true + | op_eq_nibble Nibble4 Nibble4 = true + | op_eq_nibble Nibble5 Nibble5 = true + | op_eq_nibble Nibble6 Nibble6 = true + | op_eq_nibble Nibble7 Nibble7 = true + | op_eq_nibble Nibble8 Nibble8 = true + | op_eq_nibble Nibble9 Nibble9 = true + | op_eq_nibble NibbleA NibbleA = true + | op_eq_nibble NibbleB NibbleB = true + | op_eq_nibble NibbleC NibbleC = true + | op_eq_nibble NibbleD NibbleD = true + | op_eq_nibble NibbleE NibbleE = true + | op_eq_nibble NibbleF NibbleF = true + | op_eq_nibble Nibble0 Nibble1 = false + | op_eq_nibble Nibble0 Nibble2 = false + | op_eq_nibble Nibble0 Nibble3 = false + | op_eq_nibble Nibble0 Nibble4 = false + | op_eq_nibble Nibble0 Nibble5 = false + | op_eq_nibble Nibble0 Nibble6 = false + | op_eq_nibble Nibble0 Nibble7 = false + | op_eq_nibble Nibble0 Nibble8 = false + | op_eq_nibble Nibble0 Nibble9 = false + | op_eq_nibble Nibble0 NibbleA = false + | op_eq_nibble Nibble0 NibbleB = false + | op_eq_nibble Nibble0 NibbleC = false + | op_eq_nibble Nibble0 NibbleD = false + | op_eq_nibble Nibble0 NibbleE = false + | op_eq_nibble Nibble0 NibbleF = false + | op_eq_nibble Nibble1 Nibble2 = false + | op_eq_nibble Nibble1 Nibble3 = false + | op_eq_nibble Nibble1 Nibble4 = false + | op_eq_nibble Nibble1 Nibble5 = false + | op_eq_nibble Nibble1 Nibble6 = false + | op_eq_nibble Nibble1 Nibble7 = false + | op_eq_nibble Nibble1 Nibble8 = false + | op_eq_nibble Nibble1 Nibble9 = false + | op_eq_nibble Nibble1 NibbleA = false + | op_eq_nibble Nibble1 NibbleB = false + | op_eq_nibble Nibble1 NibbleC = false + | op_eq_nibble Nibble1 NibbleD = false + | op_eq_nibble Nibble1 NibbleE = false + | op_eq_nibble Nibble1 NibbleF = false + | op_eq_nibble Nibble2 Nibble3 = false + | op_eq_nibble Nibble2 Nibble4 = false + | op_eq_nibble Nibble2 Nibble5 = false + | op_eq_nibble Nibble2 Nibble6 = false + | op_eq_nibble Nibble2 Nibble7 = false + | op_eq_nibble Nibble2 Nibble8 = false + | op_eq_nibble Nibble2 Nibble9 = false + | op_eq_nibble Nibble2 NibbleA = false + | op_eq_nibble Nibble2 NibbleB = false + | op_eq_nibble Nibble2 NibbleC = false + | op_eq_nibble Nibble2 NibbleD = false + | op_eq_nibble Nibble2 NibbleE = false + | op_eq_nibble Nibble2 NibbleF = false + | op_eq_nibble Nibble3 Nibble4 = false + | op_eq_nibble Nibble3 Nibble5 = false + | op_eq_nibble Nibble3 Nibble6 = false + | op_eq_nibble Nibble3 Nibble7 = false + | op_eq_nibble Nibble3 Nibble8 = false + | op_eq_nibble Nibble3 Nibble9 = false + | op_eq_nibble Nibble3 NibbleA = false + | op_eq_nibble Nibble3 NibbleB = false + | op_eq_nibble Nibble3 NibbleC = false + | op_eq_nibble Nibble3 NibbleD = false + | op_eq_nibble Nibble3 NibbleE = false + | op_eq_nibble Nibble3 NibbleF = false + | op_eq_nibble Nibble4 Nibble5 = false + | op_eq_nibble Nibble4 Nibble6 = false + | op_eq_nibble Nibble4 Nibble7 = false + | op_eq_nibble Nibble4 Nibble8 = false + | op_eq_nibble Nibble4 Nibble9 = false + | op_eq_nibble Nibble4 NibbleA = false + | op_eq_nibble Nibble4 NibbleB = false + | op_eq_nibble Nibble4 NibbleC = false + | op_eq_nibble Nibble4 NibbleD = false + | op_eq_nibble Nibble4 NibbleE = false + | op_eq_nibble Nibble4 NibbleF = false + | op_eq_nibble Nibble5 Nibble6 = false + | op_eq_nibble Nibble5 Nibble7 = false + | op_eq_nibble Nibble5 Nibble8 = false + | op_eq_nibble Nibble5 Nibble9 = false + | op_eq_nibble Nibble5 NibbleA = false + | op_eq_nibble Nibble5 NibbleB = false + | op_eq_nibble Nibble5 NibbleC = false + | op_eq_nibble Nibble5 NibbleD = false + | op_eq_nibble Nibble5 NibbleE = false + | op_eq_nibble Nibble5 NibbleF = false + | op_eq_nibble Nibble6 Nibble7 = false + | op_eq_nibble Nibble6 Nibble8 = false + | op_eq_nibble Nibble6 Nibble9 = false + | op_eq_nibble Nibble6 NibbleA = false + | op_eq_nibble Nibble6 NibbleB = false + | op_eq_nibble Nibble6 NibbleC = false + | op_eq_nibble Nibble6 NibbleD = false + | op_eq_nibble Nibble6 NibbleE = false + | op_eq_nibble Nibble6 NibbleF = false + | op_eq_nibble Nibble7 Nibble8 = false + | op_eq_nibble Nibble7 Nibble9 = false + | op_eq_nibble Nibble7 NibbleA = false + | op_eq_nibble Nibble7 NibbleB = false + | op_eq_nibble Nibble7 NibbleC = false + | op_eq_nibble Nibble7 NibbleD = false + | op_eq_nibble Nibble7 NibbleE = false + | op_eq_nibble Nibble7 NibbleF = false + | op_eq_nibble Nibble8 Nibble9 = false + | op_eq_nibble Nibble8 NibbleA = false + | op_eq_nibble Nibble8 NibbleB = false + | op_eq_nibble Nibble8 NibbleC = false + | op_eq_nibble Nibble8 NibbleD = false + | op_eq_nibble Nibble8 NibbleE = false + | op_eq_nibble Nibble8 NibbleF = false + | op_eq_nibble Nibble9 NibbleA = false + | op_eq_nibble Nibble9 NibbleB = false + | op_eq_nibble Nibble9 NibbleC = false + | op_eq_nibble Nibble9 NibbleD = false + | op_eq_nibble Nibble9 NibbleE = false + | op_eq_nibble Nibble9 NibbleF = false + | op_eq_nibble NibbleA NibbleB = false + | op_eq_nibble NibbleA NibbleC = false + | op_eq_nibble NibbleA NibbleD = false + | op_eq_nibble NibbleA NibbleE = false + | op_eq_nibble NibbleA NibbleF = false + | op_eq_nibble NibbleB NibbleC = false + | op_eq_nibble NibbleB NibbleD = false + | op_eq_nibble NibbleB NibbleE = false + | op_eq_nibble NibbleB NibbleF = false + | op_eq_nibble NibbleC NibbleD = false + | op_eq_nibble NibbleC NibbleE = false + | op_eq_nibble NibbleC NibbleF = false + | op_eq_nibble NibbleD NibbleE = false + | op_eq_nibble NibbleD NibbleF = false + | op_eq_nibble NibbleE NibbleF = false + | op_eq_nibble Nibble1 Nibble0 = false + | op_eq_nibble Nibble2 Nibble0 = false + | op_eq_nibble Nibble3 Nibble0 = false + | op_eq_nibble Nibble4 Nibble0 = false + | op_eq_nibble Nibble5 Nibble0 = false + | op_eq_nibble Nibble6 Nibble0 = false + | op_eq_nibble Nibble7 Nibble0 = false + | op_eq_nibble Nibble8 Nibble0 = false + | op_eq_nibble Nibble9 Nibble0 = false + | op_eq_nibble NibbleA Nibble0 = false + | op_eq_nibble NibbleB Nibble0 = false + | op_eq_nibble NibbleC Nibble0 = false + | op_eq_nibble NibbleD Nibble0 = false + | op_eq_nibble NibbleE Nibble0 = false + | op_eq_nibble NibbleF Nibble0 = false + | op_eq_nibble Nibble2 Nibble1 = false + | op_eq_nibble Nibble3 Nibble1 = false + | op_eq_nibble Nibble4 Nibble1 = false + | op_eq_nibble Nibble5 Nibble1 = false + | op_eq_nibble Nibble6 Nibble1 = false + | op_eq_nibble Nibble7 Nibble1 = false + | op_eq_nibble Nibble8 Nibble1 = false + | op_eq_nibble Nibble9 Nibble1 = false + | op_eq_nibble NibbleA Nibble1 = false + | op_eq_nibble NibbleB Nibble1 = false + | op_eq_nibble NibbleC Nibble1 = false + | op_eq_nibble NibbleD Nibble1 = false + | op_eq_nibble NibbleE Nibble1 = false + | op_eq_nibble NibbleF Nibble1 = false + | op_eq_nibble Nibble3 Nibble2 = false + | op_eq_nibble Nibble4 Nibble2 = false + | op_eq_nibble Nibble5 Nibble2 = false + | op_eq_nibble Nibble6 Nibble2 = false + | op_eq_nibble Nibble7 Nibble2 = false + | op_eq_nibble Nibble8 Nibble2 = false + | op_eq_nibble Nibble9 Nibble2 = false + | op_eq_nibble NibbleA Nibble2 = false + | op_eq_nibble NibbleB Nibble2 = false + | op_eq_nibble NibbleC Nibble2 = false + | op_eq_nibble NibbleD Nibble2 = false + | op_eq_nibble NibbleE Nibble2 = false + | op_eq_nibble NibbleF Nibble2 = false + | op_eq_nibble Nibble4 Nibble3 = false + | op_eq_nibble Nibble5 Nibble3 = false + | op_eq_nibble Nibble6 Nibble3 = false + | op_eq_nibble Nibble7 Nibble3 = false + | op_eq_nibble Nibble8 Nibble3 = false + | op_eq_nibble Nibble9 Nibble3 = false + | op_eq_nibble NibbleA Nibble3 = false + | op_eq_nibble NibbleB Nibble3 = false + | op_eq_nibble NibbleC Nibble3 = false + | op_eq_nibble NibbleD Nibble3 = false + | op_eq_nibble NibbleE Nibble3 = false + | op_eq_nibble NibbleF Nibble3 = false + | op_eq_nibble Nibble5 Nibble4 = false + | op_eq_nibble Nibble6 Nibble4 = false + | op_eq_nibble Nibble7 Nibble4 = false + | op_eq_nibble Nibble8 Nibble4 = false + | op_eq_nibble Nibble9 Nibble4 = false + | op_eq_nibble NibbleA Nibble4 = false + | op_eq_nibble NibbleB Nibble4 = false + | op_eq_nibble NibbleC Nibble4 = false + | op_eq_nibble NibbleD Nibble4 = false + | op_eq_nibble NibbleE Nibble4 = false + | op_eq_nibble NibbleF Nibble4 = false + | op_eq_nibble Nibble6 Nibble5 = false + | op_eq_nibble Nibble7 Nibble5 = false + | op_eq_nibble Nibble8 Nibble5 = false + | op_eq_nibble Nibble9 Nibble5 = false + | op_eq_nibble NibbleA Nibble5 = false + | op_eq_nibble NibbleB Nibble5 = false + | op_eq_nibble NibbleC Nibble5 = false + | op_eq_nibble NibbleD Nibble5 = false + | op_eq_nibble NibbleE Nibble5 = false + | op_eq_nibble NibbleF Nibble5 = false + | op_eq_nibble Nibble7 Nibble6 = false + | op_eq_nibble Nibble8 Nibble6 = false + | op_eq_nibble Nibble9 Nibble6 = false + | op_eq_nibble NibbleA Nibble6 = false + | op_eq_nibble NibbleB Nibble6 = false + | op_eq_nibble NibbleC Nibble6 = false + | op_eq_nibble NibbleD Nibble6 = false + | op_eq_nibble NibbleE Nibble6 = false + | op_eq_nibble NibbleF Nibble6 = false + | op_eq_nibble Nibble8 Nibble7 = false + | op_eq_nibble Nibble9 Nibble7 = false + | op_eq_nibble NibbleA Nibble7 = false + | op_eq_nibble NibbleB Nibble7 = false + | op_eq_nibble NibbleC Nibble7 = false + | op_eq_nibble NibbleD Nibble7 = false + | op_eq_nibble NibbleE Nibble7 = false + | op_eq_nibble NibbleF Nibble7 = false + | op_eq_nibble Nibble9 Nibble8 = false + | op_eq_nibble NibbleA Nibble8 = false + | op_eq_nibble NibbleB Nibble8 = false + | op_eq_nibble NibbleC Nibble8 = false + | op_eq_nibble NibbleD Nibble8 = false + | op_eq_nibble NibbleE Nibble8 = false + | op_eq_nibble NibbleF Nibble8 = false + | op_eq_nibble NibbleA Nibble9 = false + | op_eq_nibble NibbleB Nibble9 = false + | op_eq_nibble NibbleC Nibble9 = false + | op_eq_nibble NibbleD Nibble9 = false + | op_eq_nibble NibbleE Nibble9 = false + | op_eq_nibble NibbleF Nibble9 = false + | op_eq_nibble NibbleB NibbleA = false + | op_eq_nibble NibbleC NibbleA = false + | op_eq_nibble NibbleD NibbleA = false + | op_eq_nibble NibbleE NibbleA = false + | op_eq_nibble NibbleF NibbleA = false + | op_eq_nibble NibbleC NibbleB = false + | op_eq_nibble NibbleD NibbleB = false + | op_eq_nibble NibbleE NibbleB = false + | op_eq_nibble NibbleF NibbleB = false + | op_eq_nibble NibbleD NibbleC = false + | op_eq_nibble NibbleE NibbleC = false + | op_eq_nibble NibbleF NibbleC = false + | op_eq_nibble NibbleE NibbleD = false + | op_eq_nibble NibbleF NibbleD = false + | op_eq_nibble NibbleF NibbleE = false; + +fun op_eq_char (Char (nibble1, nibble2)) (Char (nibble1', nibble2')) = + op_eq_nibble nibble1 nibble1' andalso op_eq_nibble nibble2 nibble2'; + +val eq_char = {op_eq = op_eq_char} : char Code_Generator.eq; + +fun list_all p (x :: xs) = p x andalso list_all p xs + | list_all p [] = true; + +fun size_list (a :: lista) = + Nat.plus_nat (size_list lista) (Nat.Suc Nat.Zero_nat) + | size_list [] = Nat.Zero_nat; + +fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys + | list_all2 p xs [] = null xs + | list_all2 p [] ys = null ys + | list_all2 p xs ys = + Nat.op_eq_nat (size_list xs) (size_list ys) andalso + list_all (fn a as (aa, b) => p aa b) (zip xs ys); + +fun op_eq_list A_ [] [] = true + | op_eq_list A_ (a :: lista) (a' :: list') = + Code_Generator.op_eq A_ a a' andalso op_eq_list A_ lista list' + | op_eq_list A_ [] (a :: b) = false + | op_eq_list A_ (a :: b) [] = false; + +end; (*struct List*) + +structure Codegen = +struct + +datatype monotype = Mono of List.char list * monotype list; + +fun op_eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) = + List.op_eq_list List.eq_char tyco1 tyco2 andalso + List.list_all2 op_eq_monotype typargs1 typargs2; + +end; (*struct Codegen*) + +end; (*struct ROOT*)