Skip to content

Commit

Permalink
user mode reducing annotations
Browse files Browse the repository at this point in the history
  • Loading branch information
Gaetan Gilbert committed Feb 13, 2016
1 parent 10e0d59 commit 11f760f
Show file tree
Hide file tree
Showing 8 changed files with 175 additions and 72 deletions.
2 changes: 1 addition & 1 deletion examples/nat.m31
View file
Expand Up @@ -16,7 +16,7 @@ constant nat_iota_S :
nat_rect P s0 s (S m) == s m (nat_rect P s0 s m)

constant ( + ) : nat -> nat -> nat
constant plus_def : forall n m : nat,
constant plus_def : forall (n m : nat),
n + m == nat_rect (lambda _, nat) n (lambda _ x, S x) m

do add_beta nat_iota_O
Expand Down
3 changes: 3 additions & 0 deletions std/base.m31
View file
Expand Up @@ -16,3 +16,6 @@ handle
end

let (|>) = fun x f => f x

operation failure 0

210 changes: 150 additions & 60 deletions std/equal.m31
View file
Expand Up @@ -21,10 +21,12 @@ operation getreducing 0
operation getstate 0

(* Used as
`set_reducing plus [true,true]`
`set_reducing fst [false,false,true]`
`set_reducing plus [eager,eager]`
`set_reducing fst [lazy,lazy,eager]`
*)
operation set_reducing 2
data eager 0
data lazy 0

