File: double_negate_ml

package info (click to toggle)
coccinelle 1.0.8.deb-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 26,148 kB
  • sloc: ml: 136,392; ansic: 23,594; sh: 2,189; makefile: 2,157; perl: 1,576; lisp: 840; python: 823; awk: 70; csh: 12
file content (75 lines) | stat: -rw-r--r-- 1,881 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
(* optimizes triples that have complementary environments and the same
witnesses *)

let double_negate trips =
  let y =
    List.sort
      (function (s,_,wit) -> function (s',_,wit') -> compare (s,wit) (s',wit'))
      trips in
  let rec classify = function
      [] -> []
    | ((s,th,wit) as x)::rest ->
	(match classify rest with
	  [] -> [[x]]
	| (((s',th',wit')::_) as x1)::rest ->
	    if (s,wit) = (s',wit')
	    then (x::x1)::rest
	    else [x]::(x1::rest)
	| _ -> failwith "double negate: not possible") in
  let y =
    List.map
      (function
	  (((s,_,wit)::_) as all) ->
	    ((s,wit),List.map (function (_,th,_) -> th) all)
	| _ -> failwith "double negate2: not possible")
    (classify y) in
  let cnf rest_th th =
    List.fold_left
      (function rest ->
	function sub1 ->
	  List.fold_left
	    (function rest ->
	      function subs ->
		if memBy eq_sub (negate_sub sub1) subs
		then rest
		else if memBy eq_sub sub1 subs
		then subs::rest
		else (sub1::subs)::rest)
	    rest rest_th)
      [] th in
  let dnf rest_th th =
    List.fold_left
      (function rest ->
	function sub1 ->
	  List.fold_left
	    (function rest ->
	      function subs ->
		match conj_subst [sub1] subs with
		  None -> rest
		| Some th -> th::rest)
	    rest rest_th)
      [] th in
  let res =
    List.sort compare
      (List.fold_left
	 (function rest ->
	   function
	       ((s,wit),[th]) -> (s,th,wit)::rest
	     | ((s,wit),ths) ->
		 match ths with
		   [] -> failwith "dnf: not possible"
		 | (th::ths) ->
		     let (cnf : substitution list) =
		       List.fold_left cnf
			 (List.map (function x -> [x]) th) ths in
		     match cnf with
		       [] -> (s,[],wit)::rest
		     | th::ths ->
			 let res =
			   setify
			     (List.fold_left dnf
				(List.map (function x -> [x]) th)
				ths) in
			 (List.map (function th -> (s,th,wit)) res) @ rest)
	 [] y) in
  res