Add "And" and "Or"

This commit is contained in:
augustin64 2024-05-05 20:33:39 +02:00
parent 0085a91251
commit 8fc21a0988
4 changed files with 17 additions and 0 deletions

View File

@ -10,6 +10,14 @@ let rec string_of_ty = function
let s2 = string_of_ty t2 in
"(" ^ s1 ^ " -> " ^ s2 ^ ")"
| Bot -> "False"
| And(t1, t2) ->
let s1 = string_of_ty t1 in
let s2 = string_of_ty t2 in
"(" ^ s1 ^ " /\\ " ^ s2 ^ ")"
| Or(t1, t2) ->
let s1 = string_of_ty t1 in
let s2 = string_of_ty t2 in
"(" ^ s1 ^ " \\/ " ^ s2 ^ ")"
let rec string_of_expr = function
Fun ((s, t), e) ->

View File

@ -27,6 +27,8 @@ rule token = parse
| "->" { TARR }
| '~' { TILDE }
| "exf" { EXFALSO }
| "/\\" { AND }
| "\\/" { OR }
| "Goal" { GOAL }
| "exact" { EXACT }

View File

@ -9,6 +9,7 @@ open Parser_entry
%token PLUS TIMES
%token TOP BOT EXFALSO TILDE
%token LPAREN RPAREN
%token AND OR
%token FUN ARR COLON TARR
%token <string> VARID
%token <string> TYID
@ -19,6 +20,8 @@ open Parser_entry
%right TARR
%right TILDE
%right AND
%right OR
%start main
%type <parser_entry> main
@ -50,6 +53,8 @@ ty:
| BOT { Bot }
| LPAREN t=ty RPAREN { t }
| TILDE t=ty { Arr(t, Bot) }
| t1=ty AND t2=ty { And(t1, t2) }
| t1=ty OR t2=ty { Or(t1, t2) }
| t1=ty TARR t2=ty { Arr(t1, t2) }
expression:

View File

@ -3,6 +3,8 @@ type ty_id = string
type ty =
TVar of ty_id
| Arr of ty * ty
| And of ty * ty
| Or of ty * ty
| Bot
type gam = (ty_id * ty) list