Profile

Statistics
| Branch: | Revision:

cool / src / lib / FunctorParsing.ml @ de84f40d

 1 ```(* Parsing strings to sort tables *) ``` ```module CM = CoAlgMisc ``` ```type functorExp = ``` ``` | Choice of functorExp * functorExp ``` ``` | Fusion of functorExp * functorExp ``` ``` | Composition of functorExp * functorExp ``` ``` | Unary of string list (* a non-empty list of identifiers *) ``` ```let rec stringFromFunctorExp = function ``` ``` | Unary str -> String.concat " " str ``` ``` | Composition (a,b) -> "("^(stringFromFunctorExp a)^" . "^(stringFromFunctorExp b)^")" ``` ``` | Choice (a,b) -> "("^(stringFromFunctorExp a)^" + "^(stringFromFunctorExp b)^")" ``` ``` | Fusion (a,b) -> "("^(stringFromFunctorExp a)^" * "^(stringFromFunctorExp b)^")" ``` ```(* example ``` ``` Choice (Unary ["K"], Fusion (Unary ["KD"], Unary ["GML"])) ``` ```*) ``` ```let explode (s:string) : char list = ``` ``` let rec exp i l = ``` ``` if i < 0 then l else exp (i - 1) (s.[i] :: l) in ``` ``` exp (String.length s - 1) [];; ``` ```let implode (l:char list) : string = ``` ``` let res = String.create (List.length l) in ``` ``` let rec imp i = function ``` ``` | [] -> res ``` ``` | c :: l -> res.[i] <- c; imp (i + 1) l in ``` ``` imp 0 l;; ``` ```let string_of_char : char -> string = String.make 1 ``` ```exception FunctorParsingFailed of string ``` ```type state = ParseSum | ParseProduct | ParseComposition | ParseFactor ``` ```let functorExpFromString str : functorExp = ``` ``` let stream = Stream.of_string str in ``` ``` let error str = ``` ``` let msg = "At char "^(string_of_int (Stream.count stream))^": "^str in ``` ``` raise (FunctorParsingFailed msg) ``` ``` in ``` ``` let rec dropWhitespace () = ``` ``` match (Stream.peek stream) with ``` ``` | Some '\n' ``` ``` | Some '\t' ``` ``` | Some ' ' -> (Stream.junk stream ; dropWhitespace ()) ``` ``` | _ -> () ``` ``` in ``` ``` (* try to parse an identifier as long as possible *) ``` ``` let identifier () = ``` ``` let rec ident () = ``` ``` match (Stream.peek stream) with ``` ``` | None -> [] ``` ``` | Some ch -> ``` ``` if (Str.string_match (Str.regexp "[a-zA-Z0-9]") (string_of_char ch) 0) ``` ``` then (Stream.junk stream ; ch::(ident ())) ``` ``` else [] ``` ``` in ``` ``` implode (ident ()) ``` ``` in ``` ``` (* try to parse as many identifiers, separated by whitespace, as possible *) ``` ``` let rec identifier_list () = ``` ``` dropWhitespace (); ``` ``` let i = identifier () in (* get the next identifier *) ``` ``` if (String.length i <> 0) ``` ``` then i::(identifier_list ()) ``` ``` else [] ``` ``` in ``` ``` let nonempty_identifier_list () = ``` ``` let idlist = identifier_list () in ``` ``` if List.length idlist <> 0 ``` ``` then idlist ``` ``` else error "Expected list of at least one identifiers but got none" ``` ``` in ``` ``` let rec parse (state:state) : functorExp = ``` ``` let _ = dropWhitespace () in ``` ``` let binary (operator:char) (nextStep: state) ``` ``` (join: functorExp -> functorExp) : functorExp = ``` ``` let s1 = parse nextStep in (* get the first operator *) ``` ``` dropWhitespace (); ``` ``` match (Stream.peek stream) with ``` ``` | Some op when op = operator -> (Stream.junk stream; join s1) ``` ``` | _ -> s1 ``` ``` in ``` ``` match state with ``` ``` | ParseSum -> ``` ``` binary '+' ParseProduct (fun s1 -> Choice (s1,parse ParseSum)) ``` ``` | ParseProduct -> ``` ``` binary '*' ParseComposition (fun s1 -> Fusion (s1,parse ParseProduct)) ``` ``` | ParseComposition -> ``` ``` binary '.' ParseFactor (fun s1 -> Composition (s1,parse ParseComposition)) ``` ``` | ParseFactor -> begin ``` ``` match (Stream.peek stream) with ``` ``` | Some '(' -> begin ``` ``` Stream.junk stream; ``` ``` let x = parse ParseSum in ``` ``` dropWhitespace (); ``` ``` match (Stream.peek stream) with ``` ``` | Some ')' -> (Stream.junk stream; x) ``` ``` | _ -> error "Missing closing )" ``` ``` end ``` ``` | None -> error "Expected identifier but got end of string" ``` ``` | Some ch -> Unary (nonempty_identifier_list ()) ``` ``` end ``` ``` in ``` ``` let result = parse ParseSum in ``` ``` dropWhitespace (); ``` ``` match (Stream.peek stream) with ``` ``` | Some ch -> error "Unparseable remaining string" ``` ``` | None -> (); ``` ``` result ``` ```let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable = ``` ``` let logicName2Functor str params = match (CM.unaryfunctor_of_string str params) with ``` ``` | Some x -> x ``` ``` | None -> raise (FunctorParsingFailed ("Unknown Functor name or invalid number of parameters passed"^str)) ``` ``` in ``` ``` let line = ref(0) in ``` ``` let getLineNr () = ``` ``` let nr = !line in ``` ``` line := nr + 1; ``` ``` nr ``` ``` in ``` ``` let rec generateSorts (fe:functorExp): ``` ``` ((int -> (CM.functors * int list) list) * int) = ``` ``` (* generate sortTable lines for that functor and tell its line number ``` ``` the int-parameter is the sort that is given to the functorExp fe. ``` ``` So after generating the lines, you can insert the parameter-sort ``` ``` afterwards. ``` ``` *) ``` ``` match fe with ``` ``` | Unary str_list -> ``` ``` let nr = getLineNr () in ``` ``` let functorname = List.hd str_list in ``` ``` (fun parameter -> [ (logicName2Functor functorname (List.tl str_list), [parameter])]), nr ``` ``` | Choice (a,b) -> ``` ``` let nr = getLineNr () in ``` ``` let (a_table, a_nr) = generateSorts a in ``` ``` let (b_table, b_nr) = generateSorts b in ``` ``` (fun p -> ``` ``` ((CM.Choice, [a_nr; b_nr])::(List.append (a_table p) (b_table p)))), nr ``` ``` | Fusion (a,b) -> ``` ``` let nr = getLineNr () in ``` ``` let (a_table, a_nr) = generateSorts a in ``` ``` let (b_table, b_nr) = generateSorts b in ``` ``` (fun p -> ((CM.Fusion, [a_nr; b_nr])::(List.append (a_table p) (b_table p)))), nr ``` ``` | Composition (a,b) -> ``` ``` (* ``` ``` Example: K . CL should be generated as: ``` ``` 0 = K(CL(0)) ``` ``` i.e.: ``` ``` 0 = K (1) ``` ``` 1 = CL(0) ``` ``` visually: ``` ``` <-------a-----. .---< p ``` ``` | | ``` ``` .-----------' | ``` ``` | | ``` ``` '- <--b---- <---' ``` ``` *) ``` ``` let (a_table, a_nr) = generateSorts a in ``` ``` let (b_table, b_nr) = generateSorts b in ``` ``` (* feed the result of b into a as a parameter *) ``` ``` (fun p -> (List.append (a_table b_nr) (b_table p))), a_nr ``` ``` in ``` ``` let fst (x,_ ) = x in ``` ``` Array.of_list (fst (generateSorts fe) 0) ``` ```let stringFromSortTable (sorts: CoAlgReasoner.sortTable) : string = ``` ``` let printLine ((f,params) : CM.functors* int list) = ``` ``` let params_str = String.concat ";" (List.map string_of_int params) in ``` ``` (CM.string_of_functor f) ^ " [" ^ params_str ^ "];" ``` ``` in ``` ``` String.concat "\n" (List.map printLine (Array.to_list sorts)) ``` ```let sortTableFromString str : CoAlgReasoner.sortTable = ``` ``` let str = sortTableFromFunctorExp (functorExpFromString str) in ``` ``` (*print_endline (stringFromSortTable str);*) ``` ``` str ```