module MQI = MQueryInterpreter
module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
+ ProofEngine.proof := Some(uri,metasenv,bo,ty);
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
GBin.scrolled_window ~border_width:10 ~height ~width:600
~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+ let mutable_ref = ref (Some d) in
+ let depthb =
+ GButton.toggle_button
+ ~label:("depth = " ^ string_of_int d)
+ ~active:true
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore
+ (depthb#connect#toggled
+ (function () ->
+ let sel_depth = if depthb#active then Some d else None in
+ mutable_ref := sel_depth
+ )) ; mutable_ref
+ in
let rel_constraints =
List.map
- (function (position,depth) ->
+ (function p ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:position
+ ~text:(MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button
- ~label:("depth = " ^ string_of_int depth') ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
) must_rel in
(* Sort constraints *)
let label =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let sort_constraints =
List.map
- (function (position,depth,sort) ->
+ (function (p, sort) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(sort ^ " " ^ position)
+ ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None, sort
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref, sort
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, sort
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort
) must_sort in
(* Obj constraints *)
let label =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let obj_constraints =
List.map
- (function (uri,position,depth) ->
+ (function (p, uri) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(uri ^ " " ^ position)
+ ~text:(uri ^ " " ^ (MQGU.text_of_position p))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> uri, position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- uri, position, mutable_ref
+ match p with
+ | `InBody
+ | `InHypothesis
+ | `InConclusion
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, uri
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
) must_obj in
(* Confirm/abort buttons *)
let hbox =
if !chosen then
let chosen_must_rel =
List.map
- (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+ (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+ rel_constraints
+ in
let chosen_must_sort =
List.map
- (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+ (function (position, ref_depth, sort) ->
+ MQGU.set_main_position position !ref_depth,sort)
sort_constraints
in
let chosen_must_obj =
List.map
- (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+ (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
obj_constraints
in
(chosen_must_obj,chosen_must_rel,chosen_must_sort),
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
- let must = MQueryLevels2.get_constraints expr in
+ let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
- MQG.query_of_constraints
- (Some
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
- ])
- must' only
+ MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:false n
) must
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:true n
) only
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.searchPattern
+ TacticChaser.matchConclusion
mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
let font_size_spinb =
let sadj =
- GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+ GData.adjustment ~value:(float_of_int output#get_font_size)
+ ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
in
GEdit.spin_button
~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
projects / helm.git / blobdiff