X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=f99e11854738b207ed4d963766622201939f7050;hb=086099d1a60948454cf0874744ef2222c2edc1b6;hp=a1bc1dd9ed2fa0776b9b8d8ad98a25cecfd50345;hpb=3bec70852905f57198cd5b659dc72d430c1c5d2c;p=helm.git diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index a1bc1dd9e..f99e11854 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 ()