Commit c64827ba authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Typing terms using namespace and known map

parent 3a4ee4f1
......@@ -88,12 +88,6 @@ let find_psymbol_ns ns q =
if ls.ls_value = None then ls else
Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
let find_prop uc q = find_prop_ns (get_namespace uc) q
let find_tysymbol uc q = find_tysymbol_ns (get_namespace uc) q
let find_lsymbol uc q = find_lsymbol_ns (get_namespace uc) q
let find_fsymbol uc q = find_fsymbol_ns (get_namespace uc) q
let find_psymbol uc q = find_psymbol_ns (get_namespace uc) q
let find_namespace_ns ns q =
find_qualid (fun _ -> Glob.dummy_id) ns_find_ns ns q
......@@ -107,7 +101,7 @@ let ty_of_pty ?(noop=true) uc pty =
| PTtyvar ({id_str = x}, _) ->
ty_var (tv_of_string x)
| PTtyapp (q, tyl) ->
let ts = find_tysymbol uc q in
let ts = find_tysymbol_ns uc q in
let tyl = List.map get_ty tyl in
Loc.try2 ~loc:(qloc q) ty_app ts tyl
| PTtuple tyl ->
......@@ -155,36 +149,36 @@ let create_user_id {id_str = n; id_lab = label; id_loc = loc} =
let label,loc = List.fold_left get_labels (Slab.empty,loc) label in
id_user ~label n loc
let parse_record ~loc uc get_val fl =
let fl = List.map (fun (q,e) -> find_lsymbol uc q, e) fl in
let cs,pjl,flm = Loc.try2 ~loc parse_record (get_known uc) fl in
let parse_record ~loc ns km get_val fl =
let fl = List.map (fun (q,e) -> find_lsymbol_ns ns q, e) fl in
let cs,pjl,flm = Loc.try2 ~loc parse_record km fl in
let get_val pj = get_val cs pj (Mls.find_opt pj flm) in
cs, List.map get_val pjl
let rec dpattern uc { pat_desc = desc; pat_loc = loc } =
let rec dpattern ns km { pat_desc = desc; pat_loc = loc } =
Dterm.dpattern ~loc (match desc with
| Ptree.Pwild -> DPwild
| Ptree.Pvar x -> DPvar (create_user_id x)
| Ptree.Papp (q,pl) ->
let pl = List.map (dpattern uc) pl in
DPapp (find_lsymbol uc q, pl)
let pl = List.map (dpattern ns km) pl in
DPapp (find_lsymbol_ns ns q, pl)
| Ptree.Ptuple pl ->
let pl = List.map (dpattern uc) pl in
let pl = List.map (dpattern ns km) pl in
DPapp (fs_tuple (List.length pl), pl)
| Ptree.Prec fl ->
let get_val _ _ = function
| Some p -> dpattern uc p
| Some p -> dpattern ns km p
| None -> Dterm.dpattern DPwild in
let cs,fl = parse_record ~loc uc get_val fl in
let cs,fl = parse_record ~loc ns km get_val fl in
DPapp (cs,fl)
| Ptree.Pas (p, x) -> DPas (dpattern uc p, create_user_id x)
| Ptree.Por (p, q) -> DPor (dpattern uc p, dpattern uc q)
| Ptree.Pcast (p, ty) -> DPcast (dpattern uc p, ty_of_pty uc ty))
| Ptree.Pas (p, x) -> DPas (dpattern ns km p, create_user_id x)
| Ptree.Por (p, q) -> DPor (dpattern ns km p, dpattern ns km q)
| Ptree.Pcast (p, ty) -> DPcast (dpattern ns km p, ty_of_pty ns ty))
let quant_var uc (loc, id, gh, ty) =
let quant_var ns (loc, id, gh, ty) =
assert (not gh);
let ty = match ty with
| Some ty -> dty_of_ty (ty_of_pty uc ty)
| Some ty -> dty_of_ty (ty_of_pty ns ty)
| None -> dty_fresh () in
Opt.map create_user_id id, ty, Some loc
......@@ -202,10 +196,10 @@ let mk_var n dt =
let mk_let ~loc n dt node =
DTlet (dt, id_user n loc, Dterm.dterm ~loc node)
let chainable_op uc op =
let chainable_op ns op =
(* non-bool -> non-bool -> bool *)
op.id_str = "infix =" || op.id_str = "infix <>" ||
match find_lsymbol uc (Qident op) with
match find_lsymbol_ns ns (Qident op) with
| {ls_args = [ty1;ty2]; ls_value = ty} ->
Opt.fold (fun _ ty -> ty_equal ty ty_bool) true ty
&& not (ty_equal ty1 ty_bool)
......@@ -222,7 +216,7 @@ let mk_closure loc ls =
let vl = Lists.mapi mk_v ls.ls_args in
DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
let rec dterm ns km gvars denv {term_desc = desc; term_loc = loc} =
let func_app e el =
List.fold_left (fun e1 (loc, e2) ->
DTfapp (Dterm.dterm ~loc e1, e2)) e el
......@@ -235,7 +229,7 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
let qualid_app q el = match gvars q with
| Some vs -> func_app (DTgvar vs) el
| None ->
let ls = find_lsymbol uc q in
let ls = find_lsymbol_ns ns q in
apply_ls (qloc q) ls [] ls.ls_args el
in
let qualid_app q el = match q with
......@@ -247,32 +241,32 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
in
let rec unfold_app e1 e2 el = match e1.term_desc with
| Tapply (e11,e12) ->
let e12 = dterm uc gvars denv e12 in
let e12 = dterm ns km gvars denv e12 in
unfold_app e11 e12 ((e1.term_loc, e2)::el)
| Tident q ->
qualid_app q ((e1.term_loc, e2)::el)
| _ ->
func_app (DTfapp (dterm uc gvars denv e1, e2)) el
func_app (DTfapp (dterm ns km gvars denv e1, e2)) el
in
Dterm.dterm ~loc (match desc with
| Ptree.Tident q ->
qualid_app q []
| Ptree.Tidapp (q, tl) ->
let tl = List.map (dterm uc gvars denv) tl in
DTapp (find_lsymbol uc q, tl)
let tl = List.map (dterm ns km gvars denv) tl in
DTapp (find_lsymbol_ns ns q, tl)
| Ptree.Tapply (e1, e2) ->
unfold_app e1 (dterm uc gvars denv e2) []
unfold_app e1 (dterm ns km gvars denv e2) []
| Ptree.Ttuple tl ->
let tl = List.map (dterm uc gvars denv) tl in
let tl = List.map (dterm ns km gvars denv) tl in
DTapp (fs_tuple (List.length tl), tl)
| Ptree.Tinfix (e12, op2, e3)
| Ptree.Tinnfix (e12, op2, e3) ->
let make_app de1 op de2 = if op.id_str = "infix <>" then
let op = { op with id_str = "infix =" } in
let ls = find_lsymbol uc (Qident op) in
let ls = find_lsymbol_ns ns (Qident op) in
DTnot (Dterm.dterm ~loc (DTapp (ls, [de1;de2])))
else
DTapp (find_lsymbol uc (Qident op), [de1;de2])
DTapp (find_lsymbol_ns ns (Qident op), [de1;de2])
in
let rec make_chain de1 = function
| [op,de2] ->
......@@ -283,42 +277,42 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
DTbinop (DTand, de12, de23)
| [] -> assert false in
let rec get_chain e12 acc = match e12.term_desc with
| Tinfix (e1, op1, e2) when chainable_op uc op1 ->
get_chain e1 ((op1, dterm uc gvars denv e2) :: acc)
| Tinfix (e1, op1, e2) when chainable_op ns op1 ->
get_chain e1 ((op1, dterm ns km gvars denv e2) :: acc)
| _ -> e12, acc in
let ch = [op2, dterm uc gvars denv e3] in
let e1, ch = if chainable_op uc op2
let ch = [op2, dterm ns km gvars denv e3] in
let e1, ch = if chainable_op ns op2
then get_chain e12 ch else e12, ch in
make_chain (dterm uc gvars denv e1) ch
make_chain (dterm ns km gvars denv e1) ch
| Ptree.Tconst c ->
DTconst c
| Ptree.Tlet (x, e1, e2) ->
let id = create_user_id x in
let e1 = dterm uc gvars denv e1 in
let e1 = dterm ns km gvars denv e1 in
let denv = denv_add_let denv e1 id in
let e2 = dterm uc gvars denv e2 in
let e2 = dterm ns km gvars denv e2 in
DTlet (e1, id, e2)
| Ptree.Tmatch (e1, bl) ->
let e1 = dterm uc gvars denv e1 in
let e1 = dterm ns km gvars denv e1 in
let branch (p, e) =
let p = dpattern uc p in
let p = dpattern ns km p in
let denv = denv_add_pat denv p in
p, dterm uc gvars denv e in
p, dterm ns km gvars denv e in
DTcase (e1, List.map branch bl)
| Ptree.Tif (e1, e2, e3) ->
let e1 = dterm uc gvars denv e1 in
let e2 = dterm uc gvars denv e2 in
let e3 = dterm uc gvars denv e3 in
let e1 = dterm ns km gvars denv e1 in
let e2 = dterm ns km gvars denv e2 in
let e3 = dterm ns km gvars denv e3 in
DTif (e1, e2, e3)
| Ptree.Ttrue ->
DTtrue
| Ptree.Tfalse ->
DTfalse
| Ptree.Tunop (Ptree.Tnot, e1) ->
DTnot (dterm uc gvars denv e1)
DTnot (dterm ns km gvars denv e1)
| Ptree.Tbinop (e1, op, e2) ->
let e1 = dterm uc gvars denv e1 in
let e2 = dterm uc gvars denv e2 in
let e1 = dterm ns km gvars denv e1 in
let e2 = dterm ns km gvars denv e2 in
let k op = DTbinop (op, e1, e2) in
let et () =
let loc = e2.dt_loc in
......@@ -335,9 +329,9 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
| Ptree.Tso -> DTbinop (DTand, e1, et ())
end
| Ptree.Tquant (q, uqu, trl, e1) ->
let qvl = List.map (quant_var uc) uqu in
let qvl = List.map (quant_var ns) uqu in
let denv = denv_add_quant denv qvl in
let dterm e = dterm uc gvars denv e in
let dterm e = dterm ns km gvars denv e in
let trl = List.map (List.map dterm) trl in
let e1 = dterm e1 in
let q = match q with
......@@ -347,39 +341,57 @@ let rec dterm uc gvars denv {term_desc = desc; term_loc = loc} =
DTquant (q, qvl, trl, e1)
| Ptree.Trecord fl ->
let get_val cs pj = function
| Some e -> dterm uc gvars denv e
| Some e -> dterm ns km gvars denv e
| None -> Loc.error ~loc (RecordFieldMissing (cs,pj)) in
let cs, fl = parse_record ~loc uc get_val fl in
let cs, fl = parse_record ~loc ns km get_val fl in
DTapp (cs, fl)
| Ptree.Tupdate (e1, fl) ->
let e1 = dterm uc gvars denv e1 in
let e1 = dterm ns km gvars denv e1 in
let re = is_reusable e1 in
let v = if re then e1 else mk_var "_q " e1 in
let get_val _ pj = function
| Some e -> dterm uc gvars denv e
| Some e -> dterm ns km gvars denv e
| None -> Dterm.dterm ~loc (DTapp (pj,[v])) in
let cs, fl = parse_record ~loc uc get_val fl in
let cs, fl = parse_record ~loc ns km get_val fl in
let d = DTapp (cs, fl) in
if re then d else mk_let ~loc "_q " e1 d
| Ptree.Tnamed (Lpos uloc, e1) ->
DTuloc (dterm uc gvars denv e1, uloc)
DTuloc (dterm ns km gvars denv e1, uloc)
| Ptree.Tnamed (Lstr lab, e1) ->
DTlabel (dterm uc gvars denv e1, Slab.singleton lab)
DTlabel (dterm ns km gvars denv e1, Slab.singleton lab)
| Ptree.Tcast (e1, ty) ->
DTcast (dterm uc gvars denv e1, ty_of_pty uc ty))
DTcast (dterm ns km gvars denv e1, ty_of_pty ns ty))
(** Export for program parsing *)
let type_term uc gvars t =
let t = dterm uc gvars denv_empty t in
let type_term_in_namespace ns km gvars t =
let t = dterm ns km gvars denv_empty t in
Dterm.term ~strict:true ~keep_loc:true t
let type_fmla uc gvars f =
let f = dterm uc gvars denv_empty f in
let type_term uc =
type_term_in_namespace (get_namespace uc) (get_known uc)
let type_fmla_in_namespace ns km gvars f =
let f = dterm ns km gvars denv_empty f in
Dterm.fmla ~strict:true ~keep_loc:true f
let type_fmla uc =
type_fmla_in_namespace (get_namespace uc) (get_known uc)
(** Typing declarations *)
let find_prop uc q = find_prop_ns (get_namespace uc) q
let find_tysymbol uc q = find_tysymbol_ns (get_namespace uc) q
(*
let find_lsymbol uc q = find_lsymbol_ns (get_namespace uc) q
*)
let find_fsymbol uc q = find_fsymbol_ns (get_namespace uc) q
let find_psymbol uc q = find_psymbol_ns (get_namespace uc) q
let ty_of_pty ?noop uc = ty_of_pty ?noop (get_namespace uc)
let dterm uc = dterm (get_namespace uc) (get_known uc)
let tyl_of_params ?(noop=false) uc pl =
let ty_of_param (loc,_,gh,ty) =
if gh then Loc.errorm ~loc
......
......@@ -51,10 +51,12 @@ val find_qualid :
type global_vs = Ptree.qualid -> vsymbol option
val type_term_in_namespace : namespace -> global_vs -> Ptree.term -> term
val type_term_in_namespace : namespace -> Decl.known_map -> global_vs -> Ptree.term -> term
val type_term : theory_uc -> global_vs -> Ptree.term -> term
val type_fmla_in_namespace : namespace -> Decl.known_map -> global_vs -> Ptree.term -> term
val type_fmla : theory_uc -> global_vs -> Ptree.term -> term
val type_inst : theory_uc -> theory -> Ptree.clone_subst list -> th_inst
......@@ -22,11 +22,7 @@ open Theory
open Args_wrapper
let id_unique tables id =
try
Mid.find id tables.unique_names
with Not_found ->
id_unique tables.printer id
let id_unique tables id = id_unique tables.printer id
(*
let forget_tvs () =
......
......@@ -12,15 +12,17 @@ let fresh_printer =
"namespace"; "import"; "export"; "end";
"forall"; "exists"; "not"; "true"; "false"; "if"; "then"; "else";
"let"; "in"; "match"; "with"; "as"; "epsilon" ] in
(*
let isanitize = sanitizer char_to_alpha char_to_alnumus in
fun () -> create_ident_printer bl ~sanitizer:isanitize
*)
fun () -> create_ident_printer bl (* ~sanitizer:isanitize *)
open Stdlib
type name_tables = {
namespace : namespace;
unique_names : string Mid.t;
known_map : known_map;
printer : ident_printer;
}
......@@ -36,16 +38,15 @@ let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
| Ts ty ->
{tables with
namespace = {tables.namespace with ns_ts = Mstr.add s ty tables.namespace.ns_ts};
unique_names = Mid.add ty.ts_name s tables.unique_names;
}
| Ls ls ->
{tables with
namespace = {tables.namespace with ns_ls = Mstr.add s ls tables.namespace.ns_ls};
unique_names = Mid.add ls.ls_name s tables.unique_names}
}
| Pr pr ->
{tables with
namespace = {tables.namespace with ns_pr = Mstr.add s pr tables.namespace.ns_pr};
unique_names = Mid.add pr.pr_name s tables.unique_names}
}
(* Adds symbols that are introduced to a constructor *)
let constructor_add (cl: constructor list) tables : name_tables =
......@@ -140,9 +141,15 @@ let build_name_tables task : name_tables =
*)
let pr = fresh_printer () in
let tables = {
namespace = empty_ns; unique_names = Mid.empty ; printer = pr } in
let km = Task.task_known task in
let tables = {
namespace = empty_ns;
known_map = km;
(*
unique_names = Mid.empty ;
*)
printer = pr;
} in
Mid.fold
(fun _id d tables ->
(* TODO optimization. We may check if id is already there to not explore twice the same
......@@ -158,22 +165,28 @@ let build_name_tables task : name_tables =
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
(*
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
*)
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tprsymbol : 'a trans_typ -> (Decl.prsymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (term -> 'a) trans_typ
let find_pr s task =
let tables = build_name_tables task in
Mstr.find s tables.namespace.ns_pr
let type_ptree ~as_fmla t task =
(* Simply build th_uc at the same time by rebuilding the declarations with unique names ??? *)
let tables = build_name_tables task in
failwith "todo"
(* let th_uc = tables.th in
let km = tables.known_map in
let ns = tables.namespace in
if as_fmla
then Typing.type_fmla th_uc (fun _ -> None) t
else Typing.type_term th_uc (fun _ -> None) t
*)
then Typing.type_fmla_in_namespace ns km (fun _ -> None) t
else Typing.type_term_in_namespace ns km (fun _ -> None) t
(*
(*** term argument parsed in the context of the task ***)
let type_ptree ~as_fmla t task =
let used_ths = Task.used_theories task in
......@@ -210,6 +223,7 @@ let type_ptree ~as_fmla t task =
if as_fmla
then Typing.type_fmla th_uc (fun _ -> None) t
else Typing.type_term th_uc (fun _ -> None) t
*)
let parse_and_type ~as_fmla s task =
let lb = Lexing.from_string s in
......@@ -235,12 +249,14 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
with Failure _ -> raise (Failure "Parsing error: expecting an integer."))
| _ -> failwith "Missing argument: expecting an integer."
end
(*
| Tstring t' ->
begin
match l with
| s :: tail -> wrap t' (f s) tail task
| _ -> failwith "Missing argument: expecting a string."
end
*)
| Tformula t' ->
begin
match l with
......@@ -273,3 +289,11 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
wrap t' (f tys) tail task
| _ -> failwith "Missing argument: expecting a type symbol."
end
| Tprsymbol t' ->
begin
match l with
| s :: tail ->
let pr = find_pr s task in
wrap t' (f pr) tail task
| _ -> failwith "Missing argument: expecting a prop symbol."
end
open Ident
open Theory
open Task
(** Pre-processing of tasks, to build unique names for all declared
......@@ -8,7 +7,7 @@ open Task
type name_tables = {
namespace : Theory.namespace;
unique_names : string Mid.t;
known_map : Decl.known_map;
printer : ident_printer;
}
......@@ -17,9 +16,12 @@ val build_name_tables : Task.task -> name_tables
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
(*
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
*)
| Tty : 'a trans_typ -> (Ty.ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (Ty.tysymbol -> 'a) trans_typ
| Tprsymbol : 'a trans_typ -> (Decl.prsymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (Term.term -> 'a) trans_typ
......
......@@ -9,17 +9,21 @@ open Args_wrapper
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
(* TODO ugly ! Solve it an other way *)
let clean_environment task =
let clean_environment _task =
(*
let _ = Pretty.forget_all in
let _ = Pretty.print_task Format.str_formatter task in
*)
()
let gen_ident s = Ident.id_fresh (Pretty.ppunique s)
let gen_ident = Ident.id_fresh
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t task =
(*
clean_environment task;
*)
let h = Decl.create_prsymbol (gen_ident "h") in
let hnot = Decl.create_prsymbol (gen_ident "hnot") in
let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
......@@ -76,18 +80,12 @@ let exists x task =
[Task.add_decl task new_goal]
| _ -> failwith "No goal"
(* TODO ask to have functions in ident and Pretty that do something like that *)
let string_pr pr =
ignore (Format.flush_str_formatter ());
Pretty.print_pr Format.str_formatter pr;
Format.flush_str_formatter()
(* Return a new task with hypothesis name removed *)
let remove_task_decl (name: string) : task trans =
let remove_task_decl (name: Ident.ident) : task trans =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (Paxiom, pr, _) when (string_pr pr = name) ->
| Dprop (Paxiom, pr, _) when (Ident.id_equal pr.pr_name name) ->
[]
| _ -> [d])
None
......@@ -98,7 +96,7 @@ let remove_task_decl (name: string) : task trans =
(* from task [delta, name:A |- G] build the task [delta |- G] *)
let remove name task =
clean_environment task;
[Trans.apply (remove_task_decl name) task]
[Trans.apply (remove_task_decl name.pr_name) task]
let pr_prsymbol pr =
......@@ -107,26 +105,28 @@ let pr_prsymbol pr =
| _ -> None
(* Looks for the hypothesis name and return it. If not found return None *)
let find_hypothesis name task =
let find_hypothesis (name:Ident.ident) task =
let ndecl = ref None in
let _ = task_iter (fun x -> if (
match (pr_prsymbol x.td_node) with
| None -> false
| Some pr -> string_pr pr = name) then ndecl := Some x) task in
| Some pr -> Ident.id_equal pr.pr_name name) then ndecl := Some x) task in
!ndecl
(* from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let instantiate name t task =
let instantiate (pr:Decl.prsymbol) t task =
let name = pr.pr_name in
clean_environment task;
let g, task = Task.task_separate_goal task in
let ndecl = find_hypothesis name task in
match ndecl with
| None -> Format.printf "Hypothesis %s not found@." name; [Task.add_tdecl task g]
| None -> Format.printf "Hypothesis %s not found@." name.Ident.id_string;
[Task.add_tdecl task g]
| Some decl -> (match decl.td_node with
| Decl {d_node = Dprop (pk, _pr, ht)} ->
let t_subst = subst_forall ht t in
let new_pr = create_prsymbol (gen_ident name) in
let new_pr = create_prsymbol (Ident.id_clone name) in
let new_decl = create_prop_decl pk new_pr t_subst in
let task = add_decl task new_decl in
[Task.add_tdecl task g]
......@@ -187,7 +187,8 @@ let term_decl d =
(* from task [delta, name:forall x.A->B |- G,
build the task [delta,name:forall x.A->B] |- A[x -> t]] ou t est tel que B[x->t] = G *)
let apply name task =
let apply pr task =
let name = pr.pr_name in
clean_environment task;
let g, task = Task.task_separate_goal task in
let tg = term_decl g in
......@@ -225,8 +226,8 @@ let apply name task =
let () = register_transform_with_args ~desc:"test case" "case" (wrap (Tformula Ttrans) case)
let () = register_transform_with_args ~desc:"test cut" "cut" (wrap (Tformula Ttrans) cut)
let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tstring Ttrans) remove)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tprsymbol Ttrans) remove)
let () = register_transform_with_args ~desc:"test instantiate" "instantiate"
(wrap (Tstring (Tterm Ttrans)) instantiate)
let () = register_transform_with_args ~desc:"test apply" "apply" (wrap (Tstring Ttrans) apply)
(wrap (Tprsymbol (Tterm Ttrans)) instantiate)
let () = register_transform_with_args ~desc:"test apply" "apply" (wrap (Tprsymbol Ttrans) apply)
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" (wrap (Tint Ttrans) dup)
......@@ -491,7 +491,7 @@ let test_transform_and_display fmt args =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status;
match status with
| TSdone tid -> (ignore (move_to_goal_ret next_node);
| TSdone _tid -> (ignore (move_to_goal_ret next_node);
test_print_goal fmt [])
| _ -> ()
in
......
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