From e627ae3edfbe950b87069b625ec9317acaf03ec5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 11:14:07 +0000 Subject: [PATCH] * Many improvements * Added the possibility to select parts of the goal of a sequent and retrieve the corresponding CIC term. * New tactics implemented: Cut, Whd, Reduce, Simpl, Change --- helm/gTopLevel/gTopLevel.ml | 205 +++++++++- helm/gTopLevel/logicalOperations.ml | 2 +- helm/gTopLevel/proofEngine.ml | 568 ++++++++++++++++++++++------ 3 files changed, 634 insertions(+), 141 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4f8a29d76..0cfccab99 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -52,6 +52,7 @@ let htmlfooter = let htmlheader_and_content = ref htmlheader;; let current_cic_infos = ref None;; +let current_goal_infos = ref None;; (* MISC FUNCTIONS *) @@ -143,14 +144,12 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types = +let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = let xml = - Cic2Xml.print_object - (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj + Cic2Xml.print_object uri ids_to_inner_sorts annobj in let xmlinnertypes = - Cic2Xml.print_inner_types - (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts + Cic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in let input = Xml2Gdome.document_of_xml domImpl xml in @@ -166,17 +165,18 @@ let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types = (* CALLBACKS *) let refresh_proof (output : GMathView.math_view) = - let currentproof = + let uri,currentproof = match !ProofEngine.proof with None -> assert false - | Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty) + | Some (uri,metasenv,bo,ty) -> + uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty)) in let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types) = Cic2acic.acic_object_of_cic_object currentproof in - let mml = mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types in + let mml = mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in output#load_tree mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ;; @@ -188,9 +188,9 @@ let refresh_sequent (proofw : GMathView.math_view) = let metasenv = match !ProofEngine.proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in - let sequent_gdome = + let sequent_gdome,ids_to_terms,ids_to_father_ids = SequentPp.XmlPp.print_sequent metasenv currentsequent in let sequent_doc = @@ -199,7 +199,8 @@ let refresh_sequent (proofw : GMathView.math_view) = let sequent_mml = applyStylesheets sequent_doc sequent_styles sequent_args in - proofw#load_tree ~dom:sequent_mml + proofw#load_tree ~dom:sequent_mml ; + current_goal_infos := Some (ids_to_terms,ids_to_father_ids) (* ignore(domImpl#saveDocumentToFile ~doc:sequent_doc ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; @@ -210,7 +211,8 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_mml let output_html outputhtml msg = htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) + outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; + outputhtml#set_topline (-1) ;; (***********************) @@ -220,7 +222,6 @@ let output_html outputhtml msg = let call_tactic tactic rendering_window () = let proofw = (rendering_window#proofw : GMathView.math_view) in let output = (rendering_window#output : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in @@ -241,7 +242,6 @@ let call_tactic tactic rendering_window () = let call_tactic_with_input tactic rendering_window () = let proofw = (rendering_window#proofw : GMathView.math_view) in let output = (rendering_window#output : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in let inputt = (rendering_window#inputt : GEdit.text) in let savedproof = !ProofEngine.proof in @@ -250,6 +250,11 @@ let call_tactic_with_input tactic rendering_window () = let inputlen = inputt#length in let input = inputt#get_chars 0 inputlen ^ "\n" in let lexbuf = Lexing.from_string input in + let curi = + match !ProofEngine.proof with + None -> assert false + | Some (curi,_,_,_) -> curi + in let context = List.map (function (_,n,_) -> n) @@ -261,7 +266,7 @@ let call_tactic_with_input tactic rendering_window () = try while true do match - CicTextualParserContext.main context CicTextualLexer.token lexbuf + CicTextualParserContext.main curi context CicTextualLexer.token lexbuf with None -> () | Some expr -> @@ -280,6 +285,113 @@ prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ; ProofEngine.goal := savedgoal ;; +let call_tactic_with_goal_input tactic rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match proofw#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids) -> + let id = xpath in + tactic (Hashtbl.find ids_to_terms id) ; + refresh_sequent rendering_window#proofw ; + refresh_proof rendering_window#output + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ; + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +let call_tactic_with_input_and_goal_input tactic rendering_window () = + let module L = LogicalOperations in + let module G = Gdome in + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in + let inputt = (rendering_window#inputt : GEdit.text) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match proofw#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match !current_goal_infos with + Some (ids_to_terms, ids_to_father_ids) -> + let id = xpath in + (* Let's parse the input *) + let inputlen = inputt#length in + let input = inputt#get_chars 0 inputlen ^ "\n" in + let lexbuf = Lexing.from_string input in + let curi = + match !ProofEngine.proof with + None -> assert false + | Some (curi,_,_,_) -> curi + in + let context = + List.map + (function (_,n,_) -> n) + (match !ProofEngine.goal with + None -> assert false + | Some (_,(ctx,_)) -> ctx + ) + in + begin + try + while true do + match + CicTextualParserContext.main curi context + CicTextualLexer.token lexbuf + with + None -> () + | Some expr -> + tactic ~goal_input:(Hashtbl.find ids_to_terms id) + ~input:expr ; + refresh_sequent proofw ; + refresh_proof output + done + with + CicTextualParser0.Eof -> + inputt#delete_text 0 inputlen + end + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> +prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ; + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; let exact rendering_window = call_tactic_with_input ProofEngine.exact rendering_window @@ -287,6 +399,30 @@ let exact rendering_window = 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 whd rendering_window = + call_tactic_with_goal_input ProofEngine.whd rendering_window +;; +let reduce rendering_window = + call_tactic_with_goal_input ProofEngine.reduce rendering_window +;; +let simpl rendering_window = + call_tactic_with_goal_input ProofEngine.simpl rendering_window +;; +let fold rendering_window = + call_tactic_with_input ProofEngine.fold rendering_window +;; +let cut rendering_window = + call_tactic_with_input ProofEngine.cut rendering_window +;; +let change rendering_window = + call_tactic_with_input_and_goal_input ProofEngine.change rendering_window +;; + + + (**********************) (* END OF TACTICS *) @@ -298,11 +434,11 @@ exception WrongProof;; let save rendering_window () = match !ProofEngine.proof with None -> assert false - | Some ([],bo,ty) -> + | Some (uri,[],bo,ty) -> if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then begin (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Definition ("unnamed",bo,ty,[]) in + let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types) @@ -310,7 +446,7 @@ let save rendering_window () = Cic2acic.acic_object_of_cic_object proof in let mml = - mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types + mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in (rendering_window#output : GMathView.math_view)#load_tree mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids) @@ -368,7 +504,9 @@ let state rendering_window () = | Some expr -> try let _ = CicTypeChecker.type_of_aux' [] [] expr in - ProofEngine.proof := Some ([1,expr], Cic.Meta 1, expr) ; + ProofEngine.proof := + Some (UriManager.uri_of_string "cic:/dummy.con", + [1,expr], Cic.Meta 1, expr) ; ProofEngine.goal := Some (1,([],expr)) ; refresh_sequent proofw ; refresh_proof output ; @@ -587,6 +725,27 @@ class rendering_window output proofw (label : GMisc.label) = let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimb = + GButton.button ~label:"Elim" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let foldb = + GButton.button ~label:"Fold" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let cutb = + GButton.button ~label:"Cut" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let changeb = + GButton.button ~label:"Change" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -618,6 +777,13 @@ object(self) ignore(stateb#connect#clicked (state self)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; + ignore(elimb#connect#clicked (elim self)) ; + ignore(whdb#connect#clicked (whd self)) ; + ignore(reduceb#connect#clicked (reduce self)) ; + ignore(simplb#connect#clicked (simpl self)) ; + ignore(foldb#connect#clicked (fold self)) ; + ignore(cutb#connect#clicked (cut self)) ; + ignore(changeb#connect#clicked (change self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -639,5 +805,6 @@ let initialize_everything () = let _ = CicCooking.init () ; + ignore (GtkMain.Main.init ()) ; initialize_everything () ;; diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index b7c1a9bcf..277451bf4 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -73,7 +73,7 @@ let to_sequent id ids_to_terms ids_to_father_ids = let metasenv = match !P.proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in let ty = CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index b676832c1..60baf8e59 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -3,13 +3,15 @@ type binder_type = | Definition ;; -type metas_context = (int * Cic.term) list;; +type metasenv = (int * Cic.term) list;; type context = (binder_type * Cic.name * Cic.term) list;; type sequent = context * Cic.term;; -let proof = ref (None : (metas_context * Cic.term * Cic.term) option);; +let proof = + ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option) +;; (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *) (* Note: the sequent is redundant: it can be computed from the type of the *) (* metavariable and its context in the proof. We keep it just for efficiency *) @@ -28,10 +30,10 @@ let cic_context_of_context = ;; let refine_meta meta term newmetasenv = - let (metasenv,bo,ty) = + let (uri,metasenv,bo,ty) = match !proof with None -> assert false - | Some (metasenv,bo,ty) -> metasenv,bo,ty + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in let rec aux = @@ -72,7 +74,7 @@ let refine_meta meta term newmetasenv = in let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in let bo' = aux bo in - proof := Some (metasenv'',bo',ty) + proof := Some (uri,metasenv'',bo',ty) ;; (* Returns the first meta whose number is above the number of the higher meta. *) @@ -80,7 +82,7 @@ let new_meta () = let metasenv = match !proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in let rec aux = function @@ -141,47 +143,11 @@ let perforate context term ty = let newmeta = new_meta () in match !proof with None -> assert false - | Some (metasenv,bo,gty) -> + | Some (uri,metasenv,bo,gty) -> (* We push the new meta at the end of the list for pretty-printing *) (* purposes: in this way metas are ordered. *) let metasenv' = metasenv@[newmeta,ty] in - let rec aux = - function - (* Is == strong enough? *) - t when t == term -> C.Meta newmeta - | C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | 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.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,aux outt, aux t, - List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl - in - C.CoFix (i, substitutedfl) - in - let bo' = aux bo in + let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in (* It may be possible that some metavariables occurred only in *) (* the term we are perforating and they now occurs no more. We *) (* get rid of them, collecting the really useful metavariables *) @@ -190,7 +156,7 @@ let perforate context term ty = let metasenv'' = List.filter (function (n,_) -> List.mem n newmetas) metasenv' in - proof := Some (metasenv'',bo',gty) ; + proof := Some (uri,metasenv'',bo',gty) ; goal := Some (newmeta,(context,ty)) ; newmeta ;; @@ -207,7 +173,7 @@ let intros () = let metasenv = match !proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in let (metano,context,ty) = match !goal with @@ -220,7 +186,13 @@ let intros () = C.Cast (te,_) -> collect_context te | C.Prod (n,s,t) -> let (ctx,ty,bo) = collect_context t in - ((Declaration,n,s)::ctx,ty,C.Lambda(n,s,bo)) + let n' = + match n with + C.Name _ -> n +(*CSC: generatore di nomi? Chiedere il nome? *) + | C.Anonimous -> C.Name "fresh_name" + in + ((Declaration,n',s)::ctx,ty,C.Lambda(n',s,bo)) | C.LetIn (n,s,t) -> let (ctx,ty,bo) = collect_context t in ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo)) @@ -239,7 +211,7 @@ let exact bo = let metasenv = match !proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in let (metano,context,ty) = match !goal with @@ -260,6 +232,77 @@ let exact bo = raise (Fail "The type of the provided term is not the one expected.") ;; +let fix_andreas_meta mgu mgut = + let mgul = Array.to_list mgu in + let mgutl = Array.to_list mgut in + let applymetas_to_metas = + let newmeta = new_meta () in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + Array.init (List.length mgul) (function i -> newmeta + i) in + (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) + (* Here we assume that either a META has been instantiated with *) + (* a close term or with itself. *) + let uninstantiatedmetas = + List.fold_right2 + (fun bo ty newmetas -> + let module C = Cic in + match bo with + Cic.Meta i -> + let newmeta = applymetas_to_metas.(i) in + (*CSC: se ty contiene metas, queste hanno il numero errato!!! *) + let ty_with_newmetas = + (* Substitues (META n) with (META (applymetas_to_metas.(n))) *) + let rec aux = + function + C.Rel _ + | C.Var _ as t -> t + | C.Meta n -> C.Meta (applymetas_to_metas.(n)) + | C.Sort _ + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | 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.Const _ as t -> t + | C.Abst _ -> assert false + | C.MutInd _ + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux outt, aux t, + List.map aux pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux ty + in + (newmeta,ty_with_newmetas)::newmetas + | _ -> newmetas + ) mgul mgutl [] + in + let mgul' = + List.map + (function + Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) + | _ as t -> t + ) mgul + in + mgul',uninstantiatedmetas +;; + (* The term bo must be closed in the current context *) let apply term = let module T = CicTypeChecker in @@ -268,7 +311,7 @@ let apply term = let metasenv = match !proof with None -> assert false - | Some (metasenv,_,_) -> metasenv + | Some (_,metasenv,_,_) -> metasenv in let (metano,context,ty) = match !goal with @@ -281,79 +324,362 @@ let apply term = (*CSC: deve sparire! *) let ciccontext = cic_context_of_context context in let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in - let mgul = Array.to_list mgu in - let mgutl = Array.to_list mgut in - let applymetas_to_metas = - let newmeta = new_meta () in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - Array.init (List.length mgul) (function i -> newmeta + i) in - (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) - (* Here we assume that either a META has been instantiated with *) - (* a close term or with itself. *) - let uninstantiatedmetas = - List.fold_right2 - (fun bo ty newmetas -> - match bo with - Cic.Meta i -> - let newmeta = applymetas_to_metas.(i) in - (*CSC: se ty contiene metas, queste hanno il numero errato!!! *) - let ty_with_newmetas = - (* Substitues (META n) with (META (applymetas_to_metas.(n))) *) - let rec aux = - function - C.Rel _ - | C.Var _ as t -> t - | C.Meta n -> C.Meta (applymetas_to_metas.(n)) - | C.Sort _ - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | 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.Const _ as t -> t - | C.Abst _ -> assert false - | C.MutInd _ - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outt,t,pl) -> - C.MutCase (sp,cookingsno,i,aux outt, aux t, - List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl - in - C.CoFix (i, substitutedfl) - in - aux ty - in - (newmeta,ty_with_newmetas)::newmetas - | _ -> newmetas - ) mgul mgutl [] + let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in + let bo' = + if List.length mgul' = 0 then + term + else + Cic.Appl (term::mgul') + in + refine_meta metano bo' uninstantiatedmetas ; + match uninstantiatedmetas with + (n,ty)::tl -> goal := Some (n,(context,ty)) + | [] -> goal := None +;; + + +let eta_expand metasenv ciccontext t arg = + let module T = CicTypeChecker in + let module S = CicSubstitution in + let module C = Cic in + let rec aux n = + function + t' when t' = S.lift n arg -> C.Rel (1 + n) + | C.Rel m -> if m <= n then C.Rel m else C.Rel (m+1) + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) + | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) + | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) + | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) + | C.Appl l -> C.Appl (List.map (aux n) l) + | C.Const _ as t -> t + | C.Abst _ -> assert false + | C.MutInd _ + | C.MutConstruct _ as t -> t + | C.MutCase (sp,cookingsno,i,outt,t,pl) -> + C.MutCase (sp,cookingsno,i,aux n outt, aux n t, + List.map (aux n) pl) + | C.Fix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) + in + let argty = + T.type_of_aux' metasenv ciccontext arg + in + (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) +;; + +exception NotAnInductiveTypeToEliminate;; +exception NotTheRightEliminatorShape;; +exception NoHypothesesFound;; + +let elim term = + let module T = CicTypeChecker in + let module U = UriManager in + let module R = CicReduction in + let module C = Cic in + let curi,metasenv = + match !proof with + None -> assert false + | Some (curi,metasenv,_,_) -> curi,metasenv + in + let (metano,context,ty) = + match !goal with + None -> assert false + | Some (metano,(context,ty)) -> + assert (ty = List.assoc metano metasenv) ; + (* Invariant: context is the actual context of the meta in the proof *) + metano,context,ty + in + (*CSC: deve sparire! *) + let ciccontext = cic_context_of_context context in + let termty = T.type_of_aux' metasenv ciccontext term in + let uri,cookingno,typeno,args = + match termty with + C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[]) + | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) -> + (uri,cookingno,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate + in + let eliminator_uri = + let buri = U.buri_of_uri uri in + let name = + match CicEnvironment.get_cooked_obj uri cookingno with + C.InductiveDefinition (tys,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + | _ -> assert false + in + let ext = + match T.type_of_aux' metasenv ciccontext ty with + C.Sort C.Prop -> "_ind" + | C.Sort C.Set -> "_rec" + | C.Sort C.Type -> "_rect" + | _ -> assert false in - let mgul' = - List.map + U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + in + let eliminator_cookingno = + UriManager.relative_depth curi eliminator_uri 0 + in + let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in + let ety = + T.type_of_aux' [] [] eliminator_ref + in + + let earity = CicUnification.get_arity ety in + let mgu = Array.init earity (fun i -> (C.Meta i)) in + let mgut = Array.make earity C.Implicit in + (* Here we assume that we have only one inductive hypothesis to *) + (* eliminate and that it is the last hypothesis of the theorem. *) + (* A better approach would be fingering the hypotheses in some *) + (* way. *) + let hypothesis_to_eliminate,econclusion = + (* aux n h t *) + (* traverses the backbone [t] looking for the last hypothesis *) + (* and substituting Pi-abstractions with META declarations. *) + (* [h] is the last hypothesis met up to now. [n] is the next *) + (* unused META. *) + let rec aux n h = + function + C.Prod (_,s,t) -> + mgut.(n) <- s ; + aux (n+1) (Some s) (CicSubstitution.subst (C.Meta n) t) + | C.Cast (te,_) -> aux n h te + | t -> match h with + None -> raise NoHypothesesFound + | Some h' -> h',t + in + aux 0 None ety + in +prerr_endline ("HTOELIM: " ^ CicPp.ppterm hypothesis_to_eliminate) ; +prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ; +flush stderr ; + ignore (CicUnification.fo_unif_mgu 0 hypothesis_to_eliminate termty mgu) ; + ignore (CicUnification.fo_unif_mgu 0 term (C.Meta (earity - 1)) mgu) ; + let mgu = CicUnification.unwind mgu in +prerr_endline "Dopo l'unwind dell'mgu"; flush stderr ; + let mark = Array.make earity 1 in + let ueconclusion = + CicUnification.unwind_meta mgu mark econclusion + in +prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ; +flush stderr ; + (* The conclusion of our elimination principle is *) + (* (?i farg1 ... fargn) *) + (* The conclusion of our goal is ty. So, we can *) + (* eta-expand ty w.r.t. farg1 .... fargn to get *) + (* a new ty equal to (P farg1 ... fargn). Now *) + (* ?i can be instantiated with P and we are ready *) + (* to refine the term. *) + let emeta, fargs = + match ueconclusion with + C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs + | _ -> raise NotTheRightEliminatorShape + in + let eta_expanded_ty = +(*CSC: metasenv e ?????????????*) + List.fold_left (eta_expand metasenv ciccontext) ty fargs + in +(*CSC: 0????????*) +prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ; + ignore (CicUnification.fo_unif_mgu 0 ueconclusion eta_expanded_ty mgu) ; +prerr_endline "Dopo la seconda unificazione" ; flush stdout ; + let mgu = CicUnification.unwind mgu in + print_endline "unwind"; flush stdout; + (* When unwinding the META that corresponds to the elimination *) + (* predicate (which is emeta), we must also perform one-step *) + (* beta-reduction. *) + let mgut = + let mark = Array.make (Array.length mgu) 1 in + Array.map + (CicUnification.unwind_meta_reducing mgu mark (Some emeta)) + mgut ; + in + print_endline "unwind_array"; flush stdout; + let mgu' = Array.copy mgu in + let mgut' = CicUnification.list_of_array mgut in + print_endline "list"; flush stdout; + Array.iteri + (fun i ty -> +prerr_endline ("META " ^ string_of_int i ^ ": " ^ CicPp.ppterm mgu'.(i) ^ + " == " ^ CicPp.ppterm ty) ; flush stderr ; + let ty' = + CicTypeChecker.type_of_aux' mgut' ciccontext mgu'.(i) + in + ignore (CicUnification.fo_unif_mgu 0 ty ty' mgu) + ) mgut ; + let mgu = CicUnification.unwind mgu in + let mgut = CicUnification.unwind_array mgu mgut in +prerr_endline "Dopo le unwind dell'mgut" ; flush stdout ; + let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in +prerr_endline "Dopo il fissaggio" ; flush stdout ; + let bo' = Cic.Appl (eliminator_ref::mgul') in +prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ; + refine_meta metano bo' uninstantiatedmetas ; +prerr_endline "dopo refine meta" ; flush stdout ; + match uninstantiatedmetas with + (n,ty)::tl -> goal := Some (n,(context,ty)) + | [] -> goal := None +;; + +let reduction_tactic reduction_function 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' = 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')) +;; + +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 = + 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' = 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')) +;; + +let cut term = + let module C = Cic in + 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 newmeta1 = new_meta () in + let newmeta2 = newmeta1 + 1 in + let newmeta1ty = CicSubstitution.lift 1 ty in + let bo' = + C.Appl + [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ; + C.Meta newmeta2] + in +prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ; + refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty]; + goal := + Some + (newmeta1,((Declaration, C.Name "dummy_for_cut", term)::context, + newmeta1ty)) +;; + +exception NotConvertible;; + +(*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *) +(*CSC: while [goal_input] can have a richer context (because of binders) *) +(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *) +(*CSC: Is that evident? Is that right? Or should it be changed? *) +let change ~goal_input ~input = + 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 + (*CSC: deve sparire! *) + let ciccontext = cic_context_of_context context in + (* are_convertible works only on well-typed terms *) + ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ; + if CicReduction.are_convertible goal_input input then + begin + let ty' = ProofEngineReduction.replace goal_input input ty in + let metasenv' = + List.map (function - Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i)) + (n,_) when n = metano -> (metano,ty') | _ as t -> t - ) mgul in - let bo' = - if List.length mgul' = 0 then - term - else - Cic.Appl (term::mgul') - in - refine_meta metano bo' uninstantiatedmetas ; - match uninstantiatedmetas with - (n,ty)::tl -> goal := Some (n,(context,ty)) - | [] -> goal := None + ) metasenv + in + proof := Some (curi,metasenv',pbo,pty) ; + goal := Some (metano,(context,ty')) + end + else + raise NotConvertible ;; -- 2.39.2