From c4afa186c53998a10eab85d3fcc113b07bccfdf9 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:11:12 +0000 Subject: [PATCH] snapshot, notably: - added support for inductive definitions - prelimnary support for user searches --- helm/matita/matita.conf.xml.sample | 4 +- helm/matita/matita.ml | 7 +- helm/matita/matitaConsole.ml | 1 + helm/matita/matitaDisambiguator.ml | 7 ++ helm/matita/matitaInterpreter.ml | 165 +++++++++++++++++++++++++---- helm/matita/matitaInterpreter.mli | 2 +- helm/matita/matitaTypes.ml | 19 ++++ 7 files changed, 183 insertions(+), 22 deletions(-) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index db02076cb..aca8b98d6 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -7,11 +7,13 @@
matita.glade true + zack
$(prefs.server) helm - mowgli + + matita
remote diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 49488a94d..20111286e 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -55,6 +55,7 @@ let dbd = ~user:(Helm_registry.get "db.user") ~database:(Helm_registry.get "db.database") () +let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner") let gui = MatitaGui.instance () let disambiguator = new MatitaDisambiguator.disambiguator ~parserr ~dbd @@ -114,7 +115,7 @@ let proof_handler = } let interpreter = - let console = gui#console in + let console = (gui#console :> MatitaTypes.console) in new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ~dbd () @@ -222,6 +223,10 @@ let _ = (not (Helm_registry.get_bool "matita.auto_disambiguation"))); addDebugItem "dump proof status to stdout" (fun _ -> print_endline ((get_proof ())#toString)); + addDebugItem "dump environment to \"env.dump\"" (fun _ -> + let oc = open_out "env.dump" in + CicEnvironment.dump_to_channel oc; + close_out oc); addDebugItem "print selected terms" (fun () -> let i = ref 0 in List.iter diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 889d8e2d8..4735fdd4a 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -172,6 +172,7 @@ class console self#lock method echo_message msg = + self#show (); let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 46341acfd..5b95f4192 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -79,6 +79,13 @@ class disambiguator x | _ -> assert false + method disambiguateTermAsts ?(metasenv = []) ?env asts = + let ast = CicAst.pack asts in + let (env, metasenv, term, ugraph) = + self#disambiguateTermAst ~context:[] ~metasenv ?env ast + in + (env, metasenv, CicUtil.unpack term, ugraph) + method disambiguateTerm ?context ?metasenv ?env stream = self#disambiguateTermAst ?context ?metasenv ?env (parserr#parseTerm stream) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index a1bc1dd9e..4521ab21b 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -90,7 +90,7 @@ class virtual interpreterState = (* static values, shared by all states inheriting this class *) let loc = ref None in let history = ref [] in - fun ~(console: MatitaConsole.console) -> + fun ~(console: MatitaTypes.console) -> object (self) (** eval a toplevel phrase in the current state and return the new state @@ -135,7 +135,8 @@ let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy class sharedState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) - ~(console: MatitaConsole.console) + ~(console: MatitaTypes.console) + ~(dbd: Mysql.dbd) () = object (self) @@ -172,18 +173,104 @@ class sharedState gui#main#showCheckMenuItem#set_active true; widget#load_sequent (sequent::metasenv) dummyno; None + | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) -> + let uris = + match search_kind with + | `Locate -> MetadataQuery.locate ~dbd pat + | `Elim -> MetadataQuery.elim ~dbd pat + | _ -> assert false + in + (* TODO ZACK: show URIs to the user *) + None | tactical -> raise (Command_error (TacticAstPp.pp_tactical tactical)) end +open Printf + +let pp_indtypes indTypes = + List.iter + (fun (name, _, typ, constructors) -> + printf "%s: %s\n" name (CicPp.ppterm typ); + List.iter + (fun (name, term) -> printf "\t%s: %s\n" name (CicPp.ppterm term)) + constructors) + indTypes; + flush stdout + +let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) = + let add_pi binders t = + List.fold_right + (fun (name, ast) acc -> + CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) + binders t + in + let ind_binders = + List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes + in + let binders = ind_binders @ params in + let asts = ref [] in + let add_ast ast = asts := ast :: !asts in + let paramsno = List.length params in + let indbindersno = List.length ind_binders in + List.iter + (fun (name, _, typ, constructors) -> + add_ast (add_pi params typ); + List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) + indTypes; + let (_, metasenv, terms, ugraph) = + disambiguator#disambiguateTermAsts ~metasenv:[] !asts + in + let terms = ref (List.rev terms) in + let get_term () = + match !terms with [] -> assert false | hd :: tl -> terms := tl; hd + in + let uri = + match indTypes with + | (name, _, _, _) :: _ -> qualify name ^ ".ind" + | _ -> assert false + in + let mutinds = + let counter = ref 0 in + List.map + (fun _ -> + incr counter; + CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter)) + indTypes + in + let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in + let cicIndTypes = + List.fold_left + (fun acc (name, inductive, typ, constructors) -> + let cicTyp = get_term () in + let cicConstructors = + List.fold_left + (fun acc (name, _) -> + let typ = + subst_mutinds (CicUtil.strip_prods indbindersno (get_term ())) + in + (name, typ) :: acc) + [] constructors + in + (name, inductive, cicTyp, List.rev cicConstructors) :: acc) + [] indTypes + in + let cicIndTypes = List.rev cicIndTypes in +(* + prerr_endline uri; + pp_indtypes cicIndTypes; +*) + (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) + (** Implements phrases that should be accepted only in `Command state *) class commandState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) - ~(console: MatitaConsole.console) + ~(console: MatitaTypes.console) + ~(dbd: Mysql.dbd) () = - let shared = new sharedState ~disambiguator ~proof_handler ~console () in + let shared = new sharedState ~disambiguator ~proof_handler ~console ~dbd () in object (self) inherit interpreterState ~console @@ -193,10 +280,51 @@ class commandState let (_, metasenv, expr,ugraph) = disambiguator#disambiguateTermAst ast in - let uri = UriManager.uri_of_string (qualify name) in + let uri = UriManager.uri_of_string (qualify name ^ ".con") in let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in proof_handler.MatitaTypes.new_proof proof; Some `Proof + | TacticAst.Command + (TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) -> + let (_, metasenv, type_cic, ugraph) = + disambiguator#disambiguateTermAst type_ast + in + let (_, metasenv, body_cic, ugraph) = + disambiguator#disambiguateTermAst ~metasenv body_ast + in + let (body_type, ugraph) = + CicTypeChecker.type_of_aux' metasenv [] body_cic ugraph + in + let uri = UriManager.uri_of_string (qualify name ^ ".con") in + let (subst, metasenv, ugraph) = + CicUnification.fo_unif metasenv [] body_type type_cic ugraph + in + let body_cic = CicMetaSubst.apply_subst subst body_cic in + let type_cic = CicMetaSubst.apply_subst subst type_cic in + let obj = + Cic.Constant + ((UriManager.name_of_uri uri), (Some body_cic),type_cic,[]) + in +(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + CicEnvironment.add_type_checked_term uri (obj, ugraph); + MetadataDb.index_constant ~dbd + ~owner:(Helm_registry.get "matita.owner") ~uri + ~body:(Some body_cic) ~ty:type_cic; + None + | TacticAst.Command (TacticAst.Inductive (params, indTypes)) -> + let (uri, (indTypes, params, leftno)) = + inddef_of_ast params indTypes disambiguator + in + let obj = Cic.InductiveDefinition (indTypes, params, leftno) in + let ugraph = + CicTypeChecker.typecheck_mutual_inductive_defs uri + (indTypes, params, leftno) CicUniv.empty_ugraph + in +(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + CicEnvironment.put_inductive_definition uri (obj, ugraph); + MetadataDb.index_inductive_def ~dbd + ~owner:(Helm_registry.get "matita.owner") ~uri ~types:indTypes; + None | TacticAst.Command TacticAst.Quit -> proof_handler.MatitaTypes.quit (); Some `Command (* dummy answer, useless *) @@ -225,14 +353,12 @@ let namer_of names = class proofState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) - ~(console: MatitaConsole.console) + ~(console: MatitaTypes.console) ~(dbd: Mysql.dbd) () = let disambiguate ast = - let (_, _, term,ugraph) = - disambiguate ~disambiguator ~proof_handler ast - in + let (_, _, term, _) = disambiguate ~disambiguator ~proof_handler ast in term in (** tactic AST -> ProofEngineTypes.tactic *) @@ -278,7 +404,7 @@ class proofState | _ -> MatitaTypes.not_implemented "some tactic" in - let shared = new sharedState ~disambiguator ~proof_handler ~console () in + let shared = new sharedState ~disambiguator ~proof_handler ~console ~dbd () in object (self) inherit interpreterState ~console @@ -304,22 +430,23 @@ class proofState let proved_ty,ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in - let b,ugraph1 = + let b,ugraph = CicReduction.are_convertible [] proved_ty ty ugraph in if not b then failwith "Wrong proof"; (* TODO Zack [] probably wrong *) - let ugraph2 = CicUniv.fill_empty_nodes_with_uri ugraph1 uri in - CicEnvironment.add_type_checked_term uri - ((Cic.Constant ((UriManager.name_of_uri uri), - (Some bo),ty,[])), - ugraph2); + let obj = + Cic.Constant ((UriManager.name_of_uri uri), (Some bo),ty,[]) + in +(* let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in *) + CicEnvironment.add_type_checked_term uri (obj, ugraph); + MetadataDb.index_constant ~dbd + ~owner:(Helm_registry.get "matita.owner") ~uri ~body:(Some bo) ~ty; proof_handler.MatitaTypes.set_proof None; (MatitaMathView.proof_viewer_instance ())#unload; (* TODO Zack a lot more to be done here: * - save object to disk in xml format - * - collect metadata * - register uri to the getter * - save universe file *) Some `Command @@ -337,12 +464,12 @@ class proofState class interpreter ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) - ~(console: MatitaConsole.console) + ~(console: MatitaTypes.console) ~(dbd: Mysql.dbd) () = let commandState = - new commandState ~disambiguator ~proof_handler ~console () + new commandState ~disambiguator ~proof_handler ~console ~dbd () in let proofState = new proofState ~disambiguator ~proof_handler ~console ~dbd () diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index 0baa4f0f1..96f824861 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -28,7 +28,7 @@ exception Command_error of string class interpreter: disambiguator:MatitaTypes.disambiguator -> proof_handler:MatitaTypes.proof_handler -> - console:MatitaConsole.console -> + console:MatitaTypes.console -> dbd:Mysql.dbd -> unit -> MatitaTypes.interpreter diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index cd9d34f08..4631fa351 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -55,6 +55,15 @@ class type parserr = (* "parser" is a keyword :-( *) method parseTactical: char Stream.t -> DisambiguateTypes.tactical end + (* subset of MatitaConsole.console methods needed by MatitaInterpreter *) +class type console = + object + method echo_message : string -> unit + method echo_error : string -> unit + method clear : unit -> unit + method wrap_exn : (unit -> unit) -> bool + end + class type disambiguator = object method parserr: parserr @@ -81,6 +90,16 @@ class type disambiguator = ?env:DisambiguateTypes.environment -> DisambiguateTypes.term -> (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) + + (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All + * AST should be closed hence no context param is permitted on this method + *) + method disambiguateTermAsts: + ?metasenv:Cic.metasenv -> + ?env:DisambiguateTypes.environment -> + DisambiguateTypes.term list -> + (DisambiguateTypes.environment * Cic.metasenv * Cic.term list * + CicUniv.universe_graph) end (* -- 2.39.2