Revision ca7ff3f7
Added by LĂ©lio Brun 8 months ago
src/init_predef.ml  

9  9 
(* *) 
10  10 
(********************************************************************) 
11  11  
12  
13 
(** Base types and predefined operator types. *) 

14  12 
open Init 
13 
(** Base types and predefined operator types. *) 

15  14  
16  15 
let init_zero = new_univar () 
17  16  
18  17 
let init_un = 
19  18 
let univ = new_univar () in 
20 
new_init Isucc(univ)


19 
new_init Isucc univ


21  20  
22 
let rec init_omega = 

23 
{ init_desc = Isucc init_omega ; iid = 1 } 

21 
let rec init_omega = { init_desc = Isucc init_omega; iid = 1 } 

24  22  
25  23 
let is_omega init = 
26  24 
let rec search path init = 
27 
match init.init_desc with 

28 
 Isucc init' > List.mem init path or search (init::path) init' 

29 
 _ > false 

30 
in search [] init 

25 
match init.init_desc with 

26 
 Isucc init' > 

27 
List.mem init path or search (init :: path) init' 

28 
 _ > 

29 
false 

30 
in 

31 
search [] init 

31  32  
32  33 
let init_unary_poly_op = 
33  34 
let univ = new_univar () in 
...  ...  
39  40  
40  41 
let init_arrow_op = 
41  42 
let univ = new_univar () in 
42 
new_init (Iarrow (new_init (Ituple [univ; init_un]), univ))


43 
new_init (Iarrow (new_init (Ituple [ univ; init_un ]), univ))


43  44  
44  45 
let init_fby_op_1 = 
45  46 
let univ = new_univar () in 
46 
new_init (Iarrow (init_zero,init_zero)) 

47 
new_init (Iarrow (init_zero, init_zero))


47  48  
48 
let init_fby_op_2 = 

49 
init_pre_op 

49 
let init_fby_op_2 = init_pre_op 

50  50  
51  51 
let init_bin_poly_op = 
52  52 
let univ = new_univar () in 
53 
new_init (Iarrow (new_init (Ituple [univ;univ]), univ))


53 
new_init (Iarrow (new_init (Ituple [ univ; univ ]), univ))


54  54  
55  55 
let init_ter_poly_op = 
56  56 
let univ = new_univar () in 
57 
new_init (Iarrow (new_init (Ituple [univ;univ;univ]), univ))


57 
new_init (Iarrow (new_init (Ituple [ univ; univ; univ ]), univ))


58  58  
59  59 
let env = 
60  60 
let init_env = Env.initial in 
61 
let env' = 

62 
List.fold_right (fun op env > Env.add_value env op init_unary_poly_op) 

63 
["uminus"; "not"] init_env in 

64 
let env' = 

65 
List.fold_right (fun op env > Env.add_value env op init_binary_poly_op) 

66 
["+"; ""; "*"; "/"; "mod"; "&&"; ""; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in 

67 
let env' = 

68 
List.fold_right (fun op env > Env.add_value env op init_ternary_poly_op) 

69 
["ite"] init_env in 

61 
let env' = 

62 
List.fold_right 

63 
(fun op env > Env.add_value env op init_unary_poly_op) 

64 
[ "uminus"; "not" ] init_env 

65 
in 

66 
let env' = 

67 
List.fold_right 

68 
(fun op env > Env.add_value env op init_binary_poly_op) 

69 
[ 

70 
"+"; 

71 
""; 

72 
"*"; 

73 
"/"; 

74 
"mod"; 

75 
"&&"; 

76 
""; 

77 
"xor"; 

78 
"impl"; 

79 
"<"; 

80 
"<="; 

81 
">"; 

82 
">="; 

83 
"!="; 

84 
"="; 

85 
] 

86 
env' 

87 
in 

88 
let env' = 

89 
List.fold_right 

90 
(fun op env > Env.add_value env op init_ternary_poly_op) 

91 
[ "ite" ] init_env 

92 
in 

70  93 
env' 
71  94  
72  95 
(* Local Variables: *) 
Also available in: Unified diff
reformatting