-filter_auto.cmi: newConstraints.cmi
proofEngineHelpers.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
-tacticChaser.cmi: proofEngineTypes.cmi
+metadataQuery.cmi: proofEngineTypes.cmi
variousTactics.cmi: proofEngineTypes.cmi
introductionTactics.cmi: proofEngineTypes.cmi
eliminationTactics.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
-newConstraints.cmo: newConstraints.cmi
-newConstraints.cmx: newConstraints.cmi
-match_concl.cmo: newConstraints.cmi match_concl.cmi
-match_concl.cmx: newConstraints.cmx match_concl.cmi
-filter_auto.cmo: newConstraints.cmi filter_auto.cmi
-filter_auto.cmx: newConstraints.cmx filter_auto.cmi
proofEngineReduction.cmo: proofEngineReduction.cmi
proofEngineReduction.cmx: proofEngineReduction.cmi
proofEngineHelpers.cmo: proofEngineHelpers.cmi
primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
primitiveTactics.cmi
-metadataQuery.cmo: metadataQuery.cmi
-metadataQuery.cmx: metadataQuery.cmi
-tacticChaser.cmo: filter_auto.cmi match_concl.cmi newConstraints.cmi \
- primitiveTactics.cmi proofEngineTypes.cmi tacticChaser.cmi
-tacticChaser.cmx: filter_auto.cmx match_concl.cmx newConstraints.cmx \
- primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi
-variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \
- proofEngineTypes.cmi tacticChaser.cmi tacticals.cmi variousTactics.cmi
-variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \
- proofEngineTypes.cmx tacticChaser.cmx tacticals.cmx variousTactics.cmi
+metadataQuery.cmo: primitiveTactics.cmi proofEngineTypes.cmi \
+ metadataQuery.cmi
+metadataQuery.cmx: primitiveTactics.cmx proofEngineTypes.cmx \
+ metadataQuery.cmi
+variousTactics.cmo: metadataQuery.cmi primitiveTactics.cmi \
+ proofEngineReduction.cmi proofEngineTypes.cmi tacticals.cmi \
+ variousTactics.cmi
+variousTactics.cmx: metadataQuery.cmx primitiveTactics.cmx \
+ proofEngineReduction.cmx proofEngineTypes.cmx tacticals.cmx \
+ variousTactics.cmi
introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmi \
introductionTactics.cmi
introductionTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx \
PACKAGE = tactics
REQUIRES = \
- pcre helm-cic_textual_parser helm-cic_proof_checking \
+ pcre helm-cic_proof_checking \
helm-cic_unification helm-mathql_interpreter helm-mathql_generator \
dbi helm-metadata
INTERFACE_FILES = \
- proofEngineTypes.mli newConstraints.mli match_concl.mli filter_auto.mli\
+ proofEngineTypes.mli \
proofEngineReduction.mli proofEngineHelpers.mli \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
- primitiveTactics.mli metadataQuery.mli tacticChaser.mli \
+ primitiveTactics.mli metadataQuery.mli \
variousTactics.mli \
introductionTactics.mli eliminationTactics.mli negationTactics.mli \
equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \
title:string -> msg:string -> string list -> string list) ref)
;;
-exception IllFormedUri of string
-
-let cic_textual_parser_uri_of_string uri' =
- try
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
- CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
- if String.sub uri' (String.length uri' - 4) 4 = ".var" then
- CicTextualParser0.VarUri (UriManager.uri_of_string uri')
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
- CicTextualParser0.IndTyUri (uri'',typeno)
- with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
- )
- with
- _ -> raise (IllFormedUri uri')
-;;
-
-(*
-let constructor_uri_of_string uri =
- match cic_textual_parser_uri_of_string uri with
- CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
- | _ -> assert false
-;;
-
-let call_back uris =
-(* N.B.: nella finestra c'e' un campo "nessuno deei precedenti, prova questo" che non ha senso? *)
-(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
-(* domanda: due triple possono essere diverse solo per avere exp_named_subst diverse?? *)
- let module U = UriManager in
- List.map
- (constructor_uri_of_string)
- (!interactive_user_uri_choice
- ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
- ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
- (List.map
- (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1))
- uris)
- )
-;;
-*)
-
let decompose_tac ?(uris_choice_callback=(function l -> l)) term =
let decompose_tac uris_choice_callback term status =
let (proof, goal) = status in
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-
-let in_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis'" ;;
-
-let main_hypothesis = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis'" ;;
-
-let main_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'" ;;
-
-let in_conclusion = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'" ;;
-
-let in_body = "'http://www.cs.unibo.it/helm/schemas/schema-helm#InBody'";;
-
-let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
-
-let hyp_const (conn:Mysql.dbd) uri =
- let uri = escape uri in
- (*query to obtain all the constants in the hypothesis and conclusion of the theorem*)
- let query =
- "select h_occurrence from refObj where source='"^uri^
- "' and (not (h_position ="^in_body^"))" in
- (*prerr_endline ("$$$$$$$$$$$$$$$"^query);*)
- let result = Mysql.exec conn query in
- (* now we transform the result in a set *)
- let f a =
- match (Array.to_list a) with
- [Some uri] -> uri
- | _ -> assert false in
- let result = Mysql.map ~f:f result in
- List.fold_left
- (fun set uri ->
- NewConstraints.StringSet.add uri set)
- NewConstraints.StringSet.empty result
-;;
-
-(* for each uri check if its costants are a subset of
- const, the set of the costants of the proof *)
-let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
- let hyp = hyp_const conn uri in
- (* prerr_endline (NewConstraints.pp_StringSet hyp);*)
- NewConstraints.StringSet.subset hyp const
-;;
-
-
-
-
-let rec exec_query (conn:Mysql.dbd) (uris,main) k =
- let add_must (n,from,where) uri =
- let refObjn = "refObj" ^ (string_of_int n) in
- let new_must =
- [ refObjn^".h_occurrence = '" ^ uri ^ "'";
- "(not ("^refObjn^".h_position ="^in_body^"))"] in
- let where' =
- if n = 0 then new_must@where
- else
- (refObjn^".source = refObj" ^ (string_of_int (n-1))
- ^ ".source")::new_must@where in
- (n+1,("refObj as "^refObjn)::from,where')
- in
- let (_,from,where) =
- List.fold_left add_must (0,[],[]) uris in
- let from,where =
- ["no_concl_hyp";"refObj as main"]@from,
- ["no=" ^ (string_of_int k);
- "no_concl_hyp.source = refObj0.source";
- "main.source = refObj0.source";
- "main.h_occurrence = '" ^ main ^ "'";
- "main.h_position = " ^ main_conclusion]@where
- in
- let from = String.concat "," from in
- let where = String.concat " and " where in
- let query = "select distinct(refObj0.source) from " ^ from ^ " where " ^ where in
- (*prerr_endline query;*)
- Mysql.exec conn query
-;;
-
-let powerset set =
- let rec powerset_r set sub =
- if (NewConstraints.StringSet.is_empty set) then sub
- else
- let a = NewConstraints.StringSet.min_elt set in
- let newset = NewConstraints.StringSet.remove a set in
- let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a)
- (NewConstraints.SetSet.fold
- (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t))
- sub NewConstraints.SetSet.empty)) sub in
- powerset_r newset newsub in
-powerset_r set NewConstraints.SetSet.empty
-;;
-
-let setset_to_listlist setset =
- let listset = NewConstraints.SetSet.elements setset in
- let res =
- List.map
- (fun set ->
- let el = NewConstraints.StringSet.elements set in
- (List.length el, el)) listset in
- (* ordered by descending cardinality *)
-List.sort (fun (n,_) (m,_) -> m - n) res
-
-let exist_element list_of_uris (_,uri) =
- let ex u =
- if u = uri then true
- else false
- in
-List.exists ex list_of_uris
-;;
-
-
-let filter_uris (conn:Mysql.dbd) const uris main =
- let subsets_of_consts =
- setset_to_listlist (powerset const) in
- let ex u =
- if u = main then true
- else false
- in
- let subsets_of_consts =
- List.filter
- (fun (_,b) -> (List.exists ex b))
- subsets_of_consts in
- let uris_of_const =
- List.concat
- (List.map
- (fun (m,s) ->
- (let res =
- exec_query conn (s,main) m in
- let f a =
- match (Array.to_list a) with
- [Some uri] -> uri
- | _ -> assert false in
- Mysql.map ~f:f res))
- subsets_of_consts)
- in
-List.filter (exist_element uris_of_const) uris
-;;
-
-let rec power n m =
- if (m = 1) then n
- else n*(power n (m-1))
-;;
-
-
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-val power:
- int -> int -> int
-
-val filter_new_constants:
- Mysql.dbd ->
- NewConstraints.StringSet.t ->
- int * string ->
- bool
-
-val filter_uris:
- Mysql.dbd ->
- NewConstraints.StringSet.t ->
- (int * string) list ->
- string ->
- (int * string) list
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(*********************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti, Matteo Selmi *)
-(* 1/04/2004 *)
-(* *)
-(* *)
-(*********************************************************************)
-
-
-(* the file contains:
- - functions executing must, just and only constraints on the mysql
- data base;
- - the general function cmatch for retrieving all statements matching
- a given conclusion
-*)
-
-type count_condition =
- NIL | EQ of int | GT of int
-;;
-
-let main_conclusion =
- "'http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion'"
-;;
-
-let in_conclusion =
- "'http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion'"
-;;
-
-let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
-
-
-let get_inconcl (conn:Mysql.dbd) uri =
- let uri = escape uri in
- let query =
- "select h_occurrence from refObj where source='"^uri^
- "' and (h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
- prerr_endline query;
- let result = Mysql.exec conn query in
- (* now we transform the result in a set *)
- let f a =
- match (Array.to_list a) with
- [Some uri] -> uri
- | _ -> assert false in
- let result = Mysql.map ~f:f result in
- List.fold_left
- (fun set uri ->
- NewConstraints.StringSet.add uri set)
- NewConstraints.StringSet.empty result
-;;
-
-let test_only (conn:Mysql.dbd) only u =
- let inconcl = get_inconcl conn u in
- NewConstraints.StringSet.subset inconcl only
-;;
-
-let rec exec_must (conn:Mysql.dbd) (l:MQGTypes.r_obj list) (cc:count_condition) =
- let add_must (n,from,where) (pos,uri) =
- match pos with
- `MainHypothesis _ -> assert false
- | `MainConclusion None ->
- let refObjn = "refObj" ^ (string_of_int n) in
- let new_must =
- [ refObjn^".h_occurrence = '" ^ uri ^ "'";
- refObjn^".h_position = " ^ main_conclusion] in
- let where' =
- if n = 0 then new_must@where
- else
- (refObjn^".source = refObj" ^ (string_of_int (n-1))
- ^ ".source")::new_must@where in
- (n+1,("refObj as "^refObjn)::from,where')
- | `MainConclusion(Some(d)) ->
- let refObjn = "refObj" ^ (string_of_int n) in
- let new_must =
- [ refObjn^".h_occurrence = '" ^ uri ^ "'";
- refObjn^".h_position = " ^ main_conclusion;
- refObjn^".h_depth = " ^ (string_of_int d)] in
- let where' =
- if n = 0 then new_must@where
- else
- (refObjn^".source = refObj" ^ (string_of_int (n-1))
- ^ ".source")::new_must@where in
- (n+1,("refObj as "^refObjn)::from,where')
- | `InHypothesis -> assert false
- | `InConclusion ->
- let refObjn = "refObj" ^ (string_of_int n) in
- let new_must =
- [ refObjn^".h_occurrence = '" ^ uri ^ "'";
- refObjn^".h_position = " ^ in_conclusion] in
- let where' =
- if n = 0 then new_must@where
- else
- (refObjn^".source = refObj" ^ (string_of_int (n-1))
- ^ ".source")::new_must@where in
- (n+1,("refObj as "^refObjn)::from,where')
- | `InBody -> assert false
- in
- let (_,from,where) =
- List.fold_left add_must (0,[],[]) l in
- let from,where =
- (match cc with
- NIL -> from, where
- | EQ n ->
- "no_inconcl_aux"::from,
- ("no=" ^ (string_of_int n))::
- ("no_inconcl_aux.source = refObj0.source")::where
- | GT n ->
- "no_inconcl_aux"::from,
- ("no>" ^ (string_of_int n))::
- ("no_inconcl_aux.source = refObj0.source")::where) in
- let from = String.concat "," from in
- let where = String.concat " and " where in
- let query =
- "select refObj0.source from " ^ from ^ " where " ^ where in
- (* prerr_endline query;*)
- Mysql.exec conn query
-;;
-
-
-let (must_of_prefix m s):MQGTypes.r_obj list =
- let s' = List.map (fun u -> (`InConclusion, u)) s in
- (`MainConclusion None,m)::s'
-;;
-
-(* takes a list of lists and returns the list of all elements
- without repetitions *)
-let union l =
- let rec drop_repetitions = function
- [] -> []
- | [a] -> [a]
- | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
- | u::l -> u::(drop_repetitions l) in
- drop_repetitions (List.sort Pervasives.compare (List.concat l))
-;;
-
-let critical_value = 6;;
-let just_factor = 3;;
-
-let cmatch (conn:Mysql.dbd) t =
- let eq,constants = NewConstraints.constants_of t in
- (* the type of eq is not counted in constants_no *)
- let constants_no =
- if eq then (NewConstraints.StringSet.cardinal constants)
- else (NewConstraints.StringSet.cardinal constants) in
- if (constants_no > critical_value) then
- let prefixes = NewConstraints.prefixes just_factor t in
- (match prefixes with
- Some main, all_concl ->
-(*
- NewConstraints.pp_prefixes all_concl;
-*)
- (* in some cases, max_prefix_length could be less than n *)
- let max_prefix_length =
- match all_concl with
- [] -> assert false
- | (max,_)::_ -> max in
- let maximal_prefixes =
- let rec filter res = function
- [] -> res
- | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
- | _::_-> res in
- filter [] all_concl in
- let greater_than :(int*string) list=
- let all =
- union
- (List.map
- (fun (m,s) ->
- (let res =
- exec_must conn (must_of_prefix main s) (GT (m+1)) in
- let f a =
- match (Array.to_list a) with
- (* we tag the uri with m+1, for sorting purposes *)
- [Some uri] -> (m+1,uri)
- | _ -> assert false in
- Mysql.map ~f:f res))
- maximal_prefixes) in
- List.filter
- (function (_,uri) -> test_only conn constants uri) all in
- let equal_to =
- List.concat
- (List.map
- (fun (m,s) ->
- (let res =
- exec_must conn (must_of_prefix main s) (EQ (m+1)) in
- let f a =
- match (Array.to_list a) with
- (* we tag the uri with m, for sorting purposes *)
- [Some uri] -> (m,uri)
- | _ -> assert false in
- Mysql.map ~f:f res))
- all_concl) in
- greater_than @ equal_to
- | _, _ -> [])
- else if constants_no = 0 then []
- else
- (* in this case we compute all prefixes, and we do not need
- to apply the only constraints *)
- let prefixes = NewConstraints.prefixes constants_no t in
- (match prefixes with
- Some main, all_concl ->
- List.concat
- (List.map
- (fun (m,s) ->
- (let res =
- exec_must conn (must_of_prefix main s) (EQ (m+1)) in
- let f a =
- match (Array.to_list a) with
- (* we tag the uri with m, for sorting purposes *)
- [Some uri] -> (m,uri)
- | _ -> assert false in
- Mysql.map ~f:f res))
- all_concl)
- | _, _ -> [])
-;;
-
-
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(*********************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti, Matteo Selmi *)
-(* 1/04/2004 *)
-(* *)
-(* *)
-(*********************************************************************)
-
-
-type count_condition =
- NIL | EQ of int | GT of int
-
-val exec_must :
- Mysql.dbd ->
- MQGTypes.r_obj list ->
- count_condition ->
- Mysql.result
-
-val cmatch :
- Mysql.dbd ->
- Cic.term ->
- (int*string) list
let locate ~(dbh:Dbi.connection) name =
let query =
- dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\""
+ dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
MetadataTypes.name_tbl name)
in
query#execute [];
let full_signature =
List.fold_right Constr.StringSet.add main_uris constants
in
- List.filter (Constr.at_most ~dbh full_signature) uris
+ List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris
let filter_uris_backward ~dbh signature uris =
let siguris =
in
intersect uris siguris
+let compare_goal_list proof goal1 goal2 =
+ let _,metasenv,_,_ = proof in
+ let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+ let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
+ let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+ let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+ let prop1 =
+ if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
+ else 1
+ in
+ let prop2 =
+ if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
+ else 1
+ in
+ prop1 - prop2
+
let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
end else
filter_uris_backward ~dbh (main, other_constants) uris
in
- List.map
- (fun uri ->
- (uri,
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
- status))
- uris
+prerr_endline "URIS";
+List.iter prerr_endline uris;
+ let rec aux = function
+ | [] -> []
+ | uri :: tl ->
+ (let status' =
+ try
+ let (proof, goal_list) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
+ status
+ in
+ let goal_list =
+ List.stable_sort (compare_goal_list proof) goal_list
+ in
+ Some (uri, (proof, goal_list))
+ with ProofEngineTypes.Fail _ -> None
+ in
+ match status' with
+ | None -> aux tl
+ | Some status' ->
+ prerr_endline ("HO APPLICATO " ^ uri);
+ status' :: aux tl)
+ in
+ aux uris
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(*********************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti <asperti@cs.unibo.it> *)
-(* 18/03/2004 *)
-(* *)
-(* *)
-(*********************************************************************)
-
-(* the file contains functions for computing prefixes and related
- stuff, required by the new management of matching *)
-
-module SortedString =
- struct
- type t = string
- let compare = Pervasives.compare
- end
-;;
-
-module StringSet = Set.Make (SortedString)
-;;
-
-module SetSet = Set.Make (StringSet)
-;;
-
-
-(*
- module SetSet :
- sig
- type elt = StringSet.t
- and t = Set.Make(StringSet).t
- val empty : t
- val is_empty : t -> bool
- val mem : elt -> t -> bool
- val add : elt -> t -> t
- val singleton : elt -> t
- val remove : elt -> t -> t
- val union : t -> t -> t
- val inter : t -> t -> t
- val diff : t -> t -> t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val subset : t -> t -> bool
- val iter : (elt -> unit) -> t -> unit
- val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
- val for_all : (elt -> bool) -> t -> bool
- val exists : (elt -> bool) -> t -> bool
- val filter : (elt -> bool) -> t -> t
- val partition : (elt -> bool) -> t -> t * t
- val cardinal : t -> int
- val elements : t -> elt list
- val min_elt : t -> elt
- val max_elt : t -> elt
- val choose : t -> elt
- end
-*)
-
-let pp_StringSet set =
- if (StringSet.is_empty set) then "EMPTY"
- else
- "{" ^ (String.concat "," (StringSet.elements set)) ^ "}"
-;;
-
-let pp_SetSet set =
- let el = List.map pp_StringSet (SetSet.elements set) in
- "{" ^ (String.concat ",\n" el) ^ "}"
-;;
-
-let pp_prefix (n,l) =
- (string_of_int n) ^
- ": {" ^ (String.concat "," l) ^ "}"
-
-let pp_prefixes l =
- let el = List.map pp_prefix l in
- "{" ^ (String.concat ",\n" el) ^ "}"
-
-
-
-let filter_by_card n =
- SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
-;;
-
-let merge n a b =
- let init = SetSet.union a b in
- let merge_single_set s1 b =
- SetSet.fold
- (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
- b SetSet.empty in
- let res =
- SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
- in
- filter_by_card n res
-;;
-
-let mutinduri u t =
- (UriManager.string_of_uri u) ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ ")"
-;;
-
-let mutconstructuri u t c =
- (UriManager.string_of_uri u)
- ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ "/" ^ (string_of_int c) ^ ")"
-;;
-
-let rec inspect_children n childs =
- List.fold_left
- (fun res term -> merge n (inspect_conclusion n term) res)
- SetSet.empty childs
-
-and add_root n root childs =
- let childunion = inspect_children n childs in
- let addroot = StringSet.add root in
- SetSet.fold
- (fun child newsets -> SetSet.add (addroot child) newsets)
- childunion
- (SetSet.singleton (StringSet.singleton root))
-
-and inspect_conclusion n t =
-if n = 0 then SetSet.empty
-else match t with
- Cic.Rel _
- | Cic.Meta _
- | Cic.Sort _
- | Cic.Implicit _ -> SetSet.empty
- | Cic.Var (u,exp_named_subst) -> SetSet.empty
- | Cic.Const (u,exp_named_subst) ->
- SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
- | Cic.MutInd (u, t, exp_named_subst) ->
- SetSet.singleton (StringSet.singleton (mutinduri u t))
- | Cic.MutConstruct (u, t, c, exp_named_subst) ->
- SetSet.singleton (StringSet.singleton (mutconstructuri u t c))
- | Cic.Cast (t, _) -> inspect_conclusion n t
- | Cic.Prod (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.Lambda (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.LetIn (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = UriManager.string_of_uri u in
- add_root (n-1) suri l
- | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = mutinduri u t in
- add_root (n-1) suri l
- | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = mutconstructuri u t c in
- add_root (n-1) suri l
- | Cic.Appl l ->
- SetSet.empty
- | Cic.MutCase (u, t, tt, uu, m) ->
- SetSet.empty
- | Cic.Fix (_, m) ->
- SetSet.empty
- | Cic.CoFix (_, m) ->
- SetSet.empty
-;;
-
-let rec inspect_term n t =
-if n = 0 then assert false
-else match t with
- Cic.Rel _
- | Cic.Meta _
- | Cic.Sort _
- | Cic.Implicit _ -> None, SetSet.empty
- | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
- | Cic.Const (u,exp_named_subst) ->
- Some (UriManager.string_of_uri u), SetSet.empty
- | Cic.MutInd (u, t, exp_named_subst) ->
- Some (mutinduri u t), SetSet.empty
- | Cic.MutConstruct (u, t, c, exp_named_subst) ->
- Some (mutconstructuri u t c), SetSet.empty
- | Cic.Cast (t, _) -> inspect_term n t
- | Cic.Prod (_, _, t) -> inspect_term n t
- | Cic.LetIn (_, _, t) -> inspect_term n t
- | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = UriManager.string_of_uri u in
- let childunion = inspect_children (n-1) l in
- Some suri, childunion
- | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = mutinduri u t in
- if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
- (* equality is handled in a special way: in particular,
- the type, if defined, is always added to the prefix,
- and n is not decremented - it should have been n-2 *)
- match l with
- Cic.Const (u1,exp_named_subst1)::l1 ->
- let suri1 = UriManager.string_of_uri u1 in
- let inconcl = add_root (n-1) suri1 l1 in
- Some suri, inconcl
- | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
- let suri1 = mutinduri u1 t1 in
- let inconcl = add_root (n-1) suri1 l1 in
- Some suri, inconcl
- | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
- let suri1 = mutconstructuri u1 t1 c1 in
- let inconcl = add_root (n-1) suri1 l1 in
- Some suri, inconcl
- | _ :: _ -> Some suri, SetSet.empty
- | _ -> assert false (* args number must be > 0 *)
- else
- let childunion = inspect_children (n-1) l in
- Some suri, childunion
- | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = mutconstructuri u t c in
- let childunion = inspect_children (n-1) l in
- Some suri, childunion
- | _ -> None, SetSet.empty
-
-let rec add uri children =
- List.fold_left
- (fun acc t ->
- StringSet.union (constants_concl t) acc)
- (StringSet.singleton uri) children
-
-(* this function creates the set of all different constants appearing in
- the conclusion of the term *)
-and constants_concl =
- function
- Cic.Rel _
- | Cic.Meta _
- | Cic.Sort _
- | Cic.Implicit _ -> StringSet.empty
- | Cic.Var (u,exp_named_subst) -> StringSet.empty
- | Cic.Const (u,exp_named_subst) ->
- StringSet.singleton (UriManager.string_of_uri u)
- | Cic.MutInd (u, t, exp_named_subst) ->
- StringSet.singleton (mutinduri u t)
- | Cic.MutConstruct (u, t, c, exp_named_subst) ->
- StringSet.singleton (mutconstructuri u t c)
- | Cic.Cast (t, _) -> constants_concl t
- | Cic.Prod (_, s, t) ->
- StringSet.union (constants_concl s) (constants_concl t)
- | Cic.Lambda (_, s, t) ->
- StringSet.union (constants_concl s) (constants_concl t)
- | Cic.LetIn (_, s, t) ->
- StringSet.union (constants_concl s) (constants_concl t)
- | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
- let suri = UriManager.string_of_uri u in
- add suri l
- | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
- let suri = mutinduri u t in
- add suri l
- | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
- let suri = mutconstructuri u t c in
- add suri l
- | Cic.Appl l ->
- StringSet.empty
- | Cic.MutCase (u, t, tt, uu, m) ->
- StringSet.empty
- | Cic.Fix (_, m) ->
- StringSet.empty
- | Cic.CoFix (_, m) ->
- StringSet.empty
-;;
-
-(* (constants_of t) returns a pair (b,n) where n is the number of
- constants in the conclusion of t, and b is true if in MainConclusion
- we have an equality *)
-
-let rec constants_of = function
- | Cic.Cast (t, _) -> constants_of t
- | Cic.Prod (_, _, t) -> constants_of t
- | Cic.LetIn (_, _, t) -> constants_of t
- | (Cic.Appl ((Cic.MutInd (u, _, _))::l)) as t when
- u = HelmLibraryObjects.Logic.eq_URI ->
- (true, constants_concl t)
- | t -> (false, constants_concl t)
-;;
-
-
-let add_cardinality s =
- let l = SetSet.elements s in
- let res =
- List.map
- (fun set ->
- let el = StringSet.elements set in
- (List.length el, el)) l in
- (* ordered by descending cardinality *)
- List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
-;;
-
-let prefixes n t =
- match inspect_term n t with
- Some a, set -> Some a, add_cardinality set
- | None, set when (SetSet.is_empty set) -> None, []
- | _, _ -> assert false
-;;
-
-let mainandcons t =
- let const = constants_concl t in
- match prefixes 1 t with
- Some main, _ -> main, const
- | _,_ -> assert false
-;;
-
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(*********************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Andrea Asperti <asperti@cs.unibo.it> *)
-(* 18/03/2004 *)
-(* *)
-(* *)
-(*********************************************************************)
-
-
-module StringSet : Set.S with type elt = string
-
-module SetSet : Set.S with type elt = StringSet.t
-
-val pp_SetSet : SetSet.t -> string
-
-val pp_StringSet : StringSet.t -> string
-
-
-
-val inspect_term : int -> Cic.term -> string option * SetSet.t
-
-val prefixes : int -> Cic.term -> string option * ((int * (StringSet.elt list)) list)
-
-(* (constants_of t) returns a pair (b,n) where n is the set of the
- constants in the conclusion of t, and b is true if in MainConclusion
- we have an equality *)
-
-val constants_of : Cic.term -> bool * StringSet.t
-
-val constants_concl : Cic.term -> StringSet.t
-
-val pp_prefixes : ((int * (StringSet.elt list)) list) -> string
-
-val mainandcons : Cic.term -> (string * StringSet.t)
let saved_univ = CicUniv.get_working() in
try
t status
- with Fail s -> CicUniv.set_working saved_univ; raise (Fail s)
+ with Fail s ->
+ CicUniv.set_working saved_univ;
+ raise (Fail s)
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-(*****************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 18/02/2003 *)
-(* *)
-(* *)
-(*****************************************************************************)
-
-module MQI = MQueryInterpreter
-module MQIC = MQIConn
-module I = MQueryInterpreter
-module U = MQGUtil
-module G = MQueryGenerator
-
- (* search arguments on which Apply tactic doesn't fail *)
-let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
- let ((_, metasenv, _, _), metano) = status in
- let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
- let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
-match list_of_must with
- [] -> []
-|_ ->
- let must = choose_must list_of_must only in
- let result =
- I.execute mqi_handle
- (G.query_of_constraints
- (Some CGMatchConclusion.universe)
- (must,[],[]) (Some only,None,None)) in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result
- in
- let uris =
- (* TODO ristretto per ragioni di efficienza *)
- prerr_endline "STO FILTRANDO";
- List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
- in
- prerr_endline "HO FILTRATO";
- let uris',exc =
- let rec filter_out =
- function
- [] -> [],""
- | uri::tl ->
- let tl',exc = filter_out tl in
- try
- if
- let time = Unix.gettimeofday() in
- (try
- ignore(ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac
- ~term:(MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri)))
- status);
- let time1 = Unix.gettimeofday() in
- prerr_endline (Printf.sprintf "%1.3f" (time1 -. time) );
- true
- with ProofEngineTypes.Fail _ ->
- let time1 = Unix.gettimeofday() in
- prerr_endline (Printf.sprintf "%1.3f" (time1 -. time)); false)
- then
- uri::tl',exc
- else
- tl',exc
- with
- (ProofEngineTypes.Fail _) as e ->
- let exc' =
- "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
- uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
- in
- tl',exc'
- in
- filter_out uris
- in
- let html' =
- " <h1>Objects that can actually be applied: </h1> " ^
- String.concat "<br>" uris' ^ exc ^
- " <h1>Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
- " <h1>Number of good matches: " ^
- string_of_int (List.length uris') ^ "</h1>"
- in
- output_html html' ;
- uris'
-;;
-
-
-(*matchConclusion modificata per evitare una doppia apply*)
-let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
- let ((_, metasenv, _, _), metano) = status in
- let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
- let conn =
- match mqi_handle.MQIConn.pgc with
- MQIConn.MySQL_C conn -> conn
- | _ -> assert false in
- let uris = Match_concl.cmatch conn ty in
- (* List.iter
- (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
- (* delete all .var uris *)
- let isvar (_,s) =
- let len = String.length s in
- let suffix = String.sub s (len-4) 4 in
- not (suffix = ".var") in
- let uris = List.filter isvar uris in
- (* delete all not "cic:/Coq" uris *)
- (*
- let uris =
- (* TODO ristretto per ragioni di efficienza *)
- List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
- *)
- (* concl_cost are the costants in the conclusion of the proof
- while hyp_const are the constants in the hypothesis *)
- let (main_concl,concl_const) = NewConstraints.mainandcons ty in
- prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris));
- let hyp t set =
- match t with
- Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
- | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
- | _ -> set in
- let hyp_const =
- List.fold_right hyp ey NewConstraints.StringSet.empty in
- prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
- (* uris with new constants in the proof are filtered *)
- let all_const = NewConstraints.StringSet.union hyp_const concl_const in
- let uris =
- if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
- then
- (prerr_endline("metodo vecchio");List.filter (Filter_auto.filter_new_constants conn all_const) uris)
- else Filter_auto.filter_uris conn all_const uris main_concl in
-(*
- let uris =
- (* ristretto all cache *)
- prerr_endline "SOLO CACHE";
- List.filter
- (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
- in
- prerr_endline "HO FILTRATO2";
-*)
- let uris =
- List.map
- (fun (n,u) ->
- (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
- uris in
- let uris' =
- let rec filter_out =
- function
- [] -> []
- | (m,uri)::tl ->
- let tl' = filter_out tl in
- try
- prerr_endline ("STO APPLICANDO " ^ uri);
- let res = (m,
- (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
- ~term:(MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri)))
- status))::tl' in
- prerr_endline ("OK");res
- (* with ProofEngineTypes.Fail _ -> tl' *)
- (* patch to cover CSC's exportation bug *)
- with _ -> prerr_endline ("FAIL");tl'
- in
- prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris));
- filter_out uris
- in
- prerr_endline ("Ne sono rimasti 3 " ^ string_of_int (List.length uris'));
-
- uris'
-;;
-
-(*funzione che sceglie il penultimo livello di profondita' dei must*)
-
-(*
-let choose_must list_of_must only=
-let n = (List.length list_of_must) - 1 in
- List.nth list_of_must n
-;;*)
-
-(* questa prende solo il main *)
-let choose_must list_of_must only =
- List.nth list_of_must 0
-
-(* livello 1
-let choose_must list_of_must only =
- try
- List.nth list_of_must 1
- with _ ->
- List.nth list_of_must 0 *)
-
-let searchTheorems mqi_handle (proof,goal) =
- let subproofs =
- matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
- let res =
- List.sort
- (fun (n1,(_,gl1)) (n2,(_,gl2)) ->
- let l1 = List.length gl1 in
- let l2 = List.length gl2 in
- (* if the list of subgoals have the same lenght we use the
- prefix tag, where higher tags have precedence *)
- if l1 = l2 then n2 - n1
- else l1 - l2)
- subproofs
- in
- (* now we may drop the prefix tag *)
- (*let res' =
- List.map snd res in*)
- let order_goal_list proof goal1 goal2 =
- let _,metasenv,_,_ = proof in
- let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
- let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
-(*
- prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
-*)
- let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
-(*
- prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
-*)
- let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
-(*
- prerr_endline "DOPO LA SECONDA TYPE OF " ;
-*)
- let prop1 = if CicReduction.are_convertible
- ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
- else 1 in
- let prop2 = if CicReduction.are_convertible
- ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
- else 1 in
- prop1 - prop2 in
- List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res
-;;
-
+++ /dev/null
-(* Copyright (C) 2000-2002, 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/.
- *)
-
-val matchConclusion : MQIConn.handle ->
- ?output_html:(string -> unit) ->
- choose_must:(MQGTypes.r_obj list list ->
- MQGTypes.r_obj list ->
- MQGTypes.r_obj list) ->
- unit -> ProofEngineTypes.status -> string list
-
-
-(* TODO: OLD CODE TO BE REMOVED
-val searchTheorem : ProofEngineTypes.status -> ProofEngineTypes.proof * ProofEngineTypes.goal list
-*)
-
-val searchTheorems:
- MQIConn.handle -> ProofEngineTypes.status ->
- (ProofEngineTypes.proof * ProofEngineTypes.goal list) list
-
exception NoOtherChoices;;
-let rec auto_new mqi_handle = function
+let rec auto_new dbh = function
[] -> raise NoOtherChoices
| (proof, [])::tl -> (proof, [])::tl
- | (proof, (goal,0)::gtl)::tl -> auto_new mqi_handle tl
+ | (proof, (goal,0)::gtl)::tl -> auto_new dbh tl
| (proof, (goal,depth)::gtl)::tl ->
- let _,metasenv,_,_ = proof in
+ let _,metasenv,proof_obj,_ = proof in
let meta_inf =
(try
let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
Some (ey, ty) ->
prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+ prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj));
let local_choices =
new_search_theorems
search_theorems_in_context proof goal (depth-1) gtl in
let global_choices =
new_search_theorems
- (TacticChaser.searchTheorems mqi_handle)
+ (fun status -> List.map snd (MetadataQuery.hint ~dbh status))
+(* (TacticChaser.searchTheorems mqi_handle) *)
proof goal (depth-1) gtl in
let all_choices =
local_choices@global_choices@tl in
let reorder =
List.stable_sort sorting_list all_choices
in
- auto_new mqi_handle reorder
- | None -> auto_new mqi_handle ((proof,gtl)::tl)
+ auto_new dbh reorder
+ | None -> auto_new dbh ((proof,gtl)::tl)
;;
-let auto_tac mqi_handle =
+let auto_tac ~(dbh:Dbi.connection) =
(* CicMetaSubst.reset_counters (); *)
- let auto_tac mqi_handle (proof,goal) =
+ let auto_tac dbh (proof,goal) =
prerr_endline "Entro in Auto";
try
- (match auto_new mqi_handle [(proof, [(goal,depth)])] with
+ (match auto_new dbh [(proof, [(goal,depth)])] with
| (proof,_)::_ ->
prerr_endline "AUTO_TAC HA FINITO";
(* CicMetaSubst.print_counters (); *)
prerr_endline("Auto failed");
raise (ProofEngineTypes.Fail "No Applicable theorem")
in
- ProofEngineTypes.mk_tactic (auto_tac mqi_handle)
+ ProofEngineTypes.mk_tactic (auto_tac dbh)
;;
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
ProofEngineTypes.tactic
-val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic
+(* val auto_tac : MQIConn.handle -> ProofEngineTypes.tactic *)
+val auto_tac : dbh:Dbi.connection -> ProofEngineTypes.tactic
projects / helm.git / commitdiff