From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 276 ++++++++++++++++++++++++++-------------------------- 1 file changed, 137 insertions(+), 139 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 664c6fc..5ab685d 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -1,19 +1,14 @@ Require Import Coqlib. +Require Import Errors. Require Import Integers. Require Import Floats. Require Import AST. Require Import Csyntax. +Require Import Cminor. Require Import Csharpminor. -(** The error monad *) - -Definition bind (A B: Set) (f: option A) (g: A -> option B) := - match f with None => None | Some x => g x end. - -Implicit Arguments bind [A B]. - -Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). +Open Local Scope string_scope. +Open Local Scope error_monad_scope. (** ** Operations on C types *) @@ -22,28 +17,28 @@ Definition signature_of_function (f: Csyntax.function) : signature := (typlist_of_typelist (type_of_params (Csyntax.fn_params f))) (opttyp_of_type (Csyntax.fn_return f)). -Definition chunk_of_type (ty: type): option memory_chunk := +Definition chunk_of_type (ty: type): res memory_chunk := match access_mode ty with - | By_value chunk => Some chunk - | _ => None + | By_value chunk => OK chunk + | _ => Error (msg "Cshmgen.chunk_of_type") end. -Definition var_kind_of_type (ty: type): option var_kind := +Definition var_kind_of_type (ty: type): res var_kind := match ty with - | Tint I8 Signed => Some(Vscalar Mint8signed) - | Tint I8 Unsigned => Some(Vscalar Mint8unsigned) - | Tint I16 Signed => Some(Vscalar Mint16signed) - | Tint I16 Unsigned => Some(Vscalar Mint16unsigned) - | Tint I32 _ => Some(Vscalar Mint32) - | Tfloat F32 => Some(Vscalar Mfloat32) - | Tfloat F64 => Some(Vscalar Mfloat64) - | Tvoid => None - | Tpointer _ => Some(Vscalar Mint32) - | Tarray _ _ => Some(Varray (Csyntax.sizeof ty)) - | Tfunction _ _ => None - | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty)) - | Tunion _ fList => Some(Varray (Csyntax.sizeof ty)) - | Tcomp_ptr _ => Some(Vscalar Mint32) + | Tint I8 Signed => OK(Vscalar Mint8signed) + | Tint I8 Unsigned => OK(Vscalar Mint8unsigned) + | Tint I16 Signed => OK(Vscalar Mint16signed) + | Tint I16 Unsigned => OK(Vscalar Mint16unsigned) + | Tint I32 _ => OK(Vscalar Mint32) + | Tfloat F32 => OK(Vscalar Mfloat32) + | Tfloat F64 => OK(Vscalar Mfloat64) + | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)") + | Tpointer _ => OK(Vscalar Mint32) + | Tarray _ _ => OK(Varray (Csyntax.sizeof ty)) + | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)") + | Tstruct _ fList => OK(Varray (Csyntax.sizeof ty)) + | Tunion _ fList => OK(Varray (Csyntax.sizeof ty)) + | Tcomp_ptr _ => OK(Vscalar Mint32) end. (** ** Csharpminor constructors *) @@ -60,19 +55,14 @@ end. denoting a case where the operation is not defined at the given types. *) -Definition make_intconst (n: int) := Eop (Ointconst n) Enil. - -Definition make_floatconst (f: float) := Eop (Ofloatconst f) Enil. - -Definition make_unop (op: operation) (e: expr) := Eop op (Econs e Enil). +Definition make_intconst (n: int) := Econst (Ointconst n). -Definition make_binop (op: operation) (e1 e2: expr) := - Eop op (Econs e1 (Econs e2 Enil)). +Definition make_floatconst (f: float) := Econst (Ofloatconst f). Definition make_floatofint (e: expr) (sg: signedness) := match sg with - | Signed => make_unop Ofloatofint e - | Unsigned => make_unop Ofloatofintu e + | Signed => Eunop Ofloatofint e + | Unsigned => Eunop Ofloatofintu e end. (* [make_boolean e ty] returns a Csharpminor expression that evaluates @@ -84,98 +74,98 @@ Definition make_floatofint (e: expr) (sg: signedness) := *) Definition make_boolean (e: expr) (ty: type) := match ty with - | Tfloat _ => make_binop (Ocmpf Cne) e (make_floatconst Float.zero) + | Tfloat _ => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) | _ => e end. Definition make_neg (e: expr) (ty: type) := match ty with - | Tint _ _ => Some (make_binop Osub (make_intconst Int.zero) e) - | Tfloat _ => Some (make_unop Onegf e) - | _ => None + | Tint _ _ => OK (Eunop Onegint e) + | Tfloat _ => OK (Eunop Onegf e) + | _ => Error (msg "Cshmgen.make_neg") end. Definition make_notbool (e: expr) (ty: type) := match ty with - | Tfloat _ => make_binop (Ocmpf Ceq) e (make_floatconst Float.zero) - | _ => make_unop Onotbool e + | Tfloat _ => Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero) + | _ => Eunop Onotbool e end. Definition make_notint (e: expr) (ty: type) := - make_unop Onotint e. + Eunop Onotint e. Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_ii => Some (make_binop Oadd e1 e2) - | add_case_ff => Some (make_binop Oaddf e1 e2) + | add_case_ii => OK (Ebinop Oadd e1 e2) + | add_case_ff => OK (Ebinop Oaddf e1 e2) | add_case_pi ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Oadd e1 (make_binop Omul n e2)) - | add_default => None + OK (Ebinop Oadd e1 (Ebinop Omul n e2)) + | add_default => Error (msg "Cshmgen.make_add") end. Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with - | sub_case_ii => Some (make_binop Osub e1 e2) - | sub_case_ff => Some (make_binop Osubf e1 e2) + | sub_case_ii => OK (Ebinop Osub e1 e2) + | sub_case_ff => OK (Ebinop Osubf e1 e2) | sub_case_pi ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Osub e1 (make_binop Omul n e2)) + OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Odivu (make_binop Osub e1 e2) n) - | sub_default => None + OK (Ebinop Odivu (Ebinop Osub e1 e2) n) + | sub_default => Error (msg "Cshmgen.make_sub") end. Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_mul ty1 ty2 with - | mul_case_ii => Some (make_binop Omul e1 e2) - | mul_case_ff => Some (make_binop Omulf e1 e2) - | mul_default => None + | mul_case_ii => OK (Ebinop Omul e1 e2) + | mul_case_ff => OK (Ebinop Omulf e1 e2) + | mul_default => Error (msg "Cshmgen.make_mul") end. Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_div ty1 ty2 with - | div_case_I32unsi => Some (make_binop Odivu e1 e2) - | div_case_ii => Some (make_binop Odiv e1 e2) - | div_case_ff => Some (make_binop Odivf e1 e2) - | div_default => None + | div_case_I32unsi => OK (Ebinop Odivu e1 e2) + | div_case_ii => OK (Ebinop Odiv e1 e2) + | div_case_ff => OK (Ebinop Odivf e1 e2) + | div_default => Error (msg "Cshmgen.make_div") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_mod ty1 ty2 with - | mod_case_I32unsi => Some (make_binop Omodu e1 e2) - | mod_case_ii=> Some (make_binop Omod e1 e2) - | mod_default => None + | mod_case_I32unsi => OK (Ebinop Omodu e1 e2) + | mod_case_ii=> OK (Ebinop Omod e1 e2) + | mod_default => Error (msg "Cshmgen.make_mod") end. Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oand e1 e2). + OK(Ebinop Oand e1 e2). Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oor e1 e2). + OK(Ebinop Oor e1 e2). Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oxor e1 e2). + OK(Ebinop Oxor e1 e2). Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oshl e1 e2). + OK(Ebinop Oshl e1 e2). Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_shr ty1 ty2 with - | shr_case_I32unsi => Some (make_binop Oshru e1 e2) - | shr_case_ii=> Some (make_binop Oshr e1 e2) - | shr_default => None + | shr_case_I32unsi => OK (Ebinop Oshru e1 e2) + | shr_case_ii=> OK (Ebinop Oshr e1 e2) + | shr_default => Error (msg "Cshmgen.make_shr") end. Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with - | cmp_case_I32unsi => Some (make_binop (Ocmpu c) e1 e2) - | cmp_case_ii => Some (make_binop (Ocmp c) e1 e2) - | cmp_case_ff => Some (make_binop (Ocmpf c) e1 e2) - | cmp_case_pi => Some (make_binop (Ocmp c) e1 e2) - | cmp_case_pp => Some (make_binop (Ocmp c) e1 e2) - | cmp_default => None + | cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2) + | cmp_case_ii => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2) + | cmp_case_pi => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_pp => OK (Ebinop (Ocmp c) e1 e2) + | cmp_default => Error (msg "Cshmgen.make_shr") end. Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -206,17 +196,17 @@ Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_cast1 (from to: type) (e: expr) := match from, to with | Tint _ uns, Tfloat _ => make_floatofint e uns - | Tfloat _, Tint _ _ => make_unop Ointoffloat e + | Tfloat _, Tint _ _ => Eunop Ointoffloat e | _, _ => e end. Definition make_cast2 (from to: type) (e: expr) := match to with - | Tint I8 Signed => make_unop Ocast8signed e - | Tint I8 Unsigned => make_unop Ocast8unsigned e - | Tint I16 Signed => make_unop Ocast16signed e - | Tint I16 Unsigned => make_unop Ocast16unsigned e - | Tfloat F32 => make_unop Osingleoffloat e + | Tint I8 Signed => Eunop Ocast8signed e + | Tint I8 Unsigned => Eunop Ocast8unsigned e + | Tint I16 Signed => Eunop Ocast16signed e + | Tint I16 Unsigned => Eunop Ocast16unsigned e + | Tfloat F32 => Eunop Osingleoffloat e | _ => e end. @@ -231,9 +221,9 @@ Definition make_cast (from to: type) (e: expr) := Definition make_load (addr: expr) (ty_res: type) := match (access_mode ty_res) with - | By_value chunk => Some (Eload chunk addr) - | By_reference => Some addr - | By_nothing => None + | By_value chunk => OK (Eload chunk addr) + | By_reference => OK addr + | By_nothing => Error (msg "Cshmgen.make_load") end. (* [make_store addr ty_res rhs ty_rhs] stores the value of the @@ -243,8 +233,8 @@ Definition make_load (addr: expr) (ty_res: type) := Definition make_store (addr: expr) (ty: type) (rhs: expr) := match access_mode ty with - | By_value chunk => Some (Sstore chunk addr rhs) - | _ => None + | By_value chunk => OK (Sstore chunk addr rhs) + | _ => Error (msg "Cshmgen.make_store") end. (** ** Reading and writing variables *) @@ -258,9 +248,9 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := Definition var_get (id: ident) (ty: type) := match access_mode ty with - | By_value chunk => Some (Evar id) - | By_reference => Some (Eaddrof id) - | _ => None + | By_value chunk => OK (Evar id) + | By_reference => OK (Eaddrof id) + | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil) end. (* [var_set id ty rhs] stores the value of the Csharpminor @@ -269,21 +259,22 @@ Definition var_get (id: ident) (ty: type) := Definition var_set (id: ident) (ty: type) (rhs: expr) := match access_mode ty with - | By_value chunk => Some (Sassign id rhs) - | _ => None + | By_value chunk => OK (Sassign id rhs) + | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil) end. (** ** Translation of operators *) -Definition transl_unop (op: unary_operation) (a: expr) (ta: type) : option expr := +Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr := match op with - | Csyntax.Onotbool => Some(make_notbool a ta) - | Csyntax.Onotint => Some(make_notint a ta) + | Csyntax.Onotbool => OK(make_notbool a ta) + | Csyntax.Onotint => OK(make_notint a ta) | Csyntax.Oneg => make_neg a ta end. -Definition transl_binop (op: binary_operation) (a: expr) (ta: type) - (b: expr) (tb: type) : option expr := +Definition transl_binop (op: Csyntax.binary_operation) + (a: expr) (ta: type) + (b: expr) (tb: type) : res expr := match op with | Csyntax.Oadd => make_add a ta b tb | Csyntax.Osub => make_sub a ta b tb @@ -315,12 +306,12 @@ Definition transl_binop (op: binary_operation) (a: expr) (ta: type) a || b ---> a ? 1 : (b ? 1 : 0) *) -Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := +Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr := match a with | Expr (Csyntax.Econst_int n) _ => - Some(make_intconst n) + OK(make_intconst n) | Expr (Csyntax.Econst_float n) _ => - Some(make_floatconst n) + OK(make_floatconst n) | Expr (Csyntax.Evar id) ty => var_get id ty | Expr (Csyntax.Ederef b) _ => @@ -337,7 +328,7 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := transl_binop op tb (typeof b) tc (typeof c) | Expr (Csyntax.Ecast ty b) _ => do tb <- transl_expr b; - Some (make_cast (typeof b) ty tb) + OK (make_cast (typeof b) ty tb) | Expr (Csyntax.Eindex b c) ty => do tb <- transl_expr b; do tc <- transl_expr c; @@ -348,31 +339,33 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := | fun_case_f args res => do tb <- transl_expr b; do tcl <- transl_exprlist cl; - Some(Ecall (signature_of_type args res) tb tcl) - | _ => None + OK(Ecall (signature_of_type args res) tb tcl) + | _ => + Error(msg "Cshmgen.transl_expr(call)") end | Expr (Csyntax.Eandbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; - Some(make_andbool tb (typeof b) tc (typeof c)) + OK(make_andbool tb (typeof b) tc (typeof c)) | Expr (Csyntax.Eorbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; - Some(make_orbool tb (typeof b) tc (typeof c)) + OK(make_orbool tb (typeof b) tc (typeof c)) | Expr (Csyntax.Esizeof ty) _ => - Some(make_intconst (Int.repr (Csyntax.sizeof ty))) + OK(make_intconst (Int.repr (Csyntax.sizeof ty))) | Expr (Csyntax.Efield b i) ty => match typeof b with | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; make_load - (make_binop Oadd tb (make_intconst (Int.repr ofs))) + (Ebinop Oadd tb (make_intconst (Int.repr ofs))) ty | Tunion _ fld => do tb <- transl_lvalue b; make_load tb ty - | _ => None + | _ => + Error(msg "Cshmgen.transl_expr(field)") end end @@ -381,10 +374,10 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := where the value of [a] is stored. *) -with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := +with transl_lvalue (a: Csyntax.expr) {struct a} : res expr := match a with | Expr (Csyntax.Evar id) _ => - Some (Eaddrof id) + OK (Eaddrof id) | Expr (Csyntax.Ederef b) _ => transl_expr b | Expr (Csyntax.Eindex b c) _ => @@ -396,25 +389,27 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; - Some (make_binop Oadd tb (make_intconst (Int.repr ofs))) + OK (Ebinop Oadd tb (make_intconst (Int.repr ofs))) | Tunion _ fld => transl_lvalue b - | _ => None + | _ => + Error(msg "Cshmgen.transl_lvalue(field)") end - | _ => None + | _ => + Error(msg "Cshmgen.transl_lvalue") end (* [transl_exprlist al] returns a list of Csharpminor expressions that compute the values of the list [al] of Csyntax expressions. Used for function applications. *) -with transl_exprlist (al: Csyntax.exprlist): option exprlist := +with transl_exprlist (al: Csyntax.exprlist): res exprlist := match al with - | Csyntax.Enil => Some Enil + | Csyntax.Enil => OK Enil | Csyntax.Econs a1 a2 => do ta1 <- transl_expr a1; do ta2 <- transl_exprlist a2; - Some (Econs ta1 ta2) + OK (Econs ta1 ta2) end. (** ** Translation of statements *) @@ -431,9 +426,9 @@ Definition is_variable (e: Csyntax.expr) : option ident := value of the CabsCoq expression [e] and performs an [exit 0] if [e] evaluates to false. *) -Definition exit_if_false (e: Csyntax.expr) : option stmt := +Definition exit_if_false (e: Csyntax.expr) : res stmt := do te <- transl_expr e; - Some(Sifthenelse + OK(Sifthenelse (make_boolean te (typeof e)) Sskip (Sexit 0%nat)). @@ -497,13 +492,13 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int | LScase ni _ rem => (ni, k) :: switch_table rem (k+1) end. -Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : option stmt := +Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt := match s with | Csyntax.Sskip => - Some Sskip + OK Sskip | Csyntax.Sexpr e => do te <- transl_expr e; - Some (Sexpr te) + OK (Sexpr te) | Csyntax.Sassign b c => match (is_variable b) with | Some id => @@ -517,35 +512,35 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o | Csyntax.Ssequence s1 s2 => do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; - Some (Sseq ts1 ts2) + OK (Sseq ts1 ts2) | Csyntax.Sifthenelse e s1 s2 => do te <- transl_expr e; do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; - Some (Sifthenelse (make_boolean te (typeof e)) ts1 ts2) + OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2) | Csyntax.Swhile e s1 => do te <- exit_if_false e; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sblock (Sloop (Sseq te (Sblock ts1)))) + OK (Sblock (Sloop (Sseq te (Sblock ts1)))) | Csyntax.Sdowhile e s1 => do te <- exit_if_false e; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sblock (Sloop (Sseq (Sblock ts1) te))) + OK (Sblock (Sloop (Sseq (Sblock ts1) te))) | Csyntax.Sfor e1 e2 e3 s1 => do te1 <- transl_statement nbrk ncnt e1; do te2 <- exit_if_false e2; do te3 <- transl_statement nbrk ncnt e3; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) | Csyntax.Sbreak => - Some (Sexit nbrk) + OK (Sexit nbrk) | Csyntax.Scontinue => - Some (Sexit ncnt) + OK (Sexit ncnt) | Csyntax.Sreturn (Some e) => do te <- transl_expr e; - Some (Sreturn (Some te)) + OK (Sreturn (Some te)) | Csyntax.Sreturn None => - Some (Sreturn None) + OK (Sreturn None) | Csyntax.Sswitch e sl => let cases := switch_table sl 0 in let ncases := List.length cases in @@ -554,11 +549,11 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o end with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) - {struct sl}: option stmt := + {struct sl}: res stmt := match sl with | LSdefault s => do ts <- transl_statement nbrk ncnt s; - Some (Sblock (Sseq body ts)) + OK (Sblock (Sseq body ts)) | LScase _ s rem => do ts <- transl_statement nbrk ncnt s; transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts)) @@ -566,28 +561,31 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) (*** Translation of functions *) +Definition prefix_var_name (id: ident) : errmsg := + MSG "In local variable " :: CTX id :: MSG ":\n" :: nil. + Definition transl_params (l: list (ident * type)) := - AST.map_partial chunk_of_type l. + AST.map_partial prefix_var_name chunk_of_type l. Definition transl_vars (l: list (ident * type)) := - AST.map_partial var_kind_of_type l. + AST.map_partial prefix_var_name var_kind_of_type l. -Definition transl_function (f: Csyntax.function) : option function := +Definition transl_function (f: Csyntax.function) : res function := do tparams <- transl_params (Csyntax.fn_params f); do tvars <- transl_vars (Csyntax.fn_vars f); do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f); - Some (mkfunction (signature_of_function f) tparams tvars tbody). + OK (mkfunction (signature_of_function f) tparams tvars tbody). -Definition transl_fundef (f: Csyntax.fundef) : option fundef := +Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with | Csyntax.Internal g => - do tg <- transl_function g; Some(AST.Internal tg) + do tg <- transl_function g; OK(AST.Internal tg) | Csyntax.External id args res => - Some(AST.External (external_function id args res)) + OK(AST.External (external_function id args res)) end. (** ** Translation of programs *) Definition transl_globvar (ty: type) := var_kind_of_type ty. -Definition transl_program (p: Csyntax.program) : option program := +Definition transl_program (p: Csyntax.program) : res program := transform_partial_program2 transl_fundef transl_globvar p. -- cgit v1.2.3