diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/command/fi2si.ml /tmp/ground_tram-0.9.3-new/src/command/fi2si.ml --- /tmp/ground_tram-0.9.3-org/src/command/fi2si.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/command/fi2si.ml 2013-02-19 07:56:49.000000000 +0900 @@ -11,6 +11,26 @@ : flat node id on the view (integer) *.ei: editinfo file + Extended usage (vidualize traced nodes via DOT files): + + 1. Forward execution and trace information collection + % fwd_uncal -ge -sb -cl -zn -fi -np -sa -t -rw -as -db class.dot -uq class2table.unql -dot \ + table.dot -xg table.xg -ei table.ei + + 2. Backward tracing (from target node 1) + % fi2si -ipt 1 -ei table.ei -tr -db class.dot -odot table.dot + + 3. View dot files that are automatically generated from dots specified by -db and -odot + in which traced nodes are highlighted + % (b)dotty class_highlighted.dot & + % (b)dotty table_highlighted.dot & + + 4. Forward tracing (from source node 1) + % fi2si -sv 1 -ei table.ei -db class.dot -odot table.dot + + 5. Reload highlighted dot file by typing 'L' on (b)dotty. + + 6. Repeat step 2 or 4 followed by step 5. *) open Format @@ -22,25 +42,43 @@ open TestUnCALutil open Version open Fputil +open ExtSetMap +open Dotutil type bwd_config = { mutable ei_file : string; (* editinfo file *) - mutable ipt_node : int; (* flat node ID *) + mutable ipt_node : int; (* flat node ID in the view *) + mutable src_node : int; (* flat node ID in the source *) + mutable tr_flag : bool; (* trace back to source node ID *) + mutable pt_flag : bool; (* print trace table *) + mutable idot_file : string; (* input dot file *) + mutable odot_file : string; (* output dot file *) } -let default_config = { ei_file = ""; ipt_node = (-1); } +let default_config = { ei_file = ""; ipt_node = (-1); + tr_flag = false; + pt_flag = false; + idot_file = ""; + odot_file = ""; + src_node = (-1); + } let speclist = let cf = default_config in Arg.align [ - ("-ei", Arg.String (fun s->cf.ei_file <-s), " editinfo produced by forward trans."); - ("-ipt", Arg.Int (fun k->cf.ipt_node<-k), " flat node ID in the view"); + ("-ei", Arg.String (fun s->cf.ei_file <-s), " editinfo produced by forward trans."); + ("-ipt", Arg.Int (fun k->cf.ipt_node<-k), " flat node ID in the view"); + ("-tr", Arg.Unit (fun()->cf.tr_flag<-true), " trace back to source node ID"); + ("-sv", Arg.Int (fun k->cf.src_node<-k), " flat node ID in the source"); + ("-pt", Arg.Unit (fun()->cf.pt_flag<-true), " print entire trace correspondence"); + ("-db", Arg.String (fun s->cf.idot_file <-s), " input dot file (optional)"); + ("-odot",Arg.String (fun s->cf.odot_file <-s), " output dot file (optional)"); ] let speclist = add_version_spec speclist -let usage_msg = "Usage: "^Sys.executable_name^" -ipt node -ei fwd_result.ei" +let usage_msg = "Usage: "^Sys.executable_name^" -ei fwd_result.ei [-ipt node [-tr]] [-pt] [-sv node] [-db db.dot] [-odot result.dot]" let read_args () = let cf = default_config in @@ -55,17 +93,66 @@ let _ = print_version () in (* check arguments *) if cf.ei_file = "" then failwith_msg "editinfo file unspecified." - else if cf.ipt_node = -1 then failwith_msg "flat ID unspecified or invalid." else let ei = file2edinfo cf.ei_file in - let _ = skolemBulk := ei.sbulk in - let _ = escapeApnd := ei.eapnd in - let _ = cycleSemanticsOriginal := ei.cycorig in - let _ = saUnreach := ei.saunrch in - let vS = MapofVtx.find (Bid cf.ipt_node) ei.vm.mapV in - let vL = SetofVtx.elements vS in + let _ = skolemBulk := ei.sbulk in + let _ = escapeApnd := ei.eapnd in + let _ = cycleSemanticsOriginal := ei.cycorig in + let _ = saUnreach := ei.saunrch in + let expand_vtx v = MapofVtx.find v ei.vm.mapV in + let tr_list l = List.concat (List.map (fun v -> try [trace v] with _ -> []) l) in + let tr_set s = SetofVtx.setmap (fun v -> + try SetofVtx.singleton (trace v) with _ -> SetofVtx.empty) s in let pr_list_newline pr_elem fmt xs = match xs with [] -> () | x::xs -> pr_elem fmt x; List.iter (fprintf fmt "\n%a" pr_elem) xs in - Format.fprintf Format.std_formatter "%a@." (pr_list_newline pp_skolemV) vL + let pr_node_list_node_per_line node_list = + Format.fprintf Format.std_formatter "%a@." (pr_list_newline pp_skolemV) node_list in + (* generate DOT file with specified node highlighted *) + let highlight_nodes fname vS = + let traced_node_color = "red" in + let suffix = get_suffix fname in + let prefix = Filename.chop_extension fname in + let hl_dotfile = prefix ^ "_" ^ "highlighted" ^ "." ^ suffix in + let org_dot = parseDot_file fname in + let d = addAttrToNodeSet org_dot vS "fontcolor" traced_node_color in + let d = addAttrToNodeSet d vS "color" traced_node_color in + (* dispD_gc d *) + dumpDot ~prefix_n:false d hl_dotfile in + let bwd_vtx : (vtx -> SetofVtx.t) = tr_set @@ expand_vtx in + let bwd_MapofVtx = vtxSet2Map bwd_vtx ei.g_edit.v in + let invert_MapofVtx2SVtx = + MapofVtx.invert_m2s (module SetofVtx : Set.S with type elt = vtx and type t = SetofVtx.t) in + let fwd_MapofVtx = invert_MapofVtx2SVtx bwd_MapofVtx in + let fwd_vtx v = MapofVtx.find v fwd_MapofVtx in + if cf.ipt_node <> -1 then begin + let v = (Bid cf.ipt_node) in + let vS = expand_vtx v in + let vL = SetofVtx.elements vS in + if (not cf.tr_flag) then begin pr_node_list_node_per_line vL end; + if cf.tr_flag then begin + let svL = SetofVtx.elements (SetofVtx.fromList (tr_list vL)) in + pr_node_list_node_per_line svL; + if cf.odot_file <> "" then highlight_nodes cf.odot_file (SetofVtx.singleton v); + if cf.idot_file <> "" then highlight_nodes cf.idot_file (SetofVtx.fromList svL); + end; + end; + if cf.src_node <> -1 then begin + let v = (Bid cf.src_node) in + let vS = fwd_vtx v in + if cf.idot_file <> "" then highlight_nodes cf.idot_file (SetofVtx.singleton v); + if cf.odot_file <> "" then highlight_nodes cf.odot_file vS; + end; + if cf.pt_flag then begin + MapofVtx.iter (fun k v -> + Format.fprintf Format.std_formatter "%a -> %a@." pp_skolemV k (SetofVtx.pr pp_skolemV) v) fwd_MapofVtx; + MapofVtx.iter (fun k v -> + Format.fprintf Format.std_formatter "%a <- %a@." (SetofVtx.pr pp_skolemV) v pp_skolemV k) bwd_MapofVtx + end + (* + let vL = SetofVtx.elements ei.g_edit.v in + List.iter (fun v -> + let sv = tr_set (expand_vtx v) in + Format.fprintf Format.std_formatter "%a <- %a@." (SetofVtx.pr pp_skolemV) sv pp_skolemV v) vL + *) diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/datamodel/printUnCALDM.ml /tmp/ground_tram-0.9.3-new/src/datamodel/printUnCALDM.ml --- /tmp/ground_tram-0.9.3-org/src/datamodel/printUnCALDM.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/datamodel/printUnCALDM.ml 2013-02-19 07:56:49.000000000 +0900 @@ -103,10 +103,12 @@ let pr_MapofPVtxToSEdge = MapofPVtx.pr (pr_pair pr_vtx pr_vtx) pr_SetofEdge +let pr_MapofEdgeToEdge = MapofEdge.pr pr_edge pr_edge let pr_MapofEdgeToGraph = MapofEdge.pr pr_edge pr_graph let pr_MapofEdgeToSEdge = MapofEdge.pr pr_edge pr_SetofEdge + (* loading and storing graphs using Marshal standard library *) (* graph to file *) let g2file (g:graph) (file:string) : unit = diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/datamodel/unCALDMutil.ml /tmp/ground_tram-0.9.3-new/src/datamodel/unCALDMutil.ml --- /tmp/ground_tram-0.9.3-org/src/datamodel/unCALDMutil.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/datamodel/unCALDMutil.ml 2013-02-19 07:56:49.000000000 +0900 @@ -11,6 +11,7 @@ open UnCALDM open UnCAL open PrintUnCALDM +open PrintUnCAL open Fputil open ExtSetMap @@ -840,7 +841,7 @@ srcV.omarks <- SetofMarker.union dstV.omarks srcV.omarks; (* migrate outgoing edges of dstV to srcV *) SetofMEdge.iter (fun mE' -> - if (create_viewmaps && (mE'.xlabel <> ALEps)) + if (create_viewmaps (* && (mE'.xlabel <> ALEps) *)) then viewmaps_migrate_1edge ~e_to: (srcV.id,mE'.xlabel,mE'.destV) ~e_from:(dstV.id,mE'.xlabel,mE'.destV) vm; @@ -849,7 +850,7 @@ ) dstV.outgoE; (* migrate incoming edges of dstV to srcV *) SetofMEdge.iter (fun mE' -> - if (create_viewmaps && (mE'.xlabel <> ALEps)) + if (create_viewmaps (* && (mE'.xlabel <> ALEps) *)) then viewmaps_migrate_1edge ~e_to: (mE'.sourceV,mE'.xlabel,srcV.id) ~e_from:(mE'.sourceV,mE'.xlabel,dstV.id) vm; @@ -1370,6 +1371,7 @@ | ALSub -> i1 - i2 | ALMul -> i1 * i2 | ALDiv -> i1 / i2 + | ALMod -> i1 mod i2 | ALConc -> failwith "evall_bin: can't concatenate integers with ^" ) | (ALFlt f1,op ,ALFlt f2) -> @@ -1417,6 +1419,36 @@ let clean_id ?start_id g = let (g,mapV,end_id) = clean_id_aux ?start_id g in g + +(** Split graph g at node v with marker m. + Introduce new node v' and attach new input marker m' to it. + Original outgoing edges and output markers of v are moved to v', + and output marker m' is attached to v instead. + Original input markers of v remain. *) +let split_graph (g:graph) (v:vtx) (v':vtx) (m':marker) = + let {v=vS;e=eS;i=iS;o=oS} = g in + (* check overlap *) + let (imS,omS) = fsplit (inputMarkers,outputMarkers) g in + let mS = SetofMarker.union imS omS in + if SetofMarker.mem m' mS then + failwith ("split_graph: given marker " ^ (toStr pr_marker m') ^ " already exists") + else if SetofVtx.mem v' vS then + failwith ("split_graph: given node " ^ (toStr pr_vtx v') ^ " already exists") + else + (* move output marker of v to v' *) + let oS = SetofOnodeR.map (fun (u,m) -> ((if u = v then v' else u),m)) oS in + (* move outgoing edges of v to v' *) + let eS = SetofEdge.map (fun (u,l,w) -> ((if u = v then v' else u), l, w)) eS in + (* assign output marker m' to v *) + let oS = SetofOnodeR.add (v,m') oS in + (* assign input marker m' to v' *) + let iS = SetofInodeR.add (m',v') iS in + (* register node v' *) + let vS = SetofVtx.add v' vS in + {v=vS;e=eS;i=iS;o=oS} + + + (** unused *) let dumpableG (g:graph) = let is_cleaned : vtx -> bool = function diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/datamodel/unCALDMutil.mli /tmp/ground_tram-0.9.3-new/src/datamodel/unCALDMutil.mli --- /tmp/ground_tram-0.9.3-org/src/datamodel/unCALDMutil.mli 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/datamodel/unCALDMutil.mli 2013-02-19 07:56:49.000000000 +0900 @@ -167,8 +167,12 @@ val remove_eps_ec1 : graph -> graph val remove_eps : graph -> graph (* structured id elimination *) -val clean_id_aux : ?start_id:int -> graph -> graph * (int, 'a) sid MapofVtx.t * int +val clean_id_aux : ?start_id:int -> graph -> graph * vtx MapofVtx.t * int val clean_id : ?start_id:int -> graph -> graph + +(* graph decomposition *) +val split_graph : graph -> vtx -> vtx -> marker -> graph + (* extracting difference *) val graph_diff_aux : graph -> graph -> (graph * SetofVtx.t * SetofVtx.t * SetofEdge.t * SetofEdge.t * SetofEdge.t * ((edge * edge) list)) diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/dot/lexDot.mll /tmp/ground_tram-0.9.3-new/src/dot/lexDot.mll --- /tmp/ground_tram-0.9.3-org/src/dot/lexDot.mll 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/dot/lexDot.mll 2013-02-19 07:56:49.000000000 +0900 @@ -74,6 +74,7 @@ (* | { ESCAPED(lexeme lexbuf) } *) | bool { BOOL(bool_of_string(lexeme lexbuf)) } | digits '.' digits { FLOAT(float_of_string(lexeme lexbuf)) } +| digits '.' { FLOAT(float_of_string(lexeme lexbuf)) } | sn_digits { INT(int_of_string(lexeme lexbuf)) } | dotty_node_id { DOTTY_NODE_ID(int_of_string(strip1 (lexeme lexbuf))) } | letters { LETTERS(lexeme lexbuf) } diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/eval/g2UnCAL.ml /tmp/ground_tram-0.9.3-new/src/eval/g2UnCAL.ml --- /tmp/ground_tram-0.9.3-org/src/eval/g2UnCAL.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/eval/g2UnCAL.ml 2013-02-19 07:56:49.000000000 +0900 @@ -67,94 +67,74 @@ ,e) else e +(** Another reifier using tree with pointer representation. + Input graph is first decomposed at concluent points, + and then each component is recursively translated to UnCAL constructor + expression. Memoization is not necessary. *) let g2uncalT (g:graph) : 'a option aexpr = - (* more like tree representation. - confluence is represented by - &zNodeID U representation ... &zNodeID ... &zNodeID - It may violate the UnCAL graph model in that no output node should have - outgoing edges, but this representation has higher readability - *) - (** Known Issue **) - (** This function assumes previous naive implementation of remove_eps in which - source and destination node of every epsilon edge is glued together. - Therefore, it doesn't work correctly when unsafe-epsilon - (that fails to satisfy is_safe_eps predicate in UnCALDMutil.glue_safe_eps) - is included in the input graph. - It is recommended that remove_eps is applied to the input graph beforehand, - if you don't express epsilons at UnCAL level. **) - let g = clean_id g in (* normalize edge id to Bid of int *) let prefix = (* take marker that is largest in dictionary order *) let mS = SetofMarker.union (inputMarkers g) (outputMarkers g) in if SetofMarker.is_empty mS then "z" - else + else let inhabi = SetofMarker.max_elt mS in String.sub inhabi 1 ((String.length inhabi)-1) in let prefix = if prefix = "" then "z" else prefix in -(*let genMarker () : marker = Gensym.next ("&" ^ prefix) in *) - let selfCycle (g:graph) (v:vtx) : bool = - SetofEdge.fold (fun (_,_,v2) -> (||) (v = v2)) (outgoEdgeS g v) false in - let confluent (g:graph) (v:vtx) : bool = - ((SetofEdge.cardinal (incomEdgeS g v) > 1) || (selfCycle g v)) in + let (g,mapV,end_id) = clean_id_aux g in + let gid = GenId.current () in + (*let genMarker () : marker = Gensym.next ("&" ^ prefix) in *) + let incomBranches (g:graph) (v:vtx) = + let (imS,_) = markersV g v in (* set of input markers *) + let ieS = incomEdgeS g v in (* set of incoming edges *) + (imS,ieS) in + let confluent (g:graph) (v:vtx) : bool = + let (imS,ieS) = incomBranches g v in + let nib = SetofMarker.cardinal imS + SetofEdge.cardinal ieS in (* incoming branches *) + (nib > 1) in let v2m = function - (Bid i) (* as v *) -> "&" ^ prefix ^ (string_of_int i) - (*let imS = fst (markersV g v) in - if SetofMarker.is_empty imS - then "&" ^ prefix ^ (string_of_int i) - else SetofMarker.choose imS *) - | _ -> failwith "g2uncal: normalize vtx id first" in - let rMapV = ref MapofVtx.empty in - let rec g2u (v:vtx) = - try (MapofVtx.find v !rMapV) with - Not_found -> - let me = AEOMrk (None,v2m v) in - rMapV := MapofVtx.add v me !rMapV; - let e' = (SetofMarker.fold (fun m ae'' -> - AEUni (None,AEOMrk (None,m),ae'')) (snd (markersV g v)) - (SetofEdge.fold (fun (_,l,vd) ae' -> - AEUni (None,AEEdg (None,ALLit (None,l),(g2u vd)),ae')) (outgoEdgeS g v) (AETEmp None)) - ) in - if confluent g v - then AEUni (None,me,e') - else e' - (* - SetofEdge.fold (fun (_,l,vd) ae' -> - AEUni (AEEdg (ALLit l, - try (MapofVtx.find vd !rMapV) with - Not_found -> - let me = AEOMrk (v2m vd) in - rMapV := MapofVtx.add vd me !rMapV; - let e' = (SetofMarker.fold (fun m ae'' -> - AEUni (AEOMrk m,ae'')) (snd (markersV g vd)) (g2u vd)) in - if SetofEdge.cardinal (incomEdgeS g vd) > 1 - then AEUni (me,e') - else e' - ),ae')) - (outgoEdgeS g v) AETEmp - *) - in - let dunion e1 e2 = match e1,e2 with - | AEGEmp _, e | e, AEGEmp _ -> e - | _ -> AEDUni(None,e1,e2) in - let remove_root = function - | AEIMrk(_,"&",e) -> e - | e -> e in - let cycle e = - let _, omk = qtype emptyEnv e in - if SetofMarker.is_empty omk then remove_root e else AECyc (None,e) in - let d = SetofMarker.fold - (fun m es -> dunion (AEIMrk (None,m, g2u (lookupI g m))) es) (inputMarkers g) (AEGEmp None) in - cycle (dunion d - (MapofVtx.fold - (fun v e es -> if confluent g v then dunion (AEIMrk(None,v2m v,e)) es else es) - !rMapV (AEGEmp None))) -(* let d = (SetofMarker.fold (fun m es -> *) -(* AEDUni (AEIMrk (m, g2u (lookupI g m)),es)) *) -(* (inputMarkers g) AEGEmp) in *) -(* AECyc (AEDUni (d, *) -(* MapofVtx.fold (fun v e es -> *) -(* if confluent g v *) -(* then AEDUni (AEIMrk (v2m v,e), es) *) -(* else es) !rMapV AEGEmp)) *) + (Bid i) -> "&" ^ prefix ^ (string_of_int i) + | _ -> failwith "g2uncalT: normalize vtx id first" in + (* shift the id sequence *) + let _ = GenId.set end_id in + (* split graph at confluent nodes *) + let imS_orig = inputMarkers g in + let g = SetofVtx.fold (fun v g_acc -> + if confluent g v then + let m' = v2m v in + let v' = newnode () in + split_graph g_acc v v' m' + else g_acc) g.v g in + let an = None in (* default annotation *) + let marker2u m = AEOMrk (an,m) in + let rec v2u (v:vtx) = + (* branches *) (* no revisiting happen after graph split *) + let oeS = outgoEdgeS g v in (* ougoing edges *) + let omS = snd (markersV g v) in (* output markers *) + let edge2u (_,l,v) = AEEdg (an,ALLit (an,l), v2u v) in + let uni e1 e2 = AEUni (an, e1, e2) in + let eS2u oeS = SetofEdge.hom1 uni edge2u oeS in + let mS2u omS = SetofMarker.hom1 uni marker2u omS in + match (SetofEdge.cardinal oeS,SetofMarker.cardinal omS) with + 0,0 -> AETEmp an + | 0,_ -> mS2u omS + | _,0 -> eS2u oeS + | _,_ -> AEUni (an, eS2u oeS, mS2u omS) in + let g2u (g:graph) = + let irS = g.i in + match (SetofInodeR.cardinal irS) with + 0 -> AEGEmp an + | _ -> + let ir2u (m,v) = AEIMrk (an,m, v2u v) in + let duni e1 e2 = AEDUni (an, e1,e2) in + let e = SetofInodeR.hom1 duni ir2u irS in + let e = AECyc (an, e) in + if !cycleSemanticsOriginal then + let project_e = SetofMarker.hom1 duni marker2u imS_orig in + AEApnd (an,project_e,e) + else e in + let e = g2u g in + (* restore id sequence *) + let _ = GenId.set gid in + e (* dump graph to file in *.uncal format eg: dumpG db "db.uncal" *) @@ -167,9 +147,8 @@ Format.pp_print_flush fmt (); (* flush buffer of pretty printer *) close_out oc -(* works like dumpG except that it generates tree-like form +(** works like dumpG except that it generates tree-like form with revisited node marked with markers *) -(** Known issue: Please refer to the comment for g2uncalT **) let dumpGT (g:graph) (file:string) : unit = let e = g2uncalT g in let oc = open_out file in diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/eval/unCALSA.ml /tmp/ground_tram-0.9.3-new/src/eval/unCALSA.ml --- /tmp/ground_tram-0.9.3-org/src/eval/unCALSA.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/eval/unCALSA.ml 2013-02-19 07:56:49.000000000 +0900 @@ -208,7 +208,7 @@ | ALBin (_,l1,op,l2) -> let (t1,t2) = mapT2 (qtype_lpat env) (l1,l2) in match op with - ALAdd | ALSub | ALMul | ALDiv -> + ALAdd | ALSub | ALMul | ALDiv | ALMod -> (match (t1,t2) with (SLUkn,SLUkn) -> SLUkn (* there's no way to represent numeric type in general *) | (SLEps,_ ) | (_, SLEps) -> failwith "qtype_lpat: non-numeric type operand" @@ -586,7 +586,7 @@ | SALBin (l1,op,l2) -> let (t1,t2) = (l1.ltype,l2.ltype) in match op with - ALAdd | ALSub | ALMul | ALDiv -> + ALAdd | ALSub | ALMul | ALDiv | ALMod -> (match (t1,t2) with (SLUkn,SLUkn) -> SLUkn (* there's no way to represent numeric type in general *) | (SLEps,_ ) | (_, SLEps) -> failwith "qtype_lpat: non-numeric type operand" @@ -916,6 +916,7 @@ | ALSub -> SALLit (ALInt (i1 - i2)) | ALMul -> SALLit (ALInt (i1 * i2)) | ALDiv -> SALLit (ALInt (i1 / i2)) + | ALMod -> SALLit (ALInt (i1 mod i2)) | ALConc -> lpat ) | (SALLit (ALFlt f1),op ,SALLit (ALFlt f2)) -> diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/schema/km3util.ml /tmp/ground_tram-0.9.3-new/src/schema/km3util.ml --- /tmp/ground_tram-0.9.3-org/src/schema/km3util.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/schema/km3util.ml 2013-02-19 07:56:49.000000000 +0900 @@ -5,6 +5,9 @@ * MIT Licensed - http://www.biglab.org/src/mit-license.txt * *) +(** + Utilities for KM3 schema validation + *) open Format open Print open ExtSetMap @@ -16,6 +19,24 @@ open PrintUnCALDM open UnCALDMutil +(** If true, debug write by dfprintf is enabled *) +let km3util_verbose = ref false + +(** Act as fprintf if {!km3util_verbose} flag is true. + Otherwise does nothing. *) +let dfprintf = + if !km3util_verbose + then fprintf + else ifprintf + +(** [dprintf ?flag] acts like printf except that it prints + nothing if [flag] or {!km3util_verbose} is false. + These values are checked at run-time. *) +let dprintf ?(verbose:bool = false) = + if (!km3util_verbose || verbose) + then Format.printf + else Format.ifprintf std_formatter + (* Dictionary for a metamodel structure *) type mm_dictionary = { classifier: classifier NameMap.t; @@ -28,14 +49,23 @@ pp_field "package" (pp_name_map_t pp_name_set_t) mmdic.package ] fmt +(** + [make_mm_dictionary mm] creates from metamodel [mm] a metamodel dictionary + which consists of: + classifier: map from classifier name to corresponding classifier. + all the classifiers are registered here regardless of + the package they belongs to. + package: map from package name to set of names of non-abstract classes in the package. +*) + let make_mm_dictionary (mm:metamodel) : mm_dictionary = - List.fold_left - (fun mmdic pkg -> - List.fold_left + List.fold_left (* for each package *) + (fun mmdic pkg -> + List.fold_left (* for each classifier in the list of classifiers in the package *) (fun mmdic clsf -> match clsf with | `klasse kls -> let package = - if kls.is_abstract then mmdic.package + if kls.is_abstract then mmdic.package (* don't register in the package map *) else let kset = try NameMap.find pkg.pname mmdic.package @@ -51,32 +81,68 @@ { classifier = NameMap.empty; package = NameMap.empty } mm +(* auxiliary pretty printer for debugging *) +let pp_just_or_once ppf = function + `just -> fprintf ppf "just" + | `once -> fprintf ppf "once" +let pp_Hashtbl_t pp_a pp_b fmt h = + fprintf fmt "@[<1>{"; + Hashtbl.iter (fun k v -> fprintf fmt "(%a => %a);" pp_a k pp_b v) h; + fprintf fmt "}@]" +let pp_string_just_or_once_hash ppf x = (pp_Hashtbl_t PrintKm3.pp_name pp_just_or_once) ppf x + (* Topological sort on class hierarchy and expanding features *) let klasse_expand (cdic:classifier NameMap.t) : classifier NameMap.t = + (* Memo table mapping kname to either `just or `once. + `just is used for circular inheritance detection + (if the memo hits with `just while expansion then aborts). + `once is used to store a class for which expansion succeeds + without circule detection *) let visited = Hashtbl.create 97 in + (* [visit kname kls expanded] + expands the classifier dictionary [expanded] with respect + to the class [kls]. [expanded] is the dictionary with expansion + thus far has been applied. + kname: name of the classifier [kls] + returns a pair of expanded dictionary and [kls] (as is) + *) let rec visit kname kls expanded = Hashtbl.add visited kname `just; + (* exp_kls: a pair of expanded classifier dictionary and classifier definition *) let exp_kls = + (* expand features of a class along its list of superclasses *) List.fold_left + (* exp: expanded classifier map (accumulated), kls: classifier having supertype supname, + supname: name of one of the supertypes *) (fun (exp,kls) supname -> - let sup = try begin match NameMap.find supname cdic with + dprintf "exp=%a@." (pp_name_map_t pp_classifier) exp; + dprintf "visited=%a@." pp_string_just_or_once_hash visited; + (* sup: definition of one of the supertypes of the class kls *) + let sup = try begin match NameMap.find supname (* cdic *) expanded with | `klasse kls -> kls - | _ -> failwith(sprintf "%s: not class name." supname) - end with Not_found -> + | _ -> (* Can't 'extend' a primitive data type *) + failwith(sprintf "%s: not class name." supname) + end with Not_found -> (* Can't extend nonexistent class *) failwith(sprintf "%s: unknown class name." supname) in let exp, sup = if Hashtbl.mem visited supname then if Hashtbl.find visited supname = `just then failwith(sprintf "%s <=> %s: Circular inheritance detected." supname kname) - else exp, sup - else visit supname sup exp in + else exp, sup (* if already visited in different recursion or iteration + without circular detection, then returm the memoized super class *) + else visit supname sup exp (* traverse the super class recursively *) + in (* override features of supertypes *) let features = NameMap.fold NameMap.add kls.features sup.features in - let clsf = `klasse { kls with features = features } in - NameMap.add kname clsf exp, kls) (expanded,kls) kls.supertypes in + let kls' = { kls with features = features } in + let clsf = `klasse kls' in + (* replace the entry of kname with its class definition updated with expanded features *) + NameMap.add kname clsf exp, (* kls *) kls') (expanded,kls) kls.supertypes in Hashtbl.add visited kname `once; exp_kls in + (* For each class, expand its definition by their superclasses and update + the classifier dictionary with these expansions. *) NameMap.fold (fun name clsf exp -> match clsf with | `klasse kls -> fst (visit name kls exp) | _ -> exp) cdic cdic @@ -104,7 +170,13 @@ module VMap = Map.Make(Vertex) module VSet = Set.Make(Vertex) module AMap = Map.Make(struct type t = allit let compare = compare end) +(** Map of {!UnCALDM.vtx} to map of {!UnCAL.allit} to set of {!UnCALDM.vtx}. + Example: [AMap.find l VMap.find v] returns set of destination + vtx accessible from vertex [v] via label [l]. *) type edges = VSet.t AMap.t VMap.t (* source -> allit -> PowSet(destination) *) +(** Type for the map of {!UnCALDM.vtx} to {!Km3.classifier}. Used + in the validation process to memoize already visited set of nodes + associated with {!Km3.classifier} that the nodes are supposed to represent. *) type known_vtx_classifier = classifier VMap.t let pp_vtx fmt vtx = fprintf fmt "%s" (vtx2str vtx) @@ -123,6 +195,12 @@ fprintf fmt "`enumeration(%a,_)" pp_name name let pp_known_vtx_classifier = pp_vmap_t pp_classifier_simple +(** [vmap] is a map from allit to destination nodes. + [vset_amap_is_empty vamap] holds if the map is empty + or every entry of the map has empty set of nodes. + The latter case never happens if [vmap] is created from a graph. + See {!take_single_allit_dst} for detail. + *) let vset_amap_is_empty (vamap:VSet.t AMap.t) : bool = AMap.fold (fun _ vset b -> b && VSet.is_empty vset) vamap true @@ -137,6 +215,11 @@ | ALLbl str -> str (* String.capitalize str *) | _ -> invalid_arg "typeref_of_allit" +(** [edges_of_graph g] creats an index of vtx -> allit -> PowSet(vtx) from + graph [g]. It is guaranteed that every entry of the map + from allit to VSet.t is nonempty since the entry is only + created when corresponding edge exists. + *) let edges_of_graph (g:graph) : edges = SetofEdge.fold (fun (u,a,v) es -> @@ -144,11 +227,35 @@ let es_u_a = try AMap.find a es_u with Not_found -> VSet.empty in VMap.add u (AMap.add a (VSet.add v es_u_a) es_u) es) g.e VMap.empty +(** [validation_fails vtx reason] prints an error message about + the node [vtx] with string [reason] that explains the error. *) let validation_fails vtx reason = failwith (sprintf "Validation fails at %s: %s@?" (vtx2str vtx) reason) +(** A data structure that represents the outgoing edges from a node. + See {!take_single_allit_dst} for the semantics of the data structure. *) type single_allit_dst = Empty | Single of allit * vtx | Multiple of allit * allit + +(** + [take_single_allit_dst es_v] extracts {!single_allit_dst} + from a map [es_v] from allit to set of vtx. [es_v] represents + outgoing edges of a node. Entries with empty destination + nodes are ignored, because it is impossible if es_v + is taken from {!edges} that is created from a graph, + since the entry is never created without + an edge, which should always have a destination node. + If there are only such kind of entries, then + [Empty] is reported without raising error. + @return [Empty] if the node has no outgoing edges. + [Single][(l,v)] if there is exactly one outgoing edge + labeled [l] to node [v]. + [Multiple][(l1,l2)] if there are more than one outgoing + edges. If every edge is identically labeled, + then l1=l2. Otherwise, l1 <> l2 and they are + the first two labels found. + *) + let take_single_allit_dst (es_v:VSet.t AMap.t) : single_allit_dst = AMap.fold (fun allit dsts -> function | Empty -> begin match VSet.cardinal dsts with @@ -159,15 +266,61 @@ if VSet.is_empty dsts then s else Multiple(al,allit) | Multiple _ as m -> m) es_v Empty +let get_allit_dst (v:vtx) (es:edges) (typeref:name) : (allit * vtx) = + + let es_v = try VMap.find v es (* obtain branches (map from label to PSet(nodes)) *) + (* outgoing edge of v (should be singule) *) + with Not_found -> + validation_fails v + (sprintf "There is no edge for %S" (string_of pp_name typeref)) in + (* take a single edge *) + let allit, dst = match take_single_allit_dst es_v with + | Empty -> + validation_fails v + (sprintf "There is no edge for %s" (string_of pp_name typeref)) + | Single(allit,dst) -> allit, dst + | Multiple(al1,al2) -> + validation_fails v + (sprintf "There are multiple edges %s and %s." + (allit2str al1) (allit2str al2)) in + allit,dst + + + +(** [validate_klasse v es kls mmdic known] checks for each {!Km3.feature} of + the class [kls], if the node [v] of the graph (represented as [es] of + map vtx -> allit -> PowSet(vtx)) has branches that are valid instances + of the feature. Multiplicity and the opposite_of property is checked + here, and validation of each value of the feature is delegated to + {!validate_classifier_vtx}. + @param mmdic metamodel dictionary + @param known map from vtx to classifier that has been already known. + @return map from vtx to classifier accumlated after the validation, + or error is raised if the check failed. + Accumulation of [known] occurs only via {!validate_classifier_vtx}. + The following pattern is checked: + + / + (---Classifier_Name-->)[v]---- + \ + *) let rec validate_klasse_vtx (v:vtx) (es:edges) (kls:klasse) (mmdic:mm_dictionary) (known: known_vtx_classifier) : known_vtx_classifier = - let es_v = try VMap.find v es with Not_found -> AMap.empty in + let _ = dprintf "[validate_klasse_vtx]edges=%a@." pp_edges es in + let _ = dprintf "[validate_klasse_vtx]mmdic=%a@." pp_mm_dictionary mmdic in + let _ = dprintf "[validate_klasse_vtx]known=%a@." pp_known_vtx_classifier known in + (* es_v: map from edge labels (feature name) to set of destination nodes *) + (* known: accumulated map from vtx to the classifier the vtx represents *) + let es_v = try VMap.find v es with Not_found -> AMap.empty in let es_v, known = NameMap.fold (* opposite_of is not supported yet *) (fun fname ft (es_v,known) -> + let _ = dprintf "[NameMap.fold]es_v=%a@." (pp_amap_t pp_vset_t) es_v in + let _ = dprintf "[NameMap.fold]known=%a@." pp_known_vtx_classifier known in let allit = ALLbl fname in let es_v_f = try AMap.find allit es_v with Not_found -> VSet.empty in + let _ = dprintf "[NameMap.fold]es_v_f=%a@." pp_vset_t es_v_f in let f = match ft with | `attribute f | `reference{feature=f;opposite_of=None}-> f | `reference{feature=f;opposite_of=Some op} -> @@ -199,9 +352,10 @@ f in let card = VSet.cardinal es_v_f in if multiplicity_check f.multiplicity card then - (AMap.remove allit es_v, - VSet.fold + (AMap.remove allit es_v, (* exclude already checked edges *) + VSet.fold (* check each value if it is a valid instance of the feature type *) (fun dst known -> + let _ = dprintf "[VSet.fold]known=%a@." pp_known_vtx_classifier known in validate_classifier_vtx dst es f.typeref mmdic known) es_v_f known) else if card = 0 then @@ -213,51 +367,123 @@ "The number of edges %d does not match with its multiplicity %s." card (string_of pp_multiplicity f.multiplicity))) kls.features (es_v,known) in + (* Since the above fold removes all the outgoig edges that represents the features + declared in the metamodel, whatever remain in the new es_v are invalid excess + edges, so ... *) (* choose one edge to show the error if it is not empty *) AMap.iter (fun allit _ -> validation_fails v (sprintf "%s is invalid." (allit2str allit))) es_v; + (* The control reaches here if the es_v is empty, since if es_v is + non-empty, the body of the above iteration would have aborted + with an error message. *) (* just return known if it is empty *) known +(** + [validate_classifier_vtx v es typeref mmdic known] checks the node [v] + of the graph (represented as [es] of map vtx -> allit -> PowSet(vtx)) + to see if the node representes a feature of valid type [typeref] + as described in the feature description of the metamodel dictionary [mmdic]. + Note that all the abstract class entries (key-value pairs) had been removed + from [mmdic] as a preprocess by [clean_mm_dictionary], while + [typeref] may still be one of the removed abstract classes that was in the + original metamodel before the preprocessing. In this case, + if the concrete class in the graph instance is the subclass + of the superclass, then it proceeds with the subclass instead. + The node [v] is supposed to have a singleton edge with capitalized + label that represents a classifier, and this singularity is also checked here. + + @param known map from vtx to classifier that has been already known. + @return map from vtx to classifier accumlated after the validation, + or error is raised if the check failed. + + The edge of the graph checked here is the form + [v]--Classifier_name-->dst + where [v] is pointed by an edge labeled with a feature name. + First, if dst has already been memoized to have type [typ] in [known] map, + then the [typ] is compared to that indicated by [typeref] and if it matches, then + the validation just succeeds. If not, it indicates that the edge + points to the destination dst with unintended type, so the validation fails. + If dst has not been memoized in the [known] map, then first memoize dst with + the type indicated by [typeref], and Classifier_name is checked with the assumed type + (after checking of singularity of outgoing edge of [v]). + If it doesn't match with the assumed type, then the validation fails. + If matches, go on with checking if dst is a valid instance of the assumed type. + If the type is a class type, then the check is delegated to + {!validate_klasse_vtx}. If the type is a primitive data type, + then dst should have only one single edge labeled with the + value of the primitive data type. The Classifier_name is + checked with the data type name. If matches, then + after the singularity check of the value edge, the actual type + of the label of the edge is checked against the name of the primitive data type. + Correspondence of + ("String", ALStr), ("Boolean",ALBol), ("Int", ALInt), ("Float", ALFlt) + is checked. + In case of success, the memo (map) extended from [known] is returned. +*) and validate_classifier_vtx (v:vtx) (es:edges) (typeref:name) (mmdic:mm_dictionary) (known: known_vtx_classifier) : known_vtx_classifier = + let _ = dprintf "[validate_classifier_vtx]es=%a@." pp_edges es in + let _ = dprintf "[validate_classifier_vtx]mmdic=%a@." pp_mm_dictionary mmdic in + let _ = dprintf "[validate_classifier_vtx]known=%a@." pp_known_vtx_classifier known in + (* Resolve the type definition of typeref by the metamodel dictionary mmdic. *) let typ = try NameMap.find typeref mmdic.classifier - with Not_found -> validation_fails v (sprintf "%s is an unknown classifier." - (string_of pp_name typeref)) in - match VMap.find_some v known with - | Some t -> - if t = typ then known + with Not_found -> + (************ BEGIN concrete subclass of abstract class check ***********) + (* Since all abstract classes are eliminated by clean_mm_dictionary, + typeref cannot be found in mmdic if it is an abstract class + (declared in KM3 schema). However, the graph subject to validation + may have the subclass of the abstract class. + So examine the actual edge and if it is a subclass of typeref, then + continue with the subclass type. *) + + let allit,_ = get_allit_dst v es typeref in + + let kname = kname_of_allit allit in + let typ = + try NameMap.find kname mmdic.classifier + with Not_found -> validation_fails v (sprintf "%s is an unknown classifier." + (string_of pp_name kname)) in + match typ with + | `klasse kls -> + List.iter (fun t -> dprintf "supertype=%s@." t) kls.supertypes; + if (List.mem typeref kls.supertypes) then + ((dprintf "subtype %s is found for its supertype %s@." kname typeref);typ) + else + validation_fails v (sprintf "%s is an unknown classifier." + (string_of pp_name kname)) + | _ -> validation_fails v (sprintf "%s is an unknown classifier." + (string_of pp_name kname)) in + (************ END concrete subclass of abstract class check ***********) + (* check the structure v--allit(Classifier name)-->dst *) + match VMap.find_some v known with (* check the memo of node v *) + | Some t -> (* memo hit *) + if t = typ then known (* memo actually stores the type consistent with typeref *) else begin printf "%a@;does not match with@;%a.@." pp_classifier t pp_classifier typ; validation_fails v ("label not matched."^string_of pp_classifier typ) end - | None -> - let known = VMap.add v typ known in - let es_v = try VMap.find v es - with Not_found -> - validation_fails v - (sprintf "There is no edge for %s" (string_of pp_name typeref)) in - (* take a single edge *) - let allit, dst = match take_single_allit_dst es_v with - | Empty -> - validation_fails v - (sprintf "There is no edge for %s" (string_of pp_name typeref)) - | Single(allit,dst) -> allit, dst - | Multiple(al1,al2) -> - validation_fails v - (sprintf "There are multiple edges %s and %s." - (allit2str al1) (allit2str al2)) in + | None -> (* memo didn't hit. first visit of v *) + let known = VMap.add v typ known in (* memoize v with assumed type typ *) + let allit, dst = get_allit_dst v es typeref in + match typ with | `klasse kls -> let allit_kls = allit_of_kname kls.kname in if allit_kls <> allit then validation_fails v (sprintf "%s should be %s." (allit2str allit) (allit2str allit_kls)); + (* check the subgraph beyond dst if it represents a valid instance of kls *) validate_klasse_vtx dst es kls mmdic known | `datatype t -> + (* check for one of the following patterns + v--ALLbl "String" -->dst--ALStr s -->{} + v--ALLbl "Boolean"-->dst--ALBol b -->{} + v--ALLbl "Int" -->dst--ALInt i -->{} + v--ALLbl "Float" -->dst--ALFlt f -->{} *) let allit_t = allit_of_typeref t in if allit_t <> allit then validation_fails v @@ -292,36 +518,69 @@ (* It just returns vertex mapping to classifier if validation succeed. *) (* Othewise an error is raised. *) +(** [validate g pname mm] validates the graph [g] with respect to package [pname] + in the metamodel [mm] and returns a map from vtx to classifier if validation succeed. + Otherwise an error is raised. + For the graph [g], the following conditions are checked by [validate] itself: + 1. non-empty (have at least one edge at the top level) + 2. have exactly one default root marker + 3. each top-level edge should + 3-1. have labeled with a name using ALLbl. + 3-2. the label represents the name of a classifier declared in the metamodel [mm]. + 3-3. the classifier should be a class (datatype and enumeration are disallowed) + The subgraphs following the top-level edges are checked by {!validate_klasse_vtx}. + Each entry of the result map corresponds to an edge + vtx--Classifier_Name-->dst + and maps vtx to its data type description, of which dst is the valid instance, + assuming that the edge is the only outgoing edge of vtx. + Snce the root node is an exception of this (have multiple edges of + this shape), the root is not registered in the result map. + *) let validate (g:graph) (pname:name) (mm:metamodel) : known_vtx_classifier = match SetofInodeR.cardinal g.i with | 1 -> let edges = edges_of_graph g in + let _ = dprintf "edges=%a@." pp_edges edges in let mmdic = clean_mm_dictionary (make_mm_dictionary mm) in + let _ = dprintf "mmdic=%a@." pp_mm_dictionary mmdic in let (_,root) as inodeR = SetofInodeR.min_elt g.i in if isroot inodeR then let kset = try NameMap.find pname mmdic.package with - Not_found -> failwith "validate: fatal error!" in + Not_found -> failwith (Format.sprintf "validate: unknown package %s." (string_of pp_name pname)) in let es_root = try VMap.find root edges with Not_found -> failwith "validate: graph is empty." in - let allit_fails allit = - validation_fails root (sprintf "%s is invalid." (allit2str allit)) in + let _ = dprintf "es_root=%a@." (pp_amap_t pp_vset_t) es_root in + let allit_fails allit reason = + validation_fails root (sprintf "%s is invalid. %s" (allit2str allit) reason) in AMap.fold (fun allit dsts known -> + let _ = dprintf "dsts=%a@." pp_vset_t dsts in + let _ = dprintf "known=%a@." pp_known_vtx_classifier known in let kname = try kname_of_allit allit - with _ -> allit_fails allit in - if not(NameSet.mem kname kset) then allit_fails allit; + with _ -> allit_fails allit (sprintf "Invalid type of label at the top." ) in + if not(NameSet.mem kname kset) then + (* Top-level edge represents a classifier that do not belong + to the package [pname]. It may be the case that allit + reprecents non-class datatype, since these are not + registered to mmdic.package *) + allit_fails allit (sprintf "Unknown classifier %S" kname); let kls = try match NameMap.find kname mmdic.classifier with | `klasse kls -> kls - | clsf -> allit_fails allit - with Not_found -> allit_fails allit in + | clsf -> + (* this case is impossible since mmdic.package only stores the + (non-abstract) classes *) + allit_fails allit (sprintf "non class classifier at the top level.") + with Not_found -> + (* this case is impossible since all entries of mmdic.package + are also found in mmdic.classifier *) + allit_fails allit (sprintf "unknown classifier.") in VSet.fold (fun dst known -> + let _ = dprintf "[VSet.fold]dsts=%a@." pp_vset_t dsts in + let _ = dprintf "[VSet.fold]known=%a@." pp_known_vtx_classifier known in validate_klasse_vtx dst edges kls mmdic known) dsts known) es_root VMap.empty else failwith "No root node is found." | n -> failwith(sprintf "The number of input markers should be 1 (not %d)." n) - - - diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/uncal/lexUnCAL.mll /tmp/ground_tram-0.9.3-new/src/uncal/lexUnCAL.mll --- /tmp/ground_tram-0.9.3-org/src/uncal/lexUnCAL.mll 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/uncal/lexUnCAL.mll 2013-02-19 07:56:49.000000000 +0900 @@ -75,6 +75,7 @@ | '-' { MINUS } | '*' { STAR } | '/' { SLASH } +| '%' { PERCENT } | '^' { HAT } | '!' { BAN } | "?" { UKN } diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/uncal/parseUnCAL.mly /tmp/ground_tram-0.9.3-new/src/uncal/parseUnCAL.mly --- /tmp/ground_tram-0.9.3-org/src/uncal/parseUnCAL.mly 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/uncal/parseUnCAL.mly 2013-02-19 07:56:49.000000000 +0900 @@ -15,7 +15,7 @@ %token COLON_EQ ATMARK CYCLE REC BACKSLASH DOT %token IF THEN ELSE LET LLET IN %token AND OR NOT ISEMPTY BISIMILAR EQ LT GT ISEMPTY ISINT ISBOOL ISSTRING ISLABEL ISFLOAT -%token PLUS MINUS STAR SLASH HAT BAN UKN ATAT +%token PLUS MINUS STAR SLASH PERCENT HAT BAN UKN ATAT %token BOOL %token INT %token FLOAT @@ -37,7 +37,7 @@ %left EQ %nonassoc LT GT %left HAT PLUS MINUS -%left STAR SLASH +%left STAR SLASH PERCENT %left ATAT /* high */ @@ -138,6 +138,8 @@ { return ~ntsym:"alpat_albinop_alpat" (ALBin({annot=None},$1,ALMul,$3)) } | alpat SLASH alpat { return ~ntsym:"alpat_albinop_alpat" (ALBin({annot=None},$1,ALDiv,$3)) } +| alpat PERCENT alpat +{ return ~ntsym:"alpat_albinop_alpat" (ALBin({annot=None},$1,ALMod,$3)) } | alpat HAT alpat { return ~ntsym:"alpat_albinop_alpat" (ALBin({annot=None},$1,ALConc,$3)) } | LPAREN alpat_albinop_alpat RPAREN diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/uncal/printUnCAL.ml /tmp/ground_tram-0.9.3-new/src/uncal/printUnCAL.ml --- /tmp/ground_tram-0.9.3-org/src/uncal/printUnCAL.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/uncal/printUnCAL.ml 2013-02-19 07:56:49.000000000 +0900 @@ -70,8 +70,10 @@ let albinop_gt = function ALAdd,ALMul -> true | ALAdd,ALDiv -> true + | ALAdd,ALMod -> true | ALSub,ALMul -> true | ALSub,ALDiv -> true + | ALSub,ALMod -> true | _ ,_ -> false (** Annotation printing @@ -253,6 +255,7 @@ | ALSub -> fprintf ppf "%s" "-" | ALMul -> fprintf ppf "%s" "*" | ALDiv -> fprintf ppf "%s" "/" + | ALMod -> fprintf ppf "%s" "%%" | ALConc -> fprintf ppf "%s" "^" and ppr_allit ppf = function ALLbl (l) -> fprintf ppf "%s" l diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/uncal/unCAL.ml /tmp/ground_tram-0.9.3-new/src/uncal/unCAL.ml --- /tmp/ground_tram-0.9.3-org/src/uncal/unCAL.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/uncal/unCAL.ml 2013-02-19 07:56:49.000000000 +0900 @@ -38,7 +38,7 @@ | ALLit of 'a * allit (* a a \in Label *) (* label literal *) | ALBin of 'a * 'a alpat * albinop * 'a alpat (* L BOP L *) (* EXTENSION *) and albinop = - ALAdd | ALSub | ALMul | ALDiv | ALConc (* + - * / ^ *) + ALAdd | ALSub | ALMul | ALDiv | ALMod | ALConc (* + - * / % ^ *) and 'a abexpr = (* B ::= *) (* boolean expr *) AIsemp of 'a * 'a aexpr (* isempty(E) *) | ABisim of 'a * 'a aexpr * 'a aexpr (* bisimilar(E,E) *) (* EXTENSION *) diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/unql/printUnQL.ml /tmp/ground_tram-0.9.3-new/src/unql/printUnQL.ml --- /tmp/ground_tram-0.9.3-org/src/unql/printUnQL.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/unql/printUnQL.ml 2013-02-19 07:56:49.000000000 +0900 @@ -215,7 +215,7 @@ `tree (_, ttlist) -> fprintf ppf "{@[%a@]}" (pr_forest pp_tree_label_colon_template) ttlist | #variable as v -> fprintf ppf "%a" pp_variable v - | `expr(_,e) -> fprintf ppf "%a" pp_expr e + | `expr(_,e) -> fprintf ppf "(%a)" pp_expr e | `union (_,t1,t2) -> fprintf ppf "%a@ U %a" pp_template t1 pp_template t2 | `app_exp (_,fn,t1) -> fprintf ppf "%a(@[%a@])" pp_fun_name fn pp_template t1 | `let_exp (_,d,t1) -> fprintf ppf "@[let@\n%a in@]@\n%a" diff -Nur -X /Users/hidaka/proj/big/git/BiG/src/.gitignore -X /Users/hidaka/proj/big/git/BiG/src/.gitignore-patch /tmp/ground_tram-0.9.3-org/src/util/fputil.ml /tmp/ground_tram-0.9.3-new/src/util/fputil.ml --- /tmp/ground_tram-0.9.3-org/src/util/fputil.ml 2012-08-27 19:24:39.000000000 +0900 +++ /tmp/ground_tram-0.9.3-new/src/util/fputil.ml 2013-02-19 07:56:49.000000000 +0900 @@ -41,7 +41,7 @@ | (x::xs) -> List.fold_left f x xs | [] -> failwith "Fputil.fold_left1: empty list" -(* Useful to implemente fuctions given in the form of list comprehension *) +(* Useful to implement fuctions given in the form of list comprehension *) let concatMap f x = List.concat (List.map f x) (* check if all member has equal value of prop *)