"</html>"
;;
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
(* SACERDOT
let prooffile = "/public/sacerdot/currentproof";;
(*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
(* SACERDOT
let innertypesfile = "/public/sacerdot/innertypes";;
exception NoChoice;;
let
- interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
+ interactive_user_uri_choice ~selection_mode ?(ok="Ok")
+ ?(enable_button_for_non_vars=false) ~title ~msg uris
=
let choices = ref [] in
let chosen = ref false in
+ let use_only_constants = ref false in
let window =
GWindow.dialog ~modal:true ~title ~width:600 () in
let lMessage =
GButton.button ~label:ok
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let _ = okb#misc#set_sensitive false in
+ let nonvarsb =
+ GButton.button
+ ~packing:
+ (function w ->
+ if enable_button_for_non_vars then
+ hbox#pack ~expand:false ~fill:false ~padding:5 w)
+ ~label:"Try constants only" () in
let checkb =
GButton.button ~label:"Check"
~packing:(hbox#pack ~padding:5) () in
ignore (cancelb#connect#clicked window#destroy) ;
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+ ignore
+ (nonvarsb#connect#clicked
+ (function () ->
+ use_only_constants := true ;
+ chosen := true ;
+ window#destroy ()
+ )) ;
ignore (checkb#connect#clicked check_callback) ;
ignore
(clist#connect#select_row
window#set_position `CENTER ;
window#show () ;
GMain.Main.main () ;
- if !chosen && List.length !choices > 0 then
- !choices
+ if !chosen then
+ if !use_only_constants then
+ List.filter
+ (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+ uris
+ else
+ if List.length !choices > 0 then !choices else raise NoChoice
else
raise NoChoice
;;
interactive_user_uri_choice
~selection_mode:`EXTENDED
~ok:"Try every selection."
+ ~enable_button_for_non_vars:true
~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
let intros = call_tactic ProofEngine.intros;;
let exact = call_tactic_with_input ProofEngine.exact;;
let apply = call_tactic_with_input ProofEngine.apply;;
-let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
+let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
let elimtype = call_tactic_with_input ProofEngine.elim_type;;
let whd = call_tactic_with_goal_input ProofEngine.whd;;
let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
window#show ()
;;
-let
- refine_constraints (must_obj,must_rel,must_sort) (only_obj,only_rel,only_sort)
-=
+let refine_constraints (must_obj,must_rel,must_sort) =
let chosen = ref false in
let use_only = ref false in
let window =
GWindow.window
- ~modal:true ~title:"Constraints refinement." ~border_width:2 () in
+ ~modal:true ~title:"Constraints refinement."
+ ~width:800 ~border_width:2 () in
let vbox = GPack.vbox ~packing:window#add () in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let onlyb =
GButton.toggle_button ~label:"Enforce \"only\" constraints"
- ~active:false ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5)
- ()
+ ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
in
ignore
(onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
+ (* Notebook for the constraints choice *)
+ let notebook =
+ GPack.notebook ~scrollable:true
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ (* Rel constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on Rels" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
let hbox =
- GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
~text: "You can now specify the constraints on Rels."
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- (* Rel constraints *)
let expected_height = 25 * (List.length must_rel + 2) in
let height = if expected_height > 400 then 400 else expected_height in
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~height ~width:600
- ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let rel_constraints =
List.map
| Some depth' ->
let mutable_ref = ref (Some depth') in
let depthb =
- GButton.toggle_button ~label:(string_of_int depth')
- ~active:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5)
- ()
+ 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
)) ;
position, mutable_ref
) must_rel in
+ (* Sort constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on Sorts" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
+ let hbox =
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on Sorts."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_sort + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ 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 sort_constraints =
+ List.map
+ (function (position,depth,sort) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(sort ^ " " ^ 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
+ ) must_sort in
+ (* Obj constraints *)
+ let label =
+ GMisc.label
+ ~text: "Constraints on constants" () in
+ let vbox' =
+ GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+ () in
+ let hbox =
+ GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on constants."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_obj + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+ 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 obj_constraints =
+ List.map
+ (function (uri,position,depth) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(uri ^ " " ^ position)
+ ~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
+ ) must_obj in
+ (* Confirm/abort buttons *)
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
let okb =
if !chosen then
let chosen_must_rel =
List.map
-(*
- (function (position,ref_depth) -> position,!ref_depth) rel_constraints
-*)
-(function (position,ref_depth) -> prerr_endline ("### " ^ position ^ " " ^ match !ref_depth with None -> "NULL" | Some d -> string_of_int d) ; position,!ref_depth) rel_constraints
+ (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+ let chosen_must_sort =
+ List.map
+ (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+ sort_constraints
+ in
+ let chosen_must_obj =
+ List.map
+ (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+ obj_constraints
in
- (must_obj,chosen_must_rel,must_sort),
- (if !use_only then
+ (chosen_must_obj,chosen_must_rel,chosen_must_sort),
+ (if !use_only then
(*CSC: ???????????????????????? I assume that must and only are the same... *)
- only_obj,Some chosen_must_rel,only_sort
- else
- None,None,None
- )
+ Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
+ else
+ None,None,None
+ )
else
raise NoChoice
;;
try
let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
- let must,only = MQueryLevels2.get_constraints expr in
- let must',only' = refine_constraints must only in
- let results = MQueryGenerator.searchPattern must' only' in
+ let must = MQueryLevels2.get_constraints expr in
+ let must',only = refine_constraints must in
+ let results = MQueryGenerator.searchPattern must' only in
show_query_results results
with
e ->
let applyb =
GButton.button ~label:"Apply"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let elimsimplintrosb =
- GButton.button ~label:"ElimSimplIntros"
+ let elimintrossimplb =
+ GButton.button ~label:"ElimIntrosSimpl"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let elimtypeb =
GButton.button ~label:"ElimType"
ignore(exactb#connect#clicked exact) ;
ignore(applyb#connect#clicked apply) ;
- ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
+ ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
ignore(elimtypeb#connect#clicked elimtype) ;
ignore(whdb#connect#clicked whd) ;
ignore(reduceb#connect#clicked reduce) ;
projects / helm.git / blobdiff