diff options
author | Jade Philipoom <jadep@google.com> | 2018-04-27 12:19:29 +0200 |
---|---|---|
committer | jadephilipoom <jade.philipoom@gmail.com> | 2018-05-07 04:29:09 -0400 |
commit | 306b6f1900c49747b6e9c911ab395e43223ed77e (patch) | |
tree | 34563451dae5011cf17a4c6e53aaefa73d18b931 /src/Experiments | |
parent | a8b9398d3d24f1039c9b362cc26e158d414be023 (diff) |
move depth to a more sensible location
Diffstat (limited to 'src/Experiments')
-rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index d16d4a914..880128643 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -8995,17 +8995,7 @@ Module Straightline. end | None => None end. - - Fixpoint depth {t} (e : uexpr t) : nat := - match e with - | expr.Var _ _ => O - | expr.TT => O - | expr.AppIdent _ _ idc args => S (depth args) - | expr.App _ _ f x => S (Nat.max (depth f) (depth x)) - | expr.Pair _ _ x y => S (Nat.max (depth x) (depth y)) - | expr.Abs _ _ f => S (depth (f (dummy_var _))) - end. - + Definition mk_LetInAppIdent {s d t} (default : expr t) : range_type d -> ident.ident s d -> scalar s -> (var d -> expr t) -> expr t := match d as d0 return range_type d0 -> ident.ident s d0 -> scalar s -> (var d0 -> expr t) -> expr t with @@ -9072,11 +9062,21 @@ Module Straightline. End with_var. End expr. + Fixpoint depth {var t} (dummy_var : forall t, var t) (e : @Uncurried.expr.expr ident.ident var t) : nat := + match e with + | Uncurried.expr.Var _ _ => O + | Uncurried.expr.TT => O + | Uncurried.expr.AppIdent _ _ idc args => S (depth dummy_var args) + | Uncurried.expr.App _ _ f x => S (Nat.max (depth dummy_var f) (depth dummy_var x)) + | Uncurried.expr.Pair _ _ x y => S (Nat.max (depth dummy_var x) (depth dummy_var y)) + | Uncurried.expr.Abs _ _ f => S (depth dummy_var (f (dummy_var _))) + end. + (* TODO : Can I avoid having dummy_var appear here? *) Definition of_Expr {s d} (e : Expr (s->d)) (var : type -> Type) (x:var s) dummy_var : expr.expr d := match invert_Abs (e var) with - | Some f => expr.of_uncurried (dummy_var:=dummy_var) (expr.depth (dummy_var:=dummy_var) (f x)) (f x) + | Some f => expr.of_uncurried (dummy_var:=dummy_var) (depth dummy_var (f x)) (f x) | None => expr.dummy (dummy_var:=dummy_var) d end. |