Skip to content

Commit

Permalink
normalize_binding needs to accumulate the bound variables in its recu…
Browse files Browse the repository at this point in the history 
…rsive case

This function has now been replaced by a much simpler and direct implementation
of the intuitive sense of renaming to avoid capture.

Fixes #23
  • Loading branch information
@chaudhuri
chaudhuri committed Nov 19, 2013
1 parent 978e477 commit 83070ce
Show file tree
Hide file tree
Showing 4 changed files with 77 additions and 85 deletions.
2 changes: 1 addition & 1 deletion examples/lambda-calculus/type-uniq/type-uniq-lg.thm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ induction on 2. intros. case H2.
apply H8 to _ with M1 = M, N1 = N.
apply ctx_member to H1 H5. case H4.
case H3.
apply H7 to _ with T = T3, R1 = R.
apply H7 to _ with T1 = T3, R1 = R.
apply H6 to _ with M1 = M, N1 = N.
apply ctx_member to H1 H9. case H8.
apply uniq to H1 H5 H9. search.
59 changes: 26 additions & 33 deletions src/metaterm.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -505,40 +505,33 @@ let rec normalize_obj obj =
| Async obj -> Async (aux obj)
| Sync obj -> Sync (norm_ctx obj)

let rec normalize_binders alist t =
let term_aux t = replace_term_vars ~tag:Constant alist t in
let rec aux t =
match t with
| True | False -> t
| Eq(a, b) -> Eq(term_aux a, term_aux b)
| Obj(obj, r) -> Obj(map_obj term_aux obj, r)
| Arrow(a, b) -> Arrow(aux a, aux b)
| Binding(binder, bindings, body) ->
let alist =
List.remove_all (fun (x, t) -> List.mem_assoc x bindings) alist
in
let alist_used = List.map term_to_pair (List.map snd alist) in
let body_used = get_metaterm_used body in
let nominal_used = get_metaterm_used_nominals body in
let used = alist_used @ body_used @ nominal_used in
let bindings', body' =
freshen_used_bindings bindings used body
in
binding binder bindings' (normalize_binders alist body')
| Or(a, b) -> Or(aux a, aux b)
| And(a, b) -> And(aux a, aux b)
| Pred(p, r) -> Pred(term_aux p, r)
in
aux t
let rename_term rens t = replace_term_vars ~tag:Constant rens t

and freshen_used_bindings bindings used body =
let bindings_alist = fresh_alist ~tag:Constant ~used bindings in
let bindings' =
List.map2 (fun (_, v) (_, ty) -> (term_to_name v, ty))
bindings_alist bindings
let normalize_binders t =
let eigens = get_metaterm_used t @ get_metaterm_used_nominals t in
let rec aux rens used t =
match t with
| True | False -> t
| Eq (a, b) -> Eq (rename_term rens a, rename_term rens b)
| Obj (obj, r) -> Obj (map_obj (rename_term rens) obj, r)
| Arrow (a, b) -> Arrow (aux rens used a, aux rens used b)
| Or (a, b) -> Or (aux rens used a, aux rens used b)
| And (a, b) -> And (aux rens used a, aux rens used b)
| Pred (p, r) -> Pred (rename_term rens p, r)
| Binding (binder, bvars, body) ->
let (rens, used, rev_bvars) = List.fold_left begin
fun (rens, used, bvars) (v, ty) ->
if List.mem_assoc v used then begin
let (fv, used) = fresh_wrt ~ts:0 Constant v ty used in
((v, fv) :: rens, used, (term_to_name fv, ty) :: bvars)
end else begin
(rens, used, (v, ty) :: bvars)
end
end (rens, used, []) bvars in
let bvars = List.rev rev_bvars in
binding binder bvars (aux rens used body)
in
let body' = normalize_binders bindings_alist body in
(bindings', body')
aux [] eigens t

let replace_term_typed_nominals alist t =
let rec aux t =
Expand Down Expand Up @@ -592,7 +585,7 @@ let normalize term =
term
|> map_on_objs normalize_obj
|> normalize_nominals
|> normalize_binders []
|> normalize_binders

let make_nabla_alist tids body =
let (id_names, id_tys) = List.split tids in
Expand Down
96 changes: 46 additions & 50 deletions src/tactics.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -356,65 +356,61 @@ let lift_all ~used ~sr nominals =
let new_term = var Eigen id v.ts rty in
bind term (app new_term rvars))



let case ~used ~sr ~clauses ~mutual ~defs ~global_support term =

