Changeset 1224


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
Files:
1 deleted
15 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r1139 r1224  
    540540@opt_bind_OK #x cases x; #sp #b #esb
    541541@opt_bind_OK #f #ef
    542 whd; % [ whd in ⊢ (???(??%)) // | @(initial_state_intro … Ege Em esb ef) ]
     542whd; % [ whd in ⊢ (???(??%)) @Ege | @(initial_state_intro … Ege Em esb ef) ]
    543543qed.
    544544
  • src/Clight/Csyntax.ma

    r1139 r1224  
    318318  data.  See module [AST] for more details. *)
    319319
    320 definition clight_program : Type[0] ≝ program clight_fundef (list init_data × type).
     320definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
    321321
    322322(* * * Operations over types *)
  • src/Clight/SimplifyCasts.ma

    r1198 r1224  
    194194
    195195definition simplify_program : clight_program → clight_program ≝
    196 transform_program ??? simplify_fundef.
     196λp. transform_program … p simplify_fundef.
  • src/Clight/label.ma

    r1056 r1224  
    187187
    188188definition clight_label : clight_program → res clight_program ≝
    189   transform_partial_program ??? label_fundef.
     189 λp. transform_partial_program … p label_fundef.
  • src/Clight/test/search.c.ma

    r1139 r1224  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
     4definition myprog := mk_program (λ_.clight_fundef) ((list init_data) × type)
     5  []
    56  [〈ident_of_nat 0 (* search *), CL_Internal (
    67     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
     
    181182  )〉]
    182183  (ident_of_nat 7)
    183   []
    184184.
    185185
  • src/Clight/toCminor.ma

    r1207 r1224  
    691691  let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in
    692692  let globals ≝ fun_globals @ var_globals in
    693   transform_partial_program2 ???? (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)) p.
     693  transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)).
  • src/Cminor/initialisation.ma

    r1139 r1224  
    7272λp.
    7373  mk_program ??
     74    (empty_vars (prog_vars ?? p))
    7475    (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    75     (prog_main ?? p)
    76     (empty_vars (prog_vars ?? p)).
    77    
     76    (prog_main ?? p).
  • src/Cminor/syntax.ma

    r1147 r1224  
    4545   responsible for initialisation and we only give the size of each variable. *)
    4646
    47 definition Cminor_program ≝ program (fundef internal_function) (list init_data).
     47definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
    4848
    49 definition Cminor_noinit_program ≝ program (fundef internal_function) nat.
     49definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
  • src/Cminor/toRTLabs.ma

    r1139 r1224  
    296296
    297297definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    298 transform_partial_program ???
    299   (transf_partial_fundef ?? c2ra_function).
     298λp.transform_partial_program … p (transf_partial_fundef … c2ra_function).
    300299
    301300include "Cminor/initialisation.ma".
  • src/LIN/LIN.ma

    r1183 r1224  
    2424      ]
    2525    ].
    26    
     26
     27definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
     28 λglobals.
     29  mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
     30(*CSC: lookup function to be implemented *)
     31cases daemon
     32qed.
     33
     34definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals).
     35
    2736inductive lin_function_definition (globals: list ident): Type[0] ≝
    2837  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
  • src/LTL/LTLToLIN.ma

    r1180 r1224  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
    4 include "common/Graphs.ma".
    54
    65axiom LTLTag: String.
     
    3130    set_member ? (word_of_identifier ? l) g.
    3231   
    33 (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
    34    
    3532definition graph_lookup ≝
    3633  λglobals: list ident.
    3734  λl: label.
    38   λgr: ltl_statement_graph globals.
     35  λgr: graph (ltl_statement globals).
    3936    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    4037   
    41 definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    42   λglobals: list ident.
    43   λl: label.
    44   λg: ltl_statement_graph globals.
    45     graph_lookup globals l g.
     38definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝
     39  λglobals,l,g.graph_lookup globals l g.
    4640
    4741definition foo ≝
     
    4943  λvisit:
    5044  ∀globals: list ident.
    51   ∀g: ltl_statement_graph globals.
     45  ∀g: graph (ltl_statement globals).
    5246  ∀required: BitVectorTrieSet 16.
    5347  ∀visited: BitVectorTrieSet 16.
     
    6559*)
    6660let rec visit
    67   (globals: list ident) (g: ltl_statement_graph globals)
     61  (globals: list ident) (g: graph (ltl_statement globals))
    6862  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    6963  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
  • src/RTLabs/RTLAbstoRTL.ma

    r1149 r1224  
    12861286
    12871287definition translate ≝
    1288   λp: program (fundef internal_function) unit.
     1288  λp: program (λ_.fundef internal_function) nat.
    12891289  let f_funct ≝ λid_fun_def.
    12901290    let 〈id, fun_def〉 ≝ id_fun_def in
    1291       〈id, translate_fun_def fun_def〉
    1292   in
    1293   let vars' ≝ map ? ? (λx.
    1294     let 〈id_init_ignore, ignore〉 ≝ x in
    1295     let 〈id_init, ignore〉 ≝ id_init_ignore in
    1296     let 〈id, init〉 ≝ id_init in
    1297     let init_total ≝ foldr ? ? plus 0 (map ? ? init_data_to_nat init) in
    1298       〈id, init_total〉) (prog_vars ? ? p)
    1299   in
     1291      〈id, translate_fun_def fun_def〉 in
     1292  (*CSC: bug here: we are throwing away the regions doing no checks at all *)
     1293  let vars' ≝ map … (λx. let 〈id,reg,n〉 ≝ x in 〈id,n〉) (prog_vars … p) in
    13001294  let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in
    13011295  let main' ≝ prog_main ? ? p in
  • src/RTLabs/syntax.ma

    r1147 r1224  
    4343   allocate. *)
    4444
    45 definition RTLabs_program ≝ program (fundef internal_function) nat.
    46 
     45definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
  • 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.