let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
let uri =
- match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) ->
- (match baseuri with
- | Some baseuri ->
- Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
- | None -> raise BaseUriNotSetYet)
- | CicNotationPt.Inductive _ -> assert false
- | CicNotationPt.Theorem _ -> None in
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Inductive _ -> assert false
+ in
+ UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ in
let try_new cic =
(NCicLibrary.clear_cache ();
NCicEnvironment.invalidate ();
OCic2NCic.clear ();
- (match obj with
- CicNotationPt.Theorem (_,_,ty,_) ->
let graph =
match cic with
| Cic.CurrentProof (_,metasenv, _, ty,_,_) ->
let time = Unix.gettimeofday () in
(try
(match
- NCicDisambiguate.disambiguate_term
+ NCicDisambiguate.disambiguate_obj
~lookup_in_library:lookup_in_library
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
~coercion_db:(NCicCoercion.db ())
- ~context:[] ~metasenv:[] ~subst:[]
~aliases:lexicon_status.LexiconEngine.aliases
~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
- (text,prefix_len,ty)
+ (text,prefix_len,obj)
with
- | [_,metasenv,subst,ty],_ ->
+ | [_,_,_,obj],_ ->
let time = Unix.gettimeofday () -. time in
+(* NCicTypeChecker.typecheck_obj obj; *)
prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
+(*
+ let obj =
+ let u,i,m,_,o = obj in
+ u,i,m,[],o
+ in
+*)
+ prerr_endline (NCicPp.ppobj obj)
| _ ->
prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
with
| MultiPassDisambiguator.DisambiguationError (_,s) ->
- prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE:\n" ^
+ prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
+ ^UriManager.string_of_uri uri^
+ "):\n" ^
String.concat "\n"
(List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
(* | exn -> prerr_endline (Printexc.to_string exn) *)
)
- | _ -> ())
)
in
-(*
try
- let time = Unix.gettimeofday () in
-*)
+(* let time = Unix.gettimeofday () in *)
let (diff, metasenv, _, cic, _) =
~mk_implicit
~description_of_alias:LexiconAst.description_of_alias
~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~uri:(Some uri)
(text,prefix_len,obj)) in
(*
let time = Unix.gettimeofday () -. time in
- prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
- try_new cic;
+ prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
+ UriManager.string_of_uri uri ^"): " ^ string_of_float time);
*)
-
+(* try_new cic; *)
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status, metasenv, cic
-
-(*
with
| Sys.Break as exn -> raise exn
| exn ->
- try_new (Cic.InductiveDefinition ([],[],0,[]));
raise exn
-*)
-
;;
Disambiguate.Ko loc_msg
;;
+let refine_obj
+ ~coercion_db metasenv subst context uri
+ ~use_coercions obj ugraph ~localization_tbl
+=
+ assert (metasenv=[]);
+ assert (subst=[]);
+ let localise t =
+ try NCicUntrusted.NCicHash.find localization_tbl t
+ with Not_found ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+ (*assert false*)HExtlib.dummy_floc
+ in
+ try
+ let obj =
+ NCicRefiner.typeof_obj
+ (NCicUnifHint.db ())
+ ~look_for_coercion:(
+ if use_coercions then
+ NCicCoercion.look_for_coercion coercion_db
+ else (fun _ _ _ _ _ -> []))
+ obj ~localise
+ in
+ Disambiguate.Ok (obj, [], [], ())
+ with
+ | NCicRefiner.Uncertain loc_msg ->
+ debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force loc_msg) ^ "] " ^
+ NCicPp.ppobj obj)) ;
+ Disambiguate.Uncertain loc_msg
+ | NCicRefiner.RefineFailure loc_msg ->
+ debug_print (lazy (sprintf "PRUNED:\nobj: %s\nmessage: %s"
+ (NCicPp.ppobj obj) (snd(Lazy.force loc_msg))));
+ Disambiguate.Ko loc_msg
+;;
+
+
(* TODO move it to Cic *)
let find_in_context name context =
let rec aux acc = function
| `Axiom -> `Fact
;;
-(*
-let interpretate_obj ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
- ~localization_tbl
+let ncic_name_of_ident = function
+ | Ast.Ident (name, None) -> name
+ | _ -> assert false
+;;
+
+let interpretate_obj
+(* ?(create_dummy_ids=false) *)
+ ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice
=
assert (context = []);
assert (is_path = false);
- let interpretate_term ?(obj_context=[]) =
+ let interpretate_term ~obj_context =
interpretate_term ~mk_choice ~localization_tbl ~obj_context in
- let interpretate_term_option ?(obj_context=[]) =
+ let interpretate_term_option ~obj_context =
interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in
+ let uri = match uri with | None -> assert false | Some u -> u in
match obj with
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
- let attrs = `Provided, new_flavour_of_flavour flavour in
- let ty' = interpretate_term [] env None false ty in
+ let ty' =
+ interpretate_term
+ ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty
+ in
let height = (* XXX calculate *) 0 in
uri, height, [], [],
(match bo,flavour with
- None,`Axiom ->
- NCic.Constant (name,None,ty',attrs)
- | Some bo,`Axiom -> assert false
+ | None,`Axiom ->
+ let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ NCic.Constant ([],name,None,ty',attrs)
+ | Some _,`Axiom -> assert false
| None,_ ->
- NCic.Constant (name,NCic.Implicit None,ty',attrs)
+ let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs)
| Some bo,_ ->
match bo with
| CicNotationPt.LetRec (kind, defs, _) ->
let inductive = kind = `Inductive in
- let obj_context =
- List.split
- (List.fold_left
- (fun (i,acc) (_,(name,_),_,k) ->
- ((name, NReference.reference_of_spec uri
- (if inductive then NReference.Fix (i,k,0)
- else NReference.CoFix i)) :: acc)
- (0,[]) defs))
+ let _,obj_context =
+ List.fold_left
+ (fun (i,acc) (_,(name,_),_,k) ->
+ (i+1,
+ (ncic_name_of_ident name, NReference.reference_of_spec uri
+ (if inductive then NReference.Fix (i,k,0)
+ else NReference.CoFix i)) :: acc))
+ (0,[]) defs
in
let inductiveFuns =
List.map
CicNotationPt.Binder (kind, var, t)) params t
in
let cic_body =
- interpretate_term ~context ~env ~uri:None ~is_path:false
+ interpretate_term
+ ~obj_context ~context ~env ~uri:None ~is_path:false
(add_binders `Lambda body)
in
let cic_type =
- interpretate_term_option ~context ~env ~uri:None
- ~is_path:false `Type
+ interpretate_term_option
+ ~obj_context:[]
+ ~context ~env ~uri:None ~is_path:false `Type
(HExtlib.map_option (add_binders `Pi) typ)
in
- (name, decr_idx, cic_type, cic_body))
+ ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
defs
in
+ let attrs = `Provided, new_flavour_of_flavour flavour in
NCic.Fixpoint (inductive,inductiveFuns,attrs)
| bo ->
let bo =
- interpretate_term ~context:[] ~env ~uri:None ~is_path:false bo
+ interpretate_term
+ ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
in
- NCic.Constant (name,Some bo,ty',attrs))
- | _ -> assert false
+ let attrs = `Provided, new_flavour_of_flavour flavour, `Regular in
+ NCic.Constant ([],name,Some bo,ty',attrs))
+ | _ -> raise (MultiPassDisambiguator.DisambiguationError (0, []))
(*
| CicNotationPt.Inductive (params,tyl) ->
let uri = match uri with Some uri -> uri | None -> assert false in
(tyl,[],List.length params,[`Class (`Record field_names)])
*)
;;
-*)
let disambiguate_term ~context ~metasenv ~subst ?goal
~mk_implicit ~description_of_alias ~mk_choice
List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
;;
+let disambiguate_obj
+ ~mk_implicit ~description_of_alias ~mk_choice
+ ~aliases ~universe ~coercion_db ~lookup_in_library ~uri
+ (text,prefix_len,obj)
+ =
+ let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
+ let hint = (fun x y -> y), (fun x -> x) in
+ let res,b =
+ MultiPassDisambiguator.disambiguate_thing
+ ~freshen_thing:CicNotationUtil.freshen_obj
+ ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
+ ~mk_implicit ~description_of_alias
+ ~string_context_of_context:(List.map (fun (x,_) -> Some x))
+ ~universe
+ ~uri:(Some uri)
+ ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
+ ~passes:(MultiPassDisambiguator.passes ())
+ ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+ ~interpretate_thing:(interpretate_obj ~mk_choice)
+ ~refine_thing:(refine_obj ~coercion_db)
+ (text,prefix_len,obj)
+ ~mk_localization_tbl ~hint
+ in
+ List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+;;
let _ =
let mk_type n =
if n = 0 then
NCic.term) list *
bool
+val disambiguate_obj :
+ mk_implicit:(bool -> 'a) ->
+ description_of_alias:('a -> string) ->
+ mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) ->
+ aliases:'a DisambiguateTypes.Environment.t ->
+ universe:'a list DisambiguateTypes.Environment.t option ->
+ coercion_db:NCicCoercion.db ->
+ lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
+ DisambiguateTypes.input_or_locate_uri_type ->
+ DisambiguateTypes.Environment.key -> 'a list) ->
+ uri:NUri.uri ->
+ string * int * CicNotationPt.term CicNotationPt.obj ->
+ ((DisambiguateTypes.Environment.key * 'a) list * NCic.metasenv *
+ NCic.substitution * NCic.obj)
+ list * bool
+
aux false
;;
-let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
+let rec head_beta_reduce ~delta ~upto ~subst t l =
match upto, t, l with
| 0, C.Appl l1, _ -> C.Appl (l1 @ l)
| 0, t, [] -> t
| 0, t, _ -> C.Appl (t::l)
- | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto hd (tl @ l)
+ | _, C.Meta (n,ctx), _ ->
+ (try
+ let _,_, term,_ = NCicUtils.lookup_subst n subst in
+ head_beta_reduce ~delta ~upto ~subst
+ (NCicSubstitution.subst_meta ctx term) l
+ with NCicUtils.Subst_not_found _ -> if l = [] then t else C.Appl (t::l))
+ | _, C.Appl (hd::tl), _ -> head_beta_reduce ~delta ~upto ~subst hd (tl @ l)
| _, C.Lambda(_,_,bo), arg::tl ->
let bo = NCicSubstitution.subst arg bo in
- head_beta_reduce ~delta ~upto:(upto - 1) bo tl
+ head_beta_reduce ~delta ~upto:(upto - 1) ~subst bo tl
| _, C.Const (Ref.Ref (_, Ref.Def height) as re), _
when delta <= height ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
- head_beta_reduce ~upto ~delta bo l
+ head_beta_reduce ~upto ~delta ~subst bo l
| _, t, [] -> t
| _, t, _ -> C.Appl (t::l)
;;
-let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
+let head_beta_reduce ?(delta=max_int) ?(upto= -1) ?(subst=[]) t =
+ head_beta_reduce ~delta ~upto ~subst t []
+;;
type stack_item = RS.stack_term
type environment_item = RS.env_term
let from_stack = RS.from_stack
let unwind = R.unwind
+let _ =
+ NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t)
+;;
+
+
(* vim:set foldmethod=marker: *)
(* performs head beta/(delta)/cast reduction; the default is to not perform
delta reduction; if provided, ~upto is the maximum number of beta redexes
reduced *)
-val head_beta_reduce: ?delta:int -> ?upto:int -> NCic.term -> NCic.term
+val head_beta_reduce:
+ ?delta:int -> ?upto:int -> ?subst:NCic.substitution -> NCic.term -> NCic.term
type stack_item
type environment_item
| C.Rel _ as t -> a,t
| C.Appl [] | C.Appl [_] -> assert false
| C.Appl l as orig ->
+ let fire_beta, upto =
+ match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
+ in
let a,l1 =
(* sharing fold? *)
List.fold_right
(fun t (a,l) -> let a,t = f k a t in a, t :: l)
l (a,[])
in
- a, if l1 == l then orig else (match l1 with
- | C.Appl l :: tl -> C.Appl (l@tl)
- | _ -> C.Appl l1)
+ a, if l1 == l then orig else
+ let t =
+ match l1 with
+ | C.Appl l :: tl -> C.Appl (l@tl)
+ | _ -> C.Appl l1
+ in
+ if fire_beta then NCicReduction.head_beta_reduce ~upto t
+ else t
| C.Prod (n,s,t) as orig ->
let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
exception Subst_not_found of int
exception Meta_not_found of int
+let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);;
+let set_head_beta_reduce = (:=) head_beta_reduce;;
+
let expand_local_context = function
| C.Irl len ->
let rec aux acc = function
| C.Rel _ as t -> t
| C.Appl [] | C.Appl [_] -> assert false
| C.Appl l as orig ->
- (match HExtlib.sharing_map (f k) l with
+ let fire_beta, upto =
+ match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
+ in
+ let l1 = HExtlib.sharing_map (f k) l in
+ if l == l1 then orig else
+ let t =
+ match l1 with
| C.Appl l :: tl -> C.Appl (l@tl)
- | l1 when l == l1 -> orig
- | l1 -> C.Appl l1)
+ | l1 -> C.Appl l1
+ in
+ if fire_beta then !head_beta_reduce ~upto t
+ else t
| C.Prod (n,s,t) as orig ->
let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
val map:
(NCic.hypothesis -> 'k -> 'k) -> 'k ->
('k -> NCic.term -> NCic.term) -> NCic.term -> NCic.term
+
+val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit
+
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-(*
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
-*)
-
let pp _ = ();;
| _ ->
pp (lazy (
(NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^
- (NCicPp.ppterm ~metasenv ~subst ~context expty)));
+ (NCicPp.ppterm ~metasenv ~subst:[] ~context expty)));
try
let metasenv, subst =
NCicUnification.unify hdb metasenv subst context infty expty
fun t as orig ->
(*D*)inside 'R'; try let rc =
pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t));
- pp (lazy (NCicPp.ppmetasenv ~subst metasenv));
+ pp (lazy (if expty = None then "NONE" else "SOME"));
+ if (List.exists (fun (i,_) -> i=29) subst) then
+ pp (lazy (NCicPp.ppsubst ~metasenv subst));
let metasenv, subst, t, infty =
match t with
| C.Rel n ->
let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in
metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty
| C.Appl ((he as orig_he)::(_::_ as args)) ->
+ let upto =
+ match orig_he with C.Meta _ -> List.length args | _ -> 0
+ in
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
- eat_prods hdb ~localise ~look_for_coercion
- metasenv subst context orig_he he ty_he args
+ let metasenv, subst, t, ty =
+ eat_prods hdb ~localise ~look_for_coercion
+ metasenv subst context orig_he he ty_he args
+ in
+ let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in
+ metasenv, subst, t, ty
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
outtype,(term as orig_term),pl) as orig ->
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
+ let parameters, arguments = HExtlib.split_nth leftno args in
+ let outtype =
+ match outtype with
+ | C.Implicit _ as ot ->
+ let rec aux = function
+ | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot)
+ | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl)
+ in
+ aux arguments
+ | _ -> outtype
+ in
let metasenv, subst, outtype, outsort =
typeof_aux metasenv subst context None outtype in
- let parameters, arguments = HExtlib.split_nth leftno args in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let ind =
if parameters = [] then C.Const r
if List.length pl <> constructorsno then
raise (RefineFailure (lazy (localise orig,
"Wrong number of cases in a match")));
+(*
+ let metasenv, subst =
+ match expty with
+ | None -> metasenv, subst
+ | Some expty ->
+ NCicUnification.unify hdb metasenv subst context resty expty
+ in
+*)
let _, metasenv, subst, pl_rev =
List.fold_left
(fun (j, metasenv, subst, branches) p ->
j+1, metasenv, subst, p :: branches)
(1, metasenv, subst, []) pl
in
- metasenv, subst,
- C.Match (r, outtype, term, List.rev pl_rev),
- NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
- | C.Match _ as orig ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig);
- assert false
+ let resty = C.Appl (outtype::arguments@[term]) in
+ let resty = NCicReduction.head_beta_reduce ~subst resty in
+ metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
+ | C.Match _ as orig -> assert false
in
pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
NCicPp.ppterm ~metasenv ~subst ~context infty ));
NCicSubstitution.subst (NCic.Meta (-1,(0,NCic.Irl 0))) t
| _ -> assert false)
pair' context in
+(*
prerr_endline ("INDEXING: " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
+*)
DB.index hdb src data
;;
;;
let db () =
- let combine f cmp l1 l2 =
+ let combine f l =
List.flatten
- (List.map
- (fun u1 ->
- HExtlib.filter_map
- (fun u2 -> if cmp u1 u2 then None else Some (f u1 u2)) l2)
- l1)
+ (let rec aux = function
+ | u1 :: tl -> List.map (f u1) tl :: aux tl
+ | [] -> []
+ in aux l)
in
let mk_hint (u1,_,_) (u2,_,_) =
let l = OCic2NCic.convert_obj u1
let r = OCic2NCic.convert_obj u2
(fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph u2)) in
match List.hd l,List.hd r with
- | (_,_,_,_,NCic.Constant (_,_,Some l,_,_)),
- (_,_,_,_,NCic.Constant (_,_,Some r,_,_)) ->
+ | (_,h1,_,_,NCic.Constant (_,_,Some l,_,_)),
+ (_,h2,_,_,NCic.Constant (_,_,Some r,_,_)) ->
let rec aux ctx t1 t2 =
match t1, t2 with
| NCic.Lambda (n1,s1,b1), NCic.Lambda(_,s2,b2) ->
if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx s1 s2
then aux ((n1, NCic.Decl s1) :: ctx) b1 b2
- else None
+ else []
| b1,b2 ->
if NCicReduction.are_convertible ~subst:[] ~metasenv:[] ctx b1 b2
then begin
~context:ctx b1 ^ " === " ^ NCicPp.ppterm ~metasenv:[]
~subst:[] ~context:ctx b2);
*)
- Some (ctx,b1,b2)
- end else None
+ let rec mk_rels =
+ function 0 -> [] | n -> NCic.Rel n :: mk_rels (n-1)
+ in
+ let n1 =
+ NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
+ u1 (NReference.Def h1)) :: mk_rels (List.length ctx))
+ in
+ let n2 =
+ NCic.Appl (NCic.Const(OCic2NCic.reference_of_ouri
+ u2 (NReference.Def h2)) :: mk_rels (List.length ctx))
+ in
+ [ctx,b1,b2; ctx,b1,n2; ctx,n1,b2; ctx,n1,n2]
+ end else []
in
aux [] l r
- | _ -> None
+ | _ -> []
in
let hints =
List.fold_left
(fun acc (_,_,l) ->
acc @
if List.length l > 1 then
- combine mk_hint (fun (u1,_,_) (u2,_,_) -> UriManager.eq u1 u2) l l
+ combine mk_hint l
else [])
[] (CoercDb.to_list ())
in
List.fold_left
(fun db -> function
- | None -> db
- | Some (ctx,b1,b2) -> index_hint db ctx b1 b2)
- !user_db hints
+ | (ctx,b1,b2) -> index_hint db ctx b1 b2)
+ !user_db (List.flatten hints)
;;
false,NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0)
(HintSet.elements candidates2)
in
+ let rc =
List.map
(function
| (true,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t1, t2
| (false,(NCic.Appl [_; t1; t2],metasenv,_)) -> metasenv, t2, t1
| _ -> assert false)
(candidates1 @ candidates2)
+ in
+(*
+ List.iter
+ (fun (metasenv, t1, t2) ->
+ prerr_endline
+ ("CAND: "^NCicPp.ppterm ~metasenv ~subst ~context t1 ^
+ " == "^NCicPp.ppterm ~metasenv ~subst ~context t2))
+ rc;
+*)
+ rc
;;
" with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2));
;;
-let mk_appl hd tl =
- match hd with
- | NCic.Appl l -> NCic.Appl (l@tl)
- | _ -> NCic.Appl (hd :: tl)
+let mk_appl ~upto hd tl =
+ NCicReduction.head_beta_reduce ~upto
+ (match hd with
+ | NCic.Appl l -> NCic.Appl (l@tl)
+ | _ -> NCic.Appl (hd :: tl))
;;
let flexible l =
let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-(*
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
-*)
let pp _ = ();;
let term = NCicSubstitution.subst_meta lc term in
unify hdb test_eq_only metasenv subst context term t
with NCicUtils.Subst_not_found _->
- instantiate hdb test_eq_only metasenv subst context n lc t false)
+ instantiate hdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) false)
| t, C.Meta (n,lc) ->
(try
let term = NCicSubstitution.subst_meta lc term in
unify hdb test_eq_only metasenv subst context t term
with NCicUtils.Subst_not_found _->
- instantiate hdb test_eq_only metasenv subst context n lc t true)
+ instantiate hdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) true)
| NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- unify hdb test_eq_only metasenv subst context (mk_appl term args) t2
+ unify hdb test_eq_only metasenv subst context
+ (mk_appl ~upto:(List.length args) term args) t2
| _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- unify hdb test_eq_only metasenv subst context t1 (mk_appl term args)
+ unify hdb test_eq_only metasenv subst context t1
+ (mk_appl ~upto:(List.length args) term args)
| NCic.Appl (NCic.Meta (i,_)::_ as l1),
NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
projects / helm.git / commitdiff