{ status with gstatus = new_gstatus }
;;
-let fold_tactic tac status =
+let block_tac l status =
+ List.fold_left (fun status tac -> tac status) status l
+;;
+
+let compare_menv ~past ~present =
+ List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
+ List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
+;;
+
+(* Exec and distribute_tac form a retraction pair:
+ 1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
+ 2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
+ distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
+ 3) tac G = distribute_tac (exec tac) G if
+ tac = distribute_tac lowtac
+
+ Note that executing an high tactic on a set of goals may be stronger
+ than executing the same tactic on those goals, but once at a time
+ (e.g. the tactic could perform a global analysis of the set of goals)
+*)
+
+let exec tac (low_status,g) =
+ let stack = [ [0,Open g], [], [], `NoTag ] in
+ let _,_,old_metasenv,_,_ = low_status.pstatus in
+ let status = tac { gstatus = stack ; istatus = low_status } in
+ let _,_,metasenv,_,_ = status.istatus.pstatus in
+ let open_goals, closed_goals =
+ compare_menv ~past:old_metasenv ~present:metasenv
+ in
+ status.istatus, open_goals, closed_goals
+;;
+
+let distribute_tac tac status =
match status.gstatus with
| [] -> assert false
| (g, t, k, tag) :: s ->
{ gstatus = stack; istatus = sn }
;;
+type cic_term = NCic.conjecture
+type ast_term = string * int * CicNotationPt.term
+type position = Ctx of NCic.context | Term of cic_term
+
+
+let relocate (name,ctx,t as term) context =
+ let is_prefix l1 l2 =
+ let rec aux = function
+ | [],[] -> true
+ | x::xs, y::ys -> x=y && aux (xs,ys)
+ | _ -> false
+ in
+ aux (List.rev l1, List.rev l2)
+ in
+ if ctx = context then term else
+ if is_prefix ctx context then
+ (name, context,
+ NCicSubstitution.lift (List.length context - List.length ctx) t)
+ else
+ assert false
+;;
+
+let disambiguate (status : lowtac_status) (t : ast_term)
+ (ty : cic_term option) (where : position) =
+ let uri,height,metasenv,subst,obj = status.pstatus in
+ let context = match where with Ctx c -> c | Term (_,c,_) -> c in
+ let expty =
+ match ty with
+ | None -> None | Some ty -> let _,_,x = relocate ty context in Some x
+ in
+ let metasenv, subst, lexicon_status, t =
+ GrafiteDisambiguate.disambiguate_nterm expty
+ status.lstatus context metasenv subst t
+ in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+ { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t)
+;;
+
+let select_term low_status (name,context,term) (path, matched) =
+ let eq context (status as old_status) t1 t2 =
+ let _,_,t2 = relocate t2 context in
+ if t2 = t1 then true, status else false, old_status
+ in
+ let match_term m =
+ let rec aux ctx status t =
+ let b, status = eq ctx status t m in
+ if b then
+ let n,h,metasenv,subst,o = status.pstatus in
+ let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
+ let metasenv, instance, ty =
+ NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
+ in
+ let metasenv, subst =
+ NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx
+ t instance
+ in
+ let status = { status with pstatus = n,h,metasenv,subst,o } in
+ status, instance
+ else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
+ in
+ aux
+ in
+ let rec select status ctx pat cic =
+ match pat, cic with
+ | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
+ let status, s = select status ctx s1 s2 in
+ let ctx = (n, NCic.Decl s2) :: ctx in
+ let status, t = select status ctx t1 t2 in
+ status, NCic.Prod (n,s,t)
+ | NCic.Appl l1, NCic.Appl l2 ->
+ let status, l =
+ List.fold_left2
+ (fun (status,l) x y ->
+ let status, x = select status ctx x y in
+ status, l @ [x])
+ (status,[]) l1 l2
+ in
+ status, NCic.Appl l
+ | NCic.Implicit `Hole, t -> status, t
+ | NCic.Implicit `Term, t ->
+ let status, matched = disambiguate status matched None (Ctx ctx) in
+ match_term matched ctx status t
+ | _,t -> status, t
+ in
+ let status, term = select low_status context path term in
+ let _,_,_,subst,_ = status.pstatus in
+ let selections =
+ HExtlib.filter_map
+ (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None)
+ subst
+ in
+ status, (name, context, term), selections
+;;
+
+let get_goal (status : lowtac_status) (g : int) =
+ let _,_,metasenv,_,_ = status.pstatus in
+ List.assoc g metasenv
+;;
+
+let return ~orig status =
+ let _,_,past,_,_ = orig.pstatus in
+ let _,_,present,_,_ = status.pstatus in
+ let open_goals, closed_goals = compare_menv ~past ~present in
+ status, open_goals, closed_goals
+;;
+
+let instantiate status i t =
+ let name,height,metasenv,subst,obj = status.pstatus in
+ let _, context, ty = List.assoc i metasenv in
+ let _,_,t = relocate t context in
+ let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
+ let db = NCicUnifHint.db () in (* XXX fixme *)
+ let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
+ { status with pstatus = (name,height,metasenv,subst,obj) }
+;;
+
+let mkmeta name status (_,ctx,ty) =
+ let n,h,metasenv,s,o = status.pstatus in
+ let metasenv, instance, _ =
+ NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
+ in
+ let status = { status with pstatus = n,h,metasenv,s,o } in
+ status, (name,ctx,instance)
+;;
+
+let apply t (status as orig, goal) =
+ let goalty = get_goal status goal in
+ let status, t = disambiguate status t (Some goalty) (Term goalty) in
+ let status = instantiate status goal t in
+ return ~orig status
+;;
+
+let change what (*where*) with_what (status as orig, goal) =
+ let (name,_,_ as goalty) = get_goal status goal in
+ let status, newgoalty, selections =
+ select_term status goalty
+ (NCic.Prod ("_",NCic.Implicit `Hole,NCic.Implicit `Term), what)
+ in
+
+ let n,h,metasenv,subst,o = status.pstatus in
+ let subst, newm =
+ List.partition (fun i,_ -> not (List.mem i selections)) subst
+ in
+ let metasenv = List.map (fun (i,(n,c,_,t)) -> i,(n,c,t)) newm @ metasenv in
+ let status = { status with pstatus = n,h,metasenv,subst,o } in
+
+ let status = (* queste sono apply, usa un tatticale! *)
+ List.fold_left
+ (fun status i ->
+ let x = get_goal status i in
+ let status, with_what =
+ disambiguate status with_what (Some x) (Term x)
+ in
+ instantiate status i with_what)
+ status selections
+ in
+ let status, m = mkmeta name status newgoalty in
+ let status = instantiate status goal m in
+ return ~orig status
+;;
let apply t (status,goal) =
- let _,_,metasenv, subst,_ = status.pstatus in
- let _,context,gty = List.assoc goal metasenv in
+ let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
+ let name,context,gty = List.assoc goal metasenv in
let metasenv, subst, lexicon_status, t =
- GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t
+ GrafiteDisambiguate.disambiguate_nterm (Some gty)
+ status.lstatus context metasenv subst t
+ in
+ let subst, metasenv =
+ (goal, (name, context, t, gty)):: subst,
+ List.filter(fun (x,_) -> x <> goal) metasenv
in
- prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
+ let open_goals, closed_goals =
+ compare_menv ~past:old_metasenv ~present:metasenv in
+ let new_pstatus = uri,height,metasenv,subst,obj in
+
+ prerr_endline ("termine disambiguato: " ^
+ NCicPp.ppterm ~context ~metasenv ~subst t);
prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
prerr_endline "fine napply";
- { status with lstatus = lexicon_status }, [goal], []
+
+ { lstatus = lexicon_status; pstatus = new_pstatus }, open_goals, closed_goals
;;
-let apply_tac t = fold_tactic (apply t) ;;
+let apply_tac t = distribute_tac (apply t) ;;
+let change_tac w ww = distribute_tac (change w ww) ;;
projects / helm.git / blobdiff