(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-exception Error of string lazy_t
-let fail msg = raise (Error msg)
+exception Error of string lazy_t * exn option
+let fail ?exn msg = raise (Error (msg,exn))
+
+let wrap f x =
+ try f x
+ with
+ | MultiPassDisambiguator.DisambiguationError _
+ | NCicRefiner.RefineFailure _
+ | NCicUnification.UnificationFailure _
+ | NCicTypeChecker.TypeCheckerFailure _
+ | NCicMetaSubst.MetaSubstFailure _ as exn -> fail ~exn (lazy "")
+;;
class pstatus =
fun (o: NCic.obj) ->
type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
-let pp_tac_status status =
- prerr_endline (NCicPp.ppobj status#obj)
-;;
-
-let pp_lowtac_status status =
- prerr_endline "--------------------------------------------";
+let pp_status status =
prerr_endline (NCicPp.ppobj status#obj)
;;
-type cic_term = NCic.conjecture (* name, context, term *)
+type cic_term = NCic.conjecture (* attrs, context, term *)
let ctx_of (_,c,_) = c ;;
let relocate status destination (name,source,t as orig) =
let status = status#set_obj (u, d, metasenv, subst, o) in
status, (name, destination, t)
;;
+let relocate a b c = wrap (relocate a b) c;;
let term_of_cic_term s t c =
let s, (_,_,t) = relocate s c t in
GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t
in
let new_pstatus = uri,height,metasenv,subst,obj in
- status#set_obj new_pstatus, (None, context, t)
+ status#set_obj new_pstatus, ([], context, t)
;;
+let disambiguate a b c d = wrap (disambiguate a b c) d;;
let typeof status ctx t =
let status, (_,_,t) = relocate status ctx t in
let _,_,metasenv,subst,_ = status#obj in
let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
- status, (None, ctx, ty)
+ status, ([], ctx, ty)
;;
+let typeof a b c = wrap (typeof a b) c;;
let whd status ?delta ctx t =
let status, (name,_,t) = relocate status ctx t in
let metasenv, subst = NCicUnification.unify status metasenv subst ctx a b in
status#set_obj (n,h,metasenv,subst,o)
;;
+let unify a b c d = wrap (unify a b c) d;;
+
+let fix_sorts (name,ctx,t) =
+ let f () =
+ let t = NCicUnification.fix_sorts t in
+ name,ctx,t
+ in
+ wrap f ()
+;;
let refine status ctx term expty =
let status, (nt,_,term) = relocate status ctx term in
let status, ne, expty =
- match expty with None -> status, None, None
+ match expty with
+ None -> status, [], None
| Some e ->
let status, (n,_, e) = relocate status ctx e in status, n, Some e
in
in
status#set_obj (name,height,metasenv,subst,obj), (nt,ctx,t), (ne,ctx,ty)
;;
+let refine a b c d = wrap (refine a b c) d;;
let get_goalty status g =
let _,_,metasenv,_,_ = status#obj in
status#set_obj (name,height,metasenv,subst,obj)
;;
-let mk_meta status ?name ctx bo_or_ty =
+let mk_meta status ?(attrs=[]) ctx bo_or_ty =
match bo_or_ty with
| `Decl ty ->
let status, (_,_,ty) = relocate status ctx ty in
let n,h,metasenv,subst,o = status#obj in
let metasenv, _, instance, _ =
- NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
+ NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty)
in
let status = status#set_obj (n,h,metasenv,subst,o) in
- status, (None,ctx,instance)
+ status, ([],ctx,instance)
| `Def bo ->
let status, (_,_,bo_ as bo) = relocate status ctx bo in
let status, (_,_,ty) = typeof status ctx bo in
let n,h,metasenv,subst,o = status#obj in
let metasenv, metano, instance, _ =
- NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty) in
+ NCicMetaSubst.mk_meta ~attrs metasenv ctx (`WithType ty) in
let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in
- let subst = (metano, (name, ctx, bo_, ty)) :: subst in
+ let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in
let status = status#set_obj (n,h,metasenv,subst,o) in
- status, (None,ctx,instance)
+ status, ([],ctx,instance)
;;
-let mk_in_scope status t =
- mk_meta status ~name:NCicMetaSubst.in_scope_tag (ctx_of t) (`Def t)
+let mk_in_scope status t =
+ mk_meta status ~attrs:[`InScope] (ctx_of t) (`Def t)
;;
let mk_out_scope n status t =
- mk_meta status ~name:(NCicMetaSubst.out_scope_tag n) (ctx_of t) (`Def t)
+ mk_meta status ~attrs:[`OutScope n] (ctx_of t) (`Def t)
;;
(* the following unification problem will be driven by
=
let is_found status ctx t wanted =
(* we could lift wanted step-by-step *)
- try true, unify status ctx (None, ctx, t) wanted
+ try true, unify status ctx ([], ctx, t) wanted
with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> false, status
+ | Error (_, Some (NCicUnification.UnificationFailure _))
+ | Error (_, Some (NCicUnification.Uncertain _)) -> false, status
in
let match_term status ctx (wanted : cic_term) t =
let rec aux ctx (status,already_found) t =
let b, status = is_found status ctx t wanted in
if b then
- let status , (_,_,t) = found status (None, ctx, t) in
+ let status , (_,_,t) = found status ([], ctx, t) in
(status,true),t
else
let _,_,_,subst,_ = status#obj in
let (status',found), t' = match_term status' ctx wanted t in
if found then status',t' else status,t
| None ->
- let (status,_),t = match_term status ctx (None,ctx,t) t in
+ let (status,_),t = match_term status ctx ([],ctx,t) t in
status,t)
| NCic.Implicit _, t -> status, t
| _,t ->
status, (ref, consno, left, right)
;;
-let mk_cic_term c t = None,c,t ;;
+let mk_cic_term c t = [],c,t ;;
let apply_subst status ctx t =
let status, (name,_,t) = relocate status ctx t in
status, (name, ctx, NCicUntrusted.apply_subst subst ctx t)
;;
+(* ============= move this elsewhere ====================*)
+
class ['stack] status =
fun (o: NCic.obj) (s: 'stack) ->
object
class type tac_status = [Continuationals.Stack.t] status
type 'status tactic = #tac_status as 'status -> 'status
+
projects / helm.git / blobdiff