let support = metaterm_support term in

let def_case ~wrapper term =
let make_case ~support ~used (head, body) term =
let fresh_used, head, body =
freshen_def ~sr ~support ~used head body
in
match try_left_unify_cpairs ~used:(fresh_used @ used) head term with
| Some cpairs ->
(* Names created perhaps by unificiation *)
let used_head = term_vars_alist Eigen [head; term] in
let used_body = metaterm_vars_alist Eigen body in
let used = List.unique (used_head @ used_body @ used) in
begin match recursive_metaterm_case ~used ~sr body with
| None -> []
| Some case ->
[{ bind_state = get_bind_state () ;
new_vars = case.stateless_new_vars @ used ;
new_hyps =
cpairs_to_eqs cpairs @
List.map wrapper case.stateless_new_hyps }]
end
match try_left_unify_cpairs ~used:(fresh_used @ used) head term with
| Some cpairs ->
let used_head = term_vars_alist Eigen [head; term] in
let used_body = metaterm_vars_alist Eigen body in
let used = List.unique (used_head @ used_body @ used) in
let body = Metaterm.normalize body in
begin match recursive_metaterm_case ~used ~sr body with
| None -> []
| Some case ->
[{ bind_state = get_bind_state () ;
new_vars = case.stateless_new_vars @ used ;
new_hyps =
cpairs_to_eqs cpairs @
List.map wrapper case.stateless_new_hyps }]
end
| None -> []
in
defs |> List.flatten_map
(unwind_state
(function
| Pred(head, _), body ->
make_case ~support ~used (head, body) term
| Binding(Nabla, tids, Pred(head, _)), body ->
List.range 0 (List.length tids) |> List.rev |> List.flatten_map
(fun n -> (* n is the number of nablas to be raised *)
List.choose n tids |> List.flatten_map
(unwind_state
(fun raised ->
let (rids, rtys) = List.split raised in
let nominals =
(* Want freshness with respect to global support *)
fresh_nominals rtys (pred (app head global_support))
in
let () = lift_all ~used ~sr nominals in
let head = replace_term_vars (List.combine rids nominals) head in
let (pids, ptys) = List.split (List.minus tids raised) in
List.permute (List.length pids) support
|> List.find_all
(fun permuted -> ptys = List.map (tc []) permuted)
|> List.flatten_map
(unwind_state
(fun permuted ->
let support = List.minus support permuted in
let head =
replace_term_vars (List.combine pids permuted) head
in
make_case ~support ~used (head, body) term)))))
| _ -> failwith "Bad head in definition"))
defs |> List.flatten_map
(unwind_state
(function
| Pred(head, _), body ->
make_case ~support ~used (head, body) term
| Binding(Nabla, tids, Pred(head, _)), body ->
List.range 0 (List.length tids) |> List.rev |> List.flatten_map
(fun n -> (* n is the number of nablas to be raised *)
List.choose n tids |> List.flatten_map
(unwind_state
(fun raised ->
let (rids, rtys) = List.split raised in
let nominals =
(* Want freshness with respect to global support *)
fresh_nominals rtys (pred (app head global_support))
in
let () = lift_all ~used ~sr nominals in
let head = replace_term_vars (List.combine rids nominals) head in
let (pids, ptys) = List.split (List.minus tids raised) in
List.permute (List.length pids) support
|> List.find_all
(fun permuted -> ptys = List.map (tc []) permuted)
|> List.flatten_map
(unwind_state
(fun permuted ->
let support = List.minus support permuted in
let head =
replace_term_vars (List.combine pids permuted) head
in
make_case ~support ~used (head, body) term)))))
| _ -> failwith "Bad head in definition"))
in

let focus sync_obj r =
Expand Down
5 changes: 4 additions & 1 deletion src/term.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -384,10 +384,13 @@ let term_to_string term =
(* let pp_var_ty x ty = (pp_var x) ^ ":" ^ (ty_to_string ty) in *)
let rec pp cx pr n term =
match observe (hnorm term) with
| Var v -> v.name
| Var v ->
(* "$(" ^ *)
v.name
(* ^ ":" ^ (tag2str v.tag) *)
(* ^ ":" ^ (string_of_int v.ts) *)
(* ^ ":" ^ (ty_to_string v.ty) *)
(* ^ ")" *)
| DB i ->
(try List.nth cx (i - 1) with _ -> pp_var (n - i + 1))
| App (t,ts) ->
Expand Down

0 comments on commit 83070ce

Please sign in to comment.