2 * Copyright (c) 2000-2001
3 * The Regents of the University of California. All rights reserved.
5 * Redistribution and use in source and binary forms, with or without
6 * modification, are permitted provided that the following conditions
8 * 1. Redistributions of source code must retain the above copyright
9 * notice, this list of conditions and the following disclaimer.
10 * 2. Redistributions in binary form must reproduce the above copyright
11 * notice, this list of conditions and the following disclaimer in the
12 * documentation and/or other materials provided with the distribution.
13 * 3. Neither the name of the University nor the names of its contributors
14 * may be used to endorse or promote products derived from this software
15 * without specific prior written permission.
17 * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
18 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
19 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
20 * ARE DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
21 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
22 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
23 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
24 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
25 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
26 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
32 #include "flowrow-sort.h"
33 #include "flowrow-var.h"
34 #include "setif-sort.h"
35 #include "setif-var.h"
36 #include "setst-sort.h"
37 #include "setst-var.h"
38 #include "term-sort.h"
50 typedef struct constructor
*constructor
;
65 typedef struct sig_elt sig_elt
;
67 typedef struct proj_pat
79 typedef struct cons_expr
97 fprintf(stderr
, "Exceeded maximum number of constructors\n");
104 static bool fixed_sort(sort_kind s
)
106 return !(s
== sort_term
|| s
== sort_set
);
110 Convention : constructor types are even, pats are odd.
111 The smallest specialized type is 10.
113 static bool setif_is_pat(gen_e e
)
115 int type
= ((setif_term
)e
)->type
;
116 return ( (type
& 1) && (type
> 10) );
119 static bool setst_is_pat(gen_e e
)
121 int type
= ((setst_term
)e
)->type
;
122 return ( (type
& 1) && (type
> 10) );
125 static gen_e
get_proj_var(sort_kind s
, bool large
)
132 return (gen_e
)sv_fresh_large(get_sort_region(setif_sort
),NULL
);
133 else return (gen_e
)sv_fresh(get_sort_region(setif_sort
),NULL
);
139 return (gen_e
)st_fresh_large(get_sort_region(setst_sort
),NULL
);
140 else return (gen_e
)st_fresh(get_sort_region(setst_sort
),NULL
);
146 return (gen_e
)fv_fresh_large(get_sort_region(flowrow_sort
),NULL
);
147 else return (gen_e
)fv_fresh(get_sort_region(flowrow_sort
),NULL
);
153 return (gen_e
)tv_fresh_large(get_sort_region(term_sort
),NULL
);
154 else return (gen_e
)tv_fresh(get_sort_region(term_sort
),NULL
)
159 fail("Unmatched sort in get_proj_var\n");
168 static gen_e
get_sort_zero(sort_kind s
)
177 return flowrow_zero();
181 fail("Unmatched sort in get_sort_zero\n");
187 static gen_e
get_sort_one(sort_kind s
)
196 return flowrow_one();
200 fail("Unmatched sort in get_sort_zero\n");
206 static region
get_sort_region(sort s
)
215 return flowrow_region
;
219 fail("Unmatched sort in get_sort_region\n");
225 static term_hash
get_sort_hash(sort s
)
238 fail("Unmatched sort in get_sort_hash\n");
244 constructor
make_constructor(const char *name
,sort_kind sort
, sig_elt s
[],
247 constructor c
= ralloc(expr_region
,struct constructor
);
248 sig_elt
*sig
= rarrayalloc(expr_region
,arity
,sig_elt
);
250 c
->type
= new_type();
254 memcpy(sig
,s
,sizeof(sig_elt
)*arity
);
257 if ( fixed_sort(sort
) )
258 failure("Specified sort does not allow constructor types\n");
262 c
->name
= rstrdup(expr_region
,name
);
268 gen_e
constructor_expr(constructor c
, gen_e exps
[], int arity
)
272 region sort_region
= get_sort_region(c
->sort
);
273 term_hash sort_hash
= get_sort_hash(c
->sort
);
275 stamp
*st
= rarrayalloc(sort_region
,arity
+ 1,stamp
);
278 // Dynamic arity check
279 if(arity
!= c
->arity
)
280 failure("Signature mismatch\n");
282 // Dynamic sort checks
283 for (i
= 0; i
< arity
; i
++)
285 if ( c
->sig
[i
].sort
!= exps
[i
]->sort
)
286 failure(stderr
,"Signature mismatch\n");
287 st
[i
+1] = exps
[i
]->st
;
290 // Hash-consing of terms
291 if (!(result
= term_hash_find(sort_hash
,st
,arity
+1)) || arity
== 0 )
293 gen_e
*e
= rarrayalloc(sort_region
,arity
,gen_e
);
296 memcpy(e
,exps
,sizeof(gen_e
)*arity
);
300 result
= ralloc(sort_region
,struct cons_expr
);
301 result
->type
= st
[0];
302 result
->st
= stamp_fresh();
303 result
->sort
= c
->sort
;
304 result
->arity
= c
->arity
;
305 result
->name
= c
->name
;
306 result
->sig
= c
->sig
;
309 term_hash_insert(expr_hash
,result
,st
,arity
+1);
312 return (gen_e
)result
;
315 static gen_e
proj_pat(constructor c
, int i
, gen_e e
)
318 region sort_region
= get_sort_region(e
->sort
);
319 term_hash sort_hash
= get_sort_hash(e
->sort
);
326 if (! (pat
= term_hash_find(sort_hash
,s
,3)) )
328 pat
= ralloc(sort_region
,struct proj_pat
);
330 pat
->st
= stamp_fresh();
333 pat
->variance
= c
->sig
[i
].variance
;
336 term_hash_insert(sort_hash
,pat
,s
,3);
342 gen_e
setif_proj_pat(constructor c
,int i
,gen_e e
)
344 return proj_pat(c
,i
,e
);
347 gen_e
setst_proj_pat(constructor c
, int i
, gen_e e
)
349 return proj_pat(c
,i
,e
);
352 gen_e
setif_proj(constructor c
, int i
, gen_e e
)
355 gen_e proj_var
, proj
;
357 gen_e
nonspec_get_proj(gen_e_list arg1
)
360 gen_e_list_scanner scan
;
363 gen_e_list_scan(arg1
,&scan
);
364 while (gen_e_list_next(&scan
,&temp
))
366 pat
= (proj_pat
)temp
;
367 if ( pat_match(pat
->type
,c
->type
) && i
== pat
->i
)
373 if (e
->sort
!= setif_sort
)
375 failure("Sort check : setif_proj\n");
378 else if (i
< 0 || i
> c
->arity
)
380 failure("Signature mismatch\n");
383 else if (setif_is_zero(e
))
384 return get_sort_zero(c
->sig
[i
].sort
);
386 else if ( ((setif_term
)e
)->type
== c
->type
)
388 cons_expr constructed
= (cons_expr
)e
;
389 return constructed
->exps
[i
];
392 else if (setif_is_var(e
))
395 if ( (proj
= sv_get_ub_proj(v
,nonspec_get_proj
)) )
402 gen_e_list_scanner scan
;
404 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
405 pat
= setif_proj_pat(c
,i
,proj_var
);
406 sv_add_ub_proj(sort_region
,v
,pat
);
408 gen_e_list_scan(sv_get_lbs(v
),&scan
);
409 while (gen_e_list_next(&scan
,&lb
))
411 setif_inclusion(lb
,pat
);
417 else if (setif_is_union(e
))
419 if( (proj
= nonspec_get_proj(setif_get_proj_cache(e
))) )
424 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
425 pat
= setif_proj_pat(c
,i
,proj_var
);
427 setif_set_proj_cache(e
,pat
);
429 setif_inclusion(e
,pat
);
436 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
437 pat
= setif_proj_pat(c
,i
,proj_var
);
438 setif_inclusion(e
,pat
);
443 gen_e
setst_proj(constructor c
, int i
, gen_e e
)
446 gen_e proj_var
, proj
;
448 gen_e
nonspec_get_proj(gen_e_list arg1
)
451 gen_e_list_scanner scan
;
454 gen_e_list_scan(arg1
,&scan
);
455 while (gen_e_list_next(&scan
,&temp
))
457 pat
= (proj_pat
)temp
;
458 if ( pat_match(pat
->type
,c
->type
) && i
== pat
->i
)
464 if (e
->sort
!= setst_sort
)
466 failure("Sort check : setst_proj\n");
469 else if (i
< 0 || i
> c
->arity
)
471 failure("Signature mismatch\n");
474 else if (setst_is_zero(e
))
475 return get_sort_zero(c
->sig
[i
].sort
);
477 else if ( ((setst_term
)e
)->type
== c
->type
)
479 cons_expr constructed
= (cons_expr
)e
;
480 return constructed
->exps
[i
];
483 else if (setst_is_var(e
))
486 if ( (proj
= sv_get_ub_proj(v
,nonspec_get_proj
)) )
493 gen_e_list_scanner scan
;
495 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
496 pat
= setst_proj_pat(c
,i
,proj_var
);
497 sv_add_ub_proj(sort_region
,v
,pat
);
499 gen_e_list_scan(sv_get_lbs(v
),&scan
);
500 while (gen_e_list_next(&scan
,&lb
))
502 setst_inclusion(lb
,pat
);
508 else if (setst_is_union(e
))
510 if( (proj
= nonspec_get_proj(setst_get_proj_cache(e
))) )
515 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
516 pat
= setst_proj_pat(c
,i
,proj_var
);
518 setst_set_proj_cache(e
,pat
);
520 setst_inclusion(e
,pat
);
527 proj_var
= get_proj_var(c
->sig
[i
].sort
,FALSE
);
528 pat
= setst_proj_pat(c
,i
,proj_var
);
529 setst_inclusion(e
,pat
);
534 static void setif_con_match(gen_e e1
, gen_e e2
)
536 // Case where e1 is a constructor expression and e2 is a proj_pat
537 if (pat_match(((setif_term
)e2
)->type
,((setif_term
)e1
)->type
))
539 cons_expr c
= (cons_expr
)e1
;
540 proj_pat p
= (proj_pat
)e2
;
543 if (c
->sig
[i
].variance
== vnc_pos
)
544 call_inclusion_fn(c
->exps
[i
],p
->exp
);
545 else if (c
->sig
[i
].variance
== vnc_neg
)
546 call_inclusion_fn(p
->exp
,c
->exps
[i
]);
548 call_unify_fn(c
->exps
[i
],p
->exp
);
550 else if (setif_is_pat(e2
))
555 // Case where e1 and e2 are constructor expressions
558 cons_expr c1
= (cons_expr
)e1
,
561 if (c1
->type
!= c2
->type
)
562 failure("Constructor mismatch\n");
566 for (i
= 0; i
< c1
->arity
; i
++)
568 if (c1
->sig
[i
].variance
== vnc_pos
)
569 call_inclusion_fn(e1
,e2
);
570 else if (c1
->sig
[i
].variance
== vnc_neg
)
571 call_inclusion_fn(e2
,e1
);
573 call_unify_fn(e1
,e2
);
580 static void setst_con_match(gen_e e1
, gen_e e2
)
582 // Case where e1 is a constructor expression and e2 is a proj_pat
583 if (pat_match(((setst_term
)e2
)->type
,((setst_term
)e1
)->type
))
585 cons_expr c
= (cons_expr
)e1
;
586 proj_pat p
= (proj_pat
)e2
;
589 if (c
->sig
[i
].variance
== vnc_pos
)
590 call_inclusion_fn(c
->exps
[i
],p
->exp
);
591 else if (c
->sig
[i
].variance
== vnc_neg
)
592 call_inclusion_fn(p
->exp
,c
->exps
[i
]);
594 call_unify_fn(c
->exps
[i
],p
->exp
);
596 else if (setst_is_pat(e2
))
601 // Case where e1 and e2 are constructor expressions
604 cons_expr c1
= (cons_expr
)e1
,
607 if (c1
->type
!= c2
->type
)
608 failure("Constructor mismatch\n");
612 for (i
= 0; i
< c1
->arity
; i
++)
614 if (c1
->sig
[i
].variance
== vnc_pos
)
615 call_inclusion_fn(e1
,e2
);
616 else if (c1
->sig
[i
].variance
== vnc_neg
)
617 call_inclusion_fn(e2
,e1
);
619 call_unify_fn(e1
,e2
);
626 // given x <= proj(c,i,e)
627 // proj_merge(region,e,get_proj_i_arg,fresh_large_fn_ptr,
628 // sort_inclusion_fn_ptr,set_inclusion)
629 static bool nonspec_res_proj(set_var v1
,gen_e e2
)
631 proj_pat projection_pat
= (proj_pat
)e2
;
633 gen_e
setif_get_proj(gen_e_list arg1
)
635 gen_e_list_scanner scan
;
639 gen_e_list_scan(arg1
,&scan
);
640 while(gen_e_list_next(&scan
,&temp
))
642 pat
= (proj_pat
)temp
;
643 if ( pat
->type
== ((setif_term
)e2
)->type
&&
644 pat
->i
== ((proj_pat
)e2
)->i
)
650 gen_e
fresh_large(void)
652 return get_proj_var( ((proj_pat
)e2
)->exp
->sort
,TRUE
);
655 bool sort_inclusion(gen_e e1
, gen_e e2
)
657 if ( projection_pat
->variance
== vnc_pos
)
658 return call_inclusion_fn(e1
,e2
);
659 else if ( projection_pat
->variance
== vnc_neg
)
660 return call_inclusion_fn(e2
,e1
);
662 return call_unify_fn(e1
,e2
);
665 gen_e
proj_con(gen_e e
)
667 return make_proj_pat( ((proj_pat
)e2
)->c
, ((proj_pat
)e2
)->i
,e
);
670 return setif_proj_merge(setif_region
,v1
,((proj_pat
)e2
)->exp
,
671 setif_get_proj
,proj_con
,
672 fresh_large
,sort_inclusion
,
673 call_setif_inclusion
);
678 void call_setif_inclusion(gen_e e1
,gen_e e2
)
680 setif_inclusion(setif_con_match
,setif_res_proj
,e1
,e2
);
683 void call_setif_unify(gen_e e1
, gen_e e2
)
685 setif_inclusion(setif_con_match
,setif_res_proj
,e1
,e2
);
686 setif_inclusion(setif_con_match
,setif_res_proj
,e2
,e1
);
689 void call_setst_inclusion(gen_e e1
, gen_e e2
)
691 setst_inclusion(setst_con_match
,e1
,e2
);
694 void call_setst_unify(gen_e e1
, gen_e e2
)
696 setst_inclusion(setst_con_match
,e1
,e2
);
697 setst_inclusion(setst_con_match
,e2
,e1
);
700 void call_flowrow_inclusion(gen_e e1
,gen_e e2
)
703 if ( (e1
->sort
!= flowrow_sort
) || (e2
->sort
!= flowrow_sort
) )
704 failure("Constraint system is not well-sorted\n");
706 if ( flowrow_base_sort(e1
) != flowrow_base_sert(e2
))
707 failure("Constraint system is not well-sorted\n");
710 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e1
,e2
);
713 void call_flowrow_unify(gen_e e1
, gen_e e2
)
715 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e1
,e2
);
716 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e2
,e1
);
719 static void term_con_match(gen_e e1
, gen_e e2
)
721 cons_expr c1
= (cons_expr
)e1
,
724 if (c1
->type
!= c2
->type
)
725 failure("Constructor mismatch\n");
729 for (i
= 0; i
< c1
->arity
; i
++)
731 call_unify_fn(e1
,e2
);
737 static void term_occurs(term_var v
, gen_e e
)
739 gen_e ecr
= term_get_ecr(e
);
741 if (((gen_term
)ecr
)->type
== VAR_TYPE
)
742 return ( term_get_stamp((gen_e
)v
) == term_get_stamp(e
) );
744 else if (((gen_term
)ecr
)->type
>= 10)
746 cons_expr c_e
= (cons_expr
) e
;
748 for (int i
= 0; i
< arity
; i
++)
750 if (term_occurs(v
,c
->exps
[i
]))
758 void call_term_unify(gen_e e1
, gen_e e2
)
760 term_unify(term_con_match
,term_occurs
,e1
,e2
);
763 void call_term_cunify(gen_e e1
, gen_e e2
)
765 term_cunify(term_con_match
,term_occurs
,e1
,e2
);
769 static void call_inclusion_fn(gen_e e1
, gen_e e2
)
775 setif_inclusion(setif_con_match
,setif_res_proj
,e1
,e2
);
780 setst_inclusion(setst_con_match
,e1
,e2
);
785 term_unify(term_con_match
,term_occurs
,e1
,e2
);
791 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e1
,e2
);
795 fail("Unmatched sort in call inclusion\n");
799 static bool call_unify_fn(gen_e e1
, gen_e e2
)
806 setif_inclusion(setif_con_match
,setif_res_proj
,e1
,e2
);
807 setif_inclusion(setif_con_match
,setif_res_proj
,e2
,e1
);
812 setst_inclusion(setst_con_match
,e1
,e2
);
813 setst_inclusion(setst_con_match
,e2
,e1
);
818 term_unify(term_con_match
,term_occurs
,e1
,e2
);
824 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e1
,e2
);
825 flowrow_inclusion(fresh
,get_stamp
,field_incl
,zero_elem
,e2
,e1
);
829 fail("Unmatched sort in call inclusion\n");
833 void nonspec_init(void)
841 void nonspec_reset(void)
849 void expr_print(FILE *f
,gen_e e
)