+(* generic function lifting splitting from type T to type (T list) *)
+let rec list_split item_split ctx pre post =
+ match post with
+ | [] -> []
+ | x :: post' ->
+ (item_split (fun v1 -> ctx (pre@v1::post')) x)@
+ list_split item_split ctx (pre@[x]) post'
+;;
+
+(* splits a 'term capture_variable *)
+let var_split ctx = function
+ | (_,None) -> []
+ | (v,Some ty) -> [(fun x -> ctx (v,Some x)),ty]
+;;
+
+let ity_split ctx (n,isind,ty,cl) =
+ [(fun x -> ctx (n,isind,x,cl)),ty]@
+ list_split (fun ctx0 (v,ty) -> [(fun x -> ctx0 (v,x)),ty])
+ (fun x -> ctx (n,isind,ty,x)) [] cl
+;;
+
+let field_split ctx (n,ty,b,m) =
+ [(fun x -> ctx (n,x,b,m)),ty]
+;;
+
+(* splits a defn. in a mutual LetRec block *)
+let letrecaux_split ctx (args,f,bo,n) =
+ list_split var_split (fun x -> ctx (x,f,bo,n)) [] args@
+ var_split (fun x -> ctx (args,x,bo,n)) f@
+ [(fun x -> ctx (args,f,x,n)),bo]
+;;
+
+(* splits a pattern (for case analysis) *)
+let pattern_split ctx = function
+ | Ast.Wildcard -> []
+ | Ast.Pattern (s,href,pl) ->
+ let rec auxpatt pre = function
+ | [] -> []
+ | (x,Some y as x')::post' ->
+ ((fun v -> ctx (Ast.Pattern (s,href,pre@(x,Some v)::post'))),y)
+ ::auxpatt (pre@[x']) post'
+ | (x,None as x')::post' -> auxpatt (pre@[x']) post'
+ in auxpatt [] pl
+;;
+
+ (* this function is used to get the children of a given node, together with
+ * their context
+ * contexts are expressed in the form of functions Ast -> Ast *)
+(* split : ('term -> 'a) -> 'term -> (('term -> 'a) * 'term) list *)
+let rec split ctx = function
+ | Ast.AttributedTerm (attr,t) ->
+ [(fun x -> ctx (Ast.AttributedTerm(attr,x))),t]
+ | Ast.Appl tl -> list_split split (fun x -> ctx (Ast.Appl x)) [] tl
+ | Ast.Binder (k,((n,None) as n'),body) ->
+ [ (fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Binder (k,((n,Some ty) as n'),body) ->
+ [(fun v -> ctx (Ast.Binder (k,(n,Some v),body))), ty
+ ;(fun v -> ctx (Ast.Binder (k,n',v))),body]
+ | Ast.Case (t,ity,outty,pl) ->
+ let outty_split = match outty with
+ | None -> []
+ | Some u -> [(fun x -> ctx (Ast.Case (t,ity,Some x,pl))),u]
+ in
+ ((fun x -> ctx (Ast.Case (x,ity,outty,pl))),t)::
+ outty_split@list_split
+ (fun ctx0 (p,x) ->
+ ((fun y -> ctx0 (p,y)),x)::pattern_split
+ (fun y -> ctx0 (y,x)) p) (fun x -> ctx (Ast.Case(t,ity,outty,x)))
+ [] pl
+ | Ast.Cast (u,v) -> [ (fun x -> ctx (Ast.Cast (x,v))),u
+ ; (fun x -> ctx (Ast.Cast (u,x))),v ]
+ | Ast.LetIn ((n,None) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetIn ((n,Some t) as n',u,v) ->
+ [ (fun x -> ctx (Ast.LetIn ((n,Some x),u,v))), t
+ ; (fun x -> ctx (Ast.LetIn (n',x,v))), u
+ ; (fun x -> ctx (Ast.LetIn (n',u,x))), v ]
+ | Ast.LetRec (k,funs,where) -> (* we do not use where any more?? *)
+ list_split letrecaux_split (fun x -> ctx (Ast.LetRec(k,x,where))) [] funs
+ | _ -> [] (* leaves *)
+;;
+
+
+(* top_split : 'a -> ((term -> 'a) * term) list
+ * returns all the possible top-level (ctx,t) for its input *)
+let bfvisit ~pp_term top_split test t =
+ let rec aux = function
+ | [] -> None
+ | (ctx0,t0 as hd)::tl ->
+(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
+ prerr_endline ("t0 = " ^ pp_term t0);
+ if test t0 then (prerr_endline "caso 1"; Some hd)
+ else
+ let t0' = split ctx0 t0 in
+ (prerr_endline ("caso 2: length t0' = " ^ string_of_int
+ (List.length t0')); aux (tl@t0' (*split ctx0 t0*)))
+ (* in aux [(fun x -> x),t] *)
+ in aux (top_split t)
+;;
+
+let obj_split (o:Ast.term Ast.obj) = match o with
+ | Ast.Inductive (ls,itl) ->
+ list_split var_split (fun x -> Ast.Inductive (x,itl)) [] ls@
+ list_split ity_split (fun x -> Ast.Inductive (ls,x)) [] itl
+ | Ast.Theorem (flav,n,ty,None,p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,None,p)), ty]
+ | Ast.Theorem (flav,n,ty,(Some bo as bo'),p) ->
+ [(fun x -> Ast.Theorem (flav,n,x,bo',p)), ty
+ ;(fun x -> Ast.Theorem (flav,n,ty,Some x,p)), bo]
+ | Ast.Record (ls,n,ty,fl) ->
+ list_split var_split (fun x -> Ast.Record (x,n,ty,fl)) [] ls@
+ [(fun x -> Ast.Record (ls,n,x,fl)),ty]@
+ list_split field_split (fun x -> Ast.Record (ls,n,ty,x)) [] fl
+;;
+
+let bfvisit_obj = bfvisit obj_split;;
+
+let bfvisit = bfvisit (fun t -> [(fun x -> x),t]) ;;
+
+(*let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library t =
+ let mk_alias = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num _ -> DisambiguateTypes.Num None
+ | _ -> assert false
+ in
+ let lookup_choices =
+ fun item ->
+ (*match universe with
+ | None ->
+ lookup_in_library
+ interactive_user_uri_choice
+ input_or_locate_uri item
+ | Some e ->
+ (try Environment.find item e
+ with Not_found -> [])
+*)
+ (try Environment.find item universe
+ with Not_found -> [])
+ in
+ match t with
+ | Ast.Ident (_,None)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) ->
+ let choices = lookup_choices (mk_alias t) in
+ if List.length choices <> 1 then t
+ else List.hd choices
+ (* but we lose info on closedness *)
+ | t -> Ast.map (initialize_ast ~universe ~lookup_in_library) t
+;;
+*)
+
+let domain_item_of_ast = function
+ | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
+ | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
+ | Ast.Num (n,_) -> DisambiguateTypes.Num None
+ | Ast.Case(_,Some (ityname,_),_,_) -> DisambiguateTypes.Id (ityname,None)
+ | _ -> assert false
+;;
+
+let ast_of_alias_spec t alias = match (t,alias) with
+ | Ast.Ident _, GrafiteAst.Ident_alias (id,uri) -> Ast.Ident(id,`Uri uri)
+ | Ast.Case (t,_,oty,pl), GrafiteAst.Ident_alias (id,uri) ->
+ Ast.Case (t,Some (id,Some (NReference.reference_of_string uri)),oty,pl)
+ | _, GrafiteAst.Symbol_alias (sym,uri,desc) -> Ast.Symbol (sym,Some (uri,desc))
+ | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
+ | _ -> assert false
+;;
+
+let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl t =
+ try
+ let localization_tbl = mk_localization_tbl 503 in
+ let cic_thing =
+ interpretate_thing ~context ~env
+ ~uri ~is_path:false t ~localization_tbl
+ in
+ let foo () =
+ refine_thing metasenv subst context uri
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
+ in match (refine_profiler.HExtlib.profile foo ()) with
+ | Ko _ -> false
+ | _ -> true
+ with
+ (*| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+ | Invalid_choice loc_msg -> Ko loc_msg*)
+ | Invalid_choice _ -> false
+ | _ -> true
+;;
+
+let rec disambiguate_list
+ ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri ~interpretate_thing
+ ~refine_thing ~ugraph ~visit ~universe ~mk_localization_tbl ~pp_thing ~pp_term ts =
+ let disambiguate_list =
+ disambiguate_list ~context ~metasenv ~subst ~use_coercions ~expty ~env ~uri
+ ~interpretate_thing ~refine_thing ~ugraph ~visit ~universe
+ ~mk_localization_tbl ~pp_thing ~pp_term
+ in
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph ~mk_localization_tbl
+ in
+ let find_choices item =
+ let a2s = function
+ | GrafiteAst.Ident_alias (id,_)
+ | GrafiteAst.Symbol_alias (id,_,_) -> id
+ | GrafiteAst.Number_alias _ -> "NUM"
+ in
+ let d2s = function
+ | Id (id,_)
+ | Symbol (id,_) -> id
+ | Num _ -> "NUM"
+ in
+ let res =
+ Environment.find item universe
+ in
+ prerr_endline (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res)));
+ res
+ in
+
+ let get_instances ctx t =
+ try
+ let choices = find_choices (domain_item_of_ast t) in
+ List.map (fun t0 -> ctx (ast_of_alias_spec t t0)) choices
+ with
+ | Not_found -> []
+ in
+
+ match ts with
+ | [] -> None
+ | t0 :: tl ->
+ prerr_endline ("disambiguation of t0 = " ^ pp_thing t0);
+ let is_ambiguous = function
+ | Ast.Ident (_,`Ambiguous)
+ | Ast.Num (_,None)
+ | Ast.Symbol (_,None) -> true
+ | Ast.Case (_,Some (ity,None),_,_) ->
+ (prerr_endline ("ambiguous case" ^ ity);true)
+ | Ast.Case (_,None,_,_) -> prerr_endline "amb1";false
+ | Ast.Case (_,Some (ity,Some r),_,_) ->
+ (prerr_endline ("amb2 " ^ NReference.string_of_reference r);false)
+ | Ast.Ident (n,`Uri u) ->
+ (prerr_endline ("uri " ^ u ^ "inside IDENT " ^ n) ;false )
+ | _ -> false
+ in
+ let astpp = function
+ | Ast.Ident (id,_) -> "ID " ^ id
+ | Ast.Num _ -> "NUM"
+ | Ast.Symbol (sym,_) -> "SYM " ^ sym
+ | _ -> "ERROR!"
+ in
+ (* get first ambiguous subterm (or return disambiguated term) *)
+ match visit ~pp_term is_ambiguous t0 with
+ | None ->
+ prerr_endline ("not ambiguous:\n" ^ pp_thing t0);
+ Some (t0,tl)
+ | Some (ctx, t) ->
+ prerr_endline ("disambiguating node " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t));
+ (* get possible instantiations of t *)
+ let instances = get_instances ctx t in
+ (* perforate ambiguous subterms and test refinement *)
+ let survivors = List.filter test_interpr instances in
+ disambiguate_list (survivors@tl)
+;;
+
+
+(* let rec aux l =
+ match l with
+ | [] -> None
+ | (ctx,u)::vl ->
+ if test u
+ then (ctx,u)
+ else aux (vl@split ctx u)
+ in aux [t]
+;;*)
+
+(* let rec instantiate_ast = function
+ | Ident (n,Some _)
+ | Symbol (s,Some _)
+ | Num (n,Some _) as t -> []
+ | Ident (n,None) -> (* output: all possible instantiations of n *)
+ | Symbol (s,None) ->
+ | Num (n,None) ->
+
+
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> p,f u) pl in
+ Case (f t,ity,map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec -> ada (* TODO *)
+ | t -> t
+*)
+
+let disambiguate_thing
+ ~context ~metasenv ~subst ~use_coercions
+ ~string_context_of_context
+ ~initial_ugraph:base_univ ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance
+ ~aliases ~universe ~lookup_in_library
+ ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing
+ ~visit ~mk_localization_tbl
+ (thing_txt,thing_txt_prefix_len,thing)
+=
+(* XXX: will be thrown away *)
+ let todo_dom = domain_of_thing ~context:(string_context_of_context context) thing
+ in
+ let rec aux_env env = function
+ | [] -> env
+ | Node (_, item, l) :: tl ->
+ let env =
+ Environment.add item
+ (mk_implicit
+ (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+ env in
+ aux_env (aux_env env l) tl in
+ let env = aux_env aliases todo_dom in
+
+ let test_interpr = test_interpr ~context ~metasenv ~subst ~use_coercions ~expty
+ ~env ~uri ~interpretate_thing ~refine_thing ~ugraph:base_univ ~mk_localization_tbl
+ in
+(* real function *)
+ let rec aux tl =
+ match disambiguate_list ~mk_localization_tbl ~context ~metasenv ~subst
+ ~interpretate_thing ~refine_thing ~ugraph:base_univ ~visit
+ ~use_coercions ~expty ~uri ~env ~universe ~pp_thing
+ ~pp_term tl with
+ | None -> []
+ | Some (t,tl') -> t::aux tl'
+ in
+
+ let refine t =
+ let localization_tbl = mk_localization_tbl 503 in
+ match refine_thing metasenv subst context uri
+ ~use_coercions
+ (interpretate_thing ~context ~env ~uri ~is_path:false t ~localization_tbl)
+ expty base_univ ~localization_tbl with
+ | Ok (t',m',s',u') -> ([]:(Environment.key * 'f) list),m',s',t',u'
+ | Uncertain x ->
+ let _,err = Lazy.force x in
+ prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ assert false
+ | _ -> assert false
+ in
+ if not (test_interpr thing) then raise (NoWellTypedInterpretation (0,[]))
+ else
+ let res = aux [thing] in
+ let res =
+ HExtlib.filter_map (fun t -> try Some (refine t) with _ -> None) res
+ in
+ match res with
+ | [] -> raise (NoWellTypedInterpretation (0,[]))
+ | [t] -> res,false
+ | _ -> res,true
+;;
+
+(*