@@ -820,3 +820,355 @@ let undo_compress (changes, _old) =
820820            ty.desc < -  desc; r :=  ! next
821821        |  _  -> () )
822822        log
823+ 
824+ 
825+ module  Alloc_mode  =  struct 
826+   type  nonrec const  = Types .alloc_mode_const  =  Global  | Local 
827+   type  t  = Types .alloc_mode  = 
828+     | Amode  of  const 
829+     | Amodevar  of  alloc_mode_var 
830+ 
831+   let  global =  Amode  Global 
832+   let  local =  Amode  Local 
833+   let  of_const  =  function 
834+     |  Global  -> global
835+     |  Local  -> local
836+ 
837+   let  min_mode =  global
838+ 
839+   let  max_mode =  local
840+ 
841+   let  le_const  a  b  = 
842+     match  a, b with 
843+     |  Global , _  |  _ , Local  -> true 
844+     |  Local , Global  -> false 
845+ 
846+   let  join_const  a  b  = 
847+     match  a, b with 
848+     |  Local , _  |  _ , Local  -> Local 
849+     |  Global , Global  -> Global 
850+ 
851+   let  meet_const  a  b  = 
852+     match  a, b with 
853+     |  Global , _  |  _ , Global  -> Global 
854+     |  Local , Local  -> Local 
855+ 
856+   exception  NotSubmode 
857+ (* 
858+   let pp_c ppf = function 
859+     | Global -> Printf.fprintf ppf "0" 
860+     | Local -> Printf.fprintf ppf "1" 
861+   let pp_v ppf v = 
862+     let i = v.mvid in 
863+     (if i < 26 then Printf.fprintf ppf "%c" (Char.chr (Char.code 'a' + i)) 
864+     else Printf.fprintf ppf "v%d" i); 
865+     Printf.fprintf ppf "[%a%a]" pp_c v.lower pp_c v.upper 
866+ *) 
867+   let  submode_cv  m  v  = 
868+     (*  Printf.printf "  %a <= %a\n" pp_c m pp_v v; *) 
869+     if  le_const m v.lower then  () 
870+     else  if  not  (le_const m v.upper) then  raise NotSubmode 
871+     else  begin 
872+       let  m =  join_const v.lower m in 
873+       v.lower < -  m;
874+       if  m =  v.upper then  v.vlower < -  [] 
875+     end 
876+ 
877+   let  rec  submode_vc  v  m  = 
878+     (*  Printf.printf "  %a <= %a\n" pp_v v pp_c m; *) 
879+     if  le_const v.upper m then  () 
880+     else  if  not  (le_const v.lower m) then  raise NotSubmode 
881+     else  begin 
882+       let  m =  meet_const v.upper m in 
883+       v.upper < -  m;
884+       v.vlower |>  List. iter (fun  a  ->
885+         (*  a <= v <= m *) 
886+         submode_vc a m;
887+         v.lower < -  join_const v.lower a.lower;
888+       );
889+       if  v.lower =  m then  v.vlower < -  [] 
890+     end 
891+ 
892+   let  submode_vv  a  b  = 
893+     (*  Printf.printf "  %a <= %a\n" pp_v a pp_v b; *) 
894+     if  le_const a.upper b.lower then  () 
895+     else  if  List. memq a b.vlower then  () 
896+     else  begin 
897+       submode_vc a b.upper;
898+       b.vlower < -  a :: b.vlower;
899+       submode_cv a.lower b;
900+     end 
901+ 
902+   let  submode  a  b  = 
903+     match 
904+       match  a, b with 
905+       |  Amode  a , Amode  b  ->
906+          if  not  (le_const a b) then  raise NotSubmode 
907+       |  Amodevar  v , Amode  c  ->
908+          (*  Printf.printf "%a <= %a\n" pp_v v pp_c c; *) 
909+          submode_vc v c
910+       |  Amode  c , Amodevar  v  ->
911+          (*  Printf.printf "%a <= %a\n" pp_c c pp_v v; *) 
912+          submode_cv c v
913+       |  Amodevar  a , Amodevar  b  ->
914+          (*  Printf.printf "%a <= %a\n" pp_v a pp_v b; *) 
915+          submode_vv a b
916+     with 
917+     |  ()  -> Ok  () 
918+     |  exception  NotSubmode  -> Error  () 
919+ 
920+   let  submode_exn  t1  t2  = 
921+     match  submode t1 t2 with 
922+     |  Ok  ()  -> () 
923+     |  Error  ()  -> invalid_arg " submode_exn" 
924+ 
925+   let  equate  a  b  = 
926+     match  submode a b, submode b a with 
927+     |  Ok  () , Ok  ()  -> Ok  () 
928+     |  Error  (), _  |  _ , Error  ()  -> Error  () 
929+ 
930+   let  next_id =  ref  (- 1 )
931+   let  fresh  ()  = 
932+     incr next_id;
933+     { upper =  Local ; lower =  Global ; vlower =  [] ; mvid =  ! next_id }
934+ 
935+   let  rec  all_equal  v  =  function 
936+     |  []  -> true 
937+     |  v'  :: rest  ->
938+         if  v ==  v' then  all_equal v rest
939+         else  false 
940+ 
941+   let  joinvars  vars  = 
942+     match  vars with 
943+     |  []  -> global
944+     |  v  :: rest  ->
945+       let  v = 
946+         if  all_equal v rest then  v
947+         else  begin 
948+           let  v =  fresh ()  in 
949+           List. iter (fun  v'  -> submode_vv v' v) vars;
950+           v
951+         end 
952+       in 
953+       Amodevar  v
954+ 
955+   let  join  ms  = 
956+     let  rec  aux  vars  =  function 
957+       |  []  -> joinvars vars
958+       |  Amode  Global  :: ms  -> aux vars ms
959+       |  Amode  Local  :: _  -> local
960+       |  Amodevar  v  :: ms  -> aux (v :: vars) ms
961+     in  aux []  ms
962+ 
963+   let  constrain_upper  =  function 
964+     |  Amode  m  -> m
965+     |  Amodevar  v  ->
966+        submode_cv v.upper v;
967+        v.upper
968+ 
969+   let  compress_vlower  v  = 
970+     (*  Ensure that each transitive lower bound of v
971+        is a direct lower bound of v *)  
972+     let  rec  trans  v'  = 
973+       if  le_const v'.upper v.lower then  () 
974+       else  if  List. memq v' v.vlower then  () 
975+       else  begin 
976+         v.vlower < -  v' :: v.vlower;
977+         trans_low v'
978+       end 
979+     and  trans_low  v'  = 
980+       submode_cv v'.lower v;
981+       List. iter trans v'.vlower
982+     in 
983+     List. iter trans_low v.vlower
984+ 
985+   let  constrain_lower  =  function 
986+     |  Amode  m  -> m
987+     |  Amodevar  v  ->
988+         compress_vlower v;
989+         submode_vc v v.lower;
990+         v.lower
991+ 
992+   let  newvar  ()  =  Amodevar  (fresh () )
993+ 
994+   let  check_const  =  function 
995+     |  Amode  m  -> Some  m
996+     |  Amodevar  v  when  v.lower =  v.upper ->
997+        Some  v.lower
998+     |  Amodevar  _  -> None 
999+ 
1000+   let  print_const  ppf  =  function 
1001+     |  Global  -> Format. fprintf ppf " Global" 
1002+     |  Local  -> Format. fprintf ppf " Local" 
1003+ 
1004+   let  print_var_id  ppf  v  = 
1005+     Format. fprintf ppf " ?%i" 
1006+ 
1007+   let  print_var  ppf  v  = 
1008+     compress_vlower v;
1009+     if  v.lower =  v.upper then  begin 
1010+       print_const ppf v.lower
1011+     end  else  if  v.vlower =  []  then  begin 
1012+       print_var_id ppf v
1013+     end  else  begin 
1014+       Format. fprintf ppf " %a[> %a]" 
1015+         print_var_id v
1016+         (Format. pp_print_list print_var_id) v.vlower
1017+     end 
1018+ 
1019+   let  print  ppf  =  function 
1020+     |  Amode  m  -> print_const ppf m
1021+     |  Amodevar  v  -> print_var ppf v
1022+ 
1023+ end 
1024+ 
1025+ module  Value_mode  =  struct 
1026+ 
1027+   type  const  =
1028+    | Global 
1029+    | Regional 
1030+    | Local 
1031+ 
1032+   let  r_as_l  : const -> Alloc_mode.const  =  function 
1033+     |  Global  -> Global 
1034+     |  Regional  -> Local 
1035+     |  Local  -> Local 
1036+   [@@ warning " -unused-value-declaration" 
1037+ 
1038+   let  r_as_g  : const -> Alloc_mode.const  =  function 
1039+     |  Global  -> Global 
1040+     |  Regional  -> Global 
1041+     |  Local  -> Local 
1042+   [@@ warning " -unused-value-declaration" 
1043+ 
1044+   let  of_alloc_consts 
1045+         ~(r_as_l  : Alloc_mode.const )
1046+         ~(r_as_g  : Alloc_mode.const ) = 
1047+     match  r_as_l, r_as_g with 
1048+     |  Global , Global  -> Global 
1049+     |  Global , Local  -> assert  false 
1050+     |  Local , Global  -> Regional 
1051+     |  Local , Local  -> Local 
1052+ 
1053+   type  t  = Types .value_mode  = 
1054+     { r_as_l  : Alloc_mode .t ; 
1055+       (*  [r_as_l] is the image of the mode under the [r_as_l] function *) 
1056+       r_as_g  : Alloc_mode .t ; 
1057+       (*  [r_as_g] is the image of the mode under the [r_as_g] function.
1058+          Always less than [r_as_l]. *)   }
1059+ 
1060+   let  global = 
1061+     let  r_as_l =  Alloc_mode. global in 
1062+     let  r_as_g =  Alloc_mode. global in 
1063+     { r_as_l; r_as_g }
1064+ 
1065+   let  regional = 
1066+     let  r_as_l =  Alloc_mode. local in 
1067+     let  r_as_g =  Alloc_mode. global in 
1068+     { r_as_l; r_as_g }
1069+ 
1070+   let  local = 
1071+     let  r_as_l =  Alloc_mode. local in 
1072+     let  r_as_g =  Alloc_mode. local in 
1073+     { r_as_l; r_as_g }
1074+ 
1075+   let  of_const  =  function 
1076+     |  Global  -> global
1077+     |  Regional  -> regional
1078+     |  Local  -> local
1079+ 
1080+   let  max_mode = 
1081+     let  r_as_l =  Alloc_mode. max_mode in 
1082+     let  r_as_g =  Alloc_mode. max_mode in 
1083+     { r_as_l; r_as_g }
1084+ 
1085+   let  min_mode = 
1086+     let  r_as_l =  Alloc_mode. min_mode in 
1087+     let  r_as_g =  Alloc_mode. min_mode in 
1088+     { r_as_l; r_as_g }
1089+ 
1090+   let  of_alloc  mode  = 
1091+     let  r_as_l =  mode in 
1092+     let  r_as_g =  mode in 
1093+     { r_as_l; r_as_g }
1094+ 
1095+   let  local_to_regional  t  =  { t with  r_as_g =  Alloc_mode. global }
1096+ 
1097+   let  regional_to_global  t  =  { t with  r_as_l =  t.r_as_g }
1098+ 
1099+   let  regional_to_local  t  =  { t with  r_as_g =  t.r_as_l }
1100+ 
1101+   let  global_to_regional  t  =  { t with  r_as_l =  Alloc_mode. local }
1102+ 
1103+   let  regional_to_global_alloc  t  =  t.r_as_g
1104+ 
1105+   let  regional_to_local_alloc  t  =  t.r_as_l
1106+ 
1107+   type  error  = [`Regionality  | `Locality ]
1108+ 
1109+   let  submode  t1  t2  = 
1110+     match  Alloc_mode. submode t1.r_as_l t2.r_as_l with 
1111+     |  Error  ()  -> Error  `Regionality 
1112+     |  Ok  ()  as  ok  -> begin 
1113+         match  Alloc_mode. submode t1.r_as_g t2.r_as_g with 
1114+         |  Ok  ()  -> ok
1115+         |  Error  ()  -> Error  `Locality 
1116+       end 
1117+ 
1118+   let  submode_exn  t1  t2  = 
1119+     match  submode t1 t2 with 
1120+     |  Ok  ()  -> () 
1121+     |  Error  _  -> invalid_arg " submode_exn" 
1122+ 
1123+   let  rec  submode_meet  t  =  function 
1124+     |  []  -> Ok  () 
1125+     |  t'  :: rest  ->
1126+       match  submode t t' with 
1127+       |  Ok  ()  -> submode_meet t rest
1128+       |  Error  _  as  err  -> err
1129+ 
1130+   let  join  ts  = 
1131+     let  r_as_l =  Alloc_mode. join (List. map (fun  t  -> t.r_as_l) ts) in 
1132+     let  r_as_g =  Alloc_mode. join (List. map (fun  t  -> t.r_as_g) ts) in 
1133+     { r_as_l; r_as_g }
1134+ 
1135+   let  constrain_upper  t  = 
1136+     let  r_as_l =  Alloc_mode. constrain_upper t.r_as_l in 
1137+     let  r_as_g =  Alloc_mode. constrain_upper t.r_as_g in 
1138+     of_alloc_consts ~r_as_l  ~r_as_g 
1139+ 
1140+   let  constrain_lower  t  = 
1141+     let  r_as_l =  Alloc_mode. constrain_lower t.r_as_l in 
1142+     let  r_as_g =  Alloc_mode. constrain_lower t.r_as_g in 
1143+     of_alloc_consts ~r_as_l  ~r_as_g 
1144+ 
1145+   let  newvar  ()  = 
1146+     let  r_as_l =  Alloc_mode. newvar ()  in 
1147+     let  r_as_g =  Alloc_mode. newvar ()  in 
1148+     Alloc_mode. submode_exn r_as_g r_as_l;
1149+     { r_as_l; r_as_g }
1150+ 
1151+   let  check_const  t  = 
1152+     match  Alloc_mode. check_const t.r_as_l with 
1153+     |  None  -> None 
1154+     |  Some  r_as_l  ->
1155+       match  Alloc_mode. check_const t.r_as_g with 
1156+       |  None  -> None 
1157+       |  Some  r_as_g  ->
1158+         Some  (of_alloc_consts ~r_as_l  ~r_as_g )
1159+ 
1160+   let  print_const  ppf  =  function 
1161+     |  Global  -> Format. fprintf ppf " Global" 
1162+     |  Regional  -> Format. fprintf ppf " Regional" 
1163+     |  Local  -> Format. fprintf ppf " Local" 
1164+ 
1165+   let  print  ppf  t  = 
1166+     match  check_const t with 
1167+     |  Some  const  -> print_const ppf const
1168+     |  None  ->
1169+         Format. fprintf ppf
1170+           " @[<2>r_as_l: %a@ r_as_g: %a@]" 
1171+           Alloc_mode. print t.r_as_l
1172+           Alloc_mode. print t.r_as_g
1173+ 
1174+ end 
0 commit comments