type des types algebriques

parent ff062252
......@@ -126,7 +126,7 @@ bin/top: $(CMO)
ocamlmktop $(BFLAGS) -o $@ $^
test: bin/why.byte
ocamlrun -bt bin/why.byte -I lib/prelude/ src/test.why
ocamlrun -bt bin/why.byte --print-simplify-recursive -I lib/prelude/ src/test.why
# graphical interface
#####################
......
......@@ -8,11 +8,11 @@ theory Int
logic (>) (int, int)
logic (>=)(int, int)
logic ( + ) (int, int) : int
logic ( - ) (int, int) : int
logic ( * ) (int, int) : int
logic ( / ) (int, int) : int
logic ( % ) (int, int) : int
logic (+) (int, int) : int
logic (-) (int, int) : int
logic (*) (int, int) : int
logic (/) (int, int) : int
logic (%) (int, int) : int
logic neg(int) : int
......
......@@ -129,14 +129,13 @@ let rec tv_inst m ty = match ty.ty_node with
| _ -> ty_map (tv_inst m) ty
let ty_app s tl =
if List.length tl == List.length s.ts_args
then match s.ts_def with
if List.length tl != List.length s.ts_args then raise BadTypeArity;
match s.ts_def with
| Some ty ->
let add m v t = Mid.add v t m in
tv_inst (List.fold_left2 add Mid.empty s.ts_args tl) ty
| _ ->
ty_app s tl
else raise BadTypeArity
(* symbol-wise map/fold *)
......
......@@ -33,8 +33,8 @@ let () =
"--debug", Arg.Set debug, "sets the debug flag";
"-I", Arg.String (fun s -> loadpath := s :: !loadpath),
"<dir> adds dir to the loadpath";
"--print_stdout", Arg.Set print_stdout, "print the results to stdout";
"--print_simplify_recursive", Arg.Set print_simplify_recursive, "print the results of simplify recursive definition";
"--print-stdout", Arg.Set print_stdout, "print the results to stdout";
"--print-simplify-recursive", Arg.Set print_simplify_recursive, "print the results of simplify recursive definition";
]
(fun f -> files := f :: !files)
"usage: why [options] files..."
......
......@@ -175,6 +175,8 @@ rule token = parse
|(hexadigit+ as i) ("" as f))
['p' 'P'] (['-' '+']? digit+ as e)
{ FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
| "(*)"
{ LIDENT "*" }
| "(*"
{ comment lexbuf; token lexbuf }
| "'"
......@@ -279,7 +281,7 @@ and string = parse
(*
Local Variables:
compile-command: "unset LANG; make -j -C .. bin/why.byte"
compile-command: "unset LANG; make -C ../.. test"
End:
*)
......@@ -300,25 +300,37 @@ let rec qloc = function
| Qdot (m, x) -> Loc.join (qloc m) x.id_loc
(* parsed types -> intermediate types *)
let rec type_inst s ty = match ty.ty_node with
| Ty.Tyvar n -> Mid.find n s
| Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)
let rec dty env = function
| PPTtyvar {id=x} ->
Tyvar (find_user_type_var x env)
| PPTtyapp (p, x) ->
let loc = qloc x in
let s, tv = specialize_tysymbol x env in
let ts, tv = specialize_tysymbol x env in
let np = List.length p in
let a = List.length tv in
if np <> a then error ~loc (TypeArity (x, a, np));
Tyapp (s, List.map (dty env) p)
let tyl = List.map (dty env) p in
match ts.ts_def with
| None ->
Tyapp (ts, tyl)
| Some ty ->
let add m v t = Mid.add v t m in
let s = List.fold_left2 add Mid.empty ts.ts_args tyl in
type_inst s ty
(* intermediate types -> types *)
let rec ty = function
let rec ty_of_dty = function
| Tyvar { type_val = Some t } ->
ty t
ty_of_dty t
| Tyvar { tvsymbol = tv } ->
Ty.ty_var tv
| Tyapp (s, tl) ->
Ty.ty_app s (List.map ty tl)
Ty.ty_app s (List.map ty_of_dty tl)
(** Typing terms and formulas *)
......@@ -442,9 +454,9 @@ let rec term env t = match t.dt_node with
assert (M.mem x env);
t_var (M.find x env)
| Tconst c ->
t_const c (ty t.dt_ty)
t_const c (ty_of_dty t.dt_ty)
| Tapp (s, tl) ->
t_app s (List.map (term env) tl) (ty t.dt_ty)
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| _ ->
assert false (* TODO *)
......@@ -461,7 +473,7 @@ and fmla env = function
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, x, t, f1) ->
(* TODO: shouldn't we localize this ident? *)
let v = create_vsymbol (id_fresh x) (ty t) in
let v = create_vsymbol (id_fresh x) (ty_of_dty t) in
let env = M.add x v env in
f_quant q [v] [] (fmla env f1)
| Fapp (s, tl) ->
......@@ -533,14 +545,38 @@ let add_types loc dl th =
Hashtbl.add tysymbols x (Some ts);
ts
in
M.iter (fun x _ -> ignore (visit x)) def;
let th' =
let tsl =
M.fold (fun x _ tsl -> let ts = visit x in (ts, Tabstract) :: tsl) def []
in
add_decl th (create_type tsl)
in
let decl d =
(match Hashtbl.find tysymbols d.td_ident.id with
| None -> assert false
| Some ts -> ts),
(match d.td_def with
| TDabstract | TDalias _ -> Tabstract
| TDalgebraic _ -> assert false (*TODO*))
let ts, th' = match Hashtbl.find tysymbols d.td_ident.id with
| None ->
assert false
| Some ts ->
let th' = create_denv th' in
let vars = th'.utyvars in
List.iter
(fun v ->
Hashtbl.add vars v.id_short (create_type_var ~user:true v))
ts.ts_args;
ts, th'
in
let d = match d.td_def with
| TDabstract | TDalias _ ->
Tabstract
| TDalgebraic cl ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let constructor (loc, id, pl) =
let param (_, t) = ty_of_dty (dty th' t) in
let tyl = List.map param pl in
create_fsymbol (id_user id.id id.id_loc) (tyl, ty) true
in
Talgebraic (List.map constructor cl)
in
ts, d
in
let dl = List.map decl dl in
add_decl th (create_type dl)
......@@ -560,7 +596,7 @@ let add_logics loc dl th =
let v = id_user id loc in
let denv = create_denv th in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty (dty denv t) in
let type_ty (_,t) = ty_of_dty (dty denv t) in
let pl = List.map type_ty d.ld_params in
match d.ld_type with
| None -> (* predicate *)
......
......@@ -31,6 +31,9 @@ let print_ident =
let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
print
let print_typevar fmt x =
fprintf fmt "'%a" print_ident x
let rec print_ty fmt ty = match ty.ty_node with
| Tyvar n ->
fprintf fmt "'%a" print_ident n
......@@ -49,12 +52,12 @@ let rec print_term fmt t = match t.t_node with
| Tconst _ ->
fprintf fmt "[const]"
| Tapp (s, tl) ->
fprintf fmt "(%a(%a@,)@ : %a@,@,)"
fprintf fmt "(%a(%a)@ : %a)"
print_ident s.fs_name (print_list comma print_term) tl
print_ty t.t_ty
| Tlet (t1,tbound) ->
let vs,t2 = t_open_bound tbound in
fprintf fmt "(let %a = %a in %a@,)"
fprintf fmt "(let %a = %a in@ %a)"
print_ident vs.vs_name print_term t1 print_term t2
| Tcase _ -> assert false (*TODO*)
| Teps _ -> assert false
......@@ -67,17 +70,17 @@ let print_tl fmt tl =
let rec print_fmla fmt f = match f.f_node with
| Fapp (s,tl) ->
fprintf fmt "(%a(%a@,)@,)"
fprintf fmt "(%a(%a))"
print_ident s.ps_name (print_list comma print_term) tl
| Fquant (q,fquant) ->
let vl,tl,f = f_open_quant fquant in
fprintf fmt "(%s %a %a.@ %a@,)"
fprintf fmt "(%s %a %a.@ %a)"
(match q with Fforall -> "forall" | Fexists -> "exists")
(print_list comma print_vs) vl print_tl tl print_fmla f
| Ftrue -> fprintf fmt "(true@,)"
| Ffalse -> fprintf fmt "(false@,)"
| Ftrue -> fprintf fmt "true"
| Ffalse -> fprintf fmt "false)"
| Fbinop (b,f1,f2) ->
fprintf fmt "(%a@ %s@ %a@,)"
fprintf fmt "(%a@ %s@ %a)"
print_fmla f1
(match b with
| Fand -> "and" | For -> "or"
......@@ -99,15 +102,15 @@ let print_psymbol fmt {ps_name = ps_name; ps_scheme = tyl} =
(print_list_paren comma print_ty) tyl
let print_ty_decl fmt (ts,tydef) = match tydef,ts.ts_def with
| Tabstract,None -> fprintf fmt "type %a%a@."
(print_list_paren comma print_ident) ts.ts_args
| Tabstract,None -> fprintf fmt "type %a %a"
(print_list_paren comma print_typevar) ts.ts_args
print_ident ts.ts_name
| Tabstract,Some f -> fprintf fmt "type %a%a =@ %a@."
(print_list_paren comma print_ident) ts.ts_args
| Tabstract,Some f -> fprintf fmt "type %a %a =@ %a"
(print_list_paren comma print_typevar) ts.ts_args
print_ident ts.ts_name
print_ty f
| Talgebraic d, None -> fprintf fmt "type %a%a =@ %a@."
(print_list_paren comma print_ident) ts.ts_args
| Talgebraic d, None -> fprintf fmt "type %a %a =@ %a"
(print_list_paren comma print_typevar) ts.ts_args
print_ident ts.ts_name
(print_list newline print_fsymbol) d
| Talgebraic _, Some _ -> assert false
......@@ -116,30 +119,32 @@ let print_vsymbol fmt {vs_name = vs_name; vs_ty = vs_ty} =
fprintf fmt "%a :@ %a" print_ident vs_name print_ty vs_ty
let print_logic_decl fmt = function
| Lfunction (fs,None) -> fprintf fmt "logic %a@." print_fsymbol fs
| Lfunction (fs,None) -> fprintf fmt "@[<hov 2>logic %a@]" print_fsymbol fs
| Lfunction (fs,Some fd) ->
fprintf fmt "logic %a :@ %a@." print_ident fs.fs_name
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident fs.fs_name
print_fmla fd
| Lpredicate (fs,None) -> fprintf fmt "logic %a@." print_psymbol fs
| Lpredicate (fs,None) -> fprintf fmt "@[<hov 2>logic %a@]" print_psymbol fs
| Lpredicate (ps,Some fd) ->
fprintf fmt "logic %a :@ %a@." print_ident ps.ps_name
fprintf fmt "@[<hov 2>logic %a :@ %a@]" print_ident ps.ps_name
print_fmla fd
| Linductive _ -> assert false (*TODO*)
let print_decl fmt d = match d.d_node with
| Dtype tl -> fprintf fmt "(* *)@.%a" (print_list newline print_ty_decl) tl
| Dlogic ldl -> fprintf fmt "(* *)@.%a"
| Dtype tl -> fprintf fmt "(* *)@\n%a" (print_list newline print_ty_decl) tl
| Dlogic ldl -> fprintf fmt "(* *)@\n%a"
(print_list newline print_logic_decl) ldl
| Dprop (k,id,fmla) ->
fprintf fmt "%s %a :@ %a@."
fprintf fmt "%s %a :@ %a@\n"
(match k with Paxiom -> "axiom" | Pgoal -> "goal" | Plemma -> "lemma")
print_ident id
print_fmla fmla
let print_decl_or_use fmt = function
| Decl d -> fprintf fmt "%a" print_decl d
| Use u -> fprintf fmt "use export %a@." print_ident u.th_name
| Use u -> fprintf fmt "use export %a@\n" print_ident u.th_name
let print_theory fmt t =
fprintf fmt "theory %a@.%aend@." print_ident t.th_name
(print_list newline print_decl_or_use) t.th_decls
fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name
(print_list newline print_decl_or_use) t.th_decls;
fprintf fmt "@?"
......@@ -2,7 +2,9 @@
(* test file *)
theory Test
logic id(x:'a) : 'a = x
type 'a list = Nil | Cons('a, 'a list)
type 'a tree = Leaf('a) | Node('a forest)
type 'a forest = 'a tree list
end
theory TestPrelude
......
......@@ -54,6 +54,7 @@ let semi fmt () = fprintf fmt ";@ "
let space fmt () = fprintf fmt " "
let alt fmt () = fprintf fmt "|@ "
let newline fmt () = fprintf fmt "@\n"
let newline2 fmt () = fprintf fmt "@\n@\n"
let arrow fmt () = fprintf fmt "@ -> "
let lbrace fmt () = fprintf fmt "{"
let rbrace fmt () = fprintf fmt "}"
......
......@@ -49,6 +49,7 @@ val print_pair :
val space : formatter -> unit -> unit
val alt : formatter -> unit -> unit
val newline : formatter -> unit -> unit
val newline2 : formatter -> unit -> unit
val comma : formatter -> unit -> unit
val simple_comma : formatter -> unit -> unit
val semi : formatter -> unit -> unit
......
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