diff options
author | 2001-04-04 12:44:55 +0000 | |
---|---|---|
committer | 2001-04-04 12:44:55 +0000 | |
commit | e16efa883ae0cf5c82a2ee60bf05304fb9c69b51 (patch) | |
tree | c34994a4b24950cde4af71d65baa4ac29fb51d00 /contrib/interface/dad.ml | |
parent | e1d0e117652115b05faec1c276b9f14c5bf70d1f (diff) |
Files that handle the dialogue with the graphical user-interface pcoq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/dad.ml')
-rw-r--r-- | contrib/interface/dad.ml | 357 |
1 files changed, 357 insertions, 0 deletions
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml new file mode 100644 index 000000000..1fefb6c44 --- /dev/null +++ b/contrib/interface/dad.ml @@ -0,0 +1,357 @@ +(* This file contains an ml version of drag-and-drop. *) + +(* #use "/net/home/bertot/experiments/pcoq/src/dad/dad.ml" *) + +open Names;; +open Term;; +open Rawterm;; +open Util;; +open Environ;; +open Tactics;; +open Tacticals;; +open Pattern;; +open Reduction;; +open Coqast;; +open Termast;; +open Astterm;; +open Vernacinterp;; + +open Proof_type;; +open Proof_trees;; +open Tacmach;; +open Typing;; +open Pp;; + +open Paths;; + +(* In a first approximation, drag-and-drop rules are like in CtCoq + 1/ a pattern, + 2,3/ Two paths: start and end positions, + 4/ the degree: the number of steps the algorithm should go up from the + longest common prefix, + 5/ the tail path: the suffix of the longest common prefix of length the + degree, + 6/ the command pattern, where meta variables are represented by objects + of the form Node(_,"META"; [Num(_,i)]) +*) + + +type dad_rule = Coqast.t * int list * int list * int * int list * Coqast.t;; + +(* This value will be used systematically when constructing objects of + type Coqast.t, the value is stupid and meaningless, but it is needed + to construct well-typed terms. *) + +let zz = (0,0);; + +(* This function receives a length n, a path p, and a term and returns a + couple whose first component is the subterm designated by the prefix + of p of length n, and the second component is the rest of the path *) + +let rec get_subterm (depth:int) (path: int list) (constr:constr) = + match depth, path, kind_of_term constr with + 0, l, c -> (constr,l) + | n, 2::a::tl, IsApp(func,arr) -> + get_subterm (n - 2) tl arr.(a-1) + | _,l,_ -> failwith (int_list_to_string + "wrong path or wrong form of term" + l);; + +(* This function maps a substitution on an abstract syntax tree. The + first argument, an object of type env, is necessary to + transform constr terms into abstract syntax trees. The second argument is + the substitution, a list of pairs linking an integer and a constr term. *) +let map_subst (env :env) + (subst:(int * Term.constr) list) = + let rec map_subst_aux = function + Node(_, "META", [Num(_, i)]) -> + let constr = List.assoc i subst in + ast_of_constr false env constr + | Node(loc, s, l) -> Node(loc, s, List.map map_subst_aux l) + | ast -> ast in + map_subst_aux;; + + +(* This function is really the one that is important. *) +let rec find_cmd (l:(string * dad_rule) list) env constr p p1 p2 = + match l with + [] -> failwith "nothing happens" + | (name, (pat, p_f, p_l, deg, p_r, cmd))::tl -> + let length = List.length p in + try + if deg > length then + failwith "internal" + else + let term_to_match, p_r = + try + get_subterm (length - deg) p constr + with + Failure s -> failwith "internal" in + let _, constr_pat = + interp_constrpattern Evd.empty (Global.env()) + pat in + let subst = matches constr_pat term_to_match in + if (is_prefix p_f (p_r@p1)) & (is_prefix p_l (p_r@p2)) then + map_subst env subst cmd + else + failwith "internal" + with + Failure "internal" -> find_cmd tl env constr p p1 p2 + | PatternMatchingFailure -> find_cmd tl env constr p p1 p2;; + + +let dad_rule_list = ref ([]: (string * dad_rule) list);; + + +(* \\ This function is also used in pbp. *) +let rec tactic_args_to_ints = function + [] -> [] + | (Integer n)::l -> n::(tactic_args_to_ints l) + | _ -> failwith "expecting only numbers";; + +(* We assume that the two lists of integers for the tactic are simply + given in one list, separated by a dummy tactic. *) +let rec part_tac_args l = function + [] -> l,[] + | (Tacexp a)::tl -> l, (tactic_args_to_ints tl) + | (Integer n)::tl -> part_tac_args (n::l) tl + | _ -> failwith "expecting only numbers and the word \"to\"";; + + +(* The dad_tac tactic takes a display_function as argument. This makes + it possible to use it in pcoq, but also in other contexts, just by + changing the output routine. *) +let dad_tac display_function = function + l -> let p1, p2 = part_tac_args [] l in + (function g -> + let (p_a, p1prime, p2prime) = decompose_path (List.rev p1,p2) in + (display_function + (find_cmd (!dad_rule_list) (pf_env g) + (pf_concl g) p_a p1prime p2prime)); + tclIDTAC g);; + +(* Now we enter dad rule list management. *) + +let add_dad_rule name patt p1 p2 depth pr command = + dad_rule_list := (name, + (patt, p1, p2, depth, pr, command))::!dad_rule_list;; + +let rec remove_if_exists name = function + [] -> false, [] + | ((a,b) as rule1)::tl -> if a = name then + let result1, l = (remove_if_exists name tl) in + true, l + else + let result1, l = remove_if_exists name tl in + result1, (rule1::l);; + +let remove_dad_rule name = + let result1, result2 = remove_if_exists name !dad_rule_list in + if result1 then + failwith("No such name among the drag and drop rules " ^ name) + else + dad_rule_list := result2;; + +let dad_rule_names () = + List.map (function (s,_) -> s) !dad_rule_list;; + +(* this function is inspired from matches_core in pattern.ml *) +let constrain ((n : int),(pat : constr_pattern)) sigma = + if List.mem_assoc n sigma then + if pat = (List.assoc n sigma) then sigma + else failwith "internal" + else + (n,pat)::sigma + +(* This function is inspired from matches_core in pattern.ml *) +let more_general_pat pat1 pat2 = + let rec match_rec sigma p1 p2 = + match p1, p2 with + | PMeta (Some n), m -> constrain (n,m) sigma + + | PMeta None, m -> sigma + + | PRef (VarRef sp1), PRef(VarRef sp2) when sp1 = sp2 -> sigma + + | PVar v1, PVar v2 when v1 = v2 -> sigma + + | PRef ref1, PRef ref2 when ref1 = ref2 -> sigma + + | PRel n1, PRel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), PSort (RProp c2) when c1 = c2 -> sigma + + | PSort RType, PSort RType -> sigma + + | PApp (c1,arg1), PApp (c2,arg2) -> + (try array_fold_left2 match_rec (match_rec sigma c1 c2) arg1 arg2 + with Invalid_argument _ -> failwith "internal") + | _ -> failwith "unexpected case in more_general_pat" in + try let _ = match_rec [] pat1 pat2 in true + with Failure "internal" -> false;; + +let more_general r1 r2 = + match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p11 p21) & (is_prefix p12 p22);; + +let not_less_general r1 r2 = + not (match r1,r2 with + (_,(patt1,p11,p12,_,_,_)), + (_,(patt2,p21,p22,_,_,_)) -> + (more_general_pat patt1 patt2) & + (is_prefix p21 p11) & (is_prefix p22 p12));; + +let rec add_in_list_sorting rule1 = function + [] -> [rule1] + | (b::tl) as this_list -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else if not_less_general rule1 b then + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> rule1::this_list + | _ -> b::tl2) + else + rule1::this_list +and add_in_list_sorting_aux rule1 = function + [] -> [] + | b::tl -> + if more_general rule1 b then + b::(add_in_list_sorting rule1 tl) + else + let tl2 = add_in_list_sorting_aux rule1 tl in + (match tl2 with + [] -> [] + | _ -> rule1::tl2);; + +let rec sort_list = function + [] -> [] + | a::l -> add_in_list_sorting a (sort_list l);; + +let mk_dad_meta n = Node(zz,"META",[Num(zz, n)]);; +let mk_rewrite1 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteLR", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + +let mk_rewrite2 ast = + Node(zz,"TACTICLIST", + [Node(zz,"RewriteRL", + [Node(zz, "COMMAND", ast);Node(zz,"BINDINGS",[])])]);; + + + +let start_dad () = +vinterp_add "AddDadRule" + (function + | [VARG_STRING name; VARG_CONSTR pat; VARG_NUMBERLIST p1; + VARG_NUMBERLIST p2; VARG_TACTIC com] -> + (function () -> + let pr = match decompose_path (p1, p2) with pr, _, _ -> pr in + (add_dad_rule name pat p1 p2 (List.length pr) pr com)) + | _ -> errorlabstrm "AddDadRule1" + [< 'sTR "AddDadRule2">]); +add_dad_rule "distributivity-inv" +(Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-r" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "distributivity1-l" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,2)])]);Node(zz,"APPLIST",[Nvar(zz,"mult");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1; 2; 2] +[] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "mult_plus_distr");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "associativity" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"META",[Num(zz,3)])]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[] +0 +[] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_assoc_r");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-lr" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "minus-identity-rl" +(Node(zz,"APPLIST",[Nvar(zz,"minus");Node(zz,"META",[Num(zz,2)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "minus_n_n");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 2] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-sym-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])) +[2; 1] +[2; 2] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_sym");(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[2; 2] +[1] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "absorb-0-r-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,2)]);Nvar(zz,"O")])) +[1] +[2; 2] +0 +[] +(mk_rewrite2 ([Node(zz, "APPLIST", [Nvar(zz, "plus_n_O");(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-lr" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 1] +[2; 2; 2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])])); + +add_dad_rule "plus-permute-rl" +(Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,4)]);Node(zz,"APPLIST",[Nvar(zz,"plus");Node(zz,"META",[Num(zz,3)]);Node(zz,"META",[Num(zz,2)])])])) +[2; 2; 2; 1] +[2; 1] +1 +[2] +(mk_rewrite1 ([Node(zz, "APPLIST", [Nvar(zz, "plus_permute");(mk_dad_meta 4) ;(mk_dad_meta 3) ;(mk_dad_meta 2) ])]));; + +vinterp_add "StartDad" + (function + | [] -> + (function () -> start_dad()) + | _ -> errorlabstrm "StartDad" [< >]);; |