proofEngineReduction.cmx: proofEngineReduction.cmi
proofEngineHelpers.cmo: proofEngineHelpers.cmi
proofEngineHelpers.cmx: proofEngineHelpers.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
tacticals.cmo: proofEngineTypes.cmo tacticals.cmi
tacticals.cmx: proofEngineTypes.cmx tacticals.cmi
reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi
primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \
primitiveTactics.cmi
-tacticChaser.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi
-tacticChaser.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi
+tacticChaser.cmo: match_concl.cmi primitiveTactics.cmi proofEngineTypes.cmo \
+ tacticChaser.cmi
+tacticChaser.cmx: match_concl.cmx primitiveTactics.cmx proofEngineTypes.cmx \
+ tacticChaser.cmi
variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \
proofEngineTypes.cmo tacticChaser.cmi tacticals.cmi variousTactics.cmi
variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \
INTERFACE_FILES = \
proofEngineReduction.mli proofEngineHelpers.mli \
+ newConstraints.mli match_concl.mli \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli tacticChaser.mli variousTactics.mli \
introductionTactics.mli eliminationTactics.mli negationTactics.mli \
--- /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
prerr_endline "STO FILTRANDO";
List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
in
- prerr_endline "HO FILTRATO";
+ prerr_endline "HO FILTRATO";
let uris',exc =
let rec filter_out =
function
| uri::tl ->
let tl',exc = filter_out tl in
try
- if
+ if
+ let time = Unix.gettimeofday() in
(try
ignore
- (PrimitiveTactics.apply_tac
- ~term:(MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri))
- status);
- true
- with ProofEngineTypes.Fail _ -> false)
+ (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
(*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 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 ((_, 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 result = Match_concl.cmatch conn ty in
+ List.iter
+ (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result
- in
+ List.map
+ (fun (n,u) ->
+ (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
+ result in
+ 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
+ let uris =
+ (* TODO ristretto per ragioni di efficienza *)
+ prerr_endline "STO FILTRANDO2";
+ List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+(*
let uris =
(* TODO ristretto per ragioni di efficienza *)
prerr_endline "STO FILTRANDO2";
List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
in
- 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
+ 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' =
let rec filter_out =
function
[] -> []
- | uri::tl ->
- let tl' = filter_out tl in
- try
- ((PrimitiveTactics.apply_tac
- ~term:(MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri))
- status)::tl')
- with ProofEngineTypes.Fail _ -> tl'
+ | (m,uri)::tl ->
+ let tl' = filter_out tl in
+ try
+ (m,
+ (prerr_endline ("STO APPLICANDO " ^ uri);
+ (PrimitiveTactics.apply_tac
+ ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string uri))
+ status)))::tl'
+ (* with ProofEngineTypes.Fail _ -> tl' *)
+ (* patch to cover CSC's exportation bug *)
+ with _ -> tl'
in
- prerr_endline (string_of_int (List.length uris));
+ prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
filter_out uris
in
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 =
- List.nth list_of_must 0
+ try
+ List.nth list_of_must 1
+ with _ ->
+ List.nth list_of_must 0 *)
(* OLD CODE: TO BE REMOVED
(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
let searchTheorems mqi_handle (proof,goal) =
(*prerr_endline "1";*)
- let uris' =
+ let subproofs =
matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
-prerr_endline (string_of_int (List.length uris'));
-(*prerr_endline "2";*)
-(* let list_of_termin =
- List.map
- (function string ->
- (MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string string)))
- uris' in
-prerr_endline "3";
- let list_proofgoal =
- List.map
- (function term ->
- PrimitiveTactics.apply_tac ~term (proof,goal)) list_of_termin in*)
-(*prerr_endline "4";*)
-let res =
+ let res =
List.sort
- (fun (_,gl1) (_,gl2) ->
- Pervasives.compare (List.length gl1) (List.length gl2))
- uris'
- in
-(*prerr_endline "5";*)
-res
+ (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 *)
+ List.map snd res
+
+
;;
prerr_endline ("SIAM QUI = " ^ s); []
;;
-
+exception NotAProposition;;
exception NotApplicableTheorem;;
exception MaxDepth;;
-let depth = 5;;
+let depth = 3;;
-let rec auto_tac mqi_handle level proof goal =
-prerr_endline "Entro in Auto_rec";
+let rec auto_tac_aux mqi_handle level proof goal =
+prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level));
if level = 0 then
(* (proof, [goal]) *)
- (prerr_endline ("NON ci credo");
+ (prerr_endline ("MaxDepth");
raise MaxDepth)
else
- (* choices is a list of pairs proof and goallist *)
- let choices =
- (search_theorems_in_context (proof,goal))@
- (TacticChaser.searchTheorems mqi_handle (proof,goal))
- in
- let rec try_choices = function
- [] -> raise NotApplicableTheorem
- | (proof,goallist)::tl ->
+ (* let us verify that the metavariable is still an open goal --
+ it could have been closed by closing other goals -- and that
+ it is of sort Prop *)
+ let _,metasenv,_,_ = proof in
+ let meta_inf =
+ (try
+ let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+ Some (ey, ty)
+ with _ -> None) in
+ match meta_inf with
+ Some (ey, ty) ->
+ prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+ (*
+ let time1 = Unix.gettimeofday() in
+ let _, all_paths = NewConstraints.prefixes 5 ty in
+ let time2 = Unix.gettimeofday() in
+ prerr_endline
+ (Printf.sprintf "TEMPO DI CALCOLO = %1.3f" (time2 -. time1) );
+ prerr_endline
+ ("ALL PATHS: n = " ^ string_of_int
+ (List.length all_paths));
+ prerr_endline (NewConstraints.pp_prefixes all_paths);
+ *)
+ (* if the goal does not have a sort Prop we return the
+ current proof and a list containing the goal *)
+ let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in
+ if CicReduction.are_convertible
+ ey (Cic.Sort Cic.Prop) ty_sort then
+ (* sort Prop *)
+ (* choices is a list of pairs proof and goallist *)
+ let choices =
+ (search_theorems_in_context (proof,goal))@
+ (TacticChaser.searchTheorems mqi_handle (proof,goal))
+ in
+ let rec try_choices = function
+ [] -> raise NotApplicableTheorem
+ | (proof,goallist)::tl ->
prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
- (try
- List.fold_left
- (fun proof goal ->
- (* It may happen that to close the first open goal
- also some other goals are closed *)
- let _,metasenv,_,_ = proof in
- if List.exists (fun (i,_,_) -> i = goal) metasenv then
- let newproof =
- auto_tac mqi_handle (level-1) proof goal
- in
- newproof
- else
- (* goal already closed *)
- proof)
- proof goallist
- with
- | MaxDepth
- | NotApplicableTheorem ->
- try_choices tl) in
- try_choices choices;;
+ (try
+ List.fold_left
+ (fun proof goal ->
+ auto_tac_aux mqi_handle (level-1) proof goal)
+ proof goallist
+ with
+ | MaxDepth
+ | NotApplicableTheorem
+ | NotAProposition ->
+ try_choices tl) in
+ try_choices choices
+ else
+ (* CUT AND PASTE DI PROVA !! *)
+ let choices =
+ (search_theorems_in_context (proof,goal))@
+ (TacticChaser.searchTheorems mqi_handle (proof,goal))
+ in
+ let rec try_choices = function
+ [] -> raise NotApplicableTheorem
+ | (proof,[])::tl -> proof
+ | _::tl -> try_choices tl in
+ try_choices choices
+ (* raise NotAProposition *)
+ | None -> proof
+;;
let auto_tac mqi_handle (proof,goal) =
prerr_endline "Entro in Auto";
try
- let proof = auto_tac mqi_handle depth proof goal in
+ let proof = auto_tac_aux mqi_handle depth proof goal in
prerr_endline "AUTO_TAC HA FINITO";
(proof,[])
with
projects / helm.git / commitdiff