Changeset 747


Ignore:
Timestamp:
Apr 8, 2011, 2:06:46 PM (9 years ago)
Author:
campbell
Message:

Merge the two AST files together (although some definitions still need to be
harmonised).

Location:
src
Files:
1 deleted
8 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r744 r747  
    1717
    1818(*include "Integers.ma".*)
    19 include "Clight/AST.ma".
     19include "common/AST.ma".
    2020include "utilities/Coqlib.ma".
    2121include "common/Errors.ma".
  • src/RTLabs/RTLabs-syntax.ma

    r738 r747  
    22include "basics/logic.ma".
    33
    4 include "Clight/AST.ma".
     4include "common/AST.ma".
    55include "common/CostLabel.ma".
    66include "common/FrontEndOps.ma".
  • src/common/AST.ma

    r722 r747  
    1 include "arithmetics/nat.ma".
    2 
    3 include "ASM/String.ma".
     1(* *********************************************************************)
     2(*                                                                     *)
     3(*              The Compcert verified compiler                         *)
     4(*                                                                     *)
     5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
     6(*                                                                     *)
     7(*  Copyright Institut National de Recherche en Informatique et en     *)
     8(*  Automatique.  All rights reserved.  This file is distributed       *)
     9(*  under the terms of the GNU General Public License as published by  *)
     10(*  the Free Software Foundation, either version 2 of the License, or  *)
     11(*  (at your option) any later version.  This file is also distributed *)
     12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
     13(*                                                                     *)
     14(* *********************************************************************)
     15
     16(* * This file defines a number of data types and operations used in
     17  the abstract syntax trees of many of the intermediate languages. *)
     18
     19include "basics/types.ma".
     20include "common/Integers.ma".
     21include "common/Floats.ma".
    422include "ASM/BitVector.ma".
    5 include "utilities/Compare.ma".
    6 
     23include "common/Identifiers.ma".
     24
     25
     26(* * * Syntactic elements *)
     27
     28(* Global variables and functions are represented by identifiers with the
     29   tag for symbols.  Note that Clight also uses them for locals due to
     30   the ambiguous syntax. *)
     31
     32axiom SymbolTag : String.
     33
     34definition ident ≝ identifier SymbolTag.
     35
     36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
     37
     38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
     39
     40(* XXX backend is currently using untagged words as identifiers. *)
    741definition Identifier ≝ Word.
    8 definition Immediate ≝ nat.
     42
     43definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
     44
     45(* Memory spaces *)
     46
     47inductive region : Type[0] ≝
     48  | Any : region
     49  | Data : region
     50  | IData : region
     51  | PData : region
     52  | XData : region
     53  | Code : region.
     54
     55definition eq_region : region → region → bool ≝
     56λr1,r2.
     57  match r1 with
     58  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
     59  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
     60  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
     61  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
     62  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
     63  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
     64  ].
     65
     66lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
     67  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
     68  P (eq_region r1 r2).
     69#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
     70try ( @Ptrue // )
     71@Pfalse % #E destruct;
     72qed.
     73
     74definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
     75#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
     76
     77definition size_pointer : region → nat ≝
     78λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
     79
     80(* * The intermediate languages are weakly typed, using only three types:
     81  [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
     82  numbers. *)
     83
     84inductive typ : Type[0] ≝
     85  | ASTint : typ
     86  | ASTptr : region → typ
     87  | ASTfloat : typ.
     88
     89(* XXX aliases *)
     90definition SigType ≝ typ.
     91definition SigType_Int ≝ ASTint.
     92(*
     93| SigType_Float: SigType
     94*)
     95definition SigType_Ptr ≝ ASTptr Any.
     96
     97
     98(* FIXME: ASTint size is not 1 for Clight32 *)
     99definition typesize : typ → nat ≝ λty.
     100  match ty with [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
     101
     102lemma typesize_pos: ∀ty. typesize ty > 0.
     103#ty cases ty [ 2: * ] /2/ qed.
     104
     105lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
     106#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
     107
     108lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     109#t1 #t2 cases t1 cases t2
     110[ %1 @refl
     111| 2,3: #ty %2 % #H destruct
     112| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
     113]
     114qed.
     115
     116(* * Additionally, function definitions and function calls are annotated
     117  by function signatures indicating the number and types of arguments,
     118  as well as the type of the returned value if any.  These signatures
     119  are used in particular to determine appropriate calling conventions
     120  for the function. *)
     121
     122record signature : Type[0] ≝ {
     123  sig_args: list typ;
     124  sig_res: option typ
     125}.
     126
     127(* XXX aliases *)
     128definition Signature ≝ signature.
     129definition signature_args ≝ sig_args.
     130definition signature_return ≝ sig_res.
     131
     132definition proj_sig_res : signature → typ ≝ λs.
     133  match sig_res s with
     134  [ None ⇒ ASTint
     135  | Some t ⇒ t
     136  ].
     137
     138(* * Memory accesses (load and store instructions) are annotated by
     139  a ``memory chunk'' indicating the type, size and signedness of the
     140  chunk of memory being accessed. *)
     141
     142inductive memory_chunk : Type[0] ≝
     143  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
     144  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
     145  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
     146  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
     147  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
     148  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
     149  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
     150  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
     151
     152(* * Initialization data for global variables. *)
     153
     154inductive init_data: Type[0] ≝
     155  | Init_int8: int → init_data
     156  | Init_int16: int → init_data
     157  | Init_int32: int → init_data
     158  | Init_float32: float → init_data
     159  | Init_float64: float → init_data
     160  | Init_space: nat → init_data
     161  | Init_null: region → init_data
     162  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
     163
     164(* * Whole programs consist of:
     165- a collection of function definitions (name and description);
     166- the name of the ``main'' function that serves as entry point in the program;
     167- a collection of global variable declarations, consisting of
     168  a name, initialization data, and additional information.
     169
     170The type of function descriptions and that of additional information
     171for variables vary among the various intermediate languages and are
     172taken as parameters to the [program] type.  The other parts of whole
     173programs are common to all languages. *)
     174
     175record program (F,V: Type[0]) : Type[0] := {
     176  prog_funct: list (ident × F);
     177  prog_main: ident;
     178  prog_vars: list (ident × (list init_data) × region × V)
     179}.
     180
     181definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
     182  map ?? (fst ident F) (prog_funct ?? p).
     183
     184definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
     185  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     186(*
     187(** * Generic transformations over programs *)
     188
     189(** We now define a general iterator over programs that applies a given
     190  code transformation function to all function descriptions and leaves
     191  the other parts of the program unchanged. *)
     192
     193Section TRANSF_PROGRAM.
     194
     195Variable A B V: Type.
     196Variable transf: A -> B.
     197*)
     198
     199definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
     200λA,B,transf,l.
     201  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
     202
     203definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
     204λA,B,V,transf,p.
     205  mk_program B V
     206    (transf_program ?? transf (prog_funct A V p))
     207    (prog_main A V p)
     208    (prog_vars A V p).
     209(*
     210lemma transform_program_function:
     211  ∀A,B,V,transf,p,i,tf.
     212  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
     213  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
     214normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
     215#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
     216qed.
     217*)
     218(*
     219End TRANSF_PROGRAM.
     220
     221(** The following is a variant of [transform_program] where the
     222  code transformation function can fail and therefore returns an
     223  option type. *)
     224
     225Open Local Scope error_monad_scope.
     226Open Local Scope string_scope.
     227
     228Section MAP_PARTIAL.
     229
     230Variable A B C: Type.
     231Variable prefix_errmsg: A -> errmsg.
     232Variable f: B -> res C.
     233
     234Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
     235  match l with
     236  | nil => OK nil
     237  | (a, b) :: rem =>
     238      match f b with
     239      | Error msg => Error (prefix_errmsg a ++ msg)%list
     240      | OK c =>
     241          do rem' <- map_partial rem;
     242          OK ((a, c) :: rem')
     243      end
     244  end.
     245
     246Remark In_map_partial:
     247  forall l l' a c,
     248  map_partial l = OK l' ->
     249  In (a, c) l' ->
     250  exists b, In (a, b) l /\ f b = OK c.
     251Proof.
     252  induction l; simpl.
     253  intros. inv H. elim H0.
     254  intros until c. destruct a as [a1 b1].
     255  caseEq (f b1); try congruence.
     256  intro c1; intros. monadInv H0.
     257  elim H1; intro. inv H0. exists b1; auto.
     258  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
     259Qed.
     260
     261Remark map_partial_forall2:
     262  forall l l',
     263  map_partial l = OK l' ->
     264  list_forall2
     265    (fun (a_b: A * B) (a_c: A * C) =>
     266       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
     267    l l'.
     268Proof.
     269  induction l; simpl.
     270  intros. inv H. constructor.
     271  intro l'. destruct a as [a b].
     272  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
     273  constructor. simpl. auto. auto.
     274Qed.
     275
     276End MAP_PARTIAL.
     277
     278Remark map_partial_total:
     279  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
     280  map_partial prefix (fun b => OK (f b)) l =
     281  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
     282Proof.
     283  induction l; simpl.
     284  auto.
     285  destruct a as [a1 b1]. rewrite IHl. reflexivity.
     286Qed.
     287
     288Remark map_partial_identity:
     289  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
     290  map_partial prefix (fun b => OK b) l = OK l.
     291Proof.
     292  induction l; simpl.
     293  auto.
     294  destruct a as [a1 b1]. rewrite IHl. reflexivity.
     295Qed.
     296
     297Section TRANSF_PARTIAL_PROGRAM.
     298
     299Variable A B V: Type.
     300Variable transf_partial: A -> res B.
     301
     302Definition prefix_funct_name (id: ident) : errmsg :=
     303  MSG "In function " :: CTX id :: MSG ": " :: nil.
     304
     305Definition transform_partial_program (p: program A V) : res (program B V) :=
     306  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
     307  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
     308
     309Lemma transform_partial_program_function:
     310  forall p tp i tf,
     311  transform_partial_program p = OK tp ->
     312  In (i, tf) tp.(prog_funct) ->
     313  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
     314Proof.
     315  intros. monadInv H. simpl in H0. 
     316  eapply In_map_partial; eauto.
     317Qed.
     318
     319Lemma transform_partial_program_main:
     320  forall p tp,
     321  transform_partial_program p = OK tp ->
     322  tp.(prog_main) = p.(prog_main).
     323Proof.
     324  intros. monadInv H. reflexivity.
     325Qed.
     326
     327Lemma transform_partial_program_vars:
     328  forall p tp,
     329  transform_partial_program p = OK tp ->
     330  tp.(prog_vars) = p.(prog_vars).
     331Proof.
     332  intros. monadInv H. reflexivity.
     333Qed.
     334
     335End TRANSF_PARTIAL_PROGRAM.
     336
     337(** The following is a variant of [transform_program_partial] where
     338  both the program functions and the additional variable information
     339  are transformed by functions that can fail. *)
     340
     341Section TRANSF_PARTIAL_PROGRAM2.
     342
     343Variable A B V W: Type.
     344Variable transf_partial_function: A -> res B.
     345Variable transf_partial_variable: V -> res W.
     346
     347Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
     348  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
     349
     350Definition transform_partial_program2 (p: program A V) : res (program B W) :=
     351  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
     352  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
     353  OK (mkprogram fl p.(prog_main) vl).
     354
     355Lemma transform_partial_program2_function:
     356  forall p tp i tf,
     357  transform_partial_program2 p = OK tp ->
     358  In (i, tf) tp.(prog_funct) ->
     359  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
     360Proof.
     361  intros. monadInv H. 
     362  eapply In_map_partial; eauto.
     363Qed.
     364
     365Lemma transform_partial_program2_variable:
     366  forall p tp i tv,
     367  transform_partial_program2 p = OK tp ->
     368  In (i, tv) tp.(prog_vars) ->
     369  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
     370Proof.
     371  intros. monadInv H.
     372  eapply In_map_partial; eauto.
     373Qed.
     374
     375Lemma transform_partial_program2_main:
     376  forall p tp,
     377  transform_partial_program2 p = OK tp ->
     378  tp.(prog_main) = p.(prog_main).
     379Proof.
     380  intros. monadInv H. reflexivity.
     381Qed.
     382
     383End TRANSF_PARTIAL_PROGRAM2.
     384
     385(** The following is a relational presentation of
     386  [transform_program_partial2].  Given relations between function
     387  definitions and between variable information, it defines a relation
     388  between programs stating that the two programs have the same shape
     389  (same global names, etc) and that identically-named function definitions
     390  are variable information are related. *)
     391
     392Section MATCH_PROGRAM.
     393
     394Variable A B V W: Type.
     395Variable match_fundef: A -> B -> Prop.
     396Variable match_varinfo: V -> W -> Prop.
     397
     398Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
     399  match x1, x2 with
     400  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
     401  end.
     402
     403Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
     404  match x1, x2 with
     405  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
     406  end.
     407
     408Definition match_program (p1: program A V) (p2: program B W) : Prop :=
     409  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
     410  /\ p1.(prog_main) = p2.(prog_main)
     411  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
     412
     413End MATCH_PROGRAM.
     414
     415Remark transform_partial_program2_match:
     416  forall (A B V W: Type)
     417         (transf_partial_function: A -> res B)
     418         (transf_partial_variable: V -> res W)
     419         (p: program A V) (tp: program B W),
     420  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
     421  match_program
     422    (fun fd tfd => transf_partial_function fd = OK tfd)
     423    (fun info tinfo => transf_partial_variable info = OK tinfo)
     424    p tp.
     425Proof.
     426  intros. monadInv H. split.
     427  apply list_forall2_imply with
     428    (fun (ab: ident * A) (ac: ident * B) =>
     429       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
     430  eapply map_partial_forall2. eauto.
     431  intros. destruct v1; destruct v2; simpl in *. auto.
     432  split. auto.
     433  apply list_forall2_imply with
     434    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
     435       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
     436  eapply map_partial_forall2. eauto.
     437  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
     438Qed.
     439*)
     440(* * * External functions *)
     441
     442(* * For most languages, the functions composing the program are either
     443  internal functions, defined within the language, or external functions
     444  (a.k.a. system calls) that emit an event when applied.  We define
     445  a type for such functions and some generic transformation functions. *)
     446
     447record external_function : Type[0] ≝ {
     448  ef_id: ident;
     449  ef_sig: signature
     450}.
     451
     452definition ExternalFunction ≝ external_function.
     453definition external_function_tag ≝ ef_id.
     454definition external_function_sig ≝ ef_sig.
     455
     456inductive fundef (F: Type[0]): Type[0] ≝
     457  | Internal: F → fundef F
     458  | External: external_function → fundef F.
     459(*
     460(* Implicit Arguments External [F]. *)
     461(*
     462Section TRANSF_FUNDEF.
     463
     464Variable A B: Type.
     465Variable transf: A -> B.
     466*)
     467definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
     468λA,B,transf,fd.
     469  match fd with
     470  [ Internal f ⇒ Internal ? (transf f)
     471  | External ef ⇒ External ? ef
     472  ].
     473*)
     474(*
     475End TRANSF_FUNDEF.
     476
     477Section TRANSF_PARTIAL_FUNDEF.
     478
     479Variable A B: Type.
     480Variable transf_partial: A -> res B.
     481
     482Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
     483  match fd with
     484  | Internal f => do f' <- transf_partial f; OK (Internal f')
     485  | External ef => OK (External ef)
     486  end.
     487
     488End TRANSF_PARTIAL_FUNDEF.
     489*)
     490
     491
     492
     493(* Partially merged stuff derived from the prototype cerco compiler. *)
    9494
    10495definition bool_to_Prop ≝
     
    20505  ].
    21506
     507(* TODO: merge in comparison definitions from Integers.ma. *)
    22508inductive Compare: Type[0] ≝
    23509  Compare_Equal: Compare
     
    27513| Compare_GreaterEqual: Compare.
    28514
     515(* XXX unused definitions
    29516inductive Cast: Type[0] ≝
    30517  Cast_Int: Byte → Cast
     
    32519| Cast_StackOffset: Immediate → Cast.
    33520
    34 (*
    35 inductive Op1: Type[0] ≝
    36   Op1_Cast8U: Op1
    37 | Op1_Cast8S: Op1
    38 | Op1_Cast16U: Op1
    39 | Op1_Cast16S: Op1
    40 | Op1_NegInt: Op1
    41 | Op1_NotBool: Op1
    42 | Op1_NotInt: Op1
    43 (*
    44 | Op1_NegFloat: Op1
    45 | Op1_AbsFloat: Op1
    46 | Op1_SingleOfFloat: Op1
    47 | Op1_IntOfFloat: Op1
    48 | Op1_IntUOfFloat: Op1
    49 | Op1_FloatOfInt: Op1
    50 | Op1_FloatOfIntU: Op1
    51 *)
    52 | Op1_Id: Op1
    53 | Op1_PtrOfInt: Op1
    54 | Op1_IntOfPtr: Op1.
    55 
    56 inductive Op2: Type[0] ≝
    57   Op2_Add: Op2
    58 | Op2_Sub: Op2
    59 | Op2_Mul: Op2
    60 | Op2_Div: Op2
    61 | Op2_DivU: Op2
    62 | Op2_Mod: Op2
    63 | Op2_ModU: Op2
    64 | Op2_And: Op2
    65 | Op2_Or: Op2
    66 | Op2_XOr: Op2
    67 | Op2_ShL: Op2
    68 | Op2_ShR: Op2
    69 | Op2_ShRU: Op2
    70 | Op2_AddF: Op2
    71 | Op2_SubF: Op2
    72 | Op2_MulF: Op2
    73 | Op2_DivF: Op2
    74 | Op2_Cmp: Compare → Op2
    75 | Op2_CmpU: Compare → Op2
    76 (*
    77 | Op2_CmpF: Compare → Op2
    78 *)
    79 | Op2_AddP: Op2
    80 | Op2_SubP: Op2
    81 | Op2_CmpP: Compare → Op2.
    82 *)
    83 
    84521inductive Data: Type[0] ≝
    85522  Data_Reserve: nat → Data
     
    91528| DataSize_HalfWord: DataSize
    92529| DataSize_Word: DataSize.
    93 
    94 inductive SigType: Type[0] ≝
    95   SigType_Int: SigType
    96 (*
    97 | SigType_Float: SigType
    98 *)
    99 | SigType_Ptr: SigType.
    100 
    101 inductive TypeReturn: Type[0] ≝
    102   TypeReturn_Ret: SigType → TypeReturn
    103 | TypeReturn_Void: TypeReturn.
    104 
    105 record Signature: Type[0] ≝
    106 {
    107   signature_args: list SigType;
    108   signature_return: TypeReturn
    109 }.
    110 
    111 record ExternalFunction: Type[0] ≝
    112 {
    113   external_function_tag: Identifier;
    114   external_function_sig: Signature
    115 }.
     530*)
    116531
    117532definition Trace ≝ list Identifier.
  • src/common/CostLabel.ma

    r738 r747  
    1 include "Clight/AST.ma".
     1include "common/AST.ma".
    22
    33axiom CostTag : String.
  • src/common/Globalenvs.ma

    r744 r747  
    3535
    3636include "common/Errors.ma".
    37 include "Clight/AST.ma".
     37include "common/AST.ma".
    3838(*include "Values.ma".*)
    3939include "common/Mem.ma".
  • src/common/Maps.ma

    r700 r747  
    3535include "utilities/Coqlib.ma".
    3636(* XXX: For ident type; should maybe follow original and use positives *)
    37 include "Clight/AST.ma".
     37include "common/AST.ma".
    3838
    3939(*
  • src/common/Values.ma

    r744 r747  
    1818
    1919include "utilities/Coqlib.ma".
    20 include "Clight/AST.ma".
     20include "common/AST.ma".
    2121include "common/Integers.ma".
    2222include "common/Floats.ma".
     
    2828
    2929include "utilities/binary/Z.ma".
     30include "utilities/extralib.ma".
    3031
    3132(* To define pointers we need a few details about the memory model.
  • src/utilities/Coqlib.ma

    r744 r747  
    1818    library. *)
    1919
    20 include "utilities/binary/Z.ma".
    2120include "basics/types.ma".
    2221include "basics/list.ma".
    2322
    24 include "utilities/extralib.ma".
    2523include "ASM/Util.ma".
    2624
     
    350348*)
    351349(* * Properties of powers of two. *)
    352 
     350(*
    353351lemma two_power_nat_O : two_power_nat O = one.
    354352// qed.
     
    362360[ //
    363361| normalize #p elim p // #p' #H >(nat_succ_pos …) //
    364 ] qed.
     362] qed.*)
    365363(*
    366364Lemma two_p_monotone:
Note: See TracChangeset for help on using the changeset viewer.