let apply rendering_window =
call_tactic_with_input ProofEngine.apply rendering_window
;;
-let elim rendering_window =
- call_tactic_with_input ProofEngine.elim rendering_window
+let elimintros rendering_window =
+ call_tactic_with_input ProofEngine.elim_intros rendering_window
;;
let whd rendering_window =
call_tactic_with_goal_input ProofEngine.whd rendering_window
| None -> assert false (* "ERROR: No selection!!!" *)
;;
+exception NotADefinition;;
+
+let open_ rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ try
+ let uri = UriManager.uri_of_string ("cic:" ^ input) in
+ CicTypeChecker.typecheck uri ;
+ let metasenv,bo,ty =
+ match CicEnvironment.get_cooked_obj uri 0 with
+ Cic.Definition (_,bo,ty,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
+ | Cic.Axiom _
+ | Cic.Variable _
+ | Cic.InductiveDefinition _ -> raise NotADefinition
+ in
+ ProofEngine.proof :=
+ Some (uri, metasenv, bo, ty) ;
+ ProofEngine.goal := None ;
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length) ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
let state rendering_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
let oldinputt = (rendering_window#oldinputt : GEdit.text) in
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen ;
- ignore(oldinputt#insert_text input oldinputt#length) ;
+ ignore(oldinputt#insert_text input oldinputt#length)
| e ->
print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
;;
~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
~packing:(vbox#pack ~padding:5) () in
+ let hbox4 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
let stateb =
GButton.button ~label:"State"
- ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let openb =
+ GButton.button ~label:"Open"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
~packing:(vbox#pack ~padding:5) () in
let vbox1 =
let applyb =
GButton.button ~label:"Apply"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let elimb =
- GButton.button ~label:"Elim"
+ let elimintrosb =
+ GButton.button ~label:"ElimIntros"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let whdb =
GButton.button ~label:"Whd"
ignore(proveitb#connect#clicked (proveit self)) ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
ignore(stateb#connect#clicked (state self)) ;
+ ignore(openb#connect#clicked (open_ self)) ;
ignore(exactb#connect#clicked (exact self)) ;
ignore(applyb#connect#clicked (apply self)) ;
- ignore(elimb#connect#clicked (elim self)) ;
+ ignore(elimintrosb#connect#clicked (elimintros self)) ;
ignore(whdb#connect#clicked (whd self)) ;
ignore(reduceb#connect#clicked (reduce self)) ;
ignore(simplb#connect#clicked (simpl self)) ;
| [] -> goal := None
;;
+let elim_intros term =
+ elim term ;
+ intros ()
+;;
+
let reduction_tactic reduction_function term =
let curi,metasenv,pbo,pty =
match !proof with
| Some (metano,(context,ty)) -> metano,context,ty
in
let term' = reduction_function term in
- let ty' = ProofEngineReduction.replace term term' ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
+ let ty' = replace ty in
+ let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+ let metasenv' =
+ List.map
+ (function
+ (n,_) when n = metano -> (metano,ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some (metano,(context',ty'))
;;
let whd = reduction_tactic CicReduction.whd;;
let reduce = reduction_tactic ProofEngineReduction.reduce;;
-(*
let simpl = reduction_tactic ProofEngineReduction.simpl;;
-*)
-
-let simpl term =
- let curi,metasenv,pbo,pty =
- match !proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) -> metano,context,ty
- in
- let term' = ProofEngineReduction.simpl term in
- let ty' = ProofEngineReduction.replace term term' ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
-;;
(* It is just the opposite of whd. The code should probably be merged. *)
let fold term =
| Some (metano,(context,ty)) -> metano,context,ty
in
let term' = CicReduction.whd term in
- let ty' = ProofEngineReduction.replace term' term ty in
- let metasenv' =
- List.map
- (function
- (n,_) when n = metano -> (metano,ty')
- | _ as t -> t
- ) metasenv
- in
- proof := Some (curi,metasenv',pbo,pty) ;
- goal := Some (metano,(context,ty'))
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
+ let ty' = replace ty in
+ let context' = List.map (function (bt,n,t) -> bt,n,replace t) context in
+ let metasenv' =
+ List.map
+ (function
+ (n,_) when n = metano -> (metano,ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some (metano,(context',ty'))
;;
let cut term =
| C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
| C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
| C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
+ | C.Appl l ->
+ (* Invariant enforced: no application of an application *)
+ (match List.map aux l with
+ (C.Appl l')::tl -> C.Appl (l'@tl)
+ | l' -> C.Appl l')
| C.Const _ as t -> t
| C.Abst _ as t -> t
| C.MutInd _ as t -> t
struct
let print_sequent metasenv (context,goal) =
let module X = Xml in
- let final_s,final_env =
- (List.fold_right
- (fun (b,n,t) (s,env) ->
- let (acic,_,_,ids_to_inner_sorts,_) =
- Cic2acic.acic_of_cic_env metasenv env t
- in
- [< s ;
- X.xml_nempty
- (match b with
- ProofEngine.Definition -> "Def"
- | ProofEngine.Declaration -> "Decl"
- ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
- (Cic2Xml.print_term
- (UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
- >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *)
- ) context ([<>],[])
- )
- in
- let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,_) =
- Cic2acic.acic_of_cic_env metasenv final_env goal
+ let ids_to_terms = Hashtbl.create 503 in
+ let ids_to_father_ids = Hashtbl.create 503 in
+ let ids_to_inner_sorts = Hashtbl.create 503 in
+ let ids_to_inner_types = Hashtbl.create 503 in
+ let seed = ref 0 in
+ let acic_of_cic_env =
+ Cic2acic.acic_of_cic_env' seed ids_to_terms ids_to_father_ids
+ ids_to_inner_sorts ids_to_inner_types metasenv
in
- X.xml_nempty "Sequent" []
- [< final_s ;
- Xml.xml_nempty "Goal" []
- (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
- ids_to_inner_sorts acic)
- >],
- ids_to_terms,ids_to_father_ids
+ let final_s,final_env =
+ (List.fold_right
+ (fun (b,n,t) (s,env) ->
+ let acic = acic_of_cic_env env t in
+ [< s ;
+ X.xml_nempty
+ (match b with
+ ProofEngine.Definition -> "Def"
+ | ProofEngine.Declaration -> "Decl"
+ ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
+ (Cic2Xml.print_term
+ (UriManager.uri_of_string "cic:/dummy.con")
+ ids_to_inner_sorts acic)
+ >],((n,t)::env) (* CSC: sbagliato!!! Giusto solo se Declaration! *)
+ ) context ([<>],[])
+ )
+ in
+ let acic = acic_of_cic_env final_env goal in
+ X.xml_nempty "Sequent" []
+ [< final_s ;
+ Xml.xml_nempty "Goal" []
+ (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
+ ids_to_inner_sorts acic)
+ >],
+ ids_to_terms,ids_to_father_ids
;;
end
;;
projects / helm.git / commitdiff