search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Unification bug with functions in table #56

Closed jldodds closed 9 years ago

jldodds commented 9 years ago

Unification seems to fail when an applied function is put in the table. Perhaps because the unifier can't find the types of the arguments?

Definition REFLEXIVITY : rtac typ (expr typ func) :=
fun tus tvs n m c s e => 
match e with 
| (App (App (Inj (inr (Other (feq ty)))) l) r) =>
  match @exprUnify (ctx_subst c) typ func _ _ _ _ _ 3
                                 tus tvs 0 s l r ty with
    | Some s => RTac.Core.Solved s 
    | None =>  RTac.Core.Fail
  end
| _ => RTac.Core.Fail
end.

Parameter f : nat -> nat.

Goal f = f.
reify_expr_tac.
(* App(App (Inj (inr (Other (feq (tyArr tynat tynat))))) (Ext 1%positive))
         (Ext 1%positive) *)
Eval vm_compute in run_tac (THEN INTROS REFLEXIVITY) e.
(*     = Solved (TopSubst (expr typ func) [] []) *)
Abort.

Goal forall n, f n = f n.
reify_expr_tac.
(*App (ILogicFunc.fForall tynat typrop)
         (Abs tynat
            (App
               (App (Inj (inr (Other (feq tynat))))
                  (App (Ext 1%positive) (ExprCore.Var 0%nat)))
               (App (Ext 1%positive) (ExprCore.Var 0%nat)))) *)
Eval vm_compute in run_tac (THEN INTROS REFLEXIVITY) e.
(*    = Fail *)
Abort.
gmalecha commented 9 years ago

exprUnify unifies typed terms, so the symbol instantiation needs to know the type of Ext 1 in this case. I assume that this has not been set up. If it has, please re-open.