Commit 2d3b47ba authored by Andrei Paskevich's avatar Andrei Paskevich

"Please, don't shoot, I can explain everything" commit

- unify Lfunction and Lpredicate (mucho bettar)
- separation of prop and fmla
- making prop and tvsymbol private aliases of ident
parent a20e5f3a
......@@ -25,7 +25,7 @@ open Ty
open Term
open Theory
let iprinter,tprinter,lprinter,cprinter,pprinter =
let iprinter,tprinter,lprinter,pprinter =
let bl = ["theory"; "type"; "logic"; "inductive";
"axiom"; "lemma"; "goal"; "use"; "clone";
"namespace"; "import"; "export"; "end";
......@@ -39,7 +39,6 @@ let iprinter,tprinter,lprinter,cprinter,pprinter =
create_ident_printer bl ~sanitizer:isanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:lsanitize,
create_ident_printer bl ~sanitizer:usanitize,
create_ident_printer bl ~sanitizer:usanitize
let thash = Hid.create 63
......@@ -50,7 +49,6 @@ let forget_all () =
forget_all iprinter;
forget_all tprinter;
forget_all lprinter;
forget_all cprinter;
forget_all pprinter;
Hid.clear thash;
Hid.clear lhash;
......@@ -60,9 +58,9 @@ let tv_set = ref Sid.empty
(* type variables always start with a quote *)
let print_tv fmt tv =
tv_set := Sid.add tv !tv_set;
tv_set := Sid.add (tv_name tv) !tv_set;
let sanitize n = "'" ^ n in
let n = id_unique iprinter ~sanitizer:sanitize tv in
let n = id_unique iprinter ~sanitizer:sanitize (tv_name tv) in
fprintf fmt "%s" n
let forget_tvs () =
......@@ -89,12 +87,15 @@ let print_ts fmt ts =
let print_ls fmt ls =
Hid.replace lhash ls.ls_name ls;
if ls.ls_constr then fprintf fmt "%s" (id_unique cprinter ls.ls_name)
else fprintf fmt "%s" (id_unique lprinter ls.ls_name)
let n = if ls.ls_constr
then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
else id_unique lprinter ls.ls_name
in
fprintf fmt "%s" n
let print_pr fmt pr =
Hid.replace phash pr.pr_name pr;
fprintf fmt "%s" (id_unique pprinter pr.pr_name)
Hid.replace phash (pr_name pr) pr;
fprintf fmt "%s" (id_unique pprinter (pr_name pr))
(** Types *)
......@@ -248,8 +249,8 @@ and print_tl fmt tl =
(print_list alt (print_list comma print_tr)) tl
and print_tr fmt = function
| TrTerm t -> print_term fmt t
| TrFmla f -> print_fmla fmt f
| Term t -> print_term fmt t
| Fmla f -> print_fmla fmt f
(** Declarations *)
......@@ -278,37 +279,30 @@ let print_type_decl fmt (ts,def) = match def with
let print_type_decl fmt d = print_type_decl fmt d; forget_tvs ()
let print_logic_decl fmt = function
| Lfunction (fs,None) ->
fprintf fmt "@[<hov 2>logic %a%a :@ %a@]"
print_ls fs (print_paren_l print_ty) fs.ls_args
print_ty (of_option fs.ls_value)
| Lpredicate (ps,None) ->
fprintf fmt "@[<hov 2>logic %a%a@]"
print_ls ps (print_paren_l print_ty) ps.ls_args
| Lfunction (fs,Some fd) ->
let _,vl,t = open_fs_defn fd in
fprintf fmt "@[<hov 2>logic %a%a :@ %a =@ %a@]"
print_ls fs (print_paren_l print_vsty) vl
print_ty t.t_ty print_term t;
List.iter forget_var vl
| Lpredicate (ps,Some fd) ->
let _,vl,f = open_ps_defn fd in
fprintf fmt "@[<hov 2>logic %a%a =@ %a@]"
print_ls ps (print_paren_l print_vsty) vl print_fmla f;
List.iter forget_var vl
let print_logic_decl fmt d = print_logic_decl fmt d; forget_tvs ()
let print_prop fmt pr =
fprintf fmt "%a : %a" print_pr pr print_fmla pr.pr_fmla
let print_ld fmt ld =
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t -> print_term fmt t
| Fmla f -> print_fmla fmt f
end;
List.iter forget_var vl
let print_ls_defn fmt = option_iter (fprintf fmt " =@ %a" print_ld)
let print_ls_type fmt = option_iter (fprintf fmt " :@ %a" print_ty)
let print_logic_decl fmt (ls,ld) =
fprintf fmt "@[<hov 2>logic %a%a%a%a@]"
print_ls ls (print_paren_l print_ty) ls.ls_args
print_ls_type ls.ls_value print_ls_defn ld;
forget_tvs ()
let print_ind fmt pr = fprintf fmt "@[<hov 4>| %a@]" print_prop pr
let print_ind fmt (pr,f) =
fprintf fmt "@[<hov 4>| %a : %a@]" print_pr pr print_fmla f
let print_ind_decl fmt (ps,bl) =
fprintf fmt "@[<hov 2>inductive %a%a =@ @[<hov>%a@]@]"
print_ls ps (print_paren_l print_ty) ps.ls_args
(print_list newline print_ind) bl;
print_ls ps (print_paren_l print_ty) ps.ls_args
(print_list newline print_ind) bl;
forget_tvs ()
let print_pkind fmt = function
......@@ -316,6 +310,11 @@ let print_pkind fmt = function
| Plemma -> fprintf fmt "lemma"
| Pgoal -> fprintf fmt "goal"
let print_prop_decl fmt (k,pr,f) =
fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
print_pr pr print_fmla f;
forget_tvs ()
let print_inst fmt (id1,id2) =
if Hid.mem thash id2 then
let n = id_unique tprinter id1 in
......@@ -332,9 +331,7 @@ let print_decl fmt d = match d.d_node with
| Dtype tl -> print_list newline print_type_decl fmt tl
| Dlogic ll -> print_list newline print_logic_decl fmt ll
| Dind il -> print_list newline print_ind_decl fmt il
| Dprop (k,pr) ->
fprintf fmt "@[<hov 2>%a %a@]" print_pkind k print_prop pr;
forget_tvs ()
| Dprop p -> print_prop_decl fmt p
| Duse th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Dclone (th,inst) ->
......
......@@ -42,12 +42,12 @@ val print_pat : formatter -> pattern -> unit (* pattern *)
val print_term : formatter -> term -> unit (* term *)
val print_fmla : formatter -> fmla -> unit (* formula *)
val print_pkind : formatter -> prop_kind -> unit
val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_decl -> unit
val print_pkind : formatter -> prop_kind -> unit
val print_prop : formatter -> prop -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_decls : formatter -> decl list -> unit
......
......@@ -164,7 +164,7 @@ exception PredicateSymbolExpected of lsymbol
let pat_app fs pl ty =
if not fs.ls_constr then raise (ConstructorExpected fs);
let s = match fs.ls_value with
| Some vty -> Ty.matching Mid.empty vty ty
| Some vty -> Ty.matching Mtv.empty vty ty
| None -> raise (FunctionSymbolExpected fs)
in
let mtch s ty p = Ty.matching s ty p.pat_ty in
......@@ -260,20 +260,20 @@ and term_branch = pattern * int * term
and fmla_branch = pattern * int * fmla
and trigger_elt =
| TrTerm of term
| TrFmla of fmla
and expr =
| Term of term
| Fmla of fmla
and trigger = trigger_elt list
and trigger = expr list
(* trigger traversal *)
let tr_map fnT fnF =
let fn = function TrTerm t -> TrTerm (fnT t) | TrFmla f -> TrFmla (fnF f) in
let fn = function Term t -> Term (fnT t) | Fmla f -> Fmla (fnF f) in
List.map (List.map fn)
let tr_fold fnT fnF =
let fn acc = function TrTerm t -> fnT acc t | TrFmla f -> fnF acc f in
let fn acc = function Term t -> fnT acc t | Fmla f -> fnF acc f in
List.fold_left (List.fold_left fn)
module T = struct
......@@ -344,8 +344,8 @@ module F = struct
let f_eq_bound (v1, f1) (v2, f2) = v1 == v2 && f1 == f2
let tr_eq tr1 tr2 = match tr1,tr2 with
| TrTerm t1, TrTerm t2 -> t1 == t2
| TrFmla f1, TrFmla f2 -> f1 == f2
| Term t1, Term t2 -> t1 == t2
| Fmla f1, Fmla f2 -> f1 == f2
| _ -> false
let f_eq_quant (vl1, n1, tl1, f1) (vl2, n2, tl2, f2) =
......@@ -391,7 +391,7 @@ module F = struct
let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag f.f_tag
let tr_hash = function TrTerm t -> t.t_tag | TrFmla f -> f.f_tag
let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
let f_hash_quant (vl, _, tl, f) =
let h = Hashcons.combine_list v_hash f.f_tag vl in
......@@ -560,7 +560,7 @@ let f_any_unsafe prT prF lvl f =
let t_app fs tl ty =
let s = match fs.ls_value with
| Some vty -> Ty.matching Mid.empty vty ty
| Some vty -> Ty.matching Mtv.empty vty ty
| _ -> raise (FunctionSymbolExpected fs)
in
let mtch s ty t = Ty.matching s ty t.t_ty in
......@@ -570,7 +570,7 @@ let t_app fs tl ty =
let f_app ps tl =
let s = match ps.ls_value with
| None -> Mid.empty
| None -> Mtv.empty
| _ -> raise (PredicateSymbolExpected ps)
in
let mtch s ty t = Ty.matching s ty t.t_ty in
......
......@@ -152,11 +152,11 @@ and term_branch
and fmla_branch
and trigger_elt =
| TrTerm of term
| TrFmla of fmla
and expr =
| Term of term
| Fmla of fmla
and trigger = trigger_elt list
and trigger = expr list
module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
......
This diff is collapsed.
......@@ -23,18 +23,14 @@ open Term
(** Named propositions *)
type prop = private {
pr_name : ident;
pr_fmla : fmla;
}
type prop
module Spr : Set.S with type elt = prop
module Mpr : Map.S with type key = prop
module Hpr : Hashtbl.S with type key = prop
val create_prop : preid -> fmla -> prop
val shortcut_for_discussion_dont_be_mad_andrei_please : ident -> fmla -> prop
val create_prop : preid -> prop
val pr_name : prop -> ident
(** Declarations *)
......@@ -48,25 +44,23 @@ type ty_decl = tysymbol * ty_def
(* logic declaration *)
type fs_defn
type ps_defn
type ls_defn
type logic_decl =
| Lfunction of lsymbol * fs_defn option
| Lpredicate of lsymbol * ps_defn option
type logic_decl = lsymbol * ls_defn option
val make_fs_defn : lsymbol -> vsymbol list -> term -> fs_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ps_defn
val make_ls_defn : lsymbol -> vsymbol list -> expr -> ls_defn
val make_fs_defn : lsymbol -> vsymbol list -> term -> ls_defn
val make_ps_defn : lsymbol -> vsymbol list -> fmla -> ls_defn
val open_fs_defn : fs_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ps_defn -> lsymbol * vsymbol list * fmla
val open_ls_defn : ls_defn -> lsymbol * vsymbol list * expr
val open_fs_defn : ls_defn -> lsymbol * vsymbol list * term
val open_ps_defn : ls_defn -> lsymbol * vsymbol list * fmla
val fs_defn_axiom : fs_defn -> fmla
val ps_defn_axiom : ps_defn -> fmla
val ls_defn_axiom : ls_defn -> fmla
(* inductive predicate declaration *)
type ind_decl = lsymbol * prop list
type ind_decl = lsymbol * (prop * fmla) list
(* proposition declaration *)
......@@ -75,7 +69,7 @@ type prop_kind =
| Plemma
| Pgoal
type prop_decl = prop_kind * prop
type prop_decl = prop_kind * prop * fmla
(** Context and Theory *)
......@@ -125,9 +119,7 @@ and decl_node =
val create_ty_decl : ty_decl list -> decl
val create_logic_decl : logic_decl list -> decl
val create_ind_decl : ind_decl list -> decl
val create_prop_decl : prop_kind -> prop -> decl
val prop_decl_of_fmla : prop_kind -> preid -> fmla -> decl
val create_prop_decl : prop_kind -> prop -> fmla -> decl
(* separate independent groups of declarations *)
......@@ -139,11 +131,11 @@ val create_ind_decls : ind_decl list -> decl list
exception ConstructorExpected of lsymbol
exception IllegalTypeAlias of tysymbol
exception UnboundTypeVar of ident
exception UnboundTypeVar of tvsymbol
exception InvalidIndDecl of ident * ident
exception TooSpecificIndDecl of ident * ident * term
exception NonPositiveIndDecl of ident * ident * lsymbol
exception InvalidIndDecl of lsymbol * prop
exception TooSpecificIndDecl of lsymbol * prop * term
exception NonPositiveIndDecl of lsymbol * prop * lsymbol
exception IllegalConstructor of lsymbol
exception BadLogicDecl of ident
......
......@@ -24,6 +24,13 @@ open Ident
type tvsymbol = ident
module Stv = Sid
module Mtv = Mid
module Htv = Hid
let create_tvsymbol = id_register
let tv_name v = v
(* type symbols and types *)
type tysymbol = {
......@@ -58,7 +65,6 @@ let mk_ts name args def = {
ts_def = def;
}
let create_tvsymbol = id_register
let create_tysymbol name args def = mk_ts (id_register name) args def
module Ty = struct
......@@ -107,15 +113,15 @@ exception NonLinear
exception UnboundTypeVariable
let rec tv_known vs ty = match ty.ty_node with
| Tyvar n -> Sid.mem n vs
| Tyvar n -> Stv.mem n vs
| _ -> ty_all (tv_known vs) ty
let create_tysymbol name args def =
let add s v =
if Sid.mem v s then raise NonLinear;
Sid.add v s
if Stv.mem v s then raise NonLinear;
Stv.add v s
in
let s = List.fold_left add Sid.empty args in
let s = List.fold_left add Stv.empty args in
let _ = match def with
| Some ty -> tv_known s ty || raise UnboundTypeVariable
| _ -> true
......@@ -125,15 +131,15 @@ let create_tysymbol name args def =
exception BadTypeArity
let rec tv_inst m ty = match ty.ty_node with
| Tyvar n -> Mid.find n m
| Tyvar n -> Mtv.find n m
| _ -> ty_map (tv_inst m) ty
let ty_app s tl =
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
let add m v t = Mtv.add v t m in
tv_inst (List.fold_left2 add Mtv.empty s.ts_args tl) ty
| _ ->
ty_app s tl
......@@ -161,8 +167,8 @@ let rec matching s ty1 ty2 =
if ty1 == ty2 then s
else match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ ->
(try if Mid.find n1 s == ty2 then s else raise TypeMismatch
with Not_found -> Mid.add n1 ty2 s)
(try if Mtv.find n1 s == ty2 then s else raise TypeMismatch
with Not_found -> Mtv.add n1 ty2 s)
| Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
List.fold_left2 matching s l1 l2
| _ ->
......
......@@ -21,7 +21,14 @@ open Ident
(** Types *)
type tvsymbol = ident
type tvsymbol
module Stv : Set.S with type elt = tvsymbol
module Mtv : Map.S with type key = tvsymbol
module Htv : Hashtbl.S with type key = tvsymbol
val create_tvsymbol : preid -> tvsymbol
val tv_name : tvsymbol -> ident
(* type symbols and types *)
......@@ -40,17 +47,15 @@ and ty_node = private
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
exception NonLinear
exception UnboundTypeVariable
val create_tvsymbol : preid -> tvsymbol
val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
module Hts : Hashtbl.S with type key = tysymbol
exception BadTypeArity
exception NonLinear
exception UnboundTypeVariable
val create_tysymbol : preid -> tvsymbol list -> ty option -> tysymbol
val ty_var : tvsymbol -> ty
val ty_app : tysymbol -> ty list -> ty
......@@ -67,8 +72,8 @@ val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch
val matching : ty Mid.t -> ty -> ty -> ty Mid.t
val ty_match : ty -> ty -> ty Mid.t -> ty Mid.t option
val matching : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ty_match : ty -> ty -> ty Mtv.t -> ty Mtv.t option
(* built-in symbols *)
......
......@@ -188,8 +188,7 @@ let do_file env drv filename_printer file =
let goals = extract_goals env drv [] th in
List.filter (fun (_,ctxt) ->
match ctxt.ctxt_decl.d_node with
| Dprop (_,{pr_name = pr_name}) ->
Ident.id_derived_from pr_name pr.pr_name
| Dprop (_,pr',_) -> pr == pr'
| _ -> assert false) goals in
(* Apply transformations *)
let goals = List.map
......@@ -202,7 +201,7 @@ let do_file env drv filename_printer file =
let res = Driver.call_prover ~debug:!debug ?timeout drv ctxt in
printf "%s %s %s : %a@."
file th.th_name.Ident.id_short
(goal_of_ctxt ctxt).pr_name.Ident.id_long
(pr_name (goal_of_ctxt ctxt)).Ident.id_long
Call_provers.print_prover_result res in
List.iter call goals
| Some dir (* we are in the output mode *) ->
......
......@@ -36,7 +36,7 @@ let forget_var v = forget_id ident_printer v.vs_name
let rec print_type drv fmt ty = match ty.ty_node with
| Tyvar id ->
fprintf fmt "'%a" print_ident id
fprintf fmt "'%a" print_ident (tv_name id)
| Tyapp (ts, tl) ->
match Driver.query_ident drv ts.ts_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
......@@ -129,8 +129,8 @@ let rec print_fmla drv fmt f = match f.f_node with
assert false
and print_trigger drv fmt = function
| TrTerm t -> (print_term drv) fmt t
| TrFmla f -> (print_fmla drv) fmt f
| Term t -> (print_term drv) fmt t
| Fmla f -> (print_fmla drv) fmt f
and print_triggers drv fmt tl = print_list comma (print_trigger drv) fmt tl
......@@ -150,63 +150,68 @@ let print_type_decl drv fmt = function
let ac_th = ["algebra";"AC"]
let print_logic_decl drv ctxt fmt = function
| Lfunction (ls, def) ->
begin
match Driver.query_ident drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag s ->
let print_ld drv fmt ld =
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t -> print_term drv fmt t
| Fmla f -> print_fmla drv fmt f
end;
List.iter forget_var vl
let print_ls_defn drv fmt =
Util.option_iter (fprintf fmt " =@ %a" (print_ld drv))
let print_ls_type drv fmt = function
| Some ty -> print_type drv fmt ty
| None -> fprintf fmt "prop"
let print_logic_decl drv ctxt fmt (ls,ld) =
match Driver.query_ident drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag s ->
begin match ld with
| None ->
let sac = if Snm.mem "AC" s then "ac " else "" in
let ty = match ls.ls_value with None -> assert false | Some ty -> ty in
match def with
| None ->
let tyl = ls.ls_args in
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
sac
print_ident ls.ls_name
(print_list comma (print_type drv)) tyl (print_type drv) ty;
true
| Some defn ->
let id = ls.ls_name in
let _, vl, t = open_fs_defn defn in
fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n"
sac print_ident ls.ls_name
(print_list comma (print_type drv)) ls.ls_args
(print_ls_type drv) ls.ls_value
| Some ld ->
let _,vl,e = open_ls_defn ld in
begin match e with
| Term t ->
(* TODO AC? *)
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id
(print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t;
List.iter forget_var vl;true
end
| Lpredicate (ls, def) ->
begin
match Driver.query_ident drv ls.ls_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag _ ->
match def with
| None ->
fprintf fmt "@[<hov 2>logic %a : %a -> prop@]"
print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args;
true
| Some fd ->
let _,vl,f = open_ps_defn fd in
fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl
(print_type drv) (Util.of_option ls.ls_value)
(print_term drv) t
| Fmla f ->
fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]"
print_ident ls.ls_name
(print_list comma (print_logic_binder drv)) vl (print_fmla drv) f;
List.iter forget_var vl;true
end
(print_list comma (print_logic_binder drv)) vl
(print_fmla drv) f
end;
List.iter forget_var vl
end;
true
let print_decl drv ctxt fmt d = match d.d_node with
| Dtype dl ->
print_list_opt newline (print_type_decl drv) fmt dl
| Dlogic dl ->
print_list_opt newline (print_logic_decl drv ctxt) fmt dl
| Dind _ -> assert false (* TODO *)
| Dprop (Paxiom, pr) when
Driver.query_ident drv pr.pr_name = Driver.Remove -> false
| Dprop (Paxiom, pr) ->
| Dprop (Paxiom, pr, _) when
Driver.query_ident drv (pr_name pr) = Driver.Remove -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
| Dprop (Pgoal, pr) ->
print_ident (pr_name pr) (print_fmla drv) f; true
| Dprop (Pgoal, pr, f) ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true
| Dprop (Plemma, _) ->
print_ident (pr_name pr) (print_fmla drv) f; true
| Dprop (Plemma, _, _) ->
assert false
| Duse _ | Dclone _ -> false
......
......@@ -233,7 +233,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rremove (c,(loc,q)) ->
begin
try
add_htheory c (Transform.find_pr th.th_export q).pr_name Remove
add_htheory c (pr_name (Transform.find_pr th.th_export q)) Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
(string_of_qualid qualid q)
end
......@@ -274,7 +274,7 @@ let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagpr (c,(loc,q),s) ->
begin
try
add_htheory c (Transform.find_pr th.th_export q).pr_name
add_htheory c (pr_name (Transform