diff options
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 21077ecc8..a85c80a79 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -51,7 +51,7 @@ module ST=struct let enter t sign st= if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" + anomaly ~label:"enter" (Pp.str "signature already entered") else Hashtbl.replace st.toterm sign t; Hashtbl.replace st.tosign t sign @@ -272,7 +272,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly "get_representative: not a representative" + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") let find_pac uf i pac = PacMap.find pac (get_representative uf i).constructors @@ -280,7 +280,7 @@ let find_pac uf i pac = let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly "get_constructor: not a constructor" + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") let size uf i= (get_representative uf i).weight @@ -325,7 +325,7 @@ 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" + | _ -> anomaly ~label:"subterms" (Pp.str "not a node") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -402,7 +402,7 @@ let rec canonize_name c = let build_subst uf subst = Array.map (fun i -> try term uf i - with _ -> anomaly "incomplete matching") subst + with _ -> anomaly (Pp.str "incomplete matching")) subst let rec inst_pattern subst = function PVar i -> @@ -657,8 +657,8 @@ let process_constructor_mark t i rep pac state = {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" + | _-> anomaly ~label:"add_pacs" + (Pp.str "weird error in injection subterms merge") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> add_pac rep pac t; @@ -750,7 +750,7 @@ let complete_one_class state i= let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) - | _ -> anomaly "wrong incomplete class" + | _ -> anomaly (Pp.str "wrong incomplete class") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -890,7 +890,7 @@ let find_instances state = check_for_interrupt (); do_match state res pb_stack done; - anomaly "get out of here !" + anomaly (Pp.str "get out of here !") with Stack.Empty -> () in !res |