Machine.v
Require Extraction.
Require Termes.
Require Conv.
Require Types.
Require Conv_Dec.
Require Infer.
Require Expr.
Record
state: Set := {
glob_ctx: env;
glob_names: prt_names;
glob_wf_ctx: (wf glob_ctx);
glob_length: (length ? glob_ctx)=(length ? glob_names);
glob_unique: (name_unique glob_names)
}.
Hint glob_wf_ctx glob_unique.
Definition
empty_state: state.
Realizer (Build_state (nil term) (nil name)).
Program_all.
Exact wf_nil.
(Red; Intros).
Inversion H.
Save.
Record
state_ext [x:name; t:term; s0,s1:state]: Prop := {
cons_env: (glob_ctx s1)=(cons ? t (glob_ctx s0));
cons_names: (glob_names s1)=(cons ? x (glob_names s0)) }.
(* internal level *)
Inductive
command: Set :=
INFER: term -> command
| CHECK: term -> term -> command
| AXIOM: name -> term -> command
| DELETE: command
| LIST: command
| QUIT: command.
Inductive
message: Set :=
New_axiom: name -> message
| Infered_type: term -> message
| Correct: message
| Delete_axiom: name -> message
| Context_listing: prt_names -> message
| Exiting: message.
Inductive
error: Set :=
Name_clash: name -> error
| Type_error: type_error -> error
| Cannot_delete: error.
(* external level *)
Inductive
ast: Set :=
AST_INFER: expr -> ast
| AST_CHECK: expr -> expr -> ast
| AST_AXIOM: name -> expr -> ast
| AST_DELETE: ast
| AST_LIST: ast
| AST_QUIT: ast.
Inductive
expr_of_ast: ast -> expr -> Prop :=
ea_inf: (e:expr)(expr_of_ast (AST_INFER e) e)
| ea_chk1: (e1,e2:expr)(expr_of_ast (AST_CHECK e1 e2) e1)
| ea_chk2: (e1,e2:expr)(expr_of_ast (AST_CHECK e1 e2) e2)
| ea_ax: (x:name)(e:expr)(expr_of_ast (AST_AXIOM x e) e).
Hint ea_inf ea_chk1 ea_chk2 ea_ax.
(* printable messages *)
Inductive
pmessage: Set :=
Pnew_axiom: name -> pmessage
| Pinfered_type: expr -> pmessage
| Pcorrect: pmessage
| Pcontext_listing: prt_names -> pmessage
| Pdelete_axiom: name -> pmessage
| Pexiting: pmessage.
(* printable type errors *)
Inductive
ptype_error: Set :=
Punder: name -> expr -> ptype_error -> ptype_error
| Pexpected_type: expr -> expr -> expr -> ptype_error
| Pkind_ill_typed: ptype_error
| Pdb_error: nat -> ptype_error
| Plambda_kind: expr -> ptype_error
| Pnot_a_type: expr -> expr -> ptype_error
| Pnot_a_fun: expr -> expr -> ptype_error
| Papply_err: expr -> expr -> expr -> expr -> ptype_error.
(* printable errors *)
Inductive
perror: Set :=
Punbound_vars: prt_names -> perror
| Pname_clash: name -> perror
| Ptype_error: ptype_error -> perror
| Pcannot_delete: perror.
(* command translated to the internal level *)
Inductive
synthesis_trans [s:state]: ast -> command -> Prop :=
Sy_infer: (e:expr)(t:term)
(term_expr_equiv (glob_names s) t e)
->(synthesis_trans s (AST_INFER e) (INFER t))
| Sy_check: (e1,e2:expr)(m,t:term)
(term_expr_equiv (glob_names s) m e1)
->(term_expr_equiv (glob_names s) t e2)
->(synthesis_trans s (AST_CHECK e1 e2) (CHECK m t))
| Sy_axiom: (x:name)(e:expr)(t:term)
(term_expr_equiv (glob_names s) t e)
->(synthesis_trans s (AST_AXIOM x e) (AXIOM x t))
| Sy_delete: (synthesis_trans s AST_DELETE DELETE)
| Sy_list: (synthesis_trans s AST_LIST LIST)
| Sy_quit: (synthesis_trans s AST_QUIT QUIT).
Hint Sy_infer Sy_check Sy_axiom Sy_delete Sy_list Sy_quit.
(* commands *)
Inductive
transition [s1:state]: command -> state -> message -> Prop :=
Tr_infer: (m,t:term)(typ (glob_ctx s1) m t)
->(transition s1 (INFER m) s1 (Infered_type t))
| Tr_check: (m,t:term)(typ (glob_ctx s1) m t)
->(transition s1 (CHECK m t) s1 Correct)
| Tr_axiom: (x:name)(t:term)(s2:state)
(glob_ctx s2) = (cons ? t (glob_ctx s1))
->(glob_names s2) = (cons ? x (glob_names s1))
->(transition s1 (AXIOM x t) s2 (New_axiom x))
| Tr_delete: (x:name)(s2:state)
(cons ? x (glob_names s2)) = (glob_names s1)
->(transition s1 DELETE s2 (Delete_axiom x))
| Tr_list: (transition s1 LIST s1 (Context_listing (glob_names s1)))
| Tr_quit: (transition s1 QUIT s1 Exiting).
Hint Tr_infer Tr_check Tr_axiom Tr_delete Tr_list Tr_quit.
(* translation of messages *)
Inductive
transl_msg [s:state]: message -> pmessage -> Prop :=
Tm_infer: (t:term)(e:expr)(term_expr_equiv (glob_names s) t e)
->(transl_msg s (Infered_type t) (Pinfered_type e))
| Tm_check: (transl_msg s Correct Pcorrect)
| Tm_axiom: (x:name)(transl_msg s (New_axiom x) (Pnew_axiom x))
| Tm_delete: (x:name)(transl_msg s (Delete_axiom x) (Pdelete_axiom x))
| Tm_listing: (l:prt_names)
(transl_msg s (Context_listing l) (Pcontext_listing l))
| Tm_exit: (transl_msg s Exiting Pexiting).
Hint Tm_infer Tm_check Tm_axiom Tm_delete Tm_listing Tm_exit.
(* ERRORS *)
(* errors occuring during synthesis *)
Inductive
synth_error [s:state]: ast -> perror -> Prop :=
Syf_db_failed: (a:ast)(e:expr)(undef:prt_names)
(expr_of_ast a e)
->(undef_vars e (glob_names s) undef)
-> ~undef=(nil ?)
->(synth_error s a (Punbound_vars undef)).
(* errors of internal commands *)
Inductive
com_error [s:state]: command -> error -> Prop :=
Ce_inf_error: (m:term)(err:type_error)
(inf_error m err)
->(expln (glob_ctx s) err)
->(com_error s (INFER m) (Type_error err))
| Ce_chk_error: (m,t:term)(err:type_error)
(chk_error m t err)
->(expln (glob_ctx s) err)
->(com_error s (CHECK m t) (Type_error err))
| Ce_decl_error: (x:name)(m:term)(err:type_error)
(decl_error m err)
->(expln (glob_ctx s) err)
->(com_error s (AXIOM x m) (Type_error err))
| Ce_axiom: (x:name)(t:term)(In ? x (glob_names s))
->(com_error s (AXIOM x t) (Name_clash x))
| Ce_delete: (glob_names s)=(nil name)
->(com_error s DELETE Cannot_delete).
Hint Ce_inf_error Ce_chk_error Ce_decl_error Ce_axiom Ce_delete.
(* translation of type_errors *)
Inductive
transl_type_error: prt_names->ptype_error->type_error->Prop :=
Tpe_under: (l:prt_names)(x:name)(t:term)(e:expr)
~(In name x l)
->(term_expr_equiv l t e)
->(perr:ptype_error)(err:type_error)
(transl_type_error (cons name x l) perr err)
->(transl_type_error l (Punder x e perr)
(Under t err))
| Tpe_exp_type: (l:prt_names)(t0,t1,t2:term)(e0,e1,e2:expr)
(term_expr_equiv l t0 e0)
->(term_expr_equiv l t1 e1)
->(term_expr_equiv l t2 e2)
->(transl_type_error l (Pexpected_type e0 e1 e2)
(Expected_type t0 t1 t2))
| Tpe_is_kind: (l:prt_names)
(transl_type_error l Pkind_ill_typed Kind_ill_typed)
| Tpe_db_error: (l:prt_names)(n:nat)
(transl_type_error l (Pdb_error n) (Db_error n))
| Tpe_lam_kind: (l:prt_names)(t:term)(e:expr)
(term_expr_equiv l t e)
->(transl_type_error l (Plambda_kind e)
(Lambda_kind t))
| Tpe_not_a_type: (l:prt_names)(t0,t1:term)(e0,e1:expr)
(term_expr_equiv l t0 e0)
->(term_expr_equiv l t1 e1)
->(transl_type_error l (Pnot_a_type e0 e1)
(Not_a_type t0 t1))
| Tpe_not_a_fun: (l:prt_names)(t0,t1:term)(e0,e1:expr)
(term_expr_equiv l t0 e0)
->(term_expr_equiv l t1 e1)
->(transl_type_error l (Pnot_a_fun e0 e1)
(Not_a_fun t0 t1))
| Tpe_apply_err: (l:prt_names)(t0,t1,t2,t3:term)(e0,e1,e2,e3:expr)
(term_expr_equiv l t0 e0)
->(term_expr_equiv l t1 e1)
->(term_expr_equiv l t2 e2)
->(term_expr_equiv l t3 e3)
->(transl_type_error l (Papply_err e0 e1 e2 e3)
(Apply_err t0 t1 t2 t3)).
Hint Tpe_exp_type Tpe_is_kind Tpe_db_error Tpe_lam_kind Tpe_not_a_type
Tpe_not_a_fun Tpe_apply_err.
(* translation of internal errors to the external level *)
Inductive
transl_err [s:state]: error -> perror -> Prop :=
Te_name_clash: (x:name)(transl_err s (Name_clash x) (Pname_clash x))
| Te_type_error: (e:type_error)(pe:ptype_error)
(transl_type_error (glob_names s) pe e)
->(transl_err s (Type_error e) (Ptype_error pe))
| Te_cannot_delete: (transl_err s Cannot_delete Pcannot_delete).
Hint Te_name_clash Te_type_error Te_cannot_delete.
(* global architecture *)
Lemma
trans_error_no_confusion:
(si,sf:state)(c:command)(m:message)(err:error)
(transition si c sf m)
->(com_error si c err)
->False.
(Induction 1; Intros).
Inversion_clear H1.
(Elim inf_error_no_type with m0 err0 (glob_ctx si) t; Auto).
Inversion_clear H1.
(Elim chk_error_no_type with (glob_ctx si) m0 t err0; Auto).
Inversion_clear H2.
(Elim decl_err_not_wf with (glob_ctx si) t err0; Auto).
Elim H0.
Apply glob_wf_ctx.
Generalize (glob_unique s2) .
(Unfold name_unique; Intros).
(Cut (Ex [n:nat](item ? x (glob_names si) n)); Intros).
Inversion_clear H4.
(Absurd O=(S x0); Intros).
Discriminate.
Apply H2 with x.
(Rewrite -> H1; Auto).
(Rewrite -> H1; Auto).
(Elim H3; Intros).
(Exists O; Auto).
Inversion_clear H5.
(Exists (S x0); Auto).
Inversion_clear H1.
Rewrite H2 in H0.
Discriminate H0.
Inversion_clear H0.
Inversion_clear H0.
Save.
Inductive
top_trans [si:state; a:ast; sf:state; m:pmessage]: Prop :=
Top_int: (c:command)(im:message)
(synthesis_trans si a c)
->(transition si c sf im)
(* the message should be understandable in initial state! *)
->(transl_msg si im m)
->(top_trans si a sf m).
Inductive
top_error [si:state; a:ast; e:perror]: Prop :=
Te_sy: (synth_error si a e)
->(top_error si a e)
| Te_int: (c:command)(ie:error)
(synthesis_trans si a c)
->(com_error si c ie)
->(transl_err si ie e)
->(top_error si a e).
Hint Te_sy.
Lemma
synth_no_confusion:
(si:state)(a:ast)(c:command)(e:perror)
(synthesis_trans si a c)
->(synth_error si a e)
->False.
(Induction 1; Intros).
Inversion_clear H1.
Apply H4.
(Apply equiv_no_undef with (glob_names si) t e0; Auto).
(Inversion_clear H2; Auto).
Inversion_clear H2.
Apply H5.
Generalize H0 H1 .
(Inversion_clear H3; Intros).
(Apply equiv_no_undef with (glob_names si) m e0; Auto).
(Apply equiv_no_undef with (glob_names si) t e0; Auto).
Inversion_clear H1.
Apply H4.
(Apply equiv_no_undef with (glob_names si) t e0; Auto).
(Inversion_clear H2; Auto).
Inversion_clear H0.
Inversion_clear H1.
Inversion_clear H0.
Inversion_clear H1.
Inversion_clear H0.
Inversion_clear H1.
Save.
Lemma
synth_deterministic: (si:state)(a:ast)(c,d:command)
(synthesis_trans si a c)
->(synthesis_trans si a d)
->c=d.
(Induction 1; Intros).
Inversion_clear H1.
(Elim equiv_unique with (glob_names si) t e t0; Auto).
Inversion_clear H2.
(Elim equiv_unique with (glob_names si) m e1 m0; Auto).
(Elim equiv_unique with (glob_names si) t e2 t0; Auto).
Inversion_clear H1.
(Elim equiv_unique with (glob_names si) t e t0; Auto).
(Inversion_clear H0; Auto).
(Inversion_clear H0; Auto).
(Inversion_clear H0; Auto).
Save.
Lemma
top_trans_error_no_confusion:
(si,sf:state)(a:ast)(m:pmessage)(perr:perror)
(top_trans si a sf m)
->(top_error si a perr)
->False.
(Induction 1; Intros).
Inversion_clear H3.
(Apply synth_no_confusion with si a c perr; Auto).
(Apply trans_error_no_confusion with si sf c im ie; Auto).
(Elim synth_deterministic with si a c0 c; Auto).
Save.
Definition
answer: state -> ast -> Set :=
[si,a] { p: state*pmessage |
Cases p of (sf,m) => (top_trans si a sf m) end }
+ { err: perror | (top_error si a err) }.
Definition
synth_answer: state -> ast -> Set := [si,a]
{ c: command | (synthesis_trans si a c) }
+ { err: perror | (synth_error si a err) }.
Theorem
synthesis: (si:state)(a:ast)(synth_answer si a).
(*
Realizer [si:state][a:ast]
Cases a of
(AST_INFER e) => Cases (term_of_expr e (glob_names si)) of
(inl t) => (inl ? perror (INFER t))
| (inr u) => (inr command ? (Punbound_vars u))
end
| (AST_CHECK e1 e2) => Cases (term_of_expr e1 (glob_names si))
(term_of_expr e2 (glob_names si)) of
(inl m) (inl t) => (inl ? perror (CHECK m t))
| (inr u1) _ => (inr command ? (Punbound_vars u1))
| _ (inr u2) => (inr command ? (Punbound_vars u2))
end
| (AST_AXIOM x e) => Cases (term_of_expr e (glob_names si)) of
(inl t) => (inl ? perror (AXIOM x t))
| (inr u) => (inr command ? (Punbound_vars u))
end
| AST_DELETE => (inl ? perror DELETE)
| AST_LIST => (inl ? perror LIST)
| AST_QUIT => (inl ? perror QUIT)
end.
*)
(Destruct a; Intros).
(Elim (term_of_expr e (glob_names si)); Intros).
Left.
Inversion_clear y.
(Exists (INFER x); Auto).
Right.
Inversion_clear y.
(Exists (Punbound_vars x); Auto).
(Apply Syf_db_failed with e; Auto).
(Elim (term_of_expr e (glob_names si)); Intros).
Inversion_clear y.
(Elim (term_of_expr e0 (glob_names si)); Intros).
Left.
Inversion_clear y.
(Exists (CHECK x x0); Auto).
Right.
Inversion_clear y.
(Exists (Punbound_vars x0); Auto).
(Apply Syf_db_failed with e0; Auto).
Right.
Inversion_clear y.
(Exists (Punbound_vars x); Auto).
(Apply Syf_db_failed with e; Auto).
(Elim (term_of_expr e (glob_names si)); Intros).
Left.
Inversion_clear y.
(Exists (AXIOM n x); Auto).
Right.
Inversion_clear y.
(Exists (Punbound_vars x); Auto).
(Apply Syf_db_failed with e; Auto).
Left.
(Exists DELETE; Auto).
Left.
(Exists LIST; Auto).
Left.
(Exists QUIT; Auto).
Save.
Definition
com_answer: state -> command -> Set :=
[si,c]{ p: state*message |
Cases p of (sf,m) => (transition si c sf m) end }
+ { e: error | (com_error si c e) }.
Lemma
exec_infer: (s:state)(m:term)(com_answer s (INFER m)).
(*
Realizer
[s:state][m:term]Cases (infer (glob_ctx s) m) of
(inl t) => (inl ? error (s,(Infered_type t)))
| (inr err) => (inr state*message ? (Type_error err))
end.
*)
Intros.
(Elim infer with (glob_ctx s) m; Intros; Auto).
Elim y.
Intros t H.
Left.
Exists (s,(Infered_type t)).
(Apply Tr_infer; Auto).
Right.
Inversion_clear y.
(Exists (Type_error x); Auto).
Save.
Lemma
exec_check: (s:state)(m,t:term)(com_answer s (CHECK m t)).
(*
Realizer
[s:state][m,t:term]Cases (check_typ (glob_ctx s) m t) of
(inleft err) => (inr state*message ? (Type_error err))
| inright => (inl ? error (s,Correct))
end.
*)
Intros.
(Elim check_typ with (glob_ctx s) m t; Intros; Auto).
Right.
Inversion_clear y.
(Exists (Type_error x); Auto).
Left.
(Exists (s,Correct); Auto).
Save.
Lemma
exec_axiom: (s:state)(x:name)(t:term)(com_answer s (AXIOM x t)).
(*
Realizer
[s:state][x:name][t:term]Cases (add_typ (glob_ctx s) t)
(list_index ? name_dec x (glob_names s)) of
left inright => (NewState
(Build_state (cons ? (Ax t) (glob_ctx s))
(cons ? x (glob_names s)))
(Pnew_axiom x))
| left (inleft _) => (Failed (Pname_clash x))
| right _ => (Failed (Ptype_error terr))
end.
*)
Intros.
(Elim (add_typ (glob_ctx s) t); Intros; Auto).
Right.
Inversion_clear y.
(Exists (Type_error x0); Auto).
(Elim (list_index ? name_dec x (glob_names s)); Intros).
Right.
(Exists (Name_clash x); Auto).
Inversion_clear y0.
Apply Ce_axiom.
(Elim H; Auto).
Left.
(Cut (name_unique (cons ? x (glob_names s))); Intros).
(Cut (length ? (cons ? t (glob_ctx s)))
=(length ? (cons ? x (glob_names s))); Intros).
(Exists ((Build_state (cons ? t (glob_ctx s))
(cons ? x (glob_names s)) y H0 H),(New_axiom x)); Auto).
Simpl.
(Elim glob_length with s; Auto).
(Apply fv_ext; Auto).
Save.
Lemma
exec_delete: (s:state)(com_answer s DELETE).
(*
Realizer [s:state]Cases (glob_ctx s) (glob_names s) of
(cons _ e) (cons x l) => (NewState (Build_state e l) (Delete_axiom x))
| _ _ => (Failed Pcannot_delete)
end.
*)
Intros.
Generalize (refl_equal ? (glob_names s)) .
Pattern 1 (glob_names s) .
(Case (glob_names s); Intros).
Right.
(Exists Cannot_delete; Auto).
Generalize (refl_equal ? (glob_ctx s)) .
Pattern 1 (glob_ctx s) .
(Case (glob_ctx s); Intros).
Generalize (glob_length s) .
Elim H.
(Elim H0; Simpl; Intros).
Discriminate H1.
(Cut (length ? l0)=(length ? l); Intros).
(Cut (name_unique l); Intros).
(Cut (wf l0); Intros).
Left.
(Exists ((Build_state l0 l H3 H1 H2),(Delete_axiom n)); Auto).
Generalize (glob_wf_ctx s) .
(Elim H0; Intros).
Inversion_clear H3.
(Apply typ_wf with t (Srt s0); Auto).
Generalize (glob_unique s) .
Elim H.
(Unfold name_unique; Intros).
(Cut (S m)=(S n0); Intros).
(Injection H5; Auto).
(Apply H2 with x; Auto).
Generalize (glob_length s) .
Elim H.
(Elim H0; Simpl; Intros).
(Injection H1; Auto).
Save.
Theorem
interp_command: (si:state)(c:command)(com_answer si c).
Realizer [si:state][c:command]
Cases c of
(INFER t) => (exec_infer si t)
| (CHECK m t) => (exec_check si m t)
| (AXIOM x t) => (exec_axiom si x t)
| DELETE => (exec_delete si)
| LIST => (inl ? error (si,(Context_listing (glob_names si))))
| QUIT => (inl ? error (si,Exiting))
end.
Program_all.
Left.
(Exists (si,(Context_listing (glob_names si))); Auto).
Left.
Exists (si,Exiting);Auto.
Save.
Lemma
transl_message: (s:state)(im:message)
(Ex [c:command](Ex [sf:state](transition s c sf im)))
->{ m: pmessage | (transl_msg s im m) }.
Realizer [s:state][im:message]
Cases im of
(New_axiom x) => (Pnew_axiom x)
| (Infered_type t) => (Pinfered_type (expr_of_term t (glob_names s)))
| Correct => Pcorrect
| (Delete_axiom x) => (Pdelete_axiom x)
| (Context_listing l) => (Pcontext_listing l)
| Exiting => Pexiting
end.
Program_all.
Inversion_clear H.
Inversion_clear H0.
Inversion_clear H.
Elim glob_length with x0.
(Apply type_free_db with m; Auto).
Save.
Lemma
transl_ty_error: (err:type_error)(s:state)
(expln (glob_ctx s) err)
->{ perr:ptype_error |
(transl_type_error (glob_names s) perr err) }.
(*
Realizer Fix tr_ty_err { tr_ty_err/1 : type_error -> state -> ptype_error :=
[s]Cases err of
(Under t e) => let (e:expr) = expr_of_term(Punder x )
| (Expected_type t at et) =>
| Kind_ill_typed => Pkind_ill_typed
| (Db_error n) =>
| (Lambda_kind t m) =>
| (Not_a_type m t) =>
| (Not_a_fun m t) =>
| (Apply_err u tu v tv) =>
end }.
*)
(Induction err; Intros).
(Elim find_free_var with (glob_names s); Intros).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(ElimType {si:state | (state_ext x t s si)}; Intros).
(Elim H with x1; Intros).
Exists (Punder x x0 x2).
(Apply Tpe_under; Auto).
(Elim cons_names with x t s x1; Auto).
Inversion_clear H0.
(Rewrite -> (cons_env x t s x1); Auto).
(Cut (wf (cons ? t (glob_ctx s))); Intros).
(Cut (S (length ? (glob_ctx s)))=(S (length ? (glob_names s))); Intros).
(Cut (name_unique (cons ? x (glob_names s))); Intros).
Exists (Build_state (cons ? t (glob_ctx s)) (cons ? x (glob_names s))
H1 H2 H3).
(Split; Auto).
(Apply fv_ext; Auto).
(Elim glob_length with s; Auto).
(Inversion_clear H0; Auto).
(Apply expln_wf with t0; Auto).
Inversion_clear H0.
(Elim glob_length with s; Auto).
(Cut (wf (cons ? t (glob_ctx s))); Intros).
Inversion_clear H0.
(Apply typ_free_db with (Srt s0); Auto).
(Apply expln_wf with t0; Auto).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(Elim expr_of_term with t0 (glob_names s); Intros; Auto).
(Elim expr_of_term with t1 (glob_names s); Intros; Auto).
(Exists (Pexpected_type x x0 x1); Auto).
Inversion_clear H.
Elim glob_length with s.
Auto.
Inversion_clear H.
Elim glob_length with s.
(Apply type_free_db with t; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply typ_free_db with t0; Auto).
(Exists Pkind_ill_typed; Auto).
(Exists (Pdb_error n); Auto).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(Exists (Plambda_kind x); Auto).
Inversion_clear H.
Elim glob_length with s.
Apply db_abs.
(Cut (wf (cons ? t0 (glob_ctx s))); Intros).
Inversion_clear H.
(Apply typ_free_db with (Srt s0); Auto).
(Apply typ_wf with m (Srt kind); Auto).
Change (free_db (length ? (cons ? t0 (glob_ctx s))) m).
(Apply typ_free_db with (Srt kind); Auto).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(Elim expr_of_term with t0 (glob_names s); Intros; Auto).
(Exists (Pnot_a_type x x0); Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply type_free_db with t; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply typ_free_db with t0; Auto).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(Elim expr_of_term with t0 (glob_names s); Intros; Auto).
(Exists (Pnot_a_fun x x0); Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply type_free_db with t; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply typ_free_db with t0; Auto).
(Elim expr_of_term with t (glob_names s); Intros; Auto).
(Elim expr_of_term with t0 (glob_names s); Intros; Auto).
(Elim expr_of_term with t1 (glob_names s); Intros; Auto).
(Elim expr_of_term with t2 (glob_names s); Intros; Auto).
(Exists (Papply_err x x0 x1 x2); Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply type_free_db with t1; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply typ_free_db with t2; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply type_free_db with t; Auto).
Inversion_clear H.
Elim glob_length with s.
(Apply typ_free_db with (Prod a b); Auto).
Save.
Lemma
transl_error: (s:state)(err:error)
((terr:type_error)err=(Type_error terr)
->(expln (glob_ctx s) terr))
->{ perr: perror | (transl_err s err perr) }.
Realizer [s:state][err:error]
Cases err of
(Name_clash x) => (Pname_clash x)
| (Type_error er) => (Ptype_error (transl_ty_error er s))
| Cannot_delete => Pcannot_delete
end.
Program_all.
Save.
Theorem
interp_ast: (si:state)(a:ast)(answer si a).
(*
Realizer [si:state][a:ast]
Cases (synthesis si a) of
(inl c) => Cases (interp_command si c) of
(inl (sf,im)) => (inl ? perror (sf, (transl_message si im)))
| (inr ie) => (inr state*pmessage ? (transl_error si ie))
end
| (inr err) => (inr state*pmessage ? err)
end.
*)
Intros.
(Elim synthesis with si a; Intros).
Elim y; Intros c H.
(Elim interp_command with si c; Intros).
Elim y0; Destruct x; Intros.
(Elim transl_message with si m; Intros).
Left.
(Exists (s,x0); Auto).
(Apply Top_int with c m; Auto).
(Exists c; Exists s; Auto).
Right.
Inversion_clear y0.
(Elim transl_error with si x; Intros).
Exists x0.
(Apply Te_int with c x; Auto).
Rewrite H1 in H0.
(Inversion_clear H0; Auto).
Right.
Inversion_clear y.
(Exists x; Auto).
Save.
27/03/97, 21:17