X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=148f550fdcee8f3946d949f32e5bca86e605c193;hb=53ee2f5095adadffcafb40e436d23dc330d3bd87;hp=ae933d2d0022a1f08d7dca832f633a8024840ebe;hpb=15a4844b5d8f64a72964e5a917b6bd6d8d7dbe44;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index ae933d2d0..148f550fd 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -2,7 +2,7 @@ open Printf open MatitaTypes -let debug = true ;; +let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; (** create a ProofEngineTypes.mk_fresh_name_type function which uses given @@ -25,7 +25,8 @@ let tactic_of_ast = function 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) () + PrimitiveTactics.intros_tac ~howmany:num + ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Reflexivity _ -> Tactics.reflexivity | TacticAst.Assumption _ -> Tactics.assumption | TacticAst.Contradiction _ -> Tactics.contradiction @@ -49,7 +50,7 @@ let tactic_of_ast = function | 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 ()) + AutoTactic.auto_tac ~num (MatitaDb.instance ()) | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what (* (* TODO Zack a lot more of tactics to be implemented here ... *) @@ -62,7 +63,7 @@ let tactic_of_ast = function | TacticAst.Replace_pattern of 'term pattern * 'term *) | TacticAst.LetIn (loc,term,name) -> - Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name]) + Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) | TacticAst.ReduceAt (_,reduction_kind,ident,path) -> ProofEngineTypes.mk_tactic (fun (((_,metasenv,_,_),goal) as status) -> @@ -78,7 +79,9 @@ let tactic_of_ast = function | _ -> false) context with - Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis")) + Not_found -> + raise (ProofEngineTypes.Fail + (ident ^ " is not an hypothesis")) in (match hyp with | Some (_, Cic.Decl term) -> term @@ -159,31 +162,6 @@ let eval_tactical status tac = 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_coercion status coercion = let coer_uri,coer_ty = match coercion with @@ -225,8 +203,15 @@ let eval_coercion status coercion = aux ty in let ty_src,ty_tgt = extract_last_two_p coer_ty in - let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in - let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in + let context = [] in + let src_uri = + let ty_src = CicReduction.whd context ty_src in + UriManager.uri_of_string (CicUtil.uri_of_term ty_src) + in + let tgt_uri = + let ty_tgt = CicReduction.whd context ty_tgt in + UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) + in let new_coercions = (* also adds them to the Db *) CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri @@ -271,16 +256,16 @@ let eval_command status cmd = "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.Record (loc, params, name, ty, fields) -> + let suri = MatitaMisc.qualify status name ^ ".ind" in + let record_spec = (suri, params, ty, fields) in + let status = MatitaSync.add_record_def record_spec status 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). + * semantic content is the len, that is leftno (note: leftno and + * paramaters have nothing in common). *) let suri = match types with @@ -295,28 +280,9 @@ let eval_command status cmd = (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 + MatitaSync.add_inductive_def ~uri ~types ~leftno ~ugraph status in - let status = {status with proof_status = No_proof } in - { status with aliases = aliases} + {status with proof_status = No_proof } | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") @@ -335,7 +301,6 @@ let eval_command status cmd = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") in let metasenv = MatitaMisc.get_proof_metasenv status in - debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body); let (body_type, ugraph) = CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph in @@ -343,16 +308,12 @@ let eval_command status cmd = CicUnification.fo_unif metasenv [] body_type ty ugraph in if metasenv <> [] then - command_error - "metasenv not empty while giving a definition with body"; + command_error ( + "metasenv not empty while giving a definition with body: " ^ + CicMetaSubst.ppmetasenv metasenv []) ; 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!" @@ -418,7 +379,7 @@ let disambiguate_term status term = in status, cic -let disambiguate_terms status terms = +let disambiguate_closedtypes status terms = let term = CicAst.pack terms in let status, term = disambiguate_term status term in status, CicUtil.unpack term @@ -567,7 +528,7 @@ let disambiguate_inddef status params indTypes = 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 status, terms = disambiguate_closedtypes status !asts in let terms = ref (List.rev terms) in let get_term () = match !terms with [] -> assert false | hd :: tl -> terms := tl; hd @@ -605,7 +566,41 @@ let disambiguate_inddef status params indTypes = let cicIndTypes = List.rev cicIndTypes in status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) +let disambiguate_record status params ty fields = + let packed = + List.fold_right + (fun (name,ast) acc -> + CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) + (params @ ["",ty] @ fields) (CicAst.Sort `Type) + in + debug_print (CicAstPp.pp_term packed); + let status, packed = disambiguate_term status packed in + let rec split t = function + | [] -> [],t + | (n,_)::tl -> + match t with + | Cic.Prod (_, src, tgt) -> + let l, t = split tgt tl in + (n, src) :: l, t + | _-> assert false + in + let params, t = split packed params in + let ty, t = + match t with + | Cic.Prod (_ , ty, t) -> ty, t + | _ -> assert false + in + let fields, _ = + split (let t,_,_ = CicMetaSubst.delift_rels [] [] 1 t in t) fields + in + params, ty, fields + let disambiguate_command status = function + | TacticAst.Record(loc, params,name,ty,fields) -> + let params, ty, fields = + disambiguate_record status params ty fields + in + status, TacticAst.Record(loc, params, name, ty, fields) | TacticAst.Inductive (loc, params, types) -> let (status, (uri, (ind_types, vars, paramsno))) = disambiguate_inddef status params types @@ -646,9 +641,8 @@ let disambiguate_executable status ex = 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)) + command_error (sprintf "The macro %s can't be in a script" + (TacticAstPp.pp_macro_ast mac)) let disambiguate_comment status c = match c with @@ -702,3 +696,4 @@ let initial_status = objects = []; } +