Changeset 1224 for src/common

Timestamp:

Sep 16, 2011, 6:39:05 PM (9 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:

• AST.ma (modified) (5 diffs)
• Globalenvs.ma (modified) (2 diffs)
• IntValue.ma (deleted)

src/common/AST.ma

@@ -283 +283 @@
 programs are common to all languages. *)
 
-record program (F,V: Type[0]) : Type[0] := {
-  prog_funct: list (ident × F);
-  prog_main: ident;
-  prog_vars: list (ident × region × V)
+record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
+  prog_vars: list (ident × region × V);
+  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
+  prog_main: ident
 }.
 
 
-definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
-  map ? ? (fst ident F) (prog_funct ?? p).
-
-definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
-  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
+definition prog_funct_names ≝ λF,V. λp: program F V.
+  map … \fst (prog_funct … p).
+
+definition prog_var_names ≝ λF,V. λp: program F V.
+  map … (λx. \fst (\fst x)) (prog_vars … p).
 
 (* * * Generic transformations over programs *)
@@ -312 +312 @@
   map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
 
-definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
-λA,B,V,transf,p.
+definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
+λA,B,V,p,transf.
   mk_program B V
+    (prog_vars A V p)
     (transf_program ?? transf (prog_funct A V p))
-    (prog_main A V p)
-    (prog_vars A V p).
+    (prog_main A V p).
 (*
 lemma transform_program_function:
@@ -346 +346 @@
                          list (A × B) → res (list (A × C)) ≝
 λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
+
+lemma map_partial_preserves_first:
+ ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
+  map_partial … f l = OK ? l' →
+   map … \fst l = map … \fst l'.
+ #A #B #C #f #l elim l
+  [ #l' #E normalize in E; destruct %
+  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
+    [2: #err #E destruct
+    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
+      cases (map_partial … f tl) in IH ⊢ %
+      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
+      >(IH x) // ]]
+qed.
+
 (*
 Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
@@ -418 +433 @@
   MSG "In function " :: CTX id :: MSG ": " :: nil.
 *)
-definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
-λA,B,V,transf_partial,p.
-  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
-  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
+definition 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) ≝
+λA,B,V,p,transf_partial.
+  do fl ← map_partial … transf_partial (prog_funct … p);
+  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
+
 (*
 Lemma transform_partial_program_function:
@@ -464 +480 @@
   MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
 *)
-definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
-                                        program A V → res (program B W) ≝
-λA,B,V,W, transf_partial_function, transf_partial_variable, p.
-  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
-  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
-  OK ? (mk_program … fl (prog_main ?? p) vl).
+
+(* CSC: ad hoc lemma, move away? *)
+lemma map_fst:
+ ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
+  map … \fst l = map … \fst l' →
+  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
+#A #B #C #C' #l elim l
+ [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
+ | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
+   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
+   >e0 in e1 normalize #H @H ]
+qed.
+
+definition transform_partial_program2 :
+ ∀A,B,V,W. ∀p: program A V.
+  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
+  →  (V → res W) → res (program B W) ≝
+λA,B,V,W,p, transf_partial_function, transf_partial_variable.
+  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
+  (*CSC: interactive mode because of dependent types *)
+  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
+  cases (map_partial … transf_partial_variable (prog_vars … p))
+  [ #vl #EQ
+    @(OK (program B W) (mk_program … vl … (prog_main … p)))
+    <(map_fst … (EQ vl (refl …))) @fl
+  | #err #_ @(Error … err)]
+qed.
+
 (*
 Lemma transform_partial_program2_function:

src/common/Globalenvs.ma

@@ -52 +52 @@
        of function descriptions. *)
 
-  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
+  globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p)));
    (* * Return the global environment for the given program. *)
 
-  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
+  init_mem: ∀F,V. (V → list init_data) → program F V → res mem;
    (* * Return the initial memory state for the given program. *)
 
@@ -502 +502 @@
     (OK ? init_env) vars.
 
-definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
+definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝
 λF,V,init_info,p.
-  add_globals F V init_info
+  add_globals … init_info
    〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    (prog_vars ?? p).
 
-definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
+definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝
 λF,V,i,p.
   do 〈g,m〉 ← globalenv_initmem F V i p;
     OK ? g.
-definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
+definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝
 λF,V,i,p.
   do 〈g,m〉 ← globalenv_initmem F V i p;