Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.
On peut rajouter que je détestais le principe même du metamodèle UML qui empêche de faire des trucs aussi simple que de fixer la valeur d'une propriété dans un raffinement. Donc, j'ai mis les littéraux au même niveau que leur type.
La syntaxe n'est pas fixé, l'idée était plutôt un truc manipulable par des commandes externes (editeur texte ou graphique) ou un format de fichier type XML mais qui permet de définir des graphs acyclique avec le même langage pour le schéma.
type t =
(*Literals*)
| LInt of int
| LString of string
| LFloat of float
(*Internal type*)
| Integer
| Float
| String
(*Op*)
| And of t * t
| Or of t * t
| Xor of t list
(* Nommé *)
| Name of string
(* Pointeur avec un path *)
| Ref of string list (* TODO: adding integer index ref *)
(* Multiplicité *)
| Mult of int * int
J'avais tenté le gadt, mais j'avais vraiment du mal :
type _ term =
(*Literals*)
| LInt : int -> int term
| LString : string -> string term
| LFloat : float -> float term
(*Internal type*)
| Integer : int term
| Float : float term
| String : string term
(*Op*)
| And : 'a term * 'a term -> 'a term
| Or : _ term * _ term -> _ term
| Xor : 'a term list-> _ term (*agregation also used for array*)
(*Nommé *)
| Name : string -> _ term
(*Pointeur avec un path*)
| Ref : string list -> _ term
(*Multiplicité*)
| Mult : int * int -> 'a term J'avais aussi envie d'ajouter un "Not" pour faire l'inverse de "And", cela permet de faire une logique plus complète (j'y ai pensé après avoir lu logicomix). Mais le "And" n'est pas un "and" (je l'ai appelé comme ça par rapport à "|" du type sum), c'est plus un "Sont du même type" genre un "~", c'est un blanc dans ma mini syntaxe. Le "Xor" c'est le "*" de ocaml (définit par le retour à la ligne et la tabulation). Le moyen de faire les tuples et les array.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.
On peut rajouter que je détestais le principe même du metamodèle UML qui empêche de faire des trucs aussi simple que de fixer la valeur d'une propriété dans un raffinement. Donc, j'ai mis les littéraux au même niveau que leur type.
L'idée est de pouvoir écrire un truc comme :
La syntaxe n'est pas fixé, l'idée était plutôt un truc manipulable par des commandes externes (editeur texte ou graphique) ou un format de fichier type XML mais qui permet de définir des graphs acyclique avec le même langage pour le schéma.
https://github.com/nicolasboulay/cherry-lang/blob/master/src/grape.ml
J'avais tenté le gadt, mais j'avais vraiment du mal :
type _ term =
(*Literals*)
| LInt : int -> int term
| LString : string -> string term
| LFloat : float -> float term
(*Internal type*)
| Integer : int term
| Float : float term
| String : string term
(*Op*)
| And : 'a term * 'a term -> 'a term
| Or : _ term * _ term -> _ term
| Xor : 'a term list-> _ term (*agregation also used for array*)
(*Nommé *)
| Name : string -> _ term
(*Pointeur avec un path*)
| Ref : string list -> _ term
(*Multiplicité*)
| Mult : int * int -> 'a term
"La première sécurité est la liberté"