Commit 79cc2961 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

A compiler from λς-calculus to Dedukti

parent c116363d
{
open Parser
exception Unexpected_char of char
}
rule token = parse
| [ ' ' '\t' ] as c
{ Format.eprintf "ignore '%c'@\n" c; token lexbuf }
| '\n' { token lexbuf }
| '.'([ 'a'-'z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s)"<=" { UPDATE (s) }
| '.'([ 'a'-'z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s) { SELECT (s) }
| '[' { LBRACK }
| ']' { RBRACK }
| ':' { COLUMN }
| ';' { SEMICOLUMN }
| '(' { LPAR }
| ')' { RPAR }
| "ς" { SIGMA }
| '=' { EQUAL }
| ":=" { DEF }
| '.' { DOT }
| "->" { ARR }
| "λ" { LAMBDA }
| "type" { TYPE (Parsing.rhs_start_pos 1) }
| "var" { VAR (Parsing.rhs_start_pos 1) }
| "check" { CHECK (Parsing.rhs_start_pos 1) }
| "norm" { NORM (Parsing.rhs_start_pos 1) }
| [ 'a'-'z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { ID (s) }
| [ 'A'-'Z' ] ['a'-'z' 'A'-'Z' '_' '0'-'9']* as s { CID (s) }
| _ as c { raise (Unexpected_char c) }
| eof { raise End_of_file }
%{
open Parsetree
let rec insert k v = function
| [] -> [(k, v)]
| (k', v') :: l when k < k' -> (k, v) :: (k', v') :: l
| (k', _) :: l when k = k' -> (k, v) :: l
| (k', v') :: l -> (k', v') :: (k, v) :: l
let parse_error s = print_endline s
%}
%token <string> ID CID SELECT UPDATE
%token LBRACK RBRACK COLUMN SEMICOLUMN LPAR RPAR SIGMA EQUAL DEF DOT
%token LAMBDA ARR
%token <Lexing.position> TYPE VAR CHECK NORM
%right ARR
%start line
%type <Lexing.position * Parsetree.line> line
%%
prog: /* empty */ { [] }
| line prog { $1 :: $2 }
;
line: TYPE CID DEF ty DOT { ($1, Typedef (Cid ($2), $4)) }
| VAR ID COLUMN ty DEF term DOT { ($1, Vardef (Id ($2), $4, $6)) }
| CHECK term COLUMN ty DOT { ($1, Check ($2, $4)) }
| NORM term DOT { ($1, Norm ($2)) }
;
ty: CID { Tcid (Cid ($1)) }
| LBRACK type_elems RBRACK { Tlist ($2) }
| ty ARR ty { Tarr ($1, $3) }
;
type_elems: /* empty */ { [] }
| ID COLUMN ty SEMICOLUMN type_elems { insert (Label $1) $3 $5 }
;
term: ID { Var (Id ($1)) }
| LPAR term RPAR { Par ($2) }
/* | term term { App ($1, $2) } */
| LAMBDA LPAR ID COLUMN ty RPAR term { Abst (Id ($3), $5, $7)}
| LBRACK obj_elems RBRACK { Obj ($2) }
| term SELECT { Select ($1, Label ($2)) }
| term UPDATE meth { Update ($1, Label ($2), $3) }
;
meth: SIGMA LPAR ID COLUMN ty RPAR term { Method (Id ($3), $5, $7) }
;
obj_elems: /* empty */ { [] }
| ID EQUAL meth SEMICOLUMN obj_elems { insert (Label ($1)) $3 $5 }
;
%%
type id = Id of string;;
type cid = Cid of string;;
type label = Label of string;;
type stype =
| Tcid of cid
| Tlist of (label * stype) list
| Tarr of stype * stype;;
type term =
| Var of id
| Par of term
| App of term * term
| Abst of id * stype * term
| Obj of (label * meth) list
| Select of term * label
| Update of term * label * meth
and meth = Method of id * stype * term;;
type line =
| Typedef of cid * stype
| Vardef of id * stype * term
| Check of term * stype
| Norm of term
;;
open Parsetree
open Scoper
open Typer
let print_id out_fmter (Id i) = Format.fprintf out_fmter "%s" i
let print_cid out_fmter (Cid c) = Format.fprintf out_fmter "%s" c
let print_label out_fmter (Label l) = Format.fprintf out_fmter "%s" l
let rec print_ty out_fmter = function
| Stcid (c, _) -> print_cid out_fmter c
| Stlist [] ->
Format.fprintf out_fmter "@[type_nil@]"
| Stlist ((l, ty) :: ll) ->
Format.fprintf out_fmter "@[type_cons@ (%a)@ (%a)@ (%a)@]"
print_label l
print_ty ty
print_ty (Stlist ll)
| Starr (ty1, ty2) ->
Format.fprintf out_fmter "@[Arrow@ (%a)@ (%a)@]"
print_ty ty1
print_ty ty2
let rec print_term out_fmter : tterm -> unit = function
| Tvar (id, _) -> print_id out_fmter id
| Tconst (id, _, _) -> print_id out_fmter id
| Tpar t ->
Format.fprintf out_fmter "(%a)"
print_term t
| Tapp (t1, t2, ty2, ty) ->
Format.fprintf out_fmter "@[App@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_ty ty2
print_term t1
print_term t2
| Tabst (x, ty, body, rty) ->
Format.fprintf out_fmter "@[Lambda@ (%a)@ (%a)@ (%a :@ %a =>@ %a)@]"
print_ty ty
print_ty rty
print_id x
print_ty ty
print_term body
| Tobj (ll, ty) ->
print_object ty out_fmter ll
| Tsel (t, l, ty) ->
Format.fprintf out_fmter "@[select@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_term t
print_label l
| Tupd (t, l, m, ty) ->
Format.fprintf out_fmter "@[update@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_term t
print_label l
print_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[coerce@ I@ (%a)@ (%a)@ (%a)@]"
print_ty ty1
print_ty ty2
print_term t
and print_object ty out_fmter = function
| [] ->
Format.fprintf out_fmter "@[prenil@ (%a)@ (assoc@ (%a))@]"
print_ty ty
print_ty ty
| (l, m) :: ll ->
Format.fprintf out_fmter "@[precons@ (%a)@ (assoc@ (%a))@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_ty ty
print_domain ll
print_label l
print_meth m
(print_object ty) ll
and print_domain out_fmter = function
| [] -> Format.fprintf out_fmter "domain_nil"
| (l, _) :: ll ->
Format.fprintf out_fmter "@[domain_cons@ (%a)@ (%a)"
print_label l
print_domain ll
and print_meth out_fmter (Tmeth (x, ty, body, rty)) =
Format.fprintf out_fmter "@[(%a :@ %a => %a)@]"
print_id x
print_ty ty
print_term body
let print_line out_fmter = function
| Ttypedef (cid, ty) ->
Format.fprintf out_fmter "@[%a :@ type :=@ %a.@]@\n"
print_cid cid
print_ty ty
| Tvardef (id, ty, def) ->
Format.fprintf out_fmter "@[%a :@ Object (%a) :=@ %a.@]@\n"
print_id id
print_ty ty
print_term def
| Tcheck (t, ty) ->
Format.fprintf out_fmter "@[#CHECK %a :@ %a.@]@\n"
print_term (Tcast (t, infer t, ty))
print_ty ty
| Tnorm t ->
Format.fprintf out_fmter "@[#SNF %a.@]@\n"
print_term t
let print out_fmter = List.iter (print_line out_fmter)
val print : Format.formatter -> Typer.typed_tree -> unit
open Parsetree
exception Unknown_type_variable of cid
exception Unknown_variable of id
type sty =
| Stcid of cid * sty
| Stlist of (label * sty) list
| Starr of sty * sty
type sterm =
| Svar of id * sty
| Sconst of id * sty * sterm
| Spar of sterm
| Sapp of sterm * sterm
| Sabst of id * sty * sterm
| Sobj of (label * smeth) list
| Ssel of sterm * label
| Supd of sterm * label * smeth
and smeth =
| Smeth of id * sty * sterm
type sline =
| Stypedef of cid * sty
| Svardef of id * sty * sterm
| Scheck of sterm * sty
| Snorm of sterm
type scoped_tree = sline list
let rec scope_ty ty_env = function
| Tcid cid ->
(try
Stcid (cid, List.assoc cid ty_env)
with Not_found ->
raise (Unknown_type_variable cid))
| Tlist l ->
Stlist (List.map
(fun (lab, ty) -> (lab, scope_ty ty_env ty))
l)
| Tarr (ty1, ty2) ->
Starr (scope_ty ty_env ty1,
scope_ty ty_env ty2)
let rec assoc3 v = function
| [] -> raise Not_found
| (v', a, b) :: _ when v = v' -> (a, b)
| _ :: l -> assoc3 v l
let rec scope_term ty_env const_env var_env : term -> sterm = function
| Var v ->
(try
Svar (v, List.assoc v var_env)
with Not_found -> (
try
let (ty, def) = assoc3 v const_env in
Sconst (v, ty, def)
with Not_found -> raise (Unknown_variable v)))
| Par t -> Spar (scope_term ty_env const_env var_env t)
| App (t1, t2) ->
Sapp (scope_term ty_env const_env var_env t1,
scope_term ty_env const_env var_env t2)
| Abst (x, ty, body) ->
let sty = scope_ty ty_env ty in
Sabst (x, sty, scope_term ty_env const_env ((x, sty) :: var_env) body)
| Obj l ->
Sobj (List.map (fun (l, m) -> (l, scope_method ty_env const_env var_env m)) l)
| Select (t, l) ->
Ssel (scope_term ty_env const_env var_env t, l)
| Update (t, l, m) ->
Supd (scope_term ty_env const_env var_env t,
l,
scope_method ty_env const_env var_env m)
and scope_method ty_env const_env var_env (Method (id, ty, body)) =
let sty = scope_ty ty_env ty in
Smeth (id, sty, scope_term ty_env const_env ((id, sty) :: var_env) body)
let scope_line ty_env const_env = function
| Parsetree.Typedef (cid, ty) ->
let sty = scope_ty ty_env ty in
((cid, sty) :: ty_env, const_env, Stypedef (cid, sty))
| Vardef (id, ty, def) ->
let sty = scope_ty ty_env ty in
let sdef = scope_term ty_env const_env [] def in
(ty_env, (id, sty, sdef) :: const_env, Svardef (id, sty, sdef))
| Check (t, ty) ->
let sty = scope_ty ty_env ty in
let st = scope_term ty_env const_env [] t in
(ty_env, const_env, Scheck (st, sty))
| Norm t ->
(ty_env, const_env, Snorm (scope_term ty_env const_env [] t))
let rec scope_prog ty_env const_env = function
| [] -> []
| (pos, line) :: prog ->
let (nty_env, nconst_env, sline) = scope_line ty_env const_env line in
sline :: scope_prog nty_env nconst_env prog
let scope = scope_prog [] []
open Parsetree
type sty =
| Stcid of cid * sty
| Stlist of (label * sty) list
| Starr of sty * sty
type sterm =
| Svar of id * sty
| Sconst of id * sty * sterm
| Spar of sterm
| Sapp of sterm * sterm
| Sabst of id * sty * sterm
| Sobj of (label * smeth) list
| Ssel of sterm * label
| Supd of sterm * label * smeth
and smeth =
| Smeth of id * sty * sterm
type sline =
| Stypedef of cid * sty
| Svardef of id * sty * sterm
| Scheck of sterm * sty
| Snorm of sterm
type scoped_tree = sline list
val scope : (Lexing.position * Parsetree.line) list -> scoped_tree
let print_pos lb =
let start = lb.Lexing.lex_start_p in
let file = start.Lexing.pos_fname in
let line = start.Lexing.pos_lnum in
let cnum = start.Lexing.pos_cnum - start.Lexing.pos_bol in
let tok = Lexing.lexeme lb in
Format.eprintf "File: %s, line: %d, column: %d, Token \"%s\"@\n@."
file line cnum tok
let rec lex_prog lb =
try
let (pos, line) = Parser.line Lexer.token lb in
let lines = lex_prog lb in
(pos, line) :: lines
with End_of_file -> []
| e ->
let start = lb.Lexing.lex_start_p in
let file = start.Lexing.pos_fname in
let line = start.Lexing.pos_lnum in
let cnum = start.Lexing.pos_cnum - start.Lexing.pos_bol in
let tok = Lexing.lexeme lb in
Format.eprintf "File: %s, line: %d, column: %d, Parse error: unexpected token %s@\n@."
file line cnum tok;
raise e
let main () =
Arg.parse [] (fun file ->
let err = Format.err_formatter in
Format.fprintf err "Sigmaid@\n@.";
let input = open_in file in
let lexbuf = Lexing.from_channel input in
let out_fmter = Format.std_formatter in
let prog = lex_prog lexbuf in
Format.fprintf err "Programm lexed@\n.";
let scoped_prog = Scoper.scope prog in
Format.fprintf err "Programm scoped@\n.";
let typed_prog = Typer.type_check scoped_prog in
Format.fprintf err "Programm typed@\n.";
Printer.print out_fmter typed_prog;
Format.fprintf err "Programm printed@\n@.";
) "Please provide a file name."
let _ = main ()
open Parsetree
open Scoper
type tterm =
| Tvar of id * sty
| Tconst of id * sty * tterm
| Tpar of tterm
| Tapp of tterm * tterm * sty * sty
| Tabst of id * sty * tterm * sty
| Tobj of (label * tmeth) list * sty
| Tsel of tterm * label * sty
| Tupd of tterm * label * tmeth * sty
| Tcast of tterm * sty * sty
and tmeth = Tmeth of id * sty * tterm * sty
type tline =
| Ttypedef of cid * sty
| Tvardef of id * sty * tterm
| Tcheck of tterm * sty
| Tnorm of tterm
type typed_tree = tline list
exception Sty_assoc_arrow
let rec sty_assoc l = function
| Stcid (_, b) -> sty_assoc l b
| Stlist ll -> List.assoc l ll
| Starr _ -> raise Sty_assoc_arrow
exception Application_of_non_functionnal_value
let rec sty_decompose_arrow = function
| Stcid (_, b) -> sty_decompose_arrow b
| Stlist _ -> raise Application_of_non_functionnal_value
| Starr (t1, t2) -> (t1, t2)
let rec subtype (a : sty) : sty -> bool = function
| Stcid (_, b) -> subtype a b
| Starr (b1, b2) -> (match a with
| Starr (a1, a2) -> eq a1 b1 && eq a2 b2
| _ -> false)
| Stlist [] -> true
| Stlist ((l, bl) :: b) -> eq bl (sty_assoc l a) && subtype a (Stlist b)
and eq a b = subtype a b && subtype b a
let rec infer : tterm -> sty = function
| Tvar (_, ty) -> ty
| Tconst (_, ty, _) -> ty
| Tpar t -> infer t
| Tapp (_, _, _, ty) -> ty
| Tabst (x, ty, t, rty) -> Starr (ty, rty)
| Tobj (ll, ty) -> ty
| Tsel (_, _, ty) -> ty
| Tupd (_, _, _, ty) -> ty
| Tcast (_, _, ty) -> ty
and infer_meth (Tmeth (_, _, _, ty)) = ty
exception Subype_checking_error of sty * sty
let rec type_term env : sterm -> tterm = function
| Svar (x, ty) -> Tvar (x, ty)
| Sconst (x, ty, def) -> Tconst (x, ty, type_term env def)
| Spar t -> Tpar (type_term env t)
| Sapp (t1, t2) ->
let tt1 = type_term env t1 in
let tt2 = type_term env t2 in
let ty1 = infer tt1 in
let (ty1l, ty1r) = sty_decompose_arrow ty1 in
let ty2 = infer tt2 in
if subtype ty2 ty1l then
Tapp (tt1, Tcast (tt2, ty2, ty1l), ty1l, ty1r)
else
raise (Subype_checking_error (ty2, ty1l))
| Sabst (x, ty, body) ->
let tbody = type_term ((x, ty) :: env) body in
Tabst (x, ty, tbody, infer tbody)
| Sobj ll ->
let tmeths = List.map (fun (l, m) -> (l, type_meth env m)) ll in
Tobj (tmeths, Stlist (List.map (fun (l, m) -> (l, infer_meth m)) tmeths))
| Ssel (t, l) ->
let tt = type_term env t in
let ty = infer tt in
Tsel (tt, l, sty_assoc l ty)
| Supd (t, l, m) ->
let tt = type_term env t in
Tupd (tt, l, type_meth env m, infer tt)
and type_meth env (Smeth (x, ty, body)) =
let tbody = type_term ((x, ty) :: env) body in
(Tmeth (x, ty, tbody, infer tbody))
exception Check_failed
let type_line = function
| Stypedef (a, ty) -> Ttypedef (a, ty)
| Svardef (id, ty, def) -> Tvardef (id, ty, type_term [] def)
| Scheck (t, ty) ->
let tt = type_term [] t in
if subtype (infer tt) ty then
Tcheck (tt, ty)
else
raise Check_failed
| Snorm t -> Tnorm (type_term [] t)
let type_check = List.map type_line
open Parsetree
open Scoper
type tterm =
| Tvar of id * sty
| Tconst of id * sty * tterm
| Tpar of tterm
| Tapp of tterm * tterm * sty * sty
| Tabst of id * sty * tterm * sty
| Tobj of (label * tmeth) list * sty
| Tsel of tterm * label * sty
| Tupd of tterm * label * tmeth * sty
| Tcast of tterm * sty * sty
and tmeth = Tmeth of id * sty * tterm * sty
type tline =
| Ttypedef of cid * sty
| Tvardef of id * sty * tterm
| Tcheck of tterm * sty
| Tnorm of tterm
type typed_tree = tline list
val infer : tterm -> sty
val type_check : Scoper.scoped_tree -> typed_tree
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment