Commit 95902ecd authored by MARCHE Claude's avatar MARCHE Claude

test detect poly

parent 4ef014e7
...@@ -107,7 +107,11 @@ val task_decls : task -> decl list ...@@ -107,7 +107,11 @@ val task_decls : task -> decl list
val task_goal : task -> prsymbol val task_goal : task -> prsymbol
val task_goal_fmla : task -> term val task_goal_fmla : task -> term
val task_separate_goal : task -> tdecl * task val task_separate_goal : task -> tdecl * task
(** [task_separate_goal t] returns a pair [(g,t')] where [g] is the
goal of the task [t] and [t'] is the rest. raises [GoalNotFound]
if task [t] has no goal *)
(** {2 selectors} *) (** {2 selectors} *)
...@@ -131,4 +135,3 @@ exception GoalNotFound ...@@ -131,4 +135,3 @@ exception GoalNotFound
exception GoalFound exception GoalFound
exception SkipFound exception SkipFound
exception LemmaFound exception LemmaFound
...@@ -14,29 +14,54 @@ open Theory ...@@ -14,29 +14,54 @@ open Theory
open Task open Task
let meta_monomorphic_types_only = let meta_monomorphic_types_only =
register_meta "encoding:monomorphic_only" [] register_meta_excl "encoding:monomorphic_only" []
~desc:"Set@ when@ no@ occurence@ of@ type@ variables@ occur." ~desc:"Set@ when@ no@ occurence@ of@ type@ variables@ occur."
exception Found
let find_in_decl d = let find_in_decl d =
match d.d_node with match d.d_node with
| Dtype _ts -> true (* TODO *) | Dtype ts ->
| Ddata _dl -> true (* TODO *) Format.eprintf "======@\nFound type %a@\n" Pretty.print_ts ts;
| Dparam _ls -> true (* TODO *) if ts.Ty.ts_args <> [] then
| Dlogic _dl -> true (* TODO *) (Format.eprintf "Type is polymorphic!@\n=======@.";
| Dind _ind -> true (* TODO *) raise Found);
| Dprop _p -> true (* TODO *) Format.eprintf "=======@."
| Ddata _dl -> () (* TODO *)
| Dparam _ls -> () (* TODO *)
| Dlogic _dl -> () (* TODO *)
| Dind _ind -> () (* TODO *)
| Dprop _p -> () (* TODO *)
let rec find_in_theory th = List.iter find_in_tdecl th.th_decls
let find_in_tdecl td = and find_in_tdecl td =
match td.td_node with match td.td_node with
| Decl d -> find_in_decl d | Decl d -> find_in_decl d
| Use _ | Clone _ | Meta _ -> false | Use th ->
Format.eprintf "======@\nLook up in used theory %a@." Pretty.print_th th;
find_in_theory th
| Clone (th,_) ->
Format.eprintf "======@\nLook up in cloned theory %a@." Pretty.print_th th;
find_in_theory th
| Meta _ -> ()
let rec find_in_task task = let rec find_in_task task =
match task with match task with
| None -> false | None -> ()
| Some t -> find_in_task t.task_prev || find_in_tdecl t.task_decl | Some t -> find_in_task t.task_prev ; find_in_tdecl t.task_decl
let detect_polymorphism task = let detect_polymorphism task =
if find_in_task task then task else try
add_meta task meta_monomorphic_types_only [] find_in_task task;
try
let g,t = task_separate_goal task in
let ta = add_meta t meta_monomorphic_types_only [] in
Task.add_tdecl ta g
with GoalNotFound ->
add_meta task meta_monomorphic_types_only []
with Found -> task
let () = Trans.register_transform "detect_polymorphism"
(Trans.store detect_polymorphism)
~desc:"Detect if task has polymorphic types somewhere."
theory Mono
use import int.Int
goal g : 2+2 = 5
end
theory PolyType
type t 'a = A 'a
goal g: forall x y:'a. A x = A y
end
theory TestList
use import list.List
goal g : match Cons 42 Nil with Nil -> false | Cons x _ -> x=42 end
end
theory T theory T
use import option.Option use import option.Option
type t 'a = A | Lam (t (option 'a)) type t 'a = A | Lam (t (option 'a))
......
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