(* *)
(******************************************************************************)
+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 searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
let ((_, metasenv, _, _), metano) = status in
- let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let list_of_must,only = MQueryLevels.out_restr metasenv ey ty 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 torigth_restriction (u,b) =
- let p =
- if b then
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- else
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
+ prerr_endline "123";
+ let result =
+ I.execute mqi_handle
+ (G.query_of_constraints
+ (Some CGMatchConclusion.universe)
+ (must,[],[]) (Some only,None,None)) in
+ prerr_endline "456";
+ 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
+ (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)
+ 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
- (u,p,None)
+ filter_out uris
in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) 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 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 =
- MQueryInterpreter.execute mqi_handle
- (MQueryGenerator.query_of_constraints
- (Some
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"])
- (rigth_must,[],[]) (rigth_only,None,None)) in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let uris',exc =
- let rec filter_out =
- function
- [] -> [],""
- | uri::tl ->
- let tl',exc = filter_out tl in
- try
- if
- (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)
- 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'
+ 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 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
+ 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'
+ in
+ prerr_endline (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
+;;*)
+
+let choose_must list_of_must only =
+ 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*)
+(*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
+
+exception NotInTheList;;
+
+
+let position n =
+ let rec aux k =
+ function
+ [] -> raise NotInTheList
+ | m::_ when m=n -> k
+ | _::tl -> aux (k+1) tl in
+ aux 1
+;;
+
+
+
+(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
+(*generate the less number of subgoals*)
+
+let searchTheorem (proof,goal) =
+ let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+ in
+ let mqi_handle = MQIC.init mqi_flags prerr_string
+in
+ let uris' =
+ matchConclusion
+ mqi_handle ~choose_must() (proof, goal)
+ in
+ 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
+ let list_proofgoal =
+ List.map
+ (function term ->
+ PrimitiveTactics.apply_tac ~term (proof,goal))
+ list_of_termin
+ in
+ let (list_of_subgoal: int list list) =
+ List.map snd list_proofgoal
+ in
+ let list_of_num =
+ List.map List.length list_of_subgoal
+ in
+ let list_sort =
+ List.sort Pervasives.compare list_of_num
+ in (*ordino la lista in modo cresc*)
+ let min= List.nth list_sort 0 (*prendo il minimo*)
+ in
+ let uri' = (*cerco il teo di pos k*)
+ List.nth list_of_termin (position min list_of_num)
+ in
+ (* let teo=
+ String.sub uri' 4 (String.length uri' - 4)
+
+ (* modifico la str in modo che sia accettata da apply*)
+ in*)
+ PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
+;;
+*)
+
+
+let searchTheorems mqi_handle (proof,goal) =
+(*prerr_endline "1";*)
+ let uris' =
+ 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 =
+ List.sort
+ (fun (_,gl1) (_,gl2) ->
+ Pervasives.compare (List.length gl1) (List.length gl2))
+ uris'
+ in
+(*prerr_endline "5";*)
+res
;;
projects / helm.git / blobdiff