Commit 35bb2e87 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Add a conversion check

parent 810e345a
......@@ -32,10 +32,11 @@
%%
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)) }
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)) }
| CHECK term EQUAL term COLUMN ty DOT { ($1, Conv ($2, $4, $6)) }
| NORM term DOT { ($1, Norm ($2)) }
;
ty: CID { Tcid (Cid ($1)) }
......
......@@ -26,5 +26,6 @@ type line =
| Typedef of cid * stype
| Vardef of id * stype * term
| Check of term * stype
| Conv of term * term * stype
| Norm of term
;;
......@@ -109,6 +109,16 @@ let print_line out_fmter = function
Format.fprintf out_fmter "@[#CHECK %a,@ dk_obj.Expr@ (%a).@]@\n"
print_term t
print_ty ty
| Tconv (t1, t2, ty) ->
Format.fprintf out_fmter "@[<h>#CHECK %a,@ dk_obj.Expr@ %a.@]@\n"
print_term t1
print_par_ty ty;
Format.fprintf out_fmter "@[<h>#CHECK %a,@ dk_obj.Expr@ %a.@]@\n"
print_term t2
print_par_ty ty;
Format.fprintf out_fmter "@[<h>#CONV %a,@ %a.@]@\n"
print_term t1
print_term t2
| Tnorm t ->
Format.fprintf out_fmter "@[#SNF %a.@]@\n"
print_term t
......
......@@ -25,6 +25,7 @@ type sline =
| Stypedef of cid * sty
| Svardef of id * sty * sterm
| Scheck of sterm * sty
| Sconv of sterm * sterm * sty
| Snorm of sterm
type scoped_tree = sline list
......@@ -92,6 +93,11 @@ let scope_line ty_env const_env = function
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))
| Conv (t1, t2, ty) ->
let st1 = scope_term ty_env const_env [] t1 in
let st2 = scope_term ty_env const_env [] t2 in
let sty = scope_ty ty_env ty in
(ty_env, const_env, Sconv (st1, st2, sty))
| Norm t ->
(ty_env, const_env, Snorm (scope_term ty_env const_env [] t))
......
......@@ -22,6 +22,7 @@ type sline =
| Stypedef of cid * sty
| Svardef of id * sty * sterm
| Scheck of sterm * sty
| Sconv of sterm * sterm * sty
| Snorm of sterm
type scoped_tree = sline list
......
......@@ -21,9 +21,13 @@ type Nat ::= [ iszero : Bool ;
let 0 : Nat ::= [ iszero = ς(x : Nat) true ;
pred = ς(x : Nat) x.pred ].
let 42 : Nat ::= [ iszero = ς(x : Nat) true ;
pred = ς(x : Nat) x.pred ].
type RomCell ::= [ get : Nat ].
type PromCell ::= [ get : Nat ; set : Nat -> RomCell ].
let myCell : PromCell ::= [ get = ς( self : PromCell ) 0 ;
set = ς( self : PromCell ) λ(n : Nat) self.get := n ].
check (myCell.set 42).get = 42 : Nat.
......@@ -17,6 +17,7 @@ type tline =
| Ttypedef of cid * sty
| Tvardef of id * sty * tterm
| Tcheck of tterm * sty
| Tconv of tterm * tterm * sty
| Tnorm of tterm
type typed_tree = tline list
......@@ -210,6 +211,10 @@ let type_line = function
| Svardef (id, ty, def) -> Tvardef (id, ty, type_term [] def)
| Scheck (t, ty) ->
let tt = type_check [] ty t in Tcheck (tt, ty)
| Sconv (t1, t2, ty) ->
let tt1 = type_check [] ty t1 in
let tt2 = type_check [] ty t2 in
Tconv (tt1, tt2, ty)
| Snorm t -> Tnorm (type_term [] t)
let type_check = List.map type_line
......@@ -17,6 +17,7 @@ type tline =
| Ttypedef of cid * sty
| Tvardef of id * sty * tterm
| Tcheck of tterm * sty
| Tconv of tterm * tterm * sty
| Tnorm of tterm
type typed_tree = tline list
......
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