diff options
Diffstat (limited to 'contrib/dp/dp_why.ml')
| -rw-r--r-- | contrib/dp/dp_why.ml | 50 |
1 files changed, 32 insertions, 18 deletions
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml index d6a5e145c..662a5a8be 100644 --- a/contrib/dp/dp_why.ml +++ b/contrib/dp/dp_why.ml @@ -12,16 +12,28 @@ let rec print_list sep print fmt = function let space fmt () = fprintf fmt "@ " let comma fmt () = fprintf fmt ",@ " -let is_why_keyword s = false (* TODO *) +let is_why_keyword = + let h = Hashtbl.create 17 in + List.iter + (fun s -> Hashtbl.add h s ()) + ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin"; + "bool"; "do"; "done"; "else"; "end"; "exception"; "exists"; + "external"; "false"; "for"; "forall"; "fun"; "function"; "goal"; + "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not"; + "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises"; + "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try"; + "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; + Hashtbl.mem h let ident fmt s = - if is_why_keyword s then fprintf fmt "why__%s" s else fprintf fmt "%s" s + if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s let rec print_typ fmt = function - | Tvar x -> fprintf fmt "'%s" x - | Tid (x, []) -> fprintf fmt "%s" x - | Tid (x, [t]) -> fprintf fmt "%a %s" print_typ t x - | Tid (x, tl) -> fprintf fmt "(%a) %s" (print_list comma print_typ) tl x + | Tvar x -> fprintf fmt "'%a" ident x + | Tid ("int", []) -> fprintf fmt "int" + | Tid (x, []) -> fprintf fmt "%a" ident x + | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x + | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x let rec print_term fmt = function | Cst n -> @@ -79,40 +91,42 @@ let rec print_predicate fmt p = let print_query fmt (decls,concl) = let print_dtype = function | DeclType (id, 0) -> - fprintf fmt "@[type %s@]@\n@\n" id + fprintf fmt "@[type %a@]@\n@\n" ident id | DeclType (id, 1) -> - fprintf fmt "@[type 'a %s@]@\n@\n" id + fprintf fmt "@[type 'a %a@]@\n@\n" ident id | DeclType (id, n) -> fprintf fmt "@[type ("; - for i = 1 to n do fprintf fmt "'a%d" i done; - fprintf fmt ") %s@]@\n@\n" id + for i = 1 to n do + fprintf fmt "'a%d" i; if i < n then fprintf fmt ", " + done; + fprintf fmt ") %a@]@\n@\n" ident id | DeclFun _ | DeclPred _ | Axiom _ -> () in let print_dvar_dpred = function | DeclFun (id, _, [], t) -> - fprintf fmt "@[logic %s : -> %a@]@\n@\n" id print_typ t + fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t | DeclFun (id, _, l, t) -> - fprintf fmt "@[logic %s : %a -> %a@]@\n@\n" - id (print_list comma print_typ) l print_typ t + fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" + ident id (print_list comma print_typ) l print_typ t | DeclPred (id, _, []) -> - fprintf fmt "@[logic %s : -> prop @]@\n@\n" id + fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id | DeclPred (id, _, l) -> - fprintf fmt "@[logic %s : %a -> prop@]@\n@\n" - id (print_list comma print_typ) l + fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" + ident id (print_list comma print_typ) l | DeclType _ | Axiom _ -> () in let print_assert = function | Axiom (id, f) -> - fprintf fmt "@[<hov 2>axiom %s:@ %a@]@\n@\n" id print_predicate f + fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f | DeclType _ | DeclFun _ | DeclPred _ -> () in List.iter print_dtype decls; List.iter print_dvar_dpred decls; List.iter print_assert decls; - fprintf fmt "@[<hov 2>goal coq__goal: %a@]" print_predicate concl + fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl let output_file f q = let c = open_out f in |