Changeset 2645 for src/ERTLptr


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (8 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
Location:
src/ERTLptr
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr.ma

    r2604 r2645  
    2929definition ertlptr_seq_joint ≝ extension_seq ERTLptr.
    3030coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint
    31   on _s : ertlptr_seq to joint_seq ERTLptr.
     31  on _s : ertlptr_seq to joint_seq ERTLptr ?.
    3232 
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2638 r2645  
    288288
    289289definition map_inf1 :  ∀A, B: Type[0].
    290   ∀tag: String.
     290  ∀tag: identifierTag.
    291291  ∀m:identifier_map tag A.
    292292   (∀a:A.(Σid. lookup tag A m id = Some A a) → B) →
     
    311311
    312312lemma map_inf_add : ∀ A, B : Type[0].
    313   ∀tag : String.
     313  ∀tag : identifierTag.
    314314  ∀m: identifier_map tag A.
    315315  ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    365365                                    id_is_in A (p1 x) (pm_node … opt_a l r).
    366366
    367 definition id_is_in : ∀A : Type[0]. ∀tag : String.
     367definition id_is_in : ∀A : Type[0]. ∀tag : identifierTag.
    368368identifier_map tag A → identifier tag → Prop ≝
    369369λA,tag,m,id.match id with
     
    373373(*
    374374lemma lookup_map : ∀A,B : Type[0].
    375   ∀tag : String.
     375  ∀tag : identifierTag.
    376376  ∀m : identifier_map tag A.
    377377  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    400400(*
    401401lemma lookup_map_weak : ∀ A,B : Type[0].
    402   ∀tag : String.
     402  ∀tag : identifierTag.
    403403  ∀m : identifier_map tag A.
    404404  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    410410
    411411lemma lookup_map_fail : ∀A,B : Type[0].
    412 ∀tag : String.
     412∀tag : identifierTag.
    413413  ∀m : identifier_map tag A.
    414414  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    464464
    465465lemma lookup_ok_to_update : ∀ A : Type[0].
    466 ∀ tag : String.
     466∀ tag : identifierTag.
    467467∀m,m' : identifier_map tag A. ∀id,a.
    468468(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? →
     
    531531
    532532lemma update_ok_to_lookup : ∀ A : Type[0].
    533 ∀ tag : String.
     533∀ tag : identifierTag.
    534534∀m,m' : identifier_map tag A. ∀id,a.
    535535update tag A m id a = return m' →
     
    585585               
    586586lemma update_lookup_after : ∀ A : Type[0].
    587 ∀ tag : String.
     587∀ tag : identifierTag.
    588588∀m,m' : identifier_map tag A. ∀id,a.
    589589update tag A m id a = return m' →
     
    602602qed.
    603603
    604 lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : String.
     604lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : identifierTag.
    605605∀m : identifier_map tag A.
    606606∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
     
    628628
    629629lemma map_update_commute : ∀ A, B : Type[0].
    630 ∀tag : String.
     630∀tag : identifierTag.
    631631∀m1,m2 : identifier_map tag A.
    632632∀id,a.
     
    680680
    681681lemma lookup_map : ∀A,B : Type[0].
    682   ∀tag : String.
     682  ∀tag : identifierTag.
    683683  ∀m : identifier_map tag A.
    684684  ∀ f:A → B.
     
    723723qed.
    724724
    725 lemma map_add : ∀tag : String.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
     725lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
    726726map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
    727727#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
     
    754754unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
    755755 
    756 lemma map_update_commute : ∀tag : String.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
     756lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
    757757update tag B (map tag A B m f) id (f v) =
    758758!m' ← update tag A m id v; return map tag A B m' f.
     
    857857qed.
    858858*)
    859 lemma lookup_eq_id_map : ∀tag : String. ∀ A : Type[0].
     859lemma lookup_eq_id_map : ∀tag : identifierTag. ∀ A : Type[0].
    860860∀m,m' : identifier_map tag A.
    861861(∀id. lookup … m id = lookup … m' id
     
    866866
    867867(*
    868 lemma clean_leaf : ∀tag : String . ∀ A : Type[0].
     868lemma clean_leaf : ∀tag : identifierTag . ∀ A : Type[0].
    869869∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) →
    870870clean ?? m = empty_map ??.
Note: See TracChangeset for help on using the changeset viewer.