Changeset 1608


Ignore:
Timestamp:
Dec 14, 2011, 2:30:39 PM (8 years ago)
Author:
sacerdot
Message:

Porting to new library still in progress.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1605 r1608  
    567567      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
    568568  ]
    569 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
     569] and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
    570570match e with
    571571[ Expr ed _ ⇒
     
    573573  [ Evar id ⇒
    574574      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    575       match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
    576       [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
    577       | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
     575      match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
     576      [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol id 0), ?»❭
     577      | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
    578578      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    579579      ]
    580580  | Ederef e1 ⇒
    581581      do e1' ← translate_expr vars e1;
    582       match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
    583       [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
     582      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with
     583      [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭
    584584      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    585585      ] e1'
     
    590590          do off ← field_offset id fl;
    591591          match e1' with
    592           [ mk_DPair r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
     592          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) (❬r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» ❭)
    593593          ]
    594594      | Tunion _ _ ⇒ translate_addr vars e1
     
    601601[ >E @I
    602602| >(E ? (refl ??)) @refl
    603 | 3,4: @use_sig
    604 | @(translate_binop_vars … E) @use_sig
    605 | % [ % ] @use_sig
    606 | % [ % @use_sig ] whd @I
    607 | % [ % [ @use_sig | @I ] | @use_sig ]
    608 | % [ @use_sig | @I ]
    609 | % [ @use_sig | @I ]
     603| 3,4: @pi2
     604| @(translate_binop_vars … E) @pi2
     605| % [ % ] @pi2
     606| % [ % @pi2 ] whd @I
     607| % [ % [ @pi2 | @I ] | @pi2 ]
     608| % [ @pi2 | @I ]
     609| % [ @pi2 | @I ]
    610610| >(access_mode_typ … E) @refl
    611 | @use_sig
    612 | @use_sig
    613 | % [ @use_sig | @I ]
     611| @pi2
     612| @pi2
     613| % [ @pi2 | @I ]
    614614] qed.
    615615
     
    637637        | _ ⇒
    638638            do e1' ← translate_addr vars e1;
    639             match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
     639            match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r q e1') ]
    640640        ]
    641641    ].
     
    690690].
    691691#ls whd %
    692 [ % // @use_sig
     692[ % // @pi2
    693693| @I
    694 | % @use_sig
     694| % @pi2
    695695| @I
    696696] qed.
     
    703703].
    704704
    705 definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝
     705definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(𝚺t:typ.CMexpr t). match e with [ mk_DPair t e ⇒ expr_vars t e (local_id vars) ]) ≝
    706706λv,e.
    707707  do e' ← translate_expr v e;
    708   OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
    709 whd @use_sig
     708  OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?».
     709whd @pi2
    710710qed.
    711711
     
    802802| Sassign e1 e2 ⇒
    803803    do s' ← translate_assign vars e1 e2;
    804     OK ? «〈eject ?? s', u〉, ?»
     804    OK ? «〈pi1 ?? s', u〉, ?»
    805805| Scall ret ef args ⇒
    806806    do ef' ← translate_expr vars ef;
    807807    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
    808     do args' ← mmap_sigma (translate_expr_sigma vars) args;
     808    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
    809809    match ret with
    810810    [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?»
     
    874874    | Some e1 ⇒
    875875        do e1' ← translate_expr vars e1;
    876         OK ? «〈St_return (Some ? (dp … e1')), u〉, ?»
     876        OK ? «〈St_return (Some ? (mk_Sig … e1')), u〉, ?»
    877877    ]
    878878| Sswitch e1 ls ⇒ Error ? (msg FIXME)
     
    892892try (#l #H @(match H in False with [ ]))
    893893try (#id #H @H)
    894 [ @add_tmps_oblivious @(use_sig ?? s')
     894[ @add_tmps_oblivious @(pi2 ?? s')
    895895| @local_id_add_tmps_oblivious @p
    896896]
    897 try (@use_sig' #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
    898 [ 1,3,6: @use_sig' #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
     897try (@sub_pi2 #x @expr_vars_mp #i @local_id_add_tmps_oblivious)
     898[ 1,3,6: @sub_pi2 #x @All_mp * #ty #e @expr_vars_mp #i @local_id_add_tmps_oblivious
    899899| 2,4: @(local_id_fresh_tmp … Etmp)
    900900| @(alloc_tmp_preserves … Etmp)
     
    928928| #id #H @(π2 H3) @(π2 H2) @(π2 H1) @H
    929929(* Slabel *)
    930 | %{l} @E
    931 | @(π1 (π1 H1))
    932 | #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
    933 | @(π2 H1)
     930|31: %{l} @E
     931|32: @(π1 (π1 H1))
     932|33: #l'' * [ #E <E %{l'} % // %1 @refl | #EX cases (π2 (π1 H1) l'' EX) #l4 * #LK #LD %{l4} % // %2 @LD ]
     933|34: @(π2 H1)
    934934(* Sgoto *)
    935 | %{l} @E
    936 | @(π1 (π1 H1))
     935|35: %{l} @E
     936|36: @(π1 (π1 H1))
    937937(* Scost *)
    938 | @(π2 (π1 H1))
    939 | @(π2 H1)
     938|37: @(π2 (π1 H1))
     939|38: @(π2 H1)
     940|*: cases daemon (*XXXXX*)
    940941] qed.
    941942
     
    10081009        let 〈l',u1〉 ≝ fresh … u in
    10091010        do lbls1 ← populate_lenv t (add … lbls l l') u1;
    1010         OK ? «eject … lbls1, ?»
     1011        OK ? «pi1 … lbls1, ?»
    10111012    ] (refl ? (lookup_label lbls l))
    10121013].
  • src/Cminor/initialisation.ma

    r1605 r1608  
    5959λvars. foldr ? (Σs:stmt. stmt_inv s)
    6060  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst var)) (\snd (\fst var)) (\snd var))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    61 % [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
     61% [ % [ % // | @(pi2 ? stmt_inv) ] | @(pi2 ? stmt_inv) ]
    6262qed.
    6363
  • src/common/Errors.ma

    r1601 r1608  
    9191(* Dependent pair version. *)
    9292notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    93   for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     93  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
    9494
    9595lemma Prod_extensionality:
Note: See TracChangeset for help on using the changeset viewer.