]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blobdiff - extracted/lINToASM.ml
Imported Upstream version 0.2
[pkg-cerco/acc-trusted.git] / extracted / lINToASM.ml
index 770789a79c89e6d9096d69d288633a4e86487cce..dc2b40bfdd8b90038ee17d8118cf854b179ece23 100644 (file)
@@ -139,10 +139,10 @@ type aSM_universe = { id_univ : Identifiers.universe;
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
+let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21483
+    fresh_cost_label0 } = x_588
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -151,10 +151,10 @@ let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_21483 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
+let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21485
+    fresh_cost_label0 } = x_590
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -163,10 +163,10 @@ let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_21485 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
+let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21487
+    fresh_cost_label0 } = x_592
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -175,10 +175,10 @@ let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_21487 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
+let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21489
+    fresh_cost_label0 } = x_594
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -187,10 +187,10 @@ let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_21489 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
+let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21491
+    fresh_cost_label0 } = x_596
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -199,10 +199,10 @@ let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_21491 =
     (Identifiers.universe -> AST.ident -> ASM.identifier
     Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map
     Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **)
-let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_21493 =
+let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 =
   let { id_univ = id_univ0; current_funct = current_funct0; ident_map =
     ident_map0; label_map = label_map0; fresh_cost_label =
-    fresh_cost_label0 } = x_21493
+    fresh_cost_label0 } = x_598
   in
   h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0
     fresh_cost_label0
@@ -302,7 +302,7 @@ let identifier_of_label l =
       Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current
         (Identifiers.empty_map PreIdentifiers.LabelTag)
     in
-    let { Types.fst = eta28616; Types.snd = lmap0 } =
+    let { Types.fst = eta2825; Types.snd = lmap0 } =
       match Identifiers.lookup PreIdentifiers.LabelTag lmap l with
       | Types.None ->
         let { Types.fst = id; Types.snd = univ } =
@@ -314,7 +314,7 @@ let identifier_of_label l =
         { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd =
           lmap }
     in
-    let { Types.fst = id; Types.snd = univ } = eta28616 in
+    let { Types.fst = id; Types.snd = univ } = eta2825 in
     { Types.fst = { id_univ = univ; current_funct = current; ident_map =
     u.ident_map; label_map =
     (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0);
@@ -1050,9 +1050,9 @@ type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod;
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
+let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21509
+    built_code = built_code0; built_preamble = built_preamble0 } = x_614
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1060,9 +1060,9 @@ let rec init_mutable_rect_Type4 h_mk_init_mutable x_21509 =
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
+let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21511
+    built_code = built_code0; built_preamble = built_preamble0 } = x_616
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1070,9 +1070,9 @@ let rec init_mutable_rect_Type5 h_mk_init_mutable x_21511 =
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
+let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21513
+    built_code = built_code0; built_preamble = built_preamble0 } = x_618
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1080,9 +1080,9 @@ let rec init_mutable_rect_Type3 h_mk_init_mutable x_21513 =
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
+let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21515
+    built_code = built_code0; built_preamble = built_preamble0 } = x_620
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1090,9 +1090,9 @@ let rec init_mutable_rect_Type2 h_mk_init_mutable x_21515 =
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
+let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21517
+    built_code = built_code0; built_preamble = built_preamble0 } = x_622
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1100,9 +1100,9 @@ let rec init_mutable_rect_Type1 h_mk_init_mutable x_21517 =
     ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod ->
     ASM.labelled_instruction List.list List.list -> (ASM.identifier,
     BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **)
-let rec init_mutable_rect_Type0 h_mk_init_mutable x_21519 =
+let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 =
   let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0;
-    built_code = built_code0; built_preamble = built_preamble0 } = x_21519
+    built_code = built_code0; built_preamble = built_preamble0 } = x_624
   in
   h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0
 
@@ -1303,8 +1303,8 @@ let do_store_init_data m_mut data =
     Monad.smax_def__o__monad **)
 let do_store_global m_mut id_reg_data =
   Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut ->
-    let { Types.fst = eta28633; Types.snd = data } = id_reg_data in
-    let { Types.fst = id; Types.snd = reg } = eta28633 in
+    let { Types.fst = eta2842; Types.snd = data } = id_reg_data in
+    let { Types.fst = id; Types.snd = reg } = eta2842 in
     Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id)
       (fun id0 ->
       let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ };