Hi folks
Much to my astonishment, the attached file actually elaborated. It's a
newer version of ye olde unification example, with a couple of
funny-pattern-matching twists. One is that I built a flexOrRigid case
analysis which analyses a term as either (var x) or t in such a way that
subsequently doing case t doesn't give you a var case ('cos you already
know it's rigid). The other is that the occur check is constructed as a
view.
The first time I wrote this program, back in 1999, I did some painting.
This time I just watched a pot. I guess that's progress.
Cheers
Conor
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( n : Nat ! ( i : Fin n !
data !-----------! where (------------------! ; !--------------------!
! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) )
------------------------------------------------------------------------------
( i : Fin (suc n) ; j : Fin n !
let !------------------------------!
! thin i j : Fin (suc n) )
thin i j <= rec i
{ thin i j <= case i
{ thin fz j => fs j
thin (fs i) j <= case j
{ thin (fs i) fz => fz
thin (fs i) (fs j) => fs (thin i j)
}
}
}
------------------------------------------------------------------------------
( i : Fin n ! ( i : Fin (suc n) !
data !-------------! where !-------------------!
! FinNE i : * ) ! finNE i : FinNE i )
------------------------------------------------------------------------------
( i : Fin n !
let !-----------------------!
! albert _n i : FinNE i )
albert _ n i <= case n
{ albert _ zero i <= case i
albert _ (suc n) i => finNE i
}
------------------------------------------------------------------------------
( i, j : ! ( i : Fin (suc! ; j : Fin n !
! Fin n ! ! !% n) !
data !-----------! where (-------------! ; !----------------------------!
! FinEq i j ! ! same : ! ! diff j : !
! : * ) ! FinEq i i ) ! FinEq i (thin i j) )
------------------------------------------------------------------------------
( i, j : Fin n !
let !-----------------------!
! finEq i j : FinEq i j )
finEq i j <= rec i
{ finEq i j <= case i
{ finEq fz j <= case j
{ finEq fz fz => same
finEq fz (fs j) => diff j
}
finEq (fs i) j <= case j
{ finEq (fs i) fz <= view (albert i)
{ finEq (fs i) fz => diff fz
}
finEq (fs i) (fs j) <= view (finEq i j)
{ finEq (fs i) (fs i) => same
finEq (fs i) (fs (thin i j)) => diff (fs j)
}
}
}
}
------------------------------------------------------------------------------
( n : Nat ! ( i : Fin n ! ( s, t : Tm n !
data !---------! where !-----------! ; (--------! ; !-------------!
! Tm n ! ! var i ! ! leaf : ! ! fork s t !
! : * ) ! : Tm n ) ! Tm n ) ! : Tm n )
------------------------------------------------------------------------------
( T : Nat -> * !
! !
! tm : all _m => T m -> Tm m ; tau : Fin m -> T n ; u : Tm m !
let !--------------------------------------------------------------!
! image T tm tau u : Tm n )
image T tm tau u <= rec u
{ image T tm tau u <= case u
{ image T tm tau (var i) => tm (tau i)
image T tm tau leaf => leaf
image T tm tau (fork s t)
=> fork (image T tm tau s) (image T tm tau t)
}
}
------------------------------------------------------------------------------
( rho : Fin m -> Fin n !
let !------------------------!
! ren rho : Tm m -> Tm n )
ren rho => image Fin var rho
------------------------------------------------------------------------------
( x : X !
let !----------!
! id x : X )
id x => x
------------------------------------------------------------------------------
( sig : Fin m -> Tm n !
let !------------------------!
! sub sig : Tm m -> Tm n )
sub sig => image Tm id sig
------------------------------------------------------------------------------
( X : * ! ( x : X ; xs : List X !
data !------------! where (--------------! ; !----------------------!
! List X : * ) ! nil : List X ) ! cons x xs : List X )
------------------------------------------------------------------------------
( n : Nat ! ( t : Tm n ! ( s : Tm n !
data !-----------! where !-----------------! ; !-----------------!
! DTm n : * ) ! forkL t : DTm n ) ! forkR s : DTm n )
------------------------------------------------------------------------------
( z : List (DTm n) ; u : Tm n !
let !------------------------------!
! plug z u : Tm n )
plug z u <= rec z
{ plug z u <= case z
{ plug nil u => u
plug (cons x xz) u <= case x
{ plug (cons (forkL t) xz) u => fork (plug xz u) t
plug (cons (forkR s) xz) u => fork s (plug xz u)
}
}
}
------------------------------------------------------------------------------
( t : Tm n !
let !-------------!
! Rigid t : * )
Rigid t <= case t
{ Rigid (var i) => zero = suc zero
Rigid leaf => One
Rigid (fork s t) => One
}
------------------------------------------------------------------------------
( t : Tm n !
! !
! P : Tm n -> * !
! !
! mf : all i : Fin n => P (var i) !
! !
! mr : all t : Tm n => Rigid t -> P t !
let !-------------------------------------!
! flexOrRigid t P mf mr : P t )
flexOrRigid t P mf mr <= case t
{ flexOrRigid (var i) P mf mr => mf i
flexOrRigid leaf P mf mr => mr leaf ()
flexOrRigid (fork s t) P mf mr => mr (fork s t) ()
}
------------------------------------------------------------------------------
( i : Fin n !
! !
! t : Tm n ! ( t : Tm n ! ( z : List (DTm n) !
data !-----------! where !----------------------! ; !---------------------!
! Occ i t ! ! thinned t : ! ! foundAt z : !
! : * ) ! Occ i ! ! Occ i (plug z ! !
! % (ren (thin i) t) ) ! !% (var i)) )
------------------------------------------------------------------------------
let (-------------------!
! occ j t : Occ j t )
occ j t <= rec t
{ occ j t <= case t
{ occ j (var i) <= view finEq j i
{ occ i (var i) => foundAt nil
occ i (var (thin i j)) => thinned (var j)
}
occ j leaf <= view albert j
{ occ i leaf => thinned leaf
}
occ j (fork s t) <= view occ j s
{ occ i (fork (image Fin (lam _x => var) (lam j => thin i j) t) t')
<= view occ i t'
{ occ i (fork (image Fin (lam _x => var) (lam j => thin i j) t')!
!% (image Fin (lam _x => var) (lam j => thin i j) t) )
=> thinned (fork t' t)
occ i (fork (image Fin (lam _x => var) (lam j => thin i j) z')!
!% (plug z (var i)) )
=> foundAt (cons (forkR (ren (thin i) z')) z)
}
occ i (fork (plug z (var i)) z') => foundAt (cons (forkL z') z)
}
}
}
------------------------------------------------------------------------------
( i : Fin (suc n) ; t : Tm n ; j : Fin (suc n) !
let !------------------------------------------------!
! ko i t j : Tm n )
ko i t j <= view finEq i j
{ ko i t i => t
ko i t (thin i j) => var j
}
------------------------------------------------------------------------------
( i : Fin (suc n) ; t : Tm n ; u : Tm (suc n) !
let !-----------------------------------------------!
! koTm i t u : Tm n )
koTm i t u => sub (ko i t) u
------------------------------------------------------------------------------
( i : Fin (suc n) !
! !
( m, n : Nat ! ! t : Tm n ; k : KO n m !
data !------------! where (--------------! ; !--------------------------!
! KO m n : * ) ! iKO : KO n n ) ! sKO i t k : KO (suc n) m )
------------------------------------------------------------------------------
( n : Nat ! ( k : KO n m !
data !------------! where (--------------! ; !-----------------!
! UAns n : * ) ! noU : UAns n ) ! yesU k : UAns n )
------------------------------------------------------------------------------
( i : Fin (suc n) ; t : Tm n ; a : UAns n !
let !-------------------------------------------!
! sAns i t a : UAns (suc n) )
sAns i t a <= case a
{ sAns i t noU => noU
sAns i t (yesU k) => yesU (sKO i t k)
}
------------------------------------------------------------------------------
( i : Fin n ; t : Tm n !
let !------------------------!
! flexUnify i t : UAns n )
flexUnify i t <= view occ i t
{ flexUnify i (image Fin (lam _x => var) (lam j => thin i j) t)
=> yesU (sKO i t iKO)
flexUnify i (plug z (var i)) <= case z
{ flexUnify i (var i) => yesU iKO
flexUnify i (plug (cons x xz) (var i)) => noU
}
}
------------------------------------------------------------------------------
( s, t : Tm n ; a : UAns n !
let !---------------------------!
! amgu _n s t a : UAns n )
amgu _ n s t a <= rec n
{ amgu _ n s t a <= rec s
{ amgu _ n s t a <= case a
{ amgu _ n s t noU => noU
amgu _ n s t (yesU k) <= flexOrRigid s
{ amgu _ n (var i) t (yesU k) <= case k
{ amgu _ m (var i) t (yesU iKO) => flexUnify i t
amgu _ (suc m) (var i') t' (yesU (sKO i t k))
=> sAns i t (amgu (ko i t i') (koTm i t t') (yesU k))
}
amgu _ n t t' (yesU k) <= flexOrRigid t'
{ amgu _ n t (var i) (yesU k) <= case k
{ amgu _ m t (var i) (yesU iKO) => flexUnify i t
amgu _ (suc m) t' (var i') (yesU (sKO i t k))
=> sAns i t (amgu (koTm i t t') (ko i t i') (yesU k))
}
amgu _ n t' t (yesU k) <= case t'
{ amgu _ n leaf t (yesU k) <= case t
{ amgu _ n leaf leaf (yesU k) => yesU k
amgu _ n leaf (fork s t) (yesU k) => noU
}
amgu _ n (fork s t) t' (yesU k) <= case t'
{ amgu _ n (fork s t) leaf (yesU k) => noU
amgu _ n (fork s' t') (fork s t) (yesU k)
=> amgu t' t (amgu s' s (yesU k))
}
}
}
}
}
}
}
------------------------------------------------------------------------------