(* One of the tasks we need to be able to do is this: given a universally quantified type
`∏(x1:A1)...(xn:An) B` and a type `C`, find an instantiation `x1↦e1, ..., xn↦en` such that
Expand Down Expand Up @@ -345,14 +347,27 @@ let rec eta_at etas a b t =
end
end

let compute_reducing reducing e =
match assoc_find e reducing with
| Some ?v => v
| None => []
end

let opt_transitivity meq eq' = match meq with
| Some ?eq => transitivity eq eq'
| None => eq'
end

(* Compute the weak head normal form of a term `e` using the `betas` hints.
Return `Some (⊢ p : e == e')` where `e'` is the normal form, or `None` if
`e` is already normal. *)
let rec do_whnf betas e =
Return `(eq,r)` where
`eq` is `Some (⊢ p : e == e')` where `e'` is the normal form,
or `None` if `e` is already normal.
`r` is information about how to reduce arguments when `e` is applied *)
let rec do_whnf betas reducing e =
match e with
| |- ?e1 ?e2 : ?t =>
match do_whnf betas e1 with
| Some (|- ?eq : _ == ?e1') =>
match do_whnf betas reducing e1 with
| (Some (|- ?eq : _ == ?e1'), ?rlst) =>
(*
At this point, [e2] has type [a] for some [a], and both [e1] and [e1'] have the same type [forall x : a, foo] such that [foo[e2/x] == t].
However if that equality is difficult to derive the following ascription may do something undesired or fail.
Expand All @@ -378,39 +393,64 @@ let rec do_whnf betas e =
| Some ?eq => eq : e == e'
end
in
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''), ?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None => Some eq
(Some eq, rlst)
| (None,?rlst) =>
(Some eq, rlst)
end
| None =>
| (None,?rlst) =>
match reduction e with
| Some (|- ?eq : _ == ?e') =>
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''), ?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None => Some eq
(Some eq, rlst)
| (None,?rlst) => (Some eq,rlst)
end
| None =>
(* `e1` is in whnf and `e1 e2` not a beta redex *)
(* Do we need to reduce `e2`? *)
let meq = match rlst with
| [] => None
| ?b::_ =>
match b with
| eager =>
match do_whnf betas reducing e2 with
| (Some (|- ?eq2 : _ == ?e2'),_) =>
let e' = e1 e2' in
let e' = e' : t in (* <- this should use eq2 *)
handle congruence e e' with
| equal e2 e2' => yield (Some eq2)
end
| (None,_) => None
end
| lazy =>
None
end
end in
let e' = match meq with Some (|- _ : _ == ?e') => e' | None => e end in
(* e1 is in whnf and e is not a beta redex, so we only need to see if a beta hint applies to e *)
match step_at betas e with
| Some (|- ?eq : _ == ?e') =>
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
let eq = transitivity eq eq' in
Some eq
| None =>
Some eq
match step_at betas e' with
| Some (|- ?eq' : _ == ?e'') =>
let eq = opt_transitivity meq eq' in
match do_whnf betas reducing e'' with
| (Some (|- ?eq'' : _ == _),?rlst) =>
let eq = transitivity eq eq'' in
(Some eq,rlst)
| (None,?rlst) =>
(Some eq, rlst)
end
| None => None
| None =>
let rlst = match rlst with [] => [] | _::?rlst => rlst end in
(meq,rlst)
end
end
end
| |- _proj ?e0 ?l : ?t =>
match do_whnf betas e0 with
| Some (|- ?eq : _ == ?e0') =>
| |- _proj ?e0 ?l : ?t => (* TODO reducing for projections? *)
match do_whnf betas reducing e0 with
| (Some (|- ?eq : _ == ?e0'),_) =>
let e' = _proj e0' l in
let e' = e' : t in
let meq = handle congruence e e' with
Expand All @@ -421,68 +461,87 @@ let rec do_whnf betas e =
| Some ?eq => eq : e == e'
end
in
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''),?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None => Some eq
(Some eq,rlst)
| (None,?rlst) => (Some eq,rlst)
end
| None =>
| (None,?rlst) =>
match reduction e with
| Some (|- ?eq : _ == ?e') =>
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''),?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None => Some eq
(Some eq,rlst)
| (None,?rlst) => (Some eq,rlst)
end
| None =>
(* e0 is in whnf and e is not a beta redex, so we only need to see if a beta hint applies to e *)
match step_at betas e with
| Some (|- ?eq : _ == ?e') =>
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''),?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None =>
Some eq
(Some eq, rlst)
| (None, ?rlst) =>
(Some eq, rlst)
end
| None => None
| None => (None, rlst)
end
end
end
| |- _ : ?t =>
match step_at betas e with
| Some (|- ?eq : _ == ?e') =>
match do_whnf betas e' with
| Some (|- ?eq' : _ == ?e'') =>
match do_whnf betas reducing e' with
| (Some (|- ?eq' : _ == ?e''),?rlst) =>
let eq = transitivity eq eq' in
Some eq
| None => Some eq
(Some eq,rlst)
| (None,?rlst) => (Some eq,rlst)
end
| None =>
None
let rlst = compute_reducing reducing e in
(None,rlst)
end
end

let reducing_spine reducing e =
let rec fold e = match e with
| |- ?e1 _ => match fold e1 with [] => [] | _::?l => l end
| _ => compute_reducing reducing e
end in
fold e


(* Like `do_whnf betas e` except that it always returns the witness of equality between
`e` and its normal form (so reflexivity if `e` is normal). *)
let whnf_eq = fun betas e =>
match do_whnf betas e with
| Some ?eq => eq
| None => refl e
let whnf_eq betas reducing e =
match do_whnf betas reducing e with
| (Some ?eq,_) => eq
| (None,_) => refl e
end

(* Structurally compare the whnf of `a` and `b`. Return `Some (⊢ p : a == b)` on
success, otherwise `None`. It will trigger general equality problems on subterms. *)
let rec equate_congr a b =
let betas = getbetas in
match (whnf_eq betas a, whnf_eq betas b) with
let betas = getbetas and reducing = getreducing in
match (whnf_eq betas reducing a, whnf_eq betas reducing b) with
((|- ?eqa : _ == ?a'), (|- ?eqb : _ == ?b')) =>
let r = match (a',b') with
| (|- ?a1 ?a2, |- ?b1 ?b2) =>
(* We need to compare the head structurally because of lambda extensionality *)
handle congruence a' b' with | equal a1 b1 => yield (equate_congr a1 b1) end
handle congruence a' b' with
| equal a1 b1 => yield (equate_congr a1 b1)
| equal (a2 as ?x) (b2 as ?y) =>
let red = match reducing_spine reducing a1 with [] => lazy | ?b :: _ => b end in
match red with
| eager =>
yield (equate_congr x y)
| lazy =>
yield (equal x y)
end
end
| (|- _proj ?a0 _, |- _proj ?b0 _) =>
handle congruence a' b' with | equal a0 b0 => yield (equate_congr a0 b0) end
| _ =>
Expand Down Expand Up @@ -519,7 +578,7 @@ end
let rec equate x y =
(* x and y must have the same derived type *)
let t = match (x, y) with ((|- _ : ?t), (|- _ : ?t)) => t end in
match (handle whnf_eq getbetas t with equal ?a ?b => yield (equate a b) end) with
match (handle whnf_eq getbetas getreducing t with equal ?a ?b => yield (equate a b) end) with
|- ?eqt : _ == ?t' =>
let x = convert x eqt and y = convert y eqt in
match hint_at gethints (x == y) with
Expand Down Expand Up @@ -599,27 +658,27 @@ let rec equality state = handler
yield r state

| whnf ?e => fun state =>
match (with equality state handle whnf_eq getbetas e) with
match (with equality state handle whnf_eq getbetas getreducing e) with
| (?eq, (?state)) =>
yield eq state
end

| as_prod ?e => fun state =>
match (with equality state handle whnf_eq getbetas e) with
match (with equality state handle whnf_eq getbetas getreducing e) with
| ((|- ?eq : _ == (forall (_), _)), (?state)) =>
yield (Some eq) state
| (_, _) => yield None state
end

| as_eq ?e => fun state =>
match (with equality state handle whnf_eq getbetas e) with
match (with equality state handle whnf_eq getbetas getreducing e) with
| ((|- ?eq : _ == (_ == _)), (?state)) =>
yield (Some eq) state
| (_, _) => yield None state
end

| as_signature ?e => fun state =>
match (with equality state handle whnf_eq getbetas e) with
match (with equality state handle whnf_eq getbetas getreducing e) with
| ((|- ?eq : _ == (_sig _)), (?state)) =>
yield (Some eq) state
| (_, _) => yield None state
Expand All @@ -640,6 +699,15 @@ let rec equality state = handler
let state = state_add_eta state h in
yield tt state

| set_reducing ?c ?l => fun state =>
let _ = match c with
| |- _constant _ => tt
| |- _atom _ => tt
| _ => print "only constants and atoms may have reducing information"; failure
end in
let state = state_add_reducing state (c,l) in
yield tt state

| getbetas => fun state =>
yield (state_betas state) state

Expand All @@ -649,6 +717,9 @@ let rec equality state = handler
| getetas => fun state =>
yield (state_etas state) state

| getreducing => fun state =>
yield (state_reducing state) state

| getstate => fun state => yield state state

| val ?v => fun state => (v, state)
Expand Down Expand Up @@ -700,6 +771,11 @@ let equality_in = fun state => handler
| (?v, ?state) => yield v state
end

| set_reducing ?c ?l => fun state =>
match (with equality state handle set_reducing c l) with
| (?v, ?state) => yield v state
end

| getbetas => fun state =>
match (with equality state handle getbetas) with
| (?v, ?state) => yield v state
Expand All @@ -715,6 +791,11 @@ let equality_in = fun state => handler
| (?v, ?state) => yield v state
end

| getreducing => fun state =>
match (with equality state handle getreducing) with
| (?v, ?state) => yield v state
end

| getstate => fun state => yield state state

| val ?v => fun state => v
Expand Down Expand Up @@ -773,6 +854,12 @@ handle
top_state := state
end

| set_reducing ?c ?l =>
match (with equality !top_state handle set_reducing c l) with
| (_,?state) =>
top_state := state
end

| getbetas =>
state_betas !top_state

Expand All @@ -782,6 +869,9 @@ handle
| getetas =>
state_etas !top_state

| getreducing =>
state_reducing !top_state

| getstate => !top_state
end

Expand Down

0 comments on commit 11f760f

Please sign in to comment.