Skip to content

Commit

Permalink
prop&exp var binding
Browse files Browse the repository at this point in the history
  • Loading branch information
ZhiyaoZhong committed Sep 20, 2024
1 parent 8c6f7d9 commit 70abfdc
Show file tree
Hide file tree
Showing 10 changed files with 455 additions and 306 deletions.
2 changes: 2 additions & 0 deletions src/haz3lcore/derivation/DrvElab.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ and elab_prop: Drv.Prop.t => t =
|> List.concat
|> List.fold_left(cons_ctx, []),
)
| Abbr(_) => Hole(Drv.Prop.show(prop))
| Parens(p) => IdTagged.term_of(elab_prop(p))
};
{...prop, term};
Expand Down Expand Up @@ -146,6 +147,7 @@ and elab_exp: Drv.Exp.t => t =
};
| Roll => hole
| Unroll => hole
| Abbr(_) => hole
| Parens(e) => IdTagged.term_of(elab_exp(e))
};
{...exp, term};
Expand Down
19 changes: 15 additions & 4 deletions src/haz3lcore/derivation/DrvInfo.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,12 +24,23 @@ type jdmt = {
status: status_common,
};

[@deriving (show({with_path: false}), sexp, yojson)]
type error_prop =
| BadToken(Token.t)
| MultiHole
| NotAllowTuple;

[@deriving (show({with_path: false}), sexp, yojson)]
type status_prop =
| NotInHole(ok_common)
| InHole(error_prop);

[@deriving (show({with_path: false}), sexp, yojson)]
type prop = {
term: Drv.Prop.t,
cls: Cls.t,
ancestors,
status: status_common,
status: status_prop,
};

[@deriving (show({with_path: false}), sexp, yojson)]
Expand Down Expand Up @@ -109,7 +120,7 @@ type t =
[@deriving (show({with_path: false}), sexp, yojson)]
type error =
| Jdmt(error_common)
| Prop(error_common)
| Prop(error_prop)
| Exp(error_exp)
| Pat(error_pat)
| Typ(error_common)
Expand Down Expand Up @@ -160,7 +171,7 @@ let error_of: t => option(error) =
[@deriving (show({with_path: false}), sexp, yojson)]
type status_drv =
| Jdmt(status_common)
| Prop(status_common)
| Prop(status_prop)
| Exp(status_exp)
| Pat(status_pat)
| Typ(status_common)
Expand All @@ -173,7 +184,7 @@ let status_jdmt = (jdmt: Drv.Jdmt.t): status_common =>
| _ => NotInHole()
};

