open Printf open MatitaTypes let debug = true ;; let debug_print = if debug then prerr_endline else ignore ;; (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) let namer_of names = let len = List.length names in let count = ref 0 in fun metasenv context name ~typ -> if !count < len then begin let name = Cic.Name (List.nth names !count) in incr count; name end else FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ let tactic_of_ast = function | TacticAst.Intros (_, None, names) -> (* TODO Zack implement intros length *) PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Intros (_, Some num, names) -> (* TODO Zack implement intros length *) PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Reflexivity _ -> Tactics.reflexivity | TacticAst.Assumption _ -> Tactics.assumption | TacticAst.Contradiction _ -> Tactics.contradiction | TacticAst.Exists _ -> Tactics.exists | TacticAst.Fourier _ -> Tactics.fourier | TacticAst.Goal (_, n) -> Tactics.set_goal n | TacticAst.Left _ -> Tactics.left | TacticAst.Right _ -> Tactics.right | TacticAst.Ring _ -> Tactics.ring | TacticAst.Split _ -> Tactics.split | TacticAst.Symmetry _ -> Tactics.symmetry | TacticAst.Transitivity (_, term) -> Tactics.transitivity term | TacticAst.Apply (_, term) -> Tactics.apply term | TacticAst.Absurd (_, term) -> Tactics.absurd term | TacticAst.Exact (_, term) -> Tactics.exact term | TacticAst.Cut (_, term) -> Tactics.cut term | TacticAst.Elim (_, term, _) -> (* TODO Zack implement "using" argument *) (* old: Tactics.elim_intros_simpl term *) Tactics.elim_intros term | TacticAst.ElimType (_, term) -> Tactics.elim_type term | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what | TacticAst.Auto (_,num) -> AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ()) | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what (* (* TODO Zack a lot more of tactics to be implemented here ... *) | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option | TacticAst.Change of 'term * 'term * 'ident option | TacticAst.Decompose of 'ident * 'ident list | TacticAst.Discriminate of 'ident | TacticAst.Fold of reduction_kind * 'term | TacticAst.Injection of 'ident | TacticAst.LetIn of 'term * 'ident | TacticAst.Replace_pattern of 'term pattern * 'term *) | TacticAst.ReduceAt (_,reduction_kind,ident,path) -> ProofEngineTypes.mk_tactic (fun (((_,metasenv,_,_),goal) as status) -> let metano,context,ty = CicUtil.lookup_meta goal metasenv in let where, also_in_hypotheses = if ident = "goal" then ty, false else let hyp = try List.find (function | Some (Cic.Name name,entry) when name = ident -> true | _ -> false) context with Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis")) in (match hyp with | Some (_, Cic.Decl term) -> term | Some (_, Cic.Def (term,ty)) -> term | None -> assert false),true in let pointers = CicUtil.select ~term:where ~context:path in (match reduction_kind with | `Normalize -> ProofEngineTypes.apply_tactic (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers)) status | `Reduce -> ProofEngineTypes.apply_tactic (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers)) status | `Simpl -> ProofEngineTypes.apply_tactic (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers)) status | `Whd -> ProofEngineTypes.apply_tactic (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers)) status)) | TacticAst.Reduce (_,reduction_kind,opts) -> let terms, also_in_hypotheses = match opts with | Some (l,`Goal) -> Some l, false | Some (l,`Everywhere) -> Some l, true | None -> None, false in (match reduction_kind with | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms | `Whd -> Tactics.whd ~also_in_hypotheses ~terms) | TacticAst.Rewrite (_,dir,t,ident) -> if dir = `Left then EqualityTactics.rewrite_tac ~term:t else EqualityTactics.rewrite_back_tac ~term:t | _ -> assert false let eval_tactical status tac = let apply_tactic tactic = let (proof, goals) = ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in let new_status = match goals with | [] -> let (_,metasenv,_,_) = proof in (match metasenv with | [] -> Proof proof | (ng,_,_)::_ -> Incomplete_proof (proof,ng)) | ng::_ -> Incomplete_proof (proof, ng) in { status with proof_status = new_status } in let rec tactical_of_ast = function | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic | TacticAst.Fail loc -> Tacticals.fail | TacticAst.Do (loc, num, tactical) -> Tacticals.do_tactic num (tactical_of_ast tactical) | TacticAst.IdTac loc -> Tacticals.id_tac | TacticAst.Repeat (loc, tactical) -> Tacticals.repeat_tactic (tactical_of_ast tactical) | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) Tacticals.seq (List.map tactical_of_ast tacticals) | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) Tacticals.thens (tactical_of_ast tactical) (List.map tactical_of_ast tacticals) | TacticAst.Tries (loc, tacticals) -> Tacticals.try_tactics (List.map (fun t -> "", tactical_of_ast t) tacticals) | TacticAst.Try (loc, tactical) -> Tacticals.try_tactic (tactical_of_ast tactical) in apply_tactic (tactical_of_ast tac) (** given a uri and a type list (the contructors types) builds a list of pairs * (name,uri) that is used to generate authomatic aliases **) let extract_alias types uri = fst(List.fold_left ( fun (acc,i) (name, _, _, cl) -> ((name, UriManager.string_of_uriref (uri,[i])) :: (fst(List.fold_left ( fun (acc,j) (name,_) -> (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) ) (acc,1) cl))),i+1 ) ([],0) types) (** adds a (name,uri) list l to a disambiguation environment e **) let env_of_list l e = let module DT = DisambiguateTypes in let module DTE = DisambiguateTypes.Environment in List.fold_left ( fun e (name,uri) -> DTE.add (DT.Id name) (uri,fun _ _ _ -> CicUtil.term_of_uri uri) e ) e l let eval_command status cmd = match cmd with | TacticAst.Set (loc, name, value) -> set_option status name value | TacticAst.Qed loc -> let uri, metasenv, bo, ty = match status.proof_status with | Proof (Some uri, metasenv, body, ty) -> uri, metasenv, body, ty | Proof (None, metasenv, body, ty) -> command_error ("Someone allows to start a thm without giving the "^ "name/uri. This should be fixed!") | _-> command_error "You can't qed an uncomplete theorem" in let suri = UriManager.string_of_uri uri in if metasenv <> [] then command_error "Proof not completed! metasenv is not empty!"; let proved_ty,ugraph = CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in let b,ugraph = CicReduction.are_convertible [] proved_ty ty ugraph in if not b then command_error ("The type of your proof is not convertible with the "^ "type you've declared!"); MatitaLog.message (sprintf "%s defined" suri); let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in let status = let name = UriManager.name_of_uri uri in let new_env = env_of_list [(name,suri)] status.aliases in {status with aliases = new_env } in {status with proof_status = No_proof } | TacticAst.Inductive (loc, dummy_params, types) -> (* dummy_params are not real params, it is a list of nothing, and the only * semantic content is the len, that is leftno (note: leftno and pamaters * have nothing in common). *) let suri = match types with | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind" | _ -> assert false in let uri = UriManager.uri_of_string suri in let leftno = List.length dummy_params in let obj = Cic.InductiveDefinition (types, [], leftno, []) in let ugraph = CicTypeChecker.typecheck_mutual_inductive_defs uri (types, [], leftno) CicUniv.empty_ugraph in let status = MatitaSync.add_inductive_def ~uri ~types ~params:[] ~leftno ~ugraph status in (* aliases for the constructors and types *) let aliases = env_of_list (extract_alias types uri) status.aliases in (* aliases for the eliminations principles *) let aliases = let base = String.sub suri 0 (String.length suri - 4) in env_of_list (List.fold_left ( fun acc suffix -> if List.exists ( fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix ) status.objects then let u = base ^ suffix in (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc else acc ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases in let status = {status with proof_status = No_proof } in { status with aliases = aliases} | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") in let goalno = 1 in let metasenv, body = match status.proof_status with | Intermediate metasenv -> ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[]) | _-> assert false in let initial_proof = (Some uri, metasenv, body, ty) in { status with proof_status = Incomplete_proof (initial_proof,goalno)} | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") in let metasenv = MatitaMisc.get_proof_metasenv status in let (body_type, ugraph) = CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph in let (subst, metasenv, ugraph) = CicUnification.fo_unif metasenv [] body_type ty ugraph in if metasenv <> [] then command_error "metasenv not empty while giving a definition with body"; let body = CicMetaSubst.apply_subst subst body in let ty = CicMetaSubst.apply_subst subst ty in let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in let status = let suri = UriManager.string_of_uri uri in let new_env = env_of_list [(name,suri)] status.aliases in {status with aliases = new_env } in {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> command_error "The grammar should avoid having unnamed theorems!" | TacticAst.Coercion (loc, term) -> assert false (** TODO *) | TacticAst.Alias (loc, spec) -> match spec with | TacticAst.Ident_alias (id,uri) -> {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) status.aliases } | TacticAst.Symbol_alias (symb, instance, desc) -> {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symb,instance)) (DisambiguateChoices.lookup_symbol_by_dsc symb desc) status.aliases } | TacticAst.Number_alias (instance,desc) -> {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } let eval_executable status ex = match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac | TacticAst.Command (_, cmd) -> eval_command status cmd | TacticAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" (TacticAstPp.pp_macro_cic mac)) let eval_comment status c = status let eval status st = match st with | TacticAst.Executable (_,ex) -> eval_executable status ex | TacticAst.Comment (_,c) -> eval_comment status c let disambiguate_term status term = let (aliases, metasenv, cic, _) = match MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) ~metasenv:(MatitaMisc.get_proof_metasenv status) term with | [x] -> x | _ -> assert false in let proof_status = match status.proof_status with | No_proof -> Intermediate metasenv | Incomplete_proof ((uri, _, proof, ty), goal) -> Incomplete_proof ((uri, metasenv, proof, ty), goal) | Intermediate _ -> Intermediate metasenv | Proof _ -> assert false in let status = { status with aliases = aliases; proof_status = proof_status } in status, cic let disambiguate_terms status terms = let term = CicAst.pack terms in let status, term = disambiguate_term status term in status, CicUtil.unpack term let disambiguate_tactic status = function | TacticAst.Transitivity (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Transitivity (loc, cic) | TacticAst.Apply (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Apply (loc, cic) | TacticAst.Absurd (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Absurd (loc, cic) | TacticAst.Exact (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Exact (loc, cic) | TacticAst.Cut (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.Cut (loc, cic) | TacticAst.Elim (loc, term, Some term') -> let status, cic1 = disambiguate_term status term in let status, cic2 = disambiguate_term status term' in status, TacticAst.Elim (loc, cic1, Some cic2) | TacticAst.Elim (loc, term, None) -> let status, cic = disambiguate_term status term in status, TacticAst.Elim (loc, cic, None) | TacticAst.ElimType (loc, term) -> let status, cic = disambiguate_term status term in status, TacticAst.ElimType (loc, cic) | TacticAst.Replace (loc, what, with_what) -> let status, cic1 = disambiguate_term status what in let status, cic2 = disambiguate_term status with_what in status, TacticAst.Replace (loc, cic1, cic2) | TacticAst.Change (loc, what, with_what, ident) -> let status, cic1 = disambiguate_term status what in let status, cic2 = disambiguate_term status with_what in status, TacticAst.Change (loc, cic1, cic2, ident) (* (* TODO Zack a lot more of tactics to be implemented here ... *) | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option | TacticAst.Change of 'term * 'term * 'ident option | TacticAst.Decompose of 'ident * 'ident list | TacticAst.Discriminate of 'ident | TacticAst.Fold of reduction_kind * 'term | TacticAst.Injection of 'ident | TacticAst.LetIn of 'term * 'ident | TacticAst.Replace_pattern of 'term pattern * 'term *) | TacticAst.ReduceAt (loc, reduction_kind, ident, path) -> let path = Disambiguate.interpretate [] status.aliases path in status, TacticAst.ReduceAt(loc, reduction_kind, ident, path) | TacticAst.Reduce (loc, reduction_kind, opts) -> let status, opts = match opts with | None -> status, None | Some (l,pat) -> let status, l = List.fold_right (fun t (status,acc) -> let status',t' = disambiguate_term status t in status', t'::acc) l (status,[]) in status, Some (l, pat) in status, TacticAst.Reduce (loc, reduction_kind, opts) | TacticAst.Rewrite (loc,dir,t,ident) -> let status, term = disambiguate_term status t in status, TacticAst.Rewrite (loc,dir,term,ident) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc | TacticAst.Assumption loc -> status, TacticAst.Assumption loc | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc | TacticAst.Exists loc -> status, TacticAst.Exists loc | TacticAst.Fourier loc -> status, TacticAst.Fourier loc | TacticAst.Left loc -> status, TacticAst.Left loc | TacticAst.Right loc -> status, TacticAst.Right loc | TacticAst.Ring loc -> status, TacticAst.Ring loc | TacticAst.Split loc -> status, TacticAst.Split loc | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) | x -> print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x); assert false let rec disambiguate_tactical status = function | TacticAst.Tactic (loc, tactic) -> let status, tac = disambiguate_tactic status tactic in status, TacticAst.Tactic (loc, tac) | TacticAst.Do (loc, num, tactical) -> let status, tac = disambiguate_tactical status tactical in status, TacticAst.Do (loc, num, tac) | TacticAst.Repeat (loc, tactical) -> let status, tac = disambiguate_tactical status tactical in status, TacticAst.Repeat (loc, tac) | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) let status, tacticals = disambiguate_tacticals status tacticals in let tacticals = List.rev tacticals in status, TacticAst.Seq (loc, tacticals) | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) let status, tactical = disambiguate_tactical status tactical in let status, tacticals = disambiguate_tacticals status tacticals in status, TacticAst.Then (loc, tactical, tacticals) | TacticAst.Tries (loc, tacticals) -> let status, tacticals = disambiguate_tacticals status tacticals in status, TacticAst.Tries (loc, tacticals) | TacticAst.Try (loc, tactical) -> let status, tactical = disambiguate_tactical status tactical in status, TacticAst.Try (loc, tactical) | (TacticAst.IdTac _ | TacticAst.Fail _) as tac -> status, tac and disambiguate_tacticals status tacticals = let status, tacticals = List.fold_left (fun (status, tacticals) tactical -> let status, tac = disambiguate_tactical status tactical in status, tac :: tacticals) (status, []) tacticals in let tacticals = List.rev tacticals in status, tacticals let disambiguate_inddef status params indTypes = 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 status, terms = disambiguate_terms status !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, _, _, _) :: _ -> MatitaMisc.qualify status 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 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) let disambiguate_command status = function | TacticAst.Inductive (loc, params, types) -> let (status, (uri, (ind_types, vars, paramsno))) = disambiguate_inddef status params types in let rec mk_list = function | 0 -> [] | n -> ("", Cic.Rel ~-117) :: mk_list (n-1) in (* once we've built the cic inductive types we no longer need terms corresponding to parameters, but we need the leftno, and we encode it as the length of dummy_params *) let dummy_params = mk_list paramsno in status, TacticAst.Inductive (loc, dummy_params, ind_types) | TacticAst.Theorem (loc, thm_flavour, name, ty, body) -> let status, ty = disambiguate_term status ty in let status, body = match body with | None -> status, None | Some body -> let status, body = disambiguate_term status body in status, Some body in status, TacticAst.Theorem (loc, thm_flavour, name, ty, body) | TacticAst.Coercion (loc, term) -> assert false (** TODO *) | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> status, cmd | TacticAst.Alias _ as x -> status, x let disambiguate_executable status ex = match ex with | TacticAst.Tactical (loc, tac) -> let status, tac = disambiguate_tactical status tac in status, (TacticAst.Tactical (loc, tac)) | TacticAst.Command (loc, cmd) -> let status, cmd = disambiguate_command status cmd in status, (TacticAst.Command (loc, cmd)) | TacticAst.Macro (_, mac) -> command_error (sprintf ("The engine is not allowed to disambiguate any macro, "^^ "in particular %s") (TacticAstPp.pp_macro_ast mac)) let disambiguate_comment status c = match c with | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n) | TacticAst.Code (loc,ex) -> let status, ex = disambiguate_executable status ex in status, TacticAst.Code (loc,ex) let disambiguate_statement status statement = match statement with | TacticAst.Comment (loc,c) -> let status, c = disambiguate_comment status c in status, TacticAst.Comment (loc,c) | TacticAst.Executable (loc,ex) -> let status, ex = disambiguate_executable status ex in status, TacticAst.Executable (loc,ex) let eval_ast status ast = let status,st = disambiguate_statement status ast in (* this disambiguation step should be deferred to support tacticals *) eval status st let eval_from_stream status str cb = let stl = CicTextualParser2.parse_statements str in List.fold_left (fun status ast -> cb status ast;eval_ast status ast) status stl let eval_string status str = eval_from_stream status (Stream.of_string str) (fun _ _ -> ()) let default_options () = let options = StringMap.add "baseuri" (String (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner")) no_options in let options = StringMap.add "basedir" (String (Helm_registry.get "matita.basedir" )) options in options let initial_status = lazy { aliases = DisambiguateTypes.empty_environment; proof_status = No_proof; options = default_options (); coercions = []; objects = []; }