Changeset 1224 for src/common


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (8 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

Location:
src/common
Files:
1 deleted
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1213 r1224  
    283283programs are common to all languages. *)
    284284
    285 record program (F,V: Type[0]) : Type[0] := {
    286   prog_funct: list (ident × F);
    287   prog_main: ident;
    288   prog_vars: list (ident × region × V)
     285record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
     286  prog_vars: list (ident × region × V);
     287  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
     288  prog_main: ident
    289289}.
    290290
    291291
    292 definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    293   map ? ? (fst ident F) (prog_funct ?? p).
    294 
    295 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    296   map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
     292definition prog_funct_names ≝ λF,V. λp: program F V.
     293  map … \fst (prog_funct … p).
     294
     295definition prog_var_names ≝ λF,V. λp: program F V.
     296  map … (λx. \fst (\fst x)) (prog_vars … p).
    297297
    298298(* * * Generic transformations over programs *)
     
    312312  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
    313313
    314 definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
    315 λA,B,V,transf,p.
     314definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
     315λA,B,V,p,transf.
    316316  mk_program B V
     317    (prog_vars A V p)
    317318    (transf_program ?? transf (prog_funct A V p))
    318     (prog_main A V p)
    319     (prog_vars A V p).
     319    (prog_main A V p).
    320320(*
    321321lemma transform_program_function:
     
    346346                         list (A × B) → res (list (A × C)) ≝
    347347λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     348
     349lemma map_partial_preserves_first:
     350 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
     351  map_partial … f l = OK ? l' →
     352   map … \fst l = map … \fst l'.
     353 #A #B #C #f #l elim l
     354  [ #l' #E normalize in E; destruct %
     355  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
     356    [2: #err #E destruct
     357    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
     358      cases (map_partial … f tl) in IH ⊢ %
     359      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
     360      >(IH x) // ]]
     361qed.
     362
    348363(*
    349364Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
     
    418433  MSG "In function " :: CTX id :: MSG ": " :: nil.
    419434*)
    420 definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
    421 λA,B,V,transf_partial,p.
    422   do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
    423   OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
     435definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
     436λA,B,V,p,transf_partial.
     437  do fl ← map_partial … transf_partial (prog_funct … p);
     438  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
     439
    424440(*
    425441Lemma transform_partial_program_function:
     
    464480  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
    465481*)
    466 definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
    467                                         program A V → res (program B W) ≝
    468 λA,B,V,W, transf_partial_function, transf_partial_variable, p.
    469   do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
    470   do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
    471   OK ? (mk_program … fl (prog_main ?? p) vl).
     482
     483(* CSC: ad hoc lemma, move away? *)
     484lemma map_fst:
     485 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
     486  map … \fst l = map … \fst l' →
     487  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
     488#A #B #C #C' #l elim l
     489 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
     490 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
     491   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
     492   >e0 in e1 normalize #H @H ]
     493qed.
     494
     495definition transform_partial_program2 :
     496 ∀A,B,V,W. ∀p: program A V.
     497  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
     498  →  (V → res W) → res (program B W) ≝
     499λA,B,V,W,p, transf_partial_function, transf_partial_variable.
     500  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
     501  (*CSC: interactive mode because of dependent types *)
     502  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
     503  cases (map_partial … transf_partial_variable (prog_vars … p))
     504  [ #vl #EQ
     505    @(OK (program B W) (mk_program … vl … (prog_main … p)))
     506    <(map_fst … (EQ vl (refl …))) @fl
     507  | #err #_ @(Error … err)]
     508qed.
     509
    472510(*
    473511Lemma transform_partial_program2_function:
  • src/common/Globalenvs.ma

    r1139 r1224  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
     54  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p)));
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
     57  init_mem: ∀F,V. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     504definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝
    505505λF,V,init_info,p.
    506   add_globals F V init_info
     506  add_globals init_info
    507507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     510definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝
    511511λF,V,i,p.
    512512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     514definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
    515515λF,V,i,p.
    516516  do 〈g,m〉 ← globalenv_initmem F V i p;
Note: See TracChangeset for help on using the changeset viewer.