(if fields <> [] then "\n" else "") ^
String.concat ";\n"
(List.map
- (fun (name,ty,coercion) ->
- " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
+ (fun (name,ty,coercion,arity) ->
+ " " ^ name ^
+ if coercion then (":" ^
+ if arity > 0 then string_of_int arity else "" ^ ">") else ": " ^
+ pp_term ty) fields)
let pp_obj = function
| Ast.Inductive (params, types) ->
* will be given in proof editing mode using the tactical language,
* unless the flavour is an Axiom
*)
- | Record of (string * term) list * string * term * (string * term * bool) list
+ | Record of (string * term) list * string * term * (string * term * bool * int) list
(** left parameters, name, type, fields *)
(** {2 Standard precedences} *)
let index = ref 0 in
let freshen_term = freshen_term ~index in
let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
- let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
+ let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
match obj with
| CicNotationPt.Inductive (params, indtypes) ->
let indtypes =
| Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) ->
- if CoercGraph.is_a_coercion (Deannotate.deannotate_term he) &&
- !Acic2content.hide_coercions
+ let last_n n l =
+ let rec aux =
+ function
+ [] -> assert false
+ | [_] as l -> l,1
+ | he::tl ->
+ let (res,len) as res' = aux tl in
+ if len < n then
+ he::res,len + 1
+ else
+ res'
+ in
+ match fst (aux l) with
+ [] -> assert false
+ | [t] -> t
+ | Ast.AttributedTerm (_,(Ast.Appl l))::tl ->
+ idref aid (Ast.Appl (l@tl))
+ | l -> idref aid (Ast.Appl l)
+ in
+ let deannot_he = Deannotate.deannotate_term he in
+ if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
then
- let rec last =
- function
- [] -> assert false
- | [t] -> t
- | _::tl -> last tl
- in
- idref aid (k (last tl))
+ match CoercGraph.is_a_coercion_to_funclass deannot_he with
+ | None -> idref aid (last_n 1 (List.map k tl))
+ | Some i -> idref aid (last_n (i+1) (List.map k tl))
else
idref aid (Ast.Appl (List.map k args))
| Cic.AAppl (aid,args) ->
]
type object_class =
- [ `Coercion
+ [ `Coercion of int
| `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
- | `Record of (string * bool) list (**
+ | `Record of (string * bool * int) list (**
inductive type that encodes a record; the arguments are
- the record fields names and if they are coercions *)
+ the record fields names and if they are coercions and
+ then the coercion arity *)
| `Projection (** record projection *)
]
let class_modifiers = pop_class_modifiers ctxt in
push ctxt
(match pop_tag_attrs ctxt with
- | ["value", "coercion"] -> Obj_class `Coercion
+ | ["value", "coercion"] -> Obj_class (`Coercion 0)
+ | ("value", "coercion")::["arity",n]
+ | ("arity",n)::["value", "coercion"] ->
+ let arity = try int_of_string n with Failure _ ->
+ parse_error "\"arity\" must be an integer"
+ in
+ Obj_class (`Coercion arity)
| ["value", "elim"] ->
(match class_modifiers with
| [Cic_term (Cic.ASort (_, sort))] -> Obj_class (`Elim sort)
(function
| Obj_field name ->
(match Str.split (Str.regexp " ") name with
- | [name] -> name, false
- | [name;"coercion"] -> name,true
+ | [name] -> name, false, 0
+ | [name;"coercion"] -> name,true,0
+ | [name;"coercion"; n] ->
+ let n =
+ try int_of_string n
+ with Failure _ ->
+ parse_error "int expected after \"coercion\""
+ in
+ name,true,n
| _ ->
parse_error
"wrong \"field\"'s name attribute")
| Cic.CurrentProof (_, _, _, _, _, attributes)
| Cic.InductiveDefinition (_, _, _, attributes) ->
attributes
+
+let arity_of_composed_coercion obj =
+ let attrs = attributes_of_obj obj in
+ try
+ let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
+ match tag with
+ | `Class (`Coercion n) -> n
+ | _-> assert false
+ with Not_found -> 0
+;;
+
let rec mk_rels howmany from =
match howmany with
| 0 -> []
val params_of_obj: Cic.obj -> UriManager.uri list
val attributes_of_obj: Cic.obj -> Cic.attribute list
+val arity_of_composed_coercion: Cic.obj -> int
(** mk_rels [howmany] [from]
* creates a list of [howmany] rels starting from [from] in decreasing order *)
let xml_of_attrs attributes =
let class_of = function
- | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+ | `Coercion n ->
+ Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
| `Elim s ->
Xml.xml_nempty "class" [None,"value","elim"]
[< Xml.xml_empty
| `Record field_names ->
Xml.xml_nempty "class" [None,"value","record"]
(List.fold_right
- (fun (name,coercion) res ->
+ (fun (name,coercion,arity) res ->
[< Xml.xml_empty "field"
- [None,"name",if coercion then name ^ " coercion" else name];
+ [None,"name",
+ if coercion then
+ name ^ " coercion " ^ string_of_int arity
+ else
+ name];
res >]
) field_names [<>])
| `Projection -> Xml.xml_empty "class" [None,"value","projection"]
let aobj =
match obj with
C.Constant (id,Some bo,ty,params,attrs) ->
- let bo' = eta_fix [] [] bo in
+ let bo' = (*eta_fix [] []*) bo in
let ty' = eta_fix [] [] ty in
let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
(cid,i,acanonical_context,aterm))
conjectures' in
(* let time1 = Sys.time () in *)
- let bo' = eta_fix conjectures' [] bo in
+ let bo' = (*eta_fix conjectures' []*) bo in
let ty' = eta_fix conjectures' [] ty in
(*
let time2 = Sys.time () in
let fields' =
snd (
List.fold_left
- (fun (context,res) (name,ty,_coercion) ->
+ (fun (context,res) (name,ty,_coercion,arity) ->
let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
concl fields' in
let con' = add_params con in
let tyl = [name,true,ty',["mk_" ^ name,con']] in
- let field_names = List.map (fun (x,_,y) -> x,y) fields in
+ let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
| CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
- (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
+ (List.rev_map (fun (_,ty,_,_) -> domain_rev_of_term [] ty) fields) in
let dom =
List.fold_left
(fun dom (_,ty) ->
List.filter
(fun (_,name) ->
not ( List.exists (fun (name',_) -> name = Id name') params
- || List.exists (fun (name',_,_) -> name = Id name') fields)
+ || List.exists (fun (name',_,_,_) -> name = Id name') fields)
) dom
in
rev_uniq domain_rev
UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
| C.Meta (n,l1) ->
"?" ^ (string_of_int n) ^ "[" ^
-(*
String.concat " ; "
(List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
-*)
"]"
| C.Sort s ->
(match s with
| C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
- C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
- | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
+ C.Name n -> "(\forall " ^ n ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
+ | C.Anonymous -> "(" ^ pp s l ^ "\\to " ^ pp t ((Some b)::l) ^ ")"
)
| C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
| C.Lambda (b,s,t) ->
"(\\lambda " ^ ppname b ^ ":" ^ pp s l ^ "." ^ pp t ((Some b)::l) ^ ")"
| C.LetIn (b,s,t) ->
- "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ " let " ^ ppname b ^ " \def " ^ pp s l ^ " in " ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
exception AssertFailure of string Lazy.t;;
let insert_coercions = ref true
+let pack_coercions = ref true
let debug_print = fun _ -> ()
+(* let debug_print x = prerr_endline (Lazy.force x);; *)
let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
let is_a_double_coercion t =
let last_of l =
- let rec aux = function
- | x::[] -> x
- | x::tl -> aux tl
+ let rec aux acc = function
+ | x::[] -> acc,x
+ | x::tl -> aux (acc@[x]) tl
| [] -> assert false
in
- aux l
- in
- let dummyres =
- false, Cic.Implicit None, Cic.Implicit None, Cic.Implicit None
+ aux [] l
in
+ let imp = Cic.Implicit None in
+ let dummyres = false,imp, imp,imp,imp 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
+ | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 ->
+ let sib2,head = last_of tl2 in
+ true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
+ (c2::sib2@[Cic.Implicit None])])
| _ -> dummyres)
| _ -> dummyres
+
+let more_args_than_expected subst he context hetype' tlbody_and_type =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst he context ^
+ " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^
+ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected")
+;;
+
+let mk_prod_of_metas metasenv context' subst args =
+ let rec mk_prod metasenv context' = function
+ | [] ->
+ 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)
+ | (_,argty)::tl ->
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit_type metasenv subst context'
+ in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context'
+ in
+ let meta = Cic.Meta (idx,irl) in
+ let name =
+ (* The name must be fresh for context. *)
+ (* Nevertheless, argty is well-typed only in context. *)
+ (* Thus I generate a name (name_hint) in context and *)
+ (* then I generate a name --- using the hint name_hint *)
+ (* --- that is fresh in context'. *)
+ let name_hint =
+ (* Cic.Name "pippo" *)
+ FreshNamesGenerator.mk_fresh_name ~subst metasenv
+ (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
+ (CicMetaSubst.apply_subst_context subst context')
+ Cic.Anonymous
+ ~typ:(CicMetaSubst.apply_subst subst argty)
+ in
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name ~subst
+ [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
+ in
+ let metasenv,target =
+ mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
+ in
+ metasenv,Cic.Prod (name,meta,target)
+ in
+ mk_prod metasenv context' args
+;;
let rec type_of_constant uri ugraph =
let module C = Cic in
type_of_aux subst metasenv context he ugraph
in
let tlbody_and_type,subst'',metasenv'',ugraph2 =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) tl ([],subst',metasenv',ugraph1)
+ typeof_list subst' metasenv' context ugraph1 tl
in
- let tl',applty,subst''',metasenv''',ugraph3 =
+ let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
eat_prods true subst'' metasenv'' context
he' hetype tlbody_and_type ugraph2
in
- avoid_double_coercion context
- subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
+ let newappl = (C.Appl (coerced_he::coerced_args)) in
+ avoid_double_coercion
+ context subst''' metasenv''' ugraph3 newappl applty
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
subst,metasenv,ugraph)
| _ -> (* easy case *)
let tlbody_and_type,subst,metasenv,ugraph4 =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+ typeof_list subst metasenv context ugraph4 (right_args @ [term'])
in
- let _,_,subst,metasenv,ugraph4 =
+ let _,_,_,subst,metasenv,ugraph4 =
eat_prods false subst metasenv context
outtype outtypety tlbody_and_type ugraph4
in
(CicPp.ppterm t2''))))
and avoid_double_coercion context subst metasenv ugraph t ty =
- let b, c1, c2, head = is_a_double_coercion t in
+ let b, c1, c2, head, c1_c2_implicit = 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
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (fun c ->
+ (function
+ | c when not (CoercGraph.is_composite c) ->
+ debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
+ None
+ | c ->
let newt =
match c with
| Cic.Appl l -> Cic.Appl (l @ [head])
| _ -> Cic.Appl [c;head]
in
+ debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt));
(try
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context newt ugraph in
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv newt t ugraph
- in
debug_print
(lazy
("packing: " ^
CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt));
+ let newt,_,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context newt ugraph in
+ debug_print (lazy "tipa...");
+ let subst, metasenv, ugraph =
+ (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
+ fo_unif_subst subst context metasenv newt t ugraph
+ in
+ debug_print (lazy "unifica...");
Some (newt, ty, subst, metasenv, ugraph)
- with RefineFailure _ | Uncertain _ -> None))
+ with
+ | RefineFailure s | Uncertain s when not !pack_coercions->
+ debug_print s; debug_print (lazy "stop\n");None
+ | RefineFailure s | Uncertain s ->
+ debug_print s;debug_print (lazy "goon\n");
+ try
+ pack_coercions := false; (* to avoid diverging *)
+ let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context c1_c2_implicit ugraph
+ in
+ pack_coercions := true;
+ let b, _, _, _, _ =
+ is_a_double_coercion refined_c1_c2_implicit
+ in
+ if b then
+ None
+ else
+ let head' =
+ match refined_c1_c2_implicit with
+ | Cic.Appl l -> HExtlib.list_last l
+ | _ -> assert false
+ in
+ let subst, metasenv, ugraph =
+ try fo_unif_subst subst context metasenv
+ head head' ugraph
+ with RefineFailure s| Uncertain s->
+ debug_print s;assert false
+ in
+ let subst, metasenv, ugraph =
+ fo_unif_subst subst context metasenv
+ refined_c1_c2_implicit t ugraph
+ in
+ Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
+ with
+ | RefineFailure s | Uncertain s ->
+ pack_coercions := true;debug_print s;None
+ | exn -> pack_coercions := true; raise exn))
candidates
in
(match selected with
| Some x -> x
| None ->
- prerr_endline ("#### Coercion not packed: " ^ CicPp.ppterm t);
- assert false)
+ debug_print
+ (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
+ t, ty, subst, metasenv, ugraph)
| _ -> assert false) (* the composite coercion must exist *)
else
t, ty, subst, metasenv, ugraph
+ and typeof_list subst metasenv context ugraph l =
+ let tlbody_and_type,subst,metasenv,ugraph =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) l ([],subst,metasenv,ugraph)
+ in
+ tlbody_and_type,subst,metasenv,ugraph
+
and eat_prods
- allow_coercions subst metasenv context he hetype tlbody_and_type ugraph
+ allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
=
- let rec mk_prod metasenv context' =
- function
- [] ->
- 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)
- | (_,argty)::tl ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- let meta = Cic.Meta (idx,irl) in
- let name =
- (* The name must be fresh for context. *)
- (* Nevertheless, argty is well-typed only in context. *)
- (* Thus I generate a name (name_hint) in context and *)
- (* then I generate a name --- using the hint name_hint *)
- (* --- that is fresh in context'. *)
- let name_hint =
- (* Cic.Name "pippo" *)
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
- in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
- FreshNamesGenerator.mk_fresh_name ~subst
- [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
- in
- let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
- in
- metasenv,Cic.Prod (name,meta,target)
- in
- let ((subst,metasenv,ugraph1),hetype') =
- if CicUtil.is_meta_closed hetype then
- (subst,metasenv,ugraph),hetype
- else
- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- try
- fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
- with exn ->
- enrich localization_tbl he
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"
- (* "\nReason: " ^ Lazy.force exn*)))) exn
+ (* aux function to add coercions to funclass *)
+ let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+ (* {{{ body *)
+ let pristinemenv = metasenv in
+ let metasenv,hetype' =
+ mk_prod_of_metas metasenv context subst args_bo_and_ty
+ in
+ try
+ let subst,metasenv,ugraph =
+ fo_unif_subst_eat_prods
+ subst context metasenv hetype hetype' ugraph
+ in
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ with RefineFailure s | Uncertain s as exn
+ when allow_coercions && !insert_coercions ->
+ (* {{{ we search a coercion of the head (saturated) to funclass *)
+ let metasenv = pristinemenv in
+ debug_print (lazy
+ ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^
+ " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^
+ " cause: " ^ Lazy.force s));
+ let how_many_args_are_needed =
+ let rec aux n = function
+ | Cic.Prod(_,_,t) -> aux (n+1) t
+ | _ -> n
+ in
+ aux 0 (CicMetaSubst.apply_subst subst hetype)
+ in
+ let args, remainder =
+ HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
+ in
+ let args = List.map fst args in
+ let x =
+ if args <> [] then
+ match he with
+ | Cic.Appl l -> Cic.Appl (l@args)
+ | _ -> Cic.Appl (he::args)
+ else
+ he
+ in
+ let x,xty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context x ugraph
+ in
+ let carr_src =
+ CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty)
+ in
+ let carr_tgt = CoercDb.Fun 0 in
+ match CoercGraph.look_for_coercion' carr_src carr_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotMetaClosed
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.SomeCoercion candidates ->
+ match
+ HExtlib.list_findopt
+ (fun coerc ->
+ let t = Cic.Appl [coerc;x] in
+ debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t));
+ try
+ (* we want this to be available in the error handler fo the
+ * following (so it has its own try. *)
+ let t,tty,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context t ugraph
+ in
+ try
+ let metasenv, hetype' =
+ mk_prod_of_metas metasenv context subst remainder
+ in
+ debug_print (lazy
+ (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^
+ CicMetaSubst.ppterm subst hetype'));
+ let subst,metasenv,ugraph =
+ fo_unif_subst_eat_prods
+ subst context metasenv tty hetype' ugraph
+ in
+ debug_print (lazy " success!");
+ Some (subst,metasenv,ugraph,tty,t,remainder)
+ with
+ | Uncertain _ | RefineFailure _
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ try
+ let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
+ fix_arity
+ metasenv context subst t tty remainder ugraph
+ in
+ Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
+ with exn -> None
+ with exn -> None)
+ candidates
+ with
+ | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
+ subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+ | None ->
+ enrich localization_tbl he
+ ~f:(fun _-> more_args_than_expected subst he context hetype
+ args_bo_and_ty) exn
+ (* }}} end coercion to funclass stuff *)
+ (* }}} end fix_arity *)
in
- let rec eat_prods metasenv subst context hetype ugraph =
+ (* aux function to process the type of the head and the args in parallel *)
+ let rec eat_prods_and_args
+ pristinemenv metasenv subst context he hetype ugraph newargs
+ =
+ (* {{{ body *)
function
- | [] -> [],metasenv,subst,hetype,ugraph
+ | [] -> newargs,subst,metasenv,he,hetype,ugraph
| (hete, hety)::tl ->
- (match (CicReduction.whd ~subst context hetype) with
- Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph1 =
- try
- let subst,metasenv,ugraph1 =
- fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph
- in
- hete,subst,metasenv,ugraph1
- with exn when allow_coercions && !insert_coercions ->
- (* we search a coercion from hety to s *)
- let coer, tgt_carr =
- let carr t subst context =
- CicReduction.whd ~delta:false
- context (CicMetaSubst.apply_subst subst t )
- in
- let c_hety = carr hety subst context in
- let c_s = carr s subst context in
- CoercGraph.look_for_coercion c_hety c_s, c_s
- in
- (match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl hete
- (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl hete
- (Uncertain
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*))))
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (fun c ->
- try
- let t = Cic.Appl[c;hete] in
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context
- t ugraph
- in
- let newt, _, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv
- ugraph newt tgt_carr
- in
- let subst,metasenv,ugraph1 =
- fo_unif_subst subst context metasenv
- newhety s ugraph
- in
- Some (newt, subst, metasenv, ugraph)
- with Uncertain _ | RefineFailure _ -> None)
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- enrich localization_tbl hete
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst hete
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context subst hety
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn))
- | exn ->
+ match (CicReduction.whd ~subst context hetype) with
+ | Cic.Prod (n,s,t) ->
+ let arg,subst,metasenv,ugraph1 =
+ try
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst_eat_prods2
+ subst context metasenv hety s ugraph
+ in
+ (hete,hety),subst,metasenv,ugraph1
+ (* {{{ we search a coercion from hety to s if fails *)
+ with RefineFailure _ | Uncertain _ as exn
+ when allow_coercions && !insert_coercions ->
+ let coer, tgt_carr =
+ let carr t subst context =
+ CicReduction.whd ~delta:false
+ context (CicMetaSubst.apply_subst subst t )
+ in
+ let c_hety = carr hety subst context in
+ let c_s = carr s subst context in
+ CoercGraph.look_for_coercion c_hety c_s, c_s
+ in
+ (match coer with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
enrich localization_tbl hete
- ~f:(fun _ ->
+ (RefineFailure
(lazy ("The term " ^
CicMetaSubst.ppterm_in_context subst hete
context ^ " has type " ^
CicMetaSubst.ppterm_in_context subst hety
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context subst s context
- (* "\nReason: " ^ Lazy.force e*)))) exn
- in
- let coerced_args,metasenv',subst',t',ugraph2 =
- eat_prods metasenv subst context
- (CicSubstitution.subst arg t) ugraph1 tl
- in
- arg::coerced_args,metasenv',subst',t',ugraph2
- | _ ->
- raise (RefineFailure
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype'
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"))))
+ (* "\nReason: " ^ Lazy.force e*))))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl hete
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))))
+ | CoercGraph.SomeCoercion candidates ->
+ let selected =
+ HExtlib.list_findopt
+ (fun c ->
+ try
+ let t = Cic.Appl[c;hete] in
+ let newt,newhety,subst,metasenv,ugraph =
+ type_of_aux subst metasenv context
+ t ugraph
+ in
+ let newt, newty, subst, metasenv, ugraph =
+ avoid_double_coercion context subst metasenv
+ ugraph newt tgt_carr
+ in
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst subst context metasenv
+ newhety s ugraph
+ in
+ Some ((newt,newty), subst, metasenv, ugraph)
+ with Uncertain _ | RefineFailure _ -> None)
+ candidates
+ in
+ (match selected with
+ | Some x -> x
+ | None ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*)))) exn))
+ | exn ->
+ enrich localization_tbl hete
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context ^
+ "\nReason: " ^ Printexc.to_string exn))) exn
+ (* }}} end coercion stuff *)
+ in
+ eat_prods_and_args pristinemenv metasenv subst context he
+ (CicSubstitution.subst (fst arg) t)
+ ugraph1 (newargs@[arg]) tl
+ | _ ->
+ try
+ let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+ fix_arity
+ pristinemenv context subst he hetype
+ (newargs@[hete,hety]@tl) ugraph
+ in
+ eat_prods_and_args metasenv
+ metasenv subst context he hetype' ugraph [] args_bo_and_ty
+ with RefineFailure s | Uncertain s ->
+ (* unable to fix arity *)
+ let msg =
+ more_args_than_expected
+ subst he context hetype args_bo_and_ty
+ in
+ raise (RefineFailure msg)
+ (* }}} *)
+ in
+ (* first we check if we are in the simple case of a meta closed term *)
+ let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
+ if CicUtil.is_meta_closed hetype then
+ (* this optimization is to postpone fix_arity (the most common case)*)
+ subst,metasenv,ugraph,hetype,he,args_bo_and_ty
+ else
+ (* this (says CSC) is also useful to infer dependent types *)
+ fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
in
- let coerced_args,metasenv,subst,t,ugraph2 =
- eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
+ let coerced_args,subst,metasenv,he,t,ugraph =
+ eat_prods_and_args
+ metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
in
- coerced_args,t,subst,metasenv,ugraph2
+ he,(List.map fst coerced_args),t,subst,metasenv,ugraph
in
(* eat prods ends here! *)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
- let b,_,_,_ = is_a_double_coercion t in
+ let b,_,_,_,_ = is_a_double_coercion t in
(* prerr_endline "CANDIDATO!!!!"; *)
if b then
let ugraph = CicUniv.empty_ugraph in
profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
+(* vim:set foldmethod=marker: *)
fo_unif_l
test_equality_only subst metasenv (lr1, lr2) ugraph
with
- | UnificationFailure _
- | Uncertain _ as exn ->
+ | UnificationFailure s
+ | Uncertain s as exn ->
(match l1, l2 with
| (((Cic.Const (uri1, ens1)) as c1) :: tl1),
(((Cic.Const (uri2, ens2)) as c2) :: tl2) when
CoercGraph.is_a_coercion c1 &&
- CoercGraph.is_a_coercion c2 ->
+ CoercGraph.is_a_coercion c2 &&
+ not (UriManager.eq uri1 uri2) ->
let body1, attrs1, ugraph =
match CicEnvironment.get_obj ugraph uri1 with
| Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u
| _ -> assert false
in
let is_composite1 =
- List.exists ((=) (`Class `Coercion)) attrs1 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs1
+ in
let is_composite2 =
- List.exists ((=) (`Class `Coercion)) attrs2 in
+ List.exists
+ (function `Class (`Coercion _) -> true | _-> false)
+ attrs2
+ in
(match is_composite1, is_composite2 with
| false, false -> raise exn
| true, false ->
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
+trie.cmo: trie.cmi
+trie.cmx: trie.cmi
+hTopoSort.cmo: hTopoSort.cmi
+hTopoSort.cmx: hTopoSort.cmi
refCounter.cmo: refCounter.cmi
refCounter.cmx: refCounter.cmi
graphvizPp.cmo: graphvizPp.cmi
patternMatcher.mli \
hLog.mli \
trie.mli \
+ hTopoSort.mli \
refCounter.mli \
graphvizPp.mli \
$(NULL)
module type GraphvizFormatter =
sig
val header:
+ ?graph_type:string ->
?name:string -> ?graph_attrs:(attribute list) ->
?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) ->
Format.formatter ->
attributes attrs fmt;
fprintf fmt "];@]@,"
- let header ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt =
- fprintf fmt "@[<hv2>strict digraph %s {@," name;
+ let header ?(graph_type = "digraph") ?(name = "g") ?(graph_attrs = []) ?node_attrs ?edge_attrs fmt =
+ fprintf fmt "@[<hv2>%s %s {@," graph_type name;
List.iter (fun (k, v) -> fprintf fmt "@[<hv2>%s=@,%s;@]@," k v)
graph_attrs;
(match node_attrs with
module type GraphvizFormatter =
sig
(** @param name graph name
+ * @param graph_type type of dot graph, default value "digraph"
+ * interesting options: "strict digraph"
* @param graph_attrs graph attributes
* @param node_attrs graph-wide node attributes
* @param edge_attrs graph-wide edge attributes *)
val header:
+ ?graph_type:string ->
?name:string -> ?graph_attrs:(attribute list) ->
?node_attrs:(attribute list) -> ?edge_attrs:(attribute list) ->
Format.formatter ->
| n, hd :: tl -> aux (hd :: acc) (n - 1) tl in
aux [] n l
+let list_last l =
+ let l = List.rev l in
+ try List.hd l with exn -> raise (Failure "HExtlib.list_last")
+;;
+
(** {2 File predicates} *)
let is_dir fname =
val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*)
val list_findopt: ('a -> 'b option) -> 'a list -> 'b option
val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
+val list_last: 'a list -> 'a
(** split_nth n l
* @returns two list, the first contains at least n elements, the second the
--- /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/
+ *)
+
+module Make (OT:Map.OrderedType) =
+ struct
+
+ module M = Map.Make(OT);;
+
+ let topological_sort l find_deps =
+ let find_deps m x =
+ let deps = find_deps x in
+ M.add x deps m
+ in
+ (* build the partial order relation *)
+ let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+ let m = (* keep only deps inside l *)
+ List.fold_left
+ (fun m' i ->
+ M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m')
+ M.empty l
+ in
+ let m = M.map (fun x -> Some x) m in
+ (* utils *)
+ let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+ let split l m = List.filter (fun i -> M.find i m = Some []) l in
+ let purge l m =
+ M.mapi
+ (fun k v -> if List.mem k l then None else
+ match v with
+ | None -> None
+ | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll))
+ m
+ in
+ let rec aux m res =
+ let keys = keys m in
+ let ok = split keys m in
+ let m = purge ok m in
+ let res = ok @ res in
+ if ok = [] then res else aux m res
+ in
+ let rc = List.rev (aux m []) in
+ rc
+ ;;
+
+ end
+;;
+
--- /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/
+ *)
+
+module Make :
+ functor (OT : Map.OrderedType) ->
+ sig
+ module M : Map.S with type key = OT.t
+ val topological_sort :
+ M.key list -> (M.key -> M.key list) -> M.key list
+ end
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 8
+let magic = 9
type 'obj command =
| Default of loc * string * UriManager.uri list
| Drop of loc
| Print of loc * string
| Qed of loc
- | Coercion of loc * UriManager.uri * bool (* add composites *)
+ | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *)
| Obj of loc * 'obj
type ('term, 'lazy_term, 'reduction, 'ident) tactical =
sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
-let pp_coercion uri do_composites =
- sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
+let pp_coercion uri do_composites arity =
+ sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
(if do_composites then "compounds" else "no compounds")
let pp_command ~obj_pp = function
| Drop _ -> "drop"
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
- | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
+ | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
| Obj (_,obj) -> obj_pp obj
| Default (_,what,uris) ->
pp_default what uris
| GrafiteAst.Default (loc, name, uris) ->
let uris = List.map rehash_uri uris in
GrafiteAst.Default (loc, name, uris)
- | GrafiteAst.Coercion (loc, uri, close) ->
- GrafiteAst.Coercion (loc, rehash_uri uri, close)
+ | GrafiteAst.Coercion (loc, uri, close, arity) ->
+ GrafiteAst.Coercion (loc, rehash_uri uri, close, arity)
| cmd ->
prerr_endline "Found a command not expected in a .moo:";
let obj_pp _ = assert false in
type 'a eval_from_moo =
{ efm_go: GT.status -> string -> GT.status }
-let coercion_moo_statement_of uri =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
+let coercion_moo_statement_of arity uri =
+ GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
let refinement_toolkit = {
RefinementTool.type_of_aux' =
RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
}
-let eval_coercion status ~add_composites uri =
+let eval_coercion status ~add_composites uri arity =
let status,compounds =
- GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
+ GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity
+ in
let moo_content =
- List.map coercion_moo_statement_of (uri::compounds)
+ List.map (coercion_moo_statement_of arity) (uri::compounds)
in
let status = GT.add_moo_content moo_content status in
{status with GT.proof_status = GT.No_proof},
let obj,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
- List.mem (`Class `Coercion) attrs
+ try
+ match List.find
+ (function `Class (`Coercion _) -> true | _-> false) attrs
+ with `Class (`Coercion n) -> true,n | _ -> assert false
+ with Not_found -> false,0
with Not_found -> assert false
in
(* looking at the fields we can know the 'wanted' coercions, but not the
let wanted_coercions =
HExtlib.filter_map
(function
- | (name,true) ->
+ | (name,true,arity) ->
Some
- (UriManager.uri_of_string
+ (arity, UriManager.uri_of_string
(GT.qualify status name ^ ".con"))
| _ -> None)
fields
List.split
(HExtlib.filter_map
(fun uri ->
- let is_a_wanted_coercion =
- List.exists (UriManager.eq uri) wanted_coercions
+ let is_a_wanted_coercion,arity_wanted =
+ try
+ let arity,_ =
+ List.find (fun (n,u) -> UriManager.eq u uri)
+ wanted_coercions
+ in
+ true, arity
+ with Not_found -> false, 0
in
- if is_a_coercion uri || is_a_wanted_coercion then
- Some (uri, coercion_moo_statement_of uri)
+ let is_a_coercion, arity_coercion = is_a_coercion uri in
+ if is_a_coercion then
+ Some (uri, coercion_moo_statement_of arity_coercion uri)
+ else if is_a_wanted_coercion then
+ Some (uri, coercion_moo_statement_of arity_wanted uri)
else
- None)
+ None)
lemmas)
in
(*prerr_endline "actual coercions:";
let status, lemmas = add_obj uri obj status in
{status with GT.proof_status = GT.No_proof},
uri::lemmas
- | GrafiteAst.Coercion (loc, uri, add_composites) ->
- eval_coercion status ~add_composites uri
+ | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
+ eval_coercion status ~add_composites uri arity
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
match obj with
{status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
lemmas
-let add_coercion refinement_toolkit ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites refinement_toolkit uri in
+let add_coercion refinement_toolkit ~add_composites status uri arity =
+ let compounds =
+ LibrarySync.add_coercion ~add_composites refinement_toolkit uri arity in
{status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
compounds
val add_coercion:
RefinementTool.kit ->
add_composites:bool -> GrafiteTypes.status ->
- UriManager.uri ->
+ UriManager.uri -> int ->
GrafiteTypes.status * UriManager.uri list
val time_travel:
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
name = IDENT ;
- coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ;
- ty = term -> (name,ty,coercion)
+ coercion = [
+ SYMBOL ":" -> false,0
+ | SYMBOL ":"; SYMBOL ">" -> true,0
+ | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+ ];
+ ty = term ->
+ let b,n = coercion in
+ (name,ty,b,n)
] SEP SYMBOL ";"; SYMBOL "}" ->
let params =
List.fold_right
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ->
- GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
+ | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+ let arity = match arity with None -> 0 | Some x -> x in
+ GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 5
+let magic = 6
type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
| CoercDb.Uri _, CoercDb.Uri _ ->
let c_from_tgt =
List.filter
- (fun (f,t,_) -> eq_carr f tgt && not (eq_carr t src))
+ (fun (f,t,_) -> eq_carr f tgt (*&& not (eq_carr t src)*))
coercions
in
let c_to_src =
List.filter
- (fun (f,t,_) -> eq_carr t src && not (eq_carr f tgt))
+ (fun (f,t,_) -> eq_carr t src (*&& not (eq_carr f tgt)*))
coercions
in
(HExtlib.flatten_map
| _ -> [] (* do not close in case source or target is not an indty ?? *)
;;
-let obj_attrs = [`Class `Coercion; `Generated]
+let obj_attrs n = [`Class (`Coercion n); `Generated]
exception UnableToCompose
(* generate_composite_closure (c2 (c1 s)) in the universe graph univ *)
-let generate_composite_closure rt c1 c2 univ =
+let generate_composite_closure rt c1 c2 univ arity =
let module RT = RefinementTool in
let c1_ty,univ = CicTypeChecker.type_of_aux' [] [] c1 univ in
let c2_ty,univ = CicTypeChecker.type_of_aux' [] [] c2 univ in
- let rec mk_implicits n =
- match n with
- | 0 -> []
- | _ -> (Cic.Implicit None) :: mk_implicits (n-1)
+ let rec mk_implicits = function
+ | 0 -> [] | n -> (Cic.Implicit None) :: mk_implicits (n-1)
in
- let rec mk_lambda_spline c = function
+ let rec mk_lambda_spline c namer = function
| 0 -> c
| n ->
Cic.Lambda
- (Cic.Name ("A" ^ string_of_int (n-1)),
+ (namer n,
(Cic.Implicit None),
- mk_lambda_spline c (n-1))
+ mk_lambda_spline c namer (n-1))
in
- let rec count_saturations_needed n = function
- | Cic.Prod (_,src, ((Cic.Prod _) as t)) -> count_saturations_needed (n+1) t
- | _ -> n
+ let count_saturations_needed t arity =
+ let rec aux acc n = function
+ | Cic.Prod (name,src, ((Cic.Prod _) as t)) ->
+ aux (acc@[name]) (n+1) t
+ | _ -> n,acc
+ in
+ let len,names = aux [] 0 t in
+ let len = len - arity in
+ List.fold_left
+ (fun (n,l) x -> if n <= len then n+1,l@[x] else n,l) (0,[])
+ names
in
let compose c1 nc1 c2 nc2 =
Cic.Lambda
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
+ let module OT = struct type t = int let compare = Pervasives.compare end in
+ let module S = HTopoSort.Make (OT) in
+ let dep i =
+ let _,_,ty = List.find (fun (j,_,_) -> j=i) metasenv in
+ let metas = List.map fst (CicUtil.metas_of_term ty) in
+ HExtlib.list_uniq (List.sort Pervasives.compare metas)
+ in
+ let om =
+ S.topological_sort (List.map (fun (i,_,_) -> i) metasenv) dep
+ in
+ List.map (fun i -> List.find (fun (j,_,_) -> i=j) metasenv) om
in
+*)
let rec create_subst_from_metas_to_rels n = function
| [] -> []
| (metano, ctx, ty)::tl ->
in
aux t
in
+ let order_body_menv term body_metasenv =
+ let rec purge_lambdas = function
+ | Cic.Lambda (_,_,t) -> purge_lambdas t
+ | t -> t
+ in
+ let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+ let metas_that_saturate l =
+ List.fold_left
+ (fun (acc,n) t ->
+ let metas = CicUtil.metas_of_term t in
+ let metas = List.map fst metas in
+ let metas =
+ List.filter
+ (fun i -> List.for_all (fun (j,_) -> j<>i) acc)
+ metas
+ in
+ let metas = List.map (fun i -> i,n) metas in
+ metas @ acc, n+1)
+ ([],0) l
+ in
+ let l_c2 = skip_appl (purge_lambdas term) in
+ let l_c1 =
+ match HExtlib.list_last l_c2 with
+ | Cic.Appl l -> List.tl l
+ | _ -> assert false
+ in
+ (* i should cut off the laet elem of l_c2 *)
+ let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
+ List.sort
+ (fun (i,ctx1,ty1) (j,ctx1,ty1) ->
+ try List.assoc i meta2no - List.assoc j meta2no
+ with Not_found -> assert false)
+ body_metasenv
+ in
+ let namer l n =
+ let l = List.map (function Cic.Name s -> s | _ -> "A") l in
+ let l = List.fold_left
+ (fun acc s ->
+ let rec add' s =
+ if List.exists ((=) s) acc then add' (s^"'") else s
+ in
+ acc@[add' s])
+ [] l
+ in
+ let l = List.rev l in
+ Cic.Name (List.nth l (n-1))
+ 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 saturations_for_c1, names_c1 = count_saturations_needed c1_ty arity in
+ let saturations_for_c2, names_c2 = count_saturations_needed c2_ty 0 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 = mk_lambda_spline c (namer (names_c1 @ names_c2)) 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 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 body_metasenv = order_body_menv term body_metasenv in
+ debug_print(lazy("ORDERED_B_MENV: "^rt.RT.ppmetasenv [] body_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
let cleaned_ty =
FreshNamesGenerator.clean_dummy_dependent_types c_ty
in
- let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs) in
+ let obj = Cic.Constant ("xxxx",Some c,cleaned_ty,[],obj_attrs arity) in
obj,univ
;;
exception ManglingFailed of string
-let number_if_already_defined buri name =
+let number_if_already_defined buri name l =
+ let err () =
+ raise
+ (ManglingFailed
+ ("Unable to give an altenative name to " ^ buri ^ "/" ^ name ^ ".con"))
+ in
let rec aux n =
let suffix = if n > 0 then string_of_int n else "" in
- let uri = buri ^ "/" ^ name ^ suffix ^ ".con" in
- try
- let _ = Http_getter.resolve ~writable:true uri in
- if Http_getter.exists uri then
+ let suri = buri ^ "/" ^ name ^ suffix ^ ".con" in
+ let uri = UriManager.uri_of_string suri in
+ let retry () =
+ if n < 100 then
begin
- HLog.warn ("Uri " ^ uri ^ " already exists.");
- if n < 10 then aux (n+1) else
- raise
- (ManglingFailed
- ("Unable to give an altenative name to " ^
- buri ^ "/" ^ name ^ ".con"))
+ HLog.warn ("Uri " ^ suri ^ " already exists.");
+ aux (n+1)
end
else
- UriManager.uri_of_string uri
- with
- | Http_getter_types.Key_not_found _ -> UriManager.uri_of_string uri
- | Http_getter_types.Unresolvable_URI _ -> assert false
+ err ()
+ in
+ if List.exists (UriManager.eq uri) l then retry ()
+ else
+ try
+ let _ = Http_getter.resolve' ~writable:true uri in
+ if Http_getter.exists' uri then retry () else uri
+ with
+ | Http_getter_types.Key_not_found _ -> uri
+ | Http_getter_types.Unresolvable_URI _ -> assert false
in
aux 0
;;
let todo_list = filter_duplicates todo_list coercions in
try
let new_coercions =
- HExtlib.filter_map (
- fun (src, l , tgt) ->
+ List.fold_left (
+ fun acc (src, l , tgt) ->
try
(match l with
| [] -> assert false
| he :: tl ->
+ let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
let first_step =
Cic.Constant ("",
Some (CoercDb.term_of_carr (CoercDb.Uri he)),
- Cic.Sort Cic.Prop, [], obj_attrs)
+ Cic.Sort Cic.Prop, [], obj_attrs arity)
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
+ generate_composite_closure rt c
+ (CoercDb.term_of_carr (CoercDb.Uri coer)) univ arity
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl
in
let by = List.map UriManager.name_of_uri l in
let name = mangle name_tgt name_src by in
let buri = UriManager.buri_of_uri uri in
- let c_uri = number_if_already_defined buri name in
+ let c_uri =
+ number_if_already_defined buri name
+ (List.map (fun (_,_,u,_) -> u) acc)
+ in
let named_obj =
match o with
| Cic.Constant (_,bo,ty,vl,attrs) ->
Cic.Constant (name,bo,ty,vl,attrs)
| _ -> assert false
in
- Some ((src,tgt,c_uri,named_obj)))
- with UnableToCompose -> None
- ) todo_list
+ (src,tgt,c_uri,named_obj))::acc
+ with UnableToCompose -> acc
+ ) [] todo_list
in
new_coercions
with ManglingFailed s -> HLog.error s; []
(* $Id$ *)
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+type coerc_carr =
+ | Uri of UriManager.uri
+ | Sort of Cic.sort
+ | Term of Cic.term
+ | Fun of int
+;;
+
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed
| Term t ->
prerr_endline ("CoercDb.name_of_carr:" ^ CicPp.ppterm t);
"FixTheNameMangler"
+ | Fun i -> "FunClass_" ^ string_of_int i
+;;
let eq_carr src tgt =
match src, tgt with
(lazy ("Unsupported carr for coercions: " ^
CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
else raise EqCarrOnNonMetaClosed
+ | Fun _,Fun _ -> true (* only one Funclass? *)
+(* | Fun i,Fun j when i=j -> true *)
| _, _ -> false
+;;
let to_list () =
- !db
+ List.map (fun (s,t,l) -> s,t,List.map fst l) !db
+;;
let rec myfilter p = function
| [] -> []
| (s,t,l)::tl ->
- let l = List.filter (fun u -> not (p (s,t,u))) l in
+ let l =
+ HExtlib.filter_map
+ (fun (u,n) ->
+ if p (s,t,u) then
+ if n = 1 then
+ None
+ else
+ Some (u,n-1)
+ else
+ Some (u,n))
+ l
+ in
if l = [] then myfilter p tl else (s,t,l)::myfilter p tl
;;
let remove_coercion p = db := myfilter p !db;;
let find_coercion f =
- List.flatten
- (List.map
- (fun (_,_,x) -> x)
- (List.filter (fun (s,t,_) -> f (s,t)) !db))
+ List.map
+ fst
+ (List.flatten
+ (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db))
;;
let is_a_coercion u =
- List.exists (fun (_,_,xl) -> List.exists (UriManager.eq u) xl) !db
+ List.exists
+ (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl)
+ !db
;;
let get_carr uri =
try
let src, tgt, _ =
- List.find (fun (_,_,xl) -> List.exists (UriManager.eq uri) xl) !db
+ List.find
+ (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq uri x) xl)
+ !db
in
src, tgt
with Not_found -> assert false (* uri must be a coercion *)
let term_of_carr = function
| Uri u -> CicUtil.term_of_uri u
| Sort s -> Cic.Sort s
+ | Fun _ -> assert false
| Term _ -> assert false
;;
let where = List.filter (fun (s,t,_) -> f s t) !db in
let rest = List.filter (fun (s,t,_) -> not (f s t)) !db in
match where with
- | [] -> db := (src,tgt,[u]) :: !db
+ | [] -> db := (src,tgt,[u,1]) :: !db
| (src,tgt,l)::tl ->
assert (tl = []); (* not sure, this may be a feature *)
- db := (src,tgt,u::l)::tl @ rest
+ if List.exists (fun (x,_) -> UriManager.eq u x) l then
+ let l' = List.map
+ (fun (x,n) -> if UriManager.eq u x then (x,n+1) else (x,n))
+ l
+ in
+ db := (src,tgt,l')::tl @ rest
+ else
+ db := (src,tgt,(u,1)::l)::tl @ rest
+
;;
| Uri of UriManager.uri (* const, mutind, mutconstr *)
| Sort of Cic.sort (* Prop, Set, Type *)
| Term of Cic.term (* nothing supported *)
+ | Fun of int
+;;
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
(* searches a coercion fron src to tgt in the !coercions list *)
-let look_for_coercion src tgt =
+let look_for_coercion' src tgt =
let arity_of con =
try
let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in
None -> NoCoercion
| Some ul ->
let cl = List.map CicUtil.term_of_uri ul in
+ let funclass_arityl =
+ let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in
+ List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl
+ in
let arityl = List.map arity_of cl in
- let argsl = List.map (fun arity -> mk_implicits (arity - 1)) arityl in
+ let argsl =
+ List.map2
+ (fun arity fn_arity ->
+ mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl
+ in
let newtl =
List.map2
(fun args c ->
let look_for_coercion src tgt =
let src_uri = CoercDb.coerc_carr_of_term src in
let tgt_uri = CoercDb.coerc_carr_of_term tgt in
- look_for_coercion src_uri tgt_uri
+ look_for_coercion' src_uri tgt_uri
let is_a_coercion t =
try
let uri = CicUtil.uri_of_term t in
CoercDb.term_of_carr (fst (CoercDb.get_carr uri))
with Invalid_argument _ -> assert false (* t must be a coercion *)
-
-let target_of t =
+
+let is_a_coercion_to_funclass t =
try
let uri = CicUtil.uri_of_term t in
- CoercDb.term_of_carr (snd (CoercDb.get_carr uri))
- with Invalid_argument _ -> assert false (* t must be a coercion *)
-
+ match snd (CoercDb.get_carr uri) with
+ | CoercDb.Fun i -> Some i
+ | _ -> None
+ with Invalid_argument _ -> None
+
let generate_dot_file () =
let module Pp = GraphvizPp.Dot in
let buf = Buffer.create 10240 in
l;
Pp.trailer fmt;
Buffer.contents buf
+;;
+
+let is_composite t =
+ try
+ let uri =
+ match t with
+ | Cic.Appl (he::_) -> CicUtil.uri_of_term he
+ | _ -> CicUtil.uri_of_term t
+ in
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | Cic.Constant (_,_, _, _, attrs),_ ->
+ List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
+ | _ -> false
+ with Invalid_argument _ -> false
+;;
(* EOF *)
val look_for_coercion :
Cic.term -> Cic.term -> coercion_search_result
+val look_for_coercion' :
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
+
val is_a_coercion: Cic.term -> bool
+val is_a_coercion_to_funclass: Cic.term -> int option
+
+(* checks if term is a constant or
+ * a constant applyed that is marked with (`Class `Coercion) *)
+val is_composite: Cic.term -> bool
+
+
val source_of: Cic.term -> Cic.term
-val target_of: Cic.term -> Cic.term
val generate_dot_file: unit -> string
UriManager.UriHashtbl.clear coercion_hashtbl;
CoercDb.remove_coercion (fun (_,_,u1) -> true)
-let add_coercion ~add_composites refinement_toolkit uri =
+let add_coercion ~add_composites refinement_toolkit uri arity =
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
* should we saturate it with metas in case we insert it?
*
*)
- let extract_last_two_p ty =
+ let spline2list ty =
let rec aux = function
- | Cic.Prod( _, _, ((Cic.Prod _) as t)) ->
- aux t
- | Cic.Prod( _, src, tgt) -> src, tgt
- | _ -> assert false
+ | Cic.Prod( _, src, tgt) -> src::aux tgt
+ | t -> [t]
in
aux ty
in
+ let src_carr, tgt_carr =
+ let list_remove_from_tail n l =
+ let rec aux n = function
+ | hd::tl when n > 0 -> aux (n-1) tl
+ | l when n = 0 -> l
+ | _ -> assert false
+ in
+ aux n (List.rev l)
+ in
+ let types = spline2list coer_ty in
+ match arity, list_remove_from_tail arity types with
+ | 0,tgt::src::_ ->
+ (* if ~delta is true, it is impossible to define an identity coercion *)
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
+ | n,_::src::_ ->
+ CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+ CoercDb.Fun arity
+ | _ -> assert false
+ in
let already_in =
List.exists
- (fun (_,_,ul) -> List.exists (fun u -> UriManager.eq u uri) ul)
+ (fun (s,t,ul) ->
+ List.exists
+ (fun u ->
+ UriManager.eq u uri &&
+ CoercDb.eq_carr s src_carr &&
+ CoercDb.eq_carr t tgt_carr)
+ ul)
(CoercDb.to_list ())
in
- let ty_src, ty_tgt = extract_last_two_p coer_ty 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
if not add_composites then
(CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
else
let generate_projections refinement_toolkit uri fields =
let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections =
+ CicRecord.projections_of uri
+ (List.map (fun (x,_,_) -> x) fields)
+ in
try
List.iter2
- (fun (uri, name, bo) (_name, coercion) ->
+ (fun (uri, name, bo) (_name, coercion, arity) ->
try
let ty, ugraph =
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
if coercion then
begin
(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
- let x = add_coercion ~add_composites:true refinement_toolkit uri
+ let x =
+ add_coercion ~add_composites:true refinement_toolkit uri arity
in
(*prerr_endline ("are: ");
List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
(* The list of added objects is returned. *)
val add_coercion:
add_composites:bool ->
- RefinementTool.kit -> UriManager.uri ->
+ RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
UriManager.uri list
(* inverse of add_coercion, removes both the eventually created composite *)
let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
(metadata: MetadataTypes.constr list)
=
- let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables
- in
+ let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
if (metadata = []) && concl_card = None && full_card = None then
- failwith "MetadataQuery.at_least: no constraints given";
- let (n,from,where) =
- List.fold_left (add_constraint ~tables) (0,[],[]) metadata
- in
- let (n,from,where) =
- add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
- in
- exec ~dbd ?rating (n,from,where)
+ begin
+ HLog.warn "MetadataConstraints.at_least: no constraints given";
+ []
+ end
+ else
+ let (n,from,where) =
+ List.fold_left (add_constraint ~tables) (0,[],[]) metadata
+ in
+ let (n,from,where) =
+ add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
+ in
+ exec ~dbd ?rating (n,from,where)
+;;
let at_least
~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
(*eprintf "Node '%s' not found.\n" (UriManager.string_of_uri uri);*)
assert false
in
- Pp.header ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
+ Pp.header ~graph_type:"strict digraph" ~graph_attrs:["rankdir", "LR"] ~node_attrs:global_node_attrs fmt;
let rec aux =
function
| [] -> ()
=
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
+ (* occur check *)
+ let occur i t =
+ let m = CicUtil.metas_of_term t in
+ List.exists (fun (j,_) -> i=j) m
+ in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let _,_ = (* TASSI: FIXME *)
+ if occur metano term then
+ raise
+ (ProofEngineTypes.Fail (lazy
+ "You can't letin a term containing the current goal"));
+ let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmeta = new_meta_of_proof ~proof in
let fresh_name =
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Aug 31 14:46:00 CEST 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
let png_flags = "-Tpng"
let map_flags = "-Tcmapx"
-let tred_cmd = "tred" (* graphviz transitive reduction filter *)
let tempfile () = Filename.temp_file "matita_" ""
class type graphviz_widget =
object
- method load_graph_from_file: string -> unit
+ method load_graph_from_file: ?gviz_cmd:string -> string -> unit
method connect_href:
(GdkEvent.Button.t -> (string * string) list -> unit) -> unit
method center_on_href: string -> unit
method as_viewport: GBin.viewport
end
-class graphviz_impl ?packing gviz_cmd =
+class graphviz_impl ?packing () =
let viewport = GBin.viewport ?packing () in
- let mk_gviz_cmd flags src_fname dest_fname =
- sprintf "cat %s | %s | %s %s > %s" src_fname tred_cmd gviz_cmd flags
+ let mk_gviz_cmd gviz_cmd flags src_fname dest_fname =
+ sprintf "cat %s | %s %s > %s" src_fname gviz_cmd flags
dest_fname in
let image =
GMisc.image ~packing:viewport#add ~xalign:0. ~yalign:0. ~xpad:0 ~ypad:0 ()
(try href_cb button (self#find_href x y) with Not_found -> ());
false))
- method load_graph_from_file fname =
+ method load_graph_from_file ?(gviz_cmd = "dot") fname =
let tmp_png = tempfile () in
- let rc = Sys.command (mk_gviz_cmd png_flags fname tmp_png) in
+ let rc = Sys.command (mk_gviz_cmd gviz_cmd png_flags fname tmp_png) in
if rc <> 0 then
eprintf
("Graphviz command failed (exit code: %d) on the following graph:\n"
image#set_file tmp_png;
HExtlib.safe_remove tmp_png;
let tmp_map = tempfile () in
- ignore (Sys.command (mk_gviz_cmd map_flags fname tmp_map));
+ ignore (Sys.command (mk_gviz_cmd gviz_cmd map_flags fname tmp_map));
self#load_map tmp_map;
HExtlib.safe_remove tmp_map
end
-let factory cmd ?packing () =
- (new graphviz_impl ?packing cmd :> graphviz_widget)
-
-let gDot = factory "dot"
-let gNeato = factory "neato"
-let gTwopi = factory "twopi"
-let gCirco = factory "circo"
-let gFdp = factory "fdp"
+let graphviz ?packing () =
+ (new graphviz_impl ?packing () :> graphviz_widget)
* GtkImage widget
* 2) render it to a (HTML) map, internalizing its data.
* Remember that map entries are generated only for nodes, (edges, ...)
- * that have an "href" (or "URL", a synonym) attribute *)
- method load_graph_from_file: string -> unit
+ * that have an "href" (or "URL", a synonym) attribute
+ * Interesting values for gviz_cmd are:
+ * 'neato'
+ * 'dot'
+ * 'tred | dot'
+ *)
+ method load_graph_from_file: ?gviz_cmd:string -> string -> unit
(** Callback invoked when a click on a node listed in the map is received.
* @param gdk's button event
(** {2 Constructors} *)
-val gDot: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gNeato: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gTwopi: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gCirco: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
-val gFdp: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
+val graphviz: ?packing:(GObj.widget -> unit) -> unit -> graphviz_widget
cic:/Coq/Init/Logic/sym_eq.con
cic:/Coq/Init/Logic/trans_eq.con
cic:/Coq/Init/Logic/eq_ind.con
- cic:/Coq/Init/Logic/eq_ind_r.con
- cic:/Coq/Init/Logic/f_equal.con
- cic:/Coq/Init/Logic/f_equal1.con.
+ cic:/Coq/Init/Logic/eq_ind_r.con
+ cic:/Coq/Init/Logic/f_equal.con
+ cic:/matita/legacy/coq/f_equal1.con.
default "true"
cic:/Coq/Init/Logic/True.ind.
interpretation "Coq's natural 'not less or equal than'"
'nleq x y = (cic:/Coq/Init/Logic/not.con
(cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y)).
-
+
+theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A.
+ x = y \to (f y) = (f x).
+ intros.
+ symmetry.
+ apply cic:/Coq/Init/Logic/f_equal.con.
+ assumption.
+qed.
(* aliases *)
(* FG: This is because "and" is a reserved keyword of the parser *)
alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
-(* theorems *)
-
-theorem f_equal1 :
- \forall A,B:Type. \forall f:A \to B. \forall x,y:A.
- x = y \to f y = f x.
- intros.elim H.reflexivity.
-qed.
-
intros. elim (sym_eq ? ? ? H1).assumption.
qed.
+theorem eq_f: \forall A,B:Type.\forall f:A\to B.
+\forall x,y:A. x=y \to f x = f y.
+intros.elim H.reflexivity.
+qed.
+
+coercion cic:/matita/logic/equality/sym_eq.con.
+coercion cic:/matita/logic/equality/eq_f.con.
+
default "equality"
cic:/matita/logic/equality/eq.ind
cic:/matita/logic/equality/sym_eq.con
cic:/matita/logic/equality/eq_ind.con
cic:/matita/logic/equality/eq_elim_r.con
cic:/matita/logic/equality/eq_f.con
- cic:/matita/logic/equality/eq_f1.con. (* \x.sym (eq_f x) *)
-
+ cic:/matita/logic/equality/eq_OF_eq.con. (* \x.sym (eq_f x) *)
-theorem eq_f: \forall A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f x = f y.
-intros.elim H.reflexivity.
-qed.
-
-theorem eq_f1: \forall A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f y = f x.
-intros.elim H.reflexivity.
-qed.
-
theorem eq_f2: \forall A,B,C:Type.\forall f:A\to B \to C.
\forall x1,x2:A. \forall y1,y2:B.
x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
let gui = get_gui () in
let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
- let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in
+ let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
let combo,_ = GEdit.combo_box_text ~strings:queries () in
let activate_combo_query input q =
let fmt = Format.formatter_of_out_channel oc in
MetadataDeps.DepGraph.render fmt gviz_graph;
close_out oc;
- gviz#load_graph_from_file tmpfile;
+ gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
(match center_on with
| None -> ()
| Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
(**************************************************************************)
set "baseuri" "cic:/matita/tests/coercions/".
-include "nat/nat.ma".
+
+include "nat/compare.ma".
+include "datatypes/bool.ma".
inductive pos: Set \def
| one : pos
| next : pos \to pos.
-inductive nat:Set \def
-| O : nat
-| S : nat \to nat.
-
inductive int: Set \def
| positive: nat \to int
| negative : nat \to int.
\forall f:int \to int. pos \to int
\def
\lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
-
-coercion cic:/matita/logic/equality/eq_f.con.
-coercion cic:/matita/logic/equality/eq_f1.con.
-variant xxx : ? \def eq_f.
-coercion cic:/matita/tests/coercions/xxx.con.
theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
intros.
variant pos2nat' : ? \def pos2nat.
-coercion cic:/matita/tests/coercions/xxx.con.
-
inductive initial: Set \def iii : initial.
definition i2pos: ? \def \lambda x:initial.one.
coercion cic:/matita/tests/coercions/pos2nat'.con.
+inductive listn (A:Type) : nat \to Type \def
+ | Nil : listn A O
+ | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n).
+
+definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def
+ \lambda A,b,a,c.
+ match b with
+ [ true \Rightarrow a
+ | false \Rightarrow c].
+
+let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def
+ match l with
+ [ Nil \Rightarrow dummy
+ | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)].
+
+definition listn2function:
+ \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A
+\def
+ \lambda A,dummy,n,l,m.ith A n m dummy l.
+
+definition natlist2map: ? \def listn2function nat O.
+
+coercion cic:/matita/tests/coercions/natlist2map.con 1.
+definition map: \forall n:nat.\forall l:listn nat n. nat \to nat \def
+ \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m.
+
+definition church: nat \to nat \to nat \def times.
+
+coercion cic:/matita/tests/coercions/church.con 1.
+
+definition mapmult: \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def
+ \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o.
+
+
+
\ No newline at end of file
projects / helm.git / commitdiff