apaam/mlpack
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

started on the disjuction compiler

Browse Source
This commit is contained in:
sooraj
2008-07-02 04:18:11 +00:00
parent c5f2e340b9
commit ad403311ef
9 changed files with 63 additions and 69 deletions
Download Patch File Download Diff File Expand all files Collapse all files
tyl/src/examples.ml
+1 -1
View File
@@ -39,7 +39,7 @@ let diet =
(* boolean examples *)
let [b1;b2] = map name ["b1";"b2"]
let (b1,b2) = (name "b1",name "b2")
let dlf_example =
minimize (x + w)
tyl/src/tyl/mp/ast.ml
+14 -16
View File
@@ -6,7 +6,7 @@
c - prop
z - prop type
x - variable/id
cs,xts - plural (sets/lists of things)
cs,xs - plural (sets/lists of things)
*)
open List
@@ -49,18 +49,16 @@ type prop =
type prog =
| PMain of direction * ((Id.t * typ) list) * expr * prop
module Context = struct
type t = (Id.t * typ) list
let empty = []
let add ctxt x t = (x,t)::ctxt
let fromList xts = xts
let coarseContains ctxt x t =
let coarseEqual (x',t') = Id.equal x x' &&
match t,t' with
| TReal _ , TReal _ -> true
| TBool _ , TBool _ -> true
| _ -> false
in
exists coarseEqual ctxt
let lookup ctxt x = snd (find (fun (x',_) -> Id.equal x x') ctxt)
end
type context = (Id.t * typ) list
let coarseContains ctxt x t =
let coarseEqual (x',t') = Id.equal x x' &&
match t,t' with
| TReal _ , TReal _ -> true
| TBool _ , TBool _ -> true
| _ -> false
in
exists coarseEqual ctxt
(* pre: context contains x ; fails otherwise *)
let lookup ctxt x = snd (find (fun (x',_) -> Id.equal x x') ctxt)
tyl/src/tyl/mp/ast.mli
+3 -8
View File
@@ -33,11 +33,6 @@ type prop =
type prog =
| PMain of direction * ((Id.t * typ) list) * expr * prop
module Context : sig
type t
val empty : t
val add : t -> Id.t -> typ -> t
val fromList : (Id.t * typ) list -> t
val coarseContains : t -> Id.t -> typ -> bool
val lookup : t -> Id.t -> typ
end
type context = (Id.t * typ) list
val coarseContains : context -> Id.t -> typ -> bool
val lookup : context -> Id.t -> typ
tyl/src/tyl/mp/compiler.ml
+22 -15
View File
@@ -4,7 +4,6 @@ open Vars
open Wf
open Cnf
module C = Context
module S = Id.Set
module E = Edsl
@@ -13,6 +12,8 @@ let compileType t = match t with
| TBool (Some a) -> let b = if a then 1 else 0 in E.discrete b b
| _ -> t (* numeric types are left unchanged *)
let compileContext ctxt = map (fun (x,t) -> (x,compileType t)) ctxt
let rec compileDLF e =
assert (isDLF e) ;
match e with
@@ -34,19 +35,19 @@ let rec compileProp ctxt c =
| CPropOp (Conj,cs) -> CPropOp (Conj, map (compileProp ctxt) cs)
| CQuant (Exists,x,t,c) ->
let t' = compileType t in
let c' = compileProp (C.add ctxt x t') c in
let c' = compileProp ((x,t')::ctxt) c in
CQuant (Exists,x,t',c')
and compileConj e =
assert (isConj e) ;
match e with
| EBinaryOp (And,e1,e2) ->
let c1 = compileProp C.empty (E.isTrue e1) in
let c2 = compileProp C.empty (E.isTrue e2) in
let c1 = compileProp [] (E.isTrue e1) in
let c2 = compileProp [] (E.isTrue e2) in
E.(/|) c1 c2
| _ -> assert false
and typeAsProp (x',t) = let x = EVar x' in
and typeAsBoundingProp (x',t) = let x = EVar x' in
match t with
| TReal (Continuous (Some lo, Some hi)) -> E.(/|) (E.(<=) (E.litR lo) x) (E.(<=) x (E.litR hi))
| TReal (Continuous (Some lo, None )) -> (E.(<=) (E.litR lo) x)
@@ -60,10 +61,10 @@ and typeAsProp (x',t) = let x = EVar x' in
| TBool (Some false) -> E.isTrue (E.not x)
| TBool None -> E.propT
and typesAsProp ctxt c =
and addBoundingProps ctxt c =
let xs = S.elements (freeVarsc c) in
let ts = map (C.lookup ctxt) xs in
let cs = map typeAsProp (combine xs ts) in
let ts = map (lookup ctxt) xs in
let cs = map typeAsBoundingProp (combine xs ts) in
CPropOp (Conj,c::cs)
(* pre: e and e' are numeric expressions *)
@@ -102,12 +103,18 @@ and scalec e c = match c with
and compileDisj ctxt c =
assert (disjVarsBounded ctxt c) ;
match c with
| CPropOp (Disj,cs) -> assert false
| CPropOp (Disj,cs) ->
let cs' = map (compileProp ctxt) cs in
let ctxt' = compileContext ctxt in
let cs'' = map (addBoundingProps ctxt') cs' in
let xss = assert false in
let ys = assert false in
let cs''' = map () cs'' in
assert false
| _ -> failwith "compileDisj: proposition is not a disjunction"
let compile (PMain (d,xts,e,c) as p) =
let ctxt = C.fromList xts in
assert (isMP p && disjVarsBounded ctxt c) ;
let xts' = map (fun (x,t) -> (x,compileType t)) xts in
let c' = compileProp ctxt c in
PMain (d,xts',e,c')
let compile (PMain (d,ctxt,e,c) as p) =
assert (isMP p && disjVarsBounded ctxt c) ;
let ctxt' = compileContext ctxt in
let c' = compileProp ctxt c in
PMain (d,ctxt',e,c')
tyl/src/tyl/mp/edsl.ml
+3 -3
View File
@@ -38,9 +38,9 @@ let exists (EVar x,t) c = CQuant (Exists,x,t,c)
let where = 0
let subject_to = 0
let optimize d e ets c =
let xts = List.map (fun (EVar x,t) -> (x,t)) ets in
PMain (d,xts,e,c)
let optimize d e ctxt c =
let ctxt' = List.map (fun (EVar x,t) -> (x,t)) ctxt in
PMain (d,ctxt',e,c)
let minimize e _ ets _ c = optimize Min e ets c
let maximize e _ ets _ c = optimize Max e ets c
tyl/src/tyl/mp/show.ml
+9 -13
View File
@@ -1,5 +1,5 @@
open Ast
open Printf
open Format
open List
let showt t = match t with
@@ -22,13 +22,9 @@ let rec showe e = match e with
| EConst (Real r) -> sprintf "%f" r
| EConst (Int n) -> sprintf "%d" n
| EUnaryOp (op,e') ->
sprintf "(%s%s)"
(match op with Neg -> "-" | Not -> "not ")
(showe e')
| EBinaryOp (Mult,e1,e2) ->
sprintf "%s * %s" (showe e1) (showe e2)
sprintf "%s%s" (match op with Neg -> "-" | Not -> "not ") (showe e')
| EBinaryOp (op,e1,e2) ->
sprintf "(%s %s %s)"
sprintf "(@[%s %s@ %s@])"
(showe e1)
(match op with Plus -> "+" | Minus -> "-" | Mult -> "*" | Or -> "||" | And -> "&&")
(showe e2)
@@ -37,19 +33,19 @@ let showxt (x,t) = sprintf "%s:%s" (Id.toString x) (showt t)
let rec showc c = match c with
| CBoolVal b -> if b then "T" else "F"
| CIsTrue e -> sprintf "(isTrue %s)" (showe e)
| CIsTrue e -> sprintf "(@[isTrue %s@])" (showe e)
| CNumRel (op,e1,e2) ->
sprintf "(%s %s %s)"
sprintf "(@[%s %s %s@])"
(showe e1)
(match op with Lte -> "<=" | Equal -> "==" | Gte -> ">=")
(showe e2)
| CPropOp (op,cs) ->
let opstr = match op with Disj -> " disj " | Conj -> " conj " in
"(" ^ String.concat ("\n"^opstr) (map showc cs) ^ ")"
| CQuant (Exists,x,t,c) -> sprintf "(exists %s . %s)" (showxt (x,t)) (showc c)
sprintf "(@[%s@])" (String.concat opstr (map showc cs))
| CQuant (Exists,x,t,c) -> sprintf "(@[exists %s .@ %s@])" (showxt (x,t)) (showc c)
let showp p = match p with
| PMain (d,xts,e,c) ->
let vars = String.concat "\n" (map showxt xts) in
| PMain (d,ctxt,e,c) ->
let vars = String.concat "\n" (map showxt ctxt) in
let dirxn = (match d with Min -> "min" | Max -> "max") in
sprintf "%s\n\n%s %s\nsubject_to %s" vars dirxn (showe e) (showc c)
tyl/src/tyl/mp/vars.ml
+2 -2
View File
@@ -5,7 +5,7 @@ module S = Id.Set
let (--) = S.diff
let set_of_list xs = fold_left (fun s x -> S.add x s) S.empty xs
let getIds xts = set_of_list (fst (split xts))
let getIds ctxt = set_of_list (fst (split ctxt))
let rec freeVarse e = match e with
| EVar x -> S.singleton x
@@ -21,7 +21,7 @@ let rec freeVarsc c = match c with
| CQuant (_,x,_,c') -> freeVarsc c' -- S.singleton x
let freeVarsp p = match p with
| PMain (_,xts,e,c) -> S.union' [freeVarse e; freeVarsc c] -- getIds xts
| PMain (_,ctxt,e,c) -> S.union' [freeVarse e; freeVarsc c] -- getIds ctxt
let isClosede e = S.is_empty (freeVarse e)
let isClosedc c = S.is_empty (freeVarsc c)
tyl/src/tyl/mp/wf.ml
+6 -8
View File
@@ -2,7 +2,6 @@ open Ast
open List
open Vars
module C = Context
module E = Edsl
module S = Id.Set
@@ -13,7 +12,7 @@ let isType t = match t with
| _ -> true
let rec isOfType ctxt e t = match e,t with
| EVar x , _ -> C.coarseContains ctxt x t
| EVar x , _ -> coarseContains ctxt x t
| EConst (Bool _) , TBool _ -> true
| EConst (Int _) , TReal _ -> true
| EConst (Real _) , TReal _ -> true
@@ -31,12 +30,11 @@ let rec isProp ctxt c = match c with
| CIsTrue e -> isOfType ctxt e E.bool
| CNumRel (_,e1,e2) -> isOfType ctxt e1 E.real && isOfType ctxt e2 E.real
| CPropOp (_,cs) -> for_all (isProp ctxt) cs
| CQuant (_,x,t,c') -> isType t && isProp (C.add ctxt x t) c'
| CQuant (_,x,t,c') -> isType t && isProp ((x,t)::ctxt) c'
let isMP p = match p with
| PMain (_,xts,e,c) ->
let ctxt = C.fromList xts in
for_all (fun (_,t) -> isType t) xts && isOfType ctxt e E.real && isProp ctxt c
| PMain (_,ctxt,e,c) ->
for_all (fun (_,t) -> isType t) ctxt && isOfType ctxt e E.real && isProp ctxt c
(* misc type operations *)
@@ -60,7 +58,7 @@ let rec disjVarsBounded ctxt c = match c with
| CNumRel _ -> true
| CPropOp (Disj,cs) ->
let xs = S.elements (S.union' (map freeVarsc cs)) in
let ts = map (C.lookup ctxt) xs in
let ts = map (lookup ctxt) xs in
for_all bounded ts && for_all existVarsBounded cs
| CPropOp (Conj,cs) -> for_all (disjVarsBounded ctxt) cs
| CQuant (Exists,x,t,c') -> disjVarsBounded (C.add ctxt x t) c'
| CQuant (Exists,x,t,c') -> disjVarsBounded ((x,t)::ctxt) c'
tyl/src/tyl/mp/wf.mli
+3 -3
View File
@@ -1,10 +1,10 @@
open Ast
val isType : typ -> bool
val isOfType : Context.t -> expr -> typ -> bool
val isProp : Context.t -> prop -> bool
val isOfType : context -> expr -> typ -> bool
val isProp : context -> prop -> bool
val isMP : prog -> bool
val bounded : typ -> bool
val existVarsBounded : prop -> bool
val disjVarsBounded : Context.t -> prop -> bool
val disjVarsBounded : context -> prop -> bool