diff options
Diffstat (limited to 'exportclight/Clightdefs.v')
| -rw-r--r-- | exportclight/Clightdefs.v | 211 |
1 files changed, 210 insertions, 1 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index 83d82d88..8af920df 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -15,7 +15,7 @@ (** All imports and definitions used by .v Clight files generated by clightgen *) -From Coq Require Import String List ZArith. +From Coq Require Import Ascii String List ZArith. From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. Definition tvoid := Tvoid. @@ -80,3 +80,212 @@ Definition mkprogram (types: list composite_definition) prog_types := types; prog_comp_env := ce; prog_comp_env_eq := EQ |}. + +(** The following encoding of character strings as positive numbers + must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) + +Definition append_bit_pos (b: bool) (p: positive) : positive := + if b then xI p else xO p. + +Definition append_char_pos_default (c: ascii) (p: positive) : positive := + let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in + xI (xI (xI (xI (xI (xI + (append_bit_pos b0 (append_bit_pos b1 + (append_bit_pos b2 (append_bit_pos b3 + (append_bit_pos b4 (append_bit_pos b5 + (append_bit_pos b6 (append_bit_pos b7 p))))))))))))). + +Definition append_char_pos (c: ascii) (p: positive) : positive := + match c with + | "0"%char => xO (xO (xO (xO (xO (xO p))))) + | "1"%char => xI (xO (xO (xO (xO (xO p))))) + | "2"%char => xO (xI (xO (xO (xO (xO p))))) + | "3"%char => xI (xI (xO (xO (xO (xO p))))) + | "4"%char => xO (xO (xI (xO (xO (xO p))))) + | "5"%char => xI (xO (xI (xO (xO (xO p))))) + | "6"%char => xO (xI (xI (xO (xO (xO p))))) + | "7"%char => xI (xI (xI (xO (xO (xO p))))) + | "8"%char => xO (xO (xO (xI (xO (xO p))))) + | "9"%char => xI (xO (xO (xI (xO (xO p))))) + | "a"%char => xO (xI (xO (xI (xO (xO p))))) + | "b"%char => xI (xI (xO (xI (xO (xO p))))) + | "c"%char => xO (xO (xI (xI (xO (xO p))))) + | "d"%char => xI (xO (xI (xI (xO (xO p))))) + | "e"%char => xO (xI (xI (xI (xO (xO p))))) + | "f"%char => xI (xI (xI (xI (xO (xO p))))) + | "g"%char => xO (xO (xO (xO (xI (xO p))))) + | "h"%char => xI (xO (xO (xO (xI (xO p))))) + | "i"%char => xO (xI (xO (xO (xI (xO p))))) + | "j"%char => xI (xI (xO (xO (xI (xO p))))) + | "k"%char => xO (xO (xI (xO (xI (xO p))))) + | "l"%char => xI (xO (xI (xO (xI (xO p))))) + | "m"%char => xO (xI (xI (xO (xI (xO p))))) + | "n"%char => xI (xI (xI (xO (xI (xO p))))) + | "o"%char => xO (xO (xO (xI (xI (xO p))))) + | "p"%char => xI (xO (xO (xI (xI (xO p))))) + | "q"%char => xO (xI (xO (xI (xI (xO p))))) + | "r"%char => xI (xI (xO (xI (xI (xO p))))) + | "s"%char => xO (xO (xI (xI (xI (xO p))))) + | "t"%char => xI (xO (xI (xI (xI (xO p))))) + | "u"%char => xO (xI (xI (xI (xI (xO p))))) + | "v"%char => xI (xI (xI (xI (xI (xO p))))) + | "w"%char => xO (xO (xO (xO (xO (xI p))))) + | "x"%char => xI (xO (xO (xO (xO (xI p))))) + | "y"%char => xO (xI (xO (xO (xO (xI p))))) + | "z"%char => xI (xI (xO (xO (xO (xI p))))) + | "A"%char => xO (xO (xI (xO (xO (xI p))))) + | "B"%char => xI (xO (xI (xO (xO (xI p))))) + | "C"%char => xO (xI (xI (xO (xO (xI p))))) + | "D"%char => xI (xI (xI (xO (xO (xI p))))) + | "E"%char => xO (xO (xO (xI (xO (xI p))))) + | "F"%char => xI (xO (xO (xI (xO (xI p))))) + | "G"%char => xO (xI (xO (xI (xO (xI p))))) + | "H"%char => xI (xI (xO (xI (xO (xI p))))) + | "I"%char => xO (xO (xI (xI (xO (xI p))))) + | "J"%char => xI (xO (xI (xI (xO (xI p))))) + | "K"%char => xO (xI (xI (xI (xO (xI p))))) + | "L"%char => xI (xI (xI (xI (xO (xI p))))) + | "M"%char => xO (xO (xO (xO (xI (xI p))))) + | "N"%char => xI (xO (xO (xO (xI (xI p))))) + | "O"%char => xO (xI (xO (xO (xI (xI p))))) + | "P"%char => xI (xI (xO (xO (xI (xI p))))) + | "Q"%char => xO (xO (xI (xO (xI (xI p))))) + | "R"%char => xI (xO (xI (xO (xI (xI p))))) + | "S"%char => xO (xI (xI (xO (xI (xI p))))) + | "T"%char => xI (xI (xI (xO (xI (xI p))))) + | "U"%char => xO (xO (xO (xI (xI (xI p))))) + | "V"%char => xI (xO (xO (xI (xI (xI p))))) + | "W"%char => xO (xI (xO (xI (xI (xI p))))) + | "X"%char => xI (xI (xO (xI (xI (xI p))))) + | "Y"%char => xO (xO (xI (xI (xI (xI p))))) + | "Z"%char => xI (xO (xI (xI (xI (xI p))))) + | "_"%char => xO (xI (xI (xI (xI (xI p))))) + | _ => append_char_pos_default c p + end. + +Fixpoint ident_of_string (s: string) : ident := + match s with + | EmptyString => xH + | String c s => append_char_pos c (ident_of_string s) + end. + +(** A convenient notation [$ "ident"] to force evaluation of + [ident_of_string "ident"] *) + +Ltac ident_of_string s := + let x := constr:(ident_of_string s) in + let y := eval compute in x in + exact y. + +Notation "$ s" := (ltac:(ident_of_string s)) + (at level 1, only parsing) : string_scope. + +(** The inverse conversion, from encoded strings to strings *) + +Section DECODE_BITS. + +Variable rec: positive -> string. + +Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string := + match n with + | O => + match l with + | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ => + String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p) + | _ => EmptyString + end + | S n => + match p with + | xO q => decode_n_bits n (false :: l) q + | xI q => decode_n_bits n (true :: l) q + | xH => EmptyString + end + end. + +Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil). + +End DECODE_BITS. + +Fixpoint string_of_ident (p: positive) : string := + match p with + | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p) + | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p) + | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p) + | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p) + | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p) + | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p) + | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p) + | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p) + | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p) + | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p) + | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p) + | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p) + | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p) + | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p) + | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p) + | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p) + | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p) + | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p) + | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p) + | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p) + | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p) + | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p) + | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p) + | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p) + | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p) + | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p) + | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p) + | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p) + | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p) + | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p) + | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p) + | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p) + | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p) + | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p) + | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p) + | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p) + | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p) + | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p) + | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p) + | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p) + | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p) + | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p) + | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p) + | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p) + | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p) + | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p) + | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p) + | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p) + | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p) + | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p) + | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p) + | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p) + | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p) + | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p) + | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p) + | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p) + | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p) + | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p) + | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p) + | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p) + | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p) + | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p) + | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p) + | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p + | _ => EmptyString + end. + +Lemma string_of_ident_of_string: + forall s, string_of_ident (ident_of_string s) = s. +Proof. + induction s as [ | c s]; simpl. +- auto. +- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity. +Qed. + +Corollary ident_of_string_injective: + forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2. +Proof. + intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). + congruence. +Qed. |