(* Copyright (C) 2003, HELM Team.
+ *
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
in
C.CoFix (i, fl')
in
- LibrarySync.merge_coercions (um_aux term)
+ um_aux term
;;
let apply_subst =
Cic.CicHash.find localization_tbl t
with Not_found ->
prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
- assert false
+ raise exn'
in
raise (HExtlib.Localized (loc,exn'))
let exp_impl metasenv subst context =
function
| Some `Type ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+ let (metasenv', idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
| Some `Closed ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
+ metasenv', Cic.Meta (idx, [])
| None ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
+ let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ metasenv', Cic.Meta (idx, irl)
| _ -> assert false
;;
+let is_a_double_coercion t =
+ let last_of l =
+ let rec aux = function
+ | x::[] -> x
+ | x::tl -> aux tl
+ | [] -> assert false
+ in
+ aux l
+ in
+ let dummyres =
+ false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
+ in
+ match t with
+ | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 ->
+ (match last_of tl with
+ | Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ let head = last_of tl2 in
+ true, c1, c2, head
+ | _ -> dummyres)
+ | _ -> dummyres
+
+let avoid_double_coercion context subst metasenv ugraph t ty =
+ let arity_of con =
+ try
+ let ty,_=CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
+ let rec count_pi = function
+ | Cic.Prod (_,_,t) -> 1 + count_pi t
+ | _ -> 0
+ in
+ count_pi ty
+ with Invalid_argument _ -> assert false (* all coercions have an uri *)
+ in
+ let rec mk_implicits tail = function
+ | 0 -> [tail]
+ | n -> Cic.Implicit None :: mk_implicits tail (n-1)
+ in
+ let b, c1, c2, head = is_a_double_coercion t in
+ if b then
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CicMetaSubst.apply_subst subst ty in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c ->
+ let arity = arity_of c in
+ let args = mk_implicits head (arity - 1) in
+ let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in
+ let newt = Cic.Appl (c_bo::args) in
+ let subst, metasenv, ugraph =
+ CicUnification.fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print
+ (lazy
+ ("packing: " ^
+ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args))));
+ Cic.Appl (c::args), ty, subst, metasenv, ugraph
+ | _ -> assert false) (* the composite coercion must exist *)
+ else
+ t, ty, subst, metasenv, ugraph
let rec type_of_constant uri ugraph =
let module C = Cic in
| C.CurrentProof (_,_,_,ty,_,_) -> ty,u
| _ ->
raise
- (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
+ (RefineFailure
+ (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
and type_of_variable uri ugraph =
let module C = Cic in
subst coercion_src context ^ " that is not a sort")))
| CoercGraph.SomeCoercion c ->
let newt, tty, subst, metasenv, ugraph =
- avoid_double_coercion
+ avoid_double_coercion context
subst metasenv ugraph
(Cic.Appl[c;t]) coercion_tgt
in
match boh with
| CoercGraph.SomeCoercion c ->
let newt, tty, subst', metasenv', ugraph1 =
- avoid_double_coercion
+ avoid_double_coercion context
subst' metasenv' ugraph1
(Cic.Appl[c;s']) coercion_tgt
in
eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
in
- avoid_double_coercion
+ avoid_double_coercion context
subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
relocalize localization_tbl t t';
res
- and avoid_double_coercion subst metasenv ugraph t ty =
- match t with
- | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
- | _ -> assert false) (* the composite coercion must exist *)
- | _ -> t, ty, subst, metasenv, ugraph
-
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
try
fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ debug_print
+ (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
(CicPp.ppterm hetype')
(CicMetaSubst.ppmetasenv [] metasenv)
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion c ->
let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion
+ avoid_double_coercion context
subst metasenv ugraph
(Cic.Appl[c;hete]) tgt_carr in
try
are_all_occurrences_positive metasenv ugraph uri tys paramsno
in
Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
+;;
+
+(* sara' piu' veloce che raffinare da zero? mah.... *)
+let pack_coercion metasenv t =
+ let module C = Cic in
+ let rec merge_coercions ctx =
+ let aux = (fun (u,t) -> u,merge_coercions ctx t) in
+ function
+ | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
+ | C.Meta (n,subst) ->
+ let subst' =
+ List.map
+ (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
+ in
+ C.Meta (n,subst')
+ | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
+ | C.Prod (name,so,dest) ->
+ let ctx' = (Some (name,C.Decl so))::ctx in
+ C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.Lambda (name,so,dest) ->
+ let ctx' = (Some (name,C.Decl so))::ctx in
+ C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,dest) ->
+ let ctx' = Some (name,(C.Def (so,None)))::ctx in
+ C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.Appl l as t ->
+ let b,_,_,_ = is_a_double_coercion t in
+ (* prerr_endline "CANDIDATO!!!!"; *)
+ let newt =
+ if b then
+ let ugraph = CicUniv.empty_ugraph in
+ let old_insert_coercions = !insert_coercions in
+ insert_coercions := false;
+ let newt, _, menv, _ =
+ try
+ type_of_aux' metasenv ctx t ugraph
+ with RefineFailure _ | Uncertain _ ->
+ prerr_endline (CicPp.ppterm t);
+ t, t, [], ugraph
+ in
+ insert_coercions := old_insert_coercions;
+ if metasenv <> [] || menv = [] then
+ newt
+ else
+ (prerr_endline "PUO' SUCCEDERE!!!!!";t)
+ else
+ t
+ in
+ (match newt with
+ | C.Appl l -> C.Appl (List.map (merge_coercions ctx) l)
+ | _ -> assert false)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Var (uri, exp_named_subst)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.Const (uri, exp_named_subst)
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutInd (uri,tyno,exp_named_subst)
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst = List.map aux exp_named_subst in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst)
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ let pl = List.map (merge_coercions ctx) pl in
+ C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
+ | C.Fix (fno, fl) ->
+ let ctx =
+ List.fold_left
+ (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,idx,ty,bo) ->
+ (name,idx,merge_coercions ctx ty,merge_coercions ctx bo))
+ fl
+ in
+ C.Fix (fno, fl)
+ | C.CoFix (fno, fl) ->
+ let ctx =
+ List.fold_left
+ (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
+ ctx fl
+ in
+ let fl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, merge_coercions ctx ty, merge_coercions ctx bo))
+ fl
+ in
+ C.CoFix (fno, fl)
+ in
+ merge_coercions [] t
+;;
+
+let pack_coercion_obj obj =
+ let module C = Cic in
+ match obj with
+ | C.Constant (id, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] body)
+ in
+ let ty = pack_coercion [] ty in
+ C.Constant (id, body, ty, params, attrs)
+ | C.Variable (name, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (pack_coercion [] body)
+ in
+ let ty = pack_coercion [] ty in
+ C.Variable (name, body, ty, params, attrs)
+ | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
+ let conjectures =
+ List.map
+ (fun (i, ctx, ty) ->
+ let ctx =
+ List.map
+ (function
+ | Some (name, C.Decl t) ->
+ Some (name, C.Decl (pack_coercion conjectures t))
+ | Some (name, C.Def (t,None)) ->
+ Some (name, C.Def (pack_coercion conjectures t, None))
+ | Some (name, C.Def (t,Some ty)) ->
+ Some (name, C.Def (pack_coercion conjectures t,
+ Some (pack_coercion conjectures ty)))
+ | None -> None)
+ ctx
+ in
+ ((i,ctx,pack_coercion conjectures ty)))
+ conjectures
+ in
+ let body = pack_coercion conjectures body in
+ let ty = pack_coercion conjectures ty in
+ C.CurrentProof (name, conjectures, body, ty, params, attrs)
+ | C.InductiveDefinition (indtys, params, leftno, attrs) ->
+ let indtys =
+ List.map
+ (fun (name, ind, arity, cl) ->
+ let arity = pack_coercion [] arity in
+ let cl =
+ List.map (fun (name, ty) -> (name,pack_coercion [] ty)) cl
+ in
+ (name, ind, arity, cl))
+ indtys
+ in
+ C.InductiveDefinition (indtys, params, leftno, attrs)
+;;
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
val insert_coercions: bool ref (* initially true *)
+(* given a closed term returns it with all coercions packed *)
+val pack_coercion_obj: Cic.obj -> Cic.obj
+
let coercion_moo_statement_of uri =
GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let refinement_toolkit = {
+ RefinementTool.type_of_aux' =
+ (fun ?localization_tbl e c t u ->
+ let saved = !CicRefine.insert_coercions in
+ CicRefine.insert_coercions:= false;
+ let rc =
+ try
+ let t, ty, metasenv, ugraph =
+ CicRefine.type_of_aux' ?localization_tbl e c t u in
+ RefinementTool.Success (t, ty, metasenv, ugraph)
+ with
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s -> RefinementTool.Exception s
+ in
+ CicRefine.insert_coercions := saved;
+ rc);
+ RefinementTool.ppsubst = CicMetaSubst.ppsubst;
+ RefinementTool.apply_subst = CicMetaSubst.apply_subst;
+ RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
+ RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
+ }
+
let eval_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
let status,compounds =
prerr_endline "evaluating a coercion command";
- GrafiteSync.add_coercion ~basedir ~add_composites status uri in
+ GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
let moo_content = coercion_moo_statement_of uri in
let status = GrafiteTypes.add_moo_content [moo_content] status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
| _ -> None)
fields
in
+ (*
prerr_endline "wanted coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- wanted_coercions;
+ wanted_coercions; *)
let coercions, moo_content =
List.split
(HExtlib.filter_map
None)
lemmas)
in
- prerr_endline "actual coercions:";
+ (* prerr_endline "actual coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions;
+ coercions; *)
let status = GrafiteTypes.add_moo_content moo_content status in
{status with
GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},
let add_obj uri obj status =
let basedir = Helm_registry.get "matita.basedir" in
- let status,lemmas = GrafiteSync.add_obj ~basedir uri obj status in
+ let status,lemmas = GrafiteSync.add_obj ~basedir refinement_toolkit uri obj status in
status, lemmas
let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
open Printf
-let add_obj ~basedir uri obj status =
- let lemmas = LibrarySync.add_obj uri obj basedir in
+let add_obj refinement_toolkit ~basedir uri obj status =
+ let lemmas = LibrarySync.add_obj refinement_toolkit uri obj basedir in
{status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
lemmas
-let add_coercion ~basedir ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
+let add_coercion refinement_toolkit ~basedir ~add_composites status uri =
+ let compounds = LibrarySync.add_coercion ~add_composites ~basedir refinement_toolkit uri in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds
*)
val add_obj:
+ RefinementTool.kit ->
basedir:string -> UriManager.uri -> Cic.obj -> GrafiteTypes.status ->
GrafiteTypes.status * UriManager.uri list
val add_coercion:
- basedir:string -> add_composites:bool -> GrafiteTypes.status ->
- UriManager.uri -> GrafiteTypes.status * UriManager.uri list
+ RefinementTool.kit ->
+ basedir:string -> add_composites:bool -> GrafiteTypes.status ->
+ UriManager.uri ->
+ GrafiteTypes.status * UriManager.uri list
val time_travel:
present:GrafiteTypes.status -> past:GrafiteTypes.status -> unit
-cicCoercion.cmi: coercDb.cmi
+cicCoercion.cmi: refinementTool.cmo coercDb.cmi
+librarySync.cmi: refinementTool.cmo
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
cicRecord.cmo: cicRecord.cmi
libraryDb.cmx: libraryDb.cmi
coercDb.cmo: coercDb.cmi
coercDb.cmx: coercDb.cmi
-cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
-cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
+cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi
coercGraph.cmo: coercDb.cmi coercGraph.cmi
coercGraph.cmx: coercDb.cmx coercGraph.cmi
librarySync.cmo: libraryDb.cmi coercGraph.cmi coercDb.cmi cicRecord.cmi \
libraryClean.mli \
$(NULL)
IMPLEMENTATION_FILES = \
+ refinementTool.ml \
$(INTERFACE_FILES:%.mli=%.ml)
include ../../Makefile.defs
let obj_attrs = [`Class `Coercion; `Generated]
+exception UnableToCompose
+
(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure c1 c2 univ =
+let generate_composite_closure rt c1 c2 univ =
+ let module RT = RefinementTool in
let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
- let rec mk_rels n =
+ let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
+ let rec mk_implicits n =
match n with
| 0 -> []
- | _ -> (Cic.Rel n) :: (mk_rels (n-1))
+ | _ -> (Cic.Implicit None) :: mk_implicits (n-1)
in
- let rec compose k =
- function
- | Cic.Prod (name,src,tgt) ->
- let name =
- match name with
- | Cic.Anonymous -> Cic.Name "x"
- | _ -> name
- in
- Cic.Lambda (name,src,compose (k+1) tgt)
- | Cic.Appl (he::tl) ->
- Cic.Appl (c2 :: tl @ [Cic.Appl (c1 :: (mk_rels k)) ])
- | _ -> Cic.Appl (c2 :: [Cic.Appl (c1 :: (mk_rels k)) ])
+ let rec mk_lambda_spline c = function
+ | 0 -> c
+ | n ->
+ Cic.Lambda
+ (Cic.Name ("A" ^ string_of_int (n-1)),
+ (Cic.Implicit None),
+ mk_lambda_spline c (n-1))
+ in
+ let rec count_saturations_needed n = function
+ | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t
+ | _ -> n
+ in
+ let compose c1 nc1 c2 nc2 =
+ Cic.Lambda
+ (Cic.Name "x",
+ (Cic.Implicit None),
+ Cic.Appl ( c2 :: mk_implicits nc2 @
+ [ Cic.Appl ( c1 :: mk_implicits nc1 @ [Cic.Rel 1]) ]))
+ in
+ let order_metasenv metasenv =
+ List.sort
+ (fun (_,ctx1,_) (_,ctx2,_) -> List.length ctx1 - List.length ctx2)
+ metasenv
+ in
+ let rec create_subst_from_metas_to_rels n = function
+ | [] -> []
+ | (metano, ctx, ty)::tl ->
+ (metano,(ctx,Cic.Rel (n+1),ty)) ::
+ create_subst_from_metas_to_rels (n-1) tl
+ in
+ let split_metasenv metasenv n =
+ List.partition (fun (_,ctx,_) -> List.length ctx > n) metasenv
+ in
+ let purge_unused_lambdas metasenv t =
+ let rec aux = function
+ | Cic.Lambda (_, Cic.Meta (i,_), t) when
+ List.exists (fun (j,_,_) -> j = i) metasenv ->
+ CicSubstitution.subst (Cic.Rel ~-100) t
+ | Cic.Lambda (name, s, t) ->
+ Cic.Lambda (name, s, aux t)
+ | t -> t
+ in
+ aux t
in
- let c = compose 0 c1_ty in
+ debug_print (lazy ("\nCOMPOSING"));
+ debug_print (lazy (" c1= "^CicPp.ppterm c1 ^" : "^ CicPp.ppterm c1_ty));
+ debug_print (lazy (" c2= "^CicPp.ppterm c2 ^" : "^ CicPp.ppterm c2_ty));
+ let saturations_for_c1 = count_saturations_needed 0 c1_ty in
+ let saturations_for_c2 = count_saturations_needed 0 c2_ty in
+ let c = compose c1 saturations_for_c1 c2 saturations_for_c2 in
+ let spline_len = saturations_for_c1 + saturations_for_c2 in
+ let c = mk_lambda_spline c spline_len in
+ (* debug_print (lazy ("COMPOSTA: " ^ CicPp.ppterm c)); *)
+ let c, univ =
+ match rt.RT.type_of_aux' [] [] c univ with
+ | RT.Success (term, ty, metasenv, ugraph) ->
+ debug_print(lazy("COMPOSED REFINED: "^CicPp.ppterm term));
+ let metasenv = order_metasenv metasenv in
+ debug_print(lazy("ORDERED MENV: "^rt.RT.ppmetasenv [] metasenv));
+ let body_metasenv, lambdas_metasenv =
+ split_metasenv metasenv spline_len
+ in
+ debug_print(lazy("B_MENV: "^rt.RT.ppmetasenv [] body_metasenv));
+ debug_print(lazy("L_MENV: "^rt.RT.ppmetasenv [] lambdas_metasenv));
+ let subst = create_subst_from_metas_to_rels spline_len body_metasenv in
+ debug_print (lazy("SUBST: "^rt.RT.ppsubst subst));
+ let term = rt.RT.apply_subst subst term in
+ debug_print (lazy ("COMPOSED SUBSTITUTED: " ^ CicPp.ppterm term));
+ (match rt.RT.type_of_aux' metasenv [] term ugraph with
+ | RT.Success (term, ty, metasenv, ugraph) ->
+ let body_metasenv, lambdas_metasenv =
+ split_metasenv metasenv spline_len
+ in
+ let term = purge_unused_lambdas lambdas_metasenv term in
+ debug_print (lazy ("COMPOSED: " ^ CicPp.ppterm term));
+ term, ugraph
+ | RT.Exception s -> debug_print s; raise UnableToCompose)
+ | RT.Exception s -> debug_print s; raise UnableToCompose
+ in
let c_ty,univ =
try
CicTypeChecker.type_of_aux' [] [] c univ
- with CicTypeChecker.TypeCheckerFailure s as exn ->
+ with CicTypeChecker.TypeCheckerFailure s ->
debug_print (lazy (Printf.sprintf "Generated composite coercion:\n%s\n%s"
(CicPp.ppterm c) (Lazy.force s)));
- raise exn
+ raise UnableToCompose
in
let cleaned_ty =
FreshNamesGenerator.clean_dummy_dependent_types c_ty
(* given a new coercion uri from src to tgt returns
* a list of (new coercion uri, coercion obj, universe graph)
*)
-let close_coercion_graph src tgt uri =
+let close_coercion_graph rt src tgt uri =
(* check if the coercion already exists *)
let coercions = CoercDb.to_list () in
let todo_list = get_closure_coercions src tgt uri coercions in
let todo_list = filter_duplicates todo_list coercions in
let new_coercions =
- List.map (
+ HExtlib.filter_map (
fun (src, l , tgt) ->
- match l with
- | [] -> assert false
- | he :: tl ->
- let first_step =
- Cic.Constant ("",
- Some (CoercDb.term_of_carr (CoercDb.Uri he)),
- Cic.Sort Cic.Prop, [], obj_attrs)
- in
- let o,_ =
- List.fold_left (fun (o,univ) coer ->
- match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (CoercDb.term_of_carr (CoercDb.Uri
- coer)) univ
+ try
+ (match l with
+ | [] -> assert false
+ | he :: tl ->
+ let first_step =
+ Cic.Constant ("",
+ Some (CoercDb.term_of_carr (CoercDb.Uri he)),
+ Cic.Sort Cic.Prop, [], obj_attrs)
+ in
+ let o,_ =
+ List.fold_left (fun (o,univ) coer ->
+ match o with
+ | Cic.Constant (_,Some c,_,[],_) ->
+ generate_composite_closure rt c
+ (CoercDb.term_of_carr (CoercDb.Uri coer)) univ
+ | _ -> assert false
+ ) (first_step, CicUniv.empty_ugraph) tl
+ in
+ let name_src = CoercDb.name_of_carr src in
+ let name_tgt = CoercDb.name_of_carr tgt in
+ let name = name_tgt ^ "_of_" ^ name_src in
+ let buri = UriManager.buri_of_uri uri in
+ let c_uri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+ in
+ let named_obj =
+ match o with
+ | Cic.Constant (_,bo,ty,vl,attrs) ->
+ Cic.Constant (name,bo,ty,vl,attrs)
| _ -> assert false
- ) (first_step, CicUniv.empty_ugraph) tl
- in
- let name_src = CoercDb.name_of_carr src in
- let name_tgt = CoercDb.name_of_carr tgt in
- let name = name_tgt ^ "_of_" ^ name_src in
- let buri = UriManager.buri_of_uri uri in
- let c_uri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- let named_obj =
- match o with
- | Cic.Constant (_,bo,ty,vl,attrs) ->
- Cic.Constant (name,bo,ty,vl,attrs)
- | _ -> assert false
- in
- ((src,tgt,c_uri,named_obj))
+ in
+ Some ((src,tgt,c_uri,named_obj)))
+ with UnableToCompose -> None
) todo_list
in
new_coercions
(* This module implements the Coercions transitive closure *)
val close_coercion_graph:
+ RefinementTool.kit ->
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
| t -> Term t
;;
-let name_of_carr = function
+let rec name_of_carr = function
| Uri u -> UriManager.name_of_uri u
| Sort s -> CicPp.ppsort s
| Term (Cic.Appl ((Cic.Const (uri, _))::_))
| Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_))
| Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) ->
UriManager.name_of_uri uri
- | Term t -> (* CicPp.ppterm t *) assert false
+ | Term (Cic.Prod (_,_,t)) -> name_of_carr (Term t)
+ | Term t ->
+ prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t);
+ "FixTheNameMangler"
let eq_carr src tgt =
match src, tgt with
(** XXX WARNING: non-reentrant *)
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+type coerc_carr =
+ | Uri of UriManager.uri (* const, mutind, mutconstr *)
+ | Sort of Cic.sort (* Prop, Set, Type *)
+ | Term of Cic.term (* nothing supported *)
+
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed
val eq_carr: coerc_carr -> coerc_carr -> bool
val get_carr: UriManager.uri -> coerc_carr * coerc_carr
val term_of_carr: coerc_carr -> Cic.term
+
CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
+let generate_dot_file () =
+ let l = CoercDb.to_list () in
+ let preamble = "
+ digraph pippo {
+ node [fontsize=9, width=.4, height=.4];
+ edge [fontsize=10];
+ \n"
+ in
+ let conclusion = " } \n" in
+ let data = List.fold_left
+ (fun acc (src,tgt,c) ->
+ acc ^ CoercDb.name_of_carr src ^ " -> " ^
+ CoercDb.name_of_carr tgt ^ "[label=\"" ^ UriManager.name_of_uri c ^
+ "\"];\n") "" l
+ in
+ preamble ^ data ^ conclusion
+
(* EOF *)
val source_of: Cic.term -> Cic.term
val target_of: Cic.term -> Cic.term
+val generate_dot_file: unit -> string
* *)
let coercion_hashtbl = UriManager.UriHashtbl.create 3
-let rec merge_coercions =
- let module C = Cic in
- let aux = (fun (u,t) -> u,merge_coercions t) in
- function
- C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
- | C.Meta (n,subst) ->
- let subst' =
- List.map
- (function None -> None | Some t -> Some (merge_coercions t)) subst
- in
- C.Meta (n,subst')
- | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty)
- | C.Prod (name,so,dest) ->
- C.Prod (name, merge_coercions so, merge_coercions dest)
- | C.Lambda (name,so,dest) ->
- C.Lambda (name, merge_coercions so, merge_coercions dest)
- | C.LetIn (name,so,dest) ->
- C.LetIn (name, merge_coercions so, merge_coercions dest)
- | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when
- CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CoercGraph.target_of c1 in
- (match CoercGraph.look_for_coercion source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
- | _ -> assert false) (* the composite coercion must exist *)
- | C.Appl l -> C.Appl (List.map merge_coercions l)
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Var (uri, exp_named_subst)
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Const (uri, exp_named_subst)
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutInd (uri,tyno,exp_named_subst)
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutConstruct (uri,tyno,consno,exp_named_subst)
- | C.MutCase (uri,tyno,out,te,pl) ->
- let pl = List.map merge_coercions pl in
- C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl)
- | C.Fix (fno, fl) ->
- let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in
- C.Fix (fno, fl)
- | C.CoFix (fno, fl) ->
- let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in
- C.CoFix (fno, fl)
-
-let merge_coercions_in_obj obj =
- let module C = Cic in
- match obj with
- | C.Constant (id, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (merge_coercions body)
- in
- let ty = merge_coercions ty in
- C.Constant (id, body, ty, params, attrs)
- | C.Variable (name, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (merge_coercions body)
- in
- let ty = merge_coercions ty in
- C.Variable (name, body, ty, params, attrs)
- | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
- assert false
- | C.InductiveDefinition (indtys, params, leftno, attrs) ->
- let indtys =
- List.map
- (fun (name, ind, arity, cl) ->
- let arity = merge_coercions arity in
- let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in
- (name, ind, arity, cl))
- indtys
- in
- C.InductiveDefinition (indtys, params, leftno, attrs)
-
let uris_of_obj uri =
let innertypesuri = UriManager.innertypesuri_of_uri uri in
let bodyuri = UriManager.bodyuri_of_uri uri in
fun ~dbd ~uri ->
profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-let add_single_obj uri obj ~basedir =
+let add_single_obj uri obj refinement_toolkit ~basedir =
+ let module RT = RefinementTool in
let obj =
if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
then
- merge_coercions_in_obj obj
+ refinement_toolkit.RT.pack_coercion_obj obj
else
obj
in
(*** GENERATION OF AUXILIARY LEMMAS ***)
-let generate_elimination_principles ~basedir uri =
+let generate_elimination_principles ~basedir uri refinement_toolkit =
let uris = ref [] in
let elim sort =
try
let uri,obj = CicElim.elim_of ~sort uri 0 in
- add_single_obj uri obj ~basedir;
+ add_single_obj uri obj refinement_toolkit ~basedir;
uris := uri :: !uris
with CicElim.Can_t_eliminate -> ()
in
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,u1) -> true)
-let add_coercion ~basedir ~add_composites uri =
+let add_coercion ~basedir ~add_composites refinement_toolkit uri =
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
*)
let extract_last_two_p ty =
let rec aux = function
- | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) ->
- assert false
- (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
+ | Cic.Prod( _, _, ((Cic.Prod _) as t)) ->
+ aux t
| Cic.Prod( _, src, tgt) -> src, tgt
| _ -> assert false
in
aux ty
in
let ty_src, ty_tgt = extract_last_two_p coer_ty in
- let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
- let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
- let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
+ let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
+ let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
+ let new_coercions =
+ CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri in
let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
(* update the DB *)
List.iter
(fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
new_coercions;
- CoercDb.add_coercion (src_uri, tgt_uri, uri);
+ CoercDb.add_coercion (src_carr, tgt_carr, uri);
(* add the composites obj and they eventual lemmas *)
let lemmas =
if add_composites then
List.fold_left
(fun acc (_,_,uri,obj) ->
- add_single_obj ~basedir uri obj;
+ add_single_obj ~basedir uri obj refinement_toolkit;
uri::acc)
composite_uris new_coercions
else
in
(* store that composite_uris are related to uri. the first component is the
* stuff in the DB while the second is stuff for remove_obj *)
- prerr_endline ("aggiungo: " ^ string_of_bool add_composites ^ UriManager.string_of_uri uri);
- List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
- composite_uris;
+ (*
+ prerr_endline ("adding: " ^
+ string_of_bool add_composites ^ UriManager.string_of_uri uri);
+ List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+ composite_uris;
+ *)
UriManager.UriHashtbl.add coercion_hashtbl uri
(composite_uris,if add_composites then composite_uris else []);
lemmas
Not_found -> () (* mhh..... *)
-let generate_projections ~basedir uri fields =
+let generate_projections ~basedir refinement_toolkit uri fields =
let uris = ref [] in
let projections = CicRecord.projections_of uri (List.map fst fields) in
try
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
- add_single_obj ~basedir uri obj;
+ add_single_obj ~basedir uri obj refinement_toolkit;
let composites =
if coercion then
- add_coercion ~basedir ~add_composites:true uri
+ add_coercion ~basedir ~add_composites:true refinement_toolkit uri
else
[]
in
raise exn
-let add_obj uri obj ~basedir =
- add_single_obj uri obj ~basedir;
+let add_obj refinement_toolkit uri obj ~basedir =
+ add_single_obj uri obj refinement_toolkit ~basedir;
let uris = ref [] in
try
begin
match obj with
| Cic.Constant _ -> ()
| Cic.InductiveDefinition (_,_,_,attrs) ->
- uris := !uris @ generate_elimination_principles ~basedir uri;
+ uris := !uris @
+ generate_elimination_principles ~basedir uri refinement_toolkit;
let rec get_record_attrs =
function
| [] -> None
(match get_record_attrs attrs with
| None -> () (* not a record *)
| Some fields ->
- uris := !uris @ (generate_projections ~basedir uri fields))
+ uris := !uris @
+ (generate_projections ~basedir refinement_toolkit uri fields))
| Cic.CurrentProof _
| Cic.Variable _ -> assert false
end;
exception AlreadyDefined of UriManager.uri
-val merge_coercions: Cic.term -> Cic.term
-
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
-val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list
+val add_obj:
+ RefinementTool.kit ->
+ UriManager.uri -> Cic.obj -> basedir:string ->
+ UriManager.uri list
(* inverse of add_obj; *)
(* Warning: it does not remove the dependencies on the object and on its *)
(* is true are added to the library. *)
(* The list of added objects is returned. *)
val add_coercion:
- basedir:string -> add_composites:bool -> UriManager.uri ->
+ basedir:string -> add_composites:bool ->
+ RefinementTool.kit -> UriManager.uri ->
UriManager.uri list
(* inverse of add_coercion, removes both the eventually created composite *)
--- /dev/null
+(* Copyright (C) 2006, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type type_of_rc =
+ | Success of Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
+ | Exception of string Lazy.t
+
+ (* these are the same functions of cic_unification/ (eventually wrapped) *)
+type kit = {
+ type_of_aux':
+ ?localization_tbl:Token.flocation Cic.CicHash.t ->
+ Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
+ type_of_rc;
+ pack_coercion_obj: Cic.obj -> Cic.obj;
+ apply_subst: Cic.substitution -> Cic.term -> Cic.term ;
+ ppsubst: Cic.substitution -> string;
+ ppmetasenv: Cic.substitution -> Cic.metasenv -> string;
+}
+
exception Fail of string Lazy.t
(**
- calls the opaque tactic on the status, restoring the original
- universe graph if the tactic Fails
+ calls the opaque tactic on the status
*)
let apply_tactic t status =
- t status
+ let (uri,metasenv,bo,ty), gl = t status in
+ match
+ CicRefine.pack_coercion_obj
+ (Cic.CurrentProof ("",metasenv,bo,ty,[],[]))
+ with
+ | Cic.CurrentProof (_,metasenv,bo,ty,_,_) ->
+ (uri,metasenv,bo,ty), gl
+ | _ -> assert false
+;;
(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =
}.
record isGroup (G:PreGroup) : Prop ≝
- { is_monoid: isMonoid G;
+ { is_monoid:> isMonoid G;
inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
}.
unfold left_cancellable;
unfold injective;
intros (x y z);
-rewrite < (e_is_left_unit ? (is_monoid ? G));
-rewrite < (e_is_left_unit ? (is_monoid ? G) z);
+rewrite < (e_is_left_unit ? G);
+rewrite < (e_is_left_unit ? G z);
rewrite < (inv_is_left_inverse ? G x);
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
+rewrite > (associative ? (is_semi_group ? ( G)));
apply eq_f;
assumption.
qed.
unfold injective;
simplify;fold simplify (op G);
intros (x y z);
-rewrite < (e_is_right_unit ? (is_monoid ? G));
-rewrite < (e_is_right_unit ? (is_monoid ? G) z);
+rewrite < (e_is_right_unit ? ( G));
+rewrite < (e_is_right_unit ? ( G) z);
rewrite < (inv_is_right_inverse ? G x);
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
+rewrite < (associative ? (is_semi_group ? ( G)));
rewrite > H;
reflexivity.
qed.
∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
intros;
apply (eq_op_x_y_op_z_y_to_eq ? y);
-rewrite > (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite > (associative ? G);
rewrite > (inv_is_left_inverse ? G);
-rewrite > (e_is_right_unit ? (is_monoid ? G));
+rewrite > (e_is_right_unit ? G);
assumption.
qed.
∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
intros;
apply (eq_op_x_y_op_x_z_to_eq ? x);
-rewrite < (associative ? (is_semi_group ? (is_monoid ? G)));
+rewrite < (associative ? G);
rewrite > (inv_is_right_inverse ? G);
rewrite > (e_is_left_unit ? (is_monoid ? G));
assumption.
∀G,G'.∀f:morphism G G'.f˜1 = 1.
intros;
apply (eq_op_x_y_op_z_y_to_eq G' (f˜1));
-rewrite > (e_is_left_unit ? (is_monoid ? G') ?);
+rewrite > (e_is_left_unit ? G' ?);
rewrite < (f_morph ? ? f);
-rewrite > (e_is_left_unit ? (is_monoid ? G));
+rewrite > (e_is_left_unit ? G);
reflexivity.
qed.
elim H1;
clear H1;
exists;
-[
+[apply ((a \sub H)\sup-1 · x1)
|
].
qed.
(cic:/matita/algebra/monoids/magma.con M).
record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group: isSemiGroup M;
+ { is_semi_group:> isSemiGroup M;
e_is_left_unit:
is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
e_is_right_unit:
(UriManager.name_of_uri u ^ ":"
^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
(CoercDb.to_list ()));
+ addDebugItem "show coercions graph" (fun _ ->
+ let str = CoercGraph.generate_dot_file () in
+ let filename, oc = Filename.open_temp_file "xx" ".dot" in
+ output_string oc str;
+ close_out oc;
+ let ps = Filename.temp_file "yy" ".png" in
+ ignore (Sys.command ("/usr/bin/dot -Tpng -o" ^ ps ^ " " ^ filename));
+ ignore (Sys.command ("/usr/bin/display " ^ ps));
+ Sys.remove ps;
+ Sys.remove filename);
+
addDebugItem "print top-level grammar entries"
CicNotationParser.print_l2_pattern;
addDebugItem "dump moo to stderr" (fun _ ->
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
-let initial_statuses =
+let initial_statuses () =
(* these include_paths are used only to load the initial notation *)
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
val mutable statements = [] (** executed statements *)
- val mutable history = [ initial_statuses ]
+ val mutable history = [ initial_statuses () ]
(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.
method private reset_buffer =
statements <- [];
- history <- [ initial_statuses ];
+ history <- [ initial_statuses () ];
userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
rm -rf $TMPDIRNAMEOLD
cd $TMPDIRNAME
rm -rf helm
-svn co ${SVNROOT}helm/matita/scripts/ > LOG.svn 2>&1
+svn co ${SVNROOT}helm/software/matita/scripts/ > LOG.svn 2>&1
scripts/profile_svn.sh 2> LOG
MARK=`echo "select distinct mark from bench where mark like '$TODAY%' order by mark" | mysql -u helm matita | tail -n 1`
projects / helm.git / commitdiff