summaryrefslogtreecommitdiff
path: root/grammars/logic
diff options
context:
space:
mode:
Diffstat (limited to 'grammars/logic')
-rw-r--r--grammars/logic/Arithm.gf66
-rw-r--r--grammars/logic/ArithmEng.gf42
-rw-r--r--grammars/logic/ArithmFre.gf37
-rw-r--r--grammars/logic/Logic.gf97
-rw-r--r--grammars/logic/LogicEng.gf60
-rw-r--r--grammars/logic/LogicFre.gf84
-rw-r--r--grammars/logic/LogicResEng.gf27
-rw-r--r--grammars/logic/ResFre.gf78
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 ;
-
-}
generated by cgit v1.2.3 (git 2.39.1) at 2026-07-19 02:12:54 +0000