--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matita">
+ <key name="auto_disambiguation">true</key>
+ <key name="environment_trust">true</key>
+ <key name="baseuri">cic:/matita/</key>
+ <key name="basedir">.matita/xml</key>
+ <key name="owner">sacerdot</key>
+<!-- <key name="script_font">Monospace 10</key> -->
+ </section>
+ <section name="db">
+ <!-- <key name="host">localhost</key> -->
+ <key name="host">mowgli.cs.unibo.it</key>
+ <key name="user">helm</key>
+ <key name="database">matita</key>
+ </section>
+ <section name="getter">
+ <key name="prefetch">true</key>
+ <key name="servers">
+ file:///projects/helm/library/coq_contribs
+ </key>
+ <key name="cache_dir">.matita/getter/cache</key>
+ <key name="maps_dir">.matita/getter/maps</key>
+ <key name="dtd_dir">/projects/helm/xml/dtd</key>
+<!-- <key name="loglevel">180</key> -->
+ </section>
+</helm_registry>
(**********************************************************************)
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
let disambiguate_term = Disambiguator.disambiguate_term
+let disambiguate_obj = Disambiguator.disambiguate_obj
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
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
{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
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
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 =
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
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
) (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 *)
) [] ["_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
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
* 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 ->
val add_record_def:
CicRecord.record_spec ->
MatitaTypes.status -> MatitaTypes.status
+*)
val time_travel:
present:MatitaTypes.status -> past:MatitaTypes.status -> unit
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||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 *)
(* *)
(**************************************************************************)
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
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
intro.
intro.
intro.intro.
-STOP normalize goal at (? ? % ?).
-
-
+normalize goal at (? ? % ?).
+*)
\ No newline at end of file
(** 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" *)
[ 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<def>> (* ≝ *); 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<def>> (* ≝ *); 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 =
| _ -> 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 ->
| [ 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: [
(** {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} *)
exception No_choices of domain_item
exception NoWellTypedInterpretation
+exception PathNotWellFormed
(** raised when an environment is not enough informative to decide *)
exception Try_again
| 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));
(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
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
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
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
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 =
| 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 =
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) =
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 *)
(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
(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
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
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"
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 ->
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
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 =
* 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
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
?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
-
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:
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
| _ -> 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))
* @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
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
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 ||
(* 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
(* 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
* 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
* 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
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)
*)
;;
-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'
(* 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);
*)
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
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 *)
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
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 ->
| 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
| 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
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
*)
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
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 *)
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
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 =
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
projects / helm.git / commitdiff