let status_prop = (prop: Drv.Prop.t): status_common =>
let status_prop = (prop: Drv.Prop.t): status_prop =>
switch (prop.term) {
| Hole(Invalid(token)) => InHole(BadToken(token))
| Hole(MultiHole(_)) => InHole(MultiHole)
Expand Down
4 changes: 4 additions & 0 deletions src/haz3lcore/derivation/DrvTerm.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ module Prop = {
| Truth
| Falsity
| Tuple
| Abbr
| Parens;

include TermBase.Prop;
Expand Down Expand Up @@ -75,6 +76,7 @@ module Prop = {
| Truth => Truth
| Falsity => Falsity
| Tuple(_) => Tuple
| Abbr(_) => Abbr
| Parens(_) => Parens;
};

Expand Down Expand Up @@ -107,6 +109,7 @@ module ALFA_Exp = {
| Case
| Roll
| Unroll
| Abbr
| Parens;

include TermBase.ALFA_Exp;
Expand Down Expand Up @@ -153,6 +156,7 @@ module ALFA_Exp = {
| Case(_) => Case
| Roll => Roll
| Unroll => Unroll
| Abbr(_) => Abbr
| Parens(_) => Parens;
};

Expand Down
252 changes: 217 additions & 35 deletions src/haz3lcore/dynamics/Transition.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,215 @@ module Transition = (EV: EV_MODE) => {
if anything about the current node changes, if only its
children change, we use rewrap */

// let req_drv_value =
// (req, state, env, drv: Drv.t, rewrap: Drv.t => t): EV.result => {
// let req_jdmt_value =
// (jdmt: Drv.Jdmt.t, rewrap: Drv.Jdmt.t => t): EV.result => {
// // let. _ = otherwise(env, jdmt |> rewrap);
// // Constructor;
// // let wrap_ctx = (term): EvalCtx.t => Term({term, ids: [rep_id(jdmt)]});
// let (term, rewrap_: Drv.Jdmt.term => Drv.Jdmt.t) =
// IdTagged.unwrap(jdmt);
// let rewrap = term => term |> rewrap_ |> rewrap;
// switch (term) {
// | Hole(s) =>
// let. _ = otherwise(env, Hole(s) |> rewrap);
// Constructor;
// | Val(e) =>
// let. _ = otherwise(env, Fun.id)
// and. e' =
// req_value(
// req(state, env),
// Fun.id,
// (Derivation(Exp(e)): term) |> IdTagged.fresh,
// );
// let e' =
// switch (IdTagged.term_of(e')) {
// | Derivation(Exp(e')) => e'
// | _ => raise(EvaluatorError.Exception(InvalidBoxedIntLit(e')))
// };
// Step({
// expr: Val(e') |> rewrap,
// state_update,
// kind: InvalidStep,
// is_value: true,
// });
// | Eval(e1, e2) =>
// let. _ = otherwise(env, Eval(e1, e2) |> rewrap);
// Constructor;
// | Entail(p1, p2) =>
// let. _ = otherwise(env, Entail(p1, p2) |> rewrap);
// Constructor;
// };
// }
// and req_prop_value = (prop: Drv.Prop.t, rewrap): EV.result => {
// let (term, rewrap_) = IdTagged.unwrap(prop);
// let rewrap = term => term |> rewrap_ |> rewrap;
// switch (term) {
// | Hole(s) =>
// let. _ = otherwise(env, Hole(s) |> rewrap);
// Constructor;
// | HasTy(e, t) =>
// let. _ = otherwise(env, (e, t) => HasTy(e, t) |> rewrap);
// and. e' =
// req_value(
// req(state, env),
// Fun.id,
// (Derivation(Exp(e)): term) |> IdTagged.fresh,
// )
// and. t' =
// req_value(
// req(state, env),
// Fun.id,
// (Derivation(Typ(t)): term) |> IdTagged.fresh,
// );
// let e' =
// switch (IdTagged.term_of(e')) {
// | Derivation(Exp(e')) => e'
// | _ => raise(EvaluatorError.Exception(InvalidBoxedIntLit(e')))
// };
// | _ =>
// let. _ = otherwise(env, prop |> rewrap);
// Constructor;
// };
// }
// and req_exp_value = (exp: Drv.Exp.t, rewrap): EV.result => {
// let. _ = otherwise(env, exp |> rewrap);
// Constructor;
// };
// switch (drv) {
// | Jdmt(jdmt) => req_jdmt_value(jdmt, jdmt => Jdmt(jdmt) |> rewrap)
// | Prop(prop) => req_prop_value(prop, prop => Prop(prop) |> rewrap)
// | Exp(exp) => req_exp_value(exp, exp => Exp(exp) |> rewrap)
// | Pat(_)
// | Typ(_)
// | TPat(_) =>
// let. _ = otherwise(env, drv |> rewrap);
// Constructor;
// };
// };

let replace_drv_abbrs = (env, d: t): t => {
let rec go_jdmt = jdmt => {
let (term, rewrap) = Drv.Jdmt.unwrap(jdmt);
let term: Drv.Jdmt.term =
switch (term) {
| Hole(s) => Hole(s)
| Val(e) => Val(go_exp(e))
| Eval(e1, e2) => Eval(e1, e2)
| Entail(p1, p2) => Entail(p1, p2)
};
term |> rewrap;
}
and go_prop = prop => {
let (term, rewrap) = Drv.Prop.unwrap(prop);
let term: Drv.Prop.term =
switch (term) {
| Hole(s) => Hole(s)
| HasTy(e, t) => HasTy(go_exp(e), t)
| Syn(e, t) => Syn(go_exp(e), t)
| Ana(e, t) => Ana(go_exp(e), t)
| Var(x) => Var(x)
| And(p1, p2) => And(go_prop(p1), go_prop(p2))
| Or(p1, p2) => Or(go_prop(p1), go_prop(p2))
| Impl(p1, p2) => Impl(go_prop(p1), go_prop(p2))
| Truth => Truth
| Falsity => Falsity
| Tuple(ps) => Tuple(List.map(go_prop, ps))
| Abbr(p) =>
let (let+) = (x, f) =>
switch (x) {
| Ok(x) => f(x)
| Error(s) => (Hole(Invalid(s)): Drv.Prop.term)
};
let+ p =
switch (IdTagged.term_of(p)) {
| Var(x) => Ok(x)
| _ => Error("Pat Not Var")
};
let+ d =
switch (ClosureEnvironment.lookup(env, p)) {
| Some(d) => Ok(d)
| None => Error("Pat Not Found")
};
let+ e =
switch (DHExp.term_of(d)) {
| Derivation(Prop(e)) => Ok(e)
| _ => Error("Pat Not Prop type")
};
e |> IdTagged.unwrap |> fst;
| Parens(p) => Parens(go_prop(p))
};
term |> rewrap;
}
and go_exp = exp => {
let (term, rewrap) = Drv.Exp.unwrap(exp);
let term: Drv.Exp.term =
switch (term) {
| Hole(s) => Hole(s)
| NumLit(n) => NumLit(n)
| Neg(e) => Neg(go_exp(e))
| Plus(e1, e2) => Plus(go_exp(e1), go_exp(e2))
| Minus(e1, e2) => Minus(go_exp(e1), go_exp(e2))
| Times(e1, e2) => Times(go_exp(e1), go_exp(e2))
| Gt(e1, e2) => Gt(go_exp(e1), go_exp(e2))
| Lt(e1, e2) => Lt(go_exp(e1), go_exp(e2))
| Eq(e1, e2) => Eq(go_exp(e1), go_exp(e2))
| True => True
| False => False
| If(e1, e2, e3) => If(go_exp(e1), go_exp(e2), go_exp(e3))
| Var(x) => Var(x)
| Let(x, e1, e2) => Let(x, go_exp(e1), go_exp(e2))
| Fix(x, e) => Fix(x, go_exp(e))
| Fun(x, e) => Fun(x, go_exp(e))
| Ap(e1, e2) => Ap(go_exp(e1), go_exp(e2))
| Pair(e1, e2) => Pair(go_exp(e1), go_exp(e2))
| Triv => Triv
| PrjL(e) => PrjL(go_exp(e))
| PrjR(e) => PrjR(go_exp(e))
| InjL => InjL
| InjR => InjR
| Case(e1, x, e2, y, e3) =>
Case(go_exp(e1), x, go_exp(e2), y, go_exp(e3))
| Roll => Roll
| Unroll => Unroll
| Abbr(p) =>
let (let+) = (x, f) =>
switch (x) {
| Ok(x) => f(x)
| Error(s) => (Hole(Invalid(s)): Drv.Exp.term)
};
let+ p =
switch (IdTagged.term_of(p)) {
| Var(x) => Ok(x)
| _ => Error("Pat Not Var")
};
let+ d =
switch (ClosureEnvironment.lookup(env, p)) {
| Some(d) => Ok(d)
| None => Error("Pat Not Found")
};
let+ e =
switch (DHExp.term_of(d)) {
| Derivation(Exp(e)) => Ok(e)
| _ => Error("Pat Not ALFA_Exp type")
};
e |> IdTagged.unwrap |> fst;
| Parens(e) => Parens(go_exp(e))
};
term |> rewrap;
};
let (term, rewrap) = IdTagged.unwrap(d);
let term: term =
switch (term) {
| Derivation(Jdmt(jdmt)) => Derivation(Jdmt(go_jdmt(jdmt)))
| Derivation(Prop(prop)) => Derivation(Prop(go_prop(prop)))
| Derivation(Exp(exp)) => Derivation(Exp(go_exp(exp)))
| _ => term
};
term |> rewrap;
};

let transition = (req, state, env, d): 'a => {
// Split DHExp into term and id information
let (term, rewrap) = DHExp.unwrap(d);
Expand Down Expand Up @@ -343,23 +552,6 @@ module Transition = (EV: EV_MODE) => {
d2,
);
switch (DHExp.term_of(d1')) {
// | Constructor(ctr, ty)
// when
// ctr
// |> BuiltinsDerivation.to_term
// |> Option.is_some
// && Typ.matched_arrow([], ty)
// |> snd
// |> Typ.term_of == Typ.Prop =>
// let term = ctr |> BuiltinsDerivation.to_term |> Option.get;
// let expr = BuiltinsDerivation.transit(term, Some(d2'));
// Step({
// expr,
// state_update,
// // TODO(zhiyao): add new kind
// kind: BuiltinAp(ctr),
// is_value: false // Not necessarily a value because of InvalidOperations
// });
| Constructor(_) => Constructor
| Fun(dp, d3, Some(env'), _) =>
let.match env'' = (env', matches(dp, d2'));
Expand Down Expand Up @@ -459,32 +651,22 @@ module Transition = (EV: EV_MODE) => {
| Deferral(_) =>
let. _ = otherwise(env, d);
Indet;
// | Constructor(ctr, ty)
// when
// ctr
// |> BuiltinsDerivation.to_term
// |> Option.is_some
// && ty
// |> Typ.term_of == Typ.Prop =>
// let. _ = otherwise(env, d);
// let term = ctr |> BuiltinsDerivation.to_term |> Option.get;
// let expr = BuiltinsDerivation.transit(term, None);
// Step({
// expr,
// state_update,
// // TODO(zhiyao): add new kind
// kind: BuiltinAp(ctr),
// is_value: false // Not necessarily a value because of InvalidOperations
// });
| Bool(_)
| Int(_)
| Float(_)
| String(_)
| Derivation(_)
| Constructor(_)
| BuiltinFun(_) =>
let. _ = otherwise(env, d);
Constructor;
| Derivation(_) =>
let. _ = otherwise(env, d);
Step({
expr: replace_drv_abbrs(env, d),
state_update,
kind: InvalidStep,
is_value: true,
});
| If(c, d1, d2) =>
let. _ = otherwise(env, c => If(c, d1, d2) |> rewrap)
and. c' =
Expand Down
Loading

0 comments on commit 70abfdc

Please sign in to comment.