aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccalgo.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r--plugins/cc/ccalgo.ml390
1 files changed, 195 insertions, 195 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 418980c54..9cc6f9de9 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -22,45 +22,45 @@ open Proof_type
let init_size=5
-let cc_verbose=ref false
+let cc_verbose=ref false
-let debug f x =
+let debug f x =
if !cc_verbose then f x
let _=
let gdopt=
{ optsync=true;
optname="Congruence Verbose";
- optkey=["Congruence";"Verbose"];
- optread=(fun ()-> !cc_verbose);
- optwrite=(fun b -> cc_verbose := b)}
+ optkey=["Congruence";"Verbose"];
+ optread=(fun ()-> !cc_verbose);
+ optwrite=(fun b -> cc_verbose := b)}
in
declare_bool_option gdopt
(* Signature table *)
module ST=struct
-
+
(* l: sign -> term r: term -> sign *)
-
+
type t = {toterm:(int*int,int) Hashtbl.t;
tosign:(int,int*int) Hashtbl.t}
-
+
let empty ()=
{toterm=Hashtbl.create init_size;
tosign=Hashtbl.create init_size}
-
+
let enter t sign st=
- if Hashtbl.mem st.toterm sign then
+ if Hashtbl.mem st.toterm sign then
anomaly "enter: signature already entered"
- else
+ else
Hashtbl.replace st.toterm sign t;
Hashtbl.replace st.tosign t sign
-
+
let query sign st=Hashtbl.find st.toterm sign
let rev_query term st=Hashtbl.find st.tosign term
-
+
let delete st t=
try let sign=Hashtbl.find st.tosign t in
Hashtbl.remove st.toterm sign;
@@ -69,7 +69,7 @@ module ST=struct
Not_found -> ()
let rec delete_set st s = Intset.iter (delete st) s
-
+
end
type pa_constructor=
@@ -85,11 +85,11 @@ type pa_mark=
Fmark of pa_fun
| Cmark of pa_constructor
-module PacMap=Map.Make(struct
- type t=pa_constructor
- let compare=Pervasives.compare end)
+module PacMap=Map.Make(struct
+ type t=pa_constructor
+ let compare=Pervasives.compare end)
-module PafMap=Map.Make(struct
+module PafMap=Map.Make(struct
type t=pa_fun
let compare=Pervasives.compare end)
@@ -107,11 +107,11 @@ type term=
type ccpattern =
PApp of term * ccpattern list (* arguments are reversed *)
- | PVar of int
+ | PVar of int
type rule=
Congruence
- | Axiom of constr * bool
+ | Axiom of constr * bool
| Injection of int * pa_constructor * int * pa_constructor * int
type from=
@@ -127,7 +127,7 @@ type equality = rule eq
type disequality = from eq
type patt_kind =
- Normal
+ Normal
| Trivial of types
| Creates_variables
@@ -146,7 +146,7 @@ let swap eq : equality =
| Injection (i,pi,j,pj,k) -> Injection (j,pj,i,pi,k)
| Axiom (id,reversed) -> Axiom (id,not reversed)
in {lhs=eq.rhs;rhs=eq.lhs;rule=swap_rule}
-
+
type inductive_status =
Unknown
| Partial of pa_constructor
@@ -163,15 +163,15 @@ type representative=
mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality
-
-type vertex = Leaf| Node of (int*int)
-type node =
+type vertex = Leaf| Node of (int*int)
+
+type node =
{mutable clas:cl;
- mutable cpath: int;
+ mutable cpath: int;
vertex:vertex;
term:term}
-
+
type forest=
{mutable max_size:int;
mutable size:int;
@@ -180,11 +180,11 @@ type forest=
mutable epsilons: pa_constructor list;
syms:(term,int) Hashtbl.t}
-type state =
+type state =
{uf: forest;
sigtable:ST.t;
- mutable terms: Intset.t;
- combine: equality Queue.t;
+ mutable terms: Intset.t;
+ combine: equality Queue.t;
marks: (int * pa_mark) Queue.t;
mutable diseq: disequality list;
mutable quant: quant_eq list;
@@ -222,17 +222,17 @@ let empty depth gls:state =
changed=false;
gls=gls}
-let forest state = state.uf
-
+let forest state = state.uf
+
let compress_path uf i j = uf.map.(j).cpath<-i
-
-let rec find_aux uf visited i=
- let j = uf.map.(i).cpath in
+
+let rec find_aux uf visited i=
+ let j = uf.map.(i).cpath in
if j<0 then let _ = List.iter (compress_path uf i) visited in i else
find_aux uf (i::visited) j
-
+
let find uf i= find_aux uf [] i
-
+
let get_representative uf i=
match uf.map.(i).clas with
Rep r -> r
@@ -245,7 +245,7 @@ let get_constructor_info uf i=
match uf.map.(i).term with
Constructor cinfo->cinfo
| _ -> anomaly "get_constructor: not a constructor"
-
+
let size uf i=
(get_representative uf i).weight
@@ -264,36 +264,36 @@ let add_rfather uf i t=
r.weight<-r.weight+1;
r.fathers <-Intset.add t r.fathers
-exception Discriminable of int * pa_constructor * int * pa_constructor
+exception Discriminable of int * pa_constructor * int * pa_constructor
let append_pac t p =
- {p with arity=pred p.arity;args=t::p.args}
+ {p with arity=pred p.arity;args=t::p.args}
let tail_pac p=
{p with arity=succ p.arity;args=List.tl p.args}
let fsucc paf =
{paf with fnargs=succ paf.fnargs}
-
+
let add_pac rep pac t =
if not (PacMap.mem pac rep.constructors) then
rep.constructors<-PacMap.add pac t rep.constructors
let add_paf rep paf t =
- let already =
+ let already =
try PafMap.find paf rep.functions with Not_found -> Intset.empty in
rep.functions<- PafMap.add paf (Intset.add t already) rep.functions
let term uf i=uf.map.(i).term
-
+
let subterms uf i=
match uf.map.(i).vertex with
Node(j,k) -> (j,k)
| _ -> anomaly "subterms: not a node"
-
+
let signature uf i=
let j,k=subterms uf i in (find uf j,find uf k)
-
+
let next uf=
let size=uf.size in
let nsize= succ size in
@@ -304,11 +304,11 @@ let next uf=
uf.max_size<-newmax;
Array.blit uf.map 0 newmap 0 size;
uf.map<-newmap
- end
+ end
else ();
- uf.size<-nsize;
+ uf.size<-nsize;
size
-
+
let new_representative typ =
{weight=0;
lfathers=Intset.empty;
@@ -317,14 +317,14 @@ let new_representative typ =
class_type=typ;
functions=PafMap.empty;
constructors=PacMap.empty}
-
+
(* rebuild a constr from an applicative term *)
-
+
let _A_ = Name (id_of_string "A")
let _B_ = Name (id_of_string "A")
let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2)
-let cc_product s1 s2 =
+let cc_product s1 s2 =
mkLambda(_A_,mkSort(Termops.new_sort_in_family s1),
mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_))
@@ -332,27 +332,27 @@ let rec constr_of_term = function
Symb s->s
| Product(s1,s2) -> cc_product s1 s2
| Eps id -> mkVar id
- | Constructor cinfo -> mkConstruct cinfo.ci_constr
+ | Constructor cinfo -> mkConstruct cinfo.ci_constr
| Appli (s1,s2)->
make_app [(constr_of_term s2)] s1
and make_app l=function
- Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
- | other -> applistc (constr_of_term other) l
+ Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
+ | other -> applistc (constr_of_term other) l
(* rebuild a term from a pattern and a substitution *)
let build_subst uf subst =
- Array.map (fun i ->
- try term uf i
+ Array.map (fun i ->
+ try term uf i
with _ -> anomaly "incomplete matching") subst
let rec inst_pattern subst = function
- PVar i ->
- subst.(pred i)
- | PApp (t, args) ->
+ PVar i ->
+ subst.(pred i)
+ | PApp (t, args) ->
List.fold_right
(fun spat f -> Appli (f,inst_pattern subst spat))
- args t
+ args t
let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
Termops.print_constr (constr_of_term (term state.uf i)) ++ str "]"
@@ -360,9 +360,9 @@ let pr_idx_term state i = str "[" ++ int i ++ str ":=" ++
let pr_term t = str "[" ++
Termops.print_constr (constr_of_term t) ++ str "]"
-let rec add_term state t=
+let rec add_term state t=
let uf=state.uf in
- try Hashtbl.find uf.syms t with
+ try Hashtbl.find uf.syms t with
Not_found ->
let b=next uf in
let typ = pf_type_of state.gls (constr_of_term t) in
@@ -377,12 +377,12 @@ let rec add_term state t=
cpath= -1;
vertex= Leaf;
term= t}
- | Eps id ->
+ | Eps id ->
{clas= Rep (new_representative typ);
cpath= -1;
vertex= Leaf;
term= t}
- | Appli (t1,t2) ->
+ | Appli (t1,t2) ->
let i1=add_term state t1 and i2=add_term state t2 in
add_lfather uf (find uf i1) b;
add_rfather uf (find uf i2) b;
@@ -408,9 +408,9 @@ let rec add_term state t=
in
uf.map.(b)<-new_node;
Hashtbl.add uf.syms t b;
- Hashtbl.replace state.by_type typ
- (Intset.add b
- (try Hashtbl.find state.by_type typ with
+ Hashtbl.replace state.by_type typ
+ (Intset.add b
+ (try Hashtbl.find state.by_type typ with
Not_found -> Intset.empty));
b
@@ -436,22 +436,22 @@ let add_quant state id pol (nvars,valid1,patt1,valid2,patt2) =
qe_rhs_valid=valid2}::state.quant
let is_redundant state id args =
- try
+ try
let norm_args = Array.map (find state.uf) args in
let prev_args = Hashtbl.find_all state.q_history id in
- List.exists
- (fun old_args ->
- Util.array_for_all2 (fun i j -> i = find state.uf j)
- norm_args old_args)
+ List.exists
+ (fun old_args ->
+ Util.array_for_all2 (fun i j -> i = find state.uf j)
+ norm_args old_args)
prev_args
with Not_found -> false
-let add_inst state (inst,int_subst) =
+let add_inst state (inst,int_subst) =
check_for_interrupt ();
if state.rew_depth > 0 then
if is_redundant state inst.qe_hyp_id int_subst then
debug msgnl (str "discarding redundant (dis)equality")
- else
+ else
begin
Hashtbl.add state.q_history inst.qe_hyp_id int_subst;
let subst = build_subst (forest state) int_subst in
@@ -459,149 +459,149 @@ let add_inst state (inst,int_subst) =
let args = Array.map constr_of_term subst in
let _ = array_rev args in (* highest deBruijn index first *)
let prf= mkApp(prfhead,args) in
- let s = inst_pattern subst inst.qe_lhs
+ let s = inst_pattern subst inst.qe_lhs
and t = inst_pattern subst inst.qe_rhs in
state.changed<-true;
state.rew_depth<-pred state.rew_depth;
if inst.qe_pol then
begin
- debug (fun () ->
- msgnl
+ debug (fun () ->
+ msgnl
(str "Adding new equality, depth="++ int state.rew_depth);
- msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]")) ();
add_equality state prf s t
end
else
begin
- debug (fun () ->
- msgnl
+ debug (fun () ->
+ msgnl
(str "Adding new disequality, depth="++ int state.rew_depth);
- msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
+ msgnl (str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]")) ();
- add_disequality state (Hyp prf) s t
+ add_disequality state (Hyp prf) s t
end
end
let link uf i j eq = (* links i -> j *)
- let node=uf.map.(i) in
+ let node=uf.map.(i) in
node.clas<-Eqto (j,eq);
node.cpath<-j
-
+
let rec down_path uf i l=
match uf.map.(i).clas with
Eqto(j,t)->down_path uf j (((i,j),t)::l)
| Rep _ ->l
-
+
let rec min_path=function
([],l2)->([],l2)
| (l1,[])->(l1,[])
- | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2)
+ | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2)
| cpl -> cpl
-
+
let join_path uf i j=
assert (find uf i=find uf j);
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
+ debug (fun () -> msgnl (str "Linking " ++ pr_idx_term state i1 ++
str " and " ++ pr_idx_term state i2 ++ str ".")) ();
- let r1= get_representative state.uf i1
+ let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
link state.uf i1 i2 eq;
- Hashtbl.replace state.by_type r1.class_type
- (Intset.remove i1
- (try Hashtbl.find state.by_type r1.class_type with
+ Hashtbl.replace state.by_type r1.class_type
+ (Intset.remove i1
+ (try Hashtbl.find state.by_type r1.class_type with
Not_found -> Intset.empty));
let f= Intset.union r1.fathers r2.fathers in
r2.weight<-Intset.cardinal f;
r2.fathers<-f;
r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
ST.delete_set state.sigtable r1.fathers;
- state.terms<-Intset.union state.terms r1.fathers;
- PacMap.iter
- (fun pac b -> Queue.add (b,Cmark pac) state.marks)
+ state.terms<-Intset.union state.terms r1.fathers;
+ PacMap.iter
+ (fun pac b -> Queue.add (b,Cmark pac) state.marks)
r1.constructors;
- PafMap.iter
- (fun paf -> Intset.iter
- (fun b -> Queue.add (b,Fmark paf) state.marks))
+ PafMap.iter
+ (fun paf -> Intset.iter
+ (fun b -> Queue.add (b,Fmark paf) state.marks))
r1.functions;
- match r1.inductive_status,r2.inductive_status with
+ match r1.inductive_status,r2.inductive_status with
Unknown,_ -> ()
- | Partial pac,Unknown ->
+ | Partial pac,Unknown ->
r2.inductive_status<-Partial pac;
state.pa_classes<-Intset.remove i1 state.pa_classes;
state.pa_classes<-Intset.add i2 state.pa_classes
- | Partial _ ,(Partial _ |Partial_applied) ->
+ | Partial _ ,(Partial _ |Partial_applied) ->
state.pa_classes<-Intset.remove i1 state.pa_classes
- | Partial_applied,Unknown ->
- r2.inductive_status<-Partial_applied
- | Partial_applied,Partial _ ->
+ | Partial_applied,Unknown ->
+ r2.inductive_status<-Partial_applied
+ | Partial_applied,Partial _ ->
state.pa_classes<-Intset.remove i2 state.pa_classes;
r2.inductive_status<-Partial_applied
| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
- | Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
- | _,_ -> ()
-
+ | Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
+ | _,_ -> ()
+
let merge eq state = (* merge and no-merge *)
- debug (fun () -> msgnl
- (str "Merging " ++ pr_idx_term state eq.lhs ++
+ debug (fun () -> msgnl
+ (str "Merging " ++ pr_idx_term state eq.lhs ++
str " and " ++ pr_idx_term state eq.rhs ++ str ".")) ();
let uf=state.uf in
- let i=find uf eq.lhs
+ let i=find uf eq.lhs
and j=find uf eq.rhs in
- if i<>j then
+ if i<>j then
if (size uf i)<(size uf j) then
union state i j eq
else
union state j i (swap eq)
let update t state = (* update 1 and 2 *)
- debug (fun () -> msgnl
+ debug (fun () -> msgnl
(str "Updating term " ++ pr_idx_term state t ++ str ".")) ();
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
begin
- match rep.inductive_status with
+ match rep.inductive_status with
Partial _ ->
rep.inductive_status <- Partial_applied;
state.pa_classes <- Intset.remove i state.pa_classes
| _ -> ()
end;
- PacMap.iter
- (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks)
- rep.constructors;
- PafMap.iter
- (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks)
- rep.functions;
- try
- let s = ST.query sign state.sigtable in
+ PacMap.iter
+ (fun pac _ -> Queue.add (t,Cmark (append_pac v pac)) state.marks)
+ rep.constructors;
+ PafMap.iter
+ (fun paf _ -> Queue.add (t,Fmark (fsucc paf)) state.marks)
+ rep.functions;
+ try
+ let s = ST.query sign state.sigtable in
Queue.add {lhs=t;rhs=s;rule=Congruence} state.combine
- with
+ with
Not_found -> ST.enter t sign state.sigtable
let process_function_mark t rep paf state =
add_paf rep paf t;
state.terms<-Intset.union rep.lfathers state.terms
-
+
let process_constructor_mark t i rep pac state =
match rep.inductive_status with
Total (s,opac) ->
- if pac.cnode <> opac.cnode then (* Conflict *)
- raise (Discriminable (s,opac,t,pac))
+ if pac.cnode <> opac.cnode then (* Conflict *)
+ raise (Discriminable (s,opac,t,pac))
else (* Match *)
let cinfo = get_constructor_info state.uf pac.cnode in
let rec f n oargs args=
- if n > 0 then
+ if n > 0 then
match (oargs,args) with
s1::q1,s2::q2->
- Queue.add
+ Queue.add
{lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)}
state.combine;
- f (n-1) q1 q2
- | _-> anomaly
- "add_pacs : weird error in injection subterms merge"
+ f (n-1) q1 q2
+ | _-> anomaly
+ "add_pacs : weird error in injection subterms merge"
in f cinfo.ci_nhyps opac.args pac.args
| Partial_applied | Partial _ ->
add_pac rep pac t;
@@ -617,8 +617,8 @@ let process_constructor_mark t i rep pac state =
state.pa_classes<- Intset.add i state.pa_classes
end
-let process_mark t m state =
- debug (fun () -> msgnl
+let process_mark t m state =
+ debug (fun () -> msgnl
(str "Processing mark for term " ++ pr_idx_term state t ++ str ".")) ();
let i=find state.uf t in
let rep=get_representative state.uf i in
@@ -634,15 +634,15 @@ type explanation =
let check_disequalities state =
let uf=state.uf in
let rec check_aux = function
- dis::q ->
- debug (fun () -> msg
- (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
- pr_idx_term state dis.rhs ++ str " ... ")) ();
- if find uf dis.lhs=find uf dis.rhs then
- begin debug msgnl (str "Yes");Some dis end
+ dis::q ->
+ debug (fun () -> msg
+ (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+ pr_idx_term state dis.rhs ++ str " ... ")) ();
+ if find uf dis.lhs=find uf dis.rhs then
+ begin debug msgnl (str "Yes");Some dis end
else
begin debug msgnl (str "No");check_aux q end
- | [] -> None
+ | [] -> None
in
check_aux state.diseq
@@ -651,8 +651,8 @@ let one_step state =
let eq = Queue.take state.combine in
merge eq state;
true
- with Queue.Empty ->
- try
+ with Queue.Empty ->
+ try
let (t,m) = Queue.take state.marks in
process_mark t m state;
true
@@ -664,40 +664,40 @@ let one_step state =
true
with Not_found -> false
-let __eps__ = id_of_string "_eps_"
+let __eps__ = id_of_string "_eps_"
let new_state_var typ state =
let id = pf_get_new_id __eps__ state.gls in
state.gls<-
{state.gls with it =
- {state.gls.it with evar_hyps =
- Environ.push_named_context_val (id,None,typ)
+ {state.gls.it with evar_hyps =
+ Environ.push_named_context_val (id,None,typ)
state.gls.it.evar_hyps}};
id
let complete_one_class state i=
match (get_representative state.uf i).inductive_status with
Partial pac ->
- let rec app t typ n =
+ let rec app t typ n =
if n<=0 then t else
let _,etyp,rest= destProd typ in
let id = new_state_var etyp state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
let _c = pf_type_of state.gls
(constr_of_term (term state.uf pac.cnode)) in
- let _args =
- List.map (fun i -> constr_of_term (term state.uf i))
+ let _args =
+ List.map (fun i -> constr_of_term (term state.uf i))
pac.args in
- let typ = prod_applist _c (List.rev _args) in
+ let typ = prod_applist _c (List.rev _args) in
let ct = app (term state.uf i) typ pac.arity in
- state.uf.epsilons <- pac :: state.uf.epsilons;
+ state.uf.epsilons <- pac :: state.uf.epsilons;
ignore (add_term state ct)
- | _ -> anomaly "wrong incomplete class"
+ | _ -> anomaly "wrong incomplete class"
let complete state =
Intset.iter (complete_one_class state) state.pa_classes
-type matching_problem =
+type matching_problem =
{mp_subst : int array;
mp_inst : quant_eq;
mp_stack : (ccpattern*int) list }
@@ -705,31 +705,31 @@ type matching_problem =
let make_fun_table state =
let uf= state.uf in
let funtab=ref PafMap.empty in
- Array.iteri
+ Array.iteri
(fun i inode -> if i < uf.size then
match inode.clas with
Rep rep ->
- PafMap.iter
- (fun paf _ ->
- let elem =
- try PafMap.find paf !funtab
+ PafMap.iter
+ (fun paf _ ->
+ let elem =
+ try PafMap.find paf !funtab
with Not_found -> Intset.empty in
- funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+ funtab:= PafMap.add paf (Intset.add i elem) !funtab)
rep.functions
| _ -> ()) state.uf.map;
!funtab
-
+
let rec do_match state res pb_stack =
let mp=Stack.pop pb_stack in
match mp.mp_stack with
- [] ->
+ [] ->
res:= (mp.mp_inst,mp.mp_subst) :: !res
| (patt,cl)::remains ->
let uf=state.uf in
match patt with
- PVar i ->
- if mp.mp_subst.(pred i)<0 then
+ PVar i ->
+ if mp.mp_subst.(pred i)<0 then
begin
mp.mp_subst.(pred i)<- cl; (* no aliasing problem here *)
Stack.push {mp with mp_stack=remains} pb_stack
@@ -746,18 +746,18 @@ let rec do_match state res pb_stack =
with Not_found -> ()
end
| PApp(f, ((last_arg::rem_args) as args)) ->
- try
- let j=Hashtbl.find uf.syms f in
+ try
+ let j=Hashtbl.find uf.syms f in
let paf={fsym=j;fnargs=List.length args} in
let rep=get_representative uf cl in
let good_terms = PafMap.find paf rep.functions in
- let aux i =
+ let aux i =
let (s,t) = signature state.uf i in
- Stack.push
- {mp with
+ Stack.push
+ {mp with
mp_subst=Array.copy mp.mp_subst;
mp_stack=
- (PApp(f,rem_args),s) ::
+ (PApp(f,rem_args),s) ::
(last_arg,t) :: remains} pb_stack in
Intset.iter aux good_terms
with Not_found -> ()
@@ -768,7 +768,7 @@ let paf_of_patt syms = function
{fsym=Hashtbl.find syms f;
fnargs=List.length args}
-let init_pb_stack state =
+let init_pb_stack state =
let syms= state.uf.syms in
let pb_stack = Stack.create () in
let funtab = make_fun_table state in
@@ -778,51 +778,51 @@ let init_pb_stack state =
match inst.qe_lhs_valid with
Creates_variables -> Intset.empty
| Normal ->
- begin
- try
+ begin
+ try
let paf= paf_of_patt syms inst.qe_lhs in
PafMap.find paf funtab
with Not_found -> Intset.empty
end
- | Trivial typ ->
- begin
- try
+ | Trivial typ ->
+ begin
+ try
Hashtbl.find state.by_type typ
with Not_found -> Intset.empty
end in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
mp_inst=inst;
mp_stack=[inst.qe_lhs,i]} pb_stack) good_classes
end;
- begin
+ begin
let good_classes =
match inst.qe_rhs_valid with
Creates_variables -> Intset.empty
| Normal ->
- begin
- try
+ begin
+ try
let paf= paf_of_patt syms inst.qe_rhs in
PafMap.find paf funtab
with Not_found -> Intset.empty
end
- | Trivial typ ->
- begin
- try
+ | Trivial typ ->
+ begin
+ try
Hashtbl.find state.by_type typ
with Not_found -> Intset.empty
end in
- Intset.iter (fun i ->
- Stack.push
- {mp_subst = Array.make inst.qe_nvars (-1);
+ Intset.iter (fun i ->
+ Stack.push
+ {mp_subst = Array.make inst.qe_nvars (-1);
mp_inst=inst;
mp_stack=[inst.qe_rhs,i]} pb_stack) good_classes
end in
List.iter aux state.quant;
pb_stack
-let find_instances state =
+let find_instances state =
let pb_stack= init_pb_stack state in
let res =ref [] in
let _ =
@@ -830,7 +830,7 @@ let find_instances state =
try
while true do
check_for_interrupt ();
- do_match state res pb_stack
+ do_match state res pb_stack
done;
anomaly "get out of here !"
with Stack.Empty -> () in
@@ -839,34 +839,34 @@ let find_instances state =
let rec execute first_run state =
debug msgnl (str "Executing ... ");
try
- while
+ while
check_for_interrupt ();
one_step state do ()
done;
match check_disequalities state with
- None ->
+ None ->
if not(Intset.is_empty state.pa_classes) then
- begin
+ begin
debug msgnl (str "First run was incomplete, completing ... ");
complete state;
execute false state
end
- else
+ else
if state.rew_depth>0 then
let l=find_instances state in
List.iter (add_inst state) l;
- if state.changed then
+ if state.changed then
begin
state.changed <- false;
execute true state
end
else
- begin
+ begin
debug msgnl (str "Out of instances ... ");
None
end
- else
- begin
+ else
+ begin
debug msgnl (str "Out of depth ... ");
None
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 15:16:47 +0000