From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 10:55:08 +0000 (+0000) Subject: Big commit and major code clean-up: X-Git-Tag: PRE_STORAGE~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git Big commit and major code clean-up: 1. added a refine function for objects 2. added a disambiguation function for objects 3. MatitaEngine now uses the disambiguation function for objects 4. added CicTypeChecker.typecheck_obj to typecheck an object and add it to the environment --- diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml new file mode 100644 index 000000000..b50ef5b98 --- /dev/null +++ b/helm/matita/matita.conf.xml @@ -0,0 +1,27 @@ + + +
+ true + true + cic:/matita/ + .matita/xml + sacerdot + +
+
+ + mowgli.cs.unibo.it + helm + matita +
+
+ true + + file:///projects/helm/library/coq_contribs + + .matita/getter/cache + .matita/getter/maps + /projects/helm/xml/dtd + +
+ diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index eee43a935..d4365d1cc 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -2,6 +2,7 @@ (**********************************************************************) TODO +- uri_of_term and term_of_uri: cambiare il tipo per far tornare delle uri!!! - eta_expand non usata da nessuno? - eliminare eta_fix? (aspettare notazione da Zack e Luca) - bug di ferruccio: fare un refresh dei nomi dopo l'applicazione diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index fcbcdea14..f6db501b3 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -63,3 +63,4 @@ module Disambiguator = Disambiguate.Make (Callbacks) let disambiguate_term = Disambiguator.disambiguate_term +let disambiguate_obj = Disambiguator.disambiguate_obj diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 148f550fd..2ac69a575 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -214,19 +214,46 @@ let eval_coercion status coercion = in let new_coercions = (* also adds them to the Db *) - CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri - in - let status = - List.fold_left ( - fun s (uri,o,ugraph) -> - match o with - | Cic.Constant (_,Some body, ty, params, attrs) -> - MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status - | _ -> assert false - ) status new_coercions - in + CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in + let status = + List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) + status new_coercions in {status with proof_status = No_proof} - + +let generate_elimination_principles uri status = + let elim sort status = + try + let uri,obj = CicElim.elim_of ~sort uri 0 in + MatitaSync.add_obj uri obj status + with CicElim.Can_t_eliminate -> status + in + List.fold_left (fun status sort -> elim sort status) status + [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] + +let generate_projections uri status = + let projections = CicRecord.projections_of uri in + List.fold_left + (fun status (uri, name, bo) -> + try + let ty, ugraph = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let bo = Unshare.unshare bo in + let ty = Unshare.unshare ty in + let attrs = [`Class `Projection; `Generated] in + let obj = Cic.Constant (name,Some bo,ty,[],attrs) in + MatitaSync.add_obj uri obj status + with + CicTypeChecker.TypeCheckerFailure s -> + MatitaLog.message + ("Unable to create projection " ^ name ^ " cause: " ^ s); + status + | CicEnvironment.Object_not_found uri -> + let depend = UriManager.name_of_uri uri in + MatitaLog.message + ("Unable to create projection " ^ name ^ " because it requires " ^ depend); + status + ) status projections + let eval_command status cmd = match cmd with | TacticAst.Set (loc, name, value) -> set_option status name value @@ -244,83 +271,13 @@ let eval_command status cmd = 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 - {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 - * paramaters 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 ~leftno ~ugraph status - in - {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") - 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: " ^ - 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 - {status with proof_status = No_proof} - | TacticAst.Theorem (_, _, None, _, _) -> - command_error "The grammar should avoid having unnamed theorems!" + let name = UriManager.name_of_uri uri in + let obj = Cic.Constant (name,Some bo,ty,[],[]) in + MatitaSync.add_obj uri obj status | TacticAst.Coercion (loc, coercion) -> eval_coercion status coercion | TacticAst.Alias (loc, spec) -> - match spec with + (match spec with | TacticAst.Ident_alias (id,uri) -> {status with aliases = DisambiguateTypes.Environment.add @@ -337,7 +294,43 @@ let eval_command status cmd = {status with aliases = DisambiguateTypes.Environment.add (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } + (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }) + | TacticAst.Obj (loc,obj) -> + let ext,name = + match obj with + Cic.Constant (name,_,_,_,_) + | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name + | Cic.InductiveDefinition (types,_,_,_) -> + ".ind", + (match types with (name,_,_,_)::_ -> name | _ -> assert false) + | _ -> assert false in + let uri = + UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) + in + let metasenv = MatitaMisc.get_proof_metasenv status in + match obj with + Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> + assert (metasenv = metasenv'); + let goalno = + match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in + let initial_proof = (Some uri, metasenv, bo, ty) in + { status with proof_status = Incomplete_proof (initial_proof,goalno)} + | _ -> + if metasenv <> [] then + command_error ( + "metasenv not empty while giving a definition with body: " ^ + CicMetaSubst.ppmetasenv metasenv []); + let status = MatitaSync.add_obj uri obj status in + match obj with + Cic.Constant _ -> status + | Cic.InductiveDefinition (_,_,_,attrs) + when List.mem (`Class `Record) attrs -> + let status = generate_elimination_principles uri status in + generate_projections uri status + | Cic.InductiveDefinition (_,_,_,_) -> + generate_elimination_principles uri status + | Cic.CurrentProof _ + | Cic.Variable _ -> assert false let eval_executable status ex = match ex with @@ -379,6 +372,36 @@ let disambiguate_term status term = in status, cic +let disambiguate_obj status obj = + let uri = + match obj with + TacticAst.Inductive (_,(name,_,_,_)::_) + | TacticAst.Record (_,name,_,_) -> + Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind")) + | TacticAst.Inductive _ -> assert false + | _ -> None in + let (aliases, metasenv, cic, _) = + match + MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) + ~aliases:(status.aliases) ~uri obj + with + | [x] -> x + | _ -> assert false + in + let proof_status = + match status.proof_status with + | No_proof -> Intermediate metasenv + | Incomplete_proof _ + | Intermediate _ + | Proof _ -> assert false + in + let status = + { status with + aliases = aliases; + proof_status = proof_status } + in + status, cic + let disambiguate_closedtypes status terms = let term = CicAst.pack terms in let status, term = disambiguate_term status term in @@ -432,7 +455,7 @@ let disambiguate_tactic status = function let status, term = disambiguate_term status term in status, TacticAst.LetIn (loc,term,name) | TacticAst.ReduceAt (loc, reduction_kind, ident, path) -> - let path = Disambiguate.interpretate [] status.aliases path in + let path = Disambiguate.interpretate_path [] status.aliases path in status, TacticAst.ReduceAt(loc, reduction_kind, ident, path) | TacticAst.Reduce (loc, reduction_kind, opts) -> let status, opts = @@ -508,129 +531,16 @@ and disambiguate_tacticals status tacticals = 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_closedtypes 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_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 - 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) -> let status, term = disambiguate_term status term in status, TacticAst.Coercion (loc,term) | (TacticAst.Set _ | TacticAst.Qed _) as cmd -> status, cmd | TacticAst.Alias _ as x -> status, x + | TacticAst.Obj (loc,obj) -> + let status,obj = disambiguate_obj status obj in + status, TacticAst.Obj (loc,obj) let disambiguate_executable status ex = match ex with diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index d549405bb..f0730bcca 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -29,15 +29,17 @@ val eval_string: MatitaTypes.status -> string -> MatitaTypes.status val eval_from_stream: MatitaTypes.status -> char Stream.t -> - (MatitaTypes.status -> (CicAst.term,string) TacticAst.statement -> unit) -> + (MatitaTypes.status -> + (CicAst.term,TacticAst.obj,string) TacticAst.statement -> unit) -> MatitaTypes.status val eval_ast: - MatitaTypes.status -> (CicAst.term, string) TacticAst.statement -> + MatitaTypes.status -> + (CicAst.term,TacticAst.obj,string) TacticAst.statement -> MatitaTypes.status val eval: - MatitaTypes.status -> (Cic.term, string) TacticAst.statement -> + MatitaTypes.status -> (Cic.term,Cic.obj,string) TacticAst.statement -> MatitaTypes.status val initial_status: MatitaTypes.status lazy_t diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 850c23ddd..3a7f6dd32 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -40,24 +40,11 @@ let extract_alias types uri = ) (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 add_aliases_for_object status suri = - let uri = UriManager.uri_of_string suri in - let name = UriManager.name_of_uri uri in - let new_env = env_of_list [(name,suri)] status.aliases in - {status with aliases = new_env } +let env_of_list l env = + let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in + DisambiguateTypes.env_of_list l' env +(* let add_aliases_for_inductive_def status types suri = let uri = UriManager.uri_of_string suri in (* aliases for the constructors and types *) @@ -78,6 +65,26 @@ let add_aliases_for_inductive_def status types suri = ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases in {status with aliases = aliases } +*) + +let add_aliases_for_inductive_def status types suri = + let uri = UriManager.uri_of_string suri in + let aliases = env_of_list (extract_alias types uri) status.aliases in + {status with aliases = aliases } + +let add_alias_for_constant status suri = + let uri = UriManager.uri_of_string suri in + let name = UriManager.name_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + {status with aliases = new_env } + +let add_aliases_for_object status suri = + function + Cic.InductiveDefinition (types,_,_,_) -> + add_aliases_for_inductive_def status types suri + | Cic.Constant _ -> add_alias_for_constant status suri + | Cic.Variable _ + | Cic.CurrentProof _ -> assert false let paths_and_uris_of_obj uri status = let basedir = get_string_option status "basedir" in @@ -145,97 +152,20 @@ let remove_object_from_disk uri path = Sys.remove path; Http_getter.unregister' uri -let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = +let add_obj uri obj status = let dbd = MatitaDb.instance () in let suri = UriManager.string_of_uri uri in if CicEnvironment.in_library uri then - command_error (sprintf "%s constant already defined" suri) + command_error (sprintf "%s already defined" suri) else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name, body, ty, params, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.add_type_checked_term uri (obj, ugraph); + CicTypeChecker.typecheck_obj uri obj; MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in - MatitaLog.message (sprintf "%s constant defined" suri); - let status = add_aliases_for_object status suri in - { status with objects = new_stuff @ status.objects } + MatitaLog.message (sprintf "%s defined" suri); + let status = add_aliases_for_object status suri obj in + { status with objects = new_stuff @ status.objects; + proof_status = No_proof } end - -let split_obj = function - | Cic.Constant (name, body, ty, _, attrs) - | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs) - | _ -> assert false - -let add_inductive_def - ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status -= - let dbd = MatitaDb.instance () in - let suri = UriManager.string_of_uri uri in - if CicEnvironment.in_library uri then - command_error (sprintf "%s inductive type already defined" suri) - else begin - let name = UriManager.name_of_uri uri in - let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in - let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in - CicEnvironment.put_inductive_definition uri (obj, ugraph); - MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) - let new_stuff = save_object_to_disk status uri obj in - MatitaLog.message (sprintf "%s inductive type defined" suri); - let status = add_aliases_for_inductive_def status types suri in - let status = { status with objects = new_stuff @ status.objects } in - let elim sort status = - try - let obj = CicElim.elim_of ~sort uri 0 in - let (name, body, ty, attrs) = split_obj obj in - let suri = MatitaMisc.qualify status name ^ ".con" in - let uri = UriManager.uri_of_string suri in - (* TODO Zack: make CicElim returns a universe *) - let ugraph = CicUniv.empty_ugraph in - add_constant ~uri ?body ~ty ~attrs ~ugraph status; - with CicElim.Can_t_eliminate -> status - in - List.fold_left - (fun status sort -> elim sort status) - status - [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; - end - -let add_record_def (suri, params, ty, fields) status = - let module CTC = CicTypeChecker in - let uri = UriManager.uri_of_string suri in - let buri = UriManager.buri_of_uri uri in - let record_spec = suri, params, ty, fields in - let types, leftno, obj, ugraph = CicRecord.inductive_of_record record_spec in - let status = add_inductive_def ~uri ~types ~leftno ~ugraph status in - let projections = CicRecord.projections_of record_spec in - let status = - List.fold_left ( - fun status (suri, name, t) -> - try - let ty, ugraph = - CTC.type_of_aux' [] [] t CicUniv.empty_ugraph - in - (* THIS MUST BE IN SYNC WITH CicRecord *) - let uri = UriManager.uri_of_string suri in - let t = Unshare.unshare t in - let ty = Unshare.unshare ty in - let status = add_constant ~uri ~body:t ~ty ~ugraph status in - add_aliases_for_object status suri - with - | CTC.TypeCheckerFailure s -> - MatitaLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ s); - status - | Http_getter_types.Key_not_found s -> - let depend = UriManager.uri_of_string s in - let depend = UriManager.name_of_uri depend in - MatitaLog.message - ("Unable to create projection " ^ name ^ " cause uses " ^ depend); - status - ) status projections - in - status module OrderedUri = struct diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index ee0c9b6e7..d4de71f01 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -23,13 +23,10 @@ * http://helm.cs.unibo.it/ *) -val add_constant: - uri:UriManager.uri -> - ?body:Cic.term -> ty:Cic.term -> - ugraph:CicUniv.universe_graph -> - ?params:UriManager.uri list -> ?attrs:Cic.attribute list -> - MatitaTypes.status -> MatitaTypes.status +val add_obj: + UriManager.uri -> Cic.obj -> MatitaTypes.status -> MatitaTypes.status +(* val add_inductive_def: uri:UriManager.uri -> types:Cic.inductiveType list -> @@ -40,6 +37,7 @@ val add_inductive_def: val add_record_def: CicRecord.record_spec -> MatitaTypes.status -> MatitaTypes.status +*) val time_travel: present:MatitaTypes.status -> past:MatitaTypes.status -> unit diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index c75d4fda8..bc8caa223 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -1,14 +1,14 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) +(* ||T|| *) +(* ||I|| Developers: *) (* ||T|| A.Asperti, C.Sacerdoti Coen, *) (* ||A|| E.Tassi, S.Zacchiroli *) (* \ / *) (* \ / This file is distributed under the terms of the *) -(* v GNU Lesser General Public License Version 2.1 *) +(* v GNU Lesser General Public License Version 2.1 *) (* *) (**************************************************************************) @@ -19,10 +19,10 @@ I : True. inductive False: Prop \def . definition Not: Prop \to Prop \def -\lambda A:Prop. (A \to False). +\lambda A. (A \to False). theorem absurd : \forall A,C:Prop. A \to Not A \to C. -intros.cut False.elim Hcut.apply H1.assumption. +intros. elim (H1 H). qed. inductive And (A,B:Prop) : Prop \def @@ -295,6 +295,7 @@ simplify.apply le_n_S.apply H. simplify.intros.apply H.apply le_S_n.assumption. qed. +(*CSC: this requires too much time theorem prova : let three \def (S (S (S O))) in let nine \def (times three three) in @@ -304,6 +305,5 @@ let square \def (times eightyone eightyone) in intro. intro. intro.intro. -STOP normalize goal at (? ? % ?). - - +normalize goal at (? ? % ?). +*) \ No newline at end of file diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 0bf193e7d..d45078fcd 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -41,6 +41,7 @@ val strip_prods: int -> Cic.term -> Cic.term (** conversions between terms which are fully representable as uris (Var, Const, * Mutind, and MutConstruct) and corresponding tree representations *) +(*CSC: horrible: the strings are URIs. To change also DisambiguateTypes.* *) val term_of_uri: string -> Cic.term (** @raise UriManager.IllFormedUri *) val uri_of_term: Cic.term -> string (** @raise Invalid_argument "uri_of_term" *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index a7d43bb45..feb161d7f 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -553,12 +553,12 @@ EXTEND [ IDENT "set" ]; n = QSTRING; v = QSTRING -> TacticAst.Set (loc, n, v) | [ IDENT "qed" ] -> TacticAst.Qed loc - | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Theorem (loc, flavour, name, typ, body) - | flavour = theorem_flavour; name = OPT IDENT; + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body) + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = @@ -568,19 +568,19 @@ EXTEND | _ -> assert false in let body = CicAst.Ident (name,None) in - TacticAst.Theorem(loc, `Definition, Some name, ty, - Some (CicAst.LetRec (ind_kind, defs, body))) + TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty, + Some (CicAst.LetRec (ind_kind, defs, body)))) | [ IDENT "inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ IDENT "coinductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in - TacticAst.Inductive (loc, params, ind_types) + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) | [ IDENT "coercion" ] ; name = IDENT -> TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) | [ IDENT "coercion" ] ; name = URI -> @@ -588,7 +588,7 @@ EXTEND | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> - TacticAst.Record (loc, params,name,ty,fields) + TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) ]]; executable: [ diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 9e3f442d8..c95485e52 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,10 +27,11 @@ exception Parse_error of Token.flocation * string (** {2 Parsing functions} *) -val parse_term: char Stream.t -> DisambiguateTypes.term -val parse_statement: char Stream.t -> (CicAst.term, string) TacticAst.statement +val parse_term: char Stream.t -> DisambiguateTypes.term +val parse_statement: + char Stream.t -> (CicAst.term, TacticAst.obj,string) TacticAst.statement val parse_statements: - char Stream.t -> (CicAst.term, string) TacticAst.statement list + char Stream.t -> (CicAst.term, TacticAst.obj, string) TacticAst.statement list (** {2 Grammar extensions} *) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 2775aed3b..4a12727c7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -30,6 +30,7 @@ open UriManager exception No_choices of domain_item exception NoWellTypedInterpretation +exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again @@ -51,13 +52,14 @@ let descr_of_domain_item = function | Symbol (s, _) -> s | Num i -> string_of_int i -type test_result = - | Ok of Cic.term * Cic.metasenv +type 'a test_result = + | Ok of 'a * Cic.metasenv | Ko | Uncertain -let refine metasenv context term ugraph = +let refine_term metasenv context uri term ugraph = (* if benchmark then incr actual_refinements; *) + assert (uri=None); let metasenv, term = CicMkImplicit.expand_implicits metasenv [] context term in debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)); @@ -74,6 +76,22 @@ let refine metasenv context term ugraph = (CicPp.ppterm term) msg); Ko,ugraph +let refine_obj metasenv context uri obj ugraph = + assert (context = []); + let metasenv, obj = CicMkImplicit.expand_implicits_in_obj metasenv [] obj in + debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj)); + try + let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in + (Ok (obj', metasenv)),ugraph + with + | CicRefine.Uncertain s -> + debug_print ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj) ; + Uncertain,ugraph + | CicRefine.RefineFailure msg -> + debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s" + (CicPp.ppobj obj) msg); + Ko,ugraph + let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args @@ -90,7 +108,8 @@ let find_in_environment name context = in aux 1 context -let interpretate ~context ~env ast = +let interpretate_term ~context ~env ~uri ~is_path ast = + assert (uri = None); let rec aux loc context = function | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term @@ -195,6 +214,8 @@ let interpretate ~context ~env ast = Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic)) in List.fold_right (build_term inductiveFuns) inductiveFuns cic_body + | CicAst.Ident _ + | CicAst.Uri _ when is_path -> raise PathNotWellFormed | CicAst.Ident (name, subst) | CicAst.Uri (name, subst) as ast -> let is_uri = function CicAst.Uri _ -> true | _ -> false in @@ -241,9 +262,19 @@ let interpretate ~context ~env ast = let uris = CicUtil.params_of_obj o in Cic.Var (uri, mk_subst uris) | Cic.MutInd (uri, i, []) -> - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let uris = CicUtil.params_of_obj o in - Cic.MutInd (uri, i, mk_subst uris) + (try + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in + Cic.MutInd (uri, i, mk_subst uris) + with + CicEnvironment.Object_not_found _ -> + (* if we are here it is probably the case that during the + definition of a mutual inductive type we have met an + occurrence of the type in one of its constructors. + However, the inductive type is not yet in the environment + *) + (*here the explicit_named_substituion is assumed to be of length 0 *) + Cic.MutInd (uri,i,[])) | Cic.MutConstruct (uri, i, j, []) -> let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let uris = CicUtil.params_of_obj o in @@ -266,7 +297,6 @@ let interpretate ~context ~env ast = raise DisambiguateChoices.Invalid_choice)) | CicAst.Implicit -> Cic.Implicit None | CicAst.UserInput -> Cic.Implicit (Some `Hole) -(* | CicAst.UserInput -> assert false*) | CicAst.Num (num, i) -> resolve env (Num i) ~num () | CicAst.Meta (index, subst) -> let cic_subst = @@ -289,128 +319,263 @@ let interpretate ~context ~env ast = | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term | term -> aux CicAst.dummy_floc context term -let domain_of_term ~context ast = - (* "aux" keeps domain in reverse order and doesn't care about duplicates. - * Domain item more in deep in the list will be processed first. - *) - let rec aux loc context = function - | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term - | CicAst.AttributedTerm (_, term) -> aux loc context term - | CicAst.Appl terms -> - List.fold_left (fun dom term -> aux loc context term @ dom) [] terms - | CicAst.Binder (kind, (var, typ), body) -> - let kind_dom = - match kind with - | `Exists -> [ Symbol ("exists", 0) ] - | _ -> [] - in - let type_dom = aux_option loc context typ in - let body_dom = aux loc (var :: context) body in - body_dom @ type_dom @ kind_dom - | CicAst.Case (term, indty_ident, outtype, branches) -> - let term_dom = aux loc context term in - let outtype_dom = aux_option loc context outtype in - let get_first_constructor = function - | [] -> [] - | ((head, _), _) :: _ -> [ Id head ] - in - let do_branch ((head, args), term) = - let (term_context, args_domain) = - List.fold_left - (fun (cont, dom) (name, typ) -> - (name :: cont, - (match typ with - | None -> dom - | Some typ -> aux loc cont typ @ dom))) - (context, []) args - in - args_domain @ aux loc term_context term - in - let branches_dom = - List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches - in - branches_dom @ outtype_dom @ term_dom @ - (match indty_ident with - | None -> get_first_constructor branches - | Some ident -> [ Id ident ]) - | CicAst.LetIn ((var, typ), body, where) -> - let body_dom = aux loc context body in - let type_dom = aux_option loc context typ in - let where_dom = aux loc (var :: context) where in - where_dom @ type_dom @ body_dom - | CicAst.LetRec (kind, defs, where) -> - let context' = - List.fold_left (fun acc ((var, typ), _, _) -> var :: acc) - context defs - in - let where_dom = aux loc context' where in - let defs_dom = - List.fold_left - (fun dom ((_, typ), body, _) -> - aux loc context' body @ aux_option loc context typ) - [] defs - in - where_dom @ defs_dom - | CicAst.Ident (name, subst) -> - (try - let index = find_in_environment name context in - if subst <> None then - CicTextualParser2.fail loc - "Explicit substitutions not allowed here" - else - [] - with Not_found -> - (match subst with - | None -> [Id name] - | Some subst -> - List.fold_left - (fun dom (_, term) -> - let dom' = aux loc context term in - dom' @ dom) - [Id name] subst)) - | CicAst.Uri _ -> [] - | CicAst.Implicit -> [] - | CicAst.Num (num, i) -> [ Num i ] - | CicAst.Meta (index, local_context) -> - List.fold_left (fun dom term -> aux_option loc context term @ dom) [] - local_context - | CicAst.Sort _ -> [] - | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] - | CicAst.UserInput -> assert false +let interpretate_path ~context ~env path = + interpretate_term ~context ~env ~uri:None ~is_path:true path - and aux_option loc context = function - | None -> [] - | Some t -> aux loc context t - in +let interpretate_obj ~context ~env ~uri ~is_path obj = + assert (context = []); + assert (is_path = false); + match obj with + | TacticAst.Inductive (params,tyl) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + (Cic.Name name)::context, + (name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right + (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + let name_to_uris = + snd ( + List.fold_left + (*here the explicit_named_substituion is assumed to be of length 0 *) + (fun (i,res) (name,_,_,_) -> + i + 1,(name,name,Cic.MutInd (uri,i,[]))::res + ) (0,[]) tyl) in + let con_env = DisambiguateTypes.env_of_list name_to_uris env in + let undebrujin t = + snd + (List.fold_right + (fun (name,_,_,_) (i,t) -> + (*here the explicit_named_substituion is assumed to be of length 0 *) + let t' = Cic.MutInd (uri,i,[]) in + let t = CicSubstitution.subst t' t in + i - 1,t + ) tyl (List.length tyl - 1,t)) in + let tyl = + List.map + (fun (name,b,ty,cl) -> + let ty' = add_params (interpretate_term context env None false ty) in + let cl' = + List.map + (fun (name,ty) -> + let ty' = + add_params (interpretate_term context con_env None false ty) + in + name,undebrujin ty' + ) cl + in + name,b,ty',cl' + ) tyl + in + Cic.InductiveDefinition (tyl,[],List.length params,[]) + | TacticAst.Record (params,name,ty,fields) -> + let uri = match uri with Some uri -> uri | None -> assert false in + let context,params = + let context,res = + List.fold_left + (fun (context,res) (name,t) -> + (Cic.Name name)::context, + (name, interpretate_term context env None false t)::res + ) ([],[]) params + in + context,List.rev res in + let add_params = + List.fold_right + (fun (name,ty) t -> Cic.Prod (Cic.Name name,ty,t)) params in + let ty' = add_params (interpretate_term context env None false ty) in + let fields' = + snd ( + List.fold_left + (fun (context,res) (name,ty) -> + let context' = (Cic.Name name)::context in + context',(name,interpretate_term context env None false ty)::res + ) (context,[]) fields) in + let concl = + (*here the explicit_named_substituion is assumed to be of length 0 *) + let mutind = Cic.MutInd (uri,0,[]) in + if params = [] then mutind + else Cic.Appl (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in + let con = + List.fold_left + (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t)) + concl fields' in + let con' = add_params con in + let tyl = [name,true,ty',["mk_" ^ name,con']] in + Cic.InductiveDefinition (tyl,[],List.length params,[`Class `Record]) + | TacticAst.Theorem (_,name,ty,bo) -> + let ty' = interpretate_term [] env None false ty in + match bo with + None -> + Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[]) + | Some bo -> + let bo' = Some (interpretate_term [] env None false bo) in + Cic.Constant (name,bo',ty',[],[]) - (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) - let rev_uniq = - let module SortedItem = - struct - type t = DisambiguateTypes.domain_item - let compare = Pervasives.compare - end + (* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *) +let rev_uniq = + let module SortedItem = + struct + type t = DisambiguateTypes.domain_item + let compare = Pervasives.compare + end + in + let module Set = Set.Make (SortedItem) in + fun l -> + let rev_l = List.rev l in + let (_, uniq_rev_l) = + List.fold_left + (fun (members, rev_l) elt -> + if Set.mem elt members then + (members, rev_l) + else + Set.add elt members, elt :: rev_l) + (Set.empty, []) rev_l in - let module Set = Set.Make (SortedItem) in - fun l -> - let rev_l = List.rev l in - let (_, uniq_rev_l) = + List.rev uniq_rev_l + +(* "aux" keeps domain in reverse order and doesn't care about duplicates. + * Domain item more in deep in the list will be processed first. + *) +let rec domain_rev_of_term ?(loc = CicAst.dummy_floc) context = function + | CicAst.AttributedTerm (`Loc loc, term) -> + domain_rev_of_term ~loc context term + | CicAst.AttributedTerm (_, term) -> domain_rev_of_term ~loc context term + | CicAst.Appl terms -> + List.fold_left + (fun dom term -> domain_rev_of_term ~loc context term @ dom) [] terms + | CicAst.Binder (kind, (var, typ), body) -> + let kind_dom = + match kind with + | `Exists -> [ Symbol ("exists", 0) ] + | _ -> [] + in + let type_dom = domain_rev_of_term_option loc context typ in + let body_dom = domain_rev_of_term ~loc (var :: context) body in + body_dom @ type_dom @ kind_dom + | CicAst.Case (term, indty_ident, outtype, branches) -> + let term_dom = domain_rev_of_term ~loc context term in + let outtype_dom = domain_rev_of_term_option loc context outtype in + let get_first_constructor = function + | [] -> [] + | ((head, _), _) :: _ -> [ Id head ] + in + let do_branch ((head, args), term) = + let (term_context, args_domain) = + List.fold_left + (fun (cont, dom) (name, typ) -> + (name :: cont, + (match typ with + | None -> dom + | Some typ -> domain_rev_of_term ~loc cont typ @ dom))) + (context, []) args + in + args_domain @ domain_rev_of_term ~loc term_context term + in + let branches_dom = + List.fold_left (fun dom branch -> do_branch branch @ dom) [] branches + in + branches_dom @ outtype_dom @ term_dom @ + (match indty_ident with + | None -> get_first_constructor branches + | Some ident -> [ Id ident ]) + | CicAst.LetIn ((var, typ), body, where) -> + let body_dom = domain_rev_of_term ~loc context body in + let type_dom = domain_rev_of_term_option loc context typ in + let where_dom = domain_rev_of_term ~loc (var :: context) where in + where_dom @ type_dom @ body_dom + | CicAst.LetRec (kind, defs, where) -> + let context' = + List.fold_left (fun acc ((var, typ), _, _) -> var :: acc) + context defs + in + let where_dom = domain_rev_of_term ~loc context' where in + let defs_dom = List.fold_left - (fun (members, rev_l) elt -> - if Set.mem elt members then - (members, rev_l) - else - Set.add elt members, elt :: rev_l) - (Set.empty, []) rev_l + (fun dom ((_, typ), body, _) -> + domain_rev_of_term ~loc context' body @ + domain_rev_of_term_option loc context typ) + [] defs in - List.rev uniq_rev_l - in - - rev_uniq - (match ast with - | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term - | term -> aux CicAst.dummy_floc context term) + where_dom @ defs_dom + | CicAst.Ident (name, subst) -> + (try + let index = find_in_environment name context in + if subst <> None then + CicTextualParser2.fail loc + "Explicit substitutions not allowed here" + else + [] + with Not_found -> + (match subst with + | None -> [Id name] + | Some subst -> + List.fold_left + (fun dom (_, term) -> + let dom' = domain_rev_of_term ~loc context term in + dom' @ dom) + [Id name] subst)) + | CicAst.Uri _ -> [] + | CicAst.Implicit -> [] + | CicAst.Num (num, i) -> [ Num i ] + | CicAst.Meta (index, local_context) -> + List.fold_left + (fun dom term -> domain_rev_of_term_option loc context term @ dom) [] + local_context + | CicAst.Sort _ -> [] + | CicAst.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ] + | CicAst.UserInput -> assert false + +and domain_rev_of_term_option loc context = function + | None -> [] + | Some t -> domain_rev_of_term ~loc context t + +let domain_of_term ~context ast = + rev_uniq (domain_rev_of_term context ast) +let domain_of_obj ~context ast = + assert (context = []); + let domain_rev = + match ast with + | TacticAst.Theorem (_,_,ty,bo) -> + (match bo with + None -> [] + | Some bo -> domain_rev_of_term [] bo) @ + domain_of_term [] ty + | TacticAst.Inductive (params,tyl) -> + let dom = + List.flatten ( + List.rev_map + (fun (_,_,ty,cl) -> + List.flatten ( + List.rev_map + (fun (_,ty) -> domain_rev_of_term [] ty) cl) @ + domain_rev_of_term [] ty) tyl) + in + List.filter + (fun name -> + not ( List.exists (fun (name',_) -> name = Id name') params + || List.exists (fun (name',_,_,_) -> name = Id name') tyl) + ) dom + | TacticAst.Record (params,_,ty,fields) -> + let dom = + List.flatten + (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in + let dom' = + List.filter + (fun name-> + not ( List.exists (fun (name',_) -> name = Id name') params + || List.exists (fun (name',_) -> name = Id name') fields) + ) dom + in + dom' @ domain_rev_of_term [] ty + in + rev_uniq domain_rev (* dom1 \ dom2 *) let domain_diff dom1 dom2 = @@ -434,6 +599,16 @@ sig Cic.metasenv * (* new metasenv *) Cic.term* CicUniv.universe_graph) list (* disambiguated term *) + + val disambiguate_obj : + dbd:Mysql.dbd -> + aliases:environment -> (* previous interpretation status *) + uri:UriManager.uri option -> (* required only for inductive types *) + TacticAst.obj -> + (environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.obj * + CicUniv.universe_graph) list (* disambiguated obj *) end module Make (C: Callbacks) = @@ -468,9 +643,9 @@ module Make (C: Callbacks) = fun _ _ _ -> term)) uris - let disambiguate_term ~(dbd:Mysql.dbd) ~context ~metasenv + let disambiguate_thing ~dbd ~context ~metasenv ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env - term + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing = debug_print "NEW DISAMBIGUATE INPUT"; let disambiguate_context = (* cic context -> disambiguate context *) @@ -478,14 +653,14 @@ module Make (C: Callbacks) = (function None -> Cic.Anonymous | Some (name, _) -> name) context in - debug_print ("TERM IS: " ^ (CicAstPp.pp_term term)); - let term_dom = domain_of_term ~context:disambiguate_context term in + debug_print ("TERM IS: " ^ (pp_thing thing)); + let thing_dom = domain_of_thing ~context:disambiguate_context thing in debug_print (sprintf "DISAMBIGUATION DOMAIN: %s" - (string_of_domain term_dom)); + (string_of_domain thing_dom)); let current_dom = Environment.fold (fun item _ dom -> item :: dom) current_env [] in - let todo_dom = domain_diff term_dom current_dom in + let todo_dom = domain_diff thing_dom current_dom in (* (2) lookup function for any item (Id/Symbol/Num) *) let lookup_choices = let id_choices = Hashtbl.create 1023 in @@ -519,11 +694,11 @@ module Make (C: Callbacks) = (string_of_domain_item dom_item) len); len with No_choices _ -> 0) - term_dom + thing_dom in max_refinements := List.fold_left ( * ) 1 per_item_choices; actual_refinements := 0; - domain_size := List.length term_dom; + domain_size := List.length thing_dom; choices_avg := (float_of_int !max_refinements) ** (1. /. float_of_int !domain_size) end @@ -545,10 +720,11 @@ module Make (C: Callbacks) = current_env todo_dom in try - let cic_term = - interpretate ~context:disambiguate_context ~env:filled_env term + let cic_thing = + interpretate_thing ~context:disambiguate_context ~env:filled_env + ~uri ~is_path:false thing in - let k,ugraph1 = refine metasenv context cic_term ugraph in + let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in (k , ugraph1 ) with | Try_again -> Uncertain,ugraph @@ -559,8 +735,8 @@ module Make (C: Callbacks) = match todo_dom with | [] -> (match test_env current_env [] base_univ with - | Ok (term, metasenv),new_univ -> - [ current_env, metasenv, term, new_univ ] + | Ok (thing, metasenv),new_univ -> + [ current_env, metasenv, thing, new_univ ] | Ko,_ | Uncertain,_ -> []) | item :: remaining_dom -> debug_print (sprintf "CHOOSED ITEM: %s" @@ -574,9 +750,9 @@ module Make (C: Callbacks) = Environment.add item codomain_item current_env in (match test_env new_env remaining_dom univ with - | Ok (term, metasenv),new_univ -> + | Ok (thing, metasenv),new_univ -> (match remaining_dom with - | [] -> [ new_env, metasenv, term, new_univ ] + | [] -> [ new_env, metasenv, thing, new_univ ] | _ -> aux new_env remaining_dom new_univ )@ filter univ tl | Uncertain,new_univ -> @@ -607,7 +783,7 @@ module Make (C: Callbacks) = fst (Environment.find domain_item env) in (descr_of_domain_item domain_item, description)) - term_dom) + thing_dom) l in let choosed = C.interactive_interpretation_choice choices in @@ -627,6 +803,19 @@ module Make (C: Callbacks) = with CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" + + let disambiguate_term ~dbd ~context ~metasenv + ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases term + = + disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases + ~uri:None ~pp_thing:CicAstPp.pp_term ~domain_of_thing:domain_of_term + ~interpretate_thing:interpretate_term ~refine_thing:refine_term term + + let disambiguate_obj ~dbd ~aliases ~uri obj = + disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~uri + ~pp_thing:TacticAstPp.pp_obj ~domain_of_thing:domain_of_obj + ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj + obj end module Trivial = diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index b659b38ff..ca33fa422 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -23,16 +23,15 @@ * http://helm.cs.unibo.it/ *) -open DisambiguateTypes - (** {2 Disambiguation interface} *) exception NoWellTypedInterpretation +exception PathNotWellFormed + +val interpretate_path : + context:Cic.name list -> env:DisambiguateTypes.environment -> CicAst.term -> + Cic.term -val interpretate: - context:Cic.name list -> - env:DisambiguateTypes.environment -> - CicAst.term -> Cic.term module type Disambiguator = sig @@ -41,15 +40,25 @@ sig context:Cic.context -> metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:environment -> (* previous interpretation status *) + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) CicAst.term -> - (environment * (* new interpretation status *) + (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) - Cic.term* + Cic.term * CicUniv.universe_graph) list (* disambiguated term *) + + val disambiguate_obj : + dbd:Mysql.dbd -> + aliases:DisambiguateTypes.environment ->(* previous interpretation status *) + uri:UriManager.uri option -> (* required only for inductive types *) + TacticAst.obj -> + (DisambiguateTypes.environment * (* new interpretation status *) + Cic.metasenv * (* new metasenv *) + Cic.obj * + CicUniv.universe_graph) list (* disambiguated obj *) end -module Make (C : Callbacks) : Disambiguator +module Make (C : DisambiguateTypes.Callbacks) : Disambiguator module Trivial: sig @@ -63,11 +72,10 @@ sig ?context:Cic.context -> ?metasenv:Cic.metasenv -> ?initial_ugraph:CicUniv.universe_graph -> - ?aliases:environment -> (* previous interpretation status *) + ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*) string -> - (environment * (* new interpretation status *) + (DisambiguateTypes.environment * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term * CicUniv.universe_graph) list (* disambiguated term *) end - diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 292d78e4b..078297a26 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -50,6 +50,12 @@ type codomain_item = and environment = codomain_item Environment.t +(** adds a (name,uri) list l to a disambiguation environment e **) +let env_of_list l e = + List.fold_left + (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e) + e l + module type Callbacks = sig val interactive_user_uri_choice: diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 6146a082d..bd9ba5e99 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -38,6 +38,9 @@ type codomain_item = and environment = codomain_item Environment.t +(* a simple case of extension of a disambiguation environment *) +val env_of_list: (string * string * Cic.term) list -> environment -> environment + module type Callbacks = sig diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index e47b48d5d..707a7b2b2 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -364,8 +364,11 @@ debug_print (CicPp.ppterm eliminator_body); | _ -> assert false in let name = UriManager.name_of_uri uri ^ suffix in + let buri = UriManager.buri_of_uri uri in + let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in let obj_attrs = [`Class (`Elim sort); `Generated] in - Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) + uri, + Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs) | _ -> failwith (sprintf "not an inductive definition (%s)" (UriManager.string_of_uri uri)) diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index 722e52f33..0d81b7a60 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -36,6 +36,6 @@ exception Elim_failure of string * @raise Failure * @raise Can_t_eliminate * @return Cic constant corresponding to the required elimination principle +* and its uri *) -val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> Cic.obj - +val elim_of: ?sort:Cic.sort -> UriManager.uri -> int -> UriManager.uri * Cic.obj diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 695e0cffd..86b8dd921 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -482,74 +482,77 @@ let empty = Cache.empty;; let total_parsing_time = ref 0.0 let get_object_to_add uri = - let filename = Http_getter.getxml' uri in - let bodyfilename = - match UriManager.bodyuri_of_uri uri with - None -> None - | Some bodyuri -> - try - ignore (Http_getter.resolve' bodyuri) ; - (* The body exists ==> it is not an axiom *) - Some (Http_getter.getxml' bodyuri) - with - Http_getter_types.Key_not_found _ -> - (* The body does not exist ==> we consider it an axiom *) - None - in - let cleanup () = - Unix.unlink filename ; - (* - begin - match filename_univ with - Some f -> Unix.unlink f - | None -> () - end; - *) - begin - match bodyfilename with - Some f -> Unix.unlink f - | None -> () - end - in - (* restarts the numbering of named universes (the ones inside the cic) *) - let _ = CicUniv.restart_numbering () in - let obj = - try - let time = Unix.gettimeofday() in - let rc = CicParser.obj_of_xml uri filename bodyfilename in - total_parsing_time := - !total_parsing_time +. ((Unix.gettimeofday()) -. time ); - rc - with exn -> - cleanup (); - (match exn with - | CicParser.Getter_failure ("key_not_found", uri) -> - raise (Object_not_found (UriManager.uri_of_string uri)) - | _ -> raise exn) - in + try + let filename = Http_getter.getxml' uri in + let bodyfilename = + match UriManager.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + try + ignore (Http_getter.resolve' bodyuri) ; + (* The body exists ==> it is not an axiom *) + Some (Http_getter.getxml' bodyuri) + with + Http_getter_types.Key_not_found _ -> + (* The body does not exist ==> we consider it an axiom *) + None + in + let cleanup () = + Unix.unlink filename ; + (* + begin + match filename_univ with + Some f -> Unix.unlink f + | None -> () + end; + *) + begin + match bodyfilename with + Some f -> Unix.unlink f + | None -> () + end + in + (* restarts the numbering of named universes (the ones inside the cic) *) + let _ = CicUniv.restart_numbering () in + let obj = + try + let time = Unix.gettimeofday() in + let rc = CicParser.obj_of_xml uri filename bodyfilename in + total_parsing_time := + !total_parsing_time +. ((Unix.gettimeofday()) -. time ); + rc + with exn -> + cleanup (); + (match exn with + | CicParser.Getter_failure ("key_not_found", uri) -> + raise (Object_not_found (UriManager.uri_of_string uri)) + | _ -> raise exn) + in let ugraph,filename_univ = (* FIXME: decomment this when the universes will be part of the library - try - let filename_univ = - Http_getter.getxml' ( - UriManager.uri_of_string ( - (UriManager.string_of_uri uri) ^ ".univ")) - in - (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ) - with Failure s -> - - debug_print ( - "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)); - Inix.unlink - None,None - *) - (********************************************** - TASSI: should fail when universes will be ON - ***********************************************) - (Some CicUniv.empty_ugraph,None) - in - cleanup(); - obj,ugraph + try + let filename_univ = + Http_getter.getxml' ( + UriManager.uri_of_string ( + (UriManager.string_of_uri uri) ^ ".univ")) + in + (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ) + with Failure s -> + + debug_print ( + "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)); + Inix.unlink + None,None + *) + (********************************************** + TASSI: should fail when universes will be ON + ***********************************************) + (Some CicUniv.empty_ugraph,None) + in + cleanup(); + obj,ugraph + with + Http_getter_types.Key_not_found _ -> raise (Object_not_found uri) ;; (* this is the function to fetch the object in the unchecked list and @@ -665,24 +668,11 @@ let get_obj base_univ uri = o,(CicUniv.merge_ugraphs base_univ u) ;; -exception OnlyPutOfInductiveDefinitionsIsAllowed - -let put_inductive_definition uri (obj,ugraph) = - match obj with - Cic.InductiveDefinition _ -> Cache.add_cooked uri (obj,ugraph) - | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed -;; - let in_cache uri = Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri -let add_type_checked_term uri (obj,ugraph) = - match obj with - Cic.Constant (s,(Some bo),ty,ul,_) -> - Cache.add_cooked ~key:uri (obj,ugraph) - | _ -> - assert false -;; +let add_type_checked_obj uri (obj,ugraph) = + Cache.add_cooked ~key:uri (obj,ugraph) let in_library uri = in_cache uri || diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 6108467b5..4490e6586 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -75,11 +75,14 @@ val is_type_checked : (* we find in the library, we have to calculate it and then inject it *) (* in the cacke. This is an orrible backdoor used by univ_maker. *) (* see the .ml file for some reassuring invariants *) +(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *) val set_type_checking_info : ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit -(* We need this in the Qed. *) -val add_type_checked_term : +(* this function is called by CicTypeChecker.typecheck_obj to add to the *) +(* environment a new well typed object that is not yet in the library *) +(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *) +val add_type_checked_obj : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit (** remove a type checked object @@ -97,16 +100,6 @@ val get_cooked_obj : (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) -exception OnlyPutOfInductiveDefinitionsIsAllowed - -(* put_inductive_definition uri obj *) -(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *) -(* in the environment. *) -(* WARNING: VERY UNSAFE. *) -(* This function should be called only on a well-typed definition. *) -val put_inductive_definition : - UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit - (* (de)serialization *) val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml index 7348a61fc..d8dd2dc47 100644 --- a/helm/ocaml/cic_proof_checking/cicRecord.ml +++ b/helm/ocaml/cic_proof_checking/cicRecord.ml @@ -23,90 +23,69 @@ * http://helm.cs.unibo.it/ *) -type record_spec = - string * (string * Cic.term) list * Cic.term * (string * Cic.term) list - let rec_ty uri leftno = let rec_ty = Cic.MutInd (uri,0,[]) in if leftno = 0 then rec_ty else Cic.Appl (rec_ty :: (CicUtil.mk_rels leftno 0)) -let inductive_of_record (suri,params,ty,fields) = - let uri = UriManager.uri_of_string suri in - let name = UriManager.name_of_uri uri in - let leftno = List.length params in - let constructor_ty = - List.fold_right ( - fun (name, ty) acc -> - Cic.Prod (Cic.Name name, ty, acc)) - (params @ fields) (CicSubstitution.lift (List.length fields) - (rec_ty uri leftno)) - in - let ty = - List.fold_right ( - fun (name,ty) t -> - Cic.Prod(Cic.Name name,ty, t) - ) params ty - in - let types = [name,true,ty,["mk_" ^ name,constructor_ty]] in - let obj = - Cic.InductiveDefinition (types, [],leftno,[`Class `Record]) - in - let ugraph = - CicTypeChecker.typecheck_mutual_inductive_defs uri - (types, [], leftno) CicUniv.empty_ugraph - in - types, leftno, obj, ugraph - -let projections_of (suri,params,ty,fields) = - let uri = UriManager.uri_of_string suri in - let buri = UriManager.buri_of_uri uri in - let name = UriManager.name_of_uri uri in - let leftno = List.length params in - let ty = - List.fold_right ( - fun (name,ty) t -> - Cic.Prod(Cic.Name name,ty, t) - ) params ty - in - let mk_lambdas l start = - List.fold_right (fun (name,ty) acc -> - Cic.Lambda (Cic.Name name,ty,acc)) l start - in - let recty = rec_ty uri leftno in - let _,projections,_ = - let qualify name = buri ^ "/" ^ name ^ ".con" in - let mk_oty toapp typ = - Cic.Lambda (Cic.Name "w", recty, ( - let l,_ = - List.fold_right (fun (name,_) (acc,i) -> - let u = UriManager.uri_of_string (qualify name) in - (Cic.Appl ([Cic.Const (u,[])] @ - CicUtil.mk_rels leftno i @ [Cic.Rel i])) - :: acc, i+1 - ) toapp ([],1) - in - List.fold_left ( - fun res t -> CicSubstitution.subst t res - ) (CicSubstitution.lift_from (List.length toapp + 1) 1 typ) l)) - in - let toapp = try List.tl (List.rev fields) with Failure _-> [] in - List.fold_right ( - fun (name, typ) (i, acc, toapp) -> - let start = - Cic.Lambda(Cic.Name "x", recty, - Cic.MutCase (uri,0,CicSubstitution.lift 1 (mk_oty toapp typ), - Cic.Rel 1, - [CicSubstitution.lift 1 - (mk_lambdas fields (Cic.Rel i))])) - in - i+1, ((qualify name, name, mk_lambdas params start) :: acc) , - if toapp <> [] then List.tl toapp else [] - ) - fields (1, [], toapp) - in - projections - - +let generate_one_proj uri params paramsno fields t i = + let mk_lambdas l start = + List.fold_right (fun (name,ty) acc -> + Cic.Lambda (Cic.Name name,ty,acc)) l start in + let recty = rec_ty uri paramsno in + let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in + Some + (mk_lambdas params + (Cic.Lambda (Cic.Name "w", recty, + Cic.MutCase (uri,0,outtype, Cic.Rel 1, + [mk_lambdas fields (Cic.Rel i)])))) - +let projections_of uri = + let buri = UriManager.buri_of_uri uri in + let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in + match obj with + Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) -> + assert (params = []); (* general case not implemented *) + let leftparams,ty = + let rec aux = + function + 0,ty -> [],ty + | n,Cic.Prod (Cic.Name name,s,t) -> + let leftparams,ty = aux (n - 1,t) in + (name,s)::leftparams,ty + | _,_ -> assert false + in + aux (paramsno,ty) + in + let fields = + let rec aux = + function + Cic.MutInd _ + | Cic.Appl _ -> [] + | Cic.Prod (Cic.Name name,s,t) -> (name,s)::aux t + | _ -> assert false + in + aux (CicSubstitution.lift 1 ty) + in + let rec aux i = + function + Cic.MutInd _ + | Cic.Appl _ -> [] + | Cic.Prod (Cic.Name name,s,t) -> + (match generate_one_proj uri leftparams paramsno fields s i with + Some p -> + let puri = + UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") + in + (puri,name,p) :: + aux (i - 1) + (CicSubstitution.subst + (Cic.Appl + (Cic.Const (puri,[]) :: + CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1]) + ) t) + | None -> assert false) + | _ -> assert false + in + aux (List.length fields) (CicSubstitution.lift 2 ty) + | _ -> assert false diff --git a/helm/ocaml/cic_proof_checking/cicRecord.mli b/helm/ocaml/cic_proof_checking/cicRecord.mli index 780d859a8..04ee188b5 100644 --- a/helm/ocaml/cic_proof_checking/cicRecord.mli +++ b/helm/ocaml/cic_proof_checking/cicRecord.mli @@ -23,19 +23,5 @@ * http://helm.cs.unibo.it/ *) -(** [suri] [params] [ty] [fields] *) -type record_spec = - string * (string * Cic.term) list * Cic.term * (string * Cic.term) list - -(** inductive_of_record [record_spec] returns - * types * leftno * obj * ugraph *) -val inductive_of_record: - record_spec -> - Cic.inductiveType list * int * Cic.obj * CicUniv.universe_graph - -(** projections_of [record_spec] returns suri * name * term *) -val projections_of: - record_spec -> - (string * string * Cic.term) list - - +(** projections_of [uri] returns uri * name * term *) +val projections_of: UriManager.uri -> (UriManager.uri * string * Cic.term) list diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 6789c4dff..1db82a99f 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -64,7 +64,9 @@ let debrujin_constructor uri number_of_types = List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta _ -> assert false + | C.Meta (i,l) -> + let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in + C.Meta (i,l) | C.Sort _ | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) @@ -2031,13 +2033,67 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res *) ;; -let typecheck uri ugraph = +let typecheck_obj0 ~logger uri ugraph = + let module C = Cic in + function + C.Constant (_,Some te,ty,_,_) -> + let _,ugraph = type_of ~logger ty ugraph in + let ty_te,ugraph = type_of ~logger te ugraph in + let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in + if not b then + raise (TypeCheckerFailure + ("the type of the body is not the one expected")) + else + ugraph + | C.Constant (_,None,ty,_,_) -> + (* only to check that ty is well-typed *) + let _,ugraph = type_of ~logger ty ugraph in + ugraph + | C.CurrentProof (_,conjs,te,ty,_,_) -> + let _,ugraph = + List.fold_left + (fun (metasenv,ugraph) ((_,context,ty) as conj) -> + let _,ugraph = + type_of_aux' ~logger metasenv context ty ugraph + in + metasenv @ [conj],ugraph + ) ([],ugraph) conjs + in + let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in + let type_of_te,ugraph = + type_of_aux' ~logger conjs [] te ugraph + in + let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in + if not b then + raise (TypeCheckerFailure (sprintf + "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s" + (CicPp.ppterm type_of_te) (CicPp.ppterm ty))) + else + ugraph + | C.Variable (_,bo,ty,_,_) -> + (* only to check that ty is well-typed *) + let _,ugraph = type_of ~logger ty ugraph in + (match bo with + None -> ugraph + | Some bo -> + let ty_bo,ugraph = type_of ~logger bo ugraph in + let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in + if not b then + raise (TypeCheckerFailure + ("the body is not the one expected")) + else + ugraph + ) + | (C.InductiveDefinition _ as obj) -> + check_mutual_inductive_defs ~logger uri obj ugraph + +let typecheck uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in let logger = new CicLogger.logger in (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *) - match CicEnvironment.is_type_checked ~trust:false ugraph uri with + match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) cobj,ugraph' @@ -2045,60 +2101,7 @@ let typecheck uri ugraph = (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *) - let ugraph1 = - (match uobj with - C.Constant (_,Some te,ty,_,_) -> - let _,ugraph1 = type_of ~logger ty ugraph in - let ty_te,ugraph2 = type_of ~logger te ugraph1 in - let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in - if not b then - raise (TypeCheckerFailure - ("Unknown constant:" ^ U.string_of_uri uri)) - else - ugraph3 - | C.Constant (_,None,ty,_,_) -> - (* only to check that ty is well-typed *) - let _,ugraph1 = type_of ~logger ty ugraph in - ugraph1 - | C.CurrentProof (_,conjs,te,ty,_,_) -> - let _,ugraph1 = - List.fold_left - (fun (metasenv,ugraph) ((_,context,ty) as conj) -> - let _,ugraph1 = - type_of_aux' ~logger metasenv context ty ugraph - in - metasenv @ [conj],ugraph1 - ) ([],ugraph) conjs - in - let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in - let type_of_te,ugraph3 = - type_of_aux' ~logger conjs [] te ugraph2 - in - let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in - if not b then - raise (TypeCheckerFailure (sprintf - "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s" - (U.string_of_uri uri) (CicPp.ppterm type_of_te) - (CicPp.ppterm ty))) - else - ugraph4 - | C.Variable (_,bo,ty,_,_) -> - (* only to check that ty is well-typed *) - let _,ugraph1 = type_of ~logger ty ugraph in - (match bo with - None -> ugraph1 - | Some bo -> - let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in - let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in - if not b then - raise (TypeCheckerFailure - ("Unknown variable:" ^ U.string_of_uri uri)) - else - ugraph3 - ) - | C.InductiveDefinition _ -> - check_mutual_inductive_defs ~logger uri uobj ugraph - ) in + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in try CicEnvironment.set_type_checking_info uri; logger#log (`Type_checking_completed uri); @@ -2114,16 +2117,20 @@ let typecheck uri ugraph = *) Invalid_argument s -> (*debug_print s;*) - uobj,ugraph1 + uobj,ugraph ;; +let typecheck_obj ~logger uri obj = + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_obj uri (obj,ugraph) + (** wrappers which instantiate fresh loggers *) let type_of_aux' ?(subst = []) metasenv context t ugraph = let logger = new CicLogger.logger in type_of_aux' ~logger ~subst metasenv context t ugraph -let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) = - let logger = new CicLogger.logger in - typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno) - +let typecheck_obj uri obj = + let logger = new CicLogger.logger in + typecheck_obj ~logger uri obj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index ce94601f2..5cbda28d6 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -27,8 +27,9 @@ exception TypeCheckerFailure of string exception AssertFailure of string -val typecheck : - UriManager.uri -> CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph +val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term + +val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph (* FUNCTIONS USED ONLY IN THE TOPLEVEL *) @@ -38,8 +39,5 @@ val type_of_aux': Cic.term -> CicUniv.universe_graph -> Cic.term * CicUniv.universe_graph - -(* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *) -val typecheck_mutual_inductive_defs : - UriManager.uri -> Cic.inductiveType list * UriManager.uri list * int -> - CicUniv.universe_graph -> CicUniv.universe_graph +(* typechecks the obj and puts it in the environment *) +val typecheck_obj : UriManager.uri -> Cic.obj -> unit diff --git a/helm/ocaml/cic_proof_checking/utilities/create_environment.ml b/helm/ocaml/cic_proof_checking/utilities/create_environment.ml index dab8b8452..8a8524d24 100644 --- a/helm/ocaml/cic_proof_checking/utilities/create_environment.ml +++ b/helm/ocaml/cic_proof_checking/utilities/create_environment.ml @@ -63,7 +63,7 @@ let _ = print_endline uri; flush stdout; let uri = UriManager.uri_of_string uri in - ignore (CicTypeChecker.typecheck uri CicUniv.empty_ugraph) + ignore (CicTypeChecker.typecheck uri) (* with Sys.Break -> () *) done with End_of_file | Sys.Break -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 9023b4869..fab264d07 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -116,25 +116,30 @@ type alias_spec = | Symbol_alias of string * int * string (* name, instance no, description *) | Number_alias of int * string (* instance no, description *) -type 'term command = - | Set of loc * string * string - | Qed of loc - (** name. - * Name is needed when theorem was started without providing a name - *) - | Inductive of loc * (string * 'term) list * 'term inductive_type list +type obj = + | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of loc * thm_flavour * string option * 'term * 'term option + | Theorem of thm_flavour * string * CicAst.term * CicAst.term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) + | Record of + (string * CicAst.term) list * string * CicAst.term * + (string * CicAst.term) list + +type ('term,'obj) command = + | Set of loc * string * string + | Qed of loc + (** name. + * Name is needed when theorem was started without providing a name + *) | Coercion of loc * 'term | Alias of loc * alias_spec (** parameters, name, type, fields *) - | Record of loc * (string * 'term) list * string * 'term * (string * 'term) list + | Obj of loc * 'obj type ('term, 'ident) tactical = | Tactic of loc * ('term, 'ident) tactic @@ -149,19 +154,19 @@ type ('term, 'ident) tactical = | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) -type ('term, 'ident) code = - | Command of loc * 'term command +type ('term, 'obj, 'ident) code = + | Command of loc * ('term,'obj) command | Macro of loc * 'term macro (* Macro are substantially queries, but since we are not the kind of * peolpe that like to push "start" to turn off the computer * we added this command *) | Tactical of loc * ('term, 'ident) tactical -type ('term, 'ident) comment = +type ('term, 'obj, 'ident) comment = | Note of loc * string - | Code of loc * ('term, 'ident) code + | Code of loc * ('term, 'obj, 'ident) code -type ('term, 'ident) statement = - | Executable of loc * ('term, 'ident) code - | Comment of loc * ('term, 'ident) comment +type ('term, 'obj, 'ident) statement = + | Executable of loc * ('term, 'obj, 'ident) code + | Comment of loc * ('term, 'obj, 'ident) comment diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index a5c0478ac..b9babaa65 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -163,42 +163,45 @@ let pp_fields fields = String.concat ";\n" (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields) +let pp_obj = function + | Inductive (params, types) -> + let pp_constructors constructors = + String.concat "\n" + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) + constructors) + in + let pp_type (name, _, typ, constructors) = + sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) + (pp_constructors constructors) + in + (match types with + | [] -> assert false + | (name, inductive, typ, constructors) :: tl -> + let fst_typ_pp = + sprintf "%sinductive %s%s: %s \\def\n%s" + (if inductive then "" else "co") name (pp_params params) + (pp_term_ast typ) (pp_constructors constructors) + in + fst_typ_pp ^ String.concat "" (List.map pp_type tl)) + | Theorem (flavour, name, typ, body) -> + sprintf "%s %s: %s %s" + (pp_flavour flavour) + name + (pp_term_ast typ) + (match body with + | None -> "" + | Some body -> "\\def " ^ pp_term_ast body) + | Record (params,name,ty,fields) -> + "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ + pp_fields fields ^ "}" + + let pp_command = function | Qed _ -> "qed" | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value - | Inductive (_, params, types) -> - let pp_constructors constructors = - String.concat "\n" - (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ)) - constructors) - in - let pp_type (name, _, typ, constructors) = - sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ) - (pp_constructors constructors) - in - (match types with - | [] -> assert false - | (name, inductive, typ, constructors) :: tl -> - let fst_typ_pp = - sprintf "%sinductive %s%s: %s \\def\n%s" - (if inductive then "" else "co") name (pp_params params) - (pp_term_ast typ) (pp_constructors constructors) - in - fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Theorem (_, flavour, name, typ, body) -> - sprintf "%s %s: %s %s" - (pp_flavour flavour) - (match name with None -> "" | Some name -> name) - (pp_term_ast typ) - (match body with - | None -> "" - | Some body -> "\\def " ^ pp_term_ast body) | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!" | Alias (_,s) -> pp_alias s - | Record (_,params,name,ty,fields) -> - "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^ - pp_fields fields ^ "}" - + | Obj (_,obj) -> pp_obj obj let rec pp_tactical = function | Tactic (_, tac) -> pp_tactic tac diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli index 3308adf92..d4cae4405 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.mli +++ b/helm/ocaml/cic_transformations/tacticAstPp.mli @@ -24,11 +24,12 @@ *) val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string -val pp_command: CicAst.term TacticAst.command -> string +val pp_obj: TacticAst.obj -> string +val pp_command: (CicAst.term,TacticAst.obj) TacticAst.command -> string val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string -val pp_comment: (CicAst.term,string) TacticAst.comment -> string -val pp_executable: (CicAst.term,string) TacticAst.code -> string -val pp_statement: (CicAst.term,string) TacticAst.statement -> string +val pp_comment: (CicAst.term,TacticAst.obj,string) TacticAst.comment -> string +val pp_executable: (CicAst.term,TacticAst.obj,string) TacticAst.code -> string +val pp_statement: (CicAst.term,TacticAst.obj,string) TacticAst.statement -> string val pp_macro_ast: CicAst.term TacticAst.macro -> string val pp_macro_cic: Cic.term TacticAst.macro -> string val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml index 851355e95..a2d0a73d5 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.ml +++ b/helm/ocaml/cic_unification/cicMkImplicit.ml @@ -278,3 +278,36 @@ let expand_implicits metasenv subst context term = in aux metasenv context term +let expand_implicits_in_obj metasenv subst = + function + Cic.Constant (name,bo,ty,params,attrs) -> + let metasenv,bo' = + match bo with + None -> metasenv,None + | Some bo -> + let metasenv,bo' = expand_implicits metasenv subst [] bo in + metasenv,Some bo' in + let metasenv,ty' = expand_implicits metasenv subst [] ty in + metasenv,Cic.Constant (name,bo',ty',params,attrs) + | Cic.CurrentProof (name,metasenv',bo,ty,params,attrs) -> + assert (metasenv' = []); + let metasenv,bo' = expand_implicits metasenv subst [] bo in + let metasenv,ty' = expand_implicits metasenv subst [] ty in + metasenv,Cic.CurrentProof (name,metasenv,bo',ty',params,attrs) + | Cic.InductiveDefinition (tyl,params,paramsno,attrs) -> + let metasenv,tyl = + List.fold_right + (fun (name,b,ty,cl) (metasenv,res) -> + let metasenv,ty' = expand_implicits metasenv subst [] ty in + let metasenv,cl' = + List.fold_right + (fun (name,ty) (metasenv,res) -> + let metasenv,ty' = expand_implicits metasenv subst [] ty in + metasenv,(name,ty')::res + ) cl (metasenv,[]) + in + metasenv,(name,b,ty',cl')::res + ) tyl (metasenv,[]) + in + metasenv,Cic.InductiveDefinition (tyl,params,paramsno,attrs) + | Cic.Variable _ -> assert false (* Not implemented *) diff --git a/helm/ocaml/cic_unification/cicMkImplicit.mli b/helm/ocaml/cic_unification/cicMkImplicit.mli index 7821bef40..4f6fcee2e 100644 --- a/helm/ocaml/cic_unification/cicMkImplicit.mli +++ b/helm/ocaml/cic_unification/cicMkImplicit.mli @@ -62,3 +62,5 @@ val expand_implicits: Cic.metasenv -> Cic.substitution -> Cic.context -> Cic.term -> Cic.metasenv * Cic.term +val expand_implicits_in_obj: + Cic.metasenv -> Cic.substitution -> Cic.obj -> Cic.metasenv * Cic.obj diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 76642ee3d..42069ff5c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -964,7 +964,91 @@ let type_of_aux' metasenv context term ugraph = type_of_aux' metasenv context term ugraph with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg) + +(*CSC: this is a very very rough approximation; to be finished *) +let are_all_occurrences_positive uri = + let rec aux = + (*CSC: here we should do a whd; but can we do that? *) + function + Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> () + | Cic.MutInd (uri',_,_) when uri = uri' -> () + | Cic.Prod (_,_,t) -> aux t + | _ -> raise (RefineFailure "not well formed constructor type") + in + aux +let typecheck metasenv uri obj = + let ugraph = CicUniv.empty_ugraph in + match obj with + Cic.Constant (name,Some bo,ty,args,attrs) -> + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph + | Cic.Constant (name,None,ty,args,attrs) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> + assert (metasenv' = metasenv); + (* Here we do not check the metasenv for correctness *) + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph + | Cic.Variable _ -> assert false (* not implemented *) + | Cic.InductiveDefinition (tys,args,paramsno,attrs) -> + (*CSC: this code is greately simplified and many many checks are missing *) + (*CSC: e.g. the constructors are not required to build their own types, *) + (*CSC: the arities are not required to have as type a sort, etc. *) + let uri = match uri with Some uri -> uri | None -> assert false in + let typesno = List.length tys in + (* first phase: we fix only the types *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + metasenv,ugraph,(name,b,ty',cl)::res + ) tys (metasenv,ugraph,[]) in + let con_context = + List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in + (* second phase: we fix only the constructors *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let metasenv,ugraph,cl' = + List.fold_right + (fun (name,ty) (metasenv,ugraph,res) -> + let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty',_,metasenv,ugraph = + type_of_aux' metasenv con_context ty ugraph in + let undebrujin t = + snd + (List.fold_right + (fun (name,_,_,_) (i,t) -> + (* here the explicit_named_substituion is assumed to be *) + (* of length 0 *) + let t' = Cic.MutInd (uri,i,[]) in + let t = CicSubstitution.subst t' t in + i - 1,t + ) tys (typesno - 1,t)) in + let ty' = undebrujin ty in + metasenv,ugraph,(name,ty')::res + ) cl (metasenv,ugraph,[]) + in + metasenv,ugraph,(name,b,ty,cl')::res + ) tys (metasenv,ugraph,[]) in + (* third phase: we check the positivity condition *) + List.iter + (fun (_,_,_,cl) -> + List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl + ) tys ; + Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph (* DEBUGGING ONLY let type_of_aux' metasenv context term = diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 4289905c8..2e132c043 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -27,9 +27,17 @@ exception RefineFailure of string;; exception Uncertain of string;; exception AssertFailure of string;; -(* type_of_aux' metasenv context term *) -(* refines [term] and returns the refined form of [term], *) -(* its type the new metasenv. *) +(* type_of_aux' metasenv context term graph *) +(* refines [term] and returns the refined form of [term], *) +(* its type, the new metasenv and universe graph. *) val type_of_aux': Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph -> Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph + +(* typecheck metasenv uri obj graph *) +(* refines [obj] and returns the refined form of [obj], *) +(* the new metasenv and universe graph. *) +(* the [uri] is required only for inductive definitions *) +val typecheck : + Cic.metasenv -> UriManager.uri option -> Cic.obj -> + Cic.obj * Cic.metasenv * CicUniv.universe_graph