Commit 5db203c6 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Add a converter from Dedukti functions and predicates to function and predicate symbols

parent 55c42539
......@@ -77,6 +77,18 @@ def read_f : As : types -> C : type -> (terms As -> term C) -> read_f_T As C.
def fun_apply (f : function) := read_f (fun_arity f) (fun_codomain f) (apply_fun f).
def fun_arrs := read_f_T.
def fun_uncurry : As : types -> A : type -> fun_arrs As A -> terms As -> term A.
[A,f] fun_uncurry nil_type A f nil_term --> f
[A,As,B,f,a,as] fun_uncurry (cons_type A As) B f (cons_term _ a _ as) --> fun_uncurry As B (f a) as.
def make_fun : As : types -> A : type -> (fun_arrs As A) -> function.
[As] fun_arity (make_fun As _ _) --> As.
[A] fun_codomain (make_fun _ A _) --> A.
(; [As, A, f, as] apply_fun (make_fun As A f) as --> fun_uncurry As A f as. ;)
(; Formulae ;)
prop : Type.
......@@ -116,6 +128,15 @@ def read_p : As : types -> (terms As -> prop) -> read_p_T As.
def pred_apply (p : predicate) := read_p (pred_arity p) (apply_pred p).
def pred_arrs := read_p_T.
def pred_uncurry : As : types -> pred_arrs As -> terms As -> prop.
[p] pred_uncurry nil_type p nil_term --> p
[A,As,p,a,as] pred_uncurry (cons_type A As) p (cons_term _ a _ as) --> pred_uncurry As (p a) as.
def make_pred : As : types -> (pred_arrs As) -> predicate.
[As] pred_arity (make_pred As _) --> As.
(; [As, p, as] apply_pred (make_pred As p) as --> pred_uncurry As p as. ;)
(; The type of proofs of a formula is defined using an impredicative encoding ;)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment