search

rupesh4514 / grammatical-framework

Automatically exported from code.google.com/p/grammatical-framework
0 stars 0 forks source link

Instantiation of meta variables in the type checker #32

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
In some cases the instantiation of meta variables fails when the meta variable 
is moved to a nested scope. The following is a small example found by Lauri 
Alanko.

abstract Dep2 = {
 cat
   Nat;
   even Nat;
   odd Nat;
 fun
   S : Nat -> Nat;
   O : Nat;
   even_O : even O;
   odd_S : (n : Nat) -> even n -> odd (S n);
   even_S : (n : Nat) -> odd n -> even (S n);
}

concrete Dep2Cnc of Dep2 = {
 lincat
   Nat = Str;
   even = Str;
   odd = Str;
 lin
   S n = n;
   O = "";
   even_O = "";
   odd_S _ e = e;
   even_S _ e = e;
}

Dep2> p -cat="even O" ""
even_O

Dep2> p -cat="odd (S O)" ""
odd_S O even_O

Dep2> p -cat="even (S (S O))" ""
Prelude.(!!): index too large

Original issue reported on code.google.com by kr.ange...@gmail.com on 27 Aug 2010 at 3:38

GoogleCodeExporter commented 9 years ago

Original comment by kr.ange...@gmail.com on 27 Aug 2010 at 3:54