Commit a217d958 authored by MARCHE Claude's avatar MARCHE Claude

first example, typing OK

parent 113d78e9
......@@ -33,8 +33,11 @@ and cfg_expr_desc =
(** Boolean literal [False] *)
| CFGconst of Constant.constant
(** Constant literals *)
| CFGlabel of ident * cfg_expr
(** declare a label *)
| CFGgoto of ident
(** goto a label *)
| CFGassert of Expr.assertion_kind * Ptree.term
(* TODO: expand *)
......
......@@ -287,9 +287,16 @@ rule token = parse
{
let () = Exn_printer.register (fun fmt exn -> match exn with
| Cfg_parser.Error -> Format.fprintf fmt "syntax error"
| _ -> raise exn)
let parse_channel file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
Cfg_parser.cfgfile token lb
try
Cfg_parser.cfgfile token lb
with
Cfg_parser.Error as e -> raise (Loc.Located (Loc.extract (lb.lex_start_p,lb.lex_curr_p),e))
}
......@@ -15,7 +15,7 @@ open Cfg_ast
open Ptree
open Wstdlib
let debug = Debug.register_flag "CFG"
let debug = Debug.register_flag "cfg"
~desc:"CFG plugin debug flag"
(*
......@@ -315,10 +315,38 @@ let decl = function
Typing.add_decl id.id_loc (Dprop (pk, id, t))
*)
let mk_expr loc e = { expr_desc = e; expr_loc = loc }
let psexp_pty fmt t =
Ptree.sexp_of_pty t |> Sexplib.Sexp.output_hum_indent 2 stdout
let rec pp_qid fmt qid =
match qid with
| Qident id -> Format.fprintf fmt "%s" id.id_str
| Qdot(q,id) -> Format.fprintf fmt "%a.%s" pp_qid q id.id_str
let rec pp_pty fmt t =
match t with
| PTtyapp(qid,l) ->
Format.fprintf fmt "@[%a %a@]"
pp_qid qid
(Pp.print_list Pp.semi pp_pty) l
| _ ->
Format.fprintf fmt "@[<pp_pty>@]"
let translate_cfg (id,args,retty,pat,spec,locals,body) =
Debug.dprintf debug "translating cfg function `%s`@." id.id_str;
Debug.dprintf debug "return type is `%a`@." pp_pty retty;
let body = mk_expr body.cfg_expr_loc (Etuple []) in
let f =
Efun(args, Some retty, pat, Ity.MaskVisible, spec, body)
in
Dlet (id,false,Expr.RKnone,mk_expr id.id_loc f)
let translate_decl d acc =
match d with
| Dmlw_decl d -> d :: acc
| Dletcfg l -> acc (* (id,_,_) -> Dmeta (id,[]) *)
| Dletcfg l -> List.fold_right (fun d acc -> (translate_cfg d)::acc) l acc
let translate (m,dl) =
(m,List.fold_right translate_decl dl [])
......
......@@ -29,20 +29,20 @@
%%
cfgfile:
| ml=cfgmodule* EOF { ml }
| ml=cfgmodule* EOF { ml }
;
cfgmodule:
| MODULE id=attrs(uident_nq) dl=cfgdecl* END
| MODULE id=attrs(uident_nq) dl=cfgdecl* END
{ (id,dl) }
cfgdecl:
| module_decl_parsing_only { Dmlw_decl $1 }
| LET CFG dl=with_list1(recdefn) { Dletcfg dl }
| module_decl_parsing_only { Dmlw_decl $1 }
| LET CFG dl=with_list1(recdefn) { Dletcfg dl }
;
recdefn:
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL b=body
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL b=body
{ let pat, ty, _mask = ret in
let spec = apply_return pat sp in
(id, args, ty, pat, spec, [], b) }
......@@ -53,7 +53,15 @@ body:
;
cfgexpr:
| TRUE { mk_cfgexpr CFGtrue $startpos $endpos }
| FALSE { mk_cfgexpr CFGfalse $startpos $endpos }
| GOTO uident { mk_cfgexpr (CFGgoto $2) $startpos $endpos }
| TRUE
{ mk_cfgexpr CFGtrue $startpos $endpos }
| FALSE
{ mk_cfgexpr CFGfalse $startpos $endpos }
| GOTO uident
{ mk_cfgexpr (CFGgoto $2) $startpos $endpos }
| LABEL id = attrs(uident) IN e = cfgexpr
{ mk_cfgexpr (CFGlabel(id,e)) $startpos $endpos }
| k=assertion_kind id=option(ident_nq) LEFTBRC t=term RIGHTBRC
{ let (n,k)=k in
mk_cfgexpr (CFGassert(k, name_term id n t)) $startpos $endpos }
;
module Basic
use int.Int
val test (x:int) : unit
let cfg cfgassert (x:int) : unit
requires { x >= 0 }
=
assert { false }
let cfg cfggoto (x:int) : unit
requires { x >= 0 }
=
label L in
goto L
let main () = cfgassert 42; cfggoto 43
end
\ No newline at end of file
......@@ -1274,7 +1274,7 @@ ext_match_cases0:
exn_handler:
| uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
assertion_kind:
%public assertion_kind:
| ASSERT { "Assert", Expr.Assert }
| ASSUME { "Assume", Expr.Assume }
| CHECK { "Check", Expr.Check }
......@@ -1485,7 +1485,7 @@ squalid:
| lident { $1 }
| lident_op { $1 }
ident_nq:
%public ident_nq:
| uident_nq { $1 }
| lident_nq { $1 }
| lident_op_nq { $1 }
......
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