Changeset 764 for src/common


Ignore:
Timestamp:
Apr 20, 2011, 5:38:58 PM (9 years ago)
Author:
campbell
Message:

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r757 r764  
    184184definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    185185  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
    186 (*
    187 (** * Generic transformations over programs *)
    188 
    189 (** We now define a general iterator over programs that applies a given
     186
     187(* * * Generic transformations over programs *)
     188
     189(* * We now define a general iterator over programs that applies a given
    190190  code transformation function to all function descriptions and leaves
    191191  the other parts of the program unchanged. *)
    192 
     192(*
    193193Section TRANSF_PROGRAM.
    194194
     
    231231Variable prefix_errmsg: A -> errmsg.
    232232Variable f: B -> res C.
    233 
     233*)
     234definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
     235                         list (A × B) → res (list (A × C)) ≝
     236λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     237(*
    234238Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
    235239  match l with
     
    302306Definition prefix_funct_name (id: ident) : errmsg :=
    303307  MSG "In function " :: CTX id :: MSG ": " :: nil.
    304 
    305 Definition transform_partial_program (p: program A V) : res (program B V) :=
    306   do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
    307   OK (mkprogram fl p.(prog_main) p.(prog_vars)).
    308 
     308*)
     309definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
     310λA,B,V,transf_partial,p.
     311  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
     312  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
     313(*
    309314Lemma transform_partial_program_function:
    310315  forall p tp i tf,
     
    347352Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
    348353  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
    349 
    350 Definition transform_partial_program2 (p: program A V) : res (program B W) :=
    351   do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
    352   do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
    353   OK (mkprogram fl p.(prog_main) vl).
    354 
     354*)
     355definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
     356                                        program A V → res (program B W) ≝
     357λA,B,V,W, transf_partial_function, transf_partial_variable, p.
     358  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
     359  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
     360  OK ? (mk_program … fl (prog_main ?? p) vl).
     361(*
    355362Lemma transform_partial_program2_function:
    356363  forall p tp i tf,
     
    457464  | Internal: F → fundef F
    458465  | External: external_function → fundef F.
    459 (*
     466
    460467(* Implicit Arguments External [F]. *)
    461468(*
     
    471478  | External ef ⇒ External ? ef
    472479  ].
    473 *)
     480
    474481(*
    475482End TRANSF_FUNDEF.
     
    479486Variable A B: Type.
    480487Variable transf_partial: A -> res B.
    481 
    482 Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
     488*)
     489
     490definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
     491λA,B,transf_partial,fd.
    483492  match fd with
    484   | Internal f => do f' <- transf_partial f; OK (Internal f')
    485   | External ef => OK (External ef)
    486   end.
    487 
     493  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
     494  | External ef ⇒ OK ? (External ? ef)
     495  ].
     496(*
    488497End TRANSF_PARTIAL_FUNDEF.
    489498*)
  • src/common/Errors.ma

    r695 r764  
    6161  ].
    6262
     63definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
     64  match f with
     65  [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
     66  | Error (*msg*) => Error ? (*msg*)
     67  ].
     68 
    6369(* Not sure what level to use *)
    6470notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     
    7278notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    7379interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
     80notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
     81notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
     82notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
     83notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
     84interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f).
    7485(*interpretation "error monad ret" 'ret e = (ret ? e).
    7586notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
Note: See TracChangeset for help on using the changeset viewer.