Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FunctorParsing.ml @ de84f40d

History | View | Annotate | Download (6.72 KB)

1
(* Parsing strings to sort tables *)
2
module CM = CoAlgMisc
3

    
4
type functorExp =
5
    | Choice of functorExp * functorExp
6
    | Fusion of functorExp * functorExp
7
    | Composition of functorExp * functorExp
8
    | Unary of string list (* a non-empty list of identifiers *)
9

    
10
let rec stringFromFunctorExp = function
11
    | Unary str -> String.concat " " str
12
    | Composition (a,b) -> "("^(stringFromFunctorExp a)^" . "^(stringFromFunctorExp b)^")"
13
    | Choice (a,b) -> "("^(stringFromFunctorExp a)^" + "^(stringFromFunctorExp b)^")"
14
    | Fusion (a,b) -> "("^(stringFromFunctorExp a)^" * "^(stringFromFunctorExp b)^")"
15

    
16
(* example
17
    Choice (Unary ["K"], Fusion (Unary ["KD"], Unary ["GML"]))
18
*)
19

    
20

    
21
let explode (s:string) : char list =
22
  let rec exp i l =
23
    if i < 0 then l else exp (i - 1) (s.[i] :: l) in
24
  exp (String.length s - 1) [];;
25

    
26
let implode (l:char list) : string =
27
  let res = String.create (List.length l) in
28
  let rec imp i = function
29
  | [] -> res
30
  | c :: l -> res.[i] <- c; imp (i + 1) l in
31
  imp 0 l;;
32

    
33
let string_of_char : char -> string = String.make 1
34

    
35
exception FunctorParsingFailed of string
36

    
37
type state = ParseSum | ParseProduct | ParseComposition | ParseFactor
38

    
39
let functorExpFromString str : functorExp =
40
    let stream = Stream.of_string str in
41
    let error str =
42
        let msg = "At char "^(string_of_int (Stream.count stream))^": "^str in
43
        raise (FunctorParsingFailed msg)
44
    in
45
    let rec dropWhitespace () =
46
        match (Stream.peek stream) with
47
        | Some '\n'
48
        | Some '\t'
49
        | Some ' ' -> (Stream.junk stream ; dropWhitespace ())
50
        | _ -> ()
51
    in
52
    (* try to parse an identifier as long as possible *)
53
    let identifier () =
54
        let rec ident () =
55
        match (Stream.peek stream) with
56
        | None -> []
57
        | Some ch ->
58
            if (Str.string_match (Str.regexp "[a-zA-Z0-9]") (string_of_char ch) 0)
59
            then (Stream.junk stream ; ch::(ident ()))
60
            else []
61
        in
62
        implode (ident ())
63
    in
64
    (* try to parse as many identifiers, separated by whitespace, as possible *)
65
    let rec identifier_list () =
66
        dropWhitespace ();
67
        let i = identifier () in (* get the next identifier *)
68
        if (String.length i <> 0)
69
        then i::(identifier_list ())
70
        else []
71
    in
72
    let nonempty_identifier_list () =
73
        let idlist = identifier_list () in
74
        if List.length idlist <> 0
75
        then idlist
76
        else error "Expected list of at least one identifiers but got none"
77
    in
78
    let rec parse (state:state) : functorExp =
79
        let _ = dropWhitespace () in
80
        let binary (operator:char) (nextStep: state)
81
            (join: functorExp -> functorExp) : functorExp =
82
            let s1 = parse nextStep in (* get the first operator *)
83
            dropWhitespace ();
84
            match (Stream.peek stream) with
85
            | Some op when op = operator -> (Stream.junk stream; join s1)
86
            | _ -> s1
87
        in
88
        match state with
89
        | ParseSum ->
90
            binary '+' ParseProduct (fun s1 -> Choice (s1,parse ParseSum))
91
        | ParseProduct ->
92
            binary '*' ParseComposition (fun s1 -> Fusion (s1,parse ParseProduct))
93
        | ParseComposition ->
