1. Paweł Wieczorek
  2. extraction_of_untyped_evaluator

Commits

Paweł Wieczorek  committed 8f15ca8 Draft

init

  • Participants
  • Branches default

Comments (0)

Files changed (2)

File Eval.v

View file
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ * Syntax
+ *)
+
+
+Inductive Tm : Set :=
+| TmVar: nat -> Tm
+| TmApp: Tm -> Tm -> Tm
+| TmAbs: Tm -> Tm
+| Tm0  : Tm
+| TmS  : Tm
+.
+
+Inductive Tp : Set :=
+| TpN   : Tp
+| TpArr : Tp -> Tp -> Tp
+.
+
+(******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ * Domain
+ *)
+
+Inductive D : Set :=
+| DClo : Tm -> DEnv -> D
+| DNat : nat -> D
+| DS : D
+with DEnv : Set :=
+| DE : (nat -> D) -> DEnv
+.
+
+Definition Dlookup (denv:DEnv) i :=
+  let (f) := denv in f i
+.
+
+Definition Dext (denv:DEnv) d :=
+  DE (fun i =>
+    match i with
+      | 0 => d
+      | S k => let (f) := denv in f k
+    end
+  )
+.
+
+(******************************************************************************
+ * Graphs
+ *)
+
+Inductive EvalGraph: Tm -> DEnv -> D -> Prop :=
+| evgVar : forall i env,
+  EvalGraph (TmVar i) env (Dlookup env i)
+
+| evgAbs : forall t env,
+  EvalGraph (TmAbs t) env (DClo t env)
+
+| evg0 : forall env,
+  EvalGraph Tm0 env (DNat 0)
+
+| evgS : forall env,
+  EvalGraph TmS env DS
+
+| evgApp : forall tf df tx dx dr env,
+  EvalGraph tf env df ->
+  EvalGraph tx env dx ->
+  AppGraph df dx dr ->
+  EvalGraph (TmApp tf tx) env dr
+
+with AppGraph: D -> D -> D -> Prop :=
+| apgClo : forall tm denv dx dr,
+  EvalGraph tm (Dext denv dx) dr ->
+  AppGraph (DClo tm denv) dx dr
+
+| apgS : forall n,
+  AppGraph (DS) (DNat n) (DNat (S n))
+.
+Hint Constructors EvalGraph.
+Hint Constructors AppGraph.
+
+Scheme EvalGraph_mind := Induction for EvalGraph Sort Prop
+with   AppGraph_mind := Induction for AppGraph Sort Prop
+.
+
+Combined Scheme Graph_ind from EvalGraph_mind, AppGraph_mind.
+
+Fact Graph_deter: 
+  (forall tm env d1, 
+    EvalGraph tm env d1 -> forall d2,
+    EvalGraph tm env d2 ->
+    d1 = d2) /\
+  (forall df dx dy1,
+    AppGraph df dx dy1 -> forall dy2,
+    AppGraph df dx dy2 ->
+    dy1 = dy2)
+.
+Proof.
+apply Graph_ind.
+intros tm env d1 Hd1; inversion Hd1; subst; reflexivity.
+intros tm env d2 Hd2; inversion Hd2; subst; reflexivity.
+
+intros env d2 Hd2; inversion Hd2; subst; reflexivity.
+intros env d2 Hd2; inversion Hd2; subst; reflexivity.
+
+intros tf df tx dx dr env Hdf IHdf Hdx IHdx Hdr IHdr.
+intros d2 Hd2.
+inversion Hd2; subst.
+specialize (IHdf df0 H1); specialize (IHdx dx0 H2); subst.
+specialize (IHdr d2 H5). assumption.
+
+intros tm denv dx dr Hdr.
+intros IHd2 dy2 Hdy2.
+inversion Hdy2; subst.
+specialize (IHd2 dy2 H3); assumption.
+
+intros n dy2 H; inversion H; subst; reflexivity.
+Qed.
+
+
+Definition EvalGraph_deter := proj1 Graph_deter.
+Definition AppGraph_deter  := proj2 Graph_deter.
+
+Hint Resolve EvalGraph_deter.
+Hint Resolve AppGraph_deter.
+
+(******************************************************************************
+ * Dom's
+ *)
+
+
+Inductive EvalDom: Tm -> DEnv -> Prop :=
+| evgVarD : forall i env,
+  EvalDom (TmVar i) env
+
+| evgAbsD : forall t env,
+  EvalDom (TmAbs t) env
+
+| evgAppD : forall tf tx env,
+  EvalDom tf env ->
+  EvalDom tx env ->
+  (forall df dx, EvalGraph tf env df -> EvalGraph tx env dx -> AppDom df dx) ->
+  EvalDom (TmApp tf tx) env
+
+| evg0D : forall env,
+  EvalDom Tm0 env
+
+| evgSD : forall env,
+  EvalDom TmS env
+
+with AppDom: D -> D -> Prop :=
+| apgCloD : forall tm denv dx,
+  EvalDom tm (Dext denv dx) ->
+  AppDom (DClo tm denv) dx
+
+| appSD : forall n,
+  AppDom DS (DNat n)
+.
+
+Hint Constructors EvalDom.
+Hint Constructors AppDom.
+
+Scheme EvalDom_dind := Induction for EvalDom Sort Prop
+ with  AppDom_dind := Induction for AppDom Sort Prop
+.
+Print EvalDom_dind.
+
+
+Definition EvalDom_app_invF: forall tm tm0 tm1 denv,
+  EvalDom tm denv ->
+  tm = TmApp tm0 tm1 ->
+  EvalDom tm0 denv
+.
+intros tm tm0 tm1 denv Htm.
+case Htm.  
+intros A B H; discriminate H.
+intros A B H; discriminate H.
+intros tf tx env Htf Htx.
+intros HApp H; injection H.
+intros Hf Hx.
+rewrite <- Hx; assumption.
+intros A H; discriminate H.
+
+intros A H; discriminate H.
+Defined.
+Hint Resolve EvalDom_app_invF.
+
+Definition EvalDom_app_invX: forall tm tm0 tm1 denv,
+  EvalDom tm denv ->
+  tm = TmApp tm0 tm1 ->
+  EvalDom tm1 denv
+.
+intros tm tm0 tm1 denv Htm.
+case Htm.  
+intros A B H; discriminate H.
+intros A B H; discriminate H.
+intros tf tx env Htf Htx.
+intros HApp H; injection H.
+intros Hf Hx.
+rewrite <- Hf; assumption.
+intros A H; discriminate H.
+
+intros A H; discriminate H.
+Defined.
+Hint Resolve EvalDom_app_invX.
+
+Definition EvalDom_app_invA: forall tm tm0 tm1 denv,
+  EvalDom tm denv ->
+  tm = TmApp tm0 tm1 ->
+  forall df dx : D,  EvalGraph tm0 denv df -> EvalGraph tm1 denv dx -> AppDom df dx
+.
+intros tm tm0 tm1 denv Htm.
+case Htm.  
+intros A B H; discriminate H.
+intros A B H; discriminate H.
+intros tf tx env Htf Htx.
+intros HApp H; injection H.
+intros Hf Hx df dx.
+rewrite <- Hf.
+rewrite <- Hx.
+auto.
+
+intros A H; discriminate H.
+intros A H; discriminate H.
+Defined.
+Hint Resolve EvalDom_app_invA.
+
+Definition AppDom_clo_inv: forall df tm denv dx,
+  AppDom df dx ->
+  df = DClo tm denv ->
+  EvalDom tm (Dext denv dx)
+.
+intros df tm denv dx Hdf.
+case Hdf.
+intros tm0 denv0 dx0 Htm0.
+intros H; injection H.
+intros.
+rewrite <- H0. rewrite <- H1.
+assumption.
+intros A H; discriminate H.
+Defined.
+Hint Resolve AppDom_clo_inv.
+
+(******************************************************************************
+ * Evaluator
+ *)
+
+Require Import JMeq.
+Require Import Program.Tactics.
+
+Obligation Tactic := try solve [
+  program_simpl; eauto;
+  try match goal with
+    | [ H:AppDom _ _ |- _ ] =>
+      solve [ contradict H; intro H; inversion H ]
+    | [ H:EvalDom _ _ |- _ ] =>
+      solve [ contradict H; intro H; inversion H ]
+  end ]
+.
+
+Program Fixpoint eval (tm:Tm) (denv:DEnv) (H:EvalDom tm denv) {struct H}:
+  { d:D | EvalGraph tm denv d } :=
+  match tm as T
+    return (tm = T -> { d:D | EvalGraph T denv d })
+    with
+
+    | TmVar i => fun _  => Dlookup denv i 
+
+    | Tm0 => fun H' => DNat 0
+
+    | TmS => fun _ =>
+      DS
+
+    | TmAbs tm0 => fun  _ =>
+      DClo tm0 denv 
+
+    | TmApp tm0 tm1 => fun H'  =>
+      let (df,Hdf) := eval (EvalDom_app_invF H H') in
+      let (dx,Hdx) := eval (EvalDom_app_invX H H') in
+      let (dy,Hdy) := app  (EvalDom_app_invA H H' Hdf Hdx) in
+      dy
+
+  end (eq_refl tm) 
+
+with app (df dx:D) (H:AppDom df dx) {struct H} :
+  { d:D | AppGraph df dx d } :=
+  match df as DF
+    return df = DF -> { d:D | AppGraph DF dx d }
+    with
+
+    | DClo tm denv => fun H' =>
+      let (dy, Hdy) := eval (AppDom_clo_inv H H') in
+      let H         := apgClo Hdy in
+        exist (fun d => AppGraph (DClo tm denv) dx d)
+        dy H
+
+    | DS => fun H' =>
+      match dx as DX return dx = DX -> { d:D | AppGraph df DX d } with
+        | DNat n => fun H'' =>
+          (DNat (S n))
+
+        | DClo tm denv => fun H' =>
+          _
+
+        | DS => fun H' =>
+          _
+      end (eq_refl dx)
+
+    | DNat n => fun H' => 
+      _
+
+  end (eq_refl df) 
+.
+Obligations of eval.
+Obligations of app.
+Obligation 5 of app.
+program_simpl.
+set ( P :=
+(match dx as DX return (dx = DX -> {d : D | AppGraph DS DX d}) with
+         | DClo tm denv =>
+             fun H' : dx = DClo tm denv => app_obligation_2 H (eq_refl DS) H'
+         | DNat n =>
+             fun H'' : dx = DNat n =>
+             exist (fun d : D => AppGraph DS (DNat n) d) 
+               (DNat (S n)) (app_obligation_3 H (eq_refl DS) H'')
+         | DS => fun H' : dx = DS => app_obligation_4 H (eq_refl DS) H'
+         end (eq_refl dx))
+).
+destruct P; simpl; assumption.
+Qed.
+
+
+(******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ ******************************************************************************
+ * Extraction
+ *)
+
+
+Extraction Language Haskell.
+Set Extraction Optimize.
+Set Extraction AutoInline. 
+Extraction Inline proj1_sig.
+Extraction Inline False_rect.
+Extraction Inline False_rec.
+Extraction Inline eq_rect.
+Extraction Inline eq_rec.
+Extraction Inline eq_rec_r.
+Extraction Inline app_obligation_1.
+Extraction Inline app_obligation_2.
+Extraction Inline app_obligation_3.
+Extraction Inline app_obligation_4.
+Extraction Inline app_obligation_5.
+
+Extraction "test.hs" eval.
+

File test.hs

View file
+module Test where
+
+import qualified Prelude
+
+data Nat =
+   O
+ | S Nat
+
+type Sig a =
+  a
+  -- singleton inductive, whose constructor was exist
+  
+data Tm =
+   TmVar Nat
+ | TmApp Tm Tm
+ | TmAbs Tm
+ | Tm0
+ | TmS
+
+data D =
+   DClo Tm DEnv
+ | DNat Nat
+ | DS
+data DEnv =
+   DE (Nat -> D)
+
+dlookup :: DEnv -> Nat -> D
+dlookup denv i =
+  case denv of {
+   DE f -> f i}
+
+dext :: DEnv -> D -> DEnv
+dext denv d =
+  DE (\i ->
+    case i of {
+     O -> d;
+     S k ->
+      case denv of {
+       DE f -> f k}})
+
+eval :: Tm -> DEnv -> D
+eval tm denv =
+  case tm of {
+   TmVar i -> dlookup denv i;
+   TmApp tm0 tm1 -> app (eval tm0 denv) (eval tm1 denv);
+   TmAbs tm0 -> DClo tm0 denv;
+   Tm0 -> DNat O;
+   TmS -> DS}
+
+app :: D -> D -> D
+app df dx =
+  case df of {
+   DClo tm denv -> eval tm (dext denv dx);
+   DNat n -> Prelude.error "absurd case";
+   DS ->
+    case dx of {
+     DNat n -> DNat (S n);
+     _ -> Prelude.error "absurd case"}}
+