utils.cmx: utils.cmi
inference.cmo: utils.cmi inference.cmi
inference.cmx: utils.cmx inference.cmi
-path_indexing.cmo: utils.cmi trie.cmo inference.cmi
-path_indexing.cmx: utils.cmx trie.cmx inference.cmx
-discrimination_tree.cmo: utils.cmi trie.cmo inference.cmi
-discrimination_tree.cmx: utils.cmx trie.cmx inference.cmx
-indexing.cmo: utils.cmi inference.cmi discrimination_tree.cmo
-indexing.cmx: utils.cmx inference.cmx discrimination_tree.cmx
+path_indexing.cmo: utils.cmi inference.cmi
+path_indexing.cmx: utils.cmx inference.cmx
+indexing.cmo: utils.cmi inference.cmi
+indexing.cmx: utils.cmx inference.cmx
saturation.cmo: utils.cmi inference.cmi indexing.cmo
saturation.cmx: utils.cmx inference.cmx indexing.cmx
INTERFACE_FILES = \
utils.mli \
- inference.mli
+ inference.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) \
- trie.ml \
path_indexing.ml \
- discrimination_tree.ml \
indexing.ml \
saturation.ml
-retrieve retrieve only
-help Display this list of options
--help Display this list of options
+
+
+./saturate -l 10 -demod-equalities
+
+dove -l 10 e` il timeout in secondi.
+
+Il programma legge da standard input il teorema, per esempio
+
+\forall n:nat.n + n = 2 * n
+
+l'input termina con una riga vuota (quindi basta un doppio invio alla fine)
+
+In output, oltre ai vari messaggi di debug, vengono stampati gli insiemi
+active e passive alla fine dell'esecuzione. Consiglio di redirigere l'output
+su file, per esempio usando tee:
+
+./saturate -l 10 -demod-equalities | tee output.txt
+
+Il formato di stampa e` quello per gli oggetti di tipo equality (usa la
+funzione Inference.string_of_equality)
+
+
+++ /dev/null
-(* Copyright (C) 2005, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-type path_string_elem = Cic.term;;
-type path_string = path_string_elem list;;
-
-
-(* needed by the retrieve_* functions, to know the arities of the "functions" *)
-let arities = Hashtbl.create 11;;
-
-
-let rec path_string_of_term = function
- | Cic.Meta _ -> [Cic.Implicit None]
- | Cic.Appl ((hd::tl) as l) ->
- if not (Hashtbl.mem arities hd) then
- Hashtbl.add arities hd (List.length tl);
- List.concat (List.map path_string_of_term l)
- | term -> [term]
-;;
-
-
-let string_of_path_string ps =
- String.concat "." (List.map CicPp.ppterm ps)
-;;
-
-
-module OrderedPathStringElement = struct
- type t = path_string_elem
-
- let compare = Pervasives.compare
-end
-
-module PSMap = Map.Make(OrderedPathStringElement);;
-
-
-module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
-
- let compare = Pervasives.compare
-end
-
-module PosEqSet = Set.Make(OrderedPosEquality);;
-
-
-module DiscriminationTree = Trie.Make(PSMap);;
-
-
-let string_of_discrimination_tree tree =
- let rec to_string level = function
- | DiscriminationTree.Node (value, map) ->
- let s =
- match value with
- | Some v ->
- (String.make (2 * level) ' ') ^
- "{" ^ (String.concat "; "
- (List.map
- (fun (p, e) ->
- "(" ^ (Utils.string_of_pos p) ^ ", " ^
- (Inference.string_of_equality e) ^ ")")
- (PosEqSet.elements v))) ^ "}"
- | None -> ""
- in
- let rest =
- String.concat "\n"
- (PSMap.fold
- (fun k v s ->
- let ks = CicPp.ppterm k in
- let rs = to_string (level+1) v in
- ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s)
- map [])
- in
- s ^ rest
- in
- to_string 0 tree
-;;
-
-
-let index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_string_of_term l
- and psr = path_string_of_term r in
- let index pos tree ps =
- let ps_set =
- try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in
- let tree =
- DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in
- tree
- in
- match ordering with
- | Utils.Gt -> index Utils.Left tree psl
- | Utils.Lt -> index Utils.Right tree psr
- | _ ->
- let tree = index Utils.Left tree psl in
- index Utils.Right tree psr
-;;
-
-
-let remove_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_string_of_term l
- and psr = path_string_of_term r in
- let remove_index pos tree ps =
- try
- let ps_set =
- PosEqSet.remove (pos, equality) (DiscriminationTree.find ps tree) in
- if PosEqSet.is_empty ps_set then
- DiscriminationTree.remove ps tree
- else
- DiscriminationTree.add ps ps_set tree
- with Not_found ->
- tree
- in
- match ordering with
- | Utils.Gt -> remove_index Utils.Left tree psl
- | Utils.Lt -> remove_index Utils.Right tree psr
- | _ ->
- let tree = remove_index Utils.Left tree psl in
- remove_index Utils.Right tree psr
-;;
-
-
-let in_index tree equality =
- let _, _, (_, l, r, ordering), _, _ = equality in
- let psl = path_string_of_term l
- and psr = path_string_of_term r in
- let meta_convertibility = Inference.meta_convertibility_eq equality in
- let ok ps =
- try
- let set = DiscriminationTree.find ps tree in
- PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
- with Not_found ->
- false
- in
- (ok psl) || (ok psr)
-;;
-
-
-let head_of_term = function
- | Cic.Appl (hd::tl) -> hd
- | term -> term
-;;
-
-
-let rec subterm_at_pos pos term =
- match pos with
- | [] -> term
- | index::pos ->
- match term with
- | Cic.Appl l ->
- (try subterm_at_pos pos (List.nth l index)
- with Failure _ -> raise Not_found)
- | _ -> raise Not_found
-;;
-
-
-let rec after_t pos term =
- let pos' =
- match pos with
- | [] -> raise Not_found
- | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
- in
- try
- let t = subterm_at_pos pos' term in pos'
- with Not_found ->
- let pos, _ =
- List.fold_right
- (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
- in
- after_t pos term
-;;
-
-
-let next_t pos term =
- let t = subterm_at_pos pos term in
- try
- let _ = subterm_at_pos [1] t in
- pos @ [1]
- with Not_found ->
- match pos with
- | [] -> [1]
- | pos -> after_t pos term
-;;
-
-
-let retrieve_generalizations tree term =
- let rec retrieve tree term pos =
- match tree with
- | DiscriminationTree.Node (Some s, _) when pos = [] -> s
- | DiscriminationTree.Node (_, map) ->
- let res =
- try
- let hd_term = head_of_term (subterm_at_pos pos term) in
- let n = PSMap.find hd_term map in
- match n with
- | DiscriminationTree.Node (Some s, _) -> s
- | DiscriminationTree.Node (None, _) ->
- let newpos = try next_t pos term with Not_found -> [] in
- retrieve n term newpos
- with Not_found ->
- PosEqSet.empty
- in
- try
- let n = PSMap.find (Cic.Implicit None) map in
- let newpos = try after_t pos term with Not_found -> [-1] in
- if newpos = [-1] then
- match n with
- | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
- | _ -> res
- else
- PosEqSet.union res (retrieve n term newpos)
- with Not_found ->
- res
- in
- retrieve tree term []
-;;
-
-
-let jump_list = function
- | DiscriminationTree.Node (value, map) ->
- let rec get n tree =
- match tree with
- | DiscriminationTree.Node (v, m) ->
- if n = 0 then
- [tree]
- else
- PSMap.fold
- (fun k v res ->
- let a = try Hashtbl.find arities k with Not_found -> 0 in
- (get (n-1 + a) v) @ res) m []
- in
- PSMap.fold
- (fun k v res ->
- let arity = try Hashtbl.find arities k with Not_found -> 0 in
- (get arity v) @ res)
- map []
-;;
-
-
-let retrieve_unifiables tree term =
- let rec retrieve tree term pos =
- match tree with
- | DiscriminationTree.Node (Some s, _) when pos = [] -> s
- | DiscriminationTree.Node (_, map) ->
- let subterm =
- try Some (subterm_at_pos pos term) with Not_found -> None
- in
- match subterm with
- | None -> PosEqSet.empty
- | Some (Cic.Meta _) ->
- let newpos = try next_t pos term with Not_found -> [] in
- let jl = jump_list tree in
- List.fold_left
- (fun r s -> PosEqSet.union r s)
- PosEqSet.empty
- (List.map (fun t -> retrieve t term newpos) jl)
- | Some subterm ->
- let res =
- try
- let hd_term = head_of_term subterm in
- let n = PSMap.find hd_term map in
- match n with
- | DiscriminationTree.Node (Some s, _) -> s
- | DiscriminationTree.Node (None, _) ->
- retrieve n term (next_t pos term)
- with Not_found ->
- PosEqSet.empty
- in
- try
- let n = PSMap.find (Cic.Implicit None) map in
- let newpos = try after_t pos term with Not_found -> [-1] in
- if newpos = [-1] then
- match n with
- | DiscriminationTree.Node (Some s, _) -> PosEqSet.union s res
- | _ -> res
- else
- PosEqSet.union res (retrieve n term newpos)
- with Not_found ->
- res
- in
- retrieve tree term []
-;;
* http://cs.unibo.it/helm/.
*)
+module OrderedPosEquality = struct
+ type t = Utils.pos * Inference.equality
+ let compare = Pervasives.compare
+ end
+
+module PosEqSet = Set.Make(OrderedPosEquality);;
+
+module DT = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet);;
+
let debug_print = Utils.debug_print;;
let apply_subst = CicMetaSubst.apply_subst
-
-
(*
(* NO INDEXING *)
let init_index () = ()
;;
let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index
-and in_index = Path_indexing.in_index;;
+let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.remove_index tree l equality
+ | Utils.Lt -> DT.remove_index tree r equality
+ | _ ->
+ DT.remove_index (DT.remove_index tree r equality) l equality
+
+
+let in_index = Path_indexing.in_index;;
let get_candidates mode trie term =
let t1 = Unix.gettimeofday () in
;;
*)
-
(* DISCRIMINATION TREES *)
let init_index () =
- Hashtbl.clear Discrimination_tree.arities;
+ Hashtbl.clear DT.arities;
;;
let empty_table () =
- Discrimination_tree.DiscriminationTree.empty
+ DT.empty
;;
-let index = Discrimination_tree.index
-and remove_index = Discrimination_tree.remove_index
-and in_index = Discrimination_tree.in_index;;
+let remove_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.remove_index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.remove_index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.remove_index tree r (Utils.Right, equality) in
+ DT.remove_index tree l (Utils.Left, equality)
+
+let index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ match ordering with
+ | Utils.Gt -> DT.index tree l (Utils.Left, equality)
+ | Utils.Lt -> DT.index tree r (Utils.Right, equality)
+ | _ ->
+ let tree = DT.index tree r (Utils.Right, equality) in
+ DT.index tree l (Utils.Left, equality)
+
+
+let in_index tree equality =
+ let _, _, (_, l, r, ordering), _, _ = equality in
+ let meta_convertibility (pos,equality') =
+ Inference.meta_convertibility_eq equality equality'
+ in
+ DT.in_index tree l meta_convertibility || DT.in_index tree r meta_convertibility
+
(* returns a list of all the equalities in the tree that are in relation
"mode" with the given term, where mode can be either Matching or
let res =
let s =
match mode with
- | Matching -> Discrimination_tree.retrieve_generalizations tree term
- | Unification -> Discrimination_tree.retrieve_unifiables tree term
+ | Matching -> DT.retrieve_generalizations tree term
+ | Unification -> DT.retrieve_unifiables tree term
in
- Discrimination_tree.PosEqSet.elements s
+ PosEqSet.elements s
in
(* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
in
match res with
| Some (_, s, _, _, _) ->
- let c' = apply_subst s c
- and other' = apply_subst s other in
+ let c' = apply_subst s c in
+ let other' = U.guarded_simpl context (apply_subst s other) in
let order = cmp c' other' in
let names = U.names_of_context context in
if order = U.Gt then
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ let module U = Utils in
let metasenv, context, ugraph = env in
let _, proof, (eq_ty, left, right, order), metas, args = target in
let metasenv' = metasenv @ metas in
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = apply_subst subst (S.subst other t) in
+ let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
let bo' =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
- let bo' = apply_subst s (S.subst other bo) in
+ let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
incr sup_l_counter;
let bo'' =
let is_identity ((metasenv, context, ugraph) as env) = function
| ((_, _, (ty, left, right, _), menv, _) as equality) ->
- (left = right ||
+ (prerr_endline ("left = "^(CicPp.ppterm left));
+ prerr_endline ("right = "^(CicPp.ppterm right));
+ (left = right ||
(* (meta_convertibility left right) || *)
(fst (CicReduction.are_convertible
- ~metasenv:(metasenv @ menv) context left right ugraph)))
+ ~metasenv:(metasenv @ menv) context left right ugraph))))
;;
| "lpo" -> Utils.compare_terms := Utils.lpo
| "kbo" -> Utils.compare_terms := Utils.kbo
| "nr-kbo" -> Utils.compare_terms := Utils.nonrec_kbo
+ | "ao" -> Utils.compare_terms := Utils.ao
| o -> raise (Arg.Bad ("Unknown term ordering: " ^ o))
and set_fullred b = S.use_fullred := b
and set_time_limit v = S.time_limit := float_of_int v
let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
-Utils.compare_terms := Utils.nonrec_kbo;;
+(* Utils.compare_terms := Utils.nonrec_kbo;; *)
+Utils.compare_terms := Utils.ao;;
(* statistics... *)
let derived_clauses = ref 0;;
(* Negatives aren't indexed, no need to remove them... *)
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
- | [], hd::tl ->
+ | [], (hd:EqualitySet.elt)::tl ->
let passive_table =
Indexing.remove_index passive_table hd
in
+++ /dev/null
-(*
- * Trie: maps over lists.
- * Copyright (C) 2000 Jean-Christophe FILLIATRE
- *
- * This software is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Library General Public
- * License version 2, as published by the Free Software Foundation.
- *
- * This software is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
- *
- * See the GNU Library General Public License version 2 for more details
- * (enclosed in the file LGPL).
- *)
-
-(* $Id$ *)
-
-(*s A trie is a tree-like structure to implement dictionaries over
- keys which have list-like structures. The idea is that each node
- branches on an element of the list and stores the value associated
- to the path from the root, if any. Therefore, a trie can be
- defined as soon as a map over the elements of the list is
- given. *)
-
-
-module Make (M : Map.S) = struct
-
-(*s Then a trie is just a tree-like structure, where a possible
- information is stored at the node (['a option]) and where the sons
- are given by a map from type [key] to sub-tries, so of type
- ['a t M.t]. The empty trie is just the empty map. *)
-
- type key = M.key list
-
- type 'a t = Node of 'a option * 'a t M.t
-
- let empty = Node (None, M.empty)
-
-(*s To find a mapping in a trie is easy: when all the elements of the
- key have been read, we just inspect the optional info at the
- current node; otherwise, we descend in the appropriate sub-trie
- using [M.find]. *)
-
- let rec find l t = match (l,t) with
- | [], Node (None,_) -> raise Not_found
- | [], Node (Some v,_) -> v
- | x::r, Node (_,m) -> find r (M.find x m)
-
- let rec mem l t = match (l,t) with
- | [], Node (None,_) -> false
- | [], Node (Some _,_) -> true
- | x::r, Node (_,m) -> try mem r (M.find x m) with Not_found -> false
-
-(*s Insertion is more subtle. When the final node is reached, we just
- put the information ([Some v]). Otherwise, we have to insert the
- binding in the appropriate sub-trie [t']. But it may not exists,
- and in that case [t'] is bound to an empty trie. Then we get a new
- sub-trie [t''] by a recursive insertion and we modify the
- branching, so that it now points to [t''], with [M.add]. *)
-
- let add l v t =
- let rec ins = function
- | [], Node (_,m) -> Node (Some v,m)
- | x::r, Node (v,m) ->
- let t' = try M.find x m with Not_found -> empty in
- let t'' = ins (r,t') in
- Node (v, M.add x t'' m)
- in
- ins (l,t)
-
-(*s When removing a binding, we take care of not leaving bindings to empty
- sub-tries in the nodes. Therefore, we test wether the result [t'] of
- the recursive call is the empty trie [empty]: if so, we just remove
- the branching with [M.remove]; otherwise, we modify it with [M.add]. *)
-
- let rec remove l t = match (l,t) with
- | [], Node (_,m) -> Node (None,m)
- | x::r, Node (v,m) ->
- try
- let t' = remove r (M.find x m) in
- Node (v, if t' = empty then M.remove x m else M.add x t' m)
- with Not_found ->
- t
-
-(*s The iterators [map], [mapi], [iter] and [fold] are implemented in
- a straigthforward way using the corresponding iterators [M.map],
- [M.mapi], [M.iter] and [M.fold]. For the last three of them,
- we have to remember the path from the root, as an extra argument
- [revp]. Since elements are pushed in reverse order in [revp],
- we have to reverse it with [List.rev] when the actual binding
- has to be passed to function [f]. *)
-
- let rec map f = function
- | Node (None,m) -> Node (None, M.map (map f) m)
- | Node (Some v,m) -> Node (Some (f v), M.map (map f) m)
-
- let mapi f t =
- let rec maprec revp = function
- | Node (None,m) ->
- Node (None, M.mapi (fun x -> maprec (x::revp)) m)
- | Node (Some v,m) ->
- Node (Some (f (List.rev revp) v), M.mapi (fun x -> maprec (x::revp)) m)
- in
- maprec [] t
-
- let iter f t =
- let rec traverse revp = function
- | Node (None,m) ->
- M.iter (fun x -> traverse (x::revp)) m
- | Node (Some v,m) ->
- f (List.rev revp) v; M.iter (fun x t -> traverse (x::revp) t) m
- in
- traverse [] t
-
- let rec fold f t acc =
- let rec traverse revp t acc = match t with
- | Node (None,m) ->
- M.fold (fun x -> traverse (x::revp)) m acc
- | Node (Some v,m) ->
- f (List.rev revp) v (M.fold (fun x -> traverse (x::revp)) m acc)
- in
- traverse [] t acc
-
- let compare cmp a b =
- let rec comp a b = match a,b with
- | Node (Some _, _), Node (None, _) -> 1
- | Node (None, _), Node (Some _, _) -> -1
- | Node (None, m1), Node (None, m2) ->
- M.compare comp m1 m2
- | Node (Some a, m1), Node (Some b, m2) ->
- let c = cmp a b in
- if c <> 0 then c else M.compare comp m1 m2
- in
- comp a b
-
- let equal eq a b =
- let rec comp a b = match a,b with
- | Node (None, m1), Node (None, m2) ->
- M.equal comp m1 m2
- | Node (Some a, m1), Node (Some b, m2) ->
- eq a b && M.equal comp m1 m2
- | _ ->
- false
- in
- comp a b
-
- (* The base case is rather stupid, but constructable *)
- let is_empty = function
- | Node (None, m1) -> M.is_empty m1
- | _ -> false
-
-end
let debug_print s = if debug then prerr_endline (Lazy.force s);;
-
let print_metasenv metasenv =
String.concat "\n--------------------------\n"
(List.map (fun (i, context, term) ->
| res -> res
;;
+let rec ao t1 t2 =
+ let get_hd t =
+ match t with
+ Cic.MutConstruct(uri,tyno,cno,_) -> Some(uri,tyno,cno)
+ | Cic.Appl(Cic.MutConstruct(uri,tyno,cno,_)::_) ->
+ Some(uri,tyno,cno)
+ | _ -> None in
+ let aux = aux_ordering ~recursion:false in
+ let w1 = weight_of_term t1
+ and w2 = weight_of_term t2 in
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> Eq
+ | _, [] -> Gt
+ | [], _ -> Lt
+ | hd1::tl1, hd2::tl2 ->
+ let o =
+ ao hd1 hd2
+ in
+ if o = Eq then cmp tl1 tl2
+ else o
+ in
+ match get_hd t1, get_hd t2 with
+ Some(_),None -> Lt
+ | None,Some(_) -> Gt
+ | _ ->
+ let comparison = compare_weights ~normalize:true w1 w2 in
+ match comparison with
+ | Le ->
+ let r = aux t1 t2 in
+ if r = Lt then Lt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Lt then Lt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Ge ->
+ let r = aux t1 t2 in
+ if r = Gt then Gt
+ else if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ if cmp tl1 tl2 = Gt then Gt else Incomparable
+ | _, _ -> Incomparable
+ ) else Incomparable
+ | Eq ->
+ let r = aux t1 t2 in
+ if r = Eq then (
+ match t1, t2 with
+ | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
+ cmp tl1 tl2
+ | _, _ -> Incomparable
+ ) else r
+ | res -> res
+;;
let names_of_context context =
List.map
(* settable by the user... *)
-let compare_terms = ref nonrec_kbo;;
-
+(* let compare_terms = ref nonrec_kbo;; *)
+let compare_terms = ref ao;;
+
+let guarded_simpl context t =
+ let t' = ProofEngineReduction.simpl context t in
+ let simpl_order = !compare_terms t t' in
+ if simpl_order = Gt then
+ (prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t'));
+ t')
+ else t
+;;
type equality_sign = Negative | Positive;;
val kbo: Cic.term -> Cic.term -> comparison
+val ao: Cic.term -> Cic.term -> comparison
+
(** term-ordering function settable by the user *)
val compare_terms: (Cic.term -> Cic.term -> comparison) ref
+val guarded_simpl: Cic.context -> Cic.term -> Cic.term
+
type equality_sign = Negative | Positive
val string_of_sign: equality_sign -> string
projects / helm.git / commitdiff