94
            binary '.' ParseFactor (fun s1 -> Composition (s1,parse ParseComposition))
95
        | ParseFactor -> begin
96
            match (Stream.peek stream) with
97
            | Some '(' -> begin
98
                Stream.junk stream;
99
                let x = parse ParseSum in
100
                dropWhitespace ();
101
                match (Stream.peek stream) with
102
                | Some ')' -> (Stream.junk stream; x)
103
                | _ -> error "Missing closing )"
104
              end
105
            | None -> error "Expected identifier but got end of string"
106
            | Some ch -> Unary (nonempty_identifier_list ())
107
          end
108
    in
109
    let result = parse ParseSum in
110
    dropWhitespace ();
111
    match (Stream.peek stream) with
112
    | Some ch -> error "Unparseable remaining string"
113
    | None -> ();
114
    result
115

    
116

    
117
let sortTableFromFunctorExp (fe:functorExp) : CoAlgReasoner.sortTable =
118
    let logicName2Functor str params = match (CM.unaryfunctor_of_string str params) with
119
    | Some x -> x
120
    | None -> raise (FunctorParsingFailed ("Unknown Functor name or invalid number of parameters passed"^str))
121
    in
122
    let line = ref(0) in
123
    let getLineNr () =
124
        let nr = !line in
125
        line := nr + 1;
126
        nr
127
    in
128
    let rec generateSorts (fe:functorExp):
129
        ((int -> (CM.functors * int list) list) * int) =
130
        (* generate sortTable lines for that functor and tell its line number
131
            the int-parameter is the sort that is given to the functorExp fe.
132
            So after generating the lines, you can insert the parameter-sort
133
            afterwards.
134
        *)
135
        match fe with
136
        | Unary str_list ->
137
            let nr = getLineNr () in
138
            let functorname = List.hd str_list in
139
            (fun parameter -> [ (logicName2Functor functorname (List.tl str_list), [parameter])]), nr
140
        | Choice (a,b) ->
141
            let nr = getLineNr () in
142
            let (a_table, a_nr) = generateSorts a in
143
            let (b_table, b_nr) = generateSorts b in
144
            (fun p ->
145
            ((CM.Choice, [a_nr; b_nr])::(List.append (a_table p) (b_table p)))), nr
146
        | Fusion (a,b) ->
147
            let nr = getLineNr () in
148
            let (a_table, a_nr) = generateSorts a in
149
            let (b_table, b_nr) = generateSorts b in
150
            (fun p -> ((CM.Fusion, [a_nr; b_nr])::(List.append (a_table p) (b_table p)))), nr
151
        | Composition (a,b) ->
152
            (*
153
                Example: K . CL should be generated as:
154
                    0 = K(CL(0))
155
                i.e.:
156
                    0 = K (1)
157
                    1 = CL(0)
158
                visually:
159

    
160
                 <-------a-----.   .---< p
161
                               |   |
162
                   .-----------'   |
163
                   |               |
164
                   '- <--b---- <---'
165
            *)
166
            let (a_table, a_nr) = generateSorts a in
167
            let (b_table, b_nr) = generateSorts b in
168
            (* feed the result of b into a as a parameter *)
169
            (fun p -> (List.append (a_table b_nr) (b_table p))), a_nr
170
    in
171
    let fst (x,_ ) = x in
172
    Array.of_list (fst (generateSorts fe) 0)
173

    
174
let stringFromSortTable (sorts: CoAlgReasoner.sortTable) : string =
175
    let printLine ((f,params) : CM.functors* int list) =
176
        let params_str = String.concat ";" (List.map string_of_int params) in
177
        (CM.string_of_functor f) ^ " [" ^ params_str ^ "];"
178
    in
179
    String.concat "\n" (List.map printLine (Array.to_list sorts))
180

    
181
let sortTableFromString str : CoAlgReasoner.sortTable =
182
    let str = sortTableFromFunctorExp (functorExpFromString str) in
183
    (*print_endline (stringFromSortTable str);*)
184
    str
185