Remove the grammars directory. It was full of old grammars that don't compile these days. See the old source distributions if you want them.

8 files changed, 0 insertions, 491 deletions

diff --git a/grammars/logic/Arithm.gf b/grammars/logic/Arithm.gf
deleted file mode 100644
index 2a91c5ed0..000000000
--- a/grammars/logic/Arithm.gf
+++ /dev/null
@@ -1,66 +0,0 @@
-abstract Arithm = Logic ** {
-
--- arithmetic
-fun 
-  Nat, Real  : Dom ;
-data
-  zero : Elem Nat ;
-  succ : Elem Nat -> Elem Nat ;
-fun
-  trunc : Elem Real -> Elem Nat ;
-
-  EqNat : (m,n : Elem Nat) -> Prop ;
-  LtNat : (m,n : Elem Nat) -> Prop ;
-  Div   : (m,n : Elem Nat) -> Prop ;
-  Even  : Elem Nat -> Prop ;
-  Odd   : Elem Nat -> Prop ;
-  Prime : Elem Nat -> Prop ;
-
-  one  : Elem Nat ;
-  two  : Elem Nat ;
-  sum  : (m,n : Elem Nat) -> Elem Nat ;
-  prod : (m,n : Elem Nat) -> Elem Nat ;
-data
-  evax1 : Proof (Even zero) ;
-  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (succ n)) ;
-  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (succ n)) ;
-  eqax1 : Proof (EqNat zero zero) ;
-  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> Proof (EqNat (succ m) (succ n)) ;
-fun
-  IndNat : (C : Elem Nat -> Prop) -> 
-             Proof (C zero) -> 
-             ((x : Elem Nat) -> Proof (C x) -> Proof (C (succ x))) -> 
-                Proof (Univ Nat C) ;
-
-def 
-  one = succ zero ;
-  two = succ one ;
-  sum m (succ n) = succ (sum m n) ;
-  sum m zero = m ;
-  prod m (succ n) = sum (prod m n) m ;
-  prod m zero = zero ;
-  LtNat m n = Exist Nat (\x -> EqNat n (sum m (succ x))) ;
-  Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
-  Prime n = Conj 
-              (LtNat one n) 
-              (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
-
-  Abs = Abs ;
-
-fun ex1 : Text ;
-def ex1 = 
-  ThmWithProof 
-    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
-    (IndNat 
-       (\x -> Disj (Even x) (Odd x)) 
-       (DisjIl (Even zero) (Odd zero) evax1) 
-       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (succ x)) (Odd (succ x))) 
-         (Hypo (Disj (Even x) (Odd x)) h) 
-         (\a -> DisjIr (Even (succ x)) (Odd (succ x)) 
-            (evax2 x (Hypo (Even x) a))) 
-         (\b -> DisjIl (Even (succ x)) (Odd (succ x)) 
-            (evax3 x (Hypo (Odd x) b))
-         )
-       )
-     ) ;
-} ;
diff --git a/grammars/logic/ArithmEng.gf b/grammars/logic/ArithmEng.gf
deleted file mode 100644
index e09f14396..000000000
--- a/grammars/logic/ArithmEng.gf
+++ /dev/null
@@ -1,42 +0,0 @@
---# -path=.:../prelude
-
-concrete ArithmEng of Arithm = LogicEng ** open LogicResEng in {
-
-lin
-  Nat = {s = nomReg "number"} ;
-  zero = ss "zero" ;
-  succ = fun1 "successor" ;
-
-  EqNat = adj2 ["equal to"] ;
-  LtNat = adj2 ["smaller than"] ;
-  Div   = adj2 ["divisible by"] ;
-  Even  = adj1 "even" ;
-  Odd   = adj1 "odd" ;
-  Prime = adj1 "prime" ;
-
-  one = ss "one" ;
-  two = ss "two" ;
-  sum = fun2 "sum" ;
-  prod = fun2 "product" ;
-
-  evax1 = ss ["by the first axiom of evenness , zero is even"] ;
-  evax2 n c = {s = 
-    c.s ++ [". By the second axiom of evenness , the successor of"] ++ 
-    n.s ++ ["is odd"]} ;
-  evax3 n c = {s = 
-    c.s ++ [". By the third axiom of evenness , the successor of"] ++ 
-    n.s ++ ["is even"]} ;
-  eqax1 = ss ["by the first axiom of equality , zero is equal to zero"] ;
-  eqax2 m n c = {s = 
-    c.s ++ [". By the second axiom of equality , the successor of"] ++ m.s ++ 
-    ["is equal to the successor of"] ++ n.s} ;
-  IndNat C d e = {s = 
-    ["we proceed by induction . For the basis ,"] ++ d.s ++ 
-    [". For the induction step, consider a number"] ++ C.$0 ++ 
-    ["and assume"] ++ C.s ++ "(" ++ e.$1 ++ ")" ++ "." ++ e.s ++ 
-    ["Hence, for all numbers"] ++ C.$0 ++ "," ++ C.s} ;
-
-  ex1 = ss ["The first theorem and its proof ."] ;
-
-} ;
-
diff --git a/grammars/logic/ArithmFre.gf b/grammars/logic/ArithmFre.gf
deleted file mode 100644
index fcc99f4e9..000000000
--- a/grammars/logic/ArithmFre.gf
+++ /dev/null
@@ -1,37 +0,0 @@
---# -path=.:../prelude
-
-concrete ArithmFre of Arithm = LogicFre ** open ResFre in {
-
-lin Nat = {g = masc ; s = nomReg "nombre"} ;
-zero = {g = masc ; s = table {c => (prep ! c) ++ "zéro"}} ;
-succ n =
-  {g = masc ; s = table {c => defin ! sg ! masc ! c ++ "successeur" ++ n.s ! dd}} ;
-EqNat k n = mkPropA2 aa k (adjAl "éga") n ;
-LtNat k n = mkPropA2 aa k (adjReg "inférieur") n ;
-Div k n = mkPropA2 nom k (table {_ => nomReg "divisible"}) n ; --- par !
-
-Even n = mkPropA1 n (adjReg "pair") ;
-Odd n = mkPropA1 n (adjReg "impair") ;
-Prime n = mkPropA1 n (adjEr "premi") ;
-
-lin one  =
-  {g = masc ; s = table {c => (prep ! c) ++ "un"}} ;
-lin two  =
-  {g = masc ; s = table {c => (prep ! c) ++ "deux"}} ;
-lin sum m n = {g = fem ; s = table {
-  c => defin ! sg ! fem ! c ++ "somme" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
-lin prod m n = {g = masc ; s = table {
-  c => defin!sg!fem!c ++ "produit" ++ m.s ! dd ++ "et" ++ n.s ! dd}} ;
-lin evax1  =
-  {s = "par"++"le"++"premier"++"axiome"++"de"++"parité,"++"zéro"++"est"++"pair"} ;
-lin evax2 n c =
-  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"impair"} ;
-lin evax3 n c =
-  {s = c.s ++ "."++"Par"++"le"++"troisième"++"axiome"++"de"++"parité,"++"le"++"successeur" ++ (n.s ! dd) ++ "est"++"pair"} ;
-lin eqax1  =
-  {s = "par"++"le"++"premier"++"axiome"++"d'égalité,"++"zéro"++"est"++"égal"++"a"++"lui-même"} ;
-lin eqax2 m n c =
-  {s = c.s ++ "."++"Par"++"le"++"deuxième"++"axiome"++"d'égalité,"++"le"++"successeur" ++ (m.s ! dd) ++ "est"++"égal"++"au"++"successeur" ++ n.s ! dd} ;
-lin IndNat C d e =
-  {s = "nous"++"nous"++"servons"++"d'induction."++"Pour"++"la"++"base," ++ d.s ++ "."++"Pour"++"le"++"pas"++"d'induction,"++"considérons"++"un"++"nombre" ++ e.$0 ++ "et"++"supposons" ++ que ++ (C.s ! ind) ++ "(" ++ e.$1 ++ ")" ++ "." ++ e.s ++ "Donc,"++"pour"++"tous"++"les"++"nombres" ++ C.$0 ++ "," ++ C.s ! ind} ;
-}
diff --git a/grammars/logic/Logic.gf b/grammars/logic/Logic.gf
deleted file mode 100644
index dbd0566f2..000000000
--- a/grammars/logic/Logic.gf
+++ /dev/null
@@ -1,97 +0,0 @@
--- many-sorted predicate calculus
--- AR 1999, revised 2001
-
-abstract Logic = {
-
-flags startcat=Prop ; -- this is what you want to parse
-
-cat 
-  Prop ;       -- proposition
-  Dom ;        -- domain of quantification
-  Elem Dom ;   -- individual element of a domain
-  Proof Prop ; -- proof of a proposition
-  Text ;       -- theorem with proof etc. 
-
-fun 
-  -- texts
-  Statement : Prop -> Text ;
-  ThmWithProof : (A : Prop) -> Proof A -> Text ;
-  ThmWithTrivialProof : (A : Prop) -> Proof A -> Text ;
-
-  -- logically complex propositions
-  Disj : (A,B : Prop) -> Prop ;
-  Conj : (A,B : Prop) -> Prop ;
-  Impl : (A,B : Prop) -> Prop ;
-  Abs  : Prop ;
-  Neg  : Prop -> Prop ;
-
-  Univ  : (A : Dom) -> (Elem A -> Prop) -> Prop ;
-  Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
- 
-  -- progressive implication à la type theory
-  ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
-
-  -- inference rules
-data  
-  ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;
-fun  
-  ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
-  ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
-data  
-  DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
-  DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
-fun  
-  DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
-              (Proof A -> Proof C) -> (Proof B -> Proof C) -> Proof C ;
-data
-  ImplI  : (A,B : Prop) -> (Proof A -> Proof B) -> Proof (Impl A B) ;
-fun
-  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
-data
-  NegI   : (A : Prop) -> (Proof A -> Proof Abs) -> Proof (Neg A) ;
-fun
-  NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
-  AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
-data
-  UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
-              ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
-fun
-  UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
-              Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
-data
-  ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
-              (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
-fun
-  ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
-              Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
-              Proof C ;
-
-  -- use a hypothesis
-  Hypo : (A : Prop) -> Proof A -> Proof A ;
-
-  -- pronoun
-  Pron : (A : Dom) -> Elem A -> Elem A ;
-
-def 
-  -- proof normalization; does not tc 13/9/2005
-
-  ConjEl _ _ (ConjI _ _ a _) = a ;
-  ConjEr _ _ (ConjI _ _ _ b) = b ;
-  DisjE _ _ _ (DisjIl _ _ a) d _ = d a ;
-  DisjE _ _ _ (DisjIr _ _ b) _ e = e b ;
-  ImplE _ _ (ImplI _ _ b) a = b a ;
-  NegE _ (NegI _ b) a = b a ;
-  UnivE _ _ (UnivI _ _ b) a = b a ;
-  ExistE A B _ (ExistI A B a b) d = d a b ;
- 
----  ExistE _ _ _ (ExistI _ _  a b) d = d a b ; 
---- does not tc 13/9/2005: {a{-2-}<>a{-0-}}
---- moreover: no problem with
---- ConjEr _ _ (ConjI _ _ a _) = a ;
---- But this changes when A B are used instead of _ _
-
-  -- Hypo and Pron are identities
-  Hypo _ a = a ;
-  Pron _ a = a ;
-
-} ;
diff --git a/grammars/logic/LogicEng.gf b/grammars/logic/LogicEng.gf
deleted file mode 100644
index b708068e2..000000000
--- a/grammars/logic/LogicEng.gf
+++ /dev/null
@@ -1,60 +0,0 @@
-concrete LogicEng of Logic = open LogicResEng, Prelude in {
-
-flags lexer=vars ; unlexer=text ;
-
-lincat 
-  Dom = {s : Num => Str} ;
-  Prop, Elem = {s : Str} ;
-
-lin 
-Statement A = {s = A.s ++ "."} ;
-ThmWithProof A a = {s = 
-  ["Theorem ."] ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ a.s ++ "."} ;
-ThmWithTrivialProof A a = 
-  {s = "Theorem" ++ "." ++ A.s ++ "." ++ PARA ++ "Proof" ++ "." ++ "Trivial" ++ "."} ;
-Disj A B = {s = A.s ++ "or" ++ B.s} ;
-Conj A B = {s = A.s ++ "and" ++ B.s} ;
-Impl A B = {s = "if" ++ A.s ++ "then" ++ B.s} ;
-Univ A B = {s = ["for all"] ++ A.s ! pl ++ B.$0 ++ "," ++ B.s} ;
-Exist A B =
-  {s = ["there exists"] ++ indef ++ A.s ! sg ++ B.$0 ++ ["such that"] ++ B.s} ;
-Abs = {s = ["we have a contradiction"]} ;
-Neg A = {s = ["it is not the case that"] ++ A.s} ;
-ImplP A B = {s = "if" ++ A.s ++ "then" ++ B.s} ;
-ConjI A B a b = {s = a.s ++ "." ++ b.s ++ [". Hence"] ++ A.s ++ "and" ++ B.s} ;
-ConjEl A B c = {s = c.s ++ [". A fortiori ,"] ++ A.s} ;
-ConjEr A B c = {s = c.s ++ [". A fortiori ,"] ++ B.s} ;
-DisjIl A B a = {s = a.s ++ [". A fortiori ,"] ++ A.s ++ "or" ++ B.s} ;
-DisjIr A B b = {s = b.s ++ [". A fortiori ,"] ++ A.s ++ "or" ++ B.s} ;
-DisjE A B C c d e = {s = 
-  c.s ++ 
-  [". There are two possibilities . First , assume"] ++ 
-  A.s ++ "(" ++ d.$0 ++ ")" ++ "." ++ d.s ++ 
-  [". Second , assume"] ++ B.s ++ "(" ++ e.$0 ++ ")" ++ "." ++ e.s ++ 
-  [". Thus"] ++ C.s ++ ["in both cases"]} ;
-ImplI A B b = {s = 
-  "assume" ++ A.s ++ "(" ++ b.$0 ++ ")" ++ "." ++ 
-  b.s ++ [". Hence , if"] ++ A.s ++ "then" ++ B.s} ;
-ImplE A B c a = {s = a.s ++ [". But"] ++ c.s ++ [". Hence"] ++ B.s} ;
-NegI A b = {s = 
-  "assume" ++ A.s ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ 
-  [". Hence, it is not the case that"] ++ A.s} ;
-NegE A c a =
-  {s = a.s ++ [". But"] ++ c.s ++ [". We have a contradiction"]} ;
-UnivI A B b = {s = 
-  ["consider an arbitrary"] ++ A.s ! sg ++ b.$0 ++ "." ++ b.s ++ 
-  [". Hence, for all"] ++ A.s ! pl ++ B.$0 ++ "," ++ B.s} ;
-UnivE A B c a =
-  {s = c.s ++ [". Hence"] ++ B.s ++ "for" ++ B.$0 ++ ["set to"] ++ a.s} ;
-ExistI A B a b = {s = 
-  b.s ++ [". Hence, there exists"] ++ indef ++ 
-  A.s ! sg ++ B.$0 ++ ["such that"] ++ B.s} ;
-ExistE A B C c d = {s = 
-  c.s ++ [". Consider an arbitrary"] ++ d.$0 ++ 
-  ["and assume that"] ++ B.s ++ "(" ++ d.$1 ++ ")" ++ "." ++ d.s ++ 
-  [". Hence"] ++ C.s ++ ["independently of"] ++ d.$0} ;
-AbsE C c = {s = c.s ++ [". We may conclude"] ++ C.s} ;
-Hypo A a = {s = ["by the hypothesis"] ++ a.s ++ "," ++ A.s} ;
-Pron _ _ = {s = "it"} ;
-
-} ;
diff --git a/grammars/logic/LogicFre.gf b/grammars/logic/LogicFre.gf
deleted file mode 100644
index 65beb56ae..000000000
--- a/grammars/logic/LogicFre.gf
+++ /dev/null
@@ -1,84 +0,0 @@
-concrete LogicFre of Logic = open ResFre, Prelude in {
-
-flags lexer=vars ; unlexer=text ;
-
-lincat 
-Text = {s : Str} ;
-Dom = {g : Gen ; s : Num => Str} ;
-Prop = LinProp ;
-Elem = LinElem ;
-Proof = {s : Str} ;
-
-lindef Elem = \e -> {g = masc ; s = table {c => prep ! c ++ e}} ;
-
-lin
-Statement A = 
-  {s = A.s ! ind ++ "."} ;
-ThmWithProof A a =
-  {s = "Théorème"++"." ++ (A.s ! ind) ++ "."++ PARA ++ "Démonstration"++"." ++ a.s ++ "."} ;
-ThmWithTrivialProof A a =
-  {s = "Théorème"++"." ++ (A.s ! ind) ++ "."++ PARA ++ "Démonstration"++"."++"Triviale"++"."} ;
-Disj A B =
-  {s = table {m => (A.s ! m) ++ "ou" ++ B.s ! m}} ;
-Conj A B =
-  {s = table {m => (A.s ! m) ++ "et" ++ B.s ! m}} ;
-Impl A B =
-  {s = table {m => si ++ (A.s ! ind) ++ "alors" ++ B.s ! m}} ;
-Univ A B =
-  {s = table {m => "pour" ++ tout ! A.g ! pl ++ "les" ++ A.s ! pl ++ B.$0 ++ "," ++ B.s ! m}} ;
-Exist A B =
-  {s = table {m => "il"++"existe" ++ indef ! A.g ++ A.s ! sg ++ B.$0 ++ 
-        tel ! A.g ! sg ++ que ++ B.s ! subj}} ;
-Abs  =
-  {s = table {{ind} => "nous"++"avons"++"une"++"contradiction" ; {subj} => "nous"++"ayons"++"une"++"contradiction"}} ;
-Neg A =
-  {s = table {m => "il" ++ ne ++ etre ! sg ! m ++ "pas"++"vrai" ++ que ++ A.s ! subj}} ;
-ImplP A B =
-  {s = table {m => si ++ (A.s ! ind) ++ "alors" ++ B.s ! m}} ;
-ConjI A B a b =
-  {s = a.s ++ "." ++ b.s ++ "."++"Donc" ++ (A.s ! ind) ++ "et" ++ B.s ! ind} ;
-ConjEl A B c =
-  {s = c.s ++ "."++"A"++"fortiori," ++ A.s ! ind} ;
-ConjEr A B c =
-  {s = c.s ++ "."++"A"++"fortiori," ++ B.s ! ind} ;
-DisjIl A B a =
-  {s = a.s ++ "."++"A"++"fortiori," ++ (A.s ! ind) ++ "ou" ++ B.s ! ind} ;
-DisjIr A B b =
-  {s = b.s ++ "."++"A"++"fortiori," ++ (A.s ! ind) ++ "ou" ++ B.s ! ind} ;
-DisjE A B C c d e =
-  {s = c.s ++ "."++
-       "Nous"++"avons"++"deux"++"possibilités."++ 
-       "Premièrement,"++ "supposons" ++ que ++ A.s ! ind ++ "(" ++ d.$0 ++ ")" ++ 
-       "." ++ d.s ++ "."++
-       "Deuxièmement,"++ "supposons" ++ que ++ B.s ! ind ++ "(" ++ e.$0 ++ ")" ++ 
-       "." ++ e.s ++ "."++"Donc" ++ (C.s ! ind) ++ "dans"++"les"++"deux"++"cas"} ;
-ImplI A B b =
-  {s = "supposons" ++ que ++ A.s ! ind ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ "."++
-       "Donc"++"," ++ si  ++ A.s ! ind ++ "alors" ++ B.s ! ind} ;
-ImplE A B c a =
-  {s = a.s ++ "."++"Mais" ++ c.s ++ "."++"Donc" ++ B.s ! ind} ;
-NegI A b =
-  {s = "supposons" ++ que ++ A.s ! ind ++ "(" ++ b.$0 ++ ")" ++ "." ++ b.s ++ "." ++
-       ["Donc , il n'est pas vrai"] ++ que ++ A.s ! subj} ;
-NegE A c a =
-  {s = a.s ++ "."++"Mais" ++ c.s ++ "." ++ ["Nous avons une contradiction"]} ;
-UnivI A B b =
-  {s = "considérons" ++ indef ! A.g ++ A.s ! sg ++ b.$0 ++ "arbitraire." ++ 
-       b.s ++ "."++"Donc"++","++"pour" ++ tout ! A.g ! pl ++ 
-       "les" ++ A.s ! pl ++ B.$0 ++ "," ++ B.s ! ind} ;
-UnivE A B c a =
-  {s = c.s ++ "."++
-       "Donc" ++ B.s ! ind ++ "avec" ++ B.$0 ++ "remplacé" ++ "par" ++ a.s ! nom} ;
-ExistI A B a b =
-  {s = b.s ++ "."++"Donc"++"il"++"existe" ++ indef ! A.g ++ A.s ! sg ++ B.$0 ++ 
-       tel ! A.g ! sg ++ que ++ B.s ! subj} ;
-ExistE A B C c d =
-  {s = c.s ++ "."++"Considérons" ++ indef ! A.g ++ A.s ! sg ++ d.$0 ++ 
-       ["arbitraire , et supposons"] ++ que ++ B.s ! ind ++ "(" ++ d.$1 ++ ")" ++ 
-       "." ++ d.s ++ "."++"Donc" ++ C.s ! ind ++ "indépendamment" ++ "de" ++ d.$0} ;
-AbsE C c =
-  {s = c.s ++ "." ++ "Nous" ++ "concluons" ++ que ++ C.s ! ind} ;
-Hypo A a =
-  {s = "par"++"l'hypothèse" ++ a.s ++ "," ++ A.s ! ind} ;
-Pron A _ = {s = pronom ! A.g ; g = A.g} ;
-} ;
\ No newline at end of file
diff --git a/grammars/logic/LogicResEng.gf b/grammars/logic/LogicResEng.gf
deleted file mode 100644
index 94866bf05..000000000
--- a/grammars/logic/LogicResEng.gf
+++ /dev/null
@@ -1,27 +0,0 @@
-resource LogicResEng = {
-
-param Num = sg | pl  ;
-
-oper 
-  
-  ss  : Str -> {s : Str} = \s -> {s = s} ;
-
-  nomReg : Str -> Num => Str = \s -> table {sg => s ; pl => s + "s"} ;
-
-  indef : Str = pre {"a" ; "an" / strs {"a" ; "e" ; "i" ; "o"}} ;
-
-  LinElem : Type = {s : Str} ;
-  LinProp : Type = {s : Str} ;
-
-  adj1 : Str -> LinElem -> LinProp = 
-    \adj,x -> ss (x.s ++ "is" ++ adj) ;
-  adj2 : Str -> LinElem -> LinElem -> LinProp = 
-    \adj,x,y -> ss (x.s ++ "is" ++ adj ++ y.s) ;
-
-  fun1 : Str -> LinElem -> LinElem = 
-    \f,x -> ss ("the" ++ f ++ "of" ++ x.s) ;
-  fun2 : Str -> LinElem -> LinElem -> LinElem = 
-    \f,x,y -> ss ("the" ++ f ++ "of" ++ x.s ++ "and" ++ y.s) ;
-
-
-} ;
diff --git a/grammars/logic/ResFre.gf b/grammars/logic/ResFre.gf
deleted file mode 100644
index 7283e9fcd..000000000
--- a/grammars/logic/ResFre.gf
+++ /dev/null
@@ -1,78 +0,0 @@
-resource ResFre = {
-param 
-Gen = masc  | fem  ;
-Num = sg  | pl  ;
-Mod = ind  | subj  ;
-Cas = nom  | aa  | dd  ;
-
-oper 
-nomReg : Str -> Num => Str = \str -> table {{sg} => str ; {pl} => str + "s"} ;
-adjReg : Str -> Gen => Num => Str = \str -> 
-  table {{masc} => nomReg str ; {fem} => nomReg (str + "e")} ;
-adjEl : Str -> Gen => Num => Str = \str ->
-  table {{masc} => nomReg str ; {fem} => nomReg (str + "le")} ;
-adjAl : Str -> Gen => Num => Str =  \str ->
-  table {{masc} => table {{sg} => str + "l" ; {pl} => str + "ux"} ; 
-       {fem}  => nomReg (str + le) } ;
-adjEr : Str -> Gen => Num => Str = \str ->
-  table {{masc} => nomReg (str + "er") ; {fem}  => nomReg (str + "ère")} ;
-
-LinElem = {g : Gen ; s : Cas => Str} ;
-LinProp = {s : Mod => Str} ;
-
-voyelle : Strs = strs {"a" ; "e" ; "i" ; "o" ; "u" ; "y" ; "é"} ;
-elision : Str = pre {"e" ; "'" / voyelle} ;
-ne : Str = "n" + elision ;
-de : Str = "d" + elision ;
-le : Str = "l" + elision ;
-que : Str = "qu" + elision ;
-
-si : Str = pre {"si" ; "s'" / strs {"il" ; "ils"}} ;
-indef : Gen => Str = table {{masc} => "un" ; _ => "une"} ;
-tel : Gen => Num => Str = adjEl "tel" ;
-tout : Gen => Num => Str =
-  table {{masc} => table {{sg} => "tout" ; {pl} => "tous"} ; {fem} => nomReg "toute" } ;
-etre : Num => Mod => Str = formVerbe "est" "soit" "sont" "soient" ;
-
-formVerbe : Str -> Str -> Str -> Str -> Num => Mod => Str = 
- \sgi -> \sgs -> \pli -> \pls ->
-  table {{sg} => table {{ind} => sgi ; {subj} => sgs} ; 
-       {pl} => table {{ind} => pli ; {subj} => pls}} ; 
-prep : Cas => Str =
-  table {{nom} => [] ; {aa} => "à" ; {dd} => de} ;
-
-defin : Num => Gen => Cas => Str =
-  table {
-   {sg} => table {
-     {masc} => table {
-         {dd}  => pre {"du" ; "de"++"l'" / voyelle} ; 
-         {aa}  => pre {"au" ; "à"++"l'" / voyelle} ;
-         c     => prep ! c ++ le
-                   } ;
-     {fem}  => table {
-         c     => prep ! c ++ pre {"la" ; "l'" / voyelle} 
-                   }
-               } ;
-   {pl} => table {
-     _     => table {
-         {dd}  => "des" ; 
-         {aa}  => "aux" ;
-         c     => prep ! c ++ "les"
-                  }
-               }
-  } ;
-
-pronom : Gen => Cas => Str = table {
-  masc => table {nom => "il" ; c => prep ! c ++ "lui"} ;
-  fem  => table {c => prep ! c ++ "elle"} 
-  } ;
-
-mkPropA1 : LinElem -> (Gen => Num => Str) -> LinProp = \elem -> \adj ->
- {s = table {m => elem.s ! nom ++ etre ! sg ! m ++ adj ! elem.g ! sg}} ;
-
-mkPropA2 : Cas -> LinElem -> (Gen => Num => Str) -> LinElem -> LinProp = 
- \cas -> \elem -> \adj -> \elem2 -> let 
-   {adjP : Gen => Num => Str = table {g => table {n => adj ! g ! n ++ elem2.s ! cas}}}
- in mkPropA1 elem adjP ;
-